Improve the dependent induction tactic to automatically find the

generalized hypotheses. Also move part of the tactic to ML and
improve the generated proof term in case of non-dependent induction.


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

3 files changed, 63 insertions, 39 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2259af67c..9812b5f82 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1819,28 +1819,40 @@ let lift_together l = lift_togethern 0 l
 
 let lift_list l = List.map (lift 1) l
 
-let make_abstract_generalize gl id concl ctx c eqs args refls = 
+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
+    | _ -> fold_constr aux vars c
+  in aux vars c
+
+let make_abstract_generalize gl id concl dep ctx c eqs args refls = 
   let meta = Evarutil.new_meta() in
-  let cstr = 
+  let cstr =
     (* Abstract by equalitites *)
-    let abseqs = it_mkProd_or_LetIn ~init:concl (List.map (fun x -> (Anonymous, None, x)) eqs) in 
-    (* Abstract by the "generalized" hypothesis and its equality proof *)
+    let eqs = lift_togethern 1 eqs in
+    let abseqs = it_mkProd_or_LetIn ~init:concl (List.map (fun x -> (Anonymous, None, x)) eqs) in
+      (* Abstract by the "generalized" hypothesis and its equality proof *)
     let term, typ = mkVar id, pf_get_hyp_typ gl id in
     let abshyp = 
-      let abshypeq = mkProd (Anonymous, mkHEq (lift 1 c) (mkRel 1) typ term, lift 1 abseqs) in
+      let abshypeq = 
+	if dep then 
+	  mkProd (Anonymous, mkHEq (lift 1 c) (mkRel 1) typ term, lift 1 abseqs)
+	else abseqs
+      in
 	mkProd (Name id, c, abshypeq)
     in
-    (* Abstract by the extension of the context *)
+      (* Abstract by the extension of the context *)
     let genctyp = it_mkProd_or_LetIn ~init:abshyp ctx in
-    (* The goal will become this product. *)
+      (* The goal will become this product. *)
     let genc = mkCast (mkMeta meta, DEFAULTcast, genctyp) in      
-    (* Apply the old arguments giving the proper instantiation of the hyp *)
+      (* Apply the old arguments giving the proper instantiation of the hyp *)
     let instc = mkApp (genc, Array.of_list args) in
-    (* Then apply to the original instanciated hyp. *)
+      (* Then apply to the original instanciated hyp. *)
     let newc = mkApp (instc, [| mkVar id |]) in
-    (* Apply the reflexivity proof for the original hyp. *)
-    let newc = mkApp (newc, [| mkHRefl typ term |]) in
-    (* Finaly, apply the remaining reflexivity proofs on the index, to get a term of type gl again *)
+      (* Apply the reflexivity proof for the original hyp. *)
+    let newc = if dep then mkApp (newc, [| mkHRefl typ term |]) else newc in
+      (* Finaly, apply the remaining reflexivity proofs on the index, to get a term of type gl again *)
     let appeqs = mkApp (newc, Array.of_list refls) in
       appeqs
   in cstr
@@ -1850,6 +1862,7 @@ let abstract_args gl id =
   let sigma = project gl in
   let env = pf_env gl in
   let concl = pf_concl gl in
+  let dep = dependent (mkVar id) concl in
   let avoid = ref [] in
   let get_id name = 
     let id = fresh_id !avoid (match name with Name n -> n | Anonymous -> id_of_string "gen_x") gl in 
