Ajout d'un Ring pour setoides

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

5 files changed, 434 insertions, 121 deletions

diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 706b3a38d3..19b8534d1d 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -71,7 +71,7 @@ let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth
   ainv_l =
   begin
     (try
-       Ring.add_theory true true a aplus amult aone azero aopp aeq rth
+       Ring.add_theory true true false a None None None aplus amult aone azero (Some aopp) aeq rth
          Quote.ConstrSet.empty
      with | UserError("Add Semi Ring",_) -> ());
     let th = mkApp ((constant ["Field_Theory"] "Build_Field_Theory"),
diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v
index c94dce065e..88e609e3f8 100644
--- a/contrib/ring/Ring.v
+++ b/contrib/ring/Ring.v
@@ -25,11 +25,11 @@ Syntax tactic level 0:
  
 Grammar vernac vernac : ast := 
   addring [ "Add" "Ring" 
-      	     constrarg($a) constrarg($aplus) constrarg($amult) constrarg($aone)
-      	     constrarg($azero) constrarg($aopp) constrarg($aeq) constrarg($t)
-      	     "[" ne_constrarg_list($l) "]" "." ] 
+     constrarg($a) constrarg($aplus) constrarg($amult) constrarg($aone)
+     constrarg($azero) constrarg($aopp) constrarg($aeq) constrarg($t)
+     "[" ne_constrarg_list($l) "]" "." ] 
   -> [(AddRing $a $aplus $amult $aone $azero $aopp $aeq $t
-      	 ($LIST $l))]
+     ($LIST $l))]
 
 | addsemiring [ "Add" "Semi" "Ring" 
       	       	 constrarg($a) constrarg($aplus) constrarg($amult) 
@@ -49,6 +49,18 @@ Grammar vernac vernac : ast :=
                  constrarg($aone) constrarg($azero) constrarg($aeq) 
                  constrarg($t) "." ] 
   -> [(AddAbstractSemiRing $a $aplus $amult $aone $azero $aeq $t )]
+| addsetoidring [ "Add" "Setoid" "Ring"
+      	    constrarg($a) constrarg($aequiv) constrarg($asetth) constrarg($aplus) constrarg($amult) 
+	    constrarg($aone) constrarg($azero) constrarg($aopp) constrarg($aeq) constrarg($pm)
+	    constrarg($mm) constrarg($om) constrarg($t) "[" ne_constrarg_list($l) "]" "." ] 
+  -> [(AddSetoidRing $a $aequiv $asetth $aplus $amult $aone $azero $aopp $aeq $pm $mm $om $t
+      	 ($LIST $l))]
+| addsetoidsemiring [ "Add" "Semi" "Setoid" "Ring" 
+      	  constrarg($a) constrarg($aequiv) constrarg($asetth) constrarg($aplus)
+	  constrarg($amult) constrarg($aone) constrarg($azero) constrarg($aeq) 
+          constrarg($pm) constrarg($mm) constrarg($t) "[" ne_constrarg_list($l) "]" "." ] 
+  -> [(AddSemiRing $a $aequiv $asetth $aplus $amult $aone $azero $aeq $pm $mm $t
+      	   ($LIST $l))]
 .
 
 (* As an example, we provide an instantation for bool. *)
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index 94b5093c70..f44f554e0e 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -457,6 +457,7 @@ Trivial.
 Elim (varlist_lt v v0); Simpl.
 Repeat Rewrite ics_aux_ok.
 Rewrite H; Simpl; Rewrite ics_aux_ok; EAuto.
+
 Rewrite ics_aux_ok; Rewrite H0; Repeat Rewrite ics_aux_ok; Simpl; EAuto.
 
 (* monom and varlist *)
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index 867ab22fbe..8b4a0f95d3 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -58,7 +58,6 @@ Variable Aeq : A -> A -> bool.
 Record Semi_Ring_Theory : Prop :=
 { SR_plus_sym  : (n,m:A)[| n + m == m + n |];
   SR_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |];
-
   SR_mult_sym : (n,m:A)[| n*m == m*n |];
   SR_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |];
   SR_plus_zero_left :(n:A)[| 0 + n == n|];
@@ -81,8 +80,9 @@ Local mult_zero_left := (SR_mult_zero_left T).
 Local distr_left := (SR_distr_left T).
 Local plus_reg_left := (SR_plus_reg_left T).
 
-Hints Resolve  plus_sym  plus_assoc  mult_sym mult_assoc plus_zero_left
-  mult_one_left mult_zero_left distr_left plus_reg_left.
+Hints Resolve  plus_sym plus_assoc mult_sym mult_assoc
+  plus_zero_left mult_one_left mult_zero_left distr_left
+  plus_reg_left.
 
 (* Lemmas whose form is x=y are also provided in form y=x because Auto does
   not symmetry *) 
@@ -180,7 +180,7 @@ Record Ring_Theory : Prop :=
   Th_plus_zero_left :(n:A)[| 0 + n == n|];
   Th_mult_one_left : (n:A)[| 1*n == n |];
   Th_opp_def : (n:A) [| n + (-n) == 0 |];
-  Th_distr_left   : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
+  Th_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
   Th_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y
 }.
 
@@ -195,8 +195,8 @@ Local mult_one_left := (Th_mult_one_left T).
 Local opp_def := (Th_opp_def T).
 Local distr_left := (Th_distr_left T).
 
