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

3 files changed, 108 insertions, 149 deletions

diff --git a/contrib/subtac/equations.ml4 b/contrib/subtac/equations.ml4
index 515a78280..135fcf11d 100644
--- a/contrib/subtac/equations.ml4
+++ b/contrib/subtac/equations.ml4
@@ -749,7 +749,15 @@ open Evarutil
 let lift_substitution n s = map (fun (k, x) -> (k + n, x)) s
 let map_substitution s t = map (subst_rel_subst 0 s) t
 
-let term_of_tree status isevar env (i, delta, ty) tree =
+let term_of_tree status isevar env (i, delta, ty) ann tree =
+(*   let envrec = match ann with *)
+(*     | None -> [] *)
+(*     | Some (loc, i) ->  *)
+(* 	let (n, t) = lookup_rel_id i delta in *)
+(* 	let t' = lift n t in *)
+	  
+	  
+(*   in *)
   let rec aux = function
     | Compute ((ctx, _, pats as lhs), Program rhs) -> 
 	let ty' = substl (rev (constrs_of_lhs ~inacc:false env lhs)) ty in
@@ -903,7 +911,7 @@ let equations_tac = lazy
       (TacArg(TacCall(dummy_loc, 
 		     ArgArg(dummy_loc, tactics_tac "equations"), []))))
 
-let define_by_eqs with_comp i l t nt eqs =
+let define_by_eqs with_comp i (l,ann) t nt eqs =
   let env = Global.env () in
   let isevar = ref (create_evar_defs Evd.empty) in
   let (env', sign), impls = interp_context_evars isevar env l in
@@ -951,7 +959,7 @@ let define_by_eqs with_comp i l t nt eqs =
   let split = make_split env' prob equations in
     (* if valid_tree prob split then *)
   let status = (* if is_recursive then Expand else *) Define false in
-  let t, ty = term_of_tree status isevar env' prob split in
+  let t, ty = term_of_tree status isevar env' prob ann split in
   let undef = undefined_evars !isevar in
   let t, ty = if is_recursive then 
     (it_mkLambda_or_LetIn t fixdecls, it_mkProd_or_LetIn ty fixdecls)
@@ -978,7 +986,7 @@ struct
 
   let deppat_equations : equation list Gram.Entry.e = gec "deppat_equations"
 
-  let binders_let2 : local_binder list Gram.Entry.e = gec "binders_let2"
+  let binders_let2 : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e = gec "binders_let2"
 
 (*   let where_decl : decl_notation Gram.Entry.e = gec "where_decl" *)
 
@@ -1000,7 +1008,7 @@ GEXTEND Gram
   ;
 
   binders_let2:
-    [ [ l = binders_let -> l ] ]
+    [ [ l = binders_let_fixannot -> l ] ]
   ;
 
   equation:
@@ -1022,7 +1030,7 @@ let (wit_deppat_equations : Genarg.tlevel deppat_equations_argtype),
   (rawwit_deppat_equations : Genarg.rlevel deppat_equations_argtype) =
   Genarg.create_arg "deppat_equations"
 
-type 'a binders_let2_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
+type 'a binders_let2_argtype = (local_binder list * (identifier located option * recursion_order_expr), 'a) Genarg.abstract_argument_type
 
 let (wit_binders_let2 : Genarg.tlevel binders_let2_argtype),
   (globwit_binders_let2 : Genarg.glevel binders_let2_argtype),
@@ -1096,7 +1104,7 @@ let coq_eq_refl = lazy ((Coqlib.build_coq_eq_data ()).Coqlib.refl)
 let coq_heq = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq")
 let coq_heq_refl = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl")
 
-let simplify_hyp id gl =
+let specialize_hyp id gl =
   let env = pf_env gl in
   let ty = pf_get_hyp_typ gl id in
   let evars = ref (create_evar_defs (project gl)) in
@@ -1117,18 +1125,25 @@ let simplify_hyp id gl =
 		aux true (mkApp (acc, [| p |])) (subst1 p b)
 	      else error "Unconvertible members of an heterogeneous equality"
 	| _ -> 
-	    if in_eqs then acc, ty
+	    if in_eqs then acc, in_eqs, ty
 	    else 
 	      let e = e_new_evar evars env t in
 		aux false (mkApp (acc, [| e |])) (subst1 e b))
-    | t -> acc, ty
+    | t -> acc, in_eqs, ty
   in 
