- 追加された行はこの色です。
- 削除された行はこの色です。
[[ProofCafe]]
*coqの起動 [#he48700c]
-対話環境を使う -> Terminalでcoqtopコマンドを実行
-emacsで使う -> ProofGeneral
-特別な開発環境を使う -> coqide
*操作方法 [#p168315c]
-概要: CoqはVernacularというメインコマンドと対話証明用のtacticを使って操作する。
-Vernacularは大文字で始まって、tacticは小文字で始まる。いずれもコマンドの最後はドット。
*Vernacularコマンド [#zcf82e9f]
外部ライブラリをインポートしたり、型や値を定義したり、仮定したり、定理を記述したりします。コマンドの一覧と詳しい説明はマニュアルの[[Vernacular一覧:http://coq.inria.fr/refman/command-index.html]]を見てください。次のコマンドを試してみましょう。
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 [#x4eafed6]
tacticの一覧と詳しい説明はマニュアルの[[tactic一覧:http://coq.inria.fr/refman/tactic-index.html]]を見てください。
-再帰関数に関する性質を証明するには減少する引数に対して最初にinductionするのは定石。
-タクティック表
| |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.
intros P h.
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.で証明モードを抜けましょう。
![[PukiWiki]](image/caml3.jpg "[PukiWiki]")