-Hints Resolve plus_sym plus_assoc mult_sym mult_assoc plus_zero_left mult_one_left
-  opp_def distr_left.
+Hints Resolve plus_sym plus_assoc mult_sym mult_assoc
+  plus_zero_left mult_one_left opp_def distr_left.
 
 (* Lemmas whose form is x=y are also provided in form y=x because Auto does
   not symmetry *) 
@@ -285,7 +285,7 @@ Hints Resolve Th_opp_mult_left.
 Lemma Th_opp_mult_left2 : (x,y:A)[| (-x)*y == -(x*y)  |].
 Symmetry; EAuto. Save.
 
-Lemma Th_mult_zero_right : (n:A)[|  n*0 == 0|].
+Lemma Th_mult_zero_right : (n:A)[| n*0 == 0|].
 Intro; Elim mult_sym; EAuto.
 Save.
 
@@ -326,7 +326,7 @@ Apply (aux2 1![| x + y |]);
 | Auto ].
 Save.
 
-Lemma Th_plus_permute_opp: (n,m,p:A)[| (-m) + (n + p) == n + ((-m)+p) |].
+Lemma Th_plus_permute_opp: (n,m,p:A)[| (-m)+(n+p) == n+((-m)+p) |].
 EAuto. Save.
 
 Lemma Th_opp_opp : (n:A)[| -(-n) == n |].
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 0a70426ea5..fad760cba8 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -34,7 +34,7 @@ let mt_evd = Evd.empty
 let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com
 
 let constant dir s =
-  let dir = "Coq"::"ring"::dir in
+  let dir = "Coq"::dir in
   let id = id_of_string s in
   try 
     Declare.global_reference_in_absolute_module dir id
@@ -42,61 +42,93 @@ let constant dir s =
     anomaly ("Ring: cannot find "^
 	     (Nametab.string_of_qualid (Nametab.make_qualid dir id)))
 
-(* Ring_theory *)
-
-let coq_Ring_Theory = lazy (constant ["Ring_theory"] "Ring_Theory")
-let coq_Semi_Ring_Theory = lazy (constant ["Ring_theory"] "Semi_Ring_Theory")
-
-(* Ring_normalize *)
-let coq_SPplus = lazy (constant ["Ring_normalize"] "SPplus")
-let coq_SPmult = lazy (constant ["Ring_normalize"] "SPmult")
-let coq_SPvar = lazy (constant ["Ring_normalize"] "SPvar")
-let coq_SPconst = lazy (constant ["Ring_normalize"] "SPconst")
-let coq_Pplus = lazy (constant ["Ring_normalize"] "Pplus")
-let coq_Pmult = lazy (constant ["Ring_normalize"] "Pmult")
-let coq_Pvar = lazy (constant ["Ring_normalize"] "Pvar")
-let coq_Pconst = lazy (constant ["Ring_normalize"] "Pconst")
-let coq_Popp = lazy (constant ["Ring_normalize"] "Popp")
-let coq_interp_sp = lazy (constant ["Ring_normalize"] "interp_sp")
-let coq_interp_p = lazy (constant ["Ring_normalize"] "interp_p")
-let coq_interp_cs = lazy (constant ["Ring_normalize"] "interp_cs")
+(* Ring theory *)
+let coq_Ring_Theory = lazy (constant ["ring";"Ring_theory"] "Ring_Theory")
+let coq_Semi_Ring_Theory = lazy (constant ["ring";"Ring_theory"] "Semi_Ring_Theory")
+
+(* Setoid ring theory *)
+let coq_Setoid_Ring_Theory = lazy (constant ["ring";"Setoid_ring_theory"] "Setoid_Ring_Theory")
+let coq_Semi_Setoid_Ring_Theory = lazy (constant ["ring";"Setoid_ring_theory"] "Semi_Setoid_Ring_Theory")
+
+(* Ring normalize *)
+let coq_SPplus = lazy (constant ["ring";"Ring_normalize"] "SPplus")
+let coq_SPmult = lazy (constant ["ring";"Ring_normalize"] "SPmult")
+let coq_SPvar = lazy (constant ["ring";"Ring_normalize"] "SPvar")
+let coq_SPconst = lazy (constant ["ring";"Ring_normalize"] "SPconst")
+let coq_Pplus = lazy (constant ["ring";"Ring_normalize"] "Pplus")
+let coq_Pmult = lazy (constant ["ring";"Ring_normalize"] "Pmult")
+let coq_Pvar = lazy (constant ["ring";"Ring_normalize"] "Pvar")
+let coq_Pconst = lazy (constant ["ring";"Ring_normalize"] "Pconst")
+let coq_Popp = lazy (constant ["ring";"Ring_normalize"] "Popp")
+let coq_interp_sp = lazy (constant ["ring";"Ring_normalize"] "interp_sp")
+let coq_interp_p = lazy (constant ["ring";"Ring_normalize"] "interp_p")
+let coq_interp_cs = lazy (constant ["ring";"Ring_normalize"] "interp_cs")
 let coq_spolynomial_simplify = 
-  lazy (constant ["Ring_normalize"] "spolynomial_simplify")
+  lazy (constant ["ring";"Ring_normalize"] "spolynomial_simplify")
 let coq_polynomial_simplify = 
-  lazy (constant ["Ring_normalize"] "polynomial_simplify")
+  lazy (constant ["ring";"Ring_normalize"] "polynomial_simplify")
 let coq_spolynomial_simplify_ok = 
-  lazy (constant ["Ring_normalize"] "spolynomial_simplify_ok")
+  lazy (constant ["ring";"Ring_normalize"] "spolynomial_simplify_ok")
 let coq_polynomial_simplify_ok = 
