Library Asm.Util.Tactics

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.

This page has been generated by coqdoc