Lean 程式與證明 -- 教材#

以淺顯的方式，搭配簡易範例與正規 TeX 數學推導，說明 Lean（依賴型別證明器／函數式程式語言）背後的理論與實作。每一節都引用 ../ 資料夾的歷史卷宗作為典故，讓理論與歷史並行。

Lean 的核心，是「證明」與「程式」合而為一：

判斷： \(\Gamma \vdash e : \alpha\) ，在上下文 \(\Gamma\) 中項 \(e\) 具型別 \(\alpha\) 。
命題即型別： \(Proof(p) \simeq p\) ，證明就是住在命題型別裡的程式。
依賴函數： \(\Pi (x : A), B(x)\) ，值域可依賴參數，謂詞與全稱量詞的本體。
歸納： \(Nat = zero \mid succ(Nat)\) ，遞迴定義與歸納證明同一枚硬幣。
重寫： \(rw[h] : Goal[a] \to Goal[b]\) ，等式是最常用的證明變換。
tactic 狀態： \(Goals \xrightarrow{tactic} Goals'\) ，互動證明的每一步都是目標轉換。

目錄#

第 1 章：Lean 初見——證明器也是程式語言#

節	標題	重點
01.1	第一個證明與 tactic 塊	VS Code＋Lake、 \(by\) 塊、 \(intro\) ／ \(exact\) 、證明狀態閱讀
01.2	項、表達式與型別宇宙	\(\Gamma \vdash e : \alpha\) 、 \(Type_{0} : Type_{1}\) 、 \(Prop\) 、 \(def\) ／ \(theorem\)

第 2 章：命題邏輯——Gentzen 在 Lean 裡復活#

節	標題	重點
02.1	蘊涵：intro 與 apply	\(p \to q\) 、引入／消去規則、前向與後向推理
02.2	合取與析取：cases 與 constructor	\(p \land q\) 、 \(p \lor q\) 、 \(cases\) 、 \(\langle , \rangle\) 、 \(left\) ／ \(right\)
02.3	否定、假與古典邏輯	\(\lnot p := p \to False\) 、 \(False.elim\) 、排中律、 \(byContradiction\)

第 3 章：量詞——從語句到謂詞#

節	標題	重點
03.1	全稱量詞 forall	\(\forall x, P(x)\) 即 \(\Pi\) 型、 \(intro\) ／ \(apply\) 、實例化
03.2	存在量詞 exists	\(\exists x, P(x)\) 即 \(\Sigma\) 型、 \(use\) 見證、 \(cases\) 消去

第 4 章：相等與歸納——證明的兩隻腳#

節	標題	重點
04.1	相等、重寫與 simp	\(Eq\) 、 \(rfl\) 、 \(rw\) 、 \(simp\) 集、外延性
04.2	自然數與數學歸納法	\(Nat\) 歸納子、 \(induction\) 、加法交換律實戰

第 5 章：歸納型別——自訂資料即自訂邏輯#

節	標題	重點
05.1	歸納型別與模式匹配	\(inductive\) 、構造子、 \(match\) 、串列與樹
05.2	結構歸納與遞迴函數	終止性、結構遞減、歸納證明的瀑布

第 6 章：依賴型別——Curry–Howard 的應許之地#

節	標題	重點
06.1	命題即型別、證明即程式	三對照表、化簡即求值、項式證明 vs tactic 證明
06.2	宇宙、公理與古典相容	\(Type\) 階層、 \(propext\) ／ \(funext\) ／ \(choice\) 、商型別

第 7 章：mathlib 之旅——百萬行函式庫的使用法#

節	標題	重點
07.1	代數結構與型別類	\(Group\) ／ \(Ring\) 、 \(instance\) 、 \(inferInstance\) 、tabled 消解
07.2	決策程序：ring、omega、simp	正規形判定、線性算術、 \(simp\) 集管理

第 8 章：自動化與未來——自寫 tactic 到 AI 證明#

節	標題	重點
08.1	自寫 tactic 與元程式	\(syntax\) ／ \(macro\) ／ \(elab\) 、衛生性、簡單實戰
08.2	從 Lean 到 AI 證明	Sledgehammer 式錘子、AlphaProof 管線、規格導向開發

附錄#

節	標題	重點
A1	Lean 符號與 tactic 速查表	本書使用的型別、邏輯符號與常用 tactic

核心概念地圖#

                        ┌─────────────────────────────────────────┐
                        │           核心判斷                      │
                        │   Γ ⊢ e : α （項 e 住在型別 α 裡）      │
                        └───────────────────┬─────────────────────┘
                                            │
          ┌─────────────────────────────────┼─────────────────────────────────┐
          ▼                                 ▼                                 ▼
   【邏輯即規則】                    【資料即歸納】                    【自動化即程式】
   • → : intro / apply              • Nat / List / Tree              • rw / simp 重寫
   • ∧∨ : cases / constructor       • 構造子 / match                  • ring / omega 判定
   • ¬ : → False / 反證法           • 結構歸納 / 終止遞迴            • macro / elab 自寫 tactic
   • ∀∃ : Π / Σ                     • ΠΣ 即量詞本體                  • AI 錘子 / AlphaProof

學習路徑建議#

入門：01.1 → 01.2 → 02.1（先跑起第一個證明，讀懂證明狀態與宇宙）。
邏輯基礎：02.2 → 02.3 → 03.1 → 03.2（命題與量詞，Gentzen 規則在 Lean 的化身）。
證明基本功：04.1 → 04.2 → 05.1（重寫、歸納、歸納型別，日常證明八成靠這三招）。
理論加深：05.2 → 06.1 → 06.2（遞迴、Curry–Howard、宇宙與公理，連回歷史卷宗的理論篇）。
函式庫與自動化：07.1 → 07.2 → 08.1 → 08.2（mathlib、決策程序、自寫 tactic、AI 證明，接回歷史卷宗的現代篇）。

配套資源#

歷史卷宗（推理探案風格年表）：../README.md
Lean 官方文件與 mathlib 文件（各節內文引用處另註）