講演資料
講義資料スライドの表紙です。上のスライド画像をクリックすると、同じ画面のまま全編の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]
■ Part 2: Coqは人間に何を伝えたか（Hello Coq! 2/3）
人間が投入したtacticとCoqの反応の意味を事後的に分析し、「対話」の本質を明確化します。tacticとは証明の状態を変化させる命令であり、なぜそのtacticが選ばれたかはCoqの反応（証明の状態）を見なければ理解できません。[p.18〜p.29]
■ Part 3: Coqの返す「証明の状態」の意味（Hello Coq! 3）
Coqが返す「証明の状態」は仮説部（Γ）とサブゴールの対として構成されており、これは演繹ルールにおける `Γ ⊢ 命題` という判断の表現そのものであることを解説します。[p.30〜p.47]
■ Part 4: 論理式はどのような形をしているか（論理式の証明 1）
命題論理の基本記号（∧・∨・→・∀・∃）とそれらのFormation Rule（構成ルール）を整理し、複雑な論理式が単純な論理式から帰納的に構成されるという構造を確認します。[p.48〜p.54]
■ Part 5: 論理式の部分式への分解とサブゴール（論理式の証明 2）
命題の部分式（Sub Formula）と証明のサブゴール（Sub Goal）は名前が似て非なるものであることを明確にしつつ、CoqがSub GoalへのグループとSub Formulaへの分解を同時に行う仕組みを示します。[p.55〜p.59]
■ Part 6: 構成のルールと演繹のルール（論理式の証明 3）
命題の構成・分解ルールと演繹ルールの違いを鮮明にします。演繹ルールとは判断基準を「命題の形をしている」から「証明を持つ」へと置き換えたルール群であり、後ろ向き推論の方向性が証明において本質的に機能します。[p.60〜p.66]
■ Part 7: 「正しい」ことと「証明を持つ」こと（論理式の証明 4）
Coqの演繹ルールは「正しい命題」ではなく「証明を持つ命題」を基礎に置きます。この区別の重要性をゲーデルの不完全性定理と排中律の問題から掘り下げ、直観主義論理的立場のCoqの設計思想を浮かび上がらせます。[p.67〜p.79]
■ Part 8: 命題論理の演繹ルール（論理式の証明 5）
仮説部 Γ と命題 A の関係を `Γ ⊢ A`（Γのもとで A は証明を持つ）で形式化し、Assumption・→I・∧I・∨IL・∨IRという基本演繹ルールを体系的にまとめます。[p.80〜p.88]
■ Part 9: Coqの返す「証明の状態」と演繹ルール（論理式の証明 6）
Coqが返す「証明の状態（仮説部＋サブゴール）」が演繹ルールの各段に現れる `Γ ⊢ 命題` に対応することを確認し、後ろ向き推論による証明の進行原理を整合的に理解できるよう整理します。[p.89〜p.111]
■ Part 10: tacticとサブゴール・仮説部の形（論理式の証明 7/8）
サブゴールの論理記号の形と演繹ルールの選択が一対一に対応することを示し、intros・split・left・right・apply・destruct・assumption・exact H の各tacticが演繹ルールのどの適用に相当するかを、Coqの実際の画面遷移を用いて詳細に解説します。[p.112〜p.147]
ページのナビゲート