### view src/CpdtTactics.v @ 417:539ed97750bb

Update for Coq trunk version intended for final 8.4 release
author Adam Chlipala Tue, 17 Jul 2012 16:37:58 -0400 76e1dfcb86eb ed829eaa91b2
line wrap: on
line source
```(* Copyright (c) 2008-2012, Adam Chlipala
*
* Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
* The license text is available at:
*)

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.

(** 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 [match]es). *)
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'.```