02.1 蘊涵：intro 與 apply#

本章導讀#

第 2 章進入命題邏輯，本節先攻最常用的連接詞：蘊涵。

蘊涵就是日常說的如果則，Lean 記為 \(p \to q\) ，也是函數型別的化身。

你會學會一對搭檔： \(intro\) 負責引入假設， \(apply\) 負責套用已知蘊涵。

最後用恆等函數與函數複合兩個例子，把邏輯與程式一次打通。

要證明如果下雨則地濕，最自然的方法是先假設下雨了，再推出地濕。

這就是 \(intro\) ：把箭頭左邊搬進上下文，目標只剩箭頭右邊。

反過來，若已知如果下雨則地濕，又看到真的下雨，就能斷言地濕。

這就是 \(apply\) ：用一條已知蘊涵去對準目前目標，倒推出還缺的前提。

一個由前往後拆，一個由後往前找，兩者搭配就是全部的前向與後向推理。

Gentzen 自然演繹給蘊涵一條引入規則與一條消去規則。

規則	形式	Lean 戰術	方向
蘊涵引入	由 \(\Gamma, p \vdash q\) 得 \(\Gamma \vdash p \to q\)	\(intro\)	後向：目標是蘊涵就引入
蘊涵消去	由 \(\Gamma \vdash p \to q\) 與 \(\Gamma \vdash p\) 得 \(\Gamma \vdash q\)	\(apply\) 或 \(exact\)	前向：已有蘊涵就套用

函數複合是消去規則用兩次的結果，設 \(f : p \to q\) 且 \(g : q \to r\) 。

\[ \frac{f : p \to q \quad g : q \to r}{g \circ f : p \to r} \]

在 Lean 裡這正是 \(Function.comp\) 的型別，也是 \(trans\) 思想的命題版本。

後向推理的目標變換可寫成：

\[ Goals[\vdash q] \xrightarrow{apply \; h} Goals[\vdash p] \]

其中 \(h : p \to q\) ，亦即把結論換成更弱的前提，逐步倒推回去。

恆等函數是最短的蘊涵證明：對任意命題 \(p\) ，有 \(p \to p\) 。

theorem my_id (p : Prop) (h : p) : p := by
  exact h

等價的 \(intro\) 版本更能展示引入動作：

theorem my_id_intro (p : Prop) : p → p := by
  intro h
  exact h

函數複合則展示 \(apply\) 連用兩次的威力：

theorem my_comp (p q r : Prop) (f : p → q) (g : q → r) : p → r := by
  intro hp
  apply g
  apply f
  exact hp

證明狀態的變化如下表，請由上往下讀，體會目標如何倒推。

步驟	戰術	目標 \(Goals\)	上下文 \(\Gamma\)
初始	無	\(\vdash p \to r\)	\(f : p \to q, g : q \to r\)
1	\(intro\)	\(\vdash r\)	增加 \(hp : p\)
2	\(apply\) 前者	\(\vdash q\)	同上，用 \(g\) 對準 \(r\)
3	\(apply\) 後者	\(\vdash p\)	同上，用 \(f\) 對準 \(q\)
4	\(exact\)	\(No goals\)	\(hp\) 恰好結案

記住口訣：目標是箭頭就 \(intro\) ，手上有箭頭就 \(apply\) 。

蘊涵的引入與消去規則，正是 Gentzen 的招牌發明。

本節的恆等與複合例子，同時是邏輯定理與函數程式，Howard 的對應在此完全應驗。

證明 \((p \to q) \to (q \to r) \to (p \to r)\) ，只能用 \(intro\) 、 \(apply\) 、 \(exact\) ，並列出每步目標。
設有 \(h_{1} : p \to q\) 與 \(h_{2} : p\) ，試用 \(exact\) 與 \(apply\) 各寫一種證法得到 \(q\) ，比較差異。
挑戰題：證明 \((p \to q \to r) \to (p \to q) \to p \to r\) ，提示是連續三次 \(intro\) 再兩次 \(apply\) 。