-  lazy (constant ["Ring_normalize"] "polynomial_simplify_ok")
-
-(* Ring_abstract *)
-let coq_ASPplus = lazy (constant ["Ring_abstract"] "ASPplus")
-let coq_ASPmult = lazy (constant ["Ring_abstract"] "ASPmult")
-let coq_ASPvar = lazy (constant ["Ring_abstract"] "ASPvar")
-let coq_ASP0 = lazy (constant ["Ring_abstract"] "ASP0")
-let coq_ASP1 = lazy (constant ["Ring_abstract"] "ASP1")
-let coq_APplus = lazy (constant ["Ring_abstract"] "APplus")
-let coq_APmult = lazy (constant ["Ring_abstract"] "APmult")
-let coq_APvar = lazy (constant ["Ring_abstract"] "APvar")
-let coq_AP0 = lazy (constant ["Ring_abstract"] "AP0")
-let coq_AP1 = lazy (constant ["Ring_abstract"] "AP1")
-let coq_APopp = lazy (constant ["Ring_abstract"] "APopp")
+  lazy (constant ["ring";"Ring_normalize"] "polynomial_simplify_ok")
+
+(* Setoid theory *)
+let coq_Setoid_Theory = lazy(constant ["setoid";"Setoid_replace"] "Setoid_Theory")
+
+let coq_seq_refl = lazy(constant ["setoid";"Setoid_replace"] "Seq_refl")
+let coq_seq_sym = lazy(constant ["setoid";"Setoid_replace"] "Seq_sym")
+let coq_seq_trans = lazy(constant ["setoid";"Setoid_replace"] "Seq_trans")
+
+(* Setoid Ring normalize *)
+let coq_SetSPplus = lazy (constant ["ring";"Ring_normalize"] "SetSPplus")
+let coq_SetSPmult = lazy (constant ["ring";"Ring_normalize"] "SetSPmult")
+let coq_SetSPvar = lazy (constant ["ring";"Ring_normalize"] "SetSPvar")
+let coq_SetSPconst = lazy (constant ["ring";"Ring_normalize"] "SetSPconst")
+let coq_SetPplus = lazy (constant ["ring";"Ring_normalize"] "SetPplus")
+let coq_SetPmult = lazy (constant ["ring";"Ring_normalize"] "SetPmult")
+let coq_SetPvar = lazy (constant ["ring";"Ring_normalize"] "SetPvar")
+let coq_SetPconst = lazy (constant ["ring";"Ring_normalize"] "SetPconst")
+let coq_SetPopp = lazy (constant ["ring";"Ring_normalize"] "SetPopp")
+let coq_interp_setsp = lazy (constant ["ring";"Ring_normalize"] "interp_setsp")
+let coq_interp_setp = lazy (constant ["ring";"Ring_normalize"] "interp_setp")
+let coq_interp_setcs = lazy (constant ["ring";"Ring_normalize"] "interp_cs")
+let coq_setspolynomial_simplify = 
+  lazy (constant ["ring";"Ring_normalize"] "setspolynomial_simplify")
+let coq_setpolynomial_simplify = 
+  lazy (constant ["ring";"Ring_normalize"] "setpolynomial_simplify")
+let coq_setspolynomial_simplify_ok = 
+  lazy (constant ["ring";"Ring_normalize"] "setspolynomial_simplify_ok")
+let coq_setpolynomial_simplify_ok = 
+  lazy (constant ["ring";"Ring_normalize"] "setpolynomial_simplify_ok")
+
+(* Ring abstract *)
+let coq_ASPplus = lazy (constant ["ring";"Ring_abstract"] "ASPplus")
+let coq_ASPmult = lazy (constant ["ring";"Ring_abstract"] "ASPmult")
+let coq_ASPvar = lazy (constant ["ring";"Ring_abstract"] "ASPvar")
+let coq_ASP0 = lazy (constant ["ring";"Ring_abstract"] "ASP0")
+let coq_ASP1 = lazy (constant ["ring";"Ring_abstract"] "ASP1")
+let coq_APplus = lazy (constant ["ring";"Ring_abstract"] "APplus")
+let coq_APmult = lazy (constant ["ring";"Ring_abstract"] "APmult")
+let coq_APvar = lazy (constant ["ring";"Ring_abstract"] "APvar")
+let coq_AP0 = lazy (constant ["ring";"Ring_abstract"] "AP0")
+let coq_AP1 = lazy (constant ["ring";"Ring_abstract"] "AP1")
+let coq_APopp = lazy (constant ["ring";"Ring_abstract"] "APopp")
 let coq_interp_asp = 
-  lazy (constant ["Ring_abstract"] "interp_asp")
+  lazy (constant ["ring";"Ring_abstract"] "interp_asp")
 let coq_interp_ap = 
-  lazy (constant ["Ring_abstract"] "interp_ap")
+  lazy (constant ["ring";"Ring_abstract"] "interp_ap")
  let coq_interp_acs = 
-  lazy (constant ["Ring_abstract"] "interp_acs")
+  lazy (constant ["ring";"Ring_abstract"] "interp_acs")
 let coq_interp_sacs = 
-  lazy (constant ["Ring_abstract"] "interp_sacs")
+  lazy (constant ["ring";"Ring_abstract"] "interp_sacs")
 let coq_aspolynomial_normalize = 
-  lazy (constant ["Ring_abstract"] "aspolynomial_normalize")
+  lazy (constant ["ring";"Ring_abstract"] "aspolynomial_normalize")
 let coq_apolynomial_normalize = 
