前言：lean與證明#

本文來自 ccc 與 gemini 的對話，網址

對話 -- https://gemini.google.com/app/830444409b2a4529
分享 -- https://share.gemini.google/hu2vppJ1KU29

ccc: 請舉例說明 lean 的證明是怎麼進行的#

Lean 是一個基於依值型別論（Dependent Type Theory）的交互式定理證明器（Interactive Theorem Prover）。在 Lean 中，證明的核心邏輯是 「Curry-Howard 對應」：

命題（Proposition） 就是 型別（Type）
證明（Proof） 就是該型別下的 值/項（Term/Element）

證明一個命題，本質上就是構造出一個符合該型別的項。

範例：證明邏輯中的「假言三段論」 (Hypothetical Syllogism)#

我們來證明一個非常基礎的邏輯命題：

對於任意命題 \(P, Q, R\) ，如果 \(P \to Q\) 且 \(Q \to R\) ，則 \(P \to R\) 。

1. 使用「戰術語法」（Tactic Mode，最常用的證明方式）#

在 Lean 4 中，最直觀的證明方式是使用 by 關鍵字進入戰術模式。戰術就像是一步步引導 Lean 推導結論的指令：

theorem hyp_syll (P Q R : Prop) (h1 : P → Q) (h2 : Q → R) : P → R := by
  intro hP     -- 假設 P 成立，並將這個前提命名為 hP
  apply h2     -- 要證明 R，根據 h2 (Q → R)，我們只需要證明 Q
  apply h1     -- 要證明 Q，根據 h1 (P → Q)，我們只需要證明 P
  exact hP     -- 我們已經有前提 hP : P，證明完成！

戰術執行的狀態變化（Lean 的內部思考過程）：#

當你寫這段 Lean 代碼時，Lean 編輯器右側的 Goal State（目標狀態）會隨著步驟實時更新：

初始狀態：
前提：P Q R : Prop, h1 : P → Q, h2 : Q → R
目標：⊢ P → R
執行 intro hP 後：
前提新增：hP : P
目標變更：⊢ R
執行 apply h2 後：
根據 h2 : Q → R，要得到 R，目標轉化為：⊢ Q
執行 apply h1 後：
根據 h1 : P → Q，要得到 Q，目標轉化為：⊢ P
執行 exact hP 後：
目標 ⊢ P 恰好就是已知前提 hP，目標消除，出現 Goals accomplished 🎉。

2. 使用「項語法」（Term Mode，底層構造）#

戰術模式本質上是在幫你自動編譯出一個底層函數。同一個定理，完全可以不用戰術，直接寫成一個函數：

theorem hyp_syll_term (P Q R : Prop) (h1 : P → Q) (h2 : Q → R) : P → R :=
  fun hP : P => h2 (h1 hP)

這段代碼的意思是：

h1 是一個能把 P 轉成 Q 的函數。
h2 是一個能把 Q 轉成 R 的函數。
給定一個 P 的證明 hP：
h1 hP 得到一個 Q 的證明。
h2 (h1 hP) 得到一個 R 的證明。
因此 fun hP => h2 (h1 hP) 就是一個從 P 到 R 的函數，即 P → R 的證明！

範例二：數學定理（證明 \(a + b = b + a\) ）#

對於涉及等式的數學證明，Lean 提供了強大的重寫（Rewrite）戰術 rw 或代數自動化戰術 simp/ring：

-- 證明自然數加法交換律
example (a b : Nat) : a + b = b + a := by
  rw [Nat.add_comm] -- 使用 Lean 標準庫中預先證明好的加法交換律定理

如果是稍微複雜一點的等式推導：

example (a b : Nat) : (a + b) * (a + b) = a * a + 2 * a * b + b * b := by
  ring -- ring 戰術會自動運用環（Ring）的公理進行代數展開與簡化

總結 Lean 證明的運作機制#

