メモ晒し
自分の 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 くらいまでしか行ってない)
- 追記
最新版はここに。