Report improvements in Equations to the dependent elimination tactic:

- Do not touch at the user equalities and so on by using a blocking
constant. This avoids the wild autoinjections and subst tactics that
were used before. Thanks to Brian Aydemir for an example were this hurt
a lot.
- Debug the tactic used to simplify induction hypotheses.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11415 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 62 insertions, 112 deletions

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index c83b5d38d..2b914ace7 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -259,56 +259,6 @@ Ltac simpl_depind_l := subst_left_no_fail ; autoinjections_left ; try discrimina
 Ltac simpl_depind_r := subst_right_no_fail ; autoinjections_right ; try discriminates ; 
   simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs.
 
-(** The following tactics allow to do induction on an already instantiated inductive predicate
-   by first generalizing it and adding the proper equalities to the context, in a maner similar to 
-   the BasicElim tactic of "Elimination with a motive" by Conor McBride. *)
-
-(** The [do_depind] higher-order tactic takes an induction tactic as argument and an hypothesis 
-   and starts a dependent induction using this tactic. *)
-
-Ltac do_depind tac H :=
-  generalize_eqs_vars H ; tac H ; repeat progress simpl_depind_r ; subst_left_no_fail.
-
-(** 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_l ; subst_right_no_fail.
-
-(** Calls [destruct] on the generalized hypothesis, results should be similar to inversion.
-   By default, we don't try to generalize the hyp by its variable indices.  *)
-
-Tactic Notation "dependent" "destruction" ident(H) := 
-  do_depind' ltac:(fun hyp => destruct hyp ; intros) H.
-
-Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := 
-  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. We suppose the hyp has to be generalized before
-   calling [induction]. *)
-
-Tactic Notation "dependent" "induction" ident(H) := 
-  do_depind ltac:(fun hyp => induction hyp ; intros) H.
-
-Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := 
-  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 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 hyp => generalize l ; clear l ; induction hyp using c ; intros) H.
-
 (** Support for the [Equations] command.
    These tactics implement the necessary machinery to solve goals produced by the 
    [Equations] command relative to dependent pattern-matching. 
@@ -349,6 +299,18 @@ Ltac elim_tac tac p :=
 Ltac elim_case p := elim_tac ltac:(fun p el => destruct p using el) p.
 Ltac elim_ind p := elim_tac ltac:(fun p el => induction p using el) p.
 
+(** The [BelowPackage] class provides the definition of a [Below] predicate for some datatype,
+   allowing to talk about course-of-value recursion on it. *)
+
+Class BelowPackage (A : Type) :=
+  Below : A -> Type ;
+  below : Π (a : A), Below a.
+
+(** The [Recursor] class defines a recursor on a type, based on some definition of [Below]. *)
+
+Class Recursor (A : Type) (BP : BelowPackage A) := 
+  rec_type : A -> Type ; rec : Π (a : A), rec_type a.
+
 (** Lemmas used by the simplifier, mainly rephrasings of [eq_rect], [eq_ind]. *)
 
 Lemma solution_left : Π A (B : A -> Type) (t : A), B t -> (Π x, x = t -> B x).
@@ -385,6 +347,11 @@ Ltac unfold_equations := repeat progress autosimpl with equations.
 
 Ltac simplify_equations := repeat (unfold_equations ; simplify_eqs). 
 
+(** We will use the [block_induction] definition to separate the goal from the 
+   equalities generated by the tactic. *)
+
+Definition block_dep_elim {A : Type} (a : A) := a.
+
 (** Using these we can make a simplifier that will perform the unification 
    steps needed to put the goal in normalised form (provided there are only
    constructor forms). Compare with the lemma 16 of the paper.
@@ -408,7 +375,7 @@ Ltac simplify_one_dep_elim_term c :=
       intros hyp ; elimtype False ; discriminate
     | ?x = ?y -> _ => let hyp := fresh in
       intros hyp ; case hyp ; clear hyp
-    | id ?T => fail 1 (* Do not put any part of the rhs in the hyps *)
+    | block_dep_elim ?T => fail 1 (* Do not put any part of the rhs in the hyps *)
     | _ => intro
   end.
 
@@ -470,8 +437,8 @@ Ltac simpl_intros m := ((apply m || refine m) ; auto) || (intro ; simpl_intros m
 (** Hopefully the first branch suffices. *)
 
 Ltac try_intros m :=
-  solve [ intros ; unfold id ; refine m || apply m ] ||
-  solve [ unfold id ; simpl_intros m ].
+  solve [ intros ; unfold block_dep_elim ; refine m || apply m ] ||
+  solve [ unfold block_dep_elim ; simpl_intros m ].
 
 (** To solve a goal by inversion on a particular target. *)
 
@@ -504,11 +471,13 @@ Ltac intro_prototypes :=
     | _ => idtac
   end.
 
-Ltac do_case p := destruct p || elim_case p.
+Ltac do_case p := destruct p || elim_case p || (case p ; clear p).
 
-Ltac idify := match goal with [ |- ?T ] => change (id T) end.
+Ltac dep_elimify := match goal with [ |- ?T ] => change (block_dep_elim T) end.
 
-Ltac case_last := idify ;
+Ltac un_dep_elimify := unfold block_dep_elim in *.
+
+Ltac case_last := dep_elimify ;
   on_last_hyp ltac:(fun p => 
     let ty := type of p in
       match ty with
@@ -534,76 +503,57 @@ Ltac equations := set_eos ;
     | _ => nonrec_equations
   end.
 
-(*
-Equations NoConfusion_nat (P : Prop) (x y : nat) : Prop :=
-NoConfusion_nat P 0 0 := P -> P ;
-NoConfusion_nat P 0 (S y) := P ;
-NoConfusion_nat P (S x) 0 := P ;
-NoConfusion_nat P (S x) (S y) := (x = y -> P) -> P.
-
-  Solve Obligations using equations.
-
-Equations noConfusion_nat (P : Prop) (x y : nat) (H : x = y) : NoConfusion_nat P x y :=
-noConfusion_nat P 0 0 refl := λ p, p ;
-noConfusion_nat P (S n) (S n) refl := λ p : n = n -> P, p refl.
-
-  Solve Obligations using equations.
-
-Instance nat_noconf : NoConfusionPackage nat :=
-  NoConfusion := λ P, Π x y, x = y -> NoConfusion_nat P x y ;
-  noConfusion := λ P x y, noConfusion_nat P x y.
+(** The following tactics allow to do induction on an already instantiated inductive predicate
+   by first generalizing it and adding the proper equalities to the context, in a maner similar to 
+   the BasicElim tactic of "Elimination with a motive" by Conor McBride. *)
 
-Equations NoConfusion_bool (P : Prop) (x y : bool) : Prop :=
-NoConfusion_bool P true true := P -> P ;
-NoConfusion_bool P false false := P -> P ;
-NoConfusion_bool P true false := P ;
-NoConfusion_bool P false true := P.
+(** The [do_depind] higher-order tactic takes an induction tactic as argument and an hypothesis 
+   and starts a dependent induction using this tactic. *)
 
-  Solve Obligations using equations.
+Ltac do_depind tac H :=
+  (try intros until H) ; dep_elimify ; generalize_eqs_vars H ; tac H ; simplify_dep_elim ; un_dep_elimify.
 
-Equations noConfusion_bool (P : Prop) (x y : bool) (H : x = y) : NoConfusion_bool P x y :=
-noConfusion_bool P true true refl := λ p, p ;
-noConfusion_bool P false false refl := λ p, p.
+(** A variant where generalized variables should be given by the user. *)
 
-  Solve Obligations using equations.
+Ltac do_depind' tac H :=
+  (try intros until H) ; dep_elimify ; generalize_eqs H ; tac H ; simplify_dep_elim ; un_dep_elimify.
 
-Instance bool_noconf : NoConfusionPackage bool :=
-  NoConfusion := λ P, Π x y, x = y -> NoConfusion_bool P x y ;
-  noConfusion := λ P x y, noConfusion_bool P x y.
+(** Calls [destruct] on the generalized hypothesis, results should be similar to inversion.
+   By default, we don't try to generalize the hyp by its variable indices.  *)
 
-Equations NoConfusion_unit (P : Prop) (x y : unit) : Prop :=
-NoConfusion_unit P tt tt := P -> P.
+Tactic Notation "dependent" "destruction" ident(H) := 
+  do_depind' ltac:(fun hyp => destruct hyp) H.
 
-  Solve Obligations using equations.
+Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := 
+  do_depind' ltac:(fun hyp => destruct hyp using c) H.
 
-Equations noConfusion_unit (P : Prop) (x y : unit) (H : x = y) : NoConfusion_unit P x y :=
-noConfusion_unit P tt tt refl := λ p, p.
+(** This tactic also generalizes the goal by the given variables before the induction. *)
 
-  Solve Obligations using equations.
+Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := 
+  do_depind' ltac:(fun hyp => revert l ; destruct hyp) H.
 
-Instance unit_noconf : NoConfusionPackage unit :=
-  NoConfusion := λ P, Π x y, x = y -> NoConfusion_unit P x y ;
-  noConfusion := λ P x y, noConfusion_unit P x y.
+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) H.
 
-Require Import List.
+(** Then we have wrappers for usual calls to induction. One can customize the induction tactic by 
+   writting another wrapper calling do_depind. We suppose the hyp has to be generalized before
+   calling [induction]. *)
 
-Implicit Arguments nil [[A]].
+Tactic Notation "dependent" "induction" ident(H) := 
+  do_depind ltac:(fun hyp => induction hyp) H.
 
-Equations NoConfusion_list (P : Prop) (A : Type) (x y : list A) : Prop :=
-NoConfusion_list P A nil nil := P -> P ;
-NoConfusion_list P A nil (cons a y) := P ;
-NoConfusion_list P A (cons a x) nil := P ;
-NoConfusion_list P A (cons a x) (cons b y) := (a = b -> x = y -> P) -> P.
+Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := 
+  do_depind ltac:(fun hyp => induction hyp using c) H.
 
-  Solve Obligations using equations.
+(** This tactic also generalizes the goal by the given variables before the induction. *)
 
-Equations noConfusion_list (P : Prop) A (x y : list A) (H : x = y) : NoConfusion_list P A x y :=
-noConfusion_list P A nil nil refl := λ p, p ;
-noConfusion_list P A (cons a x) (cons a x) refl := λ p : a = a -> x = x -> P, p refl refl.
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := 
+  do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp) H.
 
-  Solve Obligations using equations.
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
+  do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c) H.
 
-Instance list_noconf A : NoConfusionPackage (list A) :=
-  NoConfusion := λ P, Π x y, x = y -> NoConfusion_list P A x y ;
-  noConfusion := λ P x y, noConfusion_list P A x y.
-*)
\ No newline at end of file
+Ltac simplify_IH_hyps := repeat
+  match goal with
+    | [ hyp : _ |- _ ] => specialize_hypothesis hyp
+  end.
\ No newline at end of file