![[PukiWiki]](image/caml3.jpg "[PukiWiki]")
ProofCafe/Coq01 のバックアップ(No.2)
基本操作
起動 †
シェルで次の用に入力すると対話環境が立ち上がる
$ coqtop Welcome to Coq 8.2pl1 (December 2009) Coq <
終了はQuit.(dotを忘れないように)
Coq < Quit. $
また、Coqのソースコード foo.v をコンパイルするためのcoqcコマンドもある
$ coqc foo.v
CoqソースコードからhtmlまたはLaTeX用のドキュメントを生成するためのコマンドはcoqdoc
$ coqdoc --html foo.v
Coq用のMakefileを簡単に作れるcoq_makefileやocamlmktopのようなcoqmktopもある
基本的なCoqコマンド(Vernaculer コマンドと呼ばれる) †
Coqのコマンドは大文字で始まる。そして最後に必ずdotを忘れないように。
調べる系のコマンド †
Check †
式の型を調べる
例:
Coq < Check 12.
12
: nat
Coq < Check nat.
nat
: Set
Print †
関数や命題の定義を調べる
例:
Coq < Print plus.
plus =
fix plus (n m : nat) : nat := match n with
| 0 => m
| S p => S (plus p m)
end
: nat -> nat -> nat
Argument scopes are [nat_scope nat_scope]
Coq < Print plus_n_O.
plus_n_O =
fun n : nat =>
nat_ind (fun n0 : nat => n0 = n0 + 0) (refl_equal 0)
(fun (n0 : nat) (IHn : n0 = n0 + 0) => f_equal S IHn) n
: forall n : nat, n = n + 0
Argument scope is [nat_scope]
Eval compute in †
計算結果を調べるコマンド。計算可能な関数を使った式を評価して結果を出力する。(3<5)などの命題は関数じゃないので計算されないことに注意しよう。(CheckしてProp型だったら計算されない)
例:
Coq < Eval compute in (12 * 5).
= 60
: nat
Locate †
中値演算子や特殊な記法の定義を調べる
例:
Coq < Locate "_ + _".
Notation Scope
"x + y" := sum x y : type_scope
"n + m" := plus n m : nat_scope
(default interpretation)
Coq < Locate "{ _ | _ }".
Notation Scope
"{ x | P }" := sig (fun x => P)
: type_scope
(default interpretation)
Import系のコマンド †
Open Scope †
特殊な記法を許すためにスコープをオープンする。スコープ名はだいたい"型名_scope"という命名規則で名付けられている。
例:
Open Scope Z_scope. Open Scope string_scope.
Require Import †
モジュールを読み込む. OCamlのopenに似ている
例:
Require Import ZArith. Require Import String. Require Import List.
Require Export †
モジュールをエクスポートする．OCamlのincludeに似ている
例:
Require Export ZArith. Require Export String. Require Export List.
定義、宣言系のコマンド †
Definition †
単純な値、関数、型、命題などを定義するコマンド。OCamlのlet文に似ているが := であることに注意しよう。
例:
Definition x := 3. Definition foo x := x + x * x. Definition natnat_list := list (nat * nat). Definition interval a b x := a < x < b.
Fixpoint, CoFixpoint? †
再帰関数を定義するときFixpoint、余再帰関数を定義するときにCoFixpoint?を用いる。Fixpointの場合は引数の型がInductive型でCoFixpoint?の場合は戻り値の型がCoInductive?型であることに注意しよう。
Fixpointの例(Listモジュールを使用):
Fixpoint append {A : Type} (xs ys: list A) :=
match xs with
| nil => ys
| x :: xs => x :: append xs ys
end.
CoFixpoint?の例(遅延リストのStreamsモジュールを使用):
CoFixpoint from n := Cons n (from (1 + n)).
Function †
Fixpointよりアドバンスドなコマンド。より複雑な再帰関数を定義するときに用いる。詳しくは http://d.hatena.ne.jp/yoshihiro503/20090923#p1 参照
Variable (Parameter, Axiom, Hypothesis) †
ある型を持つ値があるものと仮定して宣言する。Parameter、Axiom、Hypothesisなどもだいたい同じ機能だが、うまく使い分けると論文っぽくてかっこ良くなる。
例:
Variable x : nat. Variables y z : nat. Hypothesis foo : x < y + z.
Theorem (Lemma, Proposition, Fact, Goal、Remark, Corollary) †
型だけ宣言して、その値を対話的にtacticsで与えるためのコマンド。このコマンドのあとは対話的証明モードとなり、tacticsが使えるようになる。Lemma, Proposition, Fact, Goal、Remark, Corollaryなどのコマンドはシステム的にはみんなほぼ同じ機能。しかしうまく使い分けるとかっこ良いかも。 tacticsを駆使して証明が完了したらQedコマンドで対話的証明モードを終了させる。Definedコマンドも同様だがのちに内部を参照できるかどうかが変わってくる。(参考: http://d.hatena.ne.jp/yoshihiro503/20090425#p1 )
例:
Theorem mytheorem : forall x, 2 < x -> x + x < x * x. ... tactics ... Qed.
Inductive, CoInductive? †
代数データ型や帰納的な命題などを定義するときにInductiveコマンドを使い、遅延リストのような無限のデータ構造やその上での余帰納的な命題を扱うときはCoInductive?コマンドを使う。
Inductiveの例:
Inductive bool : Set := true : bool | false : bool. Inductive list (A:Set) : Set := | nil : list A | cons : A -> list A -> list A. Inductive even : nat -> Prop := | even_0 : even O | even_SS : forall n:nat, even n -> even (S (S n)).
(注意: Coq 8.2くらいから以下のようなライトウェイトなシンタックスでもOKになった.)
Inductive bool : Set := true | false. Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A).
CoInductive?の例:
CoInductive Stream (A : Type) : Type := | Cons : A -> Stream A -> Stream A.
