adamc@2
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@2
|
2 *
|
adamc@2
|
3 * This work is licensed under a
|
adamc@2
|
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
|
adamc@2
|
5 * Unported License.
|
adamc@2
|
6 * The license text is available at:
|
adamc@2
|
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
|
adamc@2
|
8 *)
|
adamc@2
|
9
|
adamc@85
|
10 Require Import Eqdep List.
|
adamc@2
|
11
|
adamc@38
|
12 Require Omega.
|
adamc@38
|
13
|
adamc@59
|
14 Set Implicit Arguments.
|
adamc@59
|
15
|
adamc@2
|
16
|
adamc@66
|
17 Ltac inject H := injection H; clear H; intros; try subst.
|
adamc@51
|
18
|
adamc@59
|
19 Ltac appHyps f :=
|
adamc@50
|
20 match goal with
|
adamc@59
|
21 | [ H : _ |- _ ] => f H
|
adamc@59
|
22 end.
|
adamc@59
|
23
|
adamc@59
|
24 Ltac inList x ls :=
|
adamc@59
|
25 match ls with
|
adamc@59
|
26 | x => idtac
|
adamc@84
|
27 | (_, x) => idtac
|
adamc@59
|
28 | (?LS, _) => inList x LS
|
adamc@59
|
29 end.
|
adamc@59
|
30
|
adamc@59
|
31 Ltac app f ls :=
|
adamc@59
|
32 match ls with
|
adamc@59
|
33 | (?LS, ?X) => f X || app f LS || fail 1
|
adamc@59
|
34 | _ => f ls
|
adamc@59
|
35 end.
|
adamc@59
|
36
|
adamc@59
|
37 Ltac all f ls :=
|
adamc@59
|
38 match ls with
|
adamc@59
|
39 | (?LS, ?X) => f X; all f LS
|
adamc@59
|
40 | (_, _) => fail 1
|
adamc@59
|
41 | _ => f ls
|
adamc@59
|
42 end.
|
adamc@59
|
43
|
adamc@59
|
44 Ltac simplHyp invOne :=
|
adamc@59
|
45 match goal with
|
adamc@59
|
46 | [ H : ex _ |- _ ] => destruct H
|
adamc@59
|
47
|
adamc@51
|
48 | [ H : ?F _ = ?F _ |- _ ] => injection H;
|
adamc@51
|
49 match goal with
|
adamc@85
|
50 | [ |- _ = _ -> _ ] => try clear H; intros; try subst
|
adamc@51
|
51 end
|
adamc@51
|
52 | [ H : ?F _ _ = ?F _ _ |- _ ] => injection H;
|
adamc@51
|
53 match goal with
|
adamc@85
|
54 | [ |- _ = _ -> _ = _ -> _ ] => try clear H; intros; try subst
|
adamc@51
|
55 end
|
adamc@59
|
56
|
adamc@66
|
57 | [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst
|
adamc@66
|
58 | [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst
|
adamc@84
|
59 | [ H : ?F _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst
|
adamc@84
|
60 | [ H : ?F _ _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst
|
adamc@84
|
61 | [ H : ?F _ _ _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst
|
adamc@50
|
62 end.
|
adamc@50
|
63
|
adamc@2
|
64 Ltac rewriteHyp :=
|
adamc@2
|
65 match goal with
|
adamc@2
|
66 | [ H : _ |- _ ] => rewrite H
|
adamc@2
|
67 end.
|
adamc@2
|
68
|
adamc@2
|
69 Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *).
|
adamc@2
|
70
|
adamc@2
|
71 Ltac rewriter := autorewrite with cpdt in *; rewriterP.
|
adamc@2
|
72
|
adamc@2
|
73 Hint Rewrite app_ass : cpdt.
|
adamc@2
|
74
|
adamc@59
|
75 Definition done (T : Type) (x : T) := True.
|
adamc@2
|
76
|
adamc@59
|
77 Ltac inster e trace :=
|
adamc@59
|
78 match type of e with
|
adamc@59
|
79 | forall x : _, _ =>
|
adamc@59
|
80 match goal with
|
adamc@59
|
81 | [ H : _ |- _ ] =>
|
adamc@59
|
82 inster (e H) (trace, H)
|
adamc@59
|
83 | _ => fail 2
|
adamc@59
|
84 end
|
adamc@59
|
85 | _ =>
|
adamc@59
|
86 match trace with
|
adamc@59
|
87 | (_, _) =>
|
adamc@59
|
88 match goal with
|
adamc@59
|
89 | [ H : done (trace, _) |- _ ] => fail 1
|
adamc@59
|
90 | _ =>
|
adamc@59
|
91 let T := type of e in
|
adamc@59
|
92 match type of T with
|
adamc@59
|
93 | Prop =>
|
adamc@59
|
94 generalize e; intro;
|
adamc@59
|
95 assert (done (trace, tt)); [constructor | idtac]
|
adamc@59
|
96 | _ =>
|
adamc@59
|
97 all ltac:(fun X =>
|
adamc@59
|
98 match goal with
|
adamc@59
|
99 | [ H : done (_, X) |- _ ] => fail 1
|
adamc@59
|
100 | _ => idtac
|
adamc@59
|
101 end) trace;
|
adamc@59
|
102 let i := fresh "i" in (pose (i := e);
|
adamc@59
|
103 assert (done (trace, i)); [constructor | idtac])
|
adamc@59
|
104 end
|
adamc@59
|
105 end
|
adamc@59
|
106 end
|
adamc@59
|
107 end.
|
adamc@59
|
108
|
adamc@65
|
109 Ltac un_done :=
|
adamc@65
|
110 repeat match goal with
|
adamc@65
|
111 | [ H : done _ |- _ ] => clear H
|
adamc@65
|
112 end.
|
adamc@65
|
113
|
adamc@88
|
114 Ltac crush' lemmas invOne :=
|
adamc@66
|
115 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence
|
adamc@59
|
116 in (sintuition; rewriter;
|
adamc@88
|
117 match lemmas with
|
adamc@88
|
118 | false => idtac
|
adamc@88
|
119 | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
|
adamc@86
|
120 repeat (simplHyp invOne; intuition)); un_done
|
adamc@86
|
121 end; sintuition; try omega; try (elimtype False; omega)).
|
adamc@59
|
122
|
adamc@88
|
123 Ltac crush := crush' false fail.
|
adamc@85
|
124
|
adamc@85
|
125 Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Prop),
|
adamc@85
|
126 (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with
|
adamc@85
|
127 | refl_equal => v'
|
adamc@85
|
128 end))
|
adamc@85
|
129 -> P v.
|
adamc@85
|
130 intros.
|
adamc@85
|
131 generalize (H _ v (refl_equal _)); trivial.
|
adamc@85
|
132 Qed.
|
adamc@85
|
133
|
adamc@85
|
134 Ltac dep_destruct E :=
|
adamc@85
|
135 let doit A :=
|
adamc@85
|
136 let T := type of A in
|
adamc@85
|
137 generalize dependent E;
|
adamc@85
|
138 let e := fresh "e" in
|
adamc@85
|
139 intro e; pattern e;
|
adamc@85
|
140 apply (@dep_destruct T);
|
adamc@85
|
141 let x := fresh "x" with v := fresh "v" in
|
adamc@85
|
142 intros x v; destruct v; crush;
|
adamc@85
|
143 let bestEffort Heq E tac :=
|
adamc@85
|
144 repeat match goal with
|
adamc@85
|
145 | [ H : context[E] |- _ ] =>
|
adamc@85
|
146 match H with
|
adamc@85
|
147 | Heq => fail 1
|
adamc@85
|
148 | _ => generalize dependent H
|
adamc@85
|
149 end
|
adamc@85
|
150 end;
|
adamc@85
|
151 generalize Heq; tac Heq; clear Heq; intro Heq;
|
adamc@85
|
152 rewrite (UIP_refl _ _ Heq); intros in
|
adamc@85
|
153 repeat match goal with
|
adamc@85
|
154 | [ Heq : ?X = ?X |- _ ] =>
|
adamc@85
|
155 generalize (UIP_refl _ _ Heq); intro; subst; clear Heq
|
adamc@85
|
156 | [ Heq : ?E = _ |- _ ] => bestEffort Heq E ltac:(fun E => rewrite E)
|
adamc@85
|
157 | [ Heq : _ = ?E |- _ ] => bestEffort Heq E ltac:(fun E => rewrite <- E)
|
adamc@85
|
158 end
|
adamc@85
|
159 in match type of E with
|
adamc@85
|
160 | _ _ ?A => doit A
|
adamc@85
|
161 | _ ?A => doit A
|
adamc@85
|
162 end.
|