CpdtTactics

~~~~~~~~~~~ BSD LICENSE ~~~~~~~~~~~
Copyright (c) 2006-2013, Adam Chlipala All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
  • Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
  • Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
  • The names of contributors may not be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

Require Import Eqdep List.

Require Export Coq.omega.Omega.

Set Implicit Arguments.

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.
Ltac inject H := injection H; clear H; intros; try subst.

Try calling tactic function f on all hypotheses, keeping the first application that doesn't fail.
Ltac appHyps f :=
  match goal with
    | [ H : _ |- _ ] => f H
  end.

Succeed iff x is in the list ls, represented with left-associated nested tuples.
Ltac inList x ls :=
  match ls with
    | x => idtac
    | (_, x) => idtac
    | (?LS, _) => inList x LS
  end.

Try calling tactic function f on every element of tupled list ls, keeping the first call not to fail.
Ltac app f ls :=
  match ls with
    | (?LS, ?X) => f X || app f LS || fail 1
    | _ => f ls
  end.

Run f on every element of ls, not just the first that doesn't fail.
Ltac all f ls :=
  match ls with
    | (?LS, ?X) => f X; all f LS
    | (_, _) => fail 1
    | _ => f ls
  end.

Workhorse tactic to simplify hypotheses for a variety of proofs. Argument invOne is a tuple-list of predicates for which we always do inversion automatically.
Ltac simplHyp invOne :=
  
Helper function to do inversion on certain hypotheses, where H is the hypothesis and F its head symbol
  let invert H F :=
    
We only proceed for those predicates in invOne.
    inList F invOne;
    
This case covers an inversion that succeeds immediately, meaning no constructors of F applied.
      (inversion H; fail)
    
Otherwise, we only proceed if inversion eliminates all but one constructor case.
      || (inversion H; [idtac]; clear H; try subst) in

  match goal with
    
Eliminate all existential hypotheses.
    | [ H : ex _ |- _ ] => destruct H

    
Find opportunities to take advantage of injectivity of data constructors, for several different arities.
    | [ H : ?F ?X = ?F ?Y |- ?G ] =>
      
This first branch of the || fails the whole attempt iff the arguments of the constructor applications are already easy to prove equal.
      (assert (X = Y); [ assumption | fail 1 ])
      
If we pass that filter, then we use injection on H and do some simplification as in inject. 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.
      || (injection H;
        match goal with
          | [ |- X = Y -> G ] =>
            try clear H; intros; try subst
        end)
    | [ H : ?F ?X ?U = ?F ?Y ?V |- ?G ] =>
      (assert (X = Y); [ assumption
        | assert (U = V); [ assumption | fail 1 ] ])
      || (injection H;
        match goal with
          | [ |- U = V -> X = Y -> G ] =>
            try clear H; intros; try subst
        end)

    
Consider some different arities of a predicate F in a hypothesis that we might want to invert.
    | [ H : ?F _ |- _ ] => invert H F
    | [ H : ?F _ _ |- _ ] => invert H F
    | [ H : ?F _ _ _ |- _ ] => invert H F
    | [ H : ?F _ _ _ _ |- _ ] => invert H F
    | [ H : ?F _ _ _ _ _ |- _ ] => invert H F

    
Use an (axiom-dependent!) inversion principle for dependent pairs, from the standard library.
    | [ H : existT _ ?T _ = existT _ ?T _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H

    
If we're not ready to use that principle yet, try the standard inversion, which often enables the previous rule.
    | [ H : existT _ _ _ = existT _ _ _ |- _ ] => inversion H; clear H

    
Similar logic to the cases for constructor injectivity above, but specialized to Some, since the above cases won't deal with polymorphic constructors.
    | [ H : Some _ = Some _ |- _ ] => injection H; clear H
  end.

Find some hypothesis to rewrite with, ensuring that auto proves all of the extra subgoals added by rewrite.
Ltac rewriteHyp :=
  match goal with
    | [ H : _ |- _ ] => rewrite H by solve [ auto ]
  end.

Combine autorewrite with automatic hypothesis rewrites.
Ltac rewriterP := repeat (rewriteHyp; autorewrite with core in *).
Ltac rewriter := autorewrite with core in *; rewriterP.

This one is just so darned useful, let's add it as a hint here.
Hint Rewrite app_ass.

Devious marker predicate to use for encoding state within proof goals
Definition done (T : Type) (x : T) := True.

Try a new instantiation of a universally quantified fact, proved by e. trace is an accumulator recording which instantiations we choose.
Ltac inster e trace :=
  
Does e have any quantifiers left?
  match type of e with
    | forall x : _, _ =>
      
Yes, so let's pick the first context variable of the right type.
      match goal with
        | [ H : _ |- _ ] =>
          inster (e H) (trace, H)
        | _ => fail 2
      end
    | _ =>
      
No more quantifiers, so now we check if the trace we computed was already used.
      match trace with
        | (_, _) =>
          
We only reach this case if the trace is nonempty, ensuring that inster fails if no progress can be made.
          match goal with
            | [ H : done (trace, _) |- _ ] =>
              
Uh oh, found a record of this trace in the context! Abort to backtrack to try another trace.
              fail 1
            | _ =>
              
What is the type of the proof e now?
              let T := type of e in
                match type of T with
                  | Prop =>
                    
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.
                    generalize e; intro;
                      assert (done (trace, tt)) by constructor
                  | _ =>
                    
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.)
                    all ltac:(fun X =>
                      match goal with
                        | [ H : done (_, X) |- _ ] => fail 1
                        | _ => idtac
                      end) trace;
                    
