01.1 第一個證明與 tactic 塊#

本章導讀#

本節是全書的起點，目標只有一個：讓你在電腦上跑出第一個證明。

我們會先建立正確的心態：Lean 4 同時是程式語言與證明器，你在 VS Code 裡寫的每一步，都會即時得到回饋。

讀完本節，你會理解 \(theorem\) 與 \(by\) 的分工，並用 \(intro\) 、 \(cases\) 、 \(exact\) 證完交換律。

請把本節當成開車的第一課：先發動，再學引擎原理。

想像你在跟一位很嚴格但很有耐心的助教對話。

你在 VS Code 左邊寫證明，右邊的 Lean 資訊視窗立刻告訴你還剩什麼目標，這就是互動式證明。

安裝只需要三件套：VS Code 編輯器、Lean 4 工具鏈、Lake 專案管理器，外加 VS Code 的 Lean 4 擴充套件。

Lake 好比便當盒：它幫你管好 Lean 版本、函式庫依賴與建置流程，你只要按一個鍵就能編譯檢查。

一個證明長這樣：先用 \(theorem\) 宣稱命題，再用 \(by\) 進入戰術模式，一行一個指令往下解。

Lean 的證明狀態可形式化為目標序列的轉換，記為 \(Goals \xrightarrow{tactic} Goals'\) 。

每個 \(tactic\) 都是函數：吃掉目前的目標，吐出零個或多個新目標，全部清空即證畢。

下表是本節三個基本戰術的規格， \(h : p\) 表示假設 \(h\) 證立命題 \(p\) 。

戰術	作用對象	形式規則	白話解釋
\(intro\)	\(p \to q\) 或 \(p \land q \to r\)	\(Goals[p \to q] \to Goals[q], \Gamma := \Gamma, h : p\)	把前提搬進上下文
\(cases\)	\(h : p \land q\)	\(Goals \to Goals[h_{1} : p, h_{2} : q]\)	把打包的證據拆開
\(exact\)	任意目標 \(p\)	若 \(h : p\) 則 \(Goals[p] \to [\,]\)	拿出現成證據結案

特別注意 \(by\) 的意義：它開啟一個戰術塊，塊內的每一步都必須保持型別正確。

其背後仍是同一判斷 \(\Gamma \vdash e : \alpha\) ，只是由機器幫你組出項 \(e\) 。

獨立來看，證明狀態是一個有序列表：

\[ Goals = [g_{1}, g_{2}, \dots, g_{n}] \]

當 \(n = 0\) 時顯示 \(No goals\) ，代表證明成功完成。

第一個經典例子是合取交換律：已知 \(p\) 且 \(q\) ，證明 \(q\) 且 \(p\) 。

theorem and_swap (p q : Prop) (h : p ∧ q) : q ∧ p := by
  cases h with
  | intro hp hq =>
    constructor
    · exact hq
    · exact hp

也可以寫成更短的兩行版本，先拆再合：

theorem and_swap_short (p q : Prop) (h : p ∧ q) : q ∧ p := by
  cases h with
  | intro hp hq => exact ⟨hq, hp⟩

證明過程中，右側資訊視窗的變化如下表所示。

步驟	執行的戰術	目前目標 \(Goals\)	上下文 \(\Gamma\)
初始	無	\(\vdash q \land p\)	\(h : p \land q\)
1	\(cases\)	\(\vdash q \land p\)	\(hp : p, hq : q\)
2	\(constructor\)	\(\vdash q\) , \(\vdash p\)	同上
3	\(exact\)	\(No goals\)	證畢

這裡 \(constructor\) 的意思是：要證 \(q \land p\) ，請把它拆成兩個子目標。

最後用兩次 \(exact\) 分別結案，全對上就結束了。

Lean 不是憑空出現的，它站在四十年的證明器傳統之上。

建議先讀誕生與自舉兩篇，再回頭看 \(by\) 塊的設計會更有感覺。