Software Foundations Vol.I : 归纳证明(Induction)
归纳法证明
我们在上一章中通过基于化简的简单论据证明了 0 是 + 的左幺元。 我们也观察到，当我们打算证明 0 也是 + 的 '右' 幺元时事情就没这么简单了
Theorem plus_n_O_firsttry : ∀ n:nat,n = n + 0.
Proof.intros n.simpl. (* Does nothing! *)
Abort.
只应用 reflexivity 的话不起作用，因为 n + 0 中的 n 是任意未知数，所以在 + 的定义中 match 匹配无法被化简。
即便用 destruct n 分类讨论也不会有所改善：诚然，我们能够轻易地证明 n = 0 时的情况；但在证明对于某些 n' 而言 n = S n' 时，我们又会遇到和此前相同的问题。
Theorem plus_n_O_secondtry : ∀ n:nat,n = n + 0.
Proof.intros n. destruct n as [| n'] eqn:E.- (* n = 0 *)reflexivity. (* 虽然目前还没啥问题... *)- (* n = S n' *)simpl. (* ...不过我们又卡在这儿了 *)
Abort.
虽然还可以用 destruct n' 再推进一步，但由于 n 可以任意大， 如果照这个思路继续证明的话，我们永远也证不完。
为了证明这种关于数字、列表等归纳定义的集合的有趣事实， 我们通常需要一个更强大的推理原理：'归纳'。
自然数的归纳法则:
- 证明 P(O) 成立；
- 证明对于任何 n'，若 P(n') 成立，那么 P(S n') 也成立。
- 最后得出 P(n) 对于所有 n 都成立的结论。
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.
induction: 通过数学归纳法对命题进行证明的策略.
Coq中也同样,以证明 P(n) 对于所有 n 都成立的目标开始， 然后（通过应用 induction 策略）把它分为两个子目标：一个是我们必须证明 P(O) 成立，另一个是我们必须证明 P(n') → P(S n')。
和 destruct 一样，induction 策略也能通过 as... 从句为引入到 子目标中的变量指定名字。由于这次有两个子目标，因此 as... 有两部分，用 | 隔开。
Theorem minus_diag : ∀ n,minus n n = 0.
Proof.(* 课上已完成 *)intros n. induction n as [| n' IHn'].- (* n = 0 *)simpl. reflexivity.- (* n = S n' *)simpl. rewrite → IHn'. reflexivity.
Qed.
（其实在这些证明中我们并不需要 intros：当 induction 策略被应用到包含量化变量的目标中时，它会自动将需要的变量移到上下文中。）
证明中的证明
和在非形式化的数学中一样，在 Coq 中，大的证明通常会被分为一系列定理， 后面的定理引用之前的定理。但有时一个证明会需要一些繁杂琐碎的事实， 而这些事实缺乏普遍性，以至于我们甚至都不应该给它们单独取顶级的名字。
如果能仅在需要时简单地陈述并立即证明所需的“子定理”就会很方便。 我们可以用 assert 策略来做到。
Theorem mult_0_plus' : ∀ n m : nat,(0 + n) × m = n × m.
Proof.intros n m.assert (H: 0 + n = n). { reflexivity. }rewrite → H.reflexivity.
Qed.
assert 策略引入两个子目标。第一个为断言本身，通过给它加前缀 H: 我们将该断言命名为 H。（当然也可以用 as 来命名该断言，例如 assert (0 + n = n) as H。
第二个目标 与之前执行 assert 时一样，只是这次在上下文中，我们有了名为 H 的前提 0 + n = n。
举例来说，假如我们要证明 (n + m) + (p + q) = (m + n) + (p + q)。
Theorem plus_rearrange_firsttry : ∀ n m p q : nat,(n + m) + (p + q) = (m + n) + (p + q).
Proof.intros n m p q.(* 我们只需要将 (m + n) 交换为 (n + m)... 看起来 plus_comm 能搞定！*)rewrite → plus_comm.(* 搞不定... Coq 选错了要改写的加法！ *)
Abort.
为了在需要的地方使用 plus_comm，我们可以（为此这里讨论的 m 和 n） 引入一个局部引理来陈述 n + m = m + n，之后用 plus_comm 证明它， 并用它来进行期望的改写。
Theorem plus_rearrange : ∀ n m p q : nat,(n + m) + (p + q) = (m + n) + (p + q).
Proof.intros n m p q.assert (H: n + m = m + n). { rewrite → plus_comm. reflexivity. }rewrite → H. reflexivity.
Qed.
我们不难发现,相比起上面的例子,这里的例子将引理中的符号指定为特定的m与n,解决了问题.
形式化证明 vs 非形式化证明
“'非形式化证明是算法，形式化证明是代码。'”
由于我们在本课程中使用 Coq，因此会重度使用形式化证明。但这并不意味着我们 可以完全忽略掉非形式化的证明过程！形式化证明在很多方面都非常有用， 不过它们对人类之间的思想交流而言 '并不' 十分高效。
例如，下面是一段加法结合律的证明：
Theorem plus_assoc' : forall n m p : nat,n + (m + p) = (n + m) + p.
Proof. intros n m p. induction n as [| n' IHn']. - reflexivity.- simpl. rewrite → IHn'. reflexivity.
Qed.
Coq 对此表示十分满意。然而人类却很难理解它。
一个（迂腐的）数学家可能把证明写成这样：
'定理'： 对于任何 n、m 和 p，
$$n + (m + p) = (n + m) + p.$$
'证明'： 对 n 使用归纳法。
首先，设 n = 0。我们必须证明
$$ 0 + (m + p) = (0 + m) + p.$$
此结论可从 + 的定义直接得到。
然后，设 n = S n'，其中
$$ n' + (m + p) = (n' + m) + p.$$
我们必须证明
$$ (S n') + (m + p) = ((S n') + m) + p.$$
根据 + 的定义，该式可写成
$$ S (n' + (m + p)) = S ((n' + m) + p),$$
它由归纳假设直接得出。'证毕'。
)