-  lazy (constant ["Ring_abstract"] "apolynomial_normalize")
+  lazy (constant ["ring";"Ring_abstract"] "apolynomial_normalize")
 let coq_aspolynomial_normalize_ok = 
-  lazy (constant ["Ring_abstract"] "aspolynomial_normalize_ok")
+  lazy (constant ["ring";"Ring_abstract"] "aspolynomial_normalize_ok")
 let coq_apolynomial_normalize_ok = 
-  lazy (constant ["Ring_abstract"] "apolynomial_normalize_ok")
+  lazy (constant ["ring";"Ring_abstract"] "apolynomial_normalize_ok")
 
 (* Logic --> to be found in Coqlib *)
 open Coqlib
@@ -113,17 +145,27 @@ module OperSet =
   Set.Make (struct 
 	      type t = global_reference
 	      let compare = (Pervasives.compare : t->t->int)
-	    end)	
+	    end)
+
+type morph =
+    { plusm : constr;
+      multm : constr;
+      oppm : constr;
+    }
 
 type theory =
     { th_ring : bool;                  (* false for a semi-ring *)
       th_abstract : bool;
+      th_setoid : bool;                (* true for a setoid ring *)
+      th_equiv : constr option;
+      th_setoid_th : constr option;
+      th_morph : morph option;
       th_a : constr;                   (* e.g. nat *)
       th_plus : constr;
       th_mult : constr;
       th_one : constr;
       th_zero : constr;
-      th_opp : constr;                 (* Not used if semi-ring *)
+      th_opp : constr option;          (* None if semi-ring *)
       th_eq : constr;
       th_t : constr;                   (* e.g. NatTheory *)
       th_closed : ConstrSet.t;         (* e.g. [S; O] *)
@@ -174,42 +216,66 @@ let guess_theory a =
 	 prterm a; 'fNL;
 	 'sTR "Use Add [Semi] Ring to declare it">]
 
+(* Looks up an option *)
+
+let unbox = function 
+  | Some w -> w
+  | None -> anomaly "Ring : Not in case of a setoid ring."
+
 (* Add a Ring or a Semi-Ring to the database after a type verification *)
 
-let add_theory want_ring want_abstract a aplus amult aone azero aopp aeq t cset = 
+let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus amult aone azero aopp aeq t cset = 
   if theories_map_mem a then errorlabstrm "Add Semi Ring" 
-    [< 'sTR "A (Semi-)Ring Structure is already declared for "; prterm a >];
+    [< 'sTR "A (Semi-)(Setoid-)Ring Structure is already declared for "; prterm a >];
   let env = Global.env () in
-  if (want_ring & 
-      not (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
-	     (mkApp (Lazy.force coq_Ring_Theory, [| a; aplus; amult;
-			aone; azero; aopp; aeq |])))) then
-    errorlabstrm "addring" [< 'sTR "Not a valid Ring theory" >];
-  if (not want_ring &
-      not (is_conv  env Evd.empty (Typing.type_of env Evd.empty t) 
-	     (mkApp (Lazy.force coq_Semi_Ring_Theory, [| a; 
-			aplus; amult; aone; azero; aeq |])))) then 
-    errorlabstrm "addring" [< 'sTR "Not a valid Semi-Ring theory" >];
-  Lib.add_anonymous_leaf
-    (theory_to_obj 
-       (a, { th_ring = want_ring;
-	     th_abstract = want_abstract;
-	     th_a = a;
-	     th_plus = aplus;
-	     th_mult = amult;
-	     th_one = aone;
-	     th_zero = azero;
-	     th_opp = aopp;
-	     th_eq = aeq;
-	     th_t = t;
-	     th_closed = cset }))
+    if (want_ring & want_setoid &
+	(not (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
+		(mkApp (Lazy.force coq_Setoid_Ring_Theory, 
+			[| a; (unbox aequiv); aplus; amult; aone; azero; (unbox aopp); aeq|])))) &
+	(not (is_conv env Evd.empty (Typing.type_of env Evd.empty (unbox asetth))
+		(mkApp ((Lazy.force coq_Setoid_Theory), [| a; (unbox aequiv) |]))))) then 
+      errorlabstrm "addring" [< 'sTR "Not a valid Setoid-Ring theory" >];
+    if (not want_ring & want_setoid &
+	(not (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
+		(mkApp (Lazy.force coq_Semi_Setoid_Ring_Theory, 
+			[| a; (unbox aequiv); aplus; amult; aone; azero; aeq|])))) &
+	(not (is_conv env Evd.empty (Typing.type_of env Evd.empty (unbox asetth))
+		(mkApp ((Lazy.force coq_Setoid_Theory), [| a; (unbox aequiv) |]))))) then 
+      errorlabstrm "addring" [< 'sTR "Not a valid Semi-Setoid-Ring theory" >];
+    if (want_ring & not want_setoid &
+	not (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
+	       (mkApp (Lazy.force coq_Ring_Theory, 
+		       [| a; aplus; amult; aone; azero; (unbox aopp); aeq |])))) then
+      errorlabstrm "addring" [< 'sTR "Not a valid Ring theory" >];
+    if (not want_ring & not want_setoid &
+	not (is_conv  env Evd.empty (Typing.type_of env Evd.empty t) 
+	       (mkApp (Lazy.force coq_Semi_Ring_Theory, 
+		       [| a; aplus; amult; aone; azero; aeq |])))) then 
+      errorlabstrm "addring" [< 'sTR "Not a valid Semi-Ring theory" >];
+    Lib.add_anonymous_leaf
+      (theory_to_obj 
+	 (a, { th_ring = want_ring;
+	       th_abstract = want_abstract;
+	       th_setoid = want_setoid;
+	       th_equiv = aequiv;
+	       th_setoid_th = asetth;
+	       th_morph = amorph;
+	       th_a = a;
+	       th_plus = aplus;
+	       th_mult = amult;
+	       th_one = aone;
+	       th_zero = azero;
+	       th_opp = aopp;
+	       th_eq = aeq;
+	       th_t = t;
+	       th_closed = cset }))
 
 (* The vernac commands "Add Ring" and "Add Semi Ring" *)
 (* see file Ring.v for examples of this command *)
 
 let constr_of_comarg = function 
   | VARG_CONSTR c -> constr_of c
-  | _ -> anomaly "Add (Semi) Ring"
+  | _ -> anomaly "Add (Semi) (Setoid) Ring"
   
 let cset_of_comarg_list l = 
   List.fold_right ConstrSet.add (List.map constr_of_comarg l) ConstrSet.empty
@@ -220,13 +286,16 @@ let _ =
        | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult)
 	 ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aeq)
 	 ::(VARG_CONSTR t)::l -> 
-	   (fun () -> (add_theory false false
+	   (fun () -> (add_theory false false false
 			 (constr_of a)
+			 None
+			 None
+			 None
 			 (constr_of aplus)
 			 (constr_of amult)
 			 (constr_of aone)
 			 (constr_of azero)
-			 mkImplicit
+			 None
 			 (constr_of aeq)
 			 (constr_of t)
 			 (cset_of_comarg_list l)))
@@ -238,31 +307,87 @@ let _ =
        | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult)
 	 ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aopp)
 	 ::(VARG_CONSTR aeq)::(VARG_CONSTR t)::l -> 
-	   (fun () -> (add_theory true false
+	   (fun () -> (add_theory true false false
 			 (constr_of a)
+			 None
+			 None
+			 None
 			 (constr_of aplus)
 			 (constr_of amult)
 			 (constr_of aone)
 			 (constr_of azero)
-			 (constr_of aopp)
+			 (Some (constr_of aopp))
 			 (constr_of aeq)
 			 (constr_of t)
 			 (cset_of_comarg_list l)))
        | _ -> anomaly "AddRing")
     
 let _ = 
+  vinterp_add "AddSetoidRing"
+    (function 
+       | (VARG_CONSTR a)::(VARG_CONSTR aequiv)::(VARG_CONSTR asetth)::(VARG_CONSTR aplus)
+	 ::(VARG_CONSTR amult)::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aopp)
+	 ::(VARG_CONSTR aeq)::(VARG_CONSTR pm)::(VARG_CONSTR mm)::(VARG_CONSTR om)
+	 ::(VARG_CONSTR t)::l -> 
+	   (fun () -> (add_theory true false true
+			 (constr_of a)
+			 (Some (constr_of aequiv))
+			 (Some (constr_of asetth))
+			 (Some {
+			    plusm = (constr_of pm);
+			    multm = (constr_of mm);
+			    oppm = (constr_of om)})
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 (Some (constr_of aopp))
+			 (constr_of aeq)
+			 (constr_of t)
+			 (cset_of_comarg_list l)))
+       | _ -> anomaly "AddSetoidRing")
+    
+let _ = 
+  vinterp_add "AddSemiSetoidRing"
+    (function 
+       | (VARG_CONSTR a)::(VARG_CONSTR aequiv)::(VARG_CONSTR asetth)::(VARG_CONSTR aplus)
+	 ::(VARG_CONSTR amult)::(VARG_CONSTR aone)::(VARG_CONSTR azero)
+	 ::(VARG_CONSTR aeq)::(VARG_CONSTR pm)::(VARG_CONSTR mm)::(VARG_CONSTR om)
+	 ::(VARG_CONSTR t)::l -> 
+	   (fun () -> (add_theory false false true
+			 (constr_of a)
+			 (Some (constr_of aequiv))
+			 (Some (constr_of asetth))
+			 (Some {
+			    plusm = (constr_of pm);
+			    multm = (constr_of mm);
+			    oppm = (constr_of om)})
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 None
+			 (constr_of aeq)
+			 (constr_of t)
+			 (cset_of_comarg_list l)))
+       | _ -> anomaly "AddSemiSetoidRing")
+    
+let _ = 
   vinterp_add "AddAbstractSemiRing"
     (function 
        | [VARG_CONSTR a; VARG_CONSTR aplus; 
 	  VARG_CONSTR amult; VARG_CONSTR aone;
 	  VARG_CONSTR azero; VARG_CONSTR aeq; VARG_CONSTR t] -> 
-	   (fun () -> (add_theory false false
+	   (fun () -> (add_theory false true false
 			 (constr_of a)
+			 None
+			 None
+			 None
 			 (constr_of aplus)
 			 (constr_of amult)
 			 (constr_of aone)
 			 (constr_of azero)
-			 mkImplicit
+			 None
 			 (constr_of aeq)
 			 (constr_of t)
 			 ConstrSet.empty))
@@ -275,13 +400,16 @@ let _ =
 	   VARG_CONSTR amult; VARG_CONSTR aone;
 	   VARG_CONSTR azero; VARG_CONSTR aopp; 
 	   VARG_CONSTR aeq; VARG_CONSTR t ] -> 
-	   (fun () -> (add_theory true true
+	   (fun () -> (add_theory true true false
 			 (constr_of a)
+			 None
+			 None
+			 None
 			 (constr_of aplus)
 			 (constr_of amult)
 			 (constr_of aone)
 			 (constr_of azero)
-			 (constr_of aopp)
+			 (Some (constr_of aopp))
 			 (constr_of aeq)
 			 (constr_of t)
 			 ConstrSet.empty))
@@ -370,10 +498,10 @@ let build_polynom gl th lc =
       (* The special case of Zminus *)
       | IsApp (binop, [|c1; c2|])
 	  when pf_conv_x gl c (mkAppA [| th.th_plus; c1; 
-	                                 mkAppA [| th.th_opp; c2 |] |]) ->
+	                                 mkAppA [| (unbox th.th_opp); c2 |] |]) ->
 	    mkAppA [| Lazy.force coq_Pplus; th.th_a; aux c1;
 	              mkAppA [| Lazy.force coq_Popp; th.th_a; aux c2 |] |]
-      | IsApp (unop, [|c1|]) when pf_conv_x gl unop th.th_opp ->
+      | IsApp (unop, [|c1|]) when pf_conv_x gl unop (unbox th.th_opp) ->
 	  mkAppA [| Lazy.force coq_Popp; th.th_a; aux c1 |]
       | _ when closed_under th.th_closed c ->
 	  mkAppA [| Lazy.force coq_Pconst; th.th_a; c |]
@@ -394,7 +522,7 @@ let build_polynom gl th lc =
   List.map 
     (fun p -> 
        (mkAppA [| Lazy.force coq_interp_p;
-		  th.th_a; th.th_plus; th.th_mult; th.th_zero; th.th_opp;
+		  th.th_a; th.th_plus; th.th_mult; th.th_zero; (unbox th.th_opp);
 		  v; p |],
 	mkAppA [| Lazy.force coq_interp_cs;
 		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
@@ -402,10 +530,10 @@ let build_polynom gl th lc =
 		    (mkAppA [| Lazy.force coq_polynomial_simplify; 
 			       th.th_a; th.th_plus; th.th_mult; 
 			       th.th_one; th.th_zero; 
-			       th.th_opp; th.th_eq; p |]) |],
+			       (unbox th.th_opp); th.th_eq; p |]) |],
 	mkAppA [| Lazy.force coq_polynomial_simplify_ok;
 		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
-		  th.th_opp; th.th_eq; v; th.th_t; p |]))
+		  (unbox th.th_opp); th.th_eq; v; th.th_t; p |]))
     lp
 
 (*
@@ -486,10 +614,10 @@ let build_apolynom gl th lc =
       (* The special case of Zminus *)
       | IsApp (binop, [|c1; c2|]) 
 	  when pf_conv_x gl c (mkAppA [| th.th_plus; c1; 
-	                                 mkAppA [| th.th_opp; c2 |] |]) ->
+	                                 mkAppA [|(unbox th.th_opp); c2 |] |]) ->
 	    mkAppA [| Lazy.force coq_APplus; aux c1;
 	              mkAppA [| Lazy.force coq_APopp; aux c2 |] |]
-      | IsApp (unop, [|c1|]) when pf_conv_x gl unop th.th_opp ->
+      | IsApp (unop, [|c1|]) when pf_conv_x gl unop (unbox th.th_opp) ->
 	  mkAppA [| Lazy.force coq_APopp; aux c1 |]
       | _ when pf_conv_x gl c th.th_zero -> Lazy.force coq_AP0
       | _ when pf_conv_x gl c th.th_one -> Lazy.force coq_AP1
@@ -511,18 +639,139 @@ let build_apolynom gl th lc =
     (fun p -> 
        (mkAppA [| Lazy.force coq_interp_ap;
 		  th.th_a; th.th_plus; th.th_mult; th.th_one; 
-		  th.th_zero; th.th_opp; v; p |],
+		  th.th_zero; (unbox th.th_opp); v; p |],
 	mkAppA [| Lazy.force coq_interp_sacs;
 		  th.th_a; th.th_plus; th.th_mult; 
-		  th.th_one; th.th_zero; th.th_opp; v; 
+		  th.th_one; th.th_zero; (unbox th.th_opp); v; 
 		  pf_reduce cbv_betadeltaiota gl 
 		    (mkAppA [| Lazy.force coq_apolynomial_normalize; p |]) |],
 	mkAppA [| Lazy.force coq_apolynomial_normalize_ok;
 		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; 
-		  th.th_opp; th.th_eq; v; th.th_t; p |]))
+		  (unbox th.th_opp); th.th_eq; v; th.th_t; p |]))
     lp
     
