使用策略通过互归纳证明偶数 + 偶数 = 偶数

Question

我正在 Coq 中尝试互感应，我定义的第一个类型是

Inductive IsEven : nat -> Prop :=
  | EvenO : IsEven O
  | EvenS n : IsOdd n -> IsEven (S n)
with IsOdd : nat -> Prop :=
  | OddS n : IsEven n -> IsOdd (S n).

我现在想证明偶数之和是偶数。我可以使用固定点和模式匹配来做到这一点：

Fixpoint even_plus_even (n m : nat) (evenn : IsEven n) (evenm : IsEven m) : IsEven (n + m) :=
match evenn with
  | EvenO => evenm
  | EvenS n' oddn' => EvenS (n' + m) (odd_plus_even n' m oddn' evenm)
end
with odd_plus_even (n m : nat) (oddn : IsOdd n) (evenm : IsEven m) : IsOdd (n + m) :=
match oddn with
  | OddS n' evenn' => OddS (n' + m) (even_plus_even n' m evenn' evenm)
end.

这定义了even_plus_even和odd_plus_even。我现在想以更简洁的方式使用策略来证明这一点（最好不使用许多预定义的引理来使代码尽可能独立），但我还没有走得太远。

具体来说，是否可以像使用 Fixpoint 一样仅使用一个引理even_plus_even来证明两者？odd_plus_even

编辑：非常感谢您的回答，Lemma ... with ...语法正是我正在寻找的。实际上

Lemma even_plus_even2 (n m : nat) (evenn : IsEven n) (evenm : IsEven m) : IsEven (n + m)
  with odd_plus_even2 (n m : nat) (oddn : IsOdd n)   (evenm : IsEven m) : IsOdd  (n + m).
Proof.
  induction evenn; simpl. assumption. constructor. auto.
  induction oddn;  simpl.             constructor. auto.
Defined.

生成与我原来问题中完全相同的证明项Fixpoint。

Answer 1

Coq 中支持互感应。我知道有两种方法，但我只记得如何使用一种：

1. 组合方案

下面是它的工作原理：

Scheme IsEven_ind2 := Induction for IsEven Sort Prop
  with IsOdd_ind2  := Induction for IsOdd Sort Prop.

Combined Scheme IsEvenOdd_ind from IsEven_ind2, IsOdd_ind2. 

Lemma foo: (forall (n: nat) (evenn: IsEven n), forall m (evenm: IsEven m), IsEven (n + m) ) /\
           (forall (n: nat) (oddn: IsOdd n), forall m (evenm: IsEven m), IsOdd (n + m)).
Proof.
apply IsEvenOdd_ind.
- now intros m hm.
- intros h hn hi m hm.
  rewrite plus_Sn_m.
  apply EvenS.
  now apply hi.
- intros h hn hi m hm.
  rewrite plus_Sn_m.
  apply OddS.
  now apply hi.
Qed.

2. Lemma with

在这个问题上，我只是不知道如何完成它，但这是一个语法问题iirc：

Lemma foo: forall (n m: nat) (evenn: IsEven n) (evenm: IsEven m), IsEven (n + m)
with bar:  forall (n m: nat) (oddn: IsOdd n) (evenm: IsEven m), IsOdd (n + m).
Proof.
- intros n m hn; revert m; induction hn as [ | p hp]; intros m hm; simpl in *.
  + exact hm.
  + now apply EvenS; apply bar.
- intros n m hn hm; revert n hn; induction hm as [ | p hp]; intros n hn; simpl in *.
  + now apply bar; [ exact hn | apply EvenO ].
  + apply bar; [ exact hn | ].
    now apply EvenS.
(* can't Qed, I get a Error: Cannot guess decreasing argument of fix. *)
Qed.

编辑： 这是解决方案的有效语法Lemma with。

Lemma foo (n: nat) (evenn: IsEven n): forall (m: nat) (evenm: IsEven m), IsEven (n + m)
 with bar (n: nat) (oddn:  IsOdd  n): forall (m: nat) (evenm: IsEven m), IsOdd  (n + m).
Proof.
- induction evenn as [ | p hp]; intros m hm; simpl in *.
  + exact hm.
  + now apply EvenS; apply bar.
- induction oddn as [p hp]; intros n hn; simpl in *.
  + apply OddS.
    now apply foo.
Qed.