4.1 Peano 公理：Nat 的歸納型別定義#

本節目標#

• 理解 Peano 五條公理，以及它們如何「生成」整個自然數系統
• 看懂 Lean 4 中 Nat 的 inductive type 定義原文，理解它與 Peano 公理的對應
• 認識 recursor：歸納型別附帶的「使用說明書」
• 了解 Nat.succ 與 + 的遞迴定義
• 說明為什麼 rfl 能證明 \(2 + 3 = 5\) —— 因為那是計算，不是證明

一、Peano 公理：用五句話造出自然數#

1889 年，Giuseppe Peano 用五條公理刻劃了自然數系統：

1. 零是自然數：存在一個常數 \(0\) 。
2. 後繼函數：每個自然數 \(n\) 都有後繼 \(S(n)\) （直覺上就是 \(n+1\) ）。
3. 零不是任何數的後繼：對所有 \(n\) ， \(S(n) \neq 0\) 。
4. 後繼是單射：若 \(S(m) = S(n)\) ，則 \(m = n\) 。
5. 數學歸納法：若一個性質 \(P\) 在 \(0\) 成立，且對 \(n\) 成立就對 \(S(n)\) 成立，則 \(P\) 對所有自然數成立。

這五句話看似樸素，威力卻驚人：整個算術 —— 加法、乘法、質數、唯一分解 —— 都可以從它們推出來。例如加法根本不需要「事先存在」，它是用遞迴定義出來的：

第一式是起點，第二式把加法「推」到每個後繼上。乘法同理： \(a \cdot 0 = 0\) ， \(a \cdot S(b) = a \cdot b + a\) 。

換句話說，自然數不是「被發現然後寫下性質」，而是由公理建構出來的資料結構。這正是 Lean 的切入點。

二、Lean 中的 Nat：inductive type 定義原文#

在 Lean 4 的核心函式庫（Init/Prelude.lean）中，Nat 的定義原文如下：

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

逐行對照 Peano 公理：

這就是 Lean 的設計哲學：公理不是寫在文件裡的句子，而是型別系統的規則。當你寫下 inductive，Lean 就自動為你保證了「建構子互不相同」與「建構子是單射」，這兩件事由 Nat.zero_ne_succ 與 Nat.succ.injEq 等定理免費提供。

幾個自然數的「字面值」其實是後繼的縮寫：

-- 3 = succ (succ (succ zero))
example : (3 : ℕ) = Nat.succ (Nat.succ (Nat.succ Nat.zero)) := rfl

三、recursor：歸納型別的使用說明書#

每個 inductive type 定義都附帶一個 recursor（消去子），它是 Lean 自動生成的核心函數。Nat.rec 的型別（簡化後）是：

#check @Nat.rec
-- {motive : Nat → Sort u} →
--   motive Nat.zero →
--   ((n : Nat) → motive n → motive n.succ) →
--   (t : Nat) → motive t

用中文讀這個型別：

• motive : Nat → Sort u：你想對每個自然數 \(n\) 證明（或定義）什麼性質 \(P(n)\)
• 第二個參數： \(P(0)\) 成立 —— 基底情形
• 第三個參數：對任意 \(n\) ， \(P(n)\) 成立蘊含 \(P(S(n))\) 成立 —— 歸納步驟
• 結論：對任意 t : Nat， \(P(t)\) 成立

這就是 Peano 第五公理的型別論版本！Nat.rec 同時身兼兩職：

• 當 motive 的值域是資料（如 Type）時，它是遞迴定義的工具
• 當 motive 的值域是命題（Prop）時，它是數學歸納法的原理

換言之，Lean 中「定義遞迴函數」與「數學歸納證明」共用同一台機器。第四、五章你會反覆看到這台機器的各種方便包裝（Nat.recOn、Nat.strongRecOn、induction tactic）。

四、加法的遞迴定義#

在 Lean 核心中，Nat.add 就是利用 recursor 定義的（簡化後）：