-module SectionPathSet = 
+(*
+   gl : goal sigma
+   th : setoid ring theory (concrete)
+   cl : constr list [c1; c2; ...]
+ 
+Builds 
+   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] 
+  where c'i is convertible with ci and
+  c'i_eq_c''i is a proof of equality of c'i and c''i
+
+*)
+
+let build_setpolynom gl th lc =
+  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  let varlist = ref ([] : constr list) in (* list of variables *)
+  let counter = ref 1 in (* number of variables created + 1 *)
+  let rec aux c = 
+    match (kind_of_term (strip_outer_cast c)) with 
+      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
+	  mkAppA [| Lazy.force coq_SetPplus; th.th_a; aux c1; aux c2 |]
+      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
+	  mkAppA [| Lazy.force coq_SetPmult; th.th_a; aux c1; aux c2 |]
+      (* The special case of Zminus *)
+      | IsApp (binop, [|c1; c2|])
+	  when pf_conv_x gl c (mkAppA [| th.th_plus; c1; 
+	                                 mkAppA [|(unbox th.th_opp); c2 |] |]) ->
+	    mkAppA [| Lazy.force coq_SetPplus; th.th_a; aux c1;
+	              mkAppA [| Lazy.force coq_SetPopp; th.th_a; aux c2 |] |]
+      | IsApp (unop, [|c1|]) when pf_conv_x gl unop (unbox th.th_opp) ->
+	  mkAppA [| Lazy.force coq_SetPopp; th.th_a; aux c1 |]
+      | _ when closed_under th.th_closed c ->
+	  mkAppA [| Lazy.force coq_SetPconst; th.th_a; c |]
+      | _ -> 
+	  try Hashtbl.find varhash c 
+	  with Not_found -> 
+	    let newvar = mkAppA [| Lazy.force coq_SetPvar; th.th_a; 
+				   (path_of_int !counter) |] in
+	    begin 
+	      incr counter;
+	      varlist := c :: !varlist;
+	      Hashtbl.add varhash c newvar;
+	      newvar
+	    end
+  in
+  let lp = List.map aux lc in
+  let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
+  List.map 
+    (fun p -> 
+       (mkAppA [| Lazy.force coq_interp_setp;
+		  th.th_a; th.th_plus; th.th_mult; th.th_zero; (unbox th.th_opp);
+		  v; p |],
+	mkAppA [| Lazy.force coq_interp_setcs;
+		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
+		  pf_reduce cbv_betadeltaiota gl 
+		    (mkAppA [| Lazy.force coq_setpolynomial_simplify; 
+			       th.th_a; th.th_plus; th.th_mult; 
+			       th.th_one; th.th_zero; 
+			       (unbox th.th_opp); th.th_eq; p |]) |],
+	mkAppA [| Lazy.force coq_setpolynomial_simplify_ok;
+		  th.th_a; (unbox th.th_equiv); th.th_plus; th.th_mult; th.th_one;
+		  th.th_zero;(unbox th.th_opp); th.th_eq; v; th.th_t; (unbox th.th_setoid_th);
+		  (unbox th.th_morph).plusm; (unbox th.th_morph).multm;
+		  (unbox th.th_morph).oppm; p |]))
+    lp
+
+(*
+   gl : goal sigma
+   th : semi setoid ring theory (concrete)
+   cl : constr list [c1; c2; ...]
+ 
+Builds 
+   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ] 
+  where c'i is convertible with ci and
+  c'i_eq_c''i is a proof of equality of c'i and c''i
+
+*)
+
+let build_setspolynom gl th lc =
+  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  let varlist = ref ([] : constr list) in (* list of variables *)
+  let counter = ref 1 in (* number of variables created + 1 *)
+  let rec aux c = 
+    match (kind_of_term (strip_outer_cast c)) with 
+      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
+	  mkAppA [| Lazy.force coq_SetSPplus; th.th_a; aux c1; aux c2 |]
+      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
+	  mkAppA [| Lazy.force coq_SetSPmult; th.th_a; aux c1; aux c2 |]
+      | _ when closed_under th.th_closed c ->
+	  mkAppA [| Lazy.force coq_SetSPconst; th.th_a; c |]
+      | _ -> 
+	  try Hashtbl.find varhash c
+	  with Not_found ->
+	    let newvar = mkAppA [| Lazy.force coq_SetSPvar; th.th_a; 
+				   (path_of_int !counter) |] in
+	    begin 
+	      incr counter;
+	      varlist := c :: !varlist;
+	      Hashtbl.add varhash c newvar;
+	      newvar
+	    end
+  in
+  let lp = List.map aux lc in
+  let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
+  List.map
+    (fun p ->
+       (mkAppA [| Lazy.force coq_interp_setsp;
+		  th.th_a; th.th_plus; th.th_mult; th.th_zero;
+		  v; p |],
+	mkAppA [| Lazy.force coq_interp_setcs;
+		  th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
+		  pf_reduce cbv_betadeltaiota gl 
+		    (mkAppA [| Lazy.force coq_setspolynomial_simplify; 
+			       th.th_a; th.th_plus; th.th_mult; 
+			       th.th_one; th.th_zero; 
+			       th.th_eq; p |]) |],
+	mkAppA [| Lazy.force coq_setspolynomial_simplify_ok;
+		  th.th_a; (unbox th.th_equiv); th.th_plus; th.th_mult; th.th_one;
+		  th.th_zero; th.th_eq; v; th.th_t; (unbox th.th_setoid_th);
+		  (unbox th.th_morph).plusm; (unbox th.th_morph).multm; p |]))
+    lp
+
+module SectionPathSet =
   Set.Make(struct
 	     type t = section_path
 	     let compare = Pervasives.compare
@@ -544,6 +793,12 @@ let constants_to_unfold =
       path_of_string "Coq.ring.Ring_normalize.interp_m";
       path_of_string "Coq.ring.Ring_abstract.iacs_aux";
       path_of_string "Coq.ring.Ring_abstract.isacs_aux";
+      path_of_string "Coq.ring.Setoid_ring_normalize.interp_cs";
+      path_of_string "Coq.ring.Setoid_ring_normalize.interp_var";
+      path_of_string "Coq.ring.Setoid_ring_normalize.interp_vl";
+      path_of_string "Coq.ring.Setoid_ring_normalize.ics_aux";
+      path_of_string "Coq.ring.Setoid_ring_normalize.ivl_aux";
+      path_of_string "Coq.ring.Setoid_ring_normalize.interp_m";
     ]
 (*    SectionPathSet.empty *)
 
