adam@389: (* Copyright (c) 2008-2012, Adam Chlipala adamc@2: * adamc@2: * This work is licensed under a adamc@2: * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 adamc@2: * Unported License. adamc@2: * The license text is available at: adamc@2: * http://creativecommons.org/licenses/by-nc-nd/3.0/ adamc@2: *) adamc@2: adam@574: Require Import Eqdep List Lia. adamc@38: adamc@59: Set Implicit Arguments. adamc@59: adamc@2: adam@389: (** 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: Ltac inject H := injection H; clear H; intros; try subst. adamc@51: adam@389: (** Try calling tactic function [f] on all hypotheses, keeping the first application that doesn't fail. *) adamc@59: Ltac appHyps f := adamc@50: match goal with adamc@59: | [ H : _ |- _ ] => f H adamc@59: end. adamc@59: adam@389: (** Succeed iff [x] is in the list [ls], represented with left-associated nested tuples. *) adamc@59: Ltac inList x ls := adamc@59: match ls with adamc@59: | x => idtac adamc@84: | (_, x) => idtac adamc@59: | (?LS, _) => inList x LS adamc@59: end. adamc@59: adam@389: (** Try calling tactic function [f] on every element of tupled list [ls], keeping the first call not to fail. *) adamc@59: Ltac app f ls := adamc@59: match ls with adamc@59: | (?LS, ?X) => f X || app f LS || fail 1 adamc@59: | _ => f ls adamc@59: end. adamc@59: adam@389: (** Run [f] on every element of [ls], not just the first that doesn't fail. *) adamc@59: Ltac all f ls := adamc@59: match ls with adamc@59: | (?LS, ?X) => f X; all f LS adamc@59: | (_, _) => fail 1 adamc@59: | _ => f ls adamc@59: end. adamc@59: adam@389: (** Workhorse tactic to simplify hypotheses for a variety of proofs. adam@389: * Argument [invOne] is a tuple-list of predicates for which we always do inversion automatically. *) adamc@59: Ltac simplHyp invOne := adam@389: (** Helper function to do inversion on certain hypotheses, where [H] is the hypothesis and [F] its head symbol *) adamc@99: let invert H F := adam@389: (** We only proceed for those predicates in [invOne]. *) adam@389: inList F invOne; adam@389: (** This case covers an inversion that succeeds immediately, meaning no constructors of [F] applied. *) adam@389: (inversion H; fail) adam@389: (** Otherwise, we only proceed if inversion eliminates all but one constructor case. *) adam@389: || (inversion H; [idtac]; clear H; try subst) in adam@389: adamc@59: match goal with adam@389: (** Eliminate all existential hypotheses. *) adamc@59: | [ H : ex _ |- _ ] => destruct H adamc@59: adam@389: (** Find opportunities to take advantage of injectivity of data constructors, for several different arities. *) adamc@204: | [ H : ?F ?X = ?F ?Y |- ?G ] => adam@389: (** This first branch of the [||] fails the whole attempt iff the arguments of the constructor applications are already easy to prove equal. *) adamc@204: (assert (X = Y); [ assumption | fail 1 ]) adam@389: (** If we pass that filter, then we use injection on [H] and do some simplification as in [inject]. adam@389: * 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: || (injection H; adamc@204: match goal with adamc@204: | [ |- X = Y -> G ] => adamc@204: try clear H; intros; try subst adamc@204: end) adamc@204: | [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] => adamc@204: (assert (X = Y); [ assumption adamc@204: | assert (U = V); [ assumption | fail 1 ] ]) adamc@204: || (injection H; adamc@204: match goal with adamc@204: | [ |- U = V -> X = Y -> G ] => adamc@204: try clear H; intros; try subst adamc@204: end) adamc@59: adam@389: (** Consider some different arities of a predicate [F] in a hypothesis that we might want to invert. *) adamc@99: | [ H : ?F _ |- _ ] => invert H F adamc@99: | [ H : ?F _ _ |- _ ] => invert H F adamc@99: | [ H : ?F _ _ _ |- _ ] => invert H F adamc@99: | [ H : ?F _ _ _ _ |- _ ] => invert H F adamc@99: | [ H : ?F _ _ _ _ _ |- _ ] => invert H F adamc@176: adam@389: (** Use an (axiom-dependent!) inversion principle for dependent pairs, from the standard library. *) adamc@176: | [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H adam@389: adam@389: (** If we're not ready to use that principle yet, try the standard inversion, which often enables the previous rule. *) adamc@176: | [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H adamc@179: adam@389: (** 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: | [ H : Some _ = Some _ |- _ ] => injection H; clear H adamc@50: end. adamc@50: adam@389: (** Find some hypothesis to rewrite with, ensuring that [auto] proves all of the extra subgoals added by [rewrite]. *) adamc@2: Ltac rewriteHyp := adamc@2: match goal with adam@389: | [ H : _ |- _ ] => rewrite H by solve [ auto ] adamc@2: end. adamc@2: adam@389: (** Combine [autorewrite] with automatic hypothesis rewrites. *) adam@375: Ltac rewriterP := repeat (rewriteHyp; autorewrite with core in *). adam@375: Ltac rewriter := autorewrite with core in *; rewriterP. adamc@2: adam@389: (** This one is just so darned useful, let's add it as a hint here. *) adam@375: Hint Rewrite app_ass. adamc@2: adam@389: (** Devious marker predicate to use for encoding state within proof goals *) adamc@59: Definition done (T : Type) (x : T) := True. adamc@2: adam@389: (** Try a new instantiation of a universally quantified fact, proved by [e]. adam@389: * [trace] is an accumulator recording which instantiations we choose. *) adamc@59: Ltac inster e trace := adam@389: (** Does [e] have any quantifiers left? *) adamc@59: match type of e with adamc@59: | forall x : _, _ => adam@389: (** Yes, so let's pick the first context variable of the right type. *) adamc@59: match goal with adamc@59: | [ H : _ |- _ ] => adamc@59: inster (e H) (trace, H) adamc@59: | _ => fail 2 adamc@59: end adamc@59: | _ => adam@389: (** No more quantifiers, so now we check if the trace we computed was already used. *) adamc@59: match trace with adamc@59: | (_, _) => adam@389: (** We only reach this case if the trace is nonempty, ensuring that [inster] fails if no progress can be made. *) adamc@59: match goal with adam@389: | [ H : done (trace, _) |- _ ] => adam@389: (** Uh oh, found a record of this trace in the context! Abort to backtrack to try another trace. *) adam@389: fail 1 adamc@59: | _ => adam@389: (** What is the type of the proof [e] now? *) adamc@59: let T := type of e in adamc@59: match type of T with adamc@59: | Prop => adam@389: (** [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: generalize e; intro; adam@389: assert (done (trace, tt)) by constructor adamc@59: | _ => adam@389: (** [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: all ltac:(fun X => adamc@59: match goal with adamc@59: | [ H : done (_, X) |- _ ] => fail 1 adamc@59: | _ => idtac adamc@59: end) trace; adam@389: (** Pick a new name for our new instantiation. *) adamc@59: let i := fresh "i" in (pose (i := e); adam@389: assert (done (trace, i)) by constructor) adamc@59: end adamc@59: end adamc@59: end adamc@59: end. adamc@59: adam@389: (** 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: Ltac un_done := adamc@65: repeat match goal with adamc@65: | [ H : done _ |- _ ] => clear H adamc@65: end. adamc@65: adam@297: Require Import JMeq. adam@297: adam@389: (** A more parameterized version of the famous [crush]. Extra arguments are: adam@389: * - A tuple-list of lemmas we try [inster]-ing adam@389: * - A tuple-list of predicates we try inversion for *) adamc@88: Ltac crush' lemmas invOne := adam@389: (** A useful combination of standard automation *) adam@389: let sintuition := simpl in *; intuition; try subst; adam@389: repeat (simplHyp invOne; intuition; try subst); try congruence in adamc@59: adam@389: (** A fancier version of [rewriter] from above, which uses [crush'] to discharge side conditions *) adam@389: let rewriter := autorewrite with core in *; adam@389: repeat (match goal with adam@389: | [ H : ?P |- _ ] => adam@389: match P with adam@389: | context[JMeq] => fail 1 (** JMeq is too fancy to deal with here. *) adam@389: | _ => rewrite H by crush' lemmas invOne adam@389: end adam@389: end; autorewrite with core in *) in adam@389: adam@389: (** Now the main sequence of heuristics: *) adam@389: (sintuition; rewriter; adam@389: match lemmas with adam@389: | false => idtac (** No lemmas? Nothing to do here *) adam@389: | _ => adam@389: (** Try a loop of instantiating lemmas... *) adam@389: repeat ((app ltac:(fun L => inster L L) lemmas adam@389: (** ...or instantiating hypotheses... *) adam@389: || appHyps ltac:(fun L => inster L L)); adam@389: (** ...and then simplifying hypotheses. *) adam@389: repeat (simplHyp invOne; intuition)); un_done adam@389: end; adam@389: sintuition; rewriter; sintuition; adam@574: (** End with a last attempt to prove an arithmetic fact with [lia], or prove any sort of fact in a context that is contradictory by reasoning that [lia] can do. *) adam@574: try lia; try (elimtype False; lia)). adam@389: adam@389: (** [crush] instantiates [crush'] with the simplest possible parameters. *) adamc@88: Ltac crush := crush' false fail. adamc@85: adam@389: (** * Wrap Program's [dependent destruction] in a slightly more pleasant form *) adam@389: adamc@213: Require Import Program.Equality. adamc@85: adam@389: (** Run [dependent destruction] on [E] and look for opportunities to simplify the result. adam@389: 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: Ltac dep_destruct E := adamc@213: let x := fresh "x" in adamc@213: remember E as x; simpl in x; dependent destruction x; adamc@213: try match goal with adam@417: | [ H : _ = E |- _ ] => try rewrite <- H in *; clear H adamc@213: end. adamc@118: adam@389: (** Nuke all hypotheses that we can get away with, without invalidating the goal statement. *) adamc@118: Ltac clear_all := adamc@118: repeat match goal with adamc@118: | [ H : _ |- _ ] => clear H adamc@118: end. adamc@256: adam@389: (** 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: * Also prove the lefthand sides of any implications that this exposes, simplifying [H] to leave out those implications. *) adamc@262: Ltac guess v H := adamc@256: repeat match type of H with adamc@256: | forall x : ?T, _ => adamc@256: match type of T with adamc@256: | Prop => adamc@256: (let H' := fresh "H'" in adamc@256: assert (H' : T); [ adamc@262: solve [ eauto 6 ] adam@389: | specialize (H H'); clear H' ]) adamc@256: || fail 1 adamc@256: | _ => adam@389: specialize (H v) adamc@262: || let x := fresh "x" in adamc@256: evar (x : T); adam@389: let x' := eval unfold x in x in adam@389: clear x; specialize (H x') adamc@256: end adamc@256: end. adamc@256: adam@389: (** Version of [guess] that leaves the original [H] intact *) adamc@262: Ltac guessKeep v H := adamc@256: let H' := fresh "H'" in adamc@262: generalize H; intro H'; guess v H'.