归纳证明是 Coq 中最核心的推理手段。无论是对自然数的算术性质、对列表的结构性质，还是对树的递归性质，归纳原理都以同一套框架给出严格证明。本文系统覆盖三类归纳：标准结构归纳、完全归纳（强归纳），以及依赖 Acc 和 Fix 的 well-founded 递归。

前置阅读：本系列 01（环境与项目结构）、02（目标窗口与 tactic 交互）、03（Gallina 核心语法）、04（基础 tactic 全景）提供了必要的语法和 tactic 背景。本文中出现的 induction、simpl、rewrite、auto 等 tactic 在 04 中均有详细说明。

自然数上的结构归纳

归纳原理的来源

nat 在 Coq 标准库中定义为：

1
2
3
Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

Inductive 指令自动生成归纳原理 nat_ind，其类型为：

1
2
3
4
nat_ind : forall P : nat -> Prop,
  P 0 ->
  (forall n : nat, P n -> P (S n)) ->
  forall n : nat, P n

induction tactic 正是对这条原理的调用。证明目标 forall n, P n 时，induction n 将目标拆成两个子目标：P 0 和 P n -> P (S n)。

加法结合律的证明

1
2
3
4
5
6
7
8
9
10
11
12
Require Import Arith.

Lemma add_assoc : forall a b c : nat,
  a + (b + c) = (a + b) + c.
