Mercurial > cpdt > repo
comparison src/Tactics.v @ 66:b52204928c7d
Put [try] in front of [subst], to avoid whining about recursive equalities
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Wed, 01 Oct 2008 09:33:44 -0400 |
parents | 21bb59c56b98 |
children | 506a06118014 |
comparison
equal
deleted
inserted
replaced
65:21bb59c56b98 | 66:b52204928c7d |
---|---|
12 Require Omega. | 12 Require Omega. |
13 | 13 |
14 Set Implicit Arguments. | 14 Set Implicit Arguments. |
15 | 15 |
16 | 16 |
17 Ltac inject H := injection H; clear H; intros; subst. | 17 Ltac inject H := injection H; clear H; intros; try subst. |
18 | 18 |
19 Ltac appHyps f := | 19 Ltac appHyps f := |
20 match goal with | 20 match goal with |
21 | [ H : _ |- _ ] => f H | 21 | [ H : _ |- _ ] => f H |
22 end. | 22 end. |
44 match goal with | 44 match goal with |
45 | [ H : ex _ |- _ ] => destruct H | 45 | [ H : ex _ |- _ ] => destruct H |
46 | 46 |
47 | [ H : ?F _ = ?F _ |- _ ] => injection H; | 47 | [ H : ?F _ = ?F _ |- _ ] => injection H; |
48 match goal with | 48 match goal with |
49 | [ |- _ = _ -> _ ] => clear H; intros; subst | 49 | [ |- _ = _ -> _ ] => clear H; intros; try subst |
50 end | 50 end |
51 | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H; | 51 | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H; |
52 match goal with | 52 match goal with |
53 | [ |- _ = _ -> _ = _ -> _ ] => clear H; intros; subst | 53 | [ |- _ = _ -> _ = _ -> _ ] => clear H; intros; try subst |
54 end | 54 end |
55 | 55 |
56 | [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; subst | 56 | [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst |
57 | [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; subst | 57 | [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst |
58 end. | 58 end. |
59 | 59 |
60 Ltac rewriteHyp := | 60 Ltac rewriteHyp := |
61 match goal with | 61 match goal with |
62 | [ H : _ |- _ ] => rewrite H | 62 | [ H : _ |- _ ] => rewrite H |
106 repeat match goal with | 106 repeat match goal with |
107 | [ H : done _ |- _ ] => clear H | 107 | [ H : done _ |- _ ] => clear H |
108 end. | 108 end. |
109 | 109 |
110 Ltac crush' lemmas invOne := | 110 Ltac crush' lemmas invOne := |
111 let sintuition := simpl in *; intuition; subst; repeat (simplHyp invOne; intuition; subst); try congruence | 111 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence |
112 in (sintuition; rewriter; | 112 in (sintuition; rewriter; |
113 repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); | 113 repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); |
114 repeat (simplHyp invOne; intuition)); | 114 repeat (simplHyp invOne; intuition)); |
115 un_done; sintuition; try omega). | 115 un_done; sintuition; try omega). |
116 | 116 |