講演資料
講義資料スライドの表紙です。上のスライド画像をクリックすると、同じ画面のまま全編のPDF資料を快適に閲覧・印刷することができます。
セミナーの概要
本セミナー「はじめてのCoq」は、対話型証明支援システムCoqとの「はじめての対話」を起点として、Coqが依拠する証明の哲学的・数理的基盤を段階的に解き明かす講義です [p.1, p.3]。
中心的な問いは「機械と人間はどのようにして協働し、数学的命題を厳密に証明するのか」という一点に集約されます。Coqは単なる自動証明ツールではなく、人間が戦略（tactic）を与え、Coqがその時点での「証明の状態」を返すという対話を繰り返すことで証明が進む、真の意味での「協働システム」です [p.42, p.97]。
講義が特に力を注ぐのは、Coqの演繹ルールの基礎に置かれた独特の判断基準です。一般的な論理学が「正しい命題である」を判断の基準とするのに対し、Coqは「証明を持つ」を判断の基準とします [p.234, p.236]。この違いは一見些細に見えますが、排中律（A ∨ ¬A）の扱いに象徴されるように、直観主義論理と古典論理の根本的な分岐を生み出します [p.261, p.265]。ゲーデルの不完全性定理が示した「正しいが証明を持たない命題の存在」は、この分岐の数学的根拠となっています [p.246, p.247]。
証明の操作的側面においては、tacticと演繹ルールの対応関係が丁寧に解説されます。`intros`、`split`、`left`/`right`、`apply`、`destruct`、`assumption`/`exact`といった各tacticが、それぞれΓ⊢A→B、Γ⊢A∧B、Γ⊢A∨Bといったサブゴールあるいは仮説部の論理的形状に対応する演繹ルールの適用であることが、証明状態の変化とともに視覚的に示されます [p.452, p.527]。
さらに本講義は、いったん完成した証明はtacticごとの対話なしにCoqへ一括提出して検証できることを強調します [p.57, p.58]。これは「数学は整合的な累積的知の体系である」という原理と結びつき、第三者の証明を信頼して利用できるCoqの実践的価値、さらにはDeep SpecificationやUniMathといったムーブメントの動力源となっています [p.72, p.77]。否定演算子`~`が`A→False`の省略形として定義され、Falseの定義が空であることから「偽からはどんな命題も導かれる」という*ex falso quodlibet*が成立するCoqの内部構造も、理論の整合性を支える重要な要素として紹介されます [p.559, p.586]。
講義のロードマップ
ここでは、セミナーの講演資料がどのようなパートから構成されているかを示します。また、それぞれのパートのポイントを紹介します。
■ Part 1: Coqとのはじめての対話（Hello Coq! 1〜3）
最初の証明`Theorem Hello_Coq : (forall A : Prop, A -> A)`を題材に、`Theorem`宣言、`Proof.`、tactic投入、`Qed.`という一連の流れを実際に体験させます [p.5, p.30]。証明の完成後に対話履歴なしで証明を再実行できる「対話型証明モード」と「証明自動検証モード」という二つの利用形態を整理し、Coqの実践的価値を示します [p.60, p.63]。
■ Part 2: 論理式の証明（1〜2）論理式の形と分解
命題論理の基本的な**Formation Rule（構成ルール）**を導入し、∧・∨・→・¬・∀などの論理記号によって複雑な論理式が単純な論理式から構成されることを確認します [p.122, p.124]。次いで、構成の逆である**分解ルール**を導出し、証明のサブゴールへの分割と命題の部分式への分解がどのように関連するかを論じます [p.140, p.148]。
■ Part 3: 論理式の証明（3）構成ルールと演繹ルール
命題の**構成・分解ルール**（「命題の形をしている」を基準）と**演繹ルール**（「証明を持つ」を基準）の概念的区別を明確にします [p.193]。A∧Bの証明→部分式Aの証明かつBの証明、A∨Bの証明→部分式Aまたは部分式Bの証明、という形で演繹ルールの双方向性を示します [p.195, p.196, p.200, p.201]。
■ Part 4: 論理式の証明（4）「正しい」ことと「証明を持つ」こと
「正しい命題である」を基準とする一般的な演繹ルールと、「証明を持つ」を基準とするCoqの演繹ルールを並置して比較し、両者の実質的な差異を排中律を具体例として浮き彫りにします [p.233, p.234, p.240, p.242]。
■ Part 5: 論理式の証明（5）命題論理の演繹ルール
「仮説部Γのもとで命題Aが証明を持つ」という判断をΓ⊢Aと形式化し、Assumption・→I・→E（modus ponens）・∧I・∨IL・∨IRという命題論理の基本演繹ルールを体系的に整備します [p.276, p.285, p.290, p.295, p.300, p.305]。
■ Part 6: 論理式の証明（6）Coqの返す「証明の状態」と演繹ルール
Coqが返す「証明の状態」（仮説部＋サブゴール）がΓ⊢命題という演繹ルールの各段と正確に対応していることを解明します [p.434, p.435]。後ろ向き推論（下段→上段）こそがCoqのtactic駆動型証明の本質であることを示します [p.386, p.394]。
■ Part 7: 論理式の証明（7）tactic（1）サブゴールの形と演繹ルールの選択
サブゴールの論理的形状に基づいてtacticと演繹ルールの対応を体系化します。`intros`（→I）、`split`（∧I）、`left`（∨IL）、`right`（∨IR）がそれぞれどのサブゴール形状に反応し、仮説部とサブゴールをどのように変化させるかを視覚的に整理します [p.452]。
■ Part 8: 論理式の証明（8）tactic（2）仮説部の形と演繹ルールの選択
今度は仮説部の論理的形状に基づく演繹ルールとtacticを整理します。`apply`（A→Bを仮説に持つとき）、`destruct`（A∨BまたはA∧Bを仮説に持つとき）、`assumption`/`exact`（仮説部にサブゴールと一致する命題があるとき）の三系統を解説します [p.527]。
■ Part 9: 論理式の証明（9）「否定」について
Coqでの否定演算子`~`は基本的な論理演算子ではなく、`~A`は`A→False`の省略形として定義されていることを示します [p.558, p.559]。型Falseが定義を持たない（証明を持たない）ことから、`ex falso quodlibet`（偽からはどんな命題も導かれる）という重要な定理が成立するCoqの内部論理を解説します [p.580, p.586]。
ページのナビゲート