講演資料
講義資料スライドの表紙です。スライド画像、または下の要約文中の青いページ番号リンクをクリックすると、別のタブで無駄なノイズのない、純粋な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]。
- 論理展開:
- 人間がCoqに与える命令をtactic（戦略）と呼び、tacticの選択意図はCoqの反応（証明の状態）を見なければ理解できない [p.46], [p.49]。
- Coqの反応には「定理名」「残存サブゴール数」「仮説部」「サブゴール」が含まれ、「No more subgoals」が証明完了を意味する [p.87], [p.89], [p.22]。
- 完成した証明は第三者が利用可能であり、数学の「累積的知の体系」としての原理に直結する [p.58], [p.72]。
■ Part 2: 論理式の証明（1〜2）—論理式の形と分解
- この部の核心:
命題論理の基本的なFormation Rule（構成ルール）を導入し、∧・∨・→・¬・∀などの論理記号によって複雑な論理式が単純な論理式から構成されることを確認します [p.122], [p.124]。次いで、構成の逆である分解ルールを導出し、証明のサブゴールへの分割と命題の部分式への分解がどのように関連するかを論じます [p.140], [p.148]。
- 論理展開:
- 構成ルールを「上から下」に読めば構成、「下から上」に読めば分解ルールが得られる [p.148], [p.149]。
- A∧Bの証明には部分式AとBの証明が両方必要、A∨Bの証明には一方で十分という非対称性がサブゴール数の違いに現れる [p.156], [p.158]。
- サブゴール（Sub Goal）と部分式（Sub Formula）は名前は似ているが異なる概念であり、Coqはこの二つを同時に処理する [p.166], [p.170]。
■ Part 3: 論理式の証明（3）—構成ルールと演繹ルール
- この部の核心:
命題の構成・分解ルール（「命題の形をしている」を基準）と演繹ルール（「証明を持つ」を基準）の概念的区別を明確にします [p.193]。A∧Bの証明→部分式Aの証明かつBの証明、A∨Bの証明→部分式Aまたは部分式Bの証明、という形で演繹ルールの双方向性を示します [p.195], [p.196], [p.200], [p.201]。
- 論理展開:
- 「命題である」の述語を「証明である」に単純置換すると意味不明になる問題を指摘し、「証明を持つ」という表現の必要性を導く [p.214], [p.218]。
- 構成ルールと演繹ルールは異なるレベルのルールであり、演繹ルールは命題の論理的内容に踏み込む [p.192], [p.193]。
■ Part 4: 論理式の証明（4）—「正しい」ことと「証明を持つ」こと
- この部の核心:
「正しい命題である」を基準とする一般的な演繹ルールと、「証明を持つ」を基準とするCoqの演繹ルールを並置して比較し、両者の実質的な差異を排中律を具体例として浮き彫りにします [p.233], [p.234], [p.240], [p.242]。
- 論理展開:
- 一般的な演繹ルールではA∨¬Aが正しければAまたは¬Aの正しさが自動的に帰結する [p.261]。
- Coqの演繹ルールではA∨¬Aの証明にはAまたは¬Aの証明を明示的に構成する必要があり、排中律は自明ではない [p.263], [p.265]。
- ゲーデルの不完全性定理が「正しいが証明を持たない命題の存在」を保証し、両者の基準が一致しないことの数学的根拠となる [p.246], [p.247]。
■ 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]。
- 論理展開:
- Assumption：Γ∋AならばΓ⊢A。仮説部に含まれる命題はそのまま証明を持つ [p.285], [p.287]。
- →I：Γ,A⊢BならばΓ⊢A→B。Aを仮説部に追加してBを証明できれば→が導入できる [p.290], [p.293]。
- →E（modus ponens）：Γ⊢A→BかつΓ⊢AならばΓ⊢B [p.295], [p.298]。
- ∧I・∨IL/∨IR：それぞれ両方の証明、または一方の証明から複合命題の証明が得られる [p.300], [p.305]。
■ Part 6: 論理式の証明（6）—Coqの返す「証明の状態」と演繹ルール
- この部の核心:
Coqが返す「証明の状態」（仮説部＋サブゴール）がΓ⊢命題という演繹ルールの各段と正確に対応していることを解明します [p.434], [p.435]。後ろ向き推論（下段→上段）こそがCoqのtactic駆動型証明の本質であることを示します [p.386], [p.394]。
- 論理展開:
- 仮説部A:Prop, H:A、サブゴールAという証明状態はA:Prop, H:A⊢Aと等価 [p.438], [p.439]。
- ∧Iルールの後ろ向き適用によりΓ⊢A∧BはΓ⊢AとΓ⊢Bという2サブゴールに分割される [p.413], [p.415]。
- →Iルールの後ろ向き適用によりΓ⊢A→BはΓ,A⊢Bとなり仮説部自体が変化する [p.422], [p.427]。
■ Part 7: 論理式の証明（7）—tactic（1）サブゴールの形と演繹ルールの選択
- この部の核心:
サブゴールの論理的形状に基づいてtacticと演繹ルールの対応を体系化します。`intros`（→I）、`split`（∧I）、`left`（∨IL）、`right`（∨IR）がそれぞれどのサブゴール形状に反応し、仮説部とサブゴールをどのように変化させるかを視覚的に整理します [p.452]。
- 論理展開:
- `intros`：サブゴールがA→Bの形のとき、AをΓに移動しサブゴールをBにする [p.456], [p.460]。
- `split`：サブゴールがA∧Bの形のとき、AとBの二つのサブゴールに分割する [p.462], [p.468]。
- `left`/`right`：サブゴールがA∨Bの形のとき、それぞれAまたはBという一つのサブゴールに絞る [p.469], [p.475]。
- `intros`は`A→B→C→…→X`のような連鎖的な含意にも一括して適用可能 [p.478], [p.481]。
■ Part 8: 論理式の証明（8）—tactic（2）仮説部の形と演繹ルールの選択
- この部の核心:
今度は仮説部の論理的形状に基づく演繹ルールとtacticを整理します。`apply`（A→Bを仮説に持つとき）、`destruct`（A∨BまたはA∧Bを仮説に持つとき）、`assumption`/`exact`（仮説部にサブゴールと一致する命題があるとき）の三系統を解説します [p.527]。
- 論理展開:
- `apply`：仮説にA→Bがあり現在のサブゴールがBなら、サブゴールをAに変換する（後ろ向きmodus ponens）[p.529], [p.533]。
- `destruct`（∨）：仮説A∨BをAとBの二ケースに分岐させ、サブゴールは変化せず二つのサブゴールを生む [p.534], [p.543]。
- `destruct`（∧）：仮説A∧BをAとBの二つの独立した仮説に分解する [p.534], [p.538]。
- `assumption`/`exact H`：仮説部にサブゴールと一致する命題がある場合に証明を終了させる [p.547], [p.552], [p.553]。
■ Part 9: 論理式の証明（9）—「否定」について
- この部の核心:
Coqでの否定演算子`~`は基本的な論理演算子ではなく、`~A`は`A→False`の省略形として定義されていることを示します [p.558], [p.559]。型Falseが定義を持たない（証明を持たない）ことから、`ex falso quodlibet`（偽からはどんな命題も導かれる）という重要な定理が成立するCoqの内部論理を解説します [p.580], [p.586]。