Proof.
  intros a b c.
  induction a as [| a' IHa'].
  - (* 基础情形：a = 0 *)
    simpl. reflexivity.
  - (* 归纳情形：a = S a' *)
    simpl. rewrite IHa'. reflexivity.
Qed.

as [| a' IHa'] 是引入模式（intro pattern）。[| 左侧为 O 分支，右侧为 S 分支，a' 绑定前驱，IHa' 绑定归纳假设。这个写法在 04 中已经介绍，此处可以对比实际证明情形。

用 Show Proof. 可以看到归纳情形产生的项：

1
2
3
4
5
6
7
8
9
10
Show Proof.
(*
fun (a b c : nat) =>
nat_ind (fun a0 : nat => a0 + (b + c) = (a0 + b) + c)
  (eq_refl (b + c))
  (fun (a' : nat) (IHa' : a' + (b + c) = (a' + b) + c) =>
     eq_ind_r (fun n : nat => S n = S (a' + b + c))
       eq_refl IHa')
  a
*)

这表明 induction 生成的证明项是对 nat_ind 的直接应用，IHa' 对应函数参数里的归纳假设。

引入模式的变体

不同的引入模式适用于不同场合：

1
2
3
4
5
6
7
8
(* 匿名前驱，不保留名字 *)
induction n as [| n' _].

(* 多层嵌套，列表 *)
induction l as [| x xs IHxs].

(* 带等式 destruct eqn: *)
induction n as [| n'] eqn:Hn.

eqn:Hn 会在上下文中保留 Hn : n = 0 或 Hn : n = S n'，当后续 rewrite 需要引用具体形式时很有用。

列表上的结构归纳

列表翻转的长度不变性

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
Require Import List.
Import ListNotations.

Lemma rev_length : forall (A : Type) (l : list A),
  length (rev l) = length l.
Proof.
  intros A l.
  induction l as [| x xs IHxs].
  - simpl. reflexivity.
  - simpl.
    rewrite app_length.
    simpl.
    rewrite IHxs.
    omega.
Qed.

app_length 是标准库引理 length (l1 ++ l2) = length l1 + length l2。omega 处理线性算术等式。

翻转两次等于原列表

1
2
3
4
5
6
7
8
9
10
11
12
Lemma rev_involutive : forall (A : Type) (l : list A),
  rev (rev l) = l.
Proof.
  intros A l.
  induction l as [| x xs IHxs].
  - simpl. reflexivity.
  - simpl.
    rewrite rev_app_distr.
    simpl.
    rewrite IHxs.
    reflexivity.
Qed.

rev_app_distr 的类型为 rev (l1 ++ l2) = rev l2 ++ rev l1。这个引理在 05 中的 Search 演示里出现过，读者可以用 Search rev app 自行查找。

二叉树上的结构归纳

树的定义

1
2
3
4
5
6
Inductive tree (A : Type) : Type :=
  | Leaf : tree A
  | Node : tree A -> A -> tree A -> tree A.

Arguments Leaf {A}.
Arguments Node {A} _ _ _.

Coq 自动生成 tree_ind：

1
2
3
4
5
6
7
8
tree_ind :
  forall (A : Type) (P : tree A -> Prop),
  P Leaf ->
  (forall l : tree A, P l ->
   forall a : A,
   forall r : tree A, P r ->
   P (Node l a r)) ->
  forall t : tree A, P t

树的镜像与大小

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
Fixpoint mirror {A} (t : tree A) : tree A :=
  match t with
  | Leaf => Leaf
  | Node l a r => Node (mirror r) a (mirror l)
  end.

Fixpoint size {A} (t : tree A) : nat :=
  match t with
  | Leaf => 0
  | Node l _ r => 1 + size l + size r
  end.

Lemma mirror_size : forall (A : Type) (t : tree A),
  size (mirror t) = size t.
Proof.
  intros A t.
  induction t as [| l IHl a r IHr].
  - simpl. reflexivity.
  - simpl. rewrite IHl. rewrite IHr. omega.
Qed.

as [| l IHl a r IHr] 把 Node 分支的两棵子树和两个归纳假设全部命名，避免 Coq 自动生成晦涩的名字。

1
2
3
4
5
6
7
8
Lemma mirror_involutive : forall (A : Type) (t : tree A),
  mirror (mirror t) = t.
Proof.
  intros A t.
  induction t as [| l IHl a r IHr].
  - simpl. reflexivity.
  - simpl. rewrite IHl. rewrite IHr. reflexivity.
Qed.

标准归纳卡住的情形与强归纳

卡住示例：Collatz 步骤上界

考虑一个简化问题：证明所有满足 n <= m 的自然数在某个谓词下成立，而谓词的递推关系依赖于 n/2 而非 n-1。标准 induction n 只能给出 P n -> P (S n) 形式的归纳假设，无法直接使用 P (n/2)。

一个更直接的展示场景：证明 Fibonacci 数满足某种下界。以标准归纳尝试下面的命题：

1
2
3
4
5
6
7
(* fib 定义 *)
Fixpoint fib (n : nat) : nat :=
  match n with
  | 0 => 0
  | 1 => 1
  | S (S n' as n'') => fib n'' + fib n'
  end.

证明 fib (n + 2) >= fib n + 1 时，induction n 在 S n' 情形给出的归纳假设是 fib (n' + 2) >= fib n' + 1，但目标需要用 fib (n' + 1 + 2) 和 fib (n' + 2 + 2) 的关系，跨度超出一步，归纳假设不够用。

实际上，Fibonacci 的典型归纳需要两步归纳假设（对 n 和 n+1 同时成立），这正是**完全归纳（strong induction）**的用武之地。

完全归纳的原理

Coq 标准库提供 lt_wf_ind（在 Coq.Arith.Wf_nat）：

1
2
3
4
lt_wf_ind :
  forall (n : nat) (P : nat -> Prop),
  (forall n, (forall m, m < n -> P m) -> P n) ->
  P n

这条原理说：若对任意 n，在所有小于 n 的数均满足 P 的前提下能证 P n，则 P 对所有自然数成立。

也可以自行定义等价的 strong_induction 引理并直接使用：

1
2
3
4
5
6
7
8
9
10
Require Import Coq.Arith.Wf_nat.

Lemma strong_induction :
  forall (P : nat -> Prop),
  (forall n, (forall m, m < n -> P m) -> P n) ->
  forall n, P n.
Proof.
  intros P Hstep n.
  apply lt_wf_ind. exact Hstep.
Qed.

用强归纳证明 Fibonacci 单调性

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
(* fib 严格递增（n >= 1 时）：fib n < fib (S n) *)
Lemma fib_lt : forall n, 1 <= n -> fib n < fib (S n).
Proof.
  intro n.
  apply strong_induction with (n := n).
  intros m IH Hm.
  destruct m as [| [| m']].
  - (* m = 0 *) omega.
  - (* m = 1 *) simpl. omega.
  - (* m = S (S m') *)
    simpl.
    assert (H1 : fib (S m') < fib (S (S m'))) by
      (apply IH; omega).
    assert (H2 : fib m' < fib (S m')) by
      (apply IH; omega).
    omega.
Qed.

归纳假设 IH : forall k, k < m -> 1 <= k -> fib k < fib (S k) 覆盖所有小于 m 的情形，因此对 m' 和 S m' 均可使用，而标准 induction 无法做到这一点。

Print Assumptions fib_lt. 输出：

1
2
Axioms:
  Coq.Arith.Wf_nat.lt_wf : well_founded lt

这表明整个证明只依赖 lt_wf（< 上的 well-founded 性），没有引入额外公理。

Well-Founded 递归与 Fix

Acc 与 well_founded 的定义

Coq 的 Acc（Accessibility）谓词定义在 Coq.Init.Wf：

1
2
Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop :=
  Acc_intro : (forall y, R y x -> Acc R y) -> Acc R x.

Acc R x 断言：x 关于关系 R 是可及的，即从 x 出发沿 R 无法无限下降。

1
2
Definition well_founded {A} (R : A -> A -> Prop) :=
  forall a, Acc R a.

well_founded R 意味着 R 上不存在无穷下降链，这保证了沿 R 的递归一定终止。

Fix 的类型

1
2
3
4
5
Fix : forall (A : Type) (R : A -> A -> Prop),
  well_founded R ->
  forall (P : A -> Type),
  (forall x, (forall y, R y x -> P y) -> P x) ->
  forall x, P x

Fix 是 well-founded 递归的通用组合子。第一个参数是终止证据，第二个是递归步骤（形如 forall x, (forall y < x, P y) -> P x）。

用 Fix 定义欧几里得算法

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
Require Import Coq.Arith.Wf_nat.

(* 辅助：lt_wf : well_founded lt *)

Definition gcd_step
  (n : nat)
  (rec : forall m : nat, m < n -> nat -> nat)
  (k : nat) : nat :=
  match n with
  | 0 => k
  | S _ =>
    match Nat.eq_dec k 0 with
    | left _  => n
    | right _ =>
        let r := n mod k in
        rec r (Nat.mod_upper_bound n k (fun H => match H with end)) k
    end
  end.

上面片段展示结构：rec 参数携带一个 m < n 的证明，保证递归调用仅用于更小的参数。实际可编译版本需要补充一些细节（如 k <> 0 的条件），此处意在说明 Fix 的使用模式。

在实践中，更常见的做法是使用 Program Fixpoint 或 Function，让 Coq 自动处理终止证明：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Require Import Program.

Program Fixpoint gcd (n k : nat) {measure n} : nat :=
  match n with
  | 0 => k
  | _ =>
    match k with
    | 0 => n
    | _ => gcd (n mod k) n
    end
  end.
Next Obligation.
  apply Nat.mod_upper_bound. omega.
Defined.

{measure n} 告诉 Coq 用 n 作为递减量，Next Obligation 填充终止证明。

measure 与 wf 的关系

{measure f} 在展开后等价于 well_founded (fun x y => f x < f y)。标准库里对应 lt_wf 和 measure_wf：

1
2
measure_wf : forall (A : Type) (f : A -> nat),
  well_founded (fun x y => f x < f y)

这意味着一切基于自然数度量的递归，其终止性最终归结于 lt_wf，而 lt_wf 本身在 Coq 的逻辑基础内可以证明（通过对 nat 的结构归纳）。

几个容易混淆的细节

induction 与 destruct 的区别

destruct n 对 n 做情形分析，产生 n = O 和 n = S n' 两个子目标，但不产生归纳假设。induction n 在 S n' 分支额外给出 IHn' : P n'。

若目标不依赖 n 的值而只依赖 n 的形状（如 n = 0 \/ n > 0），用 destruct 够了；只有命题需要对所有 n 递推时才用 induction。

归纳前的 generalize

一个常见错误：先用 intros 把某个变量引入上下文，再对另一个变量做归纳，导致归纳假设过弱。

1
2
3
4
5
(* 错误写法 *)
Lemma add_comm : forall a b : nat, a + b = b + a.
Proof.
  intros a b.
  induction a.   (* IH 里 b 已经固定，形式为 b + 0 = 0 + b，不够用 *)

正确做法是在 induction 之前不引入 b，让 b 保留在目标中：

1
2
3
4
5
6
7
Lemma add_comm : forall a b : nat, a + b = b + a.
Proof.
  intro a.
  induction a as [| a' IHa'].
  - intro b. simpl. rewrite Nat.add_0_r. reflexivity.
  - intro b. simpl. rewrite IHa'. rewrite Nat.add_succ_r. reflexivity.
Qed.

此时归纳假设的形式为 forall b, a' + b = b + a'，对所有 b 成立，足以推进 S a' 情形。

对嵌套归纳类型的 induction

当归纳类型含有嵌套（如树中每个节点存储一个列表），Coq 可能无法自动生成足够强的归纳原理。此时可以使用 Scheme 手动生成，或改用 size_ind（按大小归纳）：

1
2
3
4
Lemma size_ind (P : nat -> Prop) :
  (forall n, (forall m, m < n -> P m) -> P n) ->
  forall n, P n.
Proof. exact strong_induction. Qed.

然后对任意带大小函数的类型 T，通过 apply size_ind with (n := size_of t) 转化为自然数上的强归纳。

参考资料

  • Coq 官方文档，Inductive Types 章节：https://coq.inria.fr/doc/v8.19/refman/language/core/inductive.html
  • Software Foundations Vol. 1（Logical Foundations），Induction 章节
  • Certified Programming with Dependent Types（CPDT），Adam Chlipala，General Recursion 章节
  • Coq 标准库 Coq.Arith.Wf_nat：lt_wf_ind、measure_wf 的定义与证明
  • 本系列 04（基础 tactic 全景）：induction、destruct、rewrite 的详细语义

练习 1：列表追加与长度

证明 forall (A : Type) (l1 l2 : list A), length (l1 ++ l2) = length l1 + length l2，不使用标准库中的 app_length，仅用 induction、simpl、reflexivity、omega。

练习 2：树的高度与大小

定义树的高度函数：

1
2
3
4
5
Fixpoint height {A} (t : tree A) : nat :=
  match t with
  | Leaf => 0
  | Node l _ r => 1 + max (height l) (height r)
  end.

证明 forall (A : Type) (t : tree A), size t <= 2 ^ height t - 1（可以先证 size t < 2 ^ (height t + 1)，此形式更适合归纳推进）。

练习 3：用强归纳证明 Euclid 算法终止

不使用 Program Fixpoint，直接用 Fix lt_wf 定义一个对参数 a 递减的 gcd 变体，使得递归调用的第一参数严格小于当前第一参数（提示：Nat.mod_upper_bound 给出 a mod b < a 当 a > 0）。