Various useful tactics |
| version 1.0 |
Ltac elimer e := try exact e; let H := fresh "H" in (generalize e; intro H).
Use a fact, whose type is a non-dependent product.
This is modus ponens in forward chaining
use H e when the type of e is A1 -> A2 -> ... -> An -> B
will introduce the subgoals Ai and on the last
subgoal will add the hypothesis H : B
|
Ltac use H e :=
match type of e with
| ?A -> ?B =>
let H' := fresh "H'" in
(assert (H' : A);
[idtac (* we'll return the subgoal A *)
| use H (e H'); try clear H' ])
| ?B => assert (H : B);
[exact e | idtac ]
end.
Like use H H, (use a hypothesis and re-use its name)
|
Ltac usehyp H :=
let H' := fresh "H'" in
(use H' H; clear H; try rename H' into H).
This is like rewrite H in *
|
Ltac rewriteall H :=
let n := fresh "val" in
(match type of H with
?E1 = ?E2 =>
set (n:= E1) in * ;
clearbody n;
subst n
end).
History |
|