Pick a new name for our new instantiation.
                    let i := fresh "i" in (pose (i := e);
                      assert (done (trace, i)) by constructor)
                end
          end
      end
  end.

After a round of application with the above, we will have a lot of junk done markers to clean up; hence this tactic.
Ltac un_done :=
  repeat match goal with
           | [ H : done _ |- _ ] => clear H
         end.

Require Import JMeq.

A more parameterized version of the famous crush. Extra arguments are:
  • A tuple-list of lemmas we try inster-ing
  • A tuple-list of predicates we try inversion for
Ltac crush' lemmas invOne :=
  
A useful combination of standard automation
  let sintuition := simpl in *; intuition; try subst;
    repeat (simplHyp invOne; intuition; try subst); try congruence in

  
A fancier version of rewriter from above, which uses crush' to discharge side conditions
  let rewriter := autorewrite with core in *;
    repeat (match goal with
              | [ H : ?P |- _ ] =>
                match P with
                  | context[JMeq] => fail 1
JMeq is too fancy to deal with here.
                  | _ => rewrite H by crush' lemmas invOne
                end
            end; autorewrite with core in *) in

  
Now the main sequence of heuristics:
    (sintuition; rewriter;
      match lemmas with
        | false => idtac
No lemmas? Nothing to do here
        | _ =>
          
Try a loop of instantiating lemmas...
          repeat ((app ltac:(fun L => inster L L) lemmas
          
...or instantiating hypotheses...
            || appHyps ltac:(fun L => inster L L));
          
...and then simplifying hypotheses.
          repeat (simplHyp invOne; intuition)); un_done
      end;
      sintuition; rewriter; sintuition;
      
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.
      try omega; try (elimtype False; omega)).

crush instantiates crush' with the simplest possible parameters.
Ltac crush := crush' false fail.

Wrap Program's dependent destruction in a slightly more pleasant form

Require Import Program.Equality.

Run dependent destruction on E and look for opportunities to simplify the result. 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 matches).
Ltac dep_destruct E :=
  let x := fresh "x" in
    remember E as x; simpl in x; dependent destruction x;
      try match goal with
            | [ H : _ = E |- _ ] => try rewrite <- H in *; clear H
          end.

Nuke all hypotheses that we can get away with, without invalidating the goal statement.
Ltac clear_all :=
  repeat match goal with
           | [ H : _ |- _ ] => clear H
         end.

Instantiate a quantifier in a hypothesis H with value v, or, if v doesn't have the right type, with a new unification variable. Also prove the lefthand sides of any implications that this exposes, simplifying H to leave out those implications.
Ltac guess v H :=
  repeat match type of H with
           | forall x : ?T, _ =>
             match type of T with
               | Prop =>
                 (let H' := fresh "H'" in
                   assert (H' : T); [
                     solve [ eauto 6 ]
                     | specialize (H H'); clear H' ])
                 || fail 1
               | _ =>
                 specialize (H v)
                 || let x := fresh "x" in
                   evar (x : T);
                   let x' := eval unfold x in x in
                     clear x; specialize (H x')
             end
         end.

Version of guess that leaves the original H intact
Ltac guessKeep v H :=
  let H' := fresh "H'" in
    generalize H; intro H'; guess v H'.

Create HintDb X_Lib.

Ltac smack := try autorewrite with X_Lib in *; crush; eauto.