跳轉到

4.2 數學歸納法：induction tactic 的五種用法#

本節目標#

  • 用多骨諾牌的意象掌握歸納法原理的直覺
  • 熟練 induction n with 的語法與兩個分支
  • 完整證明 \(\sum_{i=1}^{n} i = \dfrac{n(n+1)}{2}\)
  • 認識強歸納與 Nat.strongRecOn、雙變數歸納
  • 判斷 decide、omega、ring 何時可用，避免「該歸納卻硬算」
  • 認識歸納證明最常見的錯誤：漏掉基底情形

一、多骨諾牌的意象#

數學歸納法可以想像成一排多骨諾牌：

  1. 推倒第一張牌（基底情形）：性質 \(P(0)\) 成立
  2. 保證每張牌會推倒下一張（歸納步驟）：對任意 \(n\) ， \(P(n) \Rightarrow P(n+1)\)
  3. 結論：所有牌都會倒 —— \(P(n)\) 對所有自然數成立

關鍵在於理解歸納步驟的邏輯：它不是「假設 \(P(n)\) 對所有 \(n\) 成立」（那是循環論證），而是「若 \(P(n)\) 成立，則 \(P(n+1)\) 成立」的條件句。這正是 4.1 節 recursor 的第二、三個參數：

#check @Nat.rec
-- motive 0 →  (∀ n, motive n → motive n.succ) →  (∀ n, motive n)
--   ↑基底         ↑歸納步驟                            ↑結論

二、induction n with 基本語法#

example (n : ℕ) : n + 0 = n := by
  induction n with
  | zero => rfl
  | succ n ih => simp [Nat.add_zero, ih]

語法拆解：

  • induction n with：對變數 n 做歸納，產生兩個目標
  • | zero => ...：基底情形，把 n = 0 代入後的命題
  • | succ n ih => ...：歸納步驟；n 是新引入的變數，ih（induction hypothesis，歸納假設）就是 \(P(n)\) ，目標是 \(P(n+1)\)

陷阱提醒：induction 的對象必須是沒有被其他假設依賴的變數。如果你已經 intro m 並且 h : m = n 依賴了它，歸納前要先把假設泛化（generalize），Lean 會報錯提醒你。

三、範例：高斯求和公式#

目標： \(\displaystyle\sum_{i=1}^{n} i = \frac{n(n+1)}{2}\) 。

自然數上沒有除法封閉性，故乘以 2 避開分數，敘述改寫為：

\[ 2\sum_{i=1}^{n} i = n(n+1) \]
import Mathlib

open Nat

theorem sum_eq (n : ℕ) : 2 * (∑ i in range (n+1), i) = n * (n + 1) := by
  induction n with
  | zero => simp
  | succ n ih =>
    -- 目標：2 * (∑ i in range (n+2), i) = (n+1) * (n+2)
    rw [Finset.sum_range_succ]        -- 拆出最後一項 (n+1)
    rw [ih]                           -- 用歸納假設
    ring                              -- 代數整理收尾

三步的結構非常典型：

  1. 拆項：Finset.sum_range_succ 把 \(\sum_{i=0}^{n+1}\) 拆成 \(\sum_{i=0}^{n}\) 加上最後一項
  2. 代假設：rw [ih] 把小和換成 \(n(n+1)\)
  3. 整理：ring 處理 \(2(n(n+1) + (n+1)) = (n+1)(n+2)\) 這類多項式恆等式

這個「歸納拆項 → 代 ih → ring 收尾」的三段式，是自然數求和證明的萬用模板。

四、強歸納與 Nat.strongRecOn#

普通歸納只用到「前一位」。但有時你需要「所有更小的數」的假設，例如質因數分解：要證 \(n\) 可分解，需假設每個小於 \(n\) 的數都可分解。這叫強歸納（strong induction / complete induction）：

\[ \left(\forall n,\; \left(\forall m < n,\; P(m)\right) \Rightarrow P(n)\right) \Rightarrow \forall n,\; P(n) \]

Mathlib 的對應工具是 Nat.strongRecOn（及 tactic 包裝 induction n using Nat.strongRecOn）。它不需要單獨的基底情形： \(n = 0\) 時「所有 \(m < 0\) 的 \(m\) 」是空集合，假設自動成立（vacuously true）。

example (n : ℕ) (P : ℕ → Prop)
    (step : ∀ m, (∀ k, k < m → P k) → P m) : P n := by
  induction n using Nat.strongRecOn with
  | ind m ih => exact step m ih

直覺上，強歸納是讓骨諾牌「一次推倒所有前面的牌」，威力更大，且與良序原理（well-ordering principle）等價。

五、雙變數歸納#

