简化证明 Proof by Simplification

现在，我们已经定义了一些数据类型和功能，让我们来说明和证明其行为的属性。实际上，我们已经开始这样做：前几个部分的每个 Example 都对某些特定输入中某些功能的行为做出精确声明。这些声明的证据总是相同的：使用 simpl 来简化方程的两侧，然后使用 reflexivity 来检查双方是否包含相同的值。

Theorem plus_O_n

同样的"简化证明"也可以用来证明更有趣的属性。例如，只要观察 0 + n 减少到n，无论 n 是什么，都可以直接从 plus 的定义中读取 0 是中性元素这一事实。

Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.
  intros n. simpl. reflexivity.  Qed.

（您可能会注意到，上述陈述看起来不同.v文件在您的 IDE 比它在 HTML 再现在您的浏览器。在.v文件，我们使用保留的标识符"forall"编写通用量化器∀。 当.v文件转换为 HTML，这被转换为标准倒置 A 符号。 这是一个好地方，值得一提的是，reflexivity 比我们承认的要强大一些。在我们所看到的例子中，实际上不需要要求 simpl ，因为 reflexivity 在检查双方是否相等时可以自动执行一些简化： simpl 只是添加，以便我们可以看到中间状态 - 简化后，但在完成证明之前。以下是定理的较短证明：

Theorem plus_O_n'

Theorem plus_O_n' : forall n : nat, 0 + n = n.
Proof.
  intros n. reflexivity. Qed.

Proof.

1 subgoal
______________________________________(1/1)
forall n : nat, 0 + n = n

intros n.

1 subgoal
n : nat
______________________________________(1/1)
0 + n = n

simpl.

1 subgoal
n : nat
______________________________________(1/1)
n = n

此外，如果知道 reflexivity 比 simpl 要简单一些，那也是有益的——例如，它尝试"展开"定义的术语，用右侧替换它们。造成这种差异的原因是，如果反射成功，整个目标就完成了，我们不需要看所有这些简化和展开所创造的任何扩展的表达 reflexivity ：相比之下，simpl 用于我们可能必须阅读和理解它创造的新目标的情况下，因此我们不希望它盲目地扩展定义，使目标处于混乱状态。

我们刚才陈述的定理形式及其证据几乎和我们之前看到的简单例子完全相同：只有几个区别。

首先，我们使用了关键字 Theorem 而不是 Example 。这种差异主要是风格问题：关键字 Example 和Theorem（以及其他几个，包括 Lemma，Fact和 Markup ）对 Coq 来说几乎是一回事。

其次，我们增加了量化器 forall n:nat，以便我们的定理谈论所有自然数字 n 。非正式地，为了证明这种形式的定理，我们通常从说"假设n是某个数字..."从形式上讲，这是通过 Inros n 在证明中实现的，它从目标中的量化器移动到当前假设的上下文。请注意，我们本可以在 Intros 条款中使用另一个标识符而不是n（当然，这可能会混淆人类读者的证明）：

Theorem plus_O_n''

Theorem plus_O_n'' : forall n : nat, 0 + n = n.
Proof.
  intros m. reflexivity. Qed.

Proof.

1 subgoal
______________________________________(1/1)
forall n : nat, 0 + n = n

intros m.

1 subgoal
m : nat
______________________________________(1/1)
0 + m = m

关键词 Intros, simpl, 和 reflexivity 是 tactics 的例子。Tactic 是在 Proof 和 Qed 之间使用的命令，用于指导检查我们提出某些声明的过程。我们将在本章的其余部分看到更多的 tactics ，在以后的章节中看到更多的 tactics。 其他类似的定理可以用相同的模式来证明。

Theorem plus__1_l'

Theorem plus_1_l : forall n:nat, 1 + n = S n.
Proof.
  intros n. reflexivity.  Qed.

Proof.

1 subgoal
______________________________________(1/1)
forall n : nat, 1 + n = S n

intros n.

1 subgoal
n : nat
______________________________________(1/1)
1 + n = S n

Theorem mult_0_l

Theorem mult_0_l : forall n:nat, 0 * n = 0.
Proof.
  intros n. reflexivity.  Qed.

Proof.

1 subgoal
______________________________________(1/1)
forall n : nat, 0 * n = 0

intros n.

1 subgoal
n : nat
______________________________________(1/1)
0 * n = 0

这些定理名称中的 _l 后缀发音为"左侧"。

值得通过这些证据来观察上下文和目标的变化。您可能需要在 reflexivity 前调用 Simpl ，以便在检查它们是否相等之前查看 Coq 在条款上执行的简化。

重写证明 Proof by Rewriting

以下定理比我们所看到的要有趣一些：

Theorem plus_id_example

Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.

它不是对所有数字n和m提出普遍声明，而是谈论一个更专业化的属性，只有在 n = m 时才能持有。箭头符号发音为"暗示"。

和以前一样，我们需要能够推理，假设我们得到这样的数字n和m。我们还需要假设这个假设。Intros 策略将有助于将这三者从目标转移到当前上下文中的假设中。

由于n和m是任意数字， 我们不能只是使用简化来证明这个定理。相反，我们通过观察来证明这一点，如果我们假设 n = m ，那么我们可以在目标陈述中用 m 替换 n ，并以双方相同的表达方式获得平等。告诉 Coq 执行这个替换的策略被称为 rewrite 。

Proof.
  (* move both quantifiers into the context: *)
  intros n m.
  (* move the hypothesis into the context: *)
  intros H.
  (* rewrite the goal using the hypothesis: *)
  rewrite → H.
  reflexivity. Qed.

