Mercurial > cpdt > repo

comparison src/Tactics.v @ 85:3746a2ded8da

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tagless interpreter & cfold
author Adam Chlipala <adamc@hcoop.net>
date Mon, 06 Oct 2008 13:07:24 -0400
parents 522436ed6688
children fd505bcb5632
comparison
equal deleted inserted replaced
84:522436ed6688 85:3746a2ded8da
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 Require Import List. 10 Require Import Eqdep List.
11 11
12 Require Omega. 12 Require Omega.
13 13
14 Set Implicit Arguments. 14 Set Implicit Arguments.
15 15
45 match goal with 45 match goal with
46 | [ H : ex _ |- _ ] => destruct H 46 | [ H : ex _ |- _ ] => destruct H
47 47
48 | [ H : ?F _ = ?F _ |- _ ] => injection H; 48 | [ H : ?F _ = ?F _ |- _ ] => injection H;
49 match goal with 49 match goal with
50 | [ |- _ = _ -> _ ] => clear H; intros; try subst 50 | [ |- _ = _ -> _ ] => try clear H; intros; try subst
51 end 51 end
52 | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H; 52 | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H;
53 match goal with 53 match goal with
54 | [ |- _ = _ -> _ = _ -> _ ] => clear H; intros; try subst 54 | [ |- _ = _ -> _ = _ -> _ ] => try clear H; intros; try subst
55 end 55 end
56 56
57 | [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst 57 | [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst
58 | [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst 58 | [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst
59 | [ H : ?F _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst 59 | [ H : ?F _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst
117 repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); 117 repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
118 repeat (simplHyp invOne; intuition)); 118 repeat (simplHyp invOne; intuition));
119 un_done; sintuition; try omega; try (elimtype False; omega)). 119 un_done; sintuition; try omega; try (elimtype False; omega)).
120 120
121 Ltac crush := crush' tt fail. 121 Ltac crush := crush' tt fail.
122
123 Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Prop),
124 (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with
125 | refl_equal => v'
126 end))
127 -> P v.
128 intros.
129 generalize (H _ v (refl_equal _)); trivial.
130 Qed.
131
132 Ltac dep_destruct E :=
133 let doit A :=
134 let T := type of A in
135 generalize dependent E;
136 let e := fresh "e" in
137 intro e; pattern e;
138 apply (@dep_destruct T);
139 let x := fresh "x" with v := fresh "v" in
140 intros x v; destruct v; crush;
141 let bestEffort Heq E tac :=
142 repeat match goal with
143 | [ H : context[E] |- _ ] =>
144 match H with
145 | Heq => fail 1
146 | _ => generalize dependent H
147 end
148 end;
149 generalize Heq; tac Heq; clear Heq; intro Heq;
150 rewrite (UIP_refl _ _ Heq); intros in
151 repeat match goal with
152 | [ Heq : ?X = ?X |- _ ] =>
153 generalize (UIP_refl _ _ Heq); intro; subst; clear Heq
154 | [ Heq : ?E = _ |- _ ] => bestEffort Heq E ltac:(fun E => rewrite E)
155 | [ Heq : _ = ?E |- _ ] => bestEffort Heq E ltac:(fun E => rewrite <- E)
156 end
157 in match type of E with
158 | _ _ ?A => doit A
159 | _ ?A => doit A
160 end.