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の起動 [#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.

 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 [#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.
  apply h.
 Qed.