Coq 入門

定理証明支援系とは

  • 証明が正しいことを検証してくれる装置。
  • 公理から定理の証明を構築する手順を、型システムで模倣する。
  • （証明は人間が作る）
  • 検証だけでなく、証明の構築も支援してくれる。

定理証明支援系の１つとして Coq がある。

インストール

以下のどちらかを選択。

  • インストーラ：レポジトリから入手できる。バージョンは遅れがち。

  • opam：Coq/SSReflect/MathCompの設定に従って入れる。

    • sudo apt get installでなくsudo apt install
    • WSLでは「新しいライブラリの設定が要るかも」の箇所でsudo apt install -y libgmp-devが必要だった(参考)
    • opam update,opam upgradeでアップデートできる（ビルドにかなり時間がかかるので注意）。

エディタ

  • VScode+VSCoq がおすすめ。VScode上で拡張機能(Ctrl+Shift+X)から「vscoq」と検索すれば出てくる。

    • Windowsの人はWSL上で動かせるように Remote - WSL も入れよう（「wsl」で検索）。

  • CoqIDE もインストーラから入れた場合は利用できる（がVSCoqの方が便利）

  • Emacs 上で Proof General を動かす手段もあるらしい。

  • jsCoq：ブラウザ上で動くCoq。

まずは簡単な例。

Section ModusPonens.
Variables P Q : Prop.
Theorem MP : P -> (P -> Q) -> Q.
Proof.
  intros Pis PimpliesQ.
  apply PimpliesQ.
  apply Pis.
Qed.

VSCoq, jsCoq上ではAlt+↓で１文ずつ証明が読み込まれる。

ここで Print MP. を実行すると

MP =
fun (Pis : P) (PimpliesQ : P -> Q) =>
PimpliesQ Pis
     : P -> (P -> Q) -> Q

Arguments MP _ _%function_scope

のように表示される。

つまりMPとは、引数としてPis(値)とPimpliesQ(関数)を受け取ってPimpliesQ Pisを返す関数。

Coqの(正確にはGallinaの)書式は変数名 : 型。

MPの型P -> (P -> Q) -> Qは、P型の値とP->Q型の値(関数)を受け取ってQ型の値を返す関数、を意味する。

これを、「Pという言明の証明とP->Qという言明の証明を受け取ってQという言明の証明を作る」ことと同一視する。

<div style="text-align: right; font-weight:bold">→ Curry-Howard同型対応</div>

（はじめから

Definition MP := fun (x : P) (y : P -> Q) => y x.

のようにGallinaの項を与えても同じ。証明が長くなってくると困難。）

Curry-Howard同型対応における解釈

論理演算 解釈
A∧BA\land B AAの証明とBBの証明のペアの集合（直積集合）
A∨BA\lor B AAの証明の集合とBBの証明の集合の和集合
A→BA\to B AAの証明からのBBの証明の構成方法の集合
∀x ⁣:A,B(x)\forall x\colon A, B(x) AAの証明xxからのB(x)B(x)の構成方法の集合（依存型）
∃x ⁣:A,B(x)\exists x \colon A, B(x) AAの証明xxとB(x)B(x)のペアの集合（依存型）

依存型は、証明の型がxxに依存する。

帰納的に定義される型

Print bool.を行うと

Inductive bool : Set :=  true : bool | false : bool.

と表示される。bool型はtrueとfalseから構成されている。

自然数も帰納的に定義されている。Print nat.を行うと

Inductive nat : Set :=  O : nat | S : nat -> nat.
  • O（これは00のこと）はnat型で
  • nat型の値にSを作用させたものもnat型で
  • それらだけがnat型である

ことが分かる。

Sを作用させることは次に大きい自然数を作ることに対応している。
O↔0, S O↔1, S (S O)↔2, S (S (S O))↔3......。

命題としてのTrue, False（bool型のtrue, falseとは異なる）やand, orも帰納的に定義されている。

SSReflect

  • Coq には標準ライブラリに加えて，SSReflect，MathComp という強力なライブラリがある．（この2つは現在は同じライブラリとしてまとめられている．）

  • このライブラリを読み込むことで，定理だけでなく新しいタクティックまで導入することができる．

move

  • move=>-> : intro TMP; rewrite TMP; clear TMP。move->とも書ける。

Coq の効用

  • とても長大で，全てを人間が検査することが難しい証明の正しさを保証できる．（例．四色定理，奇数位数定理）
  • ソフトウェアにバグがないことを保証できる．（例：CompCert）

リンク集

リンク集2

参考文献