Mercurial > cpdt > repo

annotate src/CpdtTactics.v @ 562:36b1f893c1e0

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