# Library CpdtTactics

(* Copyright (c) 2008-2012, Adam Chlipala

*

* This work is licensed under a

* Creative Commons Attribution-Noncommercial-No Derivative Works 3.0

* Unported License.

* The license text is available at:

* http://creativecommons.org/licenses/by-nc-nd/3.0/

*)

Require Import Eqdep List.

Require Omega.

Set Implicit Arguments.

*

* This work is licensed under a

* Creative Commons Attribution-Noncommercial-No Derivative Works 3.0

* Unported License.

* The license text is available at:

* http://creativecommons.org/licenses/by-nc-nd/3.0/

*)

Require Import Eqdep List.

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

match goal with

| [ H : _ |- _ ] => f H

end.

Succeed iff x is in the list ls, represented with left-associated nested tuples.

Try calling tactic function f on every element of tupled list ls, keeping the first call not to fail.

Run f on every element of ls, not just the first that doesn't fail.

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

match goal with

Eliminate all existential hypotheses.

Find opportunities to take advantage of injectivity of data constructors, for several different arities.

This first branch of the || fails the whole attempt iff the arguments of the constructor applications are already easy to prove equal.

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)

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

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

If we're not ready to use that principle yet, try the standard inversion, which often enables the previous rule.

Similar logic to the cases for constructor injectivity above, but specialized to Some, since the above cases won't deal with polymorphic constructors.

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.

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.

Ltac rewriter := autorewrite with core in *; rewriterP.

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

Devious marker predicate to use for encoding state within proof goals

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 : _, _ =>

| forall x : _, _ =>

Yes, so let's pick the first context variable of the right type.

No more quantifiers, so now we check if the trace we computed was already used.

We only reach this case if the trace is nonempty, ensuring that inster fails if no progress can be made.

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 =>

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.

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

Pick a new name for our new instantiation.

After a round of application with the above, we will have a lot of junk done markers to clean up; hence this tactic.

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

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

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

end

end; autorewrite with core in *) in

Now the main sequence of heuristics:

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;

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.

crush instantiates crush' with the simplest possible parameters.

Ltac crush := crush' false fail.

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.

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.

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.

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

let H' := fresh "H'" in

generalize H; intro H'; guess v H'.