6.1 命題即型別證明即程式#

本章導讀#

本章是全書的理論高峰 ， 把程式與證明正式連成一體 。 核心口號只有一句 ， 命題即型別 ， 證明即程式 。 學完本章 ， 你能讀懂項式證明 ， 並在項式與 tactic 兩種風格間切換 。 我們以合取交換律為主線例子 ， 給出兩種證明的逐行對照 。 下一節 6.2 會處理這個對應的邊界 ， 即宇宙與公理的取捨 。 建議先複習 02.2 節的合取規則 ， 對照閱讀效果最佳 。

淺顯說明#

把命題看成型別 ， 把證明看成住在裡面的程式 ， 化簡證明就像執行程式 。 例如命題 \(p\land q\) 對應積型別 ， 證據就是一對有序對 。 命題 \(p\to q\) 對應函數型別 ， 證據就是把證據變成證據的函數 。 命題 \(p\lor q\) 對應和型別 ， 證據要註明來自左邊或右邊 。 證明檢查等於型別檢查 ， 寫錯證明就像傳錯參數型別 。 tactic 只是幫你慢慢拼出這支程式的助手 ， 最終產物仍是一項程式 。 這就是 Gentzen 自然演繹在 Lean 中的復活 ， 引入規則即構造 ， 消去規則即使用 。 項式證明一次寫完答案 ， tactic 證明一步步請電腦幫忙填空 。 兩者沒有高下之分 ， 只是同一個程式的不同寫法 。

正規理論#

Curry-Howard 對應可用三對照表一覽 ， 邏輯概念逐項翻譯為型別概念 。

三個核心邏輯連結詞的翻譯如下 ， 每一條都是獨立公式 。

其中符號 \(Proof\) 表示某命題的證據集合 ， 符號 \(\simeq\) 表示一一對應 。 Gentzen 的自然演繹規則恰好落在構造與消去的位置 ， 見下表 。

引入規則負責製造證據 ， 消去規則負責使用證據 ， 與構造子及 \(match\) 完全平行 。 tactic 證明的每一步 ， 其實都是在反向拼裝右欄對應的左欄項 。 理解這一點之後 ， tactic 不再是魔法咒語 ， 而是項式程式的互動組裝器 。

簡易範例#

下面用合取交換律示範同一個定理的兩種證明 ， 請逐行對照閱讀 。 項式版本只有一行核心 ， tactic 版本則把構造過程攤開 。

def and_comm_fun {p q : Prop} : p ∧ q → q ∧ p :=
  fun h => And.intro h.2 h.1

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

項式版的 fun h => 對應 tactic 版的接住假設 \(h\) 的動作 。 項式版的 And.intro 對應 tactic 版的 constructor 步驟 。 項式版的 \(h.2\) 與 \(h.1\) 對應 tactic 版拆開後的 \(hq\) 與 \(hp\) 次序 。 tactic 版的兩個 exact 只是把交換後的證據逐一放回 goals 。 當你對 tactic 證明呼叫顯示項命令時 ， 會看到它生成的正是類似項式版的程式 。 初學建議先用 tactic 摸索 ， 熟練後再試著直接寫出項式一行解 。

歷史典故#

這個對應的發現者是 Howard 公式即型別 。 該卷宗記載他如何把 Gentzen 的自然演繹逐條翻譯成型別項 。 而型別一側的源頭 ， 則是 Church 簡單型別理論 。 沒有簡單型別演算的函數觀念 ， 公式即型別便無從附著 。 這個對應的集大成者是 CoC 與 CIC 。 構造演算把命題宇宙與資料宇宙統一在同一個依賴型別框架之下 。 其後的 Coq 誕生 讓程式設計師與數學家共用同一種語言 。 讀本章時 ， 不妨把 Gentzen 想成提供文法的人 ， Howard 想成發現雙語詞典的人 。

習題#

1. 用項式風格證明蘊涵的傳遞性 ， 即由 \(f\) 與 \(g\) 構造合成函數 ， 再用 tactic 風格證明同一命題並對照兩者的對應行 。
2. 把合取消去的兩個投影 \(h.1\) 與 \(h.2\) 改寫成 \(match\) 表達式 ， 說明投影只是模式匹配的語法糖 。
3. 解釋為何 tactic 證明最終仍產生一項程式 ， 並說明這句話與 Gentzen 消去規則的關係 。