ProofCafe/Coq01 のバックアップ(No.6)

はてなグループ: ProofCafe

coqの起動 &dagger;

外部ライブラリをインポートしたり、型や値を定義したり、仮定したり、定理を記述したりします。コマンドの一覧と詳しい説明はマニュアルのVernacular一覧を見てください。次のコマンドを試してみましょう。

Require Import List.

Check 3.

「nat: Set」が出力されます。natは自然数型です。

Gallinaは型も式です。型の型はSetです。なので、例えば「『nat型』の型」を調べる (Check nat.) と、 Set が返ってきます。さらにSet の型はTypeです。Typeの型はTypeと再帰的になっています。

Set以外にも、命題の型であるPropがあります。例えば、Check 1=2. と入力すると、型Propが返ってきます。

Definition x := 20.
Definition t := list nat.

式を識別子に束縛するにはコマンドDefinitionを使います。識別子の名前は小文字でも大文字でもかまいません。 Gallina は型も値と同様に扱えるので Definition t := list nat . のように型をDeifnitionで識別子に束縛することもできます。

Inductive tramp : Set := 
| Jorker : tramp
| Heart : nat -> tramp
| Spade : nat -> tramp
| Club : nat -> tramp
| Dia : nat -> tramp.

Inductive コマンドで型を定義できます。ここで Joker や Heart などはコンストラクタになります。

Fixpoint fact n :=
   match n with
   | O => 1
   | S m => n * fact m
   end.

Fixpoint は再帰関数を定義できます。 Definition との違いは、定義本体で再起呼び出しができることです。

パターンマッチでOやSを用いていますが、これはCoqではでは自然数は O (オー;ゼロの意味) と S n (n+1の意味)で表現するためです。 1, 2, 3.. などと書くと、自動的に S (S (S O)) などと展開される。

Theorem my_great_theorem : forall P:Prop, P -> P.
Abort.

Theoremコマンドで証明したい命題を定義できます。

tacticの一覧と詳しい説明はマニュアルのtactic一覧を見てください。

タクティック表
forall -> exists /\ \/ ~ =
前提 - - elim H. elim H. elim H. elim H. rewrite H.
ゴール intros. intros. exists <term>. split. left.またはright. intro. reflexivity.

Theorem my_great_theorem : forall P:Prop, P -> P.
Proof.
 intro.
 intro h.
 apply h.
Qed.

intro: ゴールにあるforallを仮定にもちあげます。
intro h: ゴール (====の下) が P -> Q (PならばQ) の形のとき Pを仮定に追加 (====の上に移動) して、残ったゴール Q の証明に移ります。同時に、 intro h. で追加した仮定には識別子 h が付いて、以後の証明で使えるようになります。intro. のように識別子を省略することもでき、この場合はcoqtopが自動的に識別子を割り当てる。
apply h: 仮定hとゴールが同じ形になりました。こういう場合は、apply hでhをゴールに適用します。
Qed: 証明がおわったら、Qed.で証明モードを抜けましょう。