はじめてのCoq (サイレント version )

講演資料

講義資料スライドの表紙です。スライド画像、または下の要約文中の青いページ番号リンクをクリックすると、別のタブで無駄なノイズのない、純粋なPDFビューア画面が起動し、指定されたページへ直接ジャンプして快適に閲覧できます。

全体概要

本セミナー「はじめてのCoq」は、対話型証明支援システムCoqの根本的な仕組みと操作方法を、初学者が確かな理解を得られるよう丁寧に解説するものです。セミナーが提起する中心的な問いは、「機械と人間はどのように協働して数学的命題の証明を行うのか」という点にあります。

Coqは単なる自動証明ツールではなく、人間とCoqが「対話」を繰り返しながら証明を段階的に構築していく「対話型証明支援システム」です。人間がtactic（戦略的命令）をCoqに与え、Coqがその時点での「証明の状態」（仮説部＋サブゴール）を人間に返すという往復のやり取りが証明の本質をなしています。この対話の過程を省略して完成した証明スクリプトだけを見ても、なぜその命令が選ばれたかは理解しにくいのです。

セミナーはさらに、Coqの演繹ルールの基礎が「命題が正しい」という判断ではなく「命題が証明を持つ」という判断に置かれていることを詳述します。この区別は、ゲーデルの不完全性定理をめぐる数学基礎論の深い問題と直結しており、排中律が自明でない直観主義論理の立場を取るCoqの設計思想を照らし出します。

論理式の証明においては、命題の構成・分解ルール（Formation Rule）と演繹ルールの関係が丁寧に整理されます。後ろ向きの推論（下段から上段へ）によってサブゴールを部分式へと分解していく手続きが、intros・split・left・right・apply・destruct・exact・assumptionといった具体的なtacticと演繹ルールの対応として明示されます。

証明が完成した後は「証明自動検証」モードで第三者がその証明を再利用・検証できるという点も強調され、数学を「整合的な累積的知の体系」として捉えるCoqの実践的意義が示されます。

講義のロードマップ

■ Part 1: Coqとのはじめての対話（Hello Coq!）

この部の核心:

Coqで最初の定理 `forall A : Prop, A -> A` を証明する実演を通じ、人間がtacticを投入しCoqが「証明の状態」を返すという対話の基本サイクルを体感させます。証明の完了が"No more subgoals"というメッセージで示されることも確認します。[p.3]〜[p.17]

論理展開:
`Theorem Hello_Coq : (forall A : Prop, A -> A).` の入力によりCoqが1つのサブゴールを返す [p.3], [p.6]
`Proof.` → `intros.` → `exact H.` → `Qed.` の順で証明を完了させる [p.7]〜[p.15]
Coqの反応には「証明中の定理名」「サブゴール数」「仮説部」「サブゴール」が含まれる [p.6]
"No more subgoals" が証明完了のシグナルである [p.13], [p.14]

■ Part 2: Coqは人間に何を伝えたか（Hello Coq! 2/3）

この部の核心:

人間が投入したtacticとCoqの反応の意味を事後的に分析し、「対話」の本質を明確化します。tacticとは証明の状態を変化させる命令であり、なぜそのtacticが選ばれたかはCoqの反応（証明の状態）を見なければ理解できません。[p.18]〜[p.29]

論理展開:
tacticは「証明の状態を変化させる戦略命令」であり、結果だけでは選択意図は見えない [p.21], [p.22]
完成した証明は対話なしに丸ごとCoqに与えて検証できる（証明自動検証モード）[p.23]〜[p.26]
数学は「整合的な累積的知の体系」であり、第三者の証明を再利用できることの意義 [p.27]〜[p.29]

■ Part 3: Coqの返す「証明の状態」の意味（Hello Coq! 3）

この部の核心:

Coqが返す「証明の状態」は仮説部（Γ）とサブゴールの対として構成されており、これは演繹ルールにおける `Γ ⊢ 命題` という判断の表現そのものであることを解説します。[p.30]〜[p.47]

論理展開:
Coqの反応における「仮説部（横棒より上）」と「サブゴール（横棒より下）」の構造 [p.35]〜[p.42]
証明状態の情報がどの演繹ルールを選ぶかの指針になる [p.43], [p.44]
destructにより複数サブゴールが生成される例（2 subgoals）[p.45], [p.46]
証明の最終目標はサブゴールをゼロにすること [p.47]

■ Part 4: 論理式はどのような形をしているか（論理式の証明 1）

この部の核心:

