メモ晒し

Coq

自分の Coq メモを晒してみる。

■ ; について
T1 ; T2
	T1 適用後、T1 によって出来た全てのサブゴールに対して T2 を適用
T1 ; [T2 | T3] 
	T1 適用後、T1 によって出来たサブゴール a, b に対して、a に T2、b に T3 を適用
	(不要なら T2, T3 を省略可(何もしない)) 
 
■tacticについて
intro / intros
	前提の導入
	ゴールの forall や -> で括られた部分を前提へ
	intros で名前を付けるときは左から
	前提に持って行かない場合は、名前を _ にする (intros のみ)
apply
	前提 A -> B、ゴール B があるとき、ゴールを A にする
	ゴールに適用できる関数があるとき、apply 関数 でゴールに関数を適用する
assert
	assert (前提の名前 := 式) で、式によって証明させる命題を前提に追加する
exact
	前提 H がゴールと同じ場合、exact H でゴールの証明を終了する
	証明と等価な関数があるとき、exact 関数 でゴールの証明を終了する
assumption
	前提にゴールがある場合、ゴールの証明を終了する
elim
	前提によって、以下の規則を適用
	・前提が A /\ B の場合
		ゴール G を、A -> B -> G にする
	・前提が A \/ B の場合
		ゴール G を、A -> G と B -> G に分割する
	・前提が not A の場合
		ゴールを A にする
	・前提が exists x : A, P x の場合
		ゴール G を、forall x:A, P x -> G にする
split
	and のゴールを分解する
	apply conj の省略形
left / right
	or のゴールの片方を選ぶ
	left は apply or_introl、right は apply or_intror の省略形
exists
	前提に H : x:A があるとき、exists H で、ゴールの exists a:A, P a を P x にする
clear
	指定した前提を除去
auto
	intro, apply, assumption 等を、ユーザの指示無しで組み合わせてゴールに辿り着ける場合、適用
trivial
	intro, apply, assumption 等を、1回だけ適用
tauto
	トートロジーである場合、適用
try tauto
	tautoが可能であれば、適用 (出来ないならば何もしない)
cut
	cut P で、ゴール G を、P -> G と P に分割する
generalize
	前提 A、ゴール G のとき、ゴールを A -> G にする
rewrite
	前提 H : A = B のとき、
		・rewrite (->) H でゴールの A を B にする
		・rewrite <- H でゴールの B を A にする
replace A with B
	ゴール G を、G 中の A を B に置き換えたものと、B = A に分割
unfold A
	ゴールの A を展開する
transitivity C
	ゴールの A = B を A = C と C = B に分割
symmetry
	ゴールの A = B を B = A にする
reflexivity
	ゴールが A = A のとき、ゴールの証明を終了する (反射律)

(* このあたりてきとう *)
simpl
	ç°¡ç´„ (?)
compute / cbv
	ç°¡ç´„ (?)
congruence
	ゴールが、同値変形で導ける場合、適用 (?)
omega
	nat, Z 上の、~, /\, \/, -> で組み立てられた等式や不等式を自動で頑張ってくれる?
	使うときは、Require Import Omega.
ring
	ゴールが、環の性質を使った変形で導ける場合、適用 (?)
field
	ゴールが、体の性質を使った変形で導ける場合、適用 (?)

induction n
	n に関する帰納法の開始
inversion H
	H が成立するための前提を前提に追加する
injection H
	コンストラクタ C に対し前提 H : C a = C b のとき、ゴール G を a = b -> G にする

■coqtopのコマンド
＊通常モード
Check ...
	...の型等を表示
Eval compute in ...
	...を計算
Locate "(演算子)"
	(演算子) の定義を表示
Section ...
	...という名前でセクションを切る
Goal ...(Prop)
	...の証明を開始
Print ...(定理とか)
	...の中身を関数形式で表示 

＊証明モード
Restart
	証明を始めから
Abort
	証明をやめる
Undo
	証明を1つ戻す

■その他
-> は右結合

チュートリアル続き読まないと。
(1.4 くらいまでしか行ってない)

  • 追記

最新版はここに。