Report r11631 from 8.2 and handle non-dependent goals better in

[dependent induction].


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

3 files changed, 60 insertions, 43 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 76daeb16b..caef1c94a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2031,15 +2031,22 @@ let ids_of_constr vars c =
     | _ -> fold_constr aux vars c
   in aux vars c
 
+let mk_term_eq env sigma ty t ty' t' =
+  if Reductionops.is_conv env sigma ty ty' then
+    mkEq ty t t', mkRefl ty' t'
+  else
+    mkHEq ty t ty' t', mkHRefl ty' t'
+
 let make_abstract_generalize gl id concl dep ctx c eqs args refls = 
   let meta = Evarutil.new_meta() in
-  let term, typ = mkVar id, pf_get_hyp_typ gl id in
+  let term, typ = mkVar id, pf_get_hyp_typ gl id (* de Bruijn closed! *) in
   let eqslen = List.length eqs in
     (* Abstract by the "generalized" hypothesis equality proof if necessary. *)
-  let abshypeq = 
+  let abshypeq, abshypt = 
     if dep then 
-      mkProd (Anonymous, mkHEq (lift 1 c) (mkRel 1) typ term, lift 1 concl)
-    else concl
+      let eq, refl = mk_term_eq (push_rel_context ctx (pf_env gl)) (project gl) (lift 1 c) (mkRel 1) typ term in
+	mkProd (Anonymous, eq, lift 1 concl), [| refl |]
+    else concl, [||]
   in
     (* Abstract by equalitites *)
   let eqs = lift_togethern 1 eqs in (* lift together and past genarg *)
@@ -2057,8 +2064,7 @@ let make_abstract_generalize gl id concl dep ctx c eqs args refls =
     (* 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
+    mkApp (appeqs, abshypt)
       
 let abstract_args gl id = 
   let c = pf_get_hyp_typ gl id in
@@ -2118,12 +2124,14 @@ let abstract_args gl id =
 		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
-	let args, refls = List.rev args, List.rev refls in
-	  Some (make_abstract_generalize gl id concl dep ctx c' eqs args refls,
-	       dep, succ (List.length ctx), vars)
+	  (match args with [||] -> None
+	  | _ ->
+	      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 args, refls = List.rev args, List.rev refls in
+		Some (make_abstract_generalize gl id concl dep ctx c' eqs args refls,
+		     dep, succ (List.length ctx), vars))
     | _ -> None
 
 let abstract_generalize id ?(generalize_vars=true) gl =
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 488b057f3..3ab7682d9 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).
+Notation " Γ , τ " := (snoc Γ τ) (at level 25, τ at next level, left associativity) : context_scope.
 
 Fixpoint conc (Δ Γ : ctx) : ctx :=
   match Δ with
@@ -48,60 +48,64 @@ Fixpoint conc (Δ Γ : ctx) : ctx :=
     | snoc Δ' x => snoc (conc Δ' Γ) x
   end.
 
-Notation " Γ ;; Δ " := (conc Δ Γ) (at level 25, left associativity) : context_scope.
+Notation " Γ  ; Δ " := (conc Δ Γ) (at level 25, left associativity) : context_scope.
+
+Reserved Notation " Γ ⊢ τ " (at level 30, no associativity). 
 
 Inductive term : ctx -> type -> Type :=
-| ax : forall Γ τ, term (snoc Γ τ) τ
-| weak : forall Γ τ, term Γ τ -> forall τ', term (Γ ,, τ') τ
-| abs : forall Γ τ τ', term (snoc Γ τ) τ' -> term Γ (τ --> τ')
-| app : forall Γ τ τ', term Γ (τ --> τ') -> term Γ τ -> term Γ τ'.
+| ax : `(Γ, τ ⊢ τ)
+| weak : `{Γ ⊢ τ -> Γ, τ' ⊢ τ}
+| abs : `{Γ, τ ⊢ τ' -> Γ ⊢ τ --> τ'}
+| app : `{Γ ⊢ τ --> τ' -> Γ ⊢ τ -> Γ ⊢ τ'}
+
+where " Γ ⊢ τ " := (term Γ τ) : type_scope.
 
 Hint Constructors term : lambda.
 
 Open Local Scope context_scope.
 
-Notation " Γ |-- τ " := (term Γ τ) (at level 0) : type_scope.
+Ltac eqns := subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps.
 
-Lemma weakening : forall Γ Δ τ, term (Γ ;; Δ) τ -> 
-  forall τ', term (Γ ,, τ' ;; Δ) τ.
-Proof with simpl in * ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; eauto with lambda.
+Lemma weakening : forall Γ Δ τ, Γ ; Δ ⊢ τ -> 
+  forall τ', Γ , τ' ; Δ ⊢ τ.
+Proof with simpl in * ; eqns ; eauto with lambda.
   intros Γ Δ τ H.
 
   dependent induction H.
 
