1989 — Coq 證明助手問世#

案件摘要#

1989 年，法國國家資訊與自動化研究所（INRIA）的 Coquand 與 Huet 團隊釋出 Coq——一個以 Calculus of Constructions 為基礎的互動式定理證明器。Curry–Howard 對應不再只是理論，而成為可以敲擊鍵盤操作的工具。三十年後，四色定理、CompCert、Feit-Thompson 定理全在 Coq 中被機械驗證。

前因 -- 為什麼會有這個案子#

Automath 的先聲：1967 年荷蘭 de Bruijn 的 Automath 系統首次嘗試「用電腦驗證數學證明」，但表達力受限。
Calculus of Constructions（1985）：Thierry Coquand 與 Gérard Huet 提出 CC——Barendregt Lambda Cube 的頂點，同時包含多型、型別運算子、依賴型別：

\[ \text{項依賴於型別（多型）} + \text{型別依賴於型別（運算子）} + \text{型別依賴於項（依賴）} \]

證明長度懸案：四色定理（Appel-Haken 1976）的證明依賴電腦枚舉上千個圖形，人工無法覆核——數學界需要「機器可檢查的證明」。
LCF 的戰術傳統：1979 年 Milner 的 LCF 系統發明「戰術（tactic）」——以函數組合的方式操作證明目標，並以 type discipline 保證「不可能產生錯誤的證明」。

線索與推理 -- 數學式、程式、理論#

Curry–Howard 對應的實作#

Coq 的核心是 Curry–Howard 對應的完整實作：

邏輯	Coq
命題	型別（`Prop`）
證明	項（程式）
蘊含 \(P \to Q\)	函數型 `P -> Q`
全稱量詞 \(\forall x:A.\, P(x)\)	依賴積型 `forall x : A, P x`
存在量詞 \(\exists x:A.\, P(x)\)	依賴和型（`ex`）
證明檢查	型別檢查（kernel）
戰術（tactic）	建構證明項的函數

關鍵設計：kernel 隔離。Coq 分為兩層：核心（kernel）只做事項型別檢查，外層（tactics）可以任意做自動化推理——但最終產出的證明項必須通過 kernel 檢查。這延續了 LCF 的安全傳統，保證「Coq 說證明成立，證明就真的成立」。

歸納構造演算 CIC#

Coq 實際的理論是 CIC（Calculus of Inductive Constructions）——CC 加上歸納型別：

\[ \frac{\text{歸納定義 } \mathsf{nat} : \mathsf{Set} \text{ 帶建構子 } 0, S}{\text{可定義遞迴函數與歸納證明}} \]

自然數的歸納原理成為一階規則：

\[ \frac{P(0) \quad \forall n.\, P(n) \to P(S\,n)}{\forall n.\, P(n)} \]

一個 Coq 範例#

(* 定義：偶數的歸納謂詞 *)
Inductive even : nat -> Prop :=
  | even_O  : even O
  | even_SS : forall n, even n -> even (S (S n)).

(* 定理：所有偶數的兩倍仍是偶數（依賴型別的全稱命題） *)
Theorem double_even : forall n, even n -> even (n + n).
Proof.
  intros n H.           (* 引入 n 與證明 H : even n *)
  induction H as [| m H' IH].   (* 對 H 做歸納 *)
  - (* 情形 1：n = 0 *) simpl. apply even_O.
  - (* 情形 2：n = m+2，歸納假設 IH : even (m+m) *)
    simpl. apply even_SS. apply IH.
Qed.

(* Check 指令顯示證明項——證明就是一個 λ 項！ *)
Check double_even.
(* double_even
     : forall n : nat, even n -> even (n + n) *)

simpl、apply、induction 是戰術；Qed 之後 Coq 將整個證明編譯成一個 λ 項交給 kernel 驗證。

證明助手譜系#

LCF (Milner 1979) ──戰術、安全 kernel──┐
                                      ├─→ Isabelle (1986)
Automath (de Bruijn 1967) ──依賴型別──┤
                                      ├─→ Coq (INRIA 1989)
MLTT (Martin-Löf 1980) ──直覺型別論───┤      │
                                      │      ├─→ Agda (2007, 直接 MLTT)
NuPRL (1985, MLTT 實作) ──────────────┘      └─→ Lean (2015, 微kernel)

譜系的三條血脈：LCF 的戰術傳統、Automath 的依賴型別、MLTT 的直覺型別論——Coq 是三者的合流點。

結案 -- 後果與影響#

四色定理（2005）：Gonthier 與 Werner 用 Coq 完整驗證 Appel-Haken 的證明，連電腦枚舉部分也被形式化——數學史上第一個「完全機械驗證的重大定理」。
Feit-Thompson 定理（2012）：有限群論的奇數階定理在 Coq 中被驗證，歷時六年。
CompCert（2008）：Leroy 用 Coq 開發經過形式驗證的 C 編譯器——證明編譯器不會改變程式語義。這是「程式即證明」最震撼的工程應用，已用於航空、汽車等安全關鍵系統。
產業應用：JetBrains、AWS、證券交易系統（Dan Grossman 等）開始使用 Coq/Lean 驗證核心邏輯；Rust 的借用檢查器理論（separation logic）也源於這個傳統。
催生 Lean：Leonardo de Moura 於 2015 年以更快的 kernel 與數學傾向開發 Lean，成為 Coq 之後最活躍的證明助手。

關鍵人物與文獻#

Thierry Coquand：瑞典 Chalmers 大學，Calculus of Constructions 的提出者。
Gérard Huet：INRIA，LCF 系統的共同開發者、Coq 的創始人。
Xavier Leroy：INRIA，OCaml 與 CompCert 的主要開發者。
Georges Gonthier：四色定理與 Feit-Thompson 定理的 Coq 形式化者。
文獻：
Coquand, T., Huet, G. (1988). The Calculus of Constructions, Information and Computation.
Coquand, T., Paulin, C. (1990). Inductively defined types (CIC 的起源).
Bertot, Y., Castéran, P. (2004). Interactive Theorem Proving and Program Development: Coq'Art.
Gonthier, G. (2008). Formal Proof—The Four-Color Theorem, Notices of the AMS.