02.2 合取與析取：cases 與 constructor#
本章導讀#
本節處理兩個最生活化的連接詞：合取且與析取或。
合取記為 \(p \land q\) ，析取記為 \(p \lor q\) ，兩者的證明手法正好互補。
你會學會 \(constructor\) 打包證據、 \(cases\) 拆解證據，以及 \(left\) 與 \(right\) 二選一。
最後登場的是匿名構造子 \(\langle , \rangle\) ，一行就能寫完小證明。
淺顯說明#
要證明今天又熱且又渴，你必須同時端出熱的證據與渴的證據。
要證明今天熱或今天冷，你只要端出一邊的證據，另一邊可以不管。
反過來使用時也對稱：拿到且的證據可以拆成兩份，拿到或的證據則要分兩案討論。
Lean 把打包叫引入，把拆包叫消去，戰術名稱正是 \(constructor\) 與 \(cases\) 。
正規理論#
合取與析取各有引入與消去規則，整理成一張對照表最清楚。
| 連接詞 | 引入規則 | 消去規則 | 對應戰術 |
|---|---|---|---|
| 合取 \(p \land q\) | 由 \(p\) 與 \(q\) 得 \(p \land q\) | 由 \(p \land q\) 得 \(p\) ，亦得 \(q\) | 引入用 \(constructor\) ，消去用 \(cases\) |
| 析取 \(p \lor q\) | 由 \(p\) 得 \(p \lor q\) ，由 \(q\) 亦得 | 由 \(p \lor q\) 、 \(p \to r\) 、 \(q \to r\) 得 \(r\) | 引入用 \(left\) ／ \(right\) ，消去用 \(cases\) |
用推理樹表示，合取引入為：
\[ \frac{\Gamma \vdash p \quad \Gamma \vdash q}{\Gamma \vdash p \land q} \]
析取消去則是分案討論，需要兩條分支都通往同一結論：
\[ \frac{\Gamma \vdash p \lor q \quad \Gamma, p \vdash r \quad \Gamma, q \vdash r}{\Gamma \vdash r} \]
匿名構造子 \(\langle , \rangle\) 只是構造子的縮寫， \(And.intro\) 與 \(Or.inl\) 的便利用法。
| 寫法 | 展開 | 用途 |
|---|---|---|
| \(\langle hp, hq \rangle\) | \(And.intro \; hp \; hq\) | 證明 \(p \land q\) |
| \(Or.inl \; hp\) | \(left \; hp\) 的項版本 | 證明 \(p \lor q\) 用左邊 |
| \(Or.inr \; hq\) | \(right \; hq\) 的項版本 | 證明 \(p \lor q\) 用右邊 |
簡易範例#
合取例子：把一包證據拆開再反向包裝回去的變體。
theorem and_intro_demo (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
constructor
· exact hp
· exact hq
匿名構造子一行版：
theorem and_anon (p q : Prop) (hp : p) (hq : q) : p ∧ q :=
⟨hp, hq⟩
析取例子：左邊進、兩案出，展示 \(left\) 與 \(cases\) 的搭配。
theorem or_demo (p q : Prop) (hp : p) : p ∨ q := by
left
exact hp
theorem or_cases_demo (p q r : Prop) (h : p ∨ q)
(f : p → r) (g : q → r) : r := by
cases h with
| inl hp => exact f hp
| inr hq => exact g hq
證明狀態表以 \(or\_cases\_demo\) 為例，重點看目標如何一分為二。
| 步驟 | 戰術 | 目標 \(Goals\) | 上下文 \(\Gamma\) |
|---|---|---|---|
| 初始 | 無 | \(\vdash r\) | \(h : p \lor q\) 等三項 |
| 1 | \(cases\) | \(\vdash r\) ， \(\vdash r\) | 分支一得 \(hp : p\) ，分支二得 \(hq : q\) |
| 2 | \(exact\) 兩次 | \(No goals\) | 分別用 \(f\) 與 \(g\) 結案 |
口訣是：要證且就打包，拿到且就拆包，要證或就選邊，拿到或就分案。
歷史典故#
且與或的規則看似平凡，卻是兩千年邏輯演進的結晶。
- Gentzen 自然演繹：首次把且或的引入消去寫成對稱規則組。
- Boole 布林代數：把且或化為代數運算，今日電路與程式的源頭。
- Frege 概念文字：最早用形式語言嚴格定義連接詞的語意。
建議對照 Gentzen 的規則表來讀 \(cases\) ，你會發現 tactic 只是把紙上規則變成按鍵。
習題#
- 證明 \(p \land q \to q \land p\) ，分別用 \(constructor\) 版與 \(\langle , \rangle\) 版各寫一次。
- 證明 \(p \to p \lor q\) 與 \(q \to p \lor q\) ，並說明何時用 \(left\) 、何時用 \(right\) 。
- 證明 \((p \lor q) \to (p \to r) \to (q \to r) \to r\) ，要求用 \(intro\) 開頭、 \(cases\) 分案。