4.2 自然數與數學歸納法：從零開始的無限階梯#
本章導讀#
證明有了邏輯與等式還不夠，遇到「對一切自然數成立」就需要歸納法。 自然數是 Lean 的第一個歸納型別：從 \(zero\) 出發，一次加一層 \(succ\) ，就能蓋出整座無限高塔。 學完這一節，你會讀懂 \(Nat.rec\) 歸納子，會用 \(induction\) 拆出兩個子目標，並親手證明零加恆等與加法交換律骨架。
淺顯說明#
想像一排無限長的骨牌。老闆要求你證明「全部都會倒」。 你不用親手推每一塊，只要做兩件事：先推倒第零塊，再證明「任一塊倒了，下一塊跟著倒」。 這就是歸納法：基底加遞推等於全體。
在 Lean 裡，自然數只有兩種長相： \(Nat.zero\) 就是 \(0\) ， \(Nat.succ \; n\) 就是 \(n + 1\) 。 數字 \(3\) 其實是 \(succ \; (succ \; (succ \; zero))\) ，一層包一層。 所以 \(induction \; n\) 永遠生出兩個子目標： \(n = 0\) 時成立嗎？假設 \(n\) 成立，能推出 \(succ \; n\) 成立嗎？ 第二個子目標裡會多一個「歸納假設」，它是免費送你的武器，記得拿起來用。
正規理論#
自然數是歸納型 \(Nat = zero \mid succ(Nat)\) ，其歸納子 \(Nat.rec\) 同時是遞迴函數與歸納證明。
| 概念 | 數學記號 | Lean 寫法 | 說明 |
|---|---|---|---|
| 零 | \(zero\) | \(Nat.zero\) 或 \(0\) | 骨牌第零塊 |
| 後繼 | \(succ(n)\) | \(Nat.succ \; n\) | 包一層即加一 |
| 歸納子 | \(Nat.rec\) | \(Nat.rec \; base \; step \; n\) | 遞迴與歸納的共同本體 |
| 加法定義 | \(add(n, zero) = n\) | \(Nat.add \; n \; zero = n\) | 递归的第一條等式 |
| 加法遞推 | \(add(n, succ \; m) = succ(add(n, m))\) | \(Nat.add \; n \; (succ \; m)\) | 递归的第二條等式 |
| tactic | 兩目標分裂 | \(induction \; n\) | 生出基底與遞推兩個子目標 |
歸納子 \(Nat.rec\) 的圖景是：一端接住基底證明 \(P(0)\) ，另一端接住遞推函數 \(P(n) \to P(n+1)\) ，中間對任意 \(n\) 吐出 \(P(n)\) 。 tactic \(induction\) 只是它的互動包裝：幫你把一個目標劈成兩半，並把歸納假設 \(ih\) 放入上下文。
簡易範例#
先看加法定義，再證零加恆等，最後搭交換律骨架。
-- 加法定義（示意）：對第二個參數遞迴
-- def Nat.add : Nat → Nat → Nat
-- | n, Nat.zero => n
-- | n, Nat.succ m => Nat.succ (Nat.add n m)
-- 零加恆等：需歸納，因加法只對右邊拆解
theorem zero_add_id (n : Nat) : 0 + n = n := by
induction n with
| zero => rfl
| succ k ih => simp [Nat.add_succ, ih]
-- 交換律骨架：先把引理備齊，再對一邊歸納
theorem add_comm_sketch (a b : Nat) : a + b = b + a := by
induction a with
| zero => simp [zero_add_id]
| succ k ih => simp [Nat.add_succ, Nat.succ_add, ih]
證明狀態表（ \(zero\_add\_id\) ，目標為 \(0 + n = n\) ）：
| 步驟 | tactic | 證明狀態 Goals |
|---|---|---|
| 起始 | — | \(\vdash \forall n, 0 + n = n\) ，上下文有 \(n : Nat\) |
| 1 | \(induction \; n\) | 分裂為 \(\vdash 0 + 0 = 0\) 與 \(k, ih : 0 + k = k \vdash 0 + succ \; k = succ \; k\) |
| 2 | 基底 \(rfl\) | 基底關閉，只剩遞推目標 |
| 3 | \(simp \; [Nat.add\_succ, ih]\) | 無剩餘目標，證畢 |
為何 \(n + 0 = n\) 用 \(rfl\) 即成，而 \(0 + n = n\) 卻要歸納？因為加法定義只會拆右邊。 左加零是「天生」的，右加零卻要一層層剝開 \(n\) 的 \(succ\) 結構。 交換律骨架同理：先備好 \(zero\_add\_id\) 與 \(succ\_add\) 引理，歸納時用 \(simp\) 把 \(ih\) 餵回去即可。
歷史典故#
- 弗雷格《概念文字》：給出自然數的邏輯主義雛形，讓歸納法第一次有了形式根基， \(Nat.rec\) 正是這條路線的後代。
- 霍華德的公式即型別：歸納證明即遞迴程式， \(induction\) 拆兩目標對應 \(rec\) 接兩參數，證明與程式在此合一。
- Prolog 邏輯程式：以 Horn 子句做遞迴搜尋， \(zero\) 與 \(succ\) 的兩子句結構與 Prolog 的基底加遞推如出一轍，可互相對照。
習題#
- 證明右加零 \((n : Nat) : n + 0 = n\) 。提示： \(induction \; n\) ，基底 \(rfl\) ，遞推用 \(simp \; [ih]\) 。對比本節的左加零，說出何者需用到加法定義。
- 證明後繼加一 \((n : Nat) : n + 1 = Nat.succ \; n\) 。提示： \(simp\) 或 \(rfl\) 即可。再用它把 \(zero\_add\_id\) 的遞推步驟改寫成 \(rw\) 版本。
- 補完交換律骨架：先證引理 \(succ\_add : succ \; a + b = succ \; (a + b)\) （對 \(b\) 歸納），再回頭完成 \(add\_comm\_sketch\) 。記錄每個引理各用了幾次 \(ih\) 。