Coq のカリー・ハワード同型周辺についてメモ．間違いあればご指摘ください．
Coq と CoC
Coq は元々，Thierry Coquand 氏により提案された Calculus of Constructions (CoC) という型システムの実装として生まれました．
その後 CoC は，帰納的データ型などが追加された Calculus of Inductive Constructions (CIC) に拡張され，現在の Coq は CIC の実装となっています．
CoC/CIC は，基本的には型システムを定義しただけのものなのですが，実は Coq の証明システムはこの型システムがベース となっています．
これは一体どういうことか，次からの節で，直観的な例を通して見ていくことにします．
プログラム ≈ 証明
一般に，プログラムの型システムは，次の図みたいな推論木を組み立ててプログラムの型付けを行います．
$$
\dfrac{
\dfrac{
\dfrac{
[f : P \to Q]
\quad
[x : P]
}{
f\ x : Q
}
}{
\mathtt{fun}\ x \Rightarrow f\ x : P \to Q
}
}{
\mathtt{fun}\ f\ x \Rightarrow f\ x : (P \to Q) \to P \to Q
}
$$
この推論木は，$\mathtt{fun}\ f\ x \Rightarrow f\ x$ というプログラムの型が $(P \to Q) \to P \to Q$ であることを示しています．
ここで，型変数 $P$ と $Q$ を論理変数とみなし，$\to$ を "ならば ($\supset$)" と読み替えてみます．
すると，この図は $(P \supset Q) \supset P \supset Q$ という論理式の証明木にもなっているということがわかります！
実際，上の図からプログラムの部分を取り除いてみると，自然演繹における論理式 $(P \supset Q) \supset P \supset Q$ の証明が得られます．
$$
\dfrac{
\dfrac{
\dfrac{
[P \supset Q]
\quad
[P]
}{
Q
}
({\supset} \textrm{E})
}{
P \supset Q
}
({\supset} \textrm{I})
}{
(P \supset Q) \supset P \supset Q
}
({\supset} \textrm{I})
$$
型システムが証明システムのベースというのは，この発想に基づいています．
Coq では，論理式の証明を，（型整合性のある）プログラムの構成に帰着させています．
今回の例でいえば，$(P \supset Q) \supset P \supset Q$ という論理式の証明を，$(P \to Q) \to P \to Q$ という型をもつプログラムの構成に帰着させているわけです．
プログラムを証明とみなすこの考え方は，"カリー・ハワード同型" としてよく知られています．
これについて，次の節で説明します．
カリー・ハワード同型
カリー・ハワード同型 (Curry–Howard isomorphism) とは，論理の世界と計算の世界との間に存在する，興味深い対応関係のことです．
この対応関係によると，命題と型が対応していて，証明とプログラムが対応しています．
| 論理の世界 | 計算の世界 |
|---|---|
| 命題 | 型 |
| 証明 | プログラム |
すでに説明してきたように，Coq の証明はこの対応関係に基づいて行われます．
Coq では，型で命題を表し，その型を持つプログラムを証明に代えます．
Coq において，含意を表す -> と関数型を表す -> の記号が一致しているのは，偶然ではありません．
Coq の論理式 P -> Q は，"P ならば Q" を表す論理式であると同時に，P から Q への関数を表す関数型でもあります．
Coq の型システムは，依存型 (dependent type) とよばれる表現力の高い型を扱える体系となっています．
そのため，量化子や述語を含む論理式も型で表せるようになっています．
次の表のような論理式と型の対応関係により，様々な論理式の証明を型システムベースで行えるようになっています．
| 論理の世界 | Coq の世界 |
|---|---|
| 真 ($\top$) |
True 型 |
| 偽 ($\bot$) |
False 型 |
| 連言 ($\land$) | 直積型 (and) |
| 選言 ($\lor$) | 直和型 (or) |
| 含意 ($\supset$) | 関数型 (->) |
| 全称量化 ($\forall$) | 依存積型 (forall _ : _, _) |
| 存在量化 ($\exists$) | 依存和型 (ex) |
証明と証明項
Coq で定理を証明するということは，その定理に対応する型をもつプログラムを構成するということです．
ここで構成されるプログラムのことを，証明項 (proof term) ともいいます．
証明が完了した定理に Print コマンドを実行すると，証明として構成されたプログラム（証明項）を見ることができます．
次の定理を例にとって，確かめてみます．
Variables P Q : Prop.
Theorem modus_ponens: (P -> Q) -> P -> Q.
Proof.
auto.
Qed.
Print コマンドで，構成されたプログラムを見てみます．
Print modus_ponens.
modus_ponens = fun H : P -> Q => H
: (P -> Q) -> P -> Q
たしかに，証明した命題と同じ型を持つプログラムが構成されていることがわかりました．
Coq の証明は，証明項を直接与えて行うこともできます．
次の例は，実際に証明項を直接与えて定理を証明したものです．
Variables P Q : Prop.
Theorem modus_ponens: (P -> Q) -> P -> Q.
Proof fun f x => f x.
次のように，exact タクティックで証明項を与える方法もあります．
Variables P Q : Prop.
Theorem modus_ponens: (P -> Q) -> P -> Q.
Proof.
exact (fun f x => f x).
Qed.
Coq で実行してみると，確かにこれで証明が完了することがわかります．