qnighy/coq-cheatsheet.md

## coq-cheatsheet.md

      
    Raw
  

              coq-cheatsheet.md
            
          
    Coqチートシートっぽい何か

Coqの入手先


Coq … INRIAが開発した証明支援系。 http://coq.inria.fr/
ssreflect … INRIAとMicrosoft Researchが開発した代数の証明群および、そのために作られたCoqの拡張文法。 http://www.msr-inria.inria.fr/Projects/math-components

Coqの開発環境


CoqTop … CoqのREPL。ちょっとした照明を書くときには使えるかもしれないが開発するのにはほぼ使えない。後述するIDEを使うこと。
CoqIDE … Gtk (lablGtk) で作られたIDE。エディタとしての機能はイマイチというか残念だけど、Coqの開発環境としてはマトモ。
ProofGeneral … Emacs用のプラグインで、Coq以外の証明支援系にも使えるらしい。Emacs使いならこれを使うのがよい。

Coqの証明の流れ

証明とは、目的の型をもつ値を組み立てることに相当する。(Curry-Howard対応)
パターン1. 定義したいものの型を宣言し、直後に値を入れる。

Definition Modus_Ponens: forall P Q:Prop, (P->Q)->P->Q
  := fun P Q => fun x y => x y.
このような方法は、定理の証明においては普通用いられない。
パターン2. 定義したいものの型を宣言し、即座に証明モードに入る。

Theorem Modus_Ponens: forall P Q:Prop, (P->Q)->P->Q.
Proof.
  intros.
  apply H.
  apply H0.
Qed.
定理の証明において一般的に用いられる手法である。
パターン3. 定義したいものの型を宣言し、その定義の一部を書き、証明モードに入って残りを埋める。

Program Definition Modus_Ponens: forall P Q:Prop, (P->Q)->P->Q
  := fun P Q x _ => x _.
Next Obligation.
Proof.
  intros.
  exact H.
Qed.
プログラムの中に証明を埋め込みたいときに有用である。
ここでは基本的にパターン2のみが出現する。
宣言部の命令


Goal … 無名の定理を証明する。
Definition … 定義。直接定義を書くのが普通だが、証明モードに入ってもよい。
Program Definition … 定義をするが、穴を証明モードで補完する。
Theorem, Lemma, Propositionなど … 証明する。

証明を始める前に行う命令


Proof. … Proofと書くことによって証明を書く人のやる気を高める。
Proof with hogehoge. … この証明中で3点リーダー「...」を用いるとhogehogeを実行することになる。

証明を終了するときに行う命令


Qed. … 証明終了。
Defined. … 定義終了。 証明終了と違い、定義された内容がTransparentになる。
Admitted. … 証明途中であっても証明を破棄し、その命題を公理として仮定してしまう。

IDEの使い方

Coqの証明モードでは、ゴールの形を見ながら次に適用するルールを決めていく。
CoqIDEやProofGeneralなどのIDEでは、証明の現在位置が記録されており、現在位置より上は色がついていて編集できないようになっている。
証明の方針が誤っていた場合などは、現在位置を後ろに戻すことができる。
詳しくは実際にIDEを使って証明してみればわかる。
初歩的なtactic

証明モード中で使える証明用のコマンドはtacticと呼ばれる。これはLtacという型なしラムダ計算のプログラムである。
最初に使うtactic

証明のはじめはほぼ確実にintrosが用いられる。
これは目的の定理から仮定をとってくるtacticである。
命題論理で使うtactic

まずは命題論理で練習するのが定石っぽいのでそれを先に書く。
Coqで命題論理を証明するときのスタンダードな方法は、シークエント計算LJのそれとほぼ同じである。
(自然演繹NJと同等の手順で証明することも不可能ではない)
つまり、仮定と帰結をそれぞれ分解していくことによって定理を証明する。

  仮定が 帰結が 
  A→B apply H. / apply H in H0. intro.
  A∧B destruct H. split.
  A∨B destruct H. left. / right.
  False destruct H. なし

帰納法

自然数やリストなどは帰納的に定義されている。こういった値についての帰納法を定義することができる。
自然数nが手元にあり、ゴールにnが含まれているとする。このゴールをP(n)と書くことにしよう。
すると、induction n. という命令をすることで二つのゴールが生成される。

(1) 仮定には何も追加されていない。ゴールにP(0)がある。
(2) 仮定には自然数nと、P(n)がある。ゴールにP(S n)がある。

ただし、S nは1+nのことだと考えればよい。
便利なtactic


auto … 仮定やヒントデータベースから証明を探していろいろ適用してみてくれる。

autoは命題論理に対しては強力なので、命題論理で練習している間は使わないこと。
	仮定が	帰結が
A→B	apply H. / apply H in H0.	intro.
A∧B	destruct H.	split.
A∨B	destruct H.	left. / right.
False	destruct H.	なし