タクティクリファレンス: 項による証明

exact タクティク

exact term

ゴールの型を持つ項 term を直接証明として与える。

Coq < Goal True.
1 subgoal

  ============================
   True

Unnamed_thm < exact I.
Proof completed.

refine タクティク

refine term

ゴールの型を持つ項 term を直接証明として与える。ただし term はプレースホルダ _ を含んでいてもよく、各プレースホルダに対してそれを与えるためのサブゴールが生成される。

Coq < Definition pred (n : nat) : n <> 0 -> nat.
1 subgoal

  ============================
   forall n : nat, n <> 0 -> nat

pred < intro n.
1 subgoal

  n : nat
  ============================
   n <> 0 -> nat

pred < refine (match n with 0 => _ | S n' => (fun _ => n') end).
1 subgoal

  n : nat
  ============================
   0 <> 0 -> nat

pred < congruence.
Proof completed.

apply タクティク

apply term

項 term を現在のゴールに適用する。term の型(の結論部分)はゴールと単一化可能でなければならない。成功すると現在のゴールは削除され、term の型の前提部分が新たなゴールとなる (前提部分がなければ新たなゴールは生成されない)。

Coq < Goal P -> (P -> Q) -> Q.
1 subgoal

  ============================
   P -> (P -> Q) -> Q

Unnamed_thm < intros H1 H2.
1 subgoal

  H1 : P
  H2 : P -> Q
  ============================
   Q

Unnamed_thm < apply H2.
1 subgoal

  H1 : P
  H2 : P -> Q
  ============================
   P

Unnamed_thm < apply H1.
Proof completed.

term の型(の結論部分)が積になっている場合は、自動的に分解を試みる。

Coq < Goal P -> (P -> Q /\ R) -> Q.
1 subgoal

  ============================
   P -> (P -> Q /\ R) -> Q

Unnamed_thm < intros H1 H2.
1 subgoal

  H1 : P
  H2 : P -> Q /\ R
  ============================
   Q

Unnamed_thm < apply H2.
1 subgoal

  H1 : P
  H2 : P -> Q /\ R
  ============================
   P

term の型が依存型の場合、ゴールとの単一化によって前提の推論を試みる。

Coq < Goal forall (P : nat -> Prop), (forall n : nat, P n) -> P 0.
1 subgoal

  ============================
   forall P : nat -> Prop, (forall n : nat, P n) -> P 0

Unnamed_thm < intros P H.
1 subgoal

  P : nat -> Prop
  H : forall n : nat, P n
  ============================
   P 0

Unnamed_thm < apply H.  (* apply (H 0). でなくともよい *)
Proof completed.

apply term with term1 … termn

apply term において推論に失敗した term への引数として term₁ … term_n を使う。

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

  ============================
   exists n : nat, n = 0

Unnamed_thm < apply ex_intro.
Error: Unable to find an instance for the variable x.

Unnamed_thm < apply ex_intro with 0.
1 subgoal

  ============================
   0 = 0

apply term with (ref1 := term1) … (refn := termn)

apply term において推論に失敗した term への引数として term₁ … term_n を使う。ref_i は引数の名前または名前のない引数の番号。

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

  ============================
   exists n : nat, n = 0

Unnamed_thm < apply ex_intro with (x := 0).
1 subgoal

  ============================
   0 = 0

apply term1, …, termn

apply term1; [ … | | apply term2, …, termn ] に同じ。すなわち、まず term₁ を適用し、残った最後のサブゴールに term₂ を適用し、さらに残った最後のサブゴールに term₃ を適用し……というように繰り返す。

apply term in ident

apply term with … in ident

普通の apply に似ているが、term をゴールではなく前提 ident に適用する。このタクティクは ident を置き換えるので、ident が他の前提やゴールで使われているときは使えない (そういう時は apply で前提を置き換えるのではなく pose などで前提を追加するとよい)。

Coq < Goal P -> (P -> Q) -> Q.
1 subgoal

  ============================
   P -> (P -> Q) -> Q

Unnamed_thm < intros H1 H2.
1 subgoal

  H1 : P
  H2 : P -> Q
  ============================
   Q

Unnamed_thm < apply H2 in H1.
1 subgoal

  H1 : Q
  H2 : P -> Q
  ============================
   Q

Coq < Goal P -> (P -> Q) -> (Q -> R) -> R.
1 subgoal

  ============================
   P -> (P -> Q) -> (Q -> R) -> R

Unnamed_thm < intros H1 H2 H3.
1 subgoal

  H1 : P
  H2 : P -> Q
  H3 : Q -> R
  ============================
   R

Unnamed_thm < apply H3 in H2.
2 subgoals

  H1 : P
  H2 : R
  H3 : Q -> R
  ============================
   R

subgoal 2 is:
 P

Unnamed_thm < apply H2.
1 subgoal

  H1 : P
  H2 : P -> Q
  H3 : Q -> R
  ============================
   P

Unnamed_thm < apply H1.
Proof completed.

with を使う例:

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

  ============================
   0 = 0 -> exists n : nat, n = 0

Unnamed_thm < intro H.
1 subgoal

  H : 0 = 0
  ============================
   exists n : nat, n = 0

Unnamed_thm < apply ex_intro with nat (fun n => n = 0) 0 in H.
1 subgoal

  H : exists n : nat, n = 0
  ============================
   exists n : nat, n = 0

apply term in ident as intropattern (Coq 8.2 以降)

apply term with … in ident as intropattern (Coq 8.2 以降)

apply term (with …) in ident; destruct ident as intropattern に同じ。

simple apply …

apply に似ているが、推論すべき変数を含む部分項については自動的な項の変換を試みない。また、term の型(の結論部分)が積になっていても自動的な分解を試みない。