@@ -573,14 +828,19 @@ let raw_polynom th op lc gl =
      modifies t in a non-desired way *)
   let lc = sort_subterm gl lc in
   let ltriplets = 
-    if th.th_abstract then 
+    if th.th_setoid then
       if th.th_ring
-      then build_apolynom gl th lc
-      else build_aspolynom gl th lc
+      then build_setpolynom gl th lc
+      else build_setspolynom gl th lc
     else
-      if th.th_ring 
-      then build_polynom gl th lc
-      else build_spolynom gl th lc in 
+      if th.th_ring then
+	if th.th_abstract
+	then build_apolynom gl th lc
+	else build_polynom gl th lc
+      else
+	if th.th_abstract 
+	then build_aspolynom gl th lc
+	else build_spolynom gl th lc in 
   let polynom_tac = 
     List.fold_right2
       (fun ci (c'i, c''i, c'i_eq_c''i) tac ->
@@ -589,7 +849,20 @@ let raw_polynom th op lc gl =
 	 in
          if !term_quality && pf_conv_x gl c'''i ci then 
 	   tac (* convertible terms *)
-         else
+         else if th.th_setoid
+	 then
+           (tclORELSE 
+              (tclORELSE
+		 (h_exact c'i_eq_c''i)
+		 (h_exact (mkAppA
+			     [| (Lazy.force coq_seq_sym); 
+				th.th_a; (unbox th.th_equiv); (unbox th.th_setoid_th);
+				c'''i; ci; c'i_eq_c''i |])))
+	      (tclTHENS 
+		 (Setoid_replace.setoid_replace ci c'''i None)
+		 [ tac;
+                   h_exact c'i_eq_c''i ])) 
+	 else
            (tclORELSE
               (tclORELSE
 		 (h_exact c'i_eq_c''i)
@@ -600,7 +873,8 @@ let raw_polynom th op lc gl =
 		 (elim_type 
 		    (mkAppA [| build_coq_eqT (); th.th_a; c'''i; ci |]))
 		 [ tac;
-                   h_exact c'i_eq_c''i ]))) 
+                   h_exact c'i_eq_c''i ]))
+)
       lc ltriplets polynom_unfold_tac 
   in
   polynom_tac gl
