Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and <- when a variable is about to be substituted (subst_one rewrite the whole context at once, while multi_rewrite rewrites each hyp independently, what may break typing in case of dependencies). Also generalize "dependent rewrite" to "sig" (to be done: generalize it to eq_dep, eq_dep1, and any dependent tuple).

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

7 files changed, 67 insertions, 28 deletions

diff --git a/CHANGES b/CHANGES
index 54b44309e8..d02e29e4d0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -38,6 +38,7 @@ Tactics
   "Unset Tactic Pattern Unification"). It also supports (full) betaiota.
 - Tactic autorewrite does no longer instantiate pre-existing
   existential variables (theoretical source of possible incompatibility).
+- Tactic "dependent rewrite" now supports equality in "sig".
 
 Vernacular commands
 
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 204b2b226f..eb7828eaa6 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -187,10 +187,17 @@ let build_sigma_set () = anomaly "Use build_sigma_type"
 let build_sigma_type () =
   { proj1 = init_constant ["Specif"] "projT1";
     proj2 = init_constant ["Specif"] "projT2";
-    elim = init_constant ["Specif"] "sigT_rec";
+    elim = init_constant ["Specif"] "sigT_rect";
     intro = init_constant ["Specif"] "existT";
     typ = init_constant ["Specif"] "sigT" }
 
+let build_sigma () =
+  { proj1 = init_constant ["Specif"] "proj1_sig";
+    proj2 = init_constant ["Specif"] "proj2_sig";
+    elim = init_constant ["Specif"] "sig_rect";
+    intro = init_constant ["Specif"] "exist";
+    typ = init_constant ["Specif"] "sig" }
+
 let build_prod () =
   { proj1 = init_constant ["Datatypes"] "fst";
     proj2 = init_constant ["Datatypes"] "snd";
@@ -363,6 +370,7 @@ let coq_jmeq_ref     = lazy (gen_reference "Coqlib" ["Logic";"JMeq"] "JMeq")
 let coq_eq_true_ref = lazy (gen_reference "Coqlib" ["Init";"Datatypes"] "eq_true")
 let coq_existS_ref  = lazy (anomaly "use coq_existT_ref")
 let coq_existT_ref  = lazy (init_reference ["Specif"] "existT")
+let coq_exist_ref  = lazy (init_reference ["Specif"] "exist")
 let coq_not_ref     = lazy (init_reference ["Logic"] "not")
 let coq_False_ref   = lazy (init_reference ["Logic"] "False")
 let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool")
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index aac1206e10..5d3580f26a 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -104,6 +104,7 @@ type coq_sigma_data = {
 
 val build_sigma_set : coq_sigma_data delayed
 val build_sigma_type : coq_sigma_data delayed
+val build_sigma : coq_sigma_data delayed
 
 (** Non-dependent pairs in Set from Datatypes *)
 val build_prod : coq_sigma_data delayed
@@ -175,6 +176,7 @@ val coq_jmeq_ref : global_reference lazy_t
 val coq_eq_true_ref : global_reference lazy_t
 val coq_existS_ref : global_reference lazy_t
 val coq_existT_ref : global_reference lazy_t
+val coq_exist_ref : global_reference lazy_t
 val coq_not_ref : global_reference lazy_t
 val coq_False_ref : global_reference lazy_t
 val coq_sumbool_ref : global_reference lazy_t
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 51265d7231..9d2e3c8e81 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1390,29 +1390,16 @@ let is_eq_x gl x (id,_,c) =
   with PatternMatchingFailure ->
     ()
 
-let subst_one dep_proof_ok x gl =
-  let hyps = pf_hyps gl in
-  let (_,xval,_) = pf_get_hyp gl x in
-  (* If x has a body, simply replace x with body and clear x *)
-  if xval <> None then tclTHEN (unfold_body x) (clear [x]) gl else
-  (* x is a variable: *)
-  let varx = mkVar x in
-  (* Find a non-recursive definition for x *)
-  let (hyp,rhs,dir) =
-    try
-      let test hyp _ = is_eq_x gl varx hyp in
-      Sign.fold_named_context test ~init:() hyps;
-      errorlabstrm "Subst"
-        (str "Cannot find any non-recursive equality over " ++ pr_id x ++
-	 str".")
-    with FoundHyp res -> res
-  in
+(* Rewrite "hyp:x=rhs" or "hyp:rhs=x" (if dir=false) everywhere and
+   erase hyp and x; proceed by generalizing all dep hyps *)
+
+let subst_one dep_proof_ok x (hyp,rhs,dir) gl =
   (* The set of hypotheses using x *)
   let depdecls =
     let test (id,_,c as dcl) =
       if id <> hyp && occur_var_in_decl (pf_env gl) x dcl then dcl
       else failwith "caught" in
-    List.rev (map_succeed test hyps) in
+    List.rev (map_succeed test (pf_hyps gl)) in
   let dephyps = List.map (fun (id,_,_) -> id) depdecls in
   (* Decides if x appears in conclusion *)
   let depconcl = occur_var (pf_env gl) x (pf_concl gl) in
@@ -1428,8 +1415,8 @@ let subst_one dep_proof_ok x gl =
       (id,None,_) -> intro_using id
     | (id,Some hval,htyp) ->
         letin_tac None (Name id)
-	  (replace_term varx rhs hval)
-	  (Some (replace_term varx rhs htyp)) nowhere
+	  (replace_term (mkVar x) rhs hval)
+	  (Some (replace_term (mkVar x) rhs htyp)) nowhere
   in
   let need_rewrite = dephyps <> [] || depconcl in
   tclTHENLIST
@@ -1438,13 +1425,37 @@ let subst_one dep_proof_ok x gl =
        general_rewrite dir all_occurrences true dep_proof_ok (mkVar hyp);
        thin dephyps;
        tclMAP introtac depdecls]
-    else
-      [thin dephyps;
-       tclMAP introtac depdecls]) @
+      else
+       [tclIDTAC]) @
      [tclTRY (clear [x;hyp])]) gl
 
