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 <
