## Mercurial > cpdt > repo

### annotate src/CpdtTactics.v @ 561:c800306b0e32

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Two more users

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Fri, 10 Nov 2017 19:02:44 -0500 |

parents | ed829eaa91b2 |

children |

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'. |