Mercurial > cpdt > repo
comparison src/Tactics.v @ 213:c4b1c0de7af9
Start of MoreDep port; new [dep_destruct] based on [dependent destruction]
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Wed, 11 Nov 2009 10:27:47 -0500 |
parents | cbf2f74a5130 |
children | 4293dd6912cd |
comparison
equal
deleted
inserted
replaced
212:3227be370687 | 213:c4b1c0de7af9 |
---|---|
141 repeat (simplHyp invOne; intuition)); un_done | 141 repeat (simplHyp invOne; intuition)); un_done |
142 end; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)). | 142 end; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)). |
143 | 143 |
144 Ltac crush := crush' false fail. | 144 Ltac crush := crush' false fail. |
145 | 145 |
146 Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Type), | 146 Require Import Program.Equality. |
147 (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with | |
148 | refl_equal => v' | |
149 end)) | |
150 -> P v. | |
151 intros. | |
152 generalize (X _ v (refl_equal _)); trivial. | |
153 Qed. | |
154 | 147 |
155 Ltac dep_destruct E := | 148 Ltac dep_destruct E := |
156 let doit A := | 149 let x := fresh "x" in |
157 let T := type of A in | 150 remember E as x; simpl in x; dependent destruction x; |
158 generalize dependent E; | 151 try match goal with |
159 let e := fresh "e" in | 152 | [ H : _ = E |- _ ] => rewrite <- H in *; clear H |
160 intro e; pattern e; | 153 end. |
161 apply (@dep_destruct T); | |
162 let x := fresh "x" with v := fresh "v" in | |
163 intros x v; destruct v; crush; | |
164 let bestEffort Heq E tac := | |
165 repeat match goal with | |
166 | [ H : context[E] |- _ ] => | |
167 match H with | |
168 | Heq => fail 1 | |
169 | _ => generalize dependent H | |
170 end | |
171 end; | |
172 generalize Heq; tac Heq; clear Heq; intro Heq; | |
173 rewrite (UIP_refl _ _ Heq); intros in | |
174 repeat match goal with | |
175 | [ Heq : ?X = ?X |- _ ] => | |
176 generalize (UIP_refl _ _ Heq); intro; subst; clear Heq | |
177 | [ Heq : ?E = _ |- _ ] => bestEffort Heq E ltac:(fun E => rewrite E) | |
178 | [ Heq : _ = ?E |- _ ] => bestEffort Heq E ltac:(fun E => rewrite <- E) | |
179 end | |
180 in match type of E with | |
181 | _ ?A => doit A | |
182 | _ _ ?A => doit A | |
183 | _ _ _ ?A => doit A | |
184 end. | |
185 | 154 |
186 Ltac clear_all := | 155 Ltac clear_all := |
187 repeat match goal with | 156 repeat match goal with |
188 | [ H : _ |- _ ] => clear H | 157 | [ H : _ |- _ ] => clear H |
189 end. | 158 end. |