@@ -1859,22 +1872,21 @@ let abstract_args gl id =
       App (f, args) -> 
 	(* Build application generalized w.r.t. the argument plus the necessary eqs.
 	   From env |- c : forall G, T and args : G we build
-	   (T[G'], G' : ctx, env ; G' |- args' : G, eqs := G'_i = G_i, refls : G' = G)
+	   (T[G'], G' : ctx, env ; G' |- args' : G, eqs := G'_i = G_i, refls : G' = G, vars to generalize)
 
 	   eqs are not lifted w.r.t. each other yet. (* will be needed when going to dependent indexes *)
 	*)
-	let aux (prod, ctx, ctxenv, c, args, eqs, refls, finalargs, env) arg =
+	let aux (prod, ctx, ctxenv, c, args, eqs, refls, vars, env) arg =
 	  let (name, _, ty), arity = 
 	    let rel, c = Reductionops.decomp_n_prod env sigma 1 prod in
 	      List.hd rel, c
 	  in
 	  let argty = pf_type_of gl arg in
-	  let liftarg = lift (List.length ctx) arg in
 	  let liftargty = lift (List.length ctx) argty in
-	  let convertible = Reductionops.is_conv ctxenv sigma ty liftargty in
+	  let convertible = Reductionops.is_conv_leq ctxenv sigma liftargty ty in
 	    match kind_of_term arg with
-	      | Var _ | Rel _ when convertible -> 
-		  (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, (Anonymous, liftarg, liftarg) :: finalargs, env)
+	      | Var _ | Rel _ | Ind _ when convertible -> 
+		  (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, vars, env)
 	      | _ ->
 		  let name = get_id name in
 		  let decl = (Name name, None, ty) in
@@ -1890,25 +1902,40 @@ let abstract_args gl id =
 		  in
 		  let eqs = eq :: lift_list eqs in
 		  let refls = refl :: refls in
-		  let finalargs = (Name name, mkRel 1, liftarg) :: List.map (fun (x, y, z) -> (x, lift 1 y, lift 1 z)) finalargs in
-		    (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, finalargs, env)
+		  let vars = ids_of_constr vars arg in
+		    (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, vars, env)
 	in 
-	let arity, ctx, ctxenv, c', args, eqs, refls, finalargs, env = 
+	let arity, ctx, ctxenv, c', args, eqs, refls, vars, env = 
 	  Array.fold_left aux (pf_type_of gl f,[],env,f,[],[],[],[],env) args
 	in
-	let eqs = lift_togethern 1 eqs in
 	let args, refls = List.rev args, List.rev refls in
-	  Some (make_abstract_generalize gl id concl ctx c' eqs args refls)
+	  Some (make_abstract_generalize gl id concl dep ctx c' eqs args refls,
+	       dep, succ (List.length ctx), vars)
     | _ -> None
 
 let abstract_generalize id gl =
   Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
 (*   let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string "Coq.Logic.JMeq")) in *)
 (*   Library.require_library [qualid] None; *)
+  let oldid = pf_get_new_id id gl in
   let newc = abstract_args gl id in
     match newc with
       | None -> tclIDTAC gl
-      | Some newc -> refine newc gl
+      | Some (newc, dep, n, vars) -> 
+	  if dep then
+	    tclTHENLIST [refine newc;
+			 rename_hyp [(id, oldid)];
+			 tclDO n intro; 
+			 generalize_dep (mkVar oldid);
+			 tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars]
+	      gl
+	  else
+	    tclTHENLIST [refine newc;
+			 clear [id];
+			 tclDO n intro; 
+			 tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars]
+	      gl
+
 
 let occur_rel n c = 
   let res = not (noccurn n c) in
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 0db172e82..482553869 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -56,7 +56,7 @@ Lemma weakening : forall Γ Δ τ, term (Γ ; Δ) τ ->
 Proof with simpl in * ; auto ; simpl_depind.
   intros Γ Δ τ H.
 
-  dependent induction H generalizing Γ Δ.
+  dependent induction H.
 
   destruct Δ...
     apply weak ; apply ax.
@@ -64,7 +64,7 @@ Proof with simpl in * ; auto ; simpl_depind.
     apply ax.
     
   destruct Δ...
-    specialize (IHterm Γ empty)...
+    specialize (IHterm Γ empty)... 
     apply weak...
 
     apply weak...
@@ -81,7 +81,7 @@ Qed.
 Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ.
 Proof with simpl in * ; simpl_depind ; auto.
   intros until 1.
-  dependent induction H generalizing Γ Δ α β.
+  dependent induction H.
 
   destruct Δ...
     apply weak ; apply ax.
@@ -94,7 +94,7 @@ Proof with simpl in * ; simpl_depind ; auto.
     apply weak...
 
   apply abs...
-  specialize (IHterm Γ0 (Δ, τ))...
+  specialize (IHterm Γ0 α β (Δ, τ))...
 
   eapply app with τ...
 Save.
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index b56ca26c3..bb1ffbd2b 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -231,37 +231,34 @@ Ltac simpl_depind := subst* ; autoinjections ; try discriminates ;
    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. *)
 
-(** First a tactic to prepare for a dependent induction on an hypothesis [H]. *)
-
-Ltac prepare_depind H :=
-  let oldH := fresh "old" H in
-    generalize_eqs H ; rename H into oldH ; (intros until H || intros until 1) ; 
-      generalize dependent oldH ;
-        try (intros _ _) (* If the goal is not dependent on the hyp, we can prove a stronger statement *).
-
 (** 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 :=
-  prepare_depind H ; tac H ; repeat progress simpl_depind.
+  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*.
 
+Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := 
+  do_depind ltac:(fun H => destruct H 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.
 
+Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := 
+  do_depind ltac:(fun H => induction H 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.
 
-(** This tactic also generalizes the goal by the given variables before the induction. *)
-
 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.
+