聲明命題：定義定理名稱、變量型別與目標結果。
互動式推推導：
使用 戰術（Tactics）：如 intro（假設）、apply（反向推導）、rw（代換）、induction（數學歸納法）一步一步簡化目標。
內核檢驗（Kernel Check）：
戰術執行完後，Lean 會將整個過程翻譯成一個最原始的「型別項」（Term）。
Lean 的核心（Kernel）會對這個項進行型別檢查。一旦檢查通過，數學上就宣告該證明完全正確且無懈可擊。

ccc: intro hP -- 假設 P 成立，並將這個前提命名為 hP，intro 的意義是什麼，為何這樣就會說，假設 P 成立？#

在邏輯與 Lean 中，intro 代表 「引進（Introduction）」，它的本質是 將邏輯上的「條件句（ \(\to\) ）」轉化為「已知的前提」。

1. 直觀理解：條件句的證明邏輯#

假設今天有人要你證明這個命題：

「如果下雨（ \(P\) ），地面就會濕（ \(R\) ）」（即 \(P \to R\) ）

你要怎麼開始證明這句話？你一定會說：「好，我們先假設現在真的下雨了（假設 \(P\) 成立），然後我們來看看地面會不會濕。」

這就是 intro 在做的事情：

當目標是 「若 \(P\) 則 \(R\) 」（ \(P \to R\) ） 時，你無法直接去證明 \(R\) （因為只有在 \(P\) 成立時 \(R\) 才需要成立）。
因此，你需要把 \(P\) 拆下來放到你的工具箱（已知前提區） 裡，此時你的證明目標就簡化成了 「證明 \(R\) 成立」。

2. 程式碼角度：`intro` 就是「定義函數的參數」#

在 Lean 底層（Curry-Howard 對應），「 \(P \to R\) 」的證明本質上是一個函數：

輸入：一個 \(P\) 成立的證明（叫它 hP）
輸出：一個 \(R\) 成立的證明

當你在 Lean 中寫 intro hP 時，就像在寫程式碼時宣告函數的參數一樣：

# 邏輯目標：P -> R
# 執行 intro hP 相當於寫下：
def prove_R(hP: P) -> R:
    # 現在函數內部已經擁有了參數 hP (P 的證明)
    # 接下來只需要回傳 R 的證明
    ...

所以 intro hP 的意思是：「給這個輸入參數起個名字叫 hP，接下來我們進入函數內部，專心處理輸出標的 \(R\) 。」

3. 目標狀態（Goal State）的變化#

透過觀察 Lean 的內部狀態，更能看出 intro 的作用：

執行 `intro hP` 前：#

-- 已知前提 (Hypotheses)
P Q R : Prop
h1 : P → Q
h2 : Q → R

-- 目標 (Goal)
⊢ P → R

(此時目標是一個條件句，你還不能直接拿 \(P\) 來用)

執行 `intro hP` 後：#

-- 已知前提 (Hypotheses)
P Q R : Prop
h1 : P → Q
h2 : Q → R
hP : P      -- <--- P 被引進（intro）到了已知前提，並命名為 hP

-- 目標 (Goal)
⊢ R         -- <--- 目標只剩下箭頭右邊的 R

總結#

intro 命名自邏輯學中的 「蘊涵引進律（Implication Introduction）」。

每當你的目標長成 A → B 的形狀時，使用 intro h 就是在跟 Lean 說：

「把箭頭左邊的 \(A\) 拿出來當作已知前提（命名為 \(h\) ），並把目標縮減為證明箭頭右邊的 \(B\) 。」

ccc: hP 一定要這樣寫嗎？不能隨便命名 xY 這樣嗎？hP 有隱含是和 P 有關係嗎？#

可以隨便命名！ hP 只是使用者自訂的變數名稱，改寫成 xY、foo 或 my_proof 程式都能正常運作。

Lean 裡面並沒有任何語法規定「名稱必須與型別對應」。

1. 為何可以寫成 `xY`？#

