跳轉到

1989 年 Coq 誕生：構造性證明的工程結晶探案#

報案人：Coquand、Huet、Paulin-Mohring、Barras、Werner，INRIA 團隊。 版本：Coq 4.10／5.x 在 1989 年前後問世。涉案物：Gallina＋Ltac。

案發現場#

1988 年 CoC 理論雖美，卻只是紙上演算，沒有互動介面、策略語言與函式庫， 數學家不可能手寫幾千行的 \(\lambda\) 項來證明四色定理。

另一邊，HOL 與 Boyer-Moore 已有 tactic 與函式庫， Automath 的夢（機器檢查整本數學書）仍無人實現。 INRIA 團隊在巴黎郊外立下軍令狀：把 CoC／CIC 變成工程師與數學家 每天能用的工具，取名 Coq（致敬 Coquand，也致敬法國公雞與 Curry 的變體）。

現場需求有三：

  1. 高階規格語言，能寫數學定義與程式。
  2. 互動證明語言，能讓人指揮、機器填細節。
  3. 構造性根基，能從證明萃取出可跑的程式。

偵查過程#

線索一：Gallina——既是數學書又是程式#

Coq 的規格語言叫 Gallina。它允許在同一檔案中寫定義、命題與證明：

Inductive nat : Type := O : nat | S : nat -> nat.
Fixpoint add (n m : nat) : nat :=
  match n with O => m | S p => S (add p m) end.
Lemma add_O_r : forall n:nat, add n O = n.

這裡 \(add\) 既是數學函數也是可執行的程式， \(add \, O \, m\) 按 \(match\) 歸約為 \(m\) ，與紙上計算一致。 命題 \(forall \, n:nat, add \, n \, O = n\) 本身也是一個型別， 它的證明將是一個 \(\lambda\) 項，型別檢查通過即證明有效。

Gallina 構造 角色
\(Inductive\) 宣告歸納型別與命題
\(Fixpoint\) ／ \(Definition\) 寫可計算函數
\(Lemma\) ／ \(Theorem\) 宣告待證的型別（命題）

線索二：Ltac＋Curry-Howard 工程化——凡證明皆程式#

Coq 把 Curry-Howard 對應變成生產線：

\[ \frac{證明 \, p : P \quad 證明 \, q : Q}{(p, q) : P \land Q} \quad,\quad \frac{f : P \to Q \quad p : P}{f(p) : Q} \]

使用者不必手寫 \(\lambda\) 項，而是用 Ltac 策略語言指揮：

Proof.
  intros n. induction n as [| p IH].
  - simpl. reflexivity.
  - simpl. rewrite IH. reflexivity.
Qed.

\(intros\) 、 \(induction\) 、 \(simpl\) 、 \(rewrite\) 、 \(reflexivity\) 皆為 tactic， 組合子 \(;\) 、 \(try\) 、 \(repeat\) 則是 tactical。 \(Qed\) 一敲， 系統構造出完整的證明項並由小核心檢查，通過才封存。

tactic 動作
\(intros\) 引進 \(\Pi\) 與 \(\to\) 的前提
\(induction\) 對歸納型別做結構歸納
\(simpl\) ／ \(rewrite\) 按等式計算與重寫
\(auto\) ／ \(omega\) 自動化收尾

線索三：構造性邏輯——不靠排中律的硬骨頭#

Coq 預設是構造性的： \(P \lor \neg P\) 不是公理， 存在性 \(\exists x. P(x)\) 的證明必須交出見證 \(x\) 。 這讓證明自帶算法， \(sort\) 正確性證明可萃取為 \(sort\) 程式：

Extraction sort_correct.
(* 得到 OCaml 的 sort 實作 *)

代價是古典數學家要額外引入排中律與選擇公理， 但 Coq 允許按需引進，並標記哪些證明用了古典公理。 嚴格與彈性兼得，正是工程化的精髓。

結案報告#

Coq 4.10／5.x 於 1989 年前後在 INRIA 誕生，1990 年代持續迭代。 它把 CoC／CIC 從論文變成工具，破了「構造性證明能否工程化」的案件。

遺產有三：

  1. 大驗證時代的武器：2005 年四色定理、2012 年 Odd Order 定理、 CompCert 編譯器，皆用 Coq 完成，詳見第四、五幕。
  2. Ltac 文化：策略語言成為證明器的標配，後來的 Ssreflect、Lean tactic 皆受啟發。
  3. 萃取範式：證明即程式不再是口號，而是 Extraction 一鍵可得的交付物。

Coq 案是第三幕的高潮：理論心臟（CoC）終於長出血肉。

證據與工具#

  • Curry-Howard 三對應：合取 \(P \land Q\) 對積型別，蘊含 \(P \to Q\) 對函數型，全稱 \(\forall x. P(x)\) 對 \(\Pi x:A. P(x)\) 。
  • 標準起手式： \(intros\) 引進假設， \(induction\) 分案， \(simpl\) 計算， \(rewrite\) 重寫， \(reflexivity\) 收尾。
  • 最小完整證明：
Lemma add_O_r : forall n:nat, add n O = n.
Proof.
  intros n. induction n as [| p IH].
  - simpl. reflexivity.
  - simpl. rewrite IH. reflexivity.
Qed.
  • 實驗：在 Coq 重跑上例，用 \(Show \, Proof.\) 看證明項，再用 \(Extraction\) 輸出 OCaml 程式。
  • 文獻：Huet 等 Coq 手冊，Bertot 與 Castéran《Interactive Theorem Proving and Program Development》。