Plug the new setoid implemtation in, leaving the original one commented

out. The semantics of the old setoid are faithfully simulated by the new
tactic, hence no scripts involving rewrite are modified. However,
parametric morphism declarations need to be changed, but there are only a
few in the standard library, notably in FSets. The declaration and the
introduction of variables in the script need to be tweaked a bit,
otherwise the proofs remain unchanged. 
Some fragile scripts not introducting their variable names explicitely
were broken. Requiring Setoid requires Program.Basics which sets stronger
implicit arguments on some constants, a few scripts benefit from that.
Ring/field have been ported but do not really use the new typeclass
architecture as well as they could. Performance should be mostly
unchanged, but will certainly improve in the near future. Size of the
vo's seems not to have changed at all.
It will certainly break some contribs using Setoid.


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

3 files changed, 110 insertions, 68 deletions

diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index 6542d280c..56b08a8fa 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -243,7 +243,7 @@ Section ZMORPHISM.
                   Zplus Zmult Zeq_bool gen_phiZ).
    apply mkRmorph;simpl;try rrefl.
    apply gen_phiZ_add.  apply gen_phiZ_mul. apply gen_Zeqb_ok.
-  apply  (Smorph_morph Rsth Reqe Rth Zsth Zth SRmorph gen_phiZ_ext).
+  apply  (Smorph_morph Rsth Reqe Rth Zth SRmorph gen_phiZ_ext).
  Qed.
 
 End ZMORPHISM.
diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v
index caa704595..cefdcf52b 100644
--- a/contrib/setoid_ring/Ring_theory.v
+++ b/contrib/setoid_ring/Ring_theory.v
@@ -59,8 +59,7 @@ Section Power.
   induction j;simpl.
   rewrite IHj.
   rewrite (mul_comm x (pow_pos x j *pow_pos x j)).
-  set (w:= x*pow_pos x j);unfold w at 2.
-  rewrite (mul_comm x (pow_pos x j));unfold w.
+  setoid_rewrite (mul_comm x (pow_pos x j)) at 2.
   repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth).
   repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth).
   apply (Seq_refl _ _ Rsth).
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 6c3b6337a..bce41b9b5 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -201,7 +201,8 @@ let constr_of = function
 let stdlib_modules =
   [["Coq";"Setoids";"Setoid"];
    ["Coq";"Lists";"List"];
-   ["Coq";"Init";"Datatypes"]
+   ["Coq";"Init";"Datatypes"];
+   ["Coq";"Init";"Logic"];
   ]
 
 let coq_constant c =
@@ -212,6 +213,7 @@ let coq_cons = coq_constant "cons"
 let coq_nil = coq_constant "nil"
 let coq_None = coq_constant "None"
 let coq_Some = coq_constant "Some"
+let coq_eq = coq_constant "eq"
 
 let lapp f args = mkApp(Lazy.force f,args)
 
@@ -448,10 +450,12 @@ let (theory_to_obj, obj_to_theory) =
       export_function = export_th }
 
 
-let setoid_of_relation r =
+let setoid_of_relation env a r =
   lapp coq_mk_Setoid
-    [|r.rel_a; r.rel_aeq;
-      Option.get r.rel_refl; Option.get r.rel_sym; Option.get r.rel_trans |]
+    [|a ; r ; 
+      Class_tactics.reflexive_proof env a r ; 
+      Class_tactics.symmetric_proof env a r ; 
+      Class_tactics.transitive_proof env a r |]
 
 let op_morph r add mul opp req m1 m2 m3 =
   lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |]
@@ -459,63 +463,108 @@ let op_morph r add mul opp req m1 m2 m3 =
 let op_smorph r add mul req m1 m2 =
   lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |]
 
-let default_ring_equality (r,add,mul,opp,req) =
-  let is_setoid = function
-      {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} ->
-        eq_constr req rel (* Qu: use conversion ? *)
-    | _ -> false in
-  match default_relation_for_carrier ~filter:is_setoid r with
-      Leibniz _ ->
-        let setoid = lapp coq_eq_setoid [|r|] in
-        let op_morph =
-          match opp with
+(* let default_ring_equality (r,add,mul,opp,req) = *)
+(*   let is_setoid = function *)
+(*       {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *)
+(*         eq_constr req rel (\* Qu: use conversion ? *\) *)
+(*     | _ -> false in *)
+(*   match default_relation_for_carrier ~filter:is_setoid r with *)
+(*       Leibniz _ -> *)
+(*         let setoid = lapp coq_eq_setoid [|r|] in *)
+(*         let op_morph = *)
+(*           match opp with *)
+(*               Some opp -> lapp coq_eq_morph [|r;add;mul;opp|] *)
+(*             | None -> lapp coq_eq_smorph [|r;add;mul|] in *)
+(*         (setoid,op_morph) *)
+(*     | Relation rel -> *)
+(*         let setoid = setoid_of_relation rel in *)
+(*         let is_endomorphism = function *)
+(*             { args=args } -> List.for_all *)
+(*                 (function (var,Relation rel) -> *)
+(*                   var=None && eq_constr req rel *)
+(*                   | _ -> false) args in *)
+(*         let add_m = *)
+(*           try default_morphism ~filter:is_endomorphism add *)
+(*           with Not_found -> *)
+(*             error "ring addition should be declared as a morphism" in *)
+(*         let mul_m = *)
+(*           try default_morphism ~filter:is_endomorphism mul *)
+(*           with Not_found -> *)
+(*             error "ring multiplication should be declared as a morphism" in *)
+(*         let op_morph = *)
+(*           match opp with *)
+(*             | Some opp -> *)
+(*             (let opp_m = *)
+(*               try default_morphism ~filter:is_endomorphism opp *)
+(*               with Not_found -> *)
+(*                 error "ring opposite should be declared as a morphism" in *)
+(*              let op_morph = *)
+(*                op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in *)
+(*              msgnl *)
+(*                (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++   *)
+(*                str"and morphisms \""++pr_constr add_m.morphism_theory++ *)
+(*                str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++ *)
+(*                str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ *)
+(*                str"\""); *)
+(*              op_morph) *)
+(*             | None -> *)
+(*             (msgnl *)
+(*               (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++   *)
+(*                str"and morphisms \""++pr_constr add_m.morphism_theory++ *)
+(*                str"\""++spc()++str"and \""++ *)
+(*                pr_constr mul_m.morphism_theory++str"\""); *)
+(*             op_smorph r add mul req add_m.lem mul_m.lem) in *)
+(*         (setoid,op_morph) *)
+
+let ring_equality (r,add,mul,opp,req) =
+  match kind_of_term req with
+    | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) ->
+	let setoid = lapp coq_eq_setoid [|r|] in
+	let op_morph =
+	  match opp with
               Some opp -> lapp coq_eq_morph [|r;add;mul;opp|]
             | None -> lapp coq_eq_smorph [|r;add;mul|] in