-  destruct Δ...
+  destruct Δ as [|Δ τ']...
 
-  destruct Δ...
+  destruct Δ as [|Δ τ'']...
 
-  destruct Δ...
-    apply abs...
-    
-    specialize (IHterm (Δ,, t,, τ)%ctx Γ0)...
+  destruct Δ as [|Δ τ'']...
+    apply abs.
 
-  intro.
-  apply app with τ...
+    specialize (IHterm (Δ, τ'', τ) Γ0)...
+
+  intro. eapply app...
 Qed.
 
-Lemma exchange : forall Γ Δ α β τ, term (Γ,, α,, β ;; Δ) τ -> term (Γ,, β,, α ;; Δ) τ.
-Proof with simpl in * ; subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; auto.
+Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ.
+Proof with simpl in * ; eqns ; eauto.
   intros until 1.
+
   dependent induction H.
 
-  destruct Δ...
+  destruct Δ ; eqns.
     apply weak ; apply ax.
 
     apply ax.
 
   destruct Δ...
-    pose (weakening Γ0 (empty,, α))...
+    pose (weakening Γ0 (empty, α))...
 
     apply weak...
 
   apply abs... 
-  specialize (IHterm (Δ ,, τ))...
+    specialize (IHterm (Δ, τ))...
 
-  eapply app with τ...
-Save.
+  eapply app...
+Defined.
 
 (** Example by Andrew Kenedy, uses simplification of the first component of dependent pairs. *)
 
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 1e19f66b8..be2f176d3 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -479,7 +479,12 @@ Ltac intro_prototypes :=
     | _ => idtac
   end.
 
-Ltac do_case p := destruct p || elim_case p || (case p ; clear p).
+Ltac introduce p := 
+  first [ match p with _ => idtac end (* Already there *)
+    | intros until p | intros ].
+
+Ltac do_case p := introduce p ; (destruct p || elim_case p || (case p ; clear p)).
+Ltac do_ind p := introduce p ; (induction p || elim_ind p).
 
 Ltac dep_elimify := match goal with [ |- ?T ] => change (block_dep_elim T) end.
 
@@ -530,7 +535,7 @@ Ltac do_depind' tac H :=
    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) H.
+  do_depind' ltac:(fun hyp => do_case hyp) H.
 
 Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := 
   do_depind' ltac:(fun hyp => destruct hyp using c) H.
@@ -538,7 +543,7 @@ Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) :=
 (** 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) H.
+  do_depind' ltac:(fun hyp => revert l ; do_case hyp) 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) H.
@@ -548,7 +553,7 @@ Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l)
    calling [induction]. *)
 
 Tactic Notation "dependent" "induction" ident(H) := 
-  do_depind ltac:(fun hyp => induction hyp) H.
+  do_depind ltac:(fun hyp => do_ind hyp) H.
 
 Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := 
   do_depind ltac:(fun hyp => induction hyp using c) H.
@@ -556,7 +561,7 @@ Tactic Notation "dependent" "induction" ident(H) "using" constr(c) :=
 (** 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) H.
+  do_depind' ltac:(fun hyp => generalize l ; clear l ; do_ind hyp) 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) H.
@@ -564,4 +569,4 @@ Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "
 Ltac simplify_IH_hyps := repeat
   match goal with
     | [ hyp : _ |- _ ] => specialize_hypothesis hyp
-  end.
+  end.
\ No newline at end of file