（本文是对 James Wilcox 的 Exercises on Generalizing the Induction Hypothesis 的一点详细解说，也感谢 James Wilcox 在文章中提供的几道颇有练习价值的证明题！）
由于大多数数据类型常见的递归属性，在 Coq 中使用归纳法证明命题是一件颇为常见且基础的操作。
然而，有些具有递归性质的命题并不易于使用归纳法直接进行证明，原因在于，这些命题中的部分变量取了特定的值，而归纳过程中这些变量的值会发生变化，从而导致归纳过程无法继续下去。对此，我们往往需要找到一个更一般性的命题，用归纳法证明这一一般命题，随后使用该一般命题构建对原命题的证明。
下面便是两道实践此类命题证明方法论的绝佳例题。
例子：尾递归求和
尾递归是一种特殊的递归形式——函数总在尾部位置递归调用自身。利用尾递归“尾部调用”的特性，我们可以将尾递归的空间复杂度优化到 \(O(1)\)。
下面给出函数式编程下，序列求和的普通版本和尾递归版本。
Fixpoint sum (l : list nat) : nat := match l with | [] => 0 | x :: xs => x + sum xs end. Fixpoint sum_tail' (l : list nat) (acc : nat) : nat := match l with | [] => acc | x :: xs => sum_tail' xs (x + acc) end. Definition sum_tail (l : list nat) : nat := sum_tail' l 0.
然而，要在 Coq 中证明尾递归形式与普通形式的等价性则并不算容易。
一个直观想法是对列表 l 进行归纳，挣扎一阵后便发现这并不可行。
Theorem sum_tail_correct_failed :
forall l,
sum_tail l = sum l.
Proof.
intros l. induction l.
- reflexivity.
- unfold sum_tail. simpl.
(* we need to prove now: sum_tail' l a = a + sum l *)
(* can't go any more step! *)
Admitted.
看起来我们好像在归纳证明的过程中又遇到了一个需要归纳证明的命题，不如考虑把这个命题拿出来单独证明！事实上，这个引理的证明相比原命题来说要容易不少：
Lemma sum_tail'_sep : forall (x : nat) (l : list nat), sum_tail' l x = x + sum l. Proof. intros x l. generalize dependent x. induction l. - auto. - simpl. intros x. rewrite IHl. lia. Qed.
接下来，看起来我们只需要在前面卡壳的位置加上 apply sum_tail'_sep 就完工了。不过等等，我们意外地（？）发现，这个引理好像不仅仅能应用于上面递归的第二种情况，而是可以直接用来构建原命题的全部证明。毕竟 sum_tail l = sum_tail' l 0 嘛：
Theorem sum_tail_correct :
forall l,
sum_tail l = sum l.
Proof.
intros l. unfold sum_tail. apply sum_tail'_sep.
Qed.
例子：尾递归序列反转
接下来再看一个针对列表的尾递归例子：
Fixpoint rev {A} (l : list A) : list A :=
match l with
| [] => []
| x :: xs => rev xs ++ [x]
end.
Fixpoint rev_tail' {A} (l : list A) (acc : list A) : list A :=
match l with
| [] => acc
| x :: l' => rev_tail' l' (x :: acc)
end.
Definition rev_tail {A} (l : list A) : list A := rev_tail' l [].
下面来证明两种反转算法的等价性。当然，直接证明还是会卡壳：
Theorem rev_tail_correct_failed :
forall A (l : list A),
rev_tail l = rev l.
Proof.
intros A l.
induction l.
- reflexivity.
- unfold rev_tail. simpl.
(* stuck at similer status! *)
Admitted.
仍然考虑把中间卡住的部分拿出来单独证明。当然，单独证明的部分已经足够构建整个命题了。
Lemma rev_tail'_sep :
forall A (l1 : list A) (l2 : list A),
rev_tail' l1 l2 = rev l1 ++ l2.
Proof.
intros A l1 l2.
generalize dependent l2.
induction l1.
- reflexivity.
- intros l2. simpl. rewrite IHl1.
(* next to prove: rev l1 ++ a :: l2 = (rev l1 ++ [a]) ++ l2 *)
rewrite <- app_assoc. rewrite app_inv_head_iff. reflexivity.
Qed.
Theorem rev_tail_correct :
forall A (l : list A),
rev_tail l = rev l.
Proof.
intros A l. unfold rev_tail. rewrite rev_tail'_sep. apply app_nil_r.
Qed.
总结
回顾一下我们构建的两个引理，他们都是原定理的更一般的形式。
- 在尾递归求和中，我们要证明的命题是
sum_tail l = sum l，实质上相当于sum_tail' l 0 = 0 + sum l，而我们构建的引理则是sum_tail' l x = x + sum l； - 在尾递归序列反转中，我们要证明的命题是
rev_tail l = rev l，实质上相当于rev_tail' l [] = rev l ++ []，而我们构建的引理则是rev_tail' l1 l2 = rev l1 ++ l2。
原命题难以证明的原因，在于其递归过程中保存状态的函数参数是可变的，这使得我们无法利用归纳假设推进定理证明。以尾递归求和为例，直接证明时，我们需要证明 sum_tail' l a = a + sum l，这与归纳假设 sum_tail' l 0 = 0 + sum l 的形式并不匹配。
将保存状态的参数设定为变量并一般化，则有效解决了这一问题。由于归纳假设中状态变量带上了全称量词，因此即使递归过程展开后状态变量的值发生了变化，我们仍可以利用归纳假设推进证明。在证明了更一般的“引理”后，作为特例的原命题的证明也就易如反掌了。
事实上，将非关键变量一般化，是不少 Coq 初学者在学习到归纳证明时学到的第一条经验教训。
（下面的示例来自于 Software Foundations I – Tactics: More Basic Tactics 一节）
Theorem double_injective_FAILED : forall n m,
double n = double m ->
n = m.
Proof.
intros n m. induction n as [| n' IHn'].
- (* n = O *) simpl. intros eq. destruct m as [| m'] eqn:E.
+ (* m = O *) reflexivity.
+ (* m = S m' *) discriminate eq.
- (* n = S n' *) intros eq. destruct m as [| m'] eqn:E.
+ (* m = O *) discriminate eq.
+ (* m = S m' *) apply f_equal.
Abort.
在上面的命题中，若将 n 视为自由变量，则 m 的值事实上是随 n 的取值变化而变化的。但在归纳过程中，m 的值并没有被一般化，而是被固定下来，不随 n 的变化而变化，导致出现了归纳假设中前提为假的情况，无法推进命题的证明。
将 m 的取值一般化，我们才能得到一个更一般，更准确的归纳假设，并利用其完成证明过程。
Theorem double_injective_take2 : forall n m,
double n = double m ->
n = m.
Proof.
intros n m.
(* n and m are both in the context *)
generalize dependent m.
(* Now m is back in the goal and we can do induction on
n and get a sufficiently general IH. *)
induction n as [| n' IHn'].
- (* n = O *) simpl. intros m eq. destruct m as [| m'] eqn:E.
+ (* m = O *) reflexivity.
+ (* m = S m' *) discriminate eq.
- (* n = S n' *) intros m eq. destruct m as [| m'] eqn:E.
+ (* m = O *) discriminate eq.
+ (* m = S m' *) apply f_equal.
apply IHn'. injection eq as goal. apply goal. Qed.
James Wilcox 的文章中还有好几道归纳证明练习题，做完全部题目，将会对构建更一般性的定理的证明的方法论有更为深入的认识。