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

• バックアップ一覧
• ソース を表示
• ProofCafe/Coq01 は削除されています。
  • 1 (2010-04-05 (月) 18:42:12)
  • 2 (2010-04-06 (火) 00:44:53)
  • 3 (2010-04-06 (火) 13:54:56)
  • 4 (2010-04-24 (土) 14:33:37)
  • 5 (2010-04-25 (日) 21:41:48)
  • 6 (2010-10-23 (土) 13:23:07)
  • 7 (2010-12-02 (木) 08:04:09)
  • 8 (2011-10-03 (月) 13:48:06)

ProofCafe

coqの起動 †

• 対話環境を使う -> Terminalでcoqtopコマンドを実行
• emacsで使う -> ProofGeneral?
• 特別な開発環境を使う -> coqide

操作方法 †

• 概要: CoqはVernacularというメインコマンドと対話証明用のtacticを使って操作する。
• Vernacularは大文字で始まって、tacticは小文字で始まる。いずれもコマンドの最後はドット。

Vernacularコマンド †

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

Require Import List.

Check 3.

Definition x := 20.

Definition t := list nat.

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

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

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

tactic †

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

• 再帰関数に関する性質を証明するには減少する引数に対して最初に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.
 apply h.
Qed.