[Coq] Coq Advent Calender : clear (18 of 25)

　Coq でよく使われる tactic の18番目は clear です...って使わないと思うけどなぁ。

　clear Hとすると、仮定 H が消えます。下記の様な感じです。

Coq < Lemma Sample_of_clear : forall A B C, (A->B->C)->(A->B)->A->C.
1 subgoal
  
  ============================
   forall A B C : Type, (A -> B -> C) -> (A -> B) -> A -> C

Sample_of_clear < intros A B C abc ab a.
1 subgoal
  
  A : Type
  B : Type
  C : Type
  abc : A -> B -> C
  ab : A -> B
  a : A
  ============================
   C

Sample_of_clear < apply abc; clear abc.
2 subgoals
  
  A : Type
  B : Type
  C : Type
  ab : A -> B
  a : A
  ============================
   A

subgoal 2 is:
 B

Sample_of_clear < exact a.
1 subgoal
  
  A : Type
  B : Type
  C : Type
  ab : A -> B
  a : A
  ============================
   B

Sample_of_clear < apply ab; clear ab.
1 subgoal
  
  A : Type
  B : Type
  C : Type
  a : A
  ============================
   A

Sample_of_clear < exact a.
Proof completed.

Sample_of_clear < Qed.

　使い終わって不要になった仮定をclearで消すと多少見通しが良くなる事もありますが、あまり使わないのではないかなぁ。

　むしろ、各種 tactic の中で内部的に使われる事が多い様な気がします。例えば下記の簡単な tactic の swap の中で使われています。apply して一回使った仮定は不要なので clear で消しているようです。

Ltac swap H := 
  idtac "swap is OBSOLETE: use contradict instead.";
  intro; apply H; clear H.

　これを使った証明です。

Coq < Lemma Sample_of_claer : forall P, ~~~P -> ~P.
1 subgoal
  
  ============================
   forall P : Prop, ~ ~ ~ P -> ~ P

Sample_of_claer < intros.
1 subgoal
  
  P : Prop
  H : ~ ~ ~ P
  ============================
   ~ P

Sample_of_claer < swap H.
swap is OBSOLETE: use contradict instead.
1 subgoal
  
  P : Prop
  H0 : P
  ============================
   ~ ~ P

Sample_of_claer < swap H.
swap is OBSOLETE: use contradict instead.
1 subgoal
  
  P : Prop
  H0 : P
  ============================
   P

Sample_of_claer < exact H0.
Proof completed.

Sample_of_claer < Qed.
intros.
swap H.
swap ipattern:H.
exact H0.

Sample_of_claer is defined

Coq <