如果將剛剛的代碼改寫成這樣：

theorem hyp_syll (P Q R : Prop) (h1 : P → Q) (h2 : Q → R) : P → R := by
  intro xY     -- 這裡完全可以使用 xY
  apply h2     
  apply h1     
  exact xY     -- 後續使用時，名稱保持一致即可

Lean 的編譯器完全能順利通過。

在程式語言的視角下，intro xY 就像你在寫函數時定義參數一樣：

def add(x: Int) 裡的 x 只是個代號。
你改成 def add(xY: Int)，電腦一樣知道它是一個整數。

2. 那 `hP` 的命名有沒有隱含關係或慣例？#

雖然 Lean 本身不強制，但 Lean 社群有一套約定俗成的命名慣例（Naming Conventions），主要是為了讓證明過程更容易閱讀：

h 前綴：代表 hypothesis（前提/假設） 或 proof hint。
P 後綴：代表這個前提對應的是命題 ** \(P\) **。

所以：

hP 直觀代表「hypothesis of P」（ \(P\) 的前提）
h1 代表「第一個前提」
h_rain 代表「下雨的前提」

如果你命名成 xY，Lean 依然看得懂，但其他閱讀你代碼的人（包含一個月後的你自己）可能無法一眼看出 xY 究竟代表什麼命題的證明。

3. 甚至可以不命名（讓 Lean 自動幫你取名）#

如果你連名稱都懶得想，直接寫 intro 不帶任何名稱，Lean 會自動根據型別幫你生成一個名稱：

theorem hyp_syll (P Q R : Prop) (h1 : P → Q) (h2 : Q → R) : P → R := by
  intro        -- Lean 會自動幫你把這個前提命名（通常是 h）

此時在右側的 Goal 視窗中，你會看到前提區多了一個 h : P。

總結#

語法上：hP 只是個自訂名稱，命名為 xY 完全沒問題。
語意上：hP 是社群習慣的寫法（h 代表 Hypothesis 假設，P 代表命題名稱），用來提升證明的可讀性。

ccc: intro hP -- 假設 P 成立，並將這個前提命名為 hP，為何這一句會是假設 P 成立？（既然和名稱無關）#

決定「假設 \(P\) 成立」的，完全不是名稱 hP**，而是你當時面對的證明目標（Goal）**。

關鍵在於：目標裡的箭頭 \(\to\)#

在執行 intro 之前，Lean 右側面板顯示的證明目標長這樣：

\[ \vdash P \to R \]

這個目標的結構是：「箭頭左邊是 \(P\) 」，「箭頭右邊是 \(R\) 」。

當你下達 intro 指令時，Lean 的機制固定如下：

自動抓取：Lean 自動去拆解當前的目標，把箭頭左邊的命題（在這裡就是 \(P\) ）拿出來。
放入前提：把這個命題變成已知假設（假設 \(P\) 成立）。
套用名字：把你寫在 intro 後面的名字（無論是 hP、xY 還是 foo）貼在這個新假設上。
更新目標：把目標縮減為箭頭右邊的命題（ \(R\) ）。

如果目標換了，`intro` 抓到的假設就會不同#

為了讓你更有感覺，假設我們換一個完全不同的目標：

情況 A：目標是 \(\vdash \text{IsRain} \to \text{Wet}\)#

intro xY

Lean 看到的目標：箭頭左邊是 \(\text{IsRain}\) 。
發生的事：Lean 會假設「下雨（ \(\text{IsRain}\) ）成立」，並把這個假設命名為 xY。
新目標變為： \(\vdash \text{Wet}\)

情況 B：目標是 \(\vdash Q \to R\)#

intro xY

Lean 看到的目標：箭頭左邊是 \(Q\) 。
發生的事：Lean 會假設「 \(Q\) 成立」，並把這個假設命名為 xY。
新目標變為： \(\vdash R\)

用「自動販賣機」來比喻#