當命題含兩個自然數變數時，要選對歸納對象。以加法交換律為例：

theorem add_comm_nat (n m : ℕ) : n + m = m + n := by
  induction n with
  | zero => simp [Nat.zero_add]
  | succ n ih => simp [Nat.add_succ, ih]

這裡對 n 歸納、把 m 固定為參數。兩個分支各用一條 Mathlib 的輔助定理：

  • 基底： \(0 + m = m\) （Nat.zero_add，注意這不是 rfl，因為 + 在第二參數遞迴）
  • 步驟： \(S(n) + m = S(n+m)\) （Nat.add_succ）再用 ih : n + m = m + n

第二種做法是雙重歸納（對 n 歸納，步驟內再對 m 歸納），但通常太囉唆。經驗法則：先對「遞迴結構在哪個變數上」的那個變數歸納 —— 這裡就是 n，因為 Nat.add 在第二參數遞迴，交換時是我們主動分析的對象。

六、decide、omega、ring：何時可用？#

三個自動化工具的分工，務必記清楚：

工具 適用範圍 例子
decide 封閉的可判定命題（無變數） 3 < 7、2^10 % 7 = 2
omega 線性整數／自然數算術（含變數，可含 <、≤、div/mod 的部分性質） ∀ a b : ℕ, (a + b) * 2 = 2*a + 2*b
ring 環上的多項式恆等式（乘法可出現） (a+b)^2 = a^2 + 2ab + b^2

重要限制：

  • omega 只做線性算術；n * m = m * n、 \(2\sum i = n(n+1)\) 這類含未知數相乘的命題它不管
  • ring 只做恆等式，不處理 < 與歸納結構
  • decide 遇到變數直接失敗 —— 它只能「算」，不能「證」

所以：具體數字的命題交給 decide；線性不等式交給 omega；代數整理交給 ring；結構性的命題（含變數相乘、求和、整除）終究要歸納法。

七、常見錯誤：漏掉 base case#

最經典的「假證明」：所有馬同色。對 \(n\) 匹馬歸納： \(n=1\) 顯然；任取 \(n+1\) 匹馬，去掉一匹後剩 \(n\) 匹同色（歸納假設），去掉另一匹也同色，兩組馬有重疊所以顏色一致，故 \(n+1\) 匹同色。錯在哪？ \(n = 1 \Rightarrow n = 2\) 時，兩組馬沒有重疊——歸納步驟在 \(n=1\) 這一步悄悄失效，而證明者從 \(n=2\) 開始檢查就會漏掉。

Lean 對此類錯誤是零容忍的：如果你在歸納步驟中用了 ih 卻沒有處理 n = 0 的情形，編譯器不會放行。

-- 錯誤示範：試圖不寫 base case
example (n : ℕ) : n + 0 = n := by
  induction n with
  | succ n ih => rfl    -- ❌ 錯誤：未處理分支 zero

在 Lean 中漏寫分支會直接編譯錯誤；寫了但步驟跳太快則會留下 sorry 警告。讓編譯器檢查歸納的完整性，正是形式化最大的紅利之一。

小結與練習#

本節重點

  • 歸納法 = 基底 + 歸納步驟；歸納步驟是條件句而非循環假設
  • induction n with | zero => ... | succ n ih => ...，ih 是你的朋友
  • 求和證明模板：拆項 → 代 ih → ring
  • 強歸納用 Nat.strongRecOn；雙變數先對「遞迴所在」的變數歸納
  • decide 算封閉命題、omega 管線性算術、ring 管多項式恆等式，但結構性命題要歸納
  • 漏 base case 在紙上可能騙過人，在 Lean 一定編譯失敗

練習

  1. ★☆☆☆☆ 證明 ∀ n : ℕ, 2 * n = n + n（提示：歸納 + ring 或 omega）。
  2. ★★☆☆☆ 證明 \(\sum_{i=1}^{n} (2i-1) = n^2\) （奇數和等於平方數）：用 Finset.sum_range_succ 拆項後歸納。
  3. ★★☆☆☆ 證明 ∀ n : ℕ, n < 2^n（提示：步驟中先用 Nat.pow_succ，再用 omega 收尾；先 decide 驗證 base）。
  4. ★★★☆☆ 證明 ∀ n : ℕ, n ≥ 2 → ∃ p, p ∣ n ∧ Nat.Prime p：用 induction n using Nat.strongRecOn（這是 5.1 節「質數無窮多」的暖身）。
  5. ★★★★☆ 寫出「所有馬同色」論證的 Lean 骨架，指出 Lean 在哪一行逼你承認 \(n=1 \Rightarrow n=2\) 的重疊問題，並用文字說明這個反例給非數學系的朋友聽。