adam@389
|
1 (* Copyright (c) 2008-2012, 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
|
adam@389
|
17 (** A version of [injection] that does some standard simplifications afterward: clear the hypothesis in question, bring the new facts above the double line, and attempt substitution for known variables. *)
|
adamc@66
|
18 Ltac inject H := injection H; clear H; intros; try subst.
|
adamc@51
|
19
|
adam@389
|
20 (** Try calling tactic function [f] on all hypotheses, keeping the first application that doesn't fail. *)
|
adamc@59
|
21 Ltac appHyps f :=
|
adamc@50
|
22 match goal with
|
adamc@59
|
23 | [ H : _ |- _ ] => f H
|
adamc@59
|
24 end.
|
adamc@59
|
25
|
adam@389
|
26 (** Succeed iff [x] is in the list [ls], represented with left-associated nested tuples. *)
|
adamc@59
|
27 Ltac inList x ls :=
|
adamc@59
|
28 match ls with
|
adamc@59
|
29 | x => idtac
|
adamc@84
|
30 | (_, x) => idtac
|
adamc@59
|
31 | (?LS, _) => inList x LS
|
adamc@59
|
32 end.
|
adamc@59
|
33
|
adam@389
|
34 (** Try calling tactic function [f] on every element of tupled list [ls], keeping the first call not to fail. *)
|
adamc@59
|
35 Ltac app f ls :=
|
adamc@59
|
36 match ls with
|
adamc@59
|
37 | (?LS, ?X) => f X || app f LS || fail 1
|
adamc@59
|
38 | _ => f ls
|
adamc@59
|
39 end.
|
adamc@59
|
40
|
adam@389
|
41 (** Run [f] on every element of [ls], not just the first that doesn't fail. *)
|
adamc@59
|
42 Ltac all f ls :=
|
adamc@59
|
43 match ls with
|
adamc@59
|
44 | (?LS, ?X) => f X; all f LS
|
adamc@59
|
45 | (_, _) => fail 1
|
adamc@59
|
46 | _ => f ls
|
adamc@59
|
47 end.
|
adamc@59
|
48
|
adam@389
|
49 (** Workhorse tactic to simplify hypotheses for a variety of proofs.
|
adam@389
|
50 * Argument [invOne] is a tuple-list of predicates for which we always do inversion automatically. *)
|
adamc@59
|
51 Ltac simplHyp invOne :=
|
adam@389
|
52 (** Helper function to do inversion on certain hypotheses, where [H] is the hypothesis and [F] its head symbol *)
|
adamc@99
|
53 let invert H F :=
|
adam@389
|
54 (** We only proceed for those predicates in [invOne]. *)
|
adam@389
|
55 inList F invOne;
|
adam@389
|
56 (** This case covers an inversion that succeeds immediately, meaning no constructors of [F] applied. *)
|
adam@389
|
57 (inversion H; fail)
|
adam@389
|
58 (** Otherwise, we only proceed if inversion eliminates all but one constructor case. *)
|
adam@389
|
59 || (inversion H; [idtac]; clear H; try subst) in
|
adam@389
|
60
|
adamc@59
|
61 match goal with
|
adam@389
|
62 (** Eliminate all existential hypotheses. *)
|
adamc@59
|
63 | [ H : ex _ |- _ ] => destruct H
|
adamc@59
|
64
|
adam@389
|
65 (** Find opportunities to take advantage of injectivity of data constructors, for several different arities. *)
|
adamc@204
|
66 | [ H : ?F ?X = ?F ?Y |- ?G ] =>
|
adam@389
|
67 (** This first branch of the [||] fails the whole attempt iff the arguments of the constructor applications are already easy to prove equal. *)
|
adamc@204
|
68 (assert (X = Y); [ assumption | fail 1 ])
|
adam@389
|
69 (** If we pass that filter, then we use injection on [H] and do some simplification as in [inject].
|
adam@389
|
70 * The odd-looking check of the goal form is to avoid cases where [injection] gives a more complex result because of dependent typing, which we aren't equipped to handle here. *)
|
adamc@204
|
71 || (injection H;
|
adamc@204
|
72 match goal with
|
adamc@204
|
73 | [ |- X = Y -> G ] =>
|
adamc@204
|
74 try clear H; intros; try subst
|
adamc@204
|
75 end)
|
adamc@204
|
76 | [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] =>
|
adamc@204
|
77 (assert (X = Y); [ assumption
|
adamc@204
|
78 | assert (U = V); [ assumption | fail 1 ] ])
|
adamc@204
|
79 || (injection H;
|
adamc@204
|
80 match goal with
|
adamc@204
|
81 | [ |- U = V -> X = Y -> G ] =>
|
adamc@204
|
82 try clear H; intros; try subst
|
adamc@204
|
83 end)
|
adamc@59
|
84
|
adam@389
|
85 (** Consider some different arities of a predicate [F] in a hypothesis that we might want to invert. *)
|
adamc@99
|
86 | [ H : ?F _ |- _ ] => invert H F
|
adamc@99
|
87 | [ H : ?F _ _ |- _ ] => invert H F
|
adamc@99
|
88 | [ H : ?F _ _ _ |- _ ] => invert H F
|
adamc@99
|
89 | [ H : ?F _ _ _ _ |- _ ] => invert H F
|
adamc@99
|
90 | [ H : ?F _ _ _ _ _ |- _ ] => invert H F
|
adamc@176
|
91
|
adam@389
|
92 (** Use an (axiom-dependent!) inversion principle for dependent pairs, from the standard library. *)
|
adamc@176
|
93 | [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H
|
adam@389
|
94
|
adam@389
|
95 (** If we're not ready to use that principle yet, try the standard inversion, which often enables the previous rule. *)
|
adamc@176
|
96 | [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H
|
adamc@179
|
97
|
adam@389
|
98 (** Similar logic to the cases for constructor injectivity above, but specialized to [Some], since the above cases won't deal with polymorphic constructors. *)
|
adamc@179
|
99 | [ H : Some _ = Some _ |- _ ] => injection H; clear H
|
adamc@50
|
100 end.
|
adamc@50
|
101
|
adam@389
|
102 (** Find some hypothesis to rewrite with, ensuring that [auto] proves all of the extra subgoals added by [rewrite]. *)
|
adamc@2
|
103 Ltac rewriteHyp :=
|
adamc@2
|
104 match goal with
|
adam@389
|
105 | [ H : _ |- _ ] => rewrite H by solve [ auto ]
|
adamc@2
|
106 end.
|
adamc@2
|
107
|
adam@389
|
108 (** Combine [autorewrite] with automatic hypothesis rewrites. *)
|
adam@375
|
109 Ltac rewriterP := repeat (rewriteHyp; autorewrite with core in *).
|
adam@375
|
110 Ltac rewriter := autorewrite with core in *; rewriterP.
|
adamc@2
|
111
|
adam@389
|
112 (** This one is just so darned useful, let's add it as a hint here. *)
|
adam@375
|
113 Hint Rewrite app_ass.
|
adamc@2
|
114
|
adam@389
|
115 (** Devious marker predicate to use for encoding state within proof goals *)
|
adamc@59
|
116 Definition done (T : Type) (x : T) := True.
|
adamc@2
|
117
|
adam@389
|
118 (** Try a new instantiation of a universally quantified fact, proved by [e].
|
adam@389
|
119 * [trace] is an accumulator recording which instantiations we choose. *)
|
adamc@59
|
120 Ltac inster e trace :=
|
adam@389
|
121 (** Does [e] have any quantifiers left? *)
|
adamc@59
|
122 match type of e with
|
adamc@59
|
123 | forall x : _, _ =>
|
adam@389
|
124 (** Yes, so let's pick the first context variable of the right type. *)
|
adamc@59
|
125 match goal with
|
adamc@59
|
126 | [ H : _ |- _ ] =>
|
adamc@59
|
127 inster (e H) (trace, H)
|
adamc@59
|
128 | _ => fail 2
|
adamc@59
|
129 end
|
adamc@59
|
130 | _ =>
|
adam@389
|
131 (** No more quantifiers, so now we check if the trace we computed was already used. *)
|
adamc@59
|
132 match trace with
|
adamc@59
|
133 | (_, _) =>
|
adam@389
|
134 (** We only reach this case if the trace is nonempty, ensuring that [inster] fails if no progress can be made. *)
|
adamc@59
|
135 match goal with
|
adam@389
|
136 | [ H : done (trace, _) |- _ ] =>
|
adam@389
|
137 (** Uh oh, found a record of this trace in the context! Abort to backtrack to try another trace. *)
|
adam@389
|
138 fail 1
|
adamc@59
|
139 | _ =>
|
adam@389
|
140 (** What is the type of the proof [e] now? *)
|
adamc@59
|
141 let T := type of e in
|
adamc@59
|
142 match type of T with
|
adamc@59
|
143 | Prop =>
|
adam@389
|
144 (** [e] should be thought of as a proof, so let's add it to the context, and also add a new marker hypothesis recording our choice of trace. *)
|
adamc@59
|
145 generalize e; intro;
|
adam@389
|
146 assert (done (trace, tt)) by constructor
|
adamc@59
|
147 | _ =>
|
adam@389
|
148 (** [e] is something beside a proof. Better make sure no element of our current trace was generated by a previous call to [inster], or we might get stuck in an infinite loop! (We store previous [inster] terms in second positions of tuples used as arguments to [done] in hypotheses. Proofs instantiated by [inster] merely use [tt] in such positions.) *)
|
adamc@59
|
149 all ltac:(fun X =>
|
adamc@59
|
150 match goal with
|
adamc@59
|
151 | [ H : done (_, X) |- _ ] => fail 1
|
adamc@59
|
152 | _ => idtac
|
adamc@59
|
153 end) trace;
|
adam@389
|
154 (** Pick a new name for our new instantiation. *)
|
adamc@59
|
155 let i := fresh "i" in (pose (i := e);
|
adam@389
|
156 assert (done (trace, i)) by constructor)
|
adamc@59
|
157 end
|
adamc@59
|
158 end
|
adamc@59
|
159 end
|
adamc@59
|
160 end.
|
adamc@59
|
161
|
adam@389
|
162 (** After a round of application with the above, we will have a lot of junk [done] markers to clean up; hence this tactic. *)
|
adamc@65
|
163 Ltac un_done :=
|
adamc@65
|
164 repeat match goal with
|
adamc@65
|
165 | [ H : done _ |- _ ] => clear H
|
adamc@65
|
166 end.
|
adamc@65
|
167
|
adam@297
|
168 Require Import JMeq.
|
adam@297
|
169
|
adam@389
|
170 (** A more parameterized version of the famous [crush]. Extra arguments are:
|
adam@389
|
171 * - A tuple-list of lemmas we try [inster]-ing
|
adam@389
|
172 * - A tuple-list of predicates we try inversion for *)
|
adamc@88
|
173 Ltac crush' lemmas invOne :=
|
adam@389
|
174 (** A useful combination of standard automation *)
|
adam@389
|
175 let sintuition := simpl in *; intuition; try subst;
|
adam@389
|
176 repeat (simplHyp invOne; intuition; try subst); try congruence in
|
adamc@59
|
177
|
adam@389
|
178 (** A fancier version of [rewriter] from above, which uses [crush'] to discharge side conditions *)
|
adam@389
|
179 let rewriter := autorewrite with core in *;
|
adam@389
|
180 repeat (match goal with
|
adam@389
|
181 | [ H : ?P |- _ ] =>
|
adam@389
|
182 match P with
|
adam@389
|
183 | context[JMeq] => fail 1 (** JMeq is too fancy to deal with here. *)
|
adam@389
|
184 | _ => rewrite H by crush' lemmas invOne
|
adam@389
|
185 end
|
adam@389
|
186 end; autorewrite with core in *) in
|
adam@389
|
187
|
adam@389
|
188 (** Now the main sequence of heuristics: *)
|
adam@389
|
189 (sintuition; rewriter;
|
adam@389
|
190 match lemmas with
|
adam@389
|
191 | false => idtac (** No lemmas? Nothing to do here *)
|
adam@389
|
192 | _ =>
|
adam@389
|
193 (** Try a loop of instantiating lemmas... *)
|
adam@389
|
194 repeat ((app ltac:(fun L => inster L L) lemmas
|
adam@389
|
195 (** ...or instantiating hypotheses... *)
|
adam@389
|
196 || appHyps ltac:(fun L => inster L L));
|
adam@389
|
197 (** ...and then simplifying hypotheses. *)
|
adam@389
|
198 repeat (simplHyp invOne; intuition)); un_done
|
adam@389
|
199 end;
|
adam@389
|
200 sintuition; rewriter; sintuition;
|
adam@389
|
201 (** End with a last attempt to prove an arithmetic fact with [omega], or prove any sort of fact in a context that is contradictory by reasoning that [omega] can do. *)
|
adam@389
|
202 try omega; try (elimtype False; omega)).
|
adam@389
|
203
|
adam@389
|
204 (** [crush] instantiates [crush'] with the simplest possible parameters. *)
|
adamc@88
|
205 Ltac crush := crush' false fail.
|
adamc@85
|
206
|
adam@389
|
207 (** * Wrap Program's [dependent destruction] in a slightly more pleasant form *)
|
adam@389
|
208
|
adamc@213
|
209 Require Import Program.Equality.
|
adamc@85
|
210
|
adam@389
|
211 (** Run [dependent destruction] on [E] and look for opportunities to simplify the result.
|
adam@389
|
212 The weird introduction of [x] helps get around limitations of [dependent destruction], in terms of which sorts of arguments it will accept (e.g., variables bound to hypotheses within Ltac [match]es). *)
|
adamc@85
|
213 Ltac dep_destruct E :=
|
adamc@213
|
214 let x := fresh "x" in
|
adamc@213
|
215 remember E as x; simpl in x; dependent destruction x;
|
adamc@213
|
216 try match goal with
|
adam@417
|
217 | [ H : _ = E |- _ ] => try rewrite <- H in *; clear H
|
adamc@213
|
218 end.
|
adamc@118
|
219
|
adam@389
|
220 (** Nuke all hypotheses that we can get away with, without invalidating the goal statement. *)
|
adamc@118
|
221 Ltac clear_all :=
|
adamc@118
|
222 repeat match goal with
|
adamc@118
|
223 | [ H : _ |- _ ] => clear H
|
adamc@118
|
224 end.
|
adamc@256
|
225
|
adam@389
|
226 (** Instantiate a quantifier in a hypothesis [H] with value [v], or, if [v] doesn't have the right type, with a new unification variable.
|
adam@389
|
227 * Also prove the lefthand sides of any implications that this exposes, simplifying [H] to leave out those implications. *)
|
adamc@262
|
228 Ltac guess v H :=
|
adamc@256
|
229 repeat match type of H with
|
adamc@256
|
230 | forall x : ?T, _ =>
|
adamc@256
|
231 match type of T with
|
adamc@256
|
232 | Prop =>
|
adamc@256
|
233 (let H' := fresh "H'" in
|
adamc@256
|
234 assert (H' : T); [
|
adamc@262
|
235 solve [ eauto 6 ]
|
adam@389
|
236 | specialize (H H'); clear H' ])
|
adamc@256
|
237 || fail 1
|
adamc@256
|
238 | _ =>
|
adam@389
|
239 specialize (H v)
|
adamc@262
|
240 || let x := fresh "x" in
|
adamc@256
|
241 evar (x : T);
|
adam@389
|
242 let x' := eval unfold x in x in
|
adam@389
|
243 clear x; specialize (H x')
|
adamc@256
|
244 end
|
adamc@256
|
245 end.
|
adamc@256
|
246
|
adam@389
|
247 (** Version of [guess] that leaves the original [H] intact *)
|
adamc@262
|
248 Ltac guessKeep v H :=
|
adamc@256
|
249 let H' := fresh "H'" in
|
adamc@262
|
250 generalize H; intro H'; guess v H'.
|