Mercurial > cpdt > repo

comparison src/CpdtTactics.v @ 314:d5787b70cf48

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Rename Tactics; change 'principal typing' to 'principal types'
author Adam Chlipala <adam@chlipala.net>
date Wed, 07 Sep 2011 13:47:24 -0400
parents src/Tactics.v@b441010125d4
children d1276004eec9
comparison
equal deleted inserted replaced
313:44f9ca08e173 314:d5787b70cf48
1 (* Copyright (c) 2008-2011, Adam Chlipala
2 *
3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License.
6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *)
9
10 Require Import Eqdep List.
11
12 Require Omega.
13
14 Set Implicit Arguments.
15
16
17 Ltac inject H := injection H; clear H; intros; try subst.
18
19 Ltac appHyps f :=
20 match goal with
21 | [ H : _ |- _ ] => f H
22 end.
23
24 Ltac inList x ls :=
25 match ls with
26 | x => idtac
27 | (_, x) => idtac
28 | (?LS, _) => inList x LS
29 end.
30
31 Ltac app f ls :=
32 match ls with
33 | (?LS, ?X) => f X || app f LS || fail 1
34 | _ => f ls
35 end.
36
37 Ltac all f ls :=
38 match ls with
39 | (?LS, ?X) => f X; all f LS
40 | (_, _) => fail 1
41 | _ => f ls
42 end.
43
44 Ltac simplHyp invOne :=
45 let invert H F :=
46 inList F invOne; (inversion H; fail)
47 || (inversion H; [idtac]; clear H; try subst) in
48 match goal with
49 | [ H : ex _ |- _ ] => destruct H
50
51 | [ H : ?F ?X = ?F ?Y |- ?G ] =>
52 (assert (X = Y); [ assumption | fail 1 ])
53 || (injection H;
54 match goal with
55 | [ |- X = Y -> G ] =>
56 try clear H; intros; try subst
57 end)
58 | [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] =>
59 (assert (X = Y); [ assumption
60 | assert (U = V); [ assumption | fail 1 ] ])
61 || (injection H;
62 match goal with
63 | [ |- U = V -> X = Y -> G ] =>
64 try clear H; intros; try subst
65 end)
66
67 | [ H : ?F _ |- _ ] => invert H F
68 | [ H : ?F _ _ |- _ ] => invert H F
69 | [ H : ?F _ _ _ |- _ ] => invert H F
70 | [ H : ?F _ _ _ _ |- _ ] => invert H F
71 | [ H : ?F _ _ _ _ _ |- _ ] => invert H F
72
73 | [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H
74 | [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H
75
76 | [ H : Some _ = Some _ |- _ ] => injection H; clear H
77 end.
78
79 Ltac rewriteHyp :=
80 match goal with
81 | [ H : _ |- _ ] => rewrite H; auto; [idtac]
82 end.
83
84 Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *).
85
86 Ltac rewriter := autorewrite with cpdt in *; rewriterP.
87
88 Hint Rewrite app_ass : cpdt.
89
90 Definition done (T : Type) (x : T) := True.
91
92 Ltac inster e trace :=
93 match type of e with
94 | forall x : _, _ =>
95 match goal with
96 | [ H : _ |- _ ] =>
97 inster (e H) (trace, H)
98 | _ => fail 2
99 end
100 | _ =>
101 match trace with
102 | (_, _) =>
103 match goal with
104 | [ H : done (trace, _) |- _ ] => fail 1
105 | _ =>
106 let T := type of e in
107 match type of T with
108 | Prop =>
109 generalize e; intro;
110 assert (done (trace, tt)); [constructor | idtac]
111 | _ =>
112 all ltac:(fun X =>
113 match goal with
114 | [ H : done (_, X) |- _ ] => fail 1
115 | _ => idtac
116 end) trace;
117 let i := fresh "i" in (pose (i := e);
118 assert (done (trace, i)); [constructor | idtac])
119 end
120 end
121 end
122 end.
123
124 Ltac un_done :=
125 repeat match goal with
126 | [ H : done _ |- _ ] => clear H
127 end.
128
129 Require Import JMeq.
130
131 Ltac crush' lemmas invOne :=
132 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in
133 let rewriter := autorewrite with cpdt in *;
134 repeat (match goal with
135 | [ H : ?P |- _ ] =>
136 match P with
137 | context[JMeq] => fail 1
138 | _ => (rewrite H; [])
139 || (rewrite H; [ | solve [ crush' lemmas invOne ] ])
140 || (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ])
141 end
142 end; autorewrite with cpdt in *)
143 in (sintuition; rewriter;
144 match lemmas with
145 | false => idtac
146 | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
147 repeat (simplHyp invOne; intuition)); un_done
148 end; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)).
149
150 Ltac crush := crush' false fail.
151
152 Require Import Program.Equality.
153
154 Ltac dep_destruct E :=
155 let x := fresh "x" in
156 remember E as x; simpl in x; dependent destruction x;
157 try match goal with
158 | [ H : _ = E |- _ ] => rewrite <- H in *; clear H
159 end.
160
161 Ltac clear_all :=
162 repeat match goal with
163 | [ H : _ |- _ ] => clear H
164 end.
165
166 Ltac guess v H :=
167 repeat match type of H with
168 | forall x : ?T, _ =>
169 match type of T with
170 | Prop =>
171 (let H' := fresh "H'" in
172 assert (H' : T); [
173 solve [ eauto 6 ]
174 | generalize (H H'); clear H H'; intro H ])
175 || fail 1
176 | _ =>
177 (generalize (H v); clear H; intro H)
178 || let x := fresh "x" in
179 evar (x : T);
180 let x' := eval cbv delta [x] in x in
181 clear x; generalize (H x'); clear H; intro H
182 end
183 end.
184
185 Ltac guessKeep v H :=
186 let H' := fresh "H'" in
187 generalize H; intro H'; guess v H'.