+(* Look for an hypothesis hyp of the form "x=rhs" or "rhs=x", rewrite
+   it everywhere, and erase hyp and x; proceed by generalizing all dep hyps *)
+
+let subst_one_var dep_proof_ok x gl =
+  let hyps = pf_hyps gl in
+  let (_,xval,_) = pf_get_hyp gl x in
+  (* If x has a body, simply replace x with body and clear x *)
+  if xval <> None then tclTHEN (unfold_body x) (clear [x]) gl else
+  (* x is a variable: *)
+  let varx = mkVar x in
+  (* Find a non-recursive definition for x *)
+  let (hyp,rhs,dir) =
+    try
+      let test hyp _ = is_eq_x gl varx hyp in
+      Sign.fold_named_context test ~init:() hyps;
+      errorlabstrm "Subst"
+        (str "Cannot find any non-recursive equality over " ++ pr_id x ++
+	 str".")
+    with FoundHyp res -> res in
+  subst_one dep_proof_ok x (hyp,rhs,dir) gl
+
 let subst_gen dep_proof_ok ids =
-  tclTHEN tclNORMEVAR (tclMAP (subst_one dep_proof_ok) ids)
+  tclTHEN tclNORMEVAR (tclMAP (subst_one_var dep_proof_ok) ids)
+
+(* For every x, look for an hypothesis hyp of the form "x=rhs" or "rhs=x",
+   rewrite it everywhere, and erase hyp and x; proceed by generalizing
+   all dep hyps *)
 
 let subst = subst_gen true
 
@@ -1521,3 +1532,5 @@ let replace_multi_term dir_opt c  =
 
 let _ = Tactics.register_general_multi_rewrite
   (fun b evars t cls -> general_multi_rewrite b evars t cls)
+
+let _ = Tactics.register_subst_one (fun b -> subst_one b)
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index e02ddb926b..f0773f793d 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -423,6 +423,7 @@ let dest_nf_eq gls eqn =
 (* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *)
 let coq_ex_pattern_gen ex = lazy PATTERN [ %ex ?X1 ?X2 ?X3 ?X4 ]
 let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref
+let coq_exist_pattern = coq_ex_pattern_gen coq_exist_ref
 
 let match_sigma ex ex_pat =
   match matches (Lazy.force ex_pat) ex with
@@ -434,7 +435,8 @@ let match_sigma ex ex_pat =
 
 let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *)
   first_match (match_sigma ex)
-    [coq_existT_pattern, build_sigma_type]
+    [coq_existT_pattern, build_sigma_type;
+     coq_exist_pattern, build_sigma]
 
 (* Pattern "(sig ?1 ?2)" *)
 let coq_sig_pattern = lazy PATTERN [ %coq_sig_ref ?X1 ?X2 ]
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 97928c87c2..ce27649d22 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1222,12 +1222,20 @@ let simplest_split = split NoBindings
 (* Decomposing introductions *)
 (*****************************)
 
+(* Rewriting function for rewriting one hypothesis at the time *)
 let forward_general_multi_rewrite =
   ref (fun _ -> failwith "general_multi_rewrite undefined")
 
+(* Rewriting function for substitution (x=t) everywhere at the same time *)
+let forward_subst_one =
+  ref (fun _ -> failwith "subst_one undefined")
+
 let register_general_multi_rewrite f =
   forward_general_multi_rewrite := f
 
+let register_subst_one f =
+  forward_subst_one := f
+
 let error_unexpected_extra_pattern loc nb pat =
   let s1,s2,s3 = match pat with
   | IntroIdentifier _ -> "name", (plural nb " introduction pattern"), "no"
@@ -1261,6 +1269,8 @@ let intro_or_and_pattern loc b ll l' tac id gl =
 let rewrite_hyp l2r id gl =
   let rew_on l2r =
     !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) in
+  let subst_on l2r x rhs =
+    !forward_subst_one true x (id,rhs,l2r) in
   let clear_var_and_eq c =
     tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in
   let t = pf_whd_betadeltaiota gl (pf_type_of gl (mkVar id)) in
@@ -1268,9 +1278,9 @@ let rewrite_hyp l2r id gl =
   match match_with_equality_type t with
   | Some (hdcncl,[_;lhs;rhs]) ->
       if l2r & isVar lhs & not (occur_var (pf_env gl) (destVar lhs) rhs) then
-	tclTHEN (rew_on l2r allHypsAndConcl) (clear_var_and_eq lhs) gl
+	subst_on l2r (destVar lhs) rhs gl
       else if not l2r & isVar rhs & not (occur_var (pf_env gl) (destVar rhs) lhs) then
-	tclTHEN (rew_on l2r allHypsAndConcl) (clear_var_and_eq rhs) gl
+	subst_on l2r (destVar rhs) lhs gl
       else
 	tclTHEN (rew_on l2r onConcl) (tclTRY (clear [id])) gl
   | Some (hdcncl,[c]) ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c52c145879..e148c5a2d6 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -379,3 +379,6 @@ val specialize_eqs : identifier -> tactic
 
 val register_general_multi_rewrite :
   (bool -> evars_flag -> constr with_bindings -> clause -> tactic) -> unit
+
+val register_subst_one :
+  (bool -> identifier -> identifier * constr * bool -> tactic) -> unit