@@ -617,6 +891,23 @@ let guess_eq_tac th =
 	      (apply (mkAppA [| build_coq_f_equal2 ();
 				th.th_a; th.th_a; th.th_a; 
 				th.th_mult |]))))))
+let guess_equiv_tac th = 
+  (tclORELSE (apply (mkAppA [|(Lazy.force coq_seq_refl);
+			      th.th_a; (unbox th.th_equiv);
+			      (unbox th.th_setoid_th)|]))
+     (tclTHEN 
+	polynom_unfold_tac
+	(tclREPEAT 
+	   (tclORELSE 
+	      (apply (unbox th.th_morph).plusm)
+	      (apply (unbox th.th_morph).multm)))))
+
+let match_with_equiv c = match (kind_of_term c) with
+  | IsApp (e,a) -> 
+      if (List.mem e (Setoid_replace.equiv_list ()))
+      then Some (decomp_app c)
+      else None
+  | _ -> None
 
 let polynom lc gl =
   match lc with 
@@ -634,20 +925,29 @@ let polynom lc gl =
 		 errorlabstrm "Ring :"
 		   [< 'sTR" All terms must have the same type" >];
 	       (tclTHEN (raw_polynom th None args) (guess_eq_tac th)) gl
-	   | _ -> 
-	       errorlabstrm "polynom :" 
-		 [< 'sTR" This goal is not an equality" >])
+	   | _ -> (match match_with_equiv (pf_concl gl) with
+		     | Some (equiv, c1::args) ->
+			 let t = (pf_type_of gl c1) in
+			 let th = (guess_theory t) in
+			   if List.exists 
+			     (fun c2 -> not (pf_conv_x gl t (pf_type_of gl c2))) args
+			   then 
+			     errorlabstrm "Ring :"
+			       [< 'sTR" All terms must have the same type" >];
+			   (tclTHEN (raw_polynom th None args) (guess_equiv_tac th)) gl		   
+		     | _ -> errorlabstrm "polynom :" 
+			 [< 'sTR" This goal is not an equality nor a setoid equivalence" >]))
     (* Elsewhere, guess the theory, check that all terms have the same type
        and apply raw_polynom *)
     | c :: lc' -> 
 	let t = pf_type_of gl c in 
 	let th = guess_theory t in 
-	if List.exists 
-	  (fun c1 -> not (pf_conv_x gl t (pf_type_of gl c1))) lc'
-	then 
-	  errorlabstrm "Ring :"
-	    [< 'sTR" All terms must have the same type" >];
-	(tclTHEN (raw_polynom th None lc) polynom_unfold_tac) gl
+	  if List.exists 
+	    (fun c1 -> not (pf_conv_x gl t (pf_type_of gl c1))) lc'
+	  then 
+	    errorlabstrm "Ring :"
+	      [< 'sTR" All terms must have the same type" >];
+	  (tclTHEN (raw_polynom th None lc) polynom_unfold_tac) gl
 
 let dyn_polynom ltacargs gl =  
   polynom (List.map