| 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". |
Ltac caseEq e := generalize (refl_equal e); pattern e at -1; case e.
Version of caseEq that introduces the equalities with a given hypothesis name
|
Ltac destrEq hyp e := caseEq e; intro hyp.
| Remove an irrelevant antecedent from a product goal. |
Ltac irrelevant := let H := fresh "irrelevant" in (intro H; clear H).
Prove the goal by proving False.
|
Ltac wrong := assert False; [idtac | contradiction].
| Add a term with a name, without bothering to keep around its value. |
Ltac add H e := generalize e; intro H.
Versions of hint-based tactics specialized to asm
|
Ltac myauto := auto with asm.
Ltac myeauto := eauto with asm.
Ltac myrewrite := autorewrite with asm; trivial.
Ltac intu := intuition; myauto.
Ltac eintu := intuition; myeauto.
Ltac myrauto := myrewrite; myauto.
Ltac srewrite := simpl; myrewrite.