-  let acc, ty = aux false (mkVar id) ty in
-  let ty = Evarutil.nf_isevar !evars ty in
-    tclTHENFIRST
-      (fun g -> Tacmach.internal_cut true id ty g)
-      (exact_no_check (Evarutil.nf_isevar !evars acc)) gl
+  try 
+    let acc, worked, ty = aux false (mkVar id) ty in
+    let ty = Evarutil.nf_isevar !evars ty in
+      if worked then
+	tclTHENFIRST
+	  (fun g -> Tacmach.internal_cut true id ty g)
+	  (exact_no_check (Evarutil.nf_isevar !evars acc)) gl
+      else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl
+  with e -> tclFAIL 0 (Cerrors.explain_exn e) gl
       
-TACTIC EXTEND simplify_hyp
-[ "simplify_hyp" ident(id) ] -> [ simplify_hyp id ]
+TACTIC EXTEND specialize_hyp
+[ "specialize_hypothesis" constr(c) ] -> [ 
+  match kind_of_term c with
+  | Var id -> specialize_hyp id
+  | _ -> tclFAIL 0 (str "Not an hypothesis") ]
 END
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 48b07db83..3f315ccb7 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -40,7 +40,7 @@ Delimit Scope context_scope with ctx.
 
 Arguments Scope snoc [context_scope].
 
-Notation " Γ , τ " := (snoc Γ τ) (at level 25, t at next level, left associativity) : context_scope.
+Notation " Γ ,, τ " := (snoc Γ τ) (at level 25, t at next level, left associativity).
 
 Fixpoint conc (Δ Γ : ctx) : ctx :=
   match Δ with
@@ -52,42 +52,36 @@ Notation " Γ ;; Δ " := (conc Δ Γ) (at level 25, left associativity) : contex
 
 Inductive term : ctx -> type -> Type :=
 | ax : forall Γ τ, term (snoc Γ τ) τ
-| weak : forall Γ τ, term Γ τ -> forall τ', term (snoc Γ τ') τ
+| weak : forall Γ τ, term Γ τ -> forall τ', term (Γ ,, τ') τ
 | abs : forall Γ τ τ', term (snoc Γ τ) τ' -> term Γ (τ --> τ')
 | app : forall Γ τ τ', term Γ (τ --> τ') -> term Γ τ -> term Γ τ'.
 
-Notation " Γ |- τ " := (term Γ τ) (at level 0).
+Hint Constructors term : lambda.
 
+Notation " Γ |-- τ " := (term Γ τ) (at level 0) : type_scope.
 
 Lemma weakening : forall Γ Δ τ, term (Γ ;; Δ) τ -> 
-  forall τ', term (Γ , τ' ;; Δ) τ.
-Proof with simpl in * ; auto ; simpl_depind.
+  forall τ', term (Γ ,, τ' ;; Δ) τ.
+Proof with simpl in * ; simplify_dep_elim ; simplify_IH_hyps ; eauto with lambda.
   intros Γ Δ τ H.
 
   dependent induction H.
 
   destruct Δ...
-    apply weak ; apply ax.
-    
-    apply ax.
-    
-  destruct Δ...
-    specialize (IHterm empty Γ)... 
-    apply weak... 
-
-    apply weak...
 
   destruct Δ...
-    apply weak. apply abs ; apply H.
 
+  destruct Δ...
     apply abs...
-    specialize (IHterm (Δ, t, τ)%ctx Γ0)...
+    
+    specialize (IHterm (Δ,, t,, τ)%ctx Γ0)...
 
+  intro.
   apply app with τ...
 Qed.
 
-Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ;; Δ) τ -> term (Γ, β, α ;; Δ) τ.
-Proof with simpl in * ; simpl_depind ; auto.
+Lemma exchange : forall Γ Δ α β τ, term (Γ,, α,, β ;; Δ) τ -> term (Γ,, β,, α ;; Δ) τ.
+Proof with simpl in * ; simplify_dep_elim ; simplify_IH_hyps ; auto.
   intros until 1.
   dependent induction H.
 
@@ -97,12 +91,12 @@ Proof with simpl in * ; simpl_depind ; auto.
     apply ax.
 
   destruct Δ...
-    pose (weakening Γ0 (empty, α))...
+    pose (weakening Γ0 (empty,, α))...
 
     apply weak...
 
-  apply abs...
-  specialize (IHterm (Δ, τ)%ctx Γ0 α β)...
+  apply abs... 
+  specialize (IHterm (Δ ,, τ))...
 
   eapply app with τ...
 Save.
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