Changement de comportement du [rewrite ... in H]: Coq échoue si H

apparaît dans le but ou dans l'une des hypothèses (ferme les bugs
#447, #883 et #1228).


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

5 files changed, 109 insertions, 70 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 7cb0cb5394..57043057a3 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -245,6 +245,31 @@ let global_vars_set env constr =
   in 
   filtrec Idset.empty constr
 
+(* like [global_vars] but don't get through evars *)
+let global_vars_set_drop_evar env constr = 
+  let fold_constr_drop_evar f acc c = match kind_of_term c with
+    | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+      | Construct _) -> acc
+    | Cast (c,_,t) -> f (f acc c) t
+    | Prod (_,t,c) -> f (f acc t) c
+    | Lambda (_,t,c) -> f (f acc t) c
+    | LetIn (_,b,t,c) -> f (f (f acc b) t) c
+    | App (c,l) -> Array.fold_left f (f acc c) l
+    | Evar (_,l) -> acc
+    | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
+    | Fix (_,(lna,tl,bl)) ->
+	let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in
+	  Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd
+    | CoFix (_,(lna,tl,bl)) ->
+	let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in
+	  Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd in
+  let rec filtrec acc c =
+    let vl = vars_of_global env c in
+    let acc = List.fold_right Idset.add vl acc in
+      fold_constr_drop_evar filtrec acc c
+  in 
+    filtrec Idset.empty constr
+
 (* [keep_hyps env ids] keeps the part of the section context of [env] which 
    contains the variables of the set [ids], and recursively the variables 
    contained in the types of the needed variables. *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 24e72b9a23..b6d9bf6d38 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -165,6 +165,7 @@ val set_engagement : engagement -> env -> env
 (* [global_vars_set env c] returns the list of [id]'s occurring as
    [VAR id] in [c] *)
 val global_vars_set : env -> constr -> Idset.t
+val global_vars_set_drop_evar : env -> constr -> Idset.t
 (* the constr must be an atomic construction *)
 val vars_of_global : env -> constr -> identifier list
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index b5c8011051..61e4ec58e0 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -80,15 +80,15 @@ let clear_hyps ids gl =
               error (string_of_id id'^
 		        " is used in hypothesis "^string_of_id id))
 	  (global_vars_set_of_decl env d) in
-    clear_hyps ids fcheck gl.evar_hyps in
+      clear_hyps ids fcheck gl.evar_hyps in
   let ncl = gl.evar_concl in
