Mercurial > cpdt > repo

annotate src/CpdtTactics.v @ 409:934945edc6b5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Typesetting pass over Universes
author Adam Chlipala <adam@chlipala.net>
date Fri, 08 Jun 2012 15:00:59 -0400
parents 76e1dfcb86eb
children 539ed97750bb
rev   line source
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
adamc@213 217 | [ H : _ = E |- _ ] => 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'.