Mercurial > cpdt > repo

comparison src/Tactics.v @ 184:699fd70c04a7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
About to stop using JMeq
author Adam Chlipala <adamc@hcoop.net>
date Sun, 16 Nov 2008 15:04:21 -0500
parents 02569049397b
children df289eb8ef76
comparison
equal deleted inserted replaced
183:02569049397b 184:699fd70c04a7
119 repeat match goal with 119 repeat match goal with
120 | [ H : done _ |- _ ] => clear H 120 | [ H : done _ |- _ ] => clear H
121 end. 121 end.
122 122
123 Ltac crush' lemmas invOne := 123 Ltac crush' lemmas invOne :=
124 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence 124 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in
125 in (sintuition; 125 let rewriter := autorewrite with cpdt in *;
126 autorewrite with cpdt in *; 126 repeat (match goal with
127 repeat (match goal with 127 | [ H : _ |- _ ] => (rewrite H; [])
128 | [ H : _ |- _ ] => (rewrite H; []) 128 || (rewrite H; [ | solve [ crush' lemmas invOne ] ])
129 || (rewrite H; [ | solve [ crush' lemmas invOne ] ]) 129 || (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ])
130 end; autorewrite with cpdt in *); 130 end; autorewrite with cpdt in *)
131 in (sintuition; rewriter;
131 match lemmas with 132 match lemmas with
132 | false => idtac 133 | false => idtac
133 | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); 134 | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
134 repeat (simplHyp invOne; intuition)); un_done 135 repeat (simplHyp invOne; intuition)); un_done
135 end; sintuition; try omega; try (elimtype False; omega)). 136 end; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)).
136 137
137 Ltac crush := crush' false fail. 138 Ltac crush := crush' false fail.
138 139
139 Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Prop), 140 Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Prop),
140 (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with 141 (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with