diff options
Diffstat (limited to 'theories/Program/Tactics.v')
| -rw-r--r-- | theories/Program/Tactics.v | 106 |
1 files changed, 82 insertions, 24 deletions
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 499629a6..e692876d 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -6,11 +6,32 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Tactics.v 11709 2008-12-20 11:42:15Z msozeau $ i*) +(*i $Id$ i*) (** This module implements various tactics used to simplify the goals produced by Program, which are also generally useful. *) +(** Debugging tactics to show the goal during evaluation. *) + +Ltac show_goal := match goal with [ |- ?T ] => idtac T end. + +Ltac show_hyp id := + match goal with + | [ H := ?b : ?T |- _ ] => + match H with + | id => idtac id ":=" b ":" T + end + | [ H : ?T |- _ ] => + match H with + | id => idtac id ":" T + end + end. + +Ltac show_hyps := + try match reverse goal with + | [ H : ?T |- _ ] => show_hyp H ; fail + end. + (** The [do] tactic but using a Coq-side nat. *) Ltac do_nat n tac := @@ -22,7 +43,7 @@ Ltac do_nat n tac := (** Do something on the last hypothesis, or fail *) Ltac on_last_hyp tac := - match goal with [ H : _ |- _ ] => tac H || fail 1 end. + match goal with [ H : _ |- _ ] => first [ tac H | fail 1 ] end. (** Destructs one pair, without care regarding naming. *) @@ -56,7 +77,7 @@ Ltac destruct_exists := repeat (destruct_one_ex). Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex). -(** Destruct an existential hypothesis [t] keeping its name for the first component +(** Destruct an existential hypothesis [t] keeping its name for the first component and using [Ht] for the second *) Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht]. @@ -75,7 +96,7 @@ Ltac discriminates := (** Revert the last hypothesis. *) -Ltac revert_last := +Ltac revert_last := match goal with [ H : _ |- _ ] => revert H end. @@ -84,11 +105,20 @@ Ltac revert_last := Ltac reverse := repeat revert_last. +(** Reverse everything up to hypothesis id (not included). *) + +Ltac revert_until id := + on_last_hyp ltac:(fun id' => + match id' with + | id => idtac + | _ => revert id' ; revert_until id + end). + (** Clear duplicated hypotheses *) Ltac clear_dup := - match goal with - | [ H : ?X |- _ ] => + match goal with + | [ H : ?X |- _ ] => match goal with | [ H' : ?Y |- _ ] => match H with @@ -100,10 +130,20 @@ Ltac clear_dup := Ltac clear_dups := repeat clear_dup. +(** Try to clear everything except some hyp *) + +Ltac clear_except hyp := + repeat match goal with [ H : _ |- _ ] => + match H with + | hyp => fail 1 + | _ => clear H + end + end. + (** A non-failing subst that substitutes as much as possible. *) Ltac subst_no_fail := - repeat (match goal with + repeat (match goal with [ H : ?X = ?Y |- _ ] => subst X || subst Y end). @@ -118,13 +158,13 @@ Ltac on_application f tac T := | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v) | context [f ?x ?y ?z ?w] => tac (f x y z w) | context [f ?x ?y ?z] => tac (f x y z) - | context [f ?x ?y] => tac (f x y) + | context [f ?x ?y] => tac (f x y) | context [f ?x] => tac (f x) end. (** A variant of [apply] using [refine], doing as much conversion as necessary. *) -Ltac rapply p := +Ltac rapply p := refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) || refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) || refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) || @@ -141,7 +181,7 @@ Ltac rapply p := refine (p _ _) || refine (p _) || refine p. - + (** Tactical [on_call f tac] applies [tac] on any application of [f] in the hypothesis or goal. *) Ltac on_call f tac := @@ -174,17 +214,29 @@ Tactic Notation "destruct_call" constr(f) := destruct_call f. (** Permit to name the results of destructing the call to [f]. *) -Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := +Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := destruct_call_as f l. (** Specify the hypothesis in which the call occurs as well. *) -Tactic Notation "destruct_call" constr(f) "in" hyp(id) := +Tactic Notation "destruct_call" constr(f) "in" hyp(id) := destruct_call_in f id. -Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(id) := +Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(id) := destruct_call_as_in f l id. +(** A marker for prototypes to destruct. *) + +Definition fix_proto {A : Type} (a : A) := a. + +Ltac destruct_rec_calls := + match goal with + | [ H : fix_proto _ |- _ ] => destruct_calls H ; clear H + end. + +Ltac destruct_all_rec_calls := + repeat destruct_rec_calls ; unfold fix_proto in *. + (** Try to inject any potential constructor equality hypothesis. *) Ltac autoinjection tac := @@ -204,23 +256,23 @@ Ltac destruct_nondep H := let H0 := fresh "H" in assert(H0 := H); destruct H0. Ltac bang := match goal with - | |- ?x => + | |- ?x => match x with - | context [False_rect _ ?p] => elim p + | appcontext [False_rect _ ?p] => elim p end end. - + (** A tactic to show contradiction by first asserting an automatically provable hypothesis. *) -Tactic Notation "contradiction" "by" constr(t) := +Tactic Notation "contradiction" "by" constr(t) := let H := fresh in assert t as H by auto with * ; contradiction. (** A tactic that adds [H:=p:typeof(p)] to the context if no hypothesis of the same type appears in the goal. Useful to do saturation using tactics. *) -Ltac add_hypothesis H' p := +Ltac add_hypothesis H' p := match type of p with - ?X => - match goal with + ?X => + match goal with | [ H : X |- _ ] => fail 1 | _ => set (H':=p) ; try (change p with H') ; clearbody H' end @@ -248,13 +300,19 @@ Ltac refine_hyp c := end. (** The default simplification tactic used by Program is defined by [program_simpl], sometimes [auto] - is not enough, better rebind using [Obligation Tactic := tac] in this case, + is not enough, better rebind using [Obligation Tactic := tac] in this case, possibly using [program_simplify] to use standard goal-cleaning tactics. *) Ltac program_simplify := - simpl ; intros ; destruct_conjs ; simpl proj1_sig in * ; subst* ; autoinjections ; try discriminates ; + simpl in |- *; intros ; destruct_all_rec_calls ; repeat (destruct_conjs; simpl proj1_sig in *); + subst*; autoinjections ; try discriminates ; try (solve [ red ; intros ; destruct_conjs ; autoinjections ; discriminates ]). -Ltac program_simpl := program_simplify ; auto. +Ltac program_solve_wf := + match goal with + |- well_founded _ => auto with * + end. + +Ltac program_simpl := program_simplify ; auto; try program_solve_wf. -Ltac obligation_tactic := program_simpl. +Obligation Tactic := program_simpl. |