coqのタクティックの動作
今まで何となく使っていたcoqのタクティックの動作を少し詳しく見てみることにした。
ソースコードを読むべきかもしれないけど、まずは実際どう動くかを観察して解釈することにした
以下はその記録
destruct
and(/\)のdestruct
Goal forall P Q: Prop, P/\Q -> Q/\P. Proof. intros.
1 subgoal P : Prop Q : Prop H : P /\ Q ============================ Q /\ P
ここで destruct H. を使うと仮定のP/\QがPとQになる
1 subgoal P : Prop Q : Prop H : P H0 : Q ============================ Q /\ P
Andの定義を参照すると
Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B where "A /\ B" := (and A B) : type_scope.
さっきP/\Qをdestructして現れたPとQはconjの仮定(->の左にあるもの)であると考えられる
or(\/)のdestruct
今度は
Goal forall P Q: Prop, P\/Q -> Q\/P. Proof. intros.
1 subgoal P : Prop Q : Prop H : P \/ Q ============================ Q \/ P
仮定のP/\Qをdestructするとゴールが二つに分かれて一つ目のゴールの証明ではPが仮定、二つ目ではQが仮定となる
2 subgoals P : Prop Q : Prop H : P ============================ Q \/ P subgoal 2 is: Q \/ P
(一つ目のゴール証明後)
1 subgoal P : Prop Q : Prop H : Q ============================ Q \/ P
orの定義を見てみると
Inductive or (A B:Prop) : Prop := | or_introl : A -> A \/ B | or_intror : B -> A \/ B where "A \/ B" := (or A B) : type_scope.
であり、二つのゴールはそれぞれのコンストラクタに対応することが分かる
代数的データ型のdestruct
では適当な代数的データ型、例えば
Inductive abc (A: Prop) (B: Prop) (C: Prop): Prop := c1 : A -> B -> abc A B C | c2 : C -> abc A B C.
のように定義した代数的データ型abcをdestructするとどうなるか
Goal forall A B C: Prop, abc A B C -> (A/\B) \/ C. intros. destruct H.
andとorでの結果から、このとき二つのゴールができて、一つ目のゴールではコンストラクターc1に対応してAとBを仮定に持ち、もう一つのゴールではc2に対応してCを仮定に持つようになると予想できる
そして実際そうなる
2 subgoals A : Prop B : Prop C : Prop H : A H0 : B ============================ A /\ B \/ C subgoal 2 is: A /\ B \/ C
(一つ目のゴール証明後)
1 subgoal A : Prop B : Prop C : Prop H : C ============================ A /\ B \/ C
existsのdestruct
コンストラクタにforallが含まれる場合が抜けていたことに気がついた
Goal forall (P: nat->Prop) (Q: Prop), (exists n:nat, P n) -> Q. intros.
1 subgoal P : nat -> Prop Q : Prop H : exists n : nat, P n ============================ Q
destruct H.
1 subgoal P : nat -> Prop Q : Prop x : nat H : P x ============================ Q
existsの定義
Inductive ex (A:Type) (P:A -> Prop) : Prop := ex_intro : forall x:A, P x -> ex (A:=A) P. Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) (at level 200, x binder, right associativity, format "'[' 'exists' '/ ' x .. y , '/ ' p ']'") : type_scope.
exの定義はA:=Aの部分がよく分からないが、コンストラクタex_introにforallがあるのがこれまでの例と違う
定義とdestructの動作を見比べるとex_introの中のforallのxと->の左の部分に対応するものが仮定になるようだ
これらはゴールが
forall x:A, P x -> ex (A:=A) P.
であるときにintrosで仮定に移動するものである
case
destructとほとんど同じように見える
->の左に追加されるか仮定に追加されるかの違い
split
http://coq.inria.fr/refman/Reference-Manual010.html#hevea_tactic18
コンストラクタが一つの場合のみ使える
コンストラクタの中の->の左にあるものがゴールになる
面倒になってきたのでここまで