你可以把 intro 想成一台「目標拆解機」：

輸入（當前的目標）：包裝盒上寫著 \(P \to R\) 。
機器的固定功能 (intro)：拆開盒子，把裡面的內容物 \(P\) ** 拿出來放在桌上，並把盒裝貼紙 \(R\) ** 留給下一階段。
你給的名字 (hP 或 xY)：你拿筆在剛剛被拿出來的 \(P\) 上面塗鴉寫下一個標籤（標籤叫什麼，完全不影響拿出來的東西是 \(P\) ）。

所以：

「假設 \(P\) 成立」 來自於目標 \(P \to R\) 的結構。
hP 或 xY** 只是你綁在這個假設上的姓名牌**。

ccc: 能用邏輯學的解釋，來解釋 intro, apply, exact, .... 這些語句嗎？#

在邏輯學（特別是自然演繹法 Natural Deduction）中，每一個 Lean 的戰術（Tactic）都精準對應到一套推導規則（Inference Rules）。

Lean 的靈魂來自 Curry-Howard 對應：

命題 (Proposition) \(\approx\) 型別 (Type)
證明 (Proof) \(\approx\) 值 / 程式 (Term)

以下為您用邏輯學與自然演繹法，剖析 Lean 最核心的戰術語句：

1. `intro` (引進) \(\approx\) 蘊涵引進律 ( \(\to\) -Introduction)#

邏輯學意義：若要證明「若 \(A\) 則 \(B\) 」（ \(A \to B\) ），你可以先假設 \(A\) 成立，在此假設下若能推导出 \(B\) ，則 \(A \to B\) 成立。
自然演繹法符號：

\[ \frac{\begin{matrix} [A] \\ \vdots \\ B \end{matrix}}{A \to B} \quad (\to\text{-Intro}) \]

Lean 的運作：
執行前目標： \(\vdash A \to B\)
執行 intro h 後：將 \(A\) 加入已知前提欄（命名為 \(h\) ），目標轉化為 \(\vdash B\) 。

2. `apply` (應用/反向套用) \(\approx\) 假言推理 / 蘊涵消去律 ( \(\to\) -Elimination / Modus Ponens)#

邏輯學意義：即傳統的 Modus Ponens（假言推理）——已知 \(A \to B\) ，若要證明 \(B\) ，只需轉而證明 \(A\) 即可。
自然演繹法符號：

\[ \frac{A \to B \quad A}{B} \quad (\to\text{-Elim}) \]

Lean 的運作（反向推導）：
執行前目標： \(\vdash B\) ，且手中已有前提 \(h : A \to B\) 。
執行 apply h 後：Lean 知道「有了 \(A\) 就能用 \(h\) 得到 \(B\) 」，因此把目前的目標改為 \(\vdash A\) 。

3. `exact` (精確給出) \(\approx\) 假設公理 / 同一律 (Axiom of Identity / Assumption)#

邏輯學意義：如果你要證明的目標 \(A\) ，已經完全存在於你的已知前提中，證明直接完成。
自然演繹法符號：

\[ \frac{}{A \vdash A} \quad (\text{Assumption}) \]

Lean 的運作：
執行前目標： \(\vdash A\) ，且已知前提區有 \(h : A\) 。
執行 exact h 後：直接指明「前提 \(h\) 就是解答」，該目標立即被消除閉合。

4. `cases` / `rcases` (分情況討論) \(\approx\) 析取消去律 ( \(\lor\) -Elimination)#

邏輯學意義：如果你知道 \(A \lor B\) （ \(A\) 或 \(B\) 成立），要證明 \(C\) ，你需要分別證明兩種情況：
假設 \(A\) 成立時， \(C\) 成立。
假設 \(B\) 成立時， \(C\) 成立。
自然演繹法符號：

\[ \frac{A \lor B \quad \begin{matrix} [A] \\ \vdots \\ C \end{matrix} \quad \begin{matrix} [B] \\ \vdots \\ C \end{matrix}}{C} \quad (\lor\text{-Elim}) \]

