Mercurial > cpdt > repo
diff src/Tactics.v @ 52:ce0c9d481ee3
What could go wrong; some exercises
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 28 Sep 2008 12:42:59 -0400 |
| parents | 9ceee967b1fc |
| children | 1a664ff9d2d1 |
line wrap: on
line diff
--- a/src/Tactics.v Sun Sep 28 11:57:15 2008 -0400 +++ b/src/Tactics.v Sun Sep 28 12:42:59 2008 -0400 @@ -12,9 +12,18 @@ Require Omega. +Ltac inject H := injection H; clear H; intros; subst. + Ltac simplHyp := match goal with - | [ H : S _ = S _ |- _ ] => injection H; clear H; intros; subst + | [ H : ?F _ = ?F _ |- _ ] => injection H; + match goal with + | [ |- _ = _ -> _ ] => clear H; intros; subst + end + | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H; + match goal with + | [ |- _ = _ -> _ = _ -> _ ] => clear H; intros; subst + end end. Ltac rewriteHyp := @@ -28,6 +37,6 @@ Hint Rewrite app_ass : cpdt. -Ltac sintuition := simpl in *; intuition; try simplHyp. +Ltac sintuition := simpl in *; intuition; try simplHyp; try congruence. Ltac crush := sintuition; rewriter; sintuition; try omega.