Fixes in dependent induction tactic to keep names, allow giving

intro-patterns and avoid useless generalizations on inductive 
parameters.


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

4 files changed, 84 insertions, 20 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 23524e850..afc4a9b96 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1909,14 +1909,26 @@ let mkEq t x y =
 let mkRefl t x = 
   mkApp ((build_coq_eq_data ()).refl, [| t; x |])
 
-let mkHEq t x u y = 
+let mkHEq t x u y =
   mkApp (coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq",
 	[| t; x; u; y |])
     
-let mkHRefl t x = 
+let mkHRefl t x =
   mkApp (coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl",
 	[| t; x |])
 
+(* let id = lazy (coq_constant "mkHEq" ["Init";"Datatypes"] "id") *)
+
+(* let mkHEq t x u y =  *)
+(*   let ty = new_Type () in *)
+(*   mkApp (coq_constant "mkHEq" ["Logic";"EqdepFacts"] "eq_dep", *)
+(* 	[| ty; mkApp (Lazy.force id, [|ty|]); t; x; u; y |]) *)
+    
+(* let mkHRefl t x =  *)
+(*   let ty = new_Type () in *)
+(*   mkApp (coq_constant "mkHEq" ["Logic";"EqdepFacts"] "eq_dep_intro", *)
+(* 	[| ty; mkApp (Lazy.force id, [|ty|]); t; x |]) *)
+
 let mkCoe a x p px y eq = 
   mkApp (Option.get (build_coq_eq_data ()).rect, [| a; x; p; px; y; eq |])
 
@@ -1936,6 +1948,14 @@ let ids_of_constr vars c =
   let rec aux vars c = 
     match kind_of_term c with
     | Var id -> if List.mem id vars then vars else id :: vars
+    | App (f, args) -> 
+	(match kind_of_term f with
+	| Construct (ind,_) 
+	| Ind ind ->
+            let (mib,mip) = Global.lookup_inductive ind in
+	      array_fold_left_from mib.Declarations.mind_nparams 
+		aux vars args
+	| _ -> fold_constr aux vars c)
     | _ -> fold_constr aux vars c
   in aux vars c
 
@@ -2018,6 +2038,16 @@ let abstract_args gl id =
 		  let vars = ids_of_constr vars arg in
 		    (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, vars, env)
 	in 
+	let f, args =
+	  match kind_of_term f with
+	  | Construct (ind,_) 
+	  | Ind ind ->
+              let (mib,mip) = Global.lookup_inductive ind in
+	      let first = mib.Declarations.mind_nparams in
+	      let pars, args = array_chop first args in
+		mkApp (f, pars), args
+	  | _ -> f, args
+	in
 	let arity, ctx, ctxenv, c', args, eqs, refls, vars, env = 
 	  Array.fold_left aux (pf_type_of gl f,[],env,f,[],[],[],[],env) args
 	in
@@ -2040,10 +2070,11 @@ let abstract_generalize id ?(generalize_vars=true) gl =
 	    else
 	      tclTHENLIST [refine newc; clear [id]; tclDO n intro]
 	  in 
-	    if generalize_vars then
-	      tclTHEN tac (tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars) gl
+	    if generalize_vars then tclTHEN tac 
+	      (tclFIRST [revert (List.rev vars) ;
+			 tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars]) gl
 	    else tac gl
-
+	      
 let occur_rel n c = 
   let res = not (noccurn n c) in
   res
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 54c97ae7b..dd082246c 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -18,7 +18,7 @@
 (* Ltac typeclass_instantiation := typeclasses eauto || eauto. *)
 
 Tactic Notation "clapply" ident(c) :=
-  eapply @c ; eauto with typeclass_instances.
+  eapply @c ; typeclasses eauto.
 
 (** The unconvertible typeclass, to test that two objects of the same type are 
    actually different. *)
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index cd30d77ca..c569f743d 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -224,7 +224,36 @@ Ltac do_simpl_IHs_eqs :=
 
 Ltac simpl_IHs_eqs := repeat do_simpl_IHs_eqs.
 
-Ltac simpl_depind := subst* ; autoinjections ; try discriminates ; 
+(** We split substitution tactics in the two directions depending on which 
+   names we want to keep corresponding to the generalization performed by the
+   [generalize_eqs] tactic. *)
+
+Ltac subst_left_no_fail :=
+  repeat (match goal with 
+            [ H : ?X = ?Y |- _ ] => subst X
+          end).
+
+Ltac subst_right_no_fail :=
+  repeat (match goal with 
+            [ H : ?X = ?Y |- _ ] => subst Y
+          end).
+
+Ltac inject_left H :=
+  progress (inversion H ; subst_left_no_fail ; clear_dups) ; clear H.
+
+Ltac inject_right H :=
+  progress (inversion H ; subst_right_no_fail ; clear_dups) ; clear H.
+
+Ltac autoinjections_left := repeat autoinjection ltac:inject_left.
+Ltac autoinjections_right := repeat autoinjection ltac:inject_right.
+
+Ltac simpl_depind := subst_no_fail ; autoinjections ; try discriminates ; 
+  simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs.
+
+Ltac simpl_depind_l := subst_left_no_fail ; autoinjections_left ; try discriminates ; 
+  simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs.
+
+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
@@ -235,20 +264,21 @@ 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.
+  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.
+  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. *)
+(** 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 ; subst*.
+  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.
+  do_depind' ltac:(fun hyp => destruct hyp using c ; intros) H.
 
 (** This tactic also generalizes the goal by the given variables before the induction. *)
 
@@ -259,7 +289,8 @@ Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l)
   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. *)
+   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.
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index d7535c323..49b883342 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -91,7 +91,7 @@ Ltac clear_dups := repeat clear_dup.
 
 Ltac subst_no_fail :=
   repeat (match goal with 
-            [ H : ?X = ?Y |- _ ] => subst X || subst Y                  
+            [ H : ?X = ?Y |- _ ] => subst X || subst Y
           end).
 
 Tactic Notation "subst" "*" := subst_no_fail.
@@ -154,13 +154,15 @@ Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(i
 
 (** Try to inject any potential constructor equality hypothesis. *)
 
-Ltac autoinjection :=
-  let tac H := progress (inversion H ; subst ; clear_dups) ; clear H in
-    match goal with
-      | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H
-    end.
+Ltac autoinjection tac :=
+  match goal with
+    | [ H : ?f ?a = ?f' ?a' |- _ ] => tac H
+  end.
+
+Ltac inject H :=
+  progress (inversion H ; subst* ; clear_dups) ; clear H.
 
-Ltac autoinjections := repeat autoinjection.
+Ltac autoinjections := repeat autoinjection ltac:inject.
 
 (** Destruct an hypothesis by first copying it to avoid dependencies. *)