Lean 的運作：
前提： \(h : A \lor B\) ，目標： \(\vdash C\) 。
執行 cases h 後：分支成兩個子目標（Sub-goals）：
子目標 1：前提加上 \(hA : A\) ，目標仍為 \(\vdash C\) 。
子目標 2：前提加上 \(hB : B\) ，目標仍為 \(\vdash C\) 。

5. `constructor` (構造) \(\approx\) 合取引進律 ( \(\land\) -Introduction)#

邏輯學意義：若要證明「 \(A\) 且 \(B\) 」（ \(A \land B\) ），你需要把目標拆成兩個獨立的證明任務：先證明 \(A\) ，再證明 \(B\) 。
自然演繹法符號：

\[ \frac{A \quad B}{A \land B} \quad (\land\text{-Intro}) \]

Lean 的運作：
執行前目標： \(\vdash A \land B\) 。
執行 constructor 後：產生兩個子目標，分別為 \(\vdash A\) 與 \(\vdash B\) 。

6. `have` (斷言/中間步驟) \(\approx\) 剖斷律 (Cut Rule)#

邏輯學意義：在推導長證明時，先證明出一個中間結論 \(K\) ，再利用 \(K\) 去推導最終目標 \(C\) 。
自然演繹法符號：

\[ \frac{\Gamma \vdash K \quad \Gamma, K \vdash C}{\Gamma \vdash C} \quad (\text{Cut Rule}) \]

Lean 的運作：
**執行 have hK : K := by ...**：
你需要先完成一個證明目標 \(\vdash K\) 。
完成後， \(hK : K\) 會被加入主證明的已知前提欄，繼續用來證明原目標。

邏輯學對照總整理#

戰術語句	邏輯學術語	運算方向	邏輯意義
`intro`	蘊涵引進律 ( \(\to\) -Intro)	正向拆目標	假設箭頭左邊成立，放入前提區
`apply`	假言推理 ( \(\to\) -Elim)	反向倒推	將目標 \(B\) 根據 \(A \to B\) 退回證明 \(A\)
`exact`	同一律 (Assumption)	閉合目標	宣告「目標就是這個已知前提」
`constructor`	合取引進律 ( \(\land\) -Intro)	拆分目標	將 \(A \land B\) 拆成證明 \(A\) 與證明 \(B\)
`cases`	析取消去律 ( \(\lor\) -Elim)	分歧推導	針對 \(A \lor B\) 進行分情況討論
`have`	剖斷律 (Cut Rule)	建立引理	先證明中間節點 \(K\) ，再以此推導

傳統邏輯學通常是從前提「正向推導」到結論；而 Lean 的戰術模式最厲害的地方，是允許你從結論「反向倒推」（Backward Reasoning）（如 apply），直到目標退化成已知的公理或前提（exact）為止。

ccc: 請說明 example (a b : Nat) : (a + b) * (a + b) = a * a + 2 * a * b + b * b := by ring -- ring 戰術會自動運用環（Ring）的公理進行代數展開與簡化，ring 的戰術是什麼？整個證明會是如何進行的？#

ring 戰術是 Lean 中專門用來處理可交換環（Commutative Ring）中代數等式的自動化戰術（Automated Tactic / Decision Procedure）。

在傳統的手動證明中，要證明 \((a + b)^2 = a^2 + 2ab + b^2\) ，你必須一步一步引用乘法分配律、加法結合律、乘法交換律等公理。而 ring 戰術能自動完成所有繁瑣的代數展開、展開項排序與同類項合併。

1. `ring` 戰術的背後演算法：規範化 (Normalization)#

ring 戰術的核心運作機制叫做 「多項式規範化（Polynomial Normalization）」：

當你要求 ring 證明 LHS = RHS（左式 = 右式）時，它會按照以下固定步驟進行：

