diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Equality.v | 29 | ||||
| -rw-r--r-- | theories/Program/Tactics.v | 22 | ||||
| -rw-r--r-- | theories/Program/Utils.v | 6 |
3 files changed, 31 insertions, 26 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index d19f29c3..c776070a 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Equality.v 11023 2008-05-30 11:08:39Z msozeau $ i*) +(*i $Id: Equality.v 11282 2008-07-28 11:51:53Z msozeau $ i*) (** Tactics related to (dependent) equality and proof irrelevance. *) @@ -82,7 +82,7 @@ Ltac simpl_uip := (** Simplify equalities appearing in the context and goal. *) -Ltac simpl_eq := simpl ; repeat (elim_eq_rect ; simpl) ; repeat (simpl_uip ; simpl). +Ltac simpl_eq := simpl ; unfold eq_rec_r, eq_rec ; repeat (elim_eq_rect ; simpl) ; repeat (simpl_uip ; simpl). (** Try to abstract a proof of equality, if no proof of the same equality is present in the context. *) @@ -235,30 +235,43 @@ Ltac simpl_depind := subst* ; autoinjections ; try discriminates ; and starts a dependent induction using this tactic. *) Ltac do_depind tac H := + generalize_eqs_vars H ; tac H ; repeat progress simpl_depind. + +(** A variant where generalized variables should be given by the user. *) + +Ltac do_depind' tac H := generalize_eqs H ; tac H ; repeat progress simpl_depind. (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. *) Tactic Notation "dependent" "destruction" ident(H) := - do_depind ltac:(fun H => destruct H ; intros) H ; subst*. + do_depind ltac:(fun hyp => destruct hyp ; intros) H ; subst*. Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := - do_depind ltac:(fun H => destruct H using c ; intros) H. + do_depind ltac:(fun hyp => destruct hyp using c ; intros) H. + +(** This tactic also generalizes the goal by the given variables before the induction. *) + +Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := + do_depind' ltac:(fun hyp => revert l ; destruct hyp ; intros) H. + +Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := + do_depind' ltac:(fun hyp => revert l ; destruct hyp using c ; intros) H. (** Then we have wrappers for usual calls to induction. One can customize the induction tactic by writting another wrapper calling do_depind. *) Tactic Notation "dependent" "induction" ident(H) := - do_depind ltac:(fun H => induction H ; intros) H. + do_depind ltac:(fun hyp => induction hyp ; intros) H. Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := - do_depind ltac:(fun H => induction H using c ; intros) H. + do_depind ltac:(fun hyp => induction hyp using c ; intros) H. (** This tactic also generalizes the goal by the given variables before the induction. *) Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := - do_depind ltac:(fun H => generalize l ; clear l ; induction H ; intros) H. + do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp ; intros) H. Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := - do_depind ltac:(fun H => generalize l ; clear l ; induction H using c ; intros) H. + do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c ; intros) H. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 41b170c9..bb5054b4 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Tactics.v 11122 2008-06-13 14:18:44Z msozeau $ i*) +(*i $Id: Tactics.v 11282 2008-07-28 11:51:53Z msozeau $ i*) (** This module implements various tactics used to simplify the goals produced by Program, which are also generally useful. *) @@ -77,10 +77,10 @@ Ltac clear_dup := match goal with | [ H : ?X |- _ ] => match goal with - | [ H' : X |- _ ] => - match H' with - | H => fail 2 - | _ => clear H' || clear H + | [ H' : ?Y |- _ ] => + match H with + | H' => fail 2 + | _ => conv X Y ; (clear H' || clear H) end end end. @@ -158,14 +158,6 @@ Ltac autoinjection := let tac H := progress (inversion H ; subst ; clear_dups) ; clear H in match goal with | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H - | [ H : ?f ?a ?b = ?f' ?a' ?b' |- _ ] => tac H - | [ H : ?f ?a ?b ?c = ?f' ?a' ?b' ?c' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d ?e ?g= ?f' ?a' ?b' ?c' ?d' ?e' ?g' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d ?e ?g ?h= ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' |- _ ] => tac H - | [ H : ?f ?a ?b ?c ?d ?e ?g ?h ?i ?j = ?f' ?a' ?b' ?c' ?d' ?e'?g' ?h' ?i' ?j' |- _ ] => tac H end. Ltac autoinjections := repeat autoinjection. @@ -222,7 +214,7 @@ 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 [Obligations 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 := @@ -231,4 +223,4 @@ Ltac program_simplify := Ltac program_simpl := program_simplify ; auto. -Ltac obligations_tactic := program_simpl. +Ltac obligation_tactic := program_simpl. diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index 21eee0ca..fcd85f41 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Utils.v 10919 2008-05-11 22:04:26Z msozeau $ i*) +(*i $Id: Utils.v 11309 2008-08-06 10:30:35Z herbelin $ i*) Require Export Coq.Program.Tactics. @@ -42,8 +42,8 @@ Notation dec := sumbool_of_bool. (** Hide proofs and generates obligations when put in a term. *) -Notation "'in_left'" := (@left _ _ _) : program_scope. -Notation "'in_right'" := (@right _ _ _) : program_scope. +Notation in_left := (@left _ _ _). +Notation in_right := (@right _ _ _). (** Extraction directives *) (* |