如何在Coq中使用证明引理

Question

表面上看来，我无法解决以下问题。这种归纳类型适用于偶数自然数和经过证明的引理，表示将两个偶数相加会产生一个偶数。

Inductive even : nat -> Prop :=
| O_even : even 0
| plus_2_even : forall n:nat, even n -> even (S (S n)).

Lemma lm_even1: forall n p:nat, even n -> even p -> even (n + p).

我想证明n + 2是偶数的特殊情况：

Lemma lm_even2: forall n: nat, even n -> even (n + 2).

更通用的lm_even1在这里会派上用场，但我在应用，重写等方面的努力一直失败，以表示lm_even2与“ p = 2”相同。帮助将不胜感激。

Answer 1

如果您（明确地）向我们展示您的尝试，可能会得到更好的答案。仅有apply和其他一种或两种基本战术的简短证明，但也许您在某个地方有误会。从长远来看，纠正这种误解将对您更有帮助。

---

我们应该先介绍所有前提。对此有充分的理由，我将在下面进行讨论。

Lemma lm_even2: forall n: nat, even n -> even (n + 2).
Proof.
  intros.

现在证明状态为

1 subgoal
n : nat
H : even n
______________________________________(1/1)
even (n + 2)

现在我们处于apply lm_even1.的位置。 apply term.试图统一目标的term类型，可能从左到右填充term的参数（如果是某种功能）。

例如，apply lm_even1.首先会尝试与完整类型统一

forall n p : nat, even n -> even p -> even (n + p)

然后将尝试将某些变量确定为第一个参数（类型为nat：]]]

forall p : nat, even ?n -> even p -> even (?n + p)
然后对p相同：even ?n -> even ?p -> even (?n + ?p)。接下来，由于它仍然是函数类型，因此可以通过使用一些未知变量来填充类型even ?n的参数：even ?p -> even (?n + ?p)，最后是even (?n + ?p)。

唯一可以达到目标的是最后一个：even (?n + ?p)与?n = n和?p = 2。如果我们没有引入变量，那么这根本就行不通，因为其他类型都不符合最初的目标。

Lemma lm_even2: forall n: nat, even n -> even (n + 2).
Proof.
  intros.
  apply lm_even1.
现在证明状态为

2 subgoals
n : nat
H : even n
______________________________________(1/2)
even n
______________________________________(2/2)
even 2
所以我们有两个目标：even n和even 2。使用前提和even的定义，两者都应该很容易达到。