完全展開（Expansion）：
利用乘法分配律 \(x(y + z) = xy + xz\) ，把等式兩邊的所有括號完全拆開。
變數排序（Term Ordering）：
根據一套固定的字典序（Lexicographical Order）規則，將單項式內部的變數重新排序。例如將 \(b \cdot a\) 統一重寫為 \(a \cdot b\) 。
同類項合併與常數化簡（Simplification）：
將結構相同的單項式係數相加（例如 \(a \cdot b + a \cdot b\) 化簡為 \(2 \cdot a \cdot b\) ）。
比對標準型（Canonical Form Comparison）：
將左式與右式各自化簡為唯一的「標準多項式形式」。
如果兩邊化簡後的字面形式（Literal Form）完全相同，ring 就宣告等式成立，證明完成。

2. 如果「手動證明」，整個過程是如何進行的？#

如果不使用 ring 戰術，而是用基本戰術（如重寫 rw）手動推導，Lean 內部實際上進行了以下漫長的公理代換：

example (a b : Nat) : (a + b) * (a + b) = a * a + 2 * a * b + b * b := by
  -- 1. 對右邊的 (a + b) 使用乘法分配律：(x + y) * z = x * z + y * z
  rw [Nat.add_mul]
  -- 當前目標：a * (a + b) + b * (a + b) = a * a + 2 * a * b + b * b

  -- 2. 對左半部 a * (a + b) 使用乘法分配律：x * (y + z) = x * y + x * z
  rw [Nat.mul_add]
  -- 當前目標：a * a + a * b + b * (a + b) = a * a + 2 * a * b + b * b

  -- 3. 對右半部 b * (a + b) 使用乘法分配律
  rw [Nat.mul_add]
  -- 當前目標：a * a + a * b + (b * a + b * b) = a * a + 2 * a * b + b * b

  -- 4. 運用乘法交換律，將 b * a 重寫為 a * b
  rw [Nat.mul_comm b a]
  -- 當前目標：a * a + a * b + (a * b + b * b) = a * a + 2 * a * b + b * b

  -- 5. 調整括號（加法結合律）並合併 a * b + a * b = 2 * a * b ...
  -- (後續還需要多次套用 Nat.add_assoc 與數字 2 的定義展開)
  sorry

可以看到，手動證明需要處理非常多繁瑣的括號與位置調整。ring 戰術正是將這一連串套用公理的過程演算法化。

3. `ring` 如何確保證明的嚴謹性？（反射戰術 Reflection）#

Lean 是一個強調高度嚴謹的系統，ring 戰術並不是「黑盒子直接宣稱正確」，它是透過依值型別論中的「反射技術」（Tactic Reflection）來工作的：

語法樹化（AST Parsing）： Lean 將代數算式抽象化為演算語法樹（例如把 + 轉化為抽象節點 Add）。
算式求值演算（Decision Procedure）：在 Lean 內部執行一個經由數學證明過「正確性」的多項式化簡演算法。
產出證明項（Proof Term）： ring 執行完畢後，會生成一個不依賴 ring 戰術本身的底層 Lean 型別項（Term），並交給 Lean 的核心（Kernel）檢查。

只要 Kernel 檢查無誤，這個代數等式就在邏輯上被嚴格證明了。

4. `ring` 適用於哪些範圍？#

ring 適用於任何符合可交換環（Commutative Ring）公理的結構：

自然數 Nat（雖然自然數是半環 Semiring，但 ring / ring_nf 也能處理加法與乘法展開）
整數 Int ( \(\mathbb{Z}\) )
有理數 Rat ( \(\mathbb{Q}\) )
實數 Real ( \(\mathbb{R}\) )
複數 Complex ( \(\mathbb{C}\) )
任何自訂的代數環結構

注意：如果算式中包含除法（/）或分數，ring 可能無法處理，此時需要使用更進階的 field_simp 或 ring 的延伸戰術。