Mercurial > cpdt > repo

comparison src/Tactics.v @ 66:b52204928c7d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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