Fixes in dependent induction tactic, putting things in better order for

simplifications (homogeneous equations first).


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

2 files changed, 72 insertions, 66 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ac76912824..2162d891a5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1961,35 +1961,33 @@ let ids_of_constr vars c =
 
 let make_abstract_generalize gl id concl dep ctx c eqs args refls = 
   let meta = Evarutil.new_meta() in
-  let cstr =
+  let term, typ = mkVar id, pf_get_hyp_typ gl id in
+  let eqslen = List.length eqs in
+    (* Abstract by the "generalized" hypothesis equality proof if necessary. *)
+  let abshypeq = 
+    if dep then 
+      mkProd (Anonymous, mkHEq (lift 1 c) (mkRel 1) typ term, lift 1 concl)
+    else concl
+  in
     (* Abstract by equalitites *)
-    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 = 
-	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 *)
-    let genctyp = it_mkProd_or_LetIn ~init:abshyp ctx in
-      (* 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 *)
-    let instc = mkApp (genc, Array.of_list args) in
-      (* Then apply to the original instanciated hyp. *)
-    let newc = mkApp (instc, [| mkVar id |]) in
-      (* 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
-    
+  let eqs = lift_togethern 1 eqs in (* lift together and past genarg *)
+  let abseqs = it_mkProd_or_LetIn ~init:(lift eqslen abshypeq) (List.map (fun x -> (Anonymous, None, x)) eqs) in
+    (* Abstract by the "generalized" hypothesis. *)
+  let genarg = mkProd (Name id, c, abseqs) in
+    (* Abstract by the extension of the context *)
+  let genctyp = it_mkProd_or_LetIn ~init:genarg ctx in
+    (* 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 *)
+  let instc = mkApp (genc, Array.of_list args) in
+    (* Then apply to the original instanciated hyp. *)
+  let instc = mkApp (instc, [| mkVar id |]) in
+    (* Apply the reflexivity proofs on the indices. *)
+  let appeqs = mkApp (instc, Array.of_list refls) in
+    (* Finaly, apply the reflexivity proof for the original hyp, to get a term of type gl again. *)
+  let newc = if dep then mkApp (appeqs, [| mkHRefl typ term |]) else appeqs in
+    newc
+      
 let abstract_args gl id = 
   let c = pf_get_hyp_typ gl id in
   let sigma = project gl in
@@ -2018,25 +2016,25 @@ let abstract_args gl id =
 	  let liftargty = lift (List.length ctx) argty in
 	  let convertible = Reductionops.is_conv_leq ctxenv sigma liftargty ty in
 	    match kind_of_term arg with
-	      | 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
-		  let ctx = decl :: ctx in
-		  let c' = mkApp (lift 1 c, [|mkRel 1|]) in
-		  let args = arg :: args in
-		  let liftarg = lift (List.length ctx) arg in
-		  let eq, refl = 
-		    if convertible then
-		      mkEq (lift 1 ty) (mkRel 1) liftarg, mkRefl argty arg
-		    else
-		      mkHEq (lift 1 ty) (mkRel 1) liftargty liftarg, mkHRefl argty arg
-		  in
-		  let eqs = eq :: lift_list eqs in
-		  let refls = refl :: refls in
-		  let vars = ids_of_constr vars arg in
-		    (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, vars, 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
+		let ctx = decl :: ctx in
+		let c' = mkApp (lift 1 c, [|mkRel 1|]) in
+		let args = arg :: args in
+		let liftarg = lift (List.length ctx) arg in
+		let eq, refl = 
+		  if convertible then
+		    mkEq (lift 1 ty) (mkRel 1) liftarg, mkRefl argty arg
+		  else
+		    mkHEq (lift 1 ty) (mkRel 1) liftargty liftarg, mkHRefl argty arg
+		in
+		let eqs = eq :: lift_list eqs in
+		let refls = refl :: refls in
+		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
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 4825538691..48b07db83d 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -1,10 +1,10 @@
 Require Import Coq.Program.Program.
-Set Implicit Arguments.
-Unset Strict Implicit.
+Set Manual Implicit Arguments.
+
 
 Variable A : Set.
 
-Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall n, vector n -> vector (S n).
+Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall {n}, vector n -> vector (S n).
 
 Goal forall n, forall v : vector (S n), vector n.
 Proof.
@@ -35,24 +35,32 @@ Inductive ctx : Type :=
 | empty : ctx
 | snoc : ctx -> type -> ctx.
 
-Notation " Γ , τ " := (snoc Γ τ) (at level 25, t at next level, left associativity).
+Bind Scope context_scope with ctx.
+Delimit Scope context_scope with ctx.
+
+Arguments Scope snoc [context_scope].
+
+Notation " Γ , τ " := (snoc Γ τ) (at level 25, t at next level, left associativity) : context_scope.
 
-Fixpoint conc (Γ Δ : ctx) : ctx :=
+Fixpoint conc (Δ Γ : ctx) : ctx :=
   match Δ with
     | empty => Γ
-    | snoc Δ' x => snoc (conc Γ Δ') x
+    | snoc Δ' x => snoc (conc Δ' Γ) x
   end.
 
-Notation " Γ ; Δ " := (conc Γ Δ) (at level 25, left associativity).
+Notation " Γ ;; Δ " := (conc Δ Γ) (at level 25, left associativity) : context_scope.
 
 Inductive term : ctx -> type -> Type :=
-| ax : forall Γ τ, term (Γ, τ) τ
-| weak : forall Γ τ, term Γ τ -> forall τ', term (Γ, τ') τ
-| abs : forall Γ τ τ', term (Γ , τ) τ' -> term Γ (τ --> τ')
+| ax : forall Γ τ, term (snoc Γ τ) τ
+| weak : forall Γ τ, term Γ τ -> forall τ', term (snoc Γ τ') τ
+| abs : forall Γ τ τ', term (snoc Γ τ) τ' -> term Γ (τ --> τ')
 | app : forall Γ τ τ', term Γ (τ --> τ') -> term Γ τ -> term Γ τ'.
 
-Lemma weakening : forall Γ Δ τ, term (Γ ; Δ) τ -> 
-  forall τ', term (Γ , τ' ; Δ) τ.
+Notation " Γ |- τ " := (term Γ τ) (at level 0).
+
+
+Lemma weakening : forall Γ Δ τ, term (Γ ;; Δ) τ -> 
+  forall τ', term (Γ , τ' ;; Δ) τ.
 Proof with simpl in * ; auto ; simpl_depind.
   intros Γ Δ τ H.
 
@@ -64,21 +72,21 @@ Proof with simpl in * ; auto ; simpl_depind.
     apply ax.
     
   destruct Δ...
-    specialize (IHterm Γ empty)... 
-    apply weak...
+    specialize (IHterm empty Γ)... 
+    apply weak... 
 
     apply weak...
 
   destruct Δ...
-    apply weak ; apply abs ; apply H.
+    apply weak. apply abs ; apply H.
 
     apply abs...
-    specialize (IHterm Γ0 (Δ, t, τ))...
+    specialize (IHterm (Δ, t, τ)%ctx Γ0)...
 
   apply app with τ...
 Qed.
 
-Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ.
+Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ;; Δ) τ -> term (Γ, β, α ;; Δ) τ.
 Proof with simpl in * ; simpl_depind ; auto.
   intros until 1.
   dependent induction H.
@@ -89,12 +97,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 Γ0 α β (Δ, τ))...
+  specialize (IHterm (Δ, τ)%ctx Γ0 α β)...
 
   eapply app with τ...
 Save.