A fix for bug #1397:

 setoid_reflexivity may discover it is doing plain Leibniz stuff (see
 exception Optimize in setoid_replace), and falls back to the usual 
 reflexivity. Except that this one, due to the lack of delta-red, 
 refuses to handle the job, and gives it back to setoid_reflexivity: 
 a loop is born.

 quick fix for the moment: add some whd_betadeltaiota to reflexivity in 
 the special situation where reflexivity is called back by
 setoid_reflexivity.
 
 Similar issue & fix for symmetry, transitivity. 

 rewrite has potentially the same problem, but I can't manage to trigger
 a wild loop in practice. This code clearly deserves a closer look
 someday...




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

3 files changed, 39 insertions, 12 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 1e70bf2771..c66a55d38c 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1934,7 +1934,7 @@ let setoid_reflexivity gl =
            (str "The relation " ++ prrelation rel ++ str " is not reflexive.")
        | Some refl -> apply refl gl
  with
-  Optimize -> reflexivity gl
+  Optimize -> reflexivity_red true gl
 
 let setoid_symmetry gl =
  try
@@ -1950,7 +1950,7 @@ let setoid_symmetry gl =
            (str "The relation " ++ prrelation rel ++ str " is not symmetric.")
        | Some sym -> apply sym gl
  with
-  Optimize -> symmetry gl
+  Optimize -> symmetry_red true gl
 
 let setoid_symmetry_in id gl =
  let new_hyp =
@@ -1985,7 +1985,7 @@ let setoid_transitivity c gl =
             apply_with_bindings
              (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl
  with
-  Optimize -> transitivity c gl
+  Optimize -> transitivity_red true c gl
 ;;
 
 Tactics.register_setoid_reflexivity setoid_reflexivity;;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8b10913def..0d643e1b53 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2389,10 +2389,18 @@ let dImp cls =
 let setoid_reflexivity = ref (fun _ -> assert false)
 let register_setoid_reflexivity f = setoid_reflexivity := f
 
-let reflexivity gl =
-  match match_with_equation (pf_concl gl) with
+let reflexivity_red allowred gl =
+  (* PL: usual reflexivity don't perform any reduction when searching 
+     for an equality, but we may need to do some when called back from 
+     inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
+  let concl = if not allowred then pf_concl gl
+  else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) 
+  in 
+  match match_with_equation concl with
     | None -> !setoid_reflexivity gl
-    | Some (hdcncl,args) ->  one_constructor 1 NoBindings gl
+    | Some _ -> one_constructor 1 NoBindings gl
+
+let reflexivity gl = reflexivity_red false gl
 
 let intros_reflexivity  = (tclTHEN intros reflexivity)
 
@@ -2406,8 +2414,14 @@ let intros_reflexivity  = (tclTHEN intros reflexivity)
 let setoid_symmetry = ref (fun _ -> assert false)
 let register_setoid_symmetry f = setoid_symmetry := f
 
-let symmetry gl =
-  match match_with_equation (pf_concl gl) with
+let symmetry_red allowred gl =
+  (* PL: usual symmetry don't perform any reduction when searching 
+     for an equality, but we may need to do some when called back from 
+     inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
+  let concl = if not allowred then pf_concl gl
+  else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) 
+  in 
+  match match_with_equation concl with
     | None -> !setoid_symmetry gl
     | Some (hdcncl,args) ->
         let hdcncls = string_of_inductive hdcncl in
@@ -2421,7 +2435,7 @@ let symmetry gl =
               | [c1;c2]     -> mkApp (hdcncl, [| c2; c1 |])
 	      | _ -> assert false 
 	    in 
-	    tclTHENLAST (cut symc)
+	    tclTHENFIRST (cut symc)
               (tclTHENLIST 
 		[ intro;
 		  tclLAST_HYP simplest_case;
@@ -2429,6 +2443,8 @@ let symmetry gl =
 	      gl
 	end
 
+let symmetry gl = symmetry_red false gl
+
 let setoid_symmetry_in = ref (fun _ _ -> assert false)
 let register_setoid_symmetry_in f = setoid_symmetry_in := f
 
@@ -2469,8 +2485,14 @@ let intros_symmetry =
 let setoid_transitivity = ref (fun _ _ -> assert false)
 let register_setoid_transitivity f = setoid_transitivity := f
 
-let transitivity t gl =
-  match match_with_equation (pf_concl gl) with
+let transitivity_red allowred t gl =
+  (* PL: usual transitivity don't perform any reduction when searching 
+     for an equality, but we may need to do some when called back from 
+     inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
+  let concl = if not allowred then pf_concl gl
+  else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) 
+  in 
+  match match_with_equation concl with
     | None -> !setoid_transitivity t gl
     | Some (hdcncl,args) -> 
         let hdcncls = string_of_inductive hdcncl in
@@ -2497,7 +2519,9 @@ let transitivity t gl =
 		    tclLAST_HYP simplest_case;
 		    assumption ])) gl
         end 
-	
+
+let transitivity t gl = transitivity_red false t gl
+
 let intros_transitivity  n  = tclTHEN intros (transitivity n)
 
 (* tactical to save as name a subproof such that the generalisation of 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0c20241620..8de2498674 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -290,16 +290,19 @@ val simplest_split             : tactic
 (*s Logical connective tactics. *)
 
 val register_setoid_reflexivity : tactic -> unit
+val reflexivity_red             : bool -> tactic
 val reflexivity                 : tactic
 val intros_reflexivity          : tactic
 
 val register_setoid_symmetry : tactic -> unit
+val symmetry_red                : bool -> tactic
 val symmetry                    : tactic
 val register_setoid_symmetry_in : (identifier -> tactic) -> unit
 val symmetry_in                 : identifier -> tactic
 val intros_symmetry             : clause -> tactic
 
 val register_setoid_transitivity : (constr -> tactic) -> unit
+val transitivity_red            : bool -> constr -> tactic
 val transitivity                : constr -> tactic
 val intros_transitivity         : constr -> tactic