命題論理の基本記号（∧・∨・→・∀・∃）とそれらのFormation Rule（構成ルール）を整理し、複雑な論理式が単純な論理式から帰納的に構成されるという構造を確認します。[p.48]〜[p.54]

論理展開:
∧・→・∨・¬・∀・∃ それぞれの Formation Rule [p.50]〜[p.53]
横棒の上が前提、下が結論であり、繰り返し適用で複雑な式が構成される [p.54]
論理式の形がCoqでの証明において重要な役割を果たす [p.54]

■ Part 5: 論理式の部分式への分解とサブゴール（論理式の証明 2）

この部の核心:

命題の部分式（Sub Formula）と証明のサブゴール（Sub Goal）は名前が似て非なるものであることを明確にしつつ、CoqがSub GoalへのグループとSub Formulaへの分解を同時に行う仕組みを示します。[p.55]〜[p.59]

論理展開:
A∧Bの証明 → サブゴールAの証明かつサブゴールBの証明 [p.59]
A∨Bの証明 → サブゴールAの証明またはサブゴールBの証明 [p.59]
部分式への分解は元の命題の構成情報を失う点でサブゴールと異なる [p.57], [p.58]

■ Part 6: 構成のルールと演繹のルール（論理式の証明 3）

この部の核心:

命題の構成・分解ルールと演繹ルールの違いを鮮明にします。演繹ルールとは判断基準を「命題の形をしている」から「証明を持つ」へと置き換えたルール群であり、後ろ向き推論の方向性が証明において本質的に機能します。[p.60]〜[p.66]

論理展開:
構成ルールと演繹ルールの対比：形の整合性 vs. 証明の存在 [p.61]〜[p.64]
前向き推論（上段→下段）と後ろ向き推論（下段→上段）の区別 [p.65], [p.66]

■ Part 7: 「正しい」ことと「証明を持つ」こと（論理式の証明 4）

この部の核心:

Coqの演繹ルールは「正しい命題」ではなく「証明を持つ命題」を基礎に置きます。この区別の重要性をゲーデルの不完全性定理と排中律の問題から掘り下げ、直観主義論理的立場のCoqの設計思想を浮かび上がらせます。[p.67]〜[p.79]

論理展開:
「正しい命題」と「証明を持つ命題」は一致しない（ゲーデルの不完全性定理）[p.75]
「A∨¬A（排中律）」は一般的演繹ルールでは自明だが、Coqでは自明でない [p.77]〜[p.79]
二つのスタイルの演繹ルールの比較（∧・∨それぞれ）[p.73], [p.74]

■ Part 8: 命題論理の演繹ルール（論理式の証明 5）

この部の核心:

仮説部 Γ と命題 A の関係を `Γ ⊢ A`（Γのもとで A は証明を持つ）で形式化し、Assumption・→I・∧I・∨IL・∨IRという基本演繹ルールを体系的にまとめます。[p.80]〜[p.88]

論理展開:
Assumptionルール：Γ∋A ならば Γ⊢A [p.83]
→Iルール：Γ,A⊢B ならば Γ⊢A→B [p.84]
∧Iルール：Γ⊢AかつΓ⊢B ならば Γ⊢A∧B [p.86]
∨IL・∨IRルール：Γ⊢A または Γ⊢B ならば Γ⊢A∨B [p.87]

■ Part 9: Coqの返す「証明の状態」と演繹ルール（論理式の証明 6）

この部の核心:

Coqが返す「証明の状態（仮説部＋サブゴール）」が演繹ルールの各段に現れる `Γ ⊢ 命題` に対応することを確認し、後ろ向き推論による証明の進行原理を整合的に理解できるよう整理します。[p.89]〜[p.111]

論理展開:
「証明の状態」＝Γ（仮説部）＋サブゴール＝ `Γ ⊢ 命題` [p.108], [p.109]
A∧B・A∨B・A→Bそれぞれについて対応する演繹ルールの後ろ向き適用を示す [p.101]〜[p.103]
仮説部の `A:Prop, H:A` など記述の意味は後続で詳述される旨を予告 [p.111]

■ Part 10: tacticとサブゴール・仮説部の形（論理式の証明 7/8）

この部の核心:

サブゴールの論理記号の形と演繹ルールの選択が一対一に対応することを示し、intros・split・left・right・apply・destruct・assumption・exact H の各tacticが演繹ルールのどの適用に相当するかを、Coqの実際の画面遷移を用いて詳細に解説します。[p.112]〜[p.147]