为什么可以使用归纳法中的 IHn' (n' = n' + 0) 来证明 Coq 中的 n = n + 0？

Question

在软件基础的逻辑基础中，他们使用归纳的思想来证明事物。通过逐步完成以下证明，很难看出为什么您可以重写您试图用原始假设证明的内容。为什么IHn' (n' = n' + 0) 可以用归纳法证明n = n + 0?

它们本质上不是同一个说法吗？

Theorem plus_n_O : ∀ n:nat, n = n + 0.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *) reflexivity.
  - (* n = S n' *) simpl. rewrite <- IHn'. reflexivity. Qed.

Answer 1

它们是同一个语句，只是关于不同的数字：一个是关于n'，一个是关于n，对应目标中的S n'。归纳法恰恰是通过知道它适用于 n' 来证明某些东西对 S n' 有效。它们是不同的数字这一事实使得这很重要。例如，假设 n' 是奇数，not 可能证明 S n' 是奇数，即使两个陈述都是 "the same".

您询问了重写的机制。简化后，您的目标如下所示：

n' : nat
IHn' : n' = n' + O
---------------------------------------
S n' = S (n' + O)

当您调用 rewrite 时，您是在告诉 Coq 在目标中用 n' 替换 n' + O。这导致陈述 S n' = S n'，这是一个简单的等式，可以通过自反性公理来证明。

编辑

这是思考归纳法的另一种方式。让我们暂时忘记 induction 策略。可以证明 0 = 0 + 0:

Lemma plus_0_0 : 0 = 0 + 0.
Proof. reflexivity. Qed.

我们可以证明关于任何具体自然数的类似陈述：

Lemma plus_1_0 : 1 = 1 + 0.
Proof. reflexivity. Qed.

Lemma plus_2_0 : 2 = 2 + 0.
Proof. reflexivity. Qed.

但是，我们可以通过不同方式获得这些证明，对我们所讨论的数字的形状做出更少的假设。首先，我们证明下面的条件语句。

Lemma plus_Sn_0 : forall n', n' = n' + 0 -> S n' = S n' + 0.
Proof. intros n' Hn'. simpl. rewrite <- Hn'. reflexivity. Qed.

这个引理说明了归纳证明的归纳步骤。请注意，它并不是说 n = n + 0 对所有自然数 n 都成立，而是只对 n = S n' 形式的数字成立，前提是 n' = n' + 0。我们知道这适用于 n' = 0，因为我们在上面证明了这一点。结合plus_Sn_0，我们又得到了1 = 1 + 0.

的证明

Lemma plus_1_0' : 1 = 1 + 0.
Proof. apply plus_Sn_0. apply plus_0_0. Qed.

现在，我们知道该语句适用于 n' = 1，我们可以对 n = 2 玩同样的把戏：

Lemma plus_2_0' : 2 = 2 + 0.
Proof. apply plus_Sn_0. apply plus_1_0'. Qed.

这个证明没有直接使用0 = 0 + 0这个事实。这就是为什么我们证明基本情况的事实与证明归纳步骤无关：我们需要知道的只是我们感兴趣的数字的前身——在这种情况下, 这个前身是 1.

自然地，我们可以在 plus_2_0' 的证明中展开 plus_1_0' 的证明：

Lemma plus_2_0'' : 2 = 2 + 0.
Proof. apply plus_Sn_0. apply plus_Sn_0. apply plus_0_0. Qed.

更一般地，给定任何自然数常数 n，我们可以通过应用 plus_Sn_0 [=18] 证明 n = n + 0 无需归纳法 =] 次后跟 plus_0_0。数学归纳法原理将这种直观观察外推为 any 表达式 n 表示自然数，而不仅仅是常数。

为什么可以使用归纳法中的 IHn' (n' = n' + 0) 来证明 Coq 中的 n = n + 0？

Why can IHn' (n' = n' + 0) from induction be used to prove n = n + 0 in Coq?

logic

coq

coq-tactic