-        (setoid,op_morph)
-    | Relation rel ->
-        let setoid = setoid_of_relation rel in
-        let is_endomorphism = function
-            { args=args } -> List.for_all
-                (function (var,Relation rel) ->
-                  var=None && eq_constr req rel
-                  | _ -> false) args in
-        let add_m =
-          try default_morphism ~filter:is_endomorphism add
+	  (setoid,op_morph)
+    | _ ->
+	let setoid = setoid_of_relation (Global.env ()) r req in
+	let signature = [Some (r,req);Some (r,req);Some(r,req)] in
+	let add_m, add_m_lem =
+	  try Class_tactics.default_morphism signature add
           with Not_found ->
             error "ring addition should be declared as a morphism" in
-        let mul_m =
-          try default_morphism ~filter:is_endomorphism mul
+	let mul_m, mul_m_lem =
+          try Class_tactics.default_morphism signature mul
           with Not_found ->
             error "ring multiplication should be declared as a morphism" in
         let op_morph =
           match opp with
             | Some opp ->
-            (let opp_m =
-              try default_morphism ~filter:is_endomorphism opp
-              with Not_found ->
-                error "ring opposite should be declared as a morphism" in
-             let op_morph =
-               op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in
-             msgnl
-               (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++  
-               str"and morphisms \""++pr_constr add_m.morphism_theory++
-               str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++
-               str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++
-               str"\"");
-             op_morph)
+		(let opp_m,opp_m_lem =
+		  try Class_tactics.default_morphism (List.tl signature) opp
+		  with Not_found ->
+                    error "ring opposite should be declared as a morphism" in
+		let op_morph =
+		  op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
+		  msgnl
+		    (str"Using setoid \""++pr_constr req++str"\""++spc()++  
+			str"and morphisms \""++pr_constr add_m ++
+			str"\","++spc()++ str"\""++pr_constr mul_m++
+			str"\""++spc()++str"and \""++pr_constr opp_m++
+			str"\"");
+		  op_morph)
             | None ->
-            (msgnl
-              (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++  
-               str"and morphisms \""++pr_constr add_m.morphism_theory++
-               str"\""++spc()++str"and \""++
-               pr_constr mul_m.morphism_theory++str"\"");
-            op_smorph r add mul req add_m.lem mul_m.lem) in
-        (setoid,op_morph)
-
+		(msgnl
+		    (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++  
+			str"and morphisms \""++pr_constr add_m ++
+			str"\""++spc()++str"and \""++
+			pr_constr mul_m++str"\"");
+		 op_smorph r add mul req add_m_lem mul_m_lem) in
+          (setoid,op_morph)
+	    
 let build_setoid_params r add mul opp req eqth =
   match eqth with
       Some th -> th
-    | None -> default_ring_equality (r,add,mul,opp,req)
+    | None -> ring_equality (r,add,mul,opp,req)
 
 let dest_ring env sigma th_spec =
   let th_typ = Retyping.get_type_of env sigma th_spec in
@@ -980,25 +1029,19 @@ let (ftheory_to_obj, obj_to_ftheory) =
       classify_function = (fun (_,x) -> Substitute x);
       export_function = export_th }
 
-let default_field_equality r inv req =
-  let is_setoid = function
-      {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _} -> true
-    | _ -> false in
-  match default_relation_for_carrier ~filter:is_setoid r with
-      Leibniz _ ->
+let field_equality r inv req =
+  match kind_of_term req with
+    | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) ->
         mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|])
-    | Relation rel ->
-        let is_endomorphism = function
-            { args=args } -> List.for_all
-                (function (var,Relation rel) ->
-                  var=None && eq_constr req rel
-                  | _ -> false) args in
-        let inv_m =
-          try default_morphism ~filter:is_endomorphism inv
+    | _ ->
+	let _setoid = setoid_of_relation (Global.env ()) r req in
+	let signature = [Some (r,req);Some(r,req)] in
+	let inv_m, inv_m_lem =
+	  try Class_tactics.default_morphism signature inv
           with Not_found ->
             error "field inverse should be declared as a morphism" in
-        inv_m.lem
-
+	  inv_m_lem
+	    
 let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odiv =
   check_required_library (cdir@["Field_tac"]);
   let env = Global.env() in
@@ -1011,7 +1054,7 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odi
   let (pow_tac, pspec) = interp_power env power in 
   let sspec = interp_sign env sign in
   let dspec = interp_div env odiv in
-  let inv_m = default_field_equality r inv req in
+  let inv_m = field_equality r inv req in
   let rk = reflect_coeff morphth in
   let params =
     exec_tactic env 9 (field_ltac"field_lemmas")