-  if !check && cleared_ids<>[] then
-    Idset.iter
-      (fun id' ->
-        if List.mem id' cleared_ids then
-          error (string_of_id id'^" is used in conclusion"))
-      (global_vars_set env ncl);
-  mk_goal nhyps ncl gl.evar_extra
+    if !check && cleared_ids<>[] then
+      Idset.iter
+	(fun id' ->
+          if List.mem id' cleared_ids then
+            error (string_of_id id'^" is used in conclusion"))
+	(global_vars_set_drop_evar env ncl);
+    mk_goal nhyps ncl gl.evar_extra
 
 (* The ClearBody tactic *)
 
@@ -155,7 +155,7 @@ let split_sign hfrom hto l =
       	else 
 	  splitrec (d::left) (toleft or (hyp = hto)) right
   in 
-  splitrec [] false l
+    splitrec [] false l
 
 let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
   let env = Global.env() in
@@ -214,19 +214,25 @@ let check_forward_dependencies id tail =
 		^ (string_of_id id')))
     tail
 
+let check_goal_dependency id cl =
+  let env = Global.env() in
+    if Idset.mem id (global_vars_set_drop_evar env cl) then
+      error (string_of_id id^" is used in conclusion")
 
 let rename_hyp id1 id2 sign =
   apply_to_hyp_and_dependent_on sign id1
     (fun (_,b,t) _ -> (id2,b,t))
     (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
 
-let replace_hyp sign id d =
+let replace_hyp sign id d cl =
+  if !check then
+    check_goal_dependency id cl;
   apply_to_hyp sign id
     (fun sign _ tail ->
-       if !check then
-	 (check_backward_dependencies sign d;
-	  check_forward_dependencies id tail);
-       d)
+      if !check then
+	(check_backward_dependencies sign d;
+	 check_forward_dependencies id tail); 
+      d)
 
 (* why we dont check that id does not appear in tail ??? *)
 let insert_after_hyp sign id d =
@@ -419,12 +425,12 @@ let prim_refiner r sigma goal =
 	(match kind_of_term (strip_outer_cast cl) with
            | Prod (_,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let sign' = replace_hyp sign id (id,None,c1) in
+	       let sign' = replace_hyp sign id (id,None,c1) cl in
 	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
 	       [sg]
            | LetIn (_,c1,t1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let sign' = replace_hyp sign id (id,Some c1,t1) in
+	       let sign' = replace_hyp sign id (id,Some c1,t1) cl in
 	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
 	       [sg]
 	   | _ ->
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4ed2613d85..72a1267c37 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -87,29 +87,29 @@ let general_rewrite_bindings_clause cls lft2rgt (c,l) gl =
      break search for a defined setoid relation in head position. *)
   let t = snd (decompose_prod (whd_betaiotazeta ctype)) in 
   let head = if isApp t then fst (destApp t) else t in 
-  if relation_table_mem head && l = NoBindings then 
-    general_s_rewrite_clause cls lft2rgt c [] gl
-  else 
-    (* Original code. In particular, [splay_prod] performs delta-reduction. *)
-    let env = pf_env gl in
-    let sigma = project gl in 
-    let _,t = splay_prod env sigma t in
-    match match_with_equation t with
-      | None -> 
-	  if l = NoBindings
-	  then general_s_rewrite_clause cls lft2rgt c [] gl
-	  else error "The term provided does not end with an equation" 
-      | Some (hdcncl,_) -> 
-          let hdcncls = string_of_inductive hdcncl in 
-	  let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
-          let dir = if cls=None then lft2rgt else not lft2rgt in
-          let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
-          let elim =
-	    try pf_global gl (id_of_string rwr_thm)
-            with Not_found ->
-              error ("Cannot find rewrite principle "^rwr_thm)
-          in 
-	  general_elim_clause cls (c,l) (elim,NoBindings) gl
+    if relation_table_mem head && l = NoBindings then 
+      general_s_rewrite_clause cls lft2rgt c [] gl
+    else 
+      (* Original code. In particular, [splay_prod] performs delta-reduction. *)
+      let env = pf_env gl in
+      let sigma = project gl in 
+      let _,t = splay_prod env sigma t in
+	match match_with_equation t with
+	  | None -> 
+	      if l = NoBindings
+	      then general_s_rewrite_clause cls lft2rgt c [] gl
+	      else error "The term provided does not end with an equation" 
+	  | Some (hdcncl,_) -> 
+              let hdcncls = string_of_inductive hdcncl in 
+	      let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
+              let dir = if cls=None then lft2rgt else not lft2rgt in
+              let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
+              let elim =
+		try pf_global gl (id_of_string rwr_thm)
+		with Not_found ->
+		  error ("Cannot find rewrite principle "^rwr_thm)
+              in 
+		general_elim_clause cls (c,l) (elim,NoBindings) gl
 
 let general_rewrite_bindings = general_rewrite_bindings_clause None
 let general_rewrite l2r c = general_rewrite_bindings l2r (c,NoBindings)
@@ -133,21 +133,21 @@ let general_multi_rewrite l2r c cl =
 	  (tclTRY (general_rewrite_bindings_in l2r id c)) 
 	  (try_do_hyps l)
   in 
-  if cl.concl_occs <> [] then 
-    error "The \"at\" syntax isn't available yet for the rewrite/replace tactic"
-  else 
-    tclTHENFIRST 
-      (if cl.onconcl then general_rewrite_bindings l2r c else tclIDTAC)
-      (match cl.onhyps with 
-	 | Some l -> do_hyps l
-	 | None -> 
-	     fun gl -> 
-	       (* try to rewrite in all hypothesis 
-		  (except maybe the rewritten one) *)
-	       let ids = match kind_of_term (fst c) with 
-		 | Var id -> list_remove id (pf_ids_of_hyps gl)
-		 | _ -> pf_ids_of_hyps gl
-	       in try_do_hyps ids gl)
+    if cl.concl_occs <> [] then 
+      error "The \"at\" syntax isn't available yet for the rewrite/replace tactic"
+    else 
+      tclTHENFIRST 
+	(if cl.onconcl then general_rewrite_bindings l2r c else tclIDTAC)
+	(match cl.onhyps with 
+	   | Some l -> do_hyps l
+	   | None -> 
+	       fun gl -> 
+		 (* try to rewrite in all hypothesis 
+		    (except maybe the rewritten one) *)
+		 let ids = match kind_of_term (fst c) with 
+		   | Var id -> list_remove id (pf_ids_of_hyps gl)
+		   | _ -> pf_ids_of_hyps gl
+		 in try_do_hyps ids gl)
 
 
 (* Conditional rewriting, the success of a rewriting is related 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a3c57c6927..433b64c326 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -529,39 +529,46 @@ let apply_without_reduce c gl =
 
 let cut_and_apply c gl =
   let goal_constr = pf_concl gl in 
-  match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with
-    | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
-	tclTHENLAST
-	  (apply_type (mkProd (Anonymous,c2,goal_constr)) [mkMeta(new_meta())])
-	  (apply_term c [mkMeta (new_meta())]) gl
-    | _ -> error "Imp_elim needs a non-dependent product"
+    match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with
+      | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
+	  tclTHENLAST
+	    (apply_type (mkProd (Anonymous,c2,goal_constr)) [mkMeta(new_meta())])
+	    (apply_term c [mkMeta (new_meta())]) gl
+      | _ -> error "Imp_elim needs a non-dependent product"
 
 let cut c gl =
   match kind_of_term (hnf_type_of gl c) with
     | Sort _ ->
         let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
         let t = mkProd (Anonymous, c, pf_concl gl) in
-        tclTHENFIRST
-          (internal_cut_rev id c)
-          (tclTHEN (apply_type t [mkVar id]) (thin [id]))
-          gl
+          tclTHENFIRST
+            (internal_cut_rev id c)
+            (tclTHEN (apply_type t [mkVar id]) (thin [id]))
+            gl
     | _  -> error "Not a proposition or a type"
 
 let cut_intro t = tclTHENFIRST (cut t) intro
 
-let cut_replacing id t tac = 
+(* let cut_replacing id t tac = 
   tclTHENS (cut t)
     [tclORELSE
-      (intro_replacing id) 
-      (tclORELSE (intro_erasing id) (intro_using id));
-     tac (refine_no_check (mkVar id)) ]
+	(intro_replacing id) 
+	(tclORELSE (intro_erasing id) (intro_using id));
+     tac (refine_no_check (mkVar id)) ] *)
+
+(* cut_replacing échoue si l'hypothèse à remplacer apparaît dans le
+   but, ou dans une autre hypothèse *)
+let cut_replacing id t tac = 
+  tclTHENS (cut t) [
+      tclORELSE (intro_replacing id) (intro_erasing id); 
+      tac (refine_no_check (mkVar id)) ]
 
 let cut_in_parallel l = 
   let rec prec = function
     | [] -> tclIDTAC 
     | h::t -> tclTHENFIRST (cut h) (prec t)
   in 
-  prec (List.rev l)
+    prec (List.rev l)
 
 (********************************************************************)
 (*               Exact tactics                                      *)
@@ -738,7 +745,7 @@ let general_elim_clause elimtac (c,lbindc) (elimc,lbindelimc) gl =
   let indclause  = make_clenv_binding gl (c,t) lbindc  in
   let elimt      = pf_type_of gl elimc in
   let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in 
-  elimtac elimclause indclause gl
+    elimtac elimclause indclause gl
 
 let general_elim c e ?(allow_K=true) =
   general_elim_clause (elimination_clause_scheme allow_K) c e