def Nat.add : Nat → Nat → Nat
  | n, Nat.zero   => n
  | n, Nat.succ m => Nat.succ (Nat.add n m)

這正是前一節的數學式： \(a + 0 = a\) ， \(a + S(b) = S(a + b)\) 。注意遞迴是在第二個參數上進行的 —— 這個選擇會影響某些證明（例如 \(a + b = b + a\) 需要歸納法，見 4.2 節）。

由於定義如此，下列性質變成定義上的重寫（definitional equality）：

example : (5 : ℕ) + 0 = 5 := rfl
example : (5 : ℕ) + 3 = 3 + 5 := rfl   -- 兩邊都會算成 8

但 n + 0 = n 當 n 是變數時就不是 rfl 能處理的，因為 n 的具體形狀未知，Lean 無法展開遞迴。這需要歸納法 —— 這是 4.2 節的主題。

五、rfl 證明 2 + 3 = 5：這是計算#

example : (2 : ℕ) + 3 = 5 := rfl

為什麼這樣就夠了？追蹤 Nat.add 2 3 的展開過程：

每一步都是套用定義 a + S(b) = S(a + b) 或起點 a + 0 = a。Lean 的核心系統（kernel）會直接把這些重寫執行到底，發現兩邊化約成同一個項，於是判定相等 —— 這就是 rfl（reflexivity，反身性）的工作原理。

重要的觀念區分：

• \(2 + 3 = 5\) 是計算（computation）：封閉項的化約
• \(\forall n, n + 0 = n\) 是證明（proof）：需要歸納法
• 甚至 \(\forall n, n + 1 = 1 + n\) 也是證明，因為 \(n\) 不是具體數字

decide tactic 是 rfl 的推廣：對可判定的封閉命題（例如 (3 : ℕ) < 7），它會直接計算真偽：

example : (2 : ℕ) + 3 = 5 := by decide
example : (3 : ℕ) < 7 := by decide

六、動手實驗#

把下面程式碼貼進 Lean 4（含 Mathlib）檔案，觀察結果：

import Mathlib

-- 觀察 recursor 的型別
#check @Nat.rec

-- 建構子互不相同與單射是免費的
example : (0 : ℕ) ≠ 3 := by decide
example (n : ℕ) (h : Nat.succ n = 5) : n = 4 := Nat.succ.inj h

-- 加法的兩條定義式
example (n : ℕ) : n + 0 = n := rfl
example (n : ℕ) : n + 1 = Nat.succ n := rfl

-- 但交換律就需要歸納法了
example (n : ℕ) : n + 1 = 1 + n := by
  induction n with
  | zero => rfl
  | succ n ih => simp [Nat.add_succ, ih]

小結與練習#

本節重點

• Peano 五公理中，前四條被 inductive Nat 的型別規則吸收，第五條（歸納法）成為 recursor
• Nat.rec 同時是遞迴定義與數學歸納法的基礎
• + 在第二個參數上遞迴： \(a + 0 = a\) 、 \(a + S(b) = S(a + b)\)
• rfl 證 \(2+3=5\) 靠的是計算；含變數的等式則需要歸納法

練習

1. ★☆☆☆☆ 用 rfl 證明 \((4 : ℕ) + 3 = 7\) ，並用自己的話寫出 Lean 的化約過程（至少三步）。
2. ★★☆☆☆ 用 Nat.succ.inj 證明：若 Nat.succ m = Nat.succ n 則 m = n。
3. ★★☆☆☆ 用 rfl 證明 \((3 : ℕ) * 2 = 6\) ，並查 #check @Nat.mul 觀察乘法的遞迴定義。
4. ★★★☆☆ 定義 inductive MyNat（自己的自然數，建構子取名 mzero / msucc），並用 #check @MyNat.rec 觀察 Lean 自動生成的 recursor，對照 Nat.rec。
5. ★★★★☆ 試著用 rfl 證明 (n : ℕ) + 0 = n（n 是變數），觀察錯誤訊息，解釋為什麼失敗 —— 這正是下一節要解決的問題。