|Some helpful tactics|
|Consider all possible cases for an expression by adding a goal that equates that expression with each possible value form. From "Coq'Art".|
LtaccaseEq e := generalize (refl_equal e); pattern e at -1; case e.
Version of |
LtacdestrEq hyp e := caseEq e; intro hyp.
|Remove an irrelevant antecedent from a product goal.|
Ltacirrelevant := let H := fresh "irrelevant" in (intro H; clear H).
Prove the goal by proving |
Ltacwrong := assert False; [idtac | contradiction].
|Add a term with a name, without bothering to keep around its value.|
Ltacadd H e := generalize e; intro H.
Versions of hint-based tactics specialized to |
Ltacmyauto := auto with asm.
Ltacmyeauto := eauto with asm.
Ltacmyrewrite := autorewrite with asm; trivial.
Ltacintu := intuition; myauto.
Ltaceintu := intuition; myeauto.
Ltacmyrauto := myrewrite; myauto.
Ltacsrewrite := simpl; myrewrite.