证明的第一行将通用量化的变量n和m移入上下文。 第二个将假设 n = m 移入上下文，并给它起名称H。 第三个告诉 Coq 重写当前目标（ n + n = m + m），将平等假设H的左侧替换为右侧。

（重写中的箭头符号与含义无关：它告诉 Coq 从左到右应用重写。事实上，您可以省略箭头，Coq 将默认在此方向重写。要从右到左重写，您可以使用 rewrite <-。尝试在上面的证明中做出此更改，看看它有什么不同。

Proof

1 subgoal
______________________________________(1/1)
forall n m : nat, n = m -> n + n = m + m

intros n m.

1 subgoal
n, m : nat
______________________________________(1/1)
n = m -> n + n = m + m

intros H.

1 subgoal
n, m : nat
H : n = m
______________________________________(1/1)
n + n = m + m

rewrite -> H.

1 subgoal
n, m : nat
H : n = m
______________________________________(1/1)
m + m = m + m

rewrite <- H.

1 subgoal
n, m : nat
H : n = m
______________________________________(1/1)
n + n = n + n

练习 Exercise

5: 1 star, standard (plus_id_exercise)

删除"已接受"。

（* SOOMER： KK： plus_id_exercise包含多个假设， 至少有一个学生对此感到困惑。也许我们可以谈论 →在它之前是正确的关联。*）

Theorem plus_id_exercise : forall n m o : nat,
n = m -> m = o -> n + m = m + o.
Proof.
(* FILL IN HERE *) Admitted.

Coq代码

Proof.
  intros n m o.
  intros G.
  intros H.
  rewrite -> G.
  rewrite <- H.
reflexivity.
Qed.

Coq运行截图

Proof.

1 subgoal
______________________________________(1/1)
forall n m o : nat, n = m -> m = o -> n + m = m + o

intros n m o.

1 subgoal
n, m, o : nat
______________________________________(1/1)
n = m -> m = o -> n + m = m + o

intros G.

1 subgoal
n, m, o : nat
G : n = m
______________________________________(1/1)
m = o -> n + m = m + o

intros H.

1 subgoal
n, m, o : nat
G : n = m
H : m = o
______________________________________(1/1)
n + m = m + o

rewrite -> G.

1 subgoal
n, m, o : nat
G : n = m
H : m = o
______________________________________(1/1)
m + m = m + o

rewrite <- H.

1 subgoal
n, m, o : nat
G : n = m
H : m = o
______________________________________(1/1)
m + m = m + m

6: 1 star, standard (mult_n_1)

承认 Admitted

Admitted 的命令告诉科克，我们想跳过试图证明这个定理，只是接受它作为一个给定的。这可能有助于开发更长的证据，因为我们可以陈述我们认为有助于提出一些更大的论点的辅助性 lemmas，暂时使用" Admitted "这些证据，并继续研究主要论点，直到我们确定它有意义：然后我们可以回去填写我们跳过的证据。不过要小心： 每次你说 Admitted 你离开一扇门， 完全无稽之谈进入 Coq 的漂亮， 严格， 正式检查的世界！

Check 命令还可用于检查先前声明的 lemmas 和定理的陈述。下面两个例子是关于乘法的 lemmas ，在标准库中已得到证明。（我们将在下一章中看到如何证明他们自己。

Check mult_n_0

Check mult_n_O.
(* ===> forall n : nat, 0 = n * 0 *)

Check mult_n_Sm

Check mult_n_Sm.
(* ===> forall n m : nat, n * m + n = n * S m *)

我们可以使用 rewrite 策略与先前证明的定理，而不是从上下文的假设。如果先前证明的定理的陈述涉及量化变量，如下示例中所示，Coq 试图通过与当前目标匹配来对它们进行实证。

Theorem mult_n_0_m_0

Theorem mult_n_0_m_0 : forall p q : nat,
  (p * 0) + (q * 0) = 0.
Proof.
  intros p q.
  rewrite <- mult_n_O.
  rewrite <- mult_n_O.
  reflexivity. Qed.

Proof.

1 subgoal
______________________________________(1/1)
forall p q : nat, p * 0 + q * 0 = 0

intros p q.

1 subgoal
p, q : nat
______________________________________(1/1)
p * 0 + q * 0 = 0

rewrite <- mult_n_O.

1 subgoal
p, q : nat
______________________________________(1/1)
0 + q * 0 = 0

rewrite <- mult_n_O.

1 subgoal
p, q : nat
______________________________________(1/1)
0 + 0 = 0

Coq题目

使用我们刚刚检查的关于乘法的这两个 Lemma 来证明以下定理。提示：回想一下，1 是 S O 。

Theorem mult_n_1 : forall p : nat,
  p * 1 = p.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Proof.
 intros p.
 rewrite <- mult_n_Sm.
 rewrite <- mult_n_O.
simpl.
reflexivity. 
Qed.

Coq运行截图

Proof.

1 subgoal
______________________________________(1/1)
forall p : nat, p * 1 = p

intros p.

1 subgoal
p : nat
______________________________________(1/1)
p * 1 = p

rewrite <- mult_n_Sm.

1 subgoal
p : nat
______________________________________(1/1)
p * 0 + p = p

rewrite <- mult_n_O.

1 subgoal
p : nat
______________________________________(1/1)
0 + p = p

simpl.

1 subgoal
p : nat
______________________________________(1/1)
p = p