归纳证明

induction tactic、归纳假设的使用、泛化技巧、强归纳与良基递归，以及为什么归纳法就是递归。

归纳法就是递归

前面说过 Nat.rec 同时是递归子和归纳原理。所以：

-- 递归定义一个函数
def sumTo : Nat → Nat
  | 0     => 0
  | n + 1 => (n + 1) + sumTo n

-- 归纳证明一个性质：结构完全一样
theorem sumTo_formula (n : Nat) : 2 * sumTo n = n * (n + 1) := by
  induction n with
  | zero => rfl
  | succ k ih =>
    simp [sumTo]
    ring_nf
    omega

induction n with | zero => ... | succ k ih => ... 里的 ih 就是归纳假设——它的类型正是「对 k 成立的那个命题」。

induction 的形式

theorem add_zero' (n : Nat) : n + 0 = n := by
  induction n with
  | zero => rfl
  | succ k ih => simp

-- 也可以用 case 语法
theorem add_zero'' (n : Nat) : n + 0 = n := by
  induction n
  case zero => rfl
  case succ k ih => simp

-- 或用 focus dot（按构造子顺序）
theorem add_zero''' (n : Nat) : n + 0 = n := by
  induction n
  · rfl
  · simp

推荐用 with | 构造子名 => 形式——按名字比按位置稳健，且 ih 可以显式命名。

对 List 归纳

theorem length_append (xs ys : List α) :
    (xs ++ ys).length = xs.length + ys.length := by
  induction xs with
  | nil => simp
  | cons x rest ih =>
    simp [ih]
    omega

归纳的结构由类型的构造子决定：List 有 nil 和 cons，所以两个分支。

注意归纳假设 ih : (rest ++ ys).length = rest.length + ys.length——它是对尾巴成立的陈述。

泛化：最关键的技巧

归纳证明失败最常见的原因是归纳假设太弱。

-- 尾递归版本的求和
def sumAcc : Nat → Nat → Nat
  | 0,     acc => acc
  | n + 1, acc => sumAcc n (acc + n + 1)

-- 直接归纳会卡住
theorem sumAcc_correct (n : Nat) : sumAcc n 0 = sumTo n := by
  -- induction n  ← ih 只对 acc = 0 成立，用不了！
  sorry

问题：归纳时 acc 的值会变，但归纳假设里的 acc 被固定成了 0。

解法：先泛化，让归纳假设覆盖所有 acc：

theorem sumAcc_gen (n acc : Nat) : sumAcc n acc = acc + sumTo n := by
  induction n generalizing acc with
  | zero => simp [sumAcc, sumTo]
  | succ k ih =>
    simp [sumAcc, sumTo, ih]
    omega

theorem sumAcc_correct' (n : Nat) : sumAcc n 0 = sumTo n := by
  simpa using sumAcc_gen n 0

generalizing 是归纳证明的头号技巧。

induction n generalizing acc 意思是：「对 n 归纳，但把 acc 也纳入归纳假设的全称范围」。得到的 ih 是 ∀ acc, sumAcc k acc = acc + sumTo k，而不是只对某个具体 acc 成立。

卡在归纳步时，第一件事就是问「归纳假设够强吗」。 常常需要先证一个更一般的引理。

另一个方向的技巧是加强命题：想证 P n 证不出来，就去证更强的 P n ∧ Q n——看似更难，但归纳假设也更强，反而能成。

强归纳

有时需要「假设对所有小于 n 的都成立」：

theorem strong_example (n : Nat) : True := by
  induction n using Nat.strong_induction_on with
  | _ n ih =>
    -- ih : ∀ m, m < n → True
    trivial

Nat.strong_induction_on 提供完全归纳。Mathlib 里也叫 Nat.strongRecOn。

对二分类算法（如快排、归并）的正确性证明，通常需要强归纳——因为递归调用的参数不是 n-1 而是 n/2。

自定义归纳原理

theorem two_step (n : Nat) : True := by
  induction n using Nat.twoStepInduction with
  | H1 => trivial          -- n = 0
  | H2 => trivial          -- n = 1
  | H3 k ih1 ih2 => trivial  -- n = k+2，有两个归纳假设

using 允许指定任意归纳原理。斐波那契这类「依赖前两项」的定义需要它。

也可以自己定义归纳原理——它就是一个普通定理：

theorem myInduction {P : Nat → Prop} (h0 : P 0) (h1 : P 1)
    (hstep : ∀ n, P n → P (n + 1) → P (n + 2)) : ∀ n, P n := by
  intro n
  induction n using Nat.twoStepInduction with
  | H1 => exact h0
  | H2 => exact h1
  | H3 k ih1 ih2 => exact hstep k ih1 ih2

cases vs induction

example (n : Nat) : n = 0 ∨ ∃ k, n = k + 1 := by
  cases n with
  | zero => left; rfl
  | succ k => right; exact ⟨k, rfl⟩

	`cases`	`induction`
提供归纳假设	否	是
用于	只需分情况	需要对子结构的结论

不需要归纳假设时用 cases——它更轻量，且不会引入用不到的假设。

rcases / obtain 是 cases 的模式化版本，见 tactic 基础。

良基递归的证明

def gcd' (a b : Nat) : Nat :=
  if h : b = 0 then a
  else gcd' b (a % b)
termination_by b
decreasing_by exact Nat.mod_lt _ (Nat.pos_of_ne_zero h)

对这类函数证性质，用它自动生成的归纳原理：

theorem gcd'_comm_ish (a b : Nat) : True := by
  induction a, b using gcd'.induct with
  | _ => trivial
  | _ => trivial

f.induct 是 Lean 为每个良基递归函数自动生成的归纳原理，它的分支结构与函数定义完全对应。证明关于该函数的性质时，用它比手工归纳方便得多。

归纳证明的标准流程

1. 写出 induction 骨架，两个分支都填 sorry
2. 看 Infoview 里 ih 的确切类型
3. 问：ih 够强吗？不够就 generalizing 或加强命题
4. base case 通常 simp / rfl 能解决
5. inductive step 用 simp [ih] 或 rw [ih] 引入归纳假设
6. 剩下的算术交给 omega / ring / linarith

一个完整例子：

theorem reverse_length (xs : List α) : xs.reverse.length = xs.length := by
  induction xs with
  | nil => rfl
  | cons x rest ih =>
    simp [List.reverse_cons, ih]

常见卡点

「ih 用不上」 → 目标形式与 ih 不匹配。检查是不是需要 generalizing，或者先 rw/simp 把目标整理成 ih 能对上的样子。

「base case 就过不去」 → 命题本身可能错了。用 #eval 在具体小值上试一下。

「归纳步差一点点算术」 → 交给 omega（线性算术）、ring（交换环恒等式）、linarith（线性不等式）。见自动化。

「对错误的变量归纳」 → 多个变量时，选递归定义所依据的那个。sumAcc n acc 的递归在 n 上，就对 n 归纳。

归纳证明的难点几乎从不在「归纳」本身，而在「找到正确的归纳命题」。 这与写递归函数时「找到正确的递归不变量」是同一件事——再次印证命题即类型。

下一篇：结构化证明。

本页目录