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.