使用策略通过互感应证明 even + even = even

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 和模式匹配来做到这一点：

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 支持互感。我知道两种方法，但我只记得如何使用一种方法：

组合方案

工作原理如下：

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.

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.

Answer 2

例如，您可以通过 "anding" 将两个引理同时证明为一个引理，然后使用 proj1 和 [=14= 提取子句的左侧或右侧部分].

Lemma even_or_odd_plus_even:  forall (n m : nat),
    (forall (evenn : IsEven n) (evenm : IsEven m), IsEven (n + m)) /\
    (forall (oddn : IsOdd n) (evenm : IsEven m), IsOdd (n + m)).
Proof.
  induction n; split; intros;
    try destruct (IHn m) as [He Ho];
    try apply evenm;
    try inversion oddn;
    try inversion evenn;
    constructor; auto.
Qed.

Definition even_plus_even n m := proj1 (even_or_odd_plus_even n m).
Definition odd_plus_even n m := proj2 (even_or_odd_plus_even n m).

给你

even_plus_even : forall n m : nat, IsEven n -> IsEven m -> IsEven (n + m)
odd_plus_even  : forall n m : nat, IsOdd n -> IsEven m -> IsOdd (n + m)

请注意，这两个子句共享 n 和 m，如果子句不能单独证明，因为它们需要相互依赖，则需要这样做。（但在这种特殊情况下，他们没有。您可以单独证明这些陈述，正如 Anton 所展示的那样。）

编辑：刚看到 Vinz 解决方案。我不知道 Lemma 有 with 语法（感谢展示！），但这是有道理的，我认为这是一种更简洁的方式来完成这个相互依赖的定义。

Lemma even_plus_even: forall n m, IsEven n -> IsEven m -> IsEven (n+m)
 with odd_plus_even: forall n m, IsOdd n -> IsEven m -> IsOdd (n+m).
Proof.
  induction 1; simpl; auto using EvenS.
  induction 1; simpl; auto using OddS.
Qed.

使用策略通过互感应证明 even + even = even

Proving even + even = even with mutual induction using tactics

coq