问Coq中如何使用证明引理

EN

如果你(明确地)告诉我们你尝试过什么，你可能会得到一个更好的答案。有一个简短的证据，只有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。