タクティクリファレンス: コンストラクタの適用

constructor タクティク

constructor num

intros した後、代数的データ型であるゴールの型について、その num 番目のコンストラクタを apply する。

constructor num with …

apply する際に必要な引数を指定する。apply … with … を参照。

constructor

apply 可能なコンストラクタを一つ目から順番に試す。

Coq < Print True.
Inductive True : Prop :=  I : True

Coq < Goal True.
1 subgoal
  
  ============================
   True

Unnamed_thm < constructor. (* apply I に同じ *)
Proof completed.

split タクティク

split

intros した後、一つのコンストラクタのみによって定義された代数的データ型のゴールについて、そのコンストラクタを apply する。constructor 1 に等しいが、一つのコンストラクタのみによって定義された代数的データ型のゴールにしか使えない。

Coq < Print and.
Inductive and (A B : Prop) : Prop :=  conj : A -> B -> A /\ B

Coq < Goal P -> Q -> P /\ Q.
1 subgoal
  
  ============================
   P -> Q -> P /\ Q

Unnamed_thm < split. (* intros; apply conj に同じ *)
2 subgoals
  
  H : P
  H0 : Q
  ============================
   P

subgoal 2 is:
 Q

Unnamed_thm < assumption.
1 subgoal
  
  H : P
  H0 : Q
  ============================
   Q

Unnamed_thm < assumption.
Proof completed.

split with bindinglist

apply する際に必要な引数を指定する。constructor 1 with bindinglist に等しいが、一つのコンストラクタのみによって定義された代数的データ型のゴールにしか使えない。apply … with … を参照。

exists タクティク

exists bindinglist

intros した後、一つのコンストラクタのみによって定義された代数的データ型のゴールについて、指定した引数でそのコンストラクタを apply する。constructor 1 with bindinglist に等しいが、一つのコンストラクタのみによって定義された代数的データ型のゴールにしか使えない。

Coq < Print ex.
Inductive ex (A : Type) (P : A -> Prop) : Prop :=
    ex_intro : forall x : A, P x -> ex P

For ex: Argument A is implicit
For ex_intro: Argument A is implicit
For ex: Argument scopes are [type_scope _]
For ex_intro: Argument scopes are [type_scope _ _ _]

Coq < Goal exists n : nat, n = 0.
1 subgoal
  
  ============================
   exists n : nat, n = 0

Unnamed_thm < exists 0. (* apply ex_intro with 0 に同じ *)
1 subgoal
  
  ============================
   0 = 0

Unnamed_thm < reflexivity.
Proof completed.

exists bindinglist1, …, bindinglistn (Coq 8.3 以降)

複数の exists を順に行う。

left タクティク

left

intros した後、二つのコンストラクタによって定義された代数的データ型のゴールについて、その一つ目のコンストラクタを apply する。constructor 1 に等しいが、ちょうど二つのコンストラクタによって定義された代数的データ型のゴールにしか使えない。

Coq < Print or.
Inductive or (A B : Prop) : Prop :=
    or_introl : A -> A \/ B | or_intror : B -> A \/ B

Coq < Goal P -> P \/ Q.
1 subgoal
  
  ============================
   P -> P \/ Q

Unnamed_thm < left. (* intros; apply or_introl に同じ *)
1 subgoal
  
  H : P
  ============================
   P

Unnamed_thm < assumption.
Proof completed.

left with bindinglist

apply する際に必要な引数を指定する。constructor 1 with bindinglist に等しいが、ちょうど二つのコンストラクタによって定義された代数的データ型のゴールにしか使えない。apply … with … を参照。

right タクティク

right

intros した後、二つのコンストラクタによって定義された代数的データ型のゴールについて、その二つ目のコンストラクタを apply する。constructor 2 に等しいが、ちょうど二つのコンストラクタによって定義された代数的データ型のゴールにしか使えない。

Coq < Print or.
Inductive or (A B : Prop) : Prop :=
    or_introl : A -> A \/ B | or_intror : B -> A \/ B

Coq < Goal Q -> P \/ Q.
1 subgoal
  
  ============================
   Q -> P \/ Q

Unnamed_thm < right. (* intros; apply or_intror に同じ *)
1 subgoal
  
  H : Q
  ============================
   Q

Unnamed_thm < assumption.
Proof completed.

right with bindinglist

apply する際に必要な引数を指定する。constructor 2 with bindinglist に等しいが、ちょうど二つのコンストラクタによって定義された代数的データ型のゴールにしか使えない。apply … with … を参照。