4.1 相等、重寫與 simp：把等式當變形金剛#

本章導讀#

前面學會了邏輯骨架，現在要學證明裡最常用的苦工：等式變形。看到 \(a + b = b + a\) 要能從左換到右，看到 \(n + 0\) 要能消掉，都是靠重寫。學完這一節，你會用 \(rfl\) 處理定義相等，用 \(rw\) 定向搬運等式，用 \(simp\) 一次清掉一堆瑣事。

淺顯說明#

想像等式是一條雙向隧道：知道 \(h : l = r\) ，就代表任何地方的 \(l\) 都可以換成 \(r\) ，反之亦然。 Lean 的 \(rw\) 就是施工隊： \(rw \; [h]\) 把目標裡的左邊挖掉換成右邊， \(rw \; [\leftarrow h]\) 則倒著換回來。方向錯了會卡住，這時看看目標長相，換個箭頭再試一次。

另一個小幫手是 \(rfl\) 。它只認「長得一樣」的等式，例如 \(2 + 2 = 4\) 按定義算一算就通了。但 \(a + b = b + a\) 對任意 \(a, b\) 可不是按定義就算得出來的，需要真正的定理加 \(rw\) 。而 \(simp\) 像大掃除：它背了一整本「一定變簡單」的等式集，看到 \(n + 0\) 就消掉、看到 \(0 + n\) 也消掉，一次清乾淨。記住分工：小事找 \(rfl\) ，指名換找 \(rw\) ，雜事全包找 \(simp\) 。

正規理論#

相等是歸納型 \(Eq\) ，只有一個構造子 \(rfl\) ，而重寫是把等式證明代入上下文的計算。

\[ \frac{}{\Gamma \vdash rfl : a = a} \; (EqI) \qquad \frac{\Gamma \vdash h : a = b \quad \Gamma \vdash P(a)}{\Gamma \vdash h ▸ P(a) : P(b)} \; (EqE) \]

\[ rw[h] : Goal[a] \to Goal[b] \quad\text{其中}\quad h : l = r \]

tactic	數學含義	用法	備註
\(rfl\)	\(a = a\) 自反	目標兩邊定義相等時收尾	按 \(\delta \beta \iota\) 化簡後一致即成
\(rw \; [h]\)	由左向右代入 \(l \to r\)	\(rw \; [Nat.add\_comm \; a \; b]\)	最常用方向
\(rw \; [\leftarrow h]\)	由右向左代入 \(r \to l\)	\(rw \; [\leftarrow Nat.add\_zero \; n]\)	展開或還原時用
\(simp\)	依 \(simp\) 集反覆重寫	\(simp\) 或 \(simp \; [h]\)	會用內建等式集自動化簡
\(congr\) ／ \(funext\)	同餘與函數外延	一句話帶過：逐項相等即整體相等	外延性詳見第 6 章宇宙與公理

一句話補充外延性： \(congr\) 把 \(f \; x = g \; y\) 拆成 \(f = g\) 與 \(x = y\) 兩個子目標；函數相等另需公理 \(funext\) 說逐點相等即函數相等。

簡易範例#

小目標：用重寫把 \(a + b\) 換成 \(b + a\) ，體會三種收尾的差異。

-- 例一：指名重寫，最透明
example (a b : Nat) : a + b = b + a := by
  rw [Nat.add_comm]

-- 例二：simp 自動化，最省力
example (a b : Nat) : a + b = b + a := by
  simp [Nat.add_comm]

-- 例三：rfl 收尾，需先把形狀對齊
example (n : Nat) : n + 0 = n := by
  rw [Nat.add_zero]
  rfl

證明狀態表（例一，目標為 \(a + b = b + a\) ）：

步驟	tactic	證明狀態 Goals
起始	—	\(a \; b : Nat \vdash a + b = b + a\)
1	\(rw \; [Nat.add\_comm]\)	\(a \; b : Nat \vdash b + a = b + a\)
2	自動 \(rfl\)	無剩餘目標，證畢

注意例一的魔法： \(rw\) 結束後兩邊長得一樣，Lean 自動補 \(rfl\) 關門。例三則示範方向感： \(Nat.add\_zero : n + 0 = n\) ，由左向右剛好把 \(n + 0\) 消掉。若寫成 \(rw \; [\leftarrow Nat.add\_zero]\) 反而會把 \(n\) 膨脹成 \(n + 0\) ，越寫越長，初學者可用此對比體會方向。

歷史典故#

根岑的自然演繹：等式的左右代入正是自然演繹消去規則的親戚， \(rw\) 的定向精神可回溯到這套對稱設計。
羅賓遜的歸結原理：以合一與代入為核心的機械推理， \(rw\) 按模式尋找 \(l\) 再換成 \(r\) 的做法正是同一血脈。
霍華德的公式即型別： \(rfl\) 作為 \(Eq\) 唯一的構造子，完美示範「證明即程式」：自反性就是一個零參數的程式值。

習題#

用 \(rw\) 證明 \((n : Nat) : n + 0 = n\) ，再故意改用 \(rw \; [\leftarrow Nat.add\_zero]\) 跑一次，記錄目標如何變長。說明何時該用正向、何時用逆向。
用 \(simp\) 化簡 \((a : Nat) : 0 + (a + 0) = a\) 。提示：直接 \(simp\) 即可。再試 \(simp \; only \; [Nat.zero\_add, Nat.add\_zero]\) 觀察「只用指定等式」的效果。
試證明 \((a \; b : Nat) : (a + b) + 0 = b + a\) 。提示：先 \(rw \; [Nat.add\_zero]\) 再 \(rw \; [Nat.add\_comm]\) 。思考兩步能否交換順序。