anneaux commutatifs ou non, reification sans ml

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

9 files changed, 2307 insertions, 0 deletions

diff --git a/plugins/setoid_ring/Algebra_syntax.v b/plugins/setoid_ring/Algebra_syntax.v
new file mode 100644
index 000000000..79f5393dd
--- /dev/null
+++ b/plugins/setoid_ring/Algebra_syntax.v
@@ -0,0 +1,18 @@
+Class Zero (A : Type) := {zero : A}.
+Notation "0" := zero.
+Class One (A : Type) := {one : A}.
+Notation "1" := one.
+Class Addition (A : Type) := {addition : A -> A -> A}.
+Notation "x + y" := (addition x y).
+Class Multiplication {A B : Type} := {multiplication : A -> B -> B}.
+Notation "x * y" := (multiplication x y).
+Class Subtraction (A : Type) := {subtraction : A -> A -> A}.
+Notation "x - y" := (subtraction x y).
+Class Opposite (A : Type) := {opposite : A -> A}.
+Notation "- x" := (opposite x).
+Class Equality {A : Type}:= {equality : A -> A -> Prop}.
+Notation "x == y" := (equality x y) (at level 70, no associativity).
+Class Bracket (A B: Type):= {bracket : A -> B}.
+Notation "[ x ]" := (bracket x).
+Class Power {A B: Type} := {power : A -> B -> A}.
+Notation "x ^ y" := (power x y).
\ No newline at end of file
diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v
new file mode 100644
index 000000000..5ba016074
--- /dev/null
+++ b/plugins/setoid_ring/Cring.v
@@ -0,0 +1,386 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* non commutative rings *)
+
+Require Import Setoid.
+Require Import BinPos.
+Require Import BinNat.
+Require Export Morphisms Setoid Bool.
+Require Import Algebra_syntax.
+Require Import Ring_theory.
+
+Set Implicit Arguments.
+
+Class Cring (R:Type) := {
+ cring0: R; cring1: R; 
+ cring_plus: R->R->R; cring_mult: R->R->R;
+ cring_sub:  R->R->R; cring_opp: R->R; 
+ cring_eq : R -> R -> Prop;
+ cring_setoid: Equivalence cring_eq;
+ cring_plus_comp: Proper (cring_eq==>cring_eq==>cring_eq) cring_plus;
+ cring_mult_comp: Proper (cring_eq==>cring_eq==>cring_eq) cring_mult;
+ cring_sub_comp: Proper (cring_eq==>cring_eq==>cring_eq) cring_sub;
+ cring_opp_comp: Proper (cring_eq==>cring_eq) cring_opp;
+
+ cring_add_0_l    : forall x, cring_eq (cring_plus cring0 x) x;
+ cring_add_comm    : forall x y, cring_eq (cring_plus x y) (cring_plus y x);
+ cring_add_assoc  : forall x y z, cring_eq (cring_plus x (cring_plus y z))
+                                         (cring_plus (cring_plus x y) z);
+ cring_mul_1_l    : forall x, cring_eq (cring_mult cring1 x) x;
+ cring_mul_assoc  : forall x y z, cring_eq (cring_mult x (cring_mult y z))
+                                         (cring_mult (cring_mult x y) z);
+ cring_mul_comm    : forall x y, cring_eq (cring_mult x y) (cring_mult y x);
+ cring_distr_l    : forall x y z, cring_eq (cring_mult (cring_plus x y) z)
+                                   (cring_plus (cring_mult x z) (cring_mult y z));
+ cring_sub_def    : forall x y, cring_eq (cring_sub x y) (cring_plus x (cring_opp y));
+ cring_opp_def    : forall x, cring_eq (cring_plus x (cring_opp x)) cring0
+}.
+
+(* Syntax *)
+
+Instance zero_cring `{R:Type}`{Rr:Cring R} : Zero R := {zero := cring0}.
+Instance one_cring`{R:Type}`{Rr:Cring R} : One R := {one := cring1}.
+Instance addition_cring`{R:Type}`{Rr:Cring R} : Addition R :=
+  {addition x y := cring_plus x y}.
+Instance multiplication_cring`{R:Type}`{Rr:Cring R} : Multiplication:= 
+  {multiplication x y := cring_mult x y}.
+Instance subtraction_cring`{R:Type}`{Rr:Cring R} : Subtraction R :=
+  {subtraction x y := cring_sub x y}.
+Instance opposite_cring`{R:Type}`{Rr:Cring R} : Opposite R := 
+  {opposite x := cring_opp x}.
+Instance equality_cring `{R:Type}`{Rr:Cring R} : Equality :=
+  {equality x y := cring_eq x y}.
+Instance power_cring {R:Type}{Rr:Cring R} : Power:=
+  {power x y := @Ring_theory.pow_N _ cring1 cring_mult x y}.
+
+Existing Instance cring_setoid.
+Existing Instance cring_plus_comp.
+Existing Instance cring_mult_comp.
+Existing Instance cring_sub_comp.
+Existing Instance cring_opp_comp.
+(** Interpretation morphisms definition*)
+
+Class Cring_morphism (C R:Type)`{Cr:Cring C} `{Rr:Cring R}:= {
+    cring_morphism_fun: C -> R;
+    cring_morphism0    : cring_morphism_fun 0 == 0;
+    cring_morphism1    : cring_morphism_fun 1 == 1;
+    cring_morphism_add : forall x y, cring_morphism_fun (x + y)
+                     == cring_morphism_fun x + cring_morphism_fun y;
+    cring_morphism_sub : forall x y, cring_morphism_fun (x - y)
+                     == cring_morphism_fun x - cring_morphism_fun y;
+    cring_morphism_mul : forall x y, cring_morphism_fun (x * y)
+                     == cring_morphism_fun x * cring_morphism_fun y;
+    cring_morphism_opp : forall x, cring_morphism_fun (-x)
+                          == -(cring_morphism_fun x);
+    cring_morphism_eq  : forall x y, x == y
+       -> cring_morphism_fun x == cring_morphism_fun y}.
+
+Instance bracket_cring {C R:Type}`{Cr:Cring C} `{Rr:Cring R}
+   `{phi:@Cring_morphism C R Cr Rr}
+  : Bracket C R  :=
+  {bracket x := cring_morphism_fun x}.
+
+(* Tactics for crings *)
+Axiom eta: forall (A B:Type) (f:A->B), (fun x:A => f x) = f.
+Axiom eta2: forall (A B C:Type) (f:A->B->C), (fun (x:A)(y:B) => f x y) = f.
+
+Ltac etarefl := try apply eta; try apply eta2; try reflexivity.
+
+Lemma cring_syntax1:forall (A:Type)(Ar:Cring A), (@cring_eq _ Ar) = equality.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma cring_syntax2:forall (A:Type)(Ar:Cring A), (@cring_plus _ Ar) = addition.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma cring_syntax3:forall (A:Type)(Ar:Cring A), (@cring_mult _ Ar) = multiplication.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma cring_syntax4:forall (A:Type)(Ar:Cring A), (@cring_sub _ Ar) = subtraction.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma cring_syntax5:forall (A:Type)(Ar:Cring A), (@cring_opp _ Ar) = opposite.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma cring_syntax6:forall (A:Type)(Ar:Cring A), (@cring0 _ Ar) = zero.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma cring_syntax7:forall (A:Type)(Ar:Cring A), (@cring1 _ Ar) = one.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma cring_syntax8:forall (A:Type)(Ar:Cring A)(B:Type)(Br:Cring B)
+  (pM:@Cring_morphism A B Ar Br), (@cring_morphism_fun _ _ _ _ pM) = bracket.
+intros. symmetry. simpl; etarefl. Qed.
+
+Ltac set_cring_notations :=
+  repeat (rewrite cring_syntax1);
+  repeat (rewrite cring_syntax2);
+  repeat (rewrite cring_syntax3);
+  repeat (rewrite cring_syntax4);
+  repeat (rewrite cring_syntax5);
+  repeat (rewrite cring_syntax6);
+  repeat (rewrite cring_syntax7);
+  repeat (rewrite cring_syntax8).
+
+Ltac unset_cring_notations :=
+  unfold equality, equality_cring, addition, addition_cring,
+     multiplication, multiplication_cring, subtraction, subtraction_cring,
+     opposite, opposite_cring, one, one_cring, zero, zero_cring,
+     bracket, bracket_cring, power, power_cring.
+
+Ltac cring_simpl := simpl; set_cring_notations.
+
+Ltac cring_rewrite H:=
+  generalize H;
+  let h := fresh "H" in
+  unset_cring_notations; intro h;
+  rewrite h; clear h;
+  set_cring_notations.
+
+Ltac cring_rewrite_rev H:=
+  generalize H;
+  let h := fresh "H" in
+  unset_cring_notations; intro h;
+  rewrite <- h; clear h;
+  set_cring_notations.
+
+Ltac rrefl := unset_cring_notations; reflexivity.
+
+(* Useful properties *)
+
+Section Cring.
+
+Variable R: Type.
+Variable Rr: Cring R.
+
+(* Powers *)
+
+ Fixpoint pow_pos (x:R) (i:positive) {struct i}: R :=
+  match i with
+  | xH => x
+  | xO i => let p := pow_pos x i in p * p
+  | xI i => let p := pow_pos x i in x * (p * p)
+  end.
+Add Setoid R cring_eq cring_setoid as R_set_Power.
+ Add Morphism cring_mult : rmul_ext_Power. exact cring_mult_comp. Qed.
+
+ Lemma pow_pos_comm : forall x j,  x * pow_pos x j == pow_pos x j * x.
+induction j; cring_simpl. 
+cring_rewrite_rev cring_mul_assoc. cring_rewrite_rev cring_mul_assoc. 
+cring_rewrite_rev IHj. cring_rewrite (cring_mul_assoc (pow_pos x j) x (pow_pos x j)).
+cring_rewrite_rev IHj. cring_rewrite_rev cring_mul_assoc. rrefl.
+cring_rewrite_rev cring_mul_assoc. cring_rewrite_rev IHj.
+cring_rewrite cring_mul_assoc. cring_rewrite IHj.
+cring_rewrite_rev cring_mul_assoc. cring_rewrite IHj. rrefl. rrefl.
+Qed.
+
+ Lemma pow_pos_Psucc : forall x j, pow_pos x (Psucc j) == x * pow_pos x j.
+ Proof.
+  induction j; cring_simpl. 
+  cring_rewrite IHj. 
+cring_rewrite_rev (cring_mul_assoc x (pow_pos x j) (x * pow_pos x j)).
+cring_rewrite (cring_mul_assoc (pow_pos x j) x  (pow_pos x j)).
+  cring_rewrite_rev pow_pos_comm. unset_cring_notations.
+rewrite <- cring_mul_assoc. reflexivity.
+rrefl. rrefl.
+Qed.
+
+ Lemma pow_pos_Pplus : forall x i j, pow_pos x (i + j) == pow_pos x i * pow_pos x j.
+ Proof.
+  intro x;induction i;intros.
+  rewrite xI_succ_xO;rewrite Pplus_one_succ_r.
+  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
+  repeat cring_rewrite IHi.
+  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;
+  cring_rewrite pow_pos_Psucc.
+  cring_simpl;repeat cring_rewrite cring_mul_assoc. rrefl.
+  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
+  repeat cring_rewrite IHi. cring_rewrite cring_mul_assoc. rrefl.
+  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;cring_rewrite pow_pos_Psucc.
+   simpl. reflexivity. 
+ Qed.
+
+ Definition pow_N (x:R) (p:N) :=
+  match p with
+  | N0 => 1
+  | Npos p => pow_pos x p
+  end.
+
+ Definition id_phi_N (x:N) : N := x.
+
+ Lemma pow_N_pow_N : forall x n, pow_N x (id_phi_N n) == pow_N x n.
+ Proof.
+  intros; rrefl.
+ Qed.
+
+End Cring.
+
+
+
+
+Section Cring2.
+Variable R: Type.
+Variable Rr: Cring R.
+ (** Identity is a morphism *)
+ Definition IDphi (x:R) := x.
+ Lemma IDmorph : @Cring_morphism R R Rr Rr.
+ Proof.
+  apply (Build_Cring_morphism Rr Rr IDphi);intros;unfold IDphi; try rrefl. trivial.
+ Qed.
+
+Ltac cring_replace a b :=
+  unset_cring_notations; setoid_replace a with b; set_cring_notations.
+
+ (** crings are almost crings*)
+ Lemma cring_mul_0_l : forall x, 0 * x == 0.
+ Proof.
+  intro x. cring_replace (0*x) ((0+1)*x + -x). 
+  cring_rewrite cring_add_0_l. cring_rewrite cring_mul_1_l .
+  cring_rewrite cring_opp_def ;rrefl.
+  cring_rewrite cring_distr_l ;cring_rewrite cring_mul_1_l .
+  cring_rewrite_rev cring_add_assoc ; cring_rewrite cring_opp_def .
+  cring_rewrite cring_add_comm ; cring_rewrite cring_add_0_l ;rrefl.
+ Qed.
+
+Lemma cring_mul_1_r: forall x, x * 1 == x.
+intro x. cring_rewrite (cring_mul_comm x 1). cring_rewrite cring_mul_1_l.
+rrefl. Qed.
+
+Lemma cring_distr_r: forall x y z,
+  x*(y+z) == x*y + x*z.
+intros. cring_rewrite (cring_mul_comm x (y+z)).
+cring_rewrite cring_distr_l. cring_rewrite (cring_mul_comm x y).
+ cring_rewrite (cring_mul_comm x z). rrefl. Qed.
+
+ Lemma cring_mul_0_r : forall x, x * 0 == 0.
+ Proof.
+  intro x; cring_replace (x*0)  (x*(0+1) + -x).
+  cring_rewrite cring_add_0_l ;  cring_rewrite cring_mul_1_r .
+  cring_rewrite cring_opp_def ;rrefl.
+  cring_rewrite cring_distr_r . cring_rewrite cring_mul_1_r .
+  cring_rewrite_rev cring_add_assoc ; cring_rewrite cring_opp_def .
+  cring_rewrite cring_add_comm ; cring_rewrite cring_add_0_l ;rrefl.
+ Qed.
+
+ Lemma cring_opp_mul_l : forall x y, -(x * y) == -x * y.
+ Proof.
+  intros x y;cring_rewrite_rev (cring_add_0_l (- x * y)).
+  cring_rewrite cring_add_comm .
+  cring_rewrite_rev (cring_opp_def (x*y)).
+  cring_rewrite cring_add_assoc .
+  cring_rewrite_rev cring_distr_l.
+  cring_rewrite (cring_add_comm (-x));cring_rewrite cring_opp_def .
+  cring_rewrite cring_mul_0_l;cring_rewrite cring_add_0_l ;rrefl.
+ Qed.
+
+Lemma cring_opp_mul_r : forall x y, -(x * y) == x * -y.
+ Proof.
+  intros x y;cring_rewrite_rev (cring_add_0_l (x * - y)).
+  cring_rewrite cring_add_comm .
+  cring_rewrite_rev (cring_opp_def (x*y)).
+  cring_rewrite cring_add_assoc .
+  cring_rewrite_rev cring_distr_r .
+  cring_rewrite (cring_add_comm (-y));cring_rewrite cring_opp_def .
+  cring_rewrite cring_mul_0_r;cring_rewrite cring_add_0_l ;rrefl.
+ Qed.
+
+ Lemma cring_opp_add : forall x y, -(x + y) == -x + -y.
+ Proof.
+  intros x y;cring_rewrite_rev (cring_add_0_l  (-(x+y))).
+  cring_rewrite_rev (cring_opp_def  x).
+  cring_rewrite_rev (cring_add_0_l  (x + - x + - (x + y))).
+  cring_rewrite_rev (cring_opp_def  y).
+  cring_rewrite (cring_add_comm  x).
+  cring_rewrite (cring_add_comm  y).
+  cring_rewrite_rev (cring_add_assoc  (-y)).
+  cring_rewrite_rev (cring_add_assoc  (- x)).
+  cring_rewrite (cring_add_assoc   y).
+  cring_rewrite (cring_add_comm  y).
+  cring_rewrite_rev (cring_add_assoc   (- x)).
+  cring_rewrite (cring_add_assoc  y).
+  cring_rewrite (cring_add_comm  y);cring_rewrite cring_opp_def .
+  cring_rewrite (cring_add_comm  (-x) 0);cring_rewrite cring_add_0_l .
+  cring_rewrite cring_add_comm; rrefl.
+ Qed.
+
+ Lemma cring_opp_opp : forall x, - -x == x.
+ Proof.
+  intros x; cring_rewrite_rev (cring_add_0_l (- -x)).
+  cring_rewrite_rev (cring_opp_def x).
+  cring_rewrite_rev cring_add_assoc ; cring_rewrite cring_opp_def .
+  cring_rewrite (cring_add_comm  x); cring_rewrite cring_add_0_l . rrefl.
+ Qed.
+
+ Lemma cring_sub_ext :
+      forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 - y1 == x2 - y2.
+ Proof.
+  intros.
+  cring_replace (x1 - y1)  (x1 + -y1).
+  cring_replace (x2 - y2)  (x2 + -y2).
+  cring_rewrite H;cring_rewrite H0;rrefl.
+  cring_rewrite cring_sub_def. rrefl.
+  cring_rewrite cring_sub_def. rrefl.
+ Qed.
+
+ Ltac mcring_rewrite :=
+   repeat first
+     [ cring_rewrite cring_add_0_l
+     | cring_rewrite_rev (cring_add_comm 0)
+     | cring_rewrite cring_mul_1_l
+     | cring_rewrite cring_mul_0_l
+     | cring_rewrite cring_distr_l
+     | rrefl
+     ].
+
+ Lemma cring_add_0_r : forall x, (x + 0) == x.
+ Proof. intros; mcring_rewrite. Qed.
+
+ 
+ Lemma cring_add_assoc1 : forall x y z, (x + y) + z == (y + z) + x.
+ Proof.
+  intros;cring_rewrite_rev (cring_add_assoc x).
+  cring_rewrite (cring_add_comm x);rrefl.
+ Qed.
+
+ Lemma cring_add_assoc2 : forall x y z, (y + x) + z == (y + z) + x.
+ Proof.
+  intros; repeat cring_rewrite_rev cring_add_assoc.
+   cring_rewrite (cring_add_comm x); rrefl.
+ Qed.
+
+ Lemma cring_opp_zero : -0 == 0.
+ Proof.
+  cring_rewrite_rev (cring_mul_0_r 0). cring_rewrite cring_opp_mul_l.
+  repeat cring_rewrite cring_mul_0_r. rrefl.
+ Qed.
+
+End Cring2.
+
+(** Some simplification tactics*)
+Ltac gen_reflexivity := rrefl.
+ 
+Ltac gen_cring_rewrite :=
+  repeat first
+     [ rrefl
+     | progress cring_rewrite cring_opp_zero
+     | cring_rewrite cring_add_0_l
+     | cring_rewrite cring_add_0_r
+     | cring_rewrite cring_mul_1_l 
+     | cring_rewrite cring_mul_1_r
+     | cring_rewrite cring_mul_0_l 
+     | cring_rewrite cring_mul_0_r 
+     | cring_rewrite cring_distr_l 
+     | cring_rewrite cring_distr_r 
+     | cring_rewrite cring_add_assoc 
+     | cring_rewrite cring_mul_assoc
+     | progress cring_rewrite cring_opp_add 
+     | progress cring_rewrite cring_sub_def 
+     | progress cring_rewrite_rev cring_opp_mul_l 
+     | progress cring_rewrite_rev cring_opp_mul_r ].
+
+Ltac gen_add_push x :=
+set_cring_notations;
+repeat (match goal with
+  | |- context [(?y + x) + ?z] =>
+     progress cring_rewrite (@cring_add_assoc2 _ _ x y z)
+  | |- context [(x + ?y) + ?z] =>
+     progress cring_rewrite  (@cring_add_assoc1 _ _ x y z)
+  end).
diff --git a/plugins/setoid_ring/Cring_initial.v b/plugins/setoid_ring/Cring_initial.v
new file mode 100644
index 000000000..4a0beb3fa
--- /dev/null
+++ b/plugins/setoid_ring/Cring_initial.v
@@ -0,0 +1,225 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import ZArith_base.
+Require Import Zpow_def.
+Require Import BinInt.
+Require Import BinNat.
+Require Import Setoid.
+Require Import Algebra_syntax.
+Require Export Ring_polynom.
+Require Export Cring.
+Import List.
+
+Set Implicit Arguments.
+
+(* An object to return when an expression is not recognized as a constant *)
+Definition NotConstant := false.
+
+(** Z is a ring and a setoid*)
+
+Lemma Zsth : Setoid_Theory Z (@eq Z).
+constructor;red;intros;subst;trivial.
+Qed.
+
+Definition Zr : Cring Z.
+apply (@Build_Cring Z Z0 (Zpos xH) Zplus Zmult Zminus Zopp (@eq Z)); 
+try apply Zsth; try (red; red; intros; rewrite H; reflexivity). 
+ exact Zplus_comm. exact Zplus_assoc.
+ exact Zmult_1_l.  exact Zmult_assoc. exact Zmult_comm.
+ exact Zmult_plus_distr_l. trivial. exact Zminus_diag.
+Defined.
+
+(** Two generic morphisms from Z to (abrbitrary) rings, *)
+(**second one is more convenient for proofs but they are ext. equal*)
+Section ZMORPHISM.
+ Variable R : Type.
+ Variable Rr: Cring R.
+Existing Instance Rr.
+ 
+ Ltac rrefl := gen_reflexivity Rr.
+
+(*
+Print HintDb typeclass_instances.
+Print Scopes.
+*)
+
+ Fixpoint gen_phiPOS1 (p:positive) : R :=
+  match p with
+  | xH => 1
+  | xO p => (1 + 1) * (gen_phiPOS1 p)
+  | xI p => 1 + ((1 + 1) * (gen_phiPOS1 p))
+  end.
+
+ Fixpoint gen_phiPOS (p:positive) : R :=
+  match p with
+  | xH => 1
+  | xO xH => (1 + 1)
+  | xO p => (1 + 1) * (gen_phiPOS p)
+  | xI xH => 1 + (1 +1)
+  | xI p => 1 + ((1 + 1) * (gen_phiPOS p))
+  end.
+
+ Definition gen_phiZ1 z :=
+  match z with
+  | Zpos p => gen_phiPOS1 p
+  | Z0 => 0
+  | Zneg p => -(gen_phiPOS1 p)
+  end.
+
+ Definition gen_phiZ z :=
+  match z with
+  | Zpos p => gen_phiPOS p
+  | Z0 => 0
+  | Zneg p => -(gen_phiPOS p)
+  end.
+ Notation "[ x ]" := (gen_phiZ x).
+
+ Definition get_signZ z :=
+  match z with
+  | Zneg p => Some (Zpos p)
+  | _ => None
+  end.
+
+   Ltac norm := gen_cring_rewrite.
+   Ltac add_push :=  gen_add_push.
+Ltac rsimpl := simpl;  set_cring_notations.
+
+ Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x.
+ Proof.
+  induction x;rsimpl.
+  cring_rewrite IHx. destruct x;simpl;norm.
+  cring_rewrite IHx;destruct x;simpl;norm.
+  gen_reflexivity.
+ Qed.
+
+ Lemma ARgen_phiPOS_Psucc : forall x,
+   gen_phiPOS1 (Psucc x) == 1 + (gen_phiPOS1 x).
+ Proof.
+  induction x;rsimpl;norm.
+  cring_rewrite IHx ;norm.
+  add_push 1;gen_reflexivity.
+ Qed.
+
+ Lemma ARgen_phiPOS_add : forall x y,
+   gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y).
+ Proof.
+  induction x;destruct y;simpl;norm.
+  cring_rewrite Pplus_carry_spec.
+  cring_rewrite ARgen_phiPOS_Psucc.
+  cring_rewrite IHx;norm.
+  add_push (gen_phiPOS1 y);add_push 1;gen_reflexivity.
+  cring_rewrite IHx;norm;add_push (gen_phiPOS1 y);gen_reflexivity.
+  cring_rewrite ARgen_phiPOS_Psucc;norm;add_push 1;gen_reflexivity.
+  cring_rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;gen_reflexivity.
+  cring_rewrite IHx;norm;add_push(gen_phiPOS1 y);gen_reflexivity.
+  add_push 1;gen_reflexivity.
+  cring_rewrite ARgen_phiPOS_Psucc;norm;add_push 1;gen_reflexivity.
+ Qed.
+
+ Lemma ARgen_phiPOS_mult :
+   forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y.
+ Proof.
+  induction x;intros;simpl;norm.
+  cring_rewrite ARgen_phiPOS_add;simpl;cring_rewrite IHx;norm.
+  cring_rewrite IHx;gen_reflexivity.
+ Qed.
+
+
+(*morphisms are extensionaly equal*)
+ Lemma same_genZ : forall x, [x] == gen_phiZ1 x.
+ Proof.
+  destruct x;rsimpl; try cring_rewrite same_gen; gen_reflexivity.
+ Qed.
+
+ Lemma gen_Zeqb_ok : forall x y,
+   Zeq_bool x y = true -> [x] == [y].
+ Proof.
+  intros x y H.
+  assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1.
+  cring_rewrite H1;gen_reflexivity.
+ Qed.
+
+ Lemma gen_phiZ1_add_pos_neg : forall x y,
+ gen_phiZ1
+    match (x ?= y)%positive Eq with
+    | Eq => Z0
+    | Lt => Zneg (y - x)
+    | Gt => Zpos (x - y)
+    end
+ == gen_phiPOS1 x + -gen_phiPOS1 y.
+ Proof.
+  intros x y.
+  assert (H:= (Pcompare_Eq_eq x y)); assert (H0 := Pminus_mask_Gt x y).
+  generalize (Pminus_mask_Gt y x).
+  replace Eq with (CompOpp Eq);[intro H1;simpl|trivial].
+  rewrite <- Pcompare_antisym in H1.
+  destruct ((x ?= y)%positive Eq).
+  cring_rewrite H;trivial. cring_rewrite cring_opp_def;gen_reflexivity.
+  destruct H1 as [h [Heq1 [Heq2 Hor]]];trivial.
+  unfold Pminus; cring_rewrite Heq1;rewrite <- Heq2.
+  cring_rewrite ARgen_phiPOS_add;simpl;norm.
+  cring_rewrite cring_opp_def;norm.
+  destruct H0 as [h [Heq1 [Heq2 Hor]]];trivial.
+  unfold Pminus; rewrite Heq1;rewrite <- Heq2.
+  cring_rewrite ARgen_phiPOS_add;simpl;norm.
+  set_cring_notations. add_push (gen_phiPOS1 h). cring_rewrite cring_opp_def ; norm.
+ Qed.
+
+ Lemma match_compOpp : forall x (B:Type) (be bl bg:B),
+  match CompOpp x with Eq => be | Lt => bl | Gt => bg end
+  = match x with Eq => be | Lt => bg | Gt => bl end.
+ Proof. destruct x;simpl;intros;trivial. Qed.
+
+ Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y].
+ Proof.
+  intros x y; repeat cring_rewrite same_genZ; generalize x y;clear x y.
+  induction x;destruct y;simpl;norm.
+  apply ARgen_phiPOS_add.
+  apply gen_phiZ1_add_pos_neg.
+  replace Eq with (CompOpp Eq);trivial.
+  rewrite <- Pcompare_antisym;simpl.
+  cring_rewrite match_compOpp.
+  cring_rewrite cring_add_comm.
+  apply gen_phiZ1_add_pos_neg.
+  cring_rewrite ARgen_phiPOS_add; norm.
+ Qed.
+
+Lemma gen_phiZ_opp : forall x, [- x] == - [x].
+ Proof.
+  intros x. repeat cring_rewrite same_genZ. generalize x ;clear x.
+  induction x;simpl;norm.
+  cring_rewrite cring_opp_opp.  gen_reflexivity.
+ Qed.
+
+ Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y].
+ Proof.
+  intros x y;repeat cring_rewrite same_genZ.
+  destruct x;destruct y;simpl;norm;
+  cring_rewrite  ARgen_phiPOS_mult;try (norm;fail).
+  cring_rewrite cring_opp_opp ;gen_reflexivity.
+ Qed.
+
+ Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y].
+ Proof. intros;subst;gen_reflexivity. Qed.
+
+(*proof that [.] satisfies morphism specifications*)
+ Lemma gen_phiZ_morph : @Cring_morphism Z R Zr Rr.
+ apply (Build_Cring_morphism Zr Rr gen_phiZ);simpl;try gen_reflexivity.
+   apply gen_phiZ_add. intros. cring_rewrite cring_sub_def. 
+replace (x-y)%Z with (x + (-y))%Z. cring_rewrite gen_phiZ_add. 
+cring_rewrite gen_phiZ_opp. gen_reflexivity.
+reflexivity.
+ apply gen_phiZ_mul. apply gen_phiZ_opp. apply gen_phiZ_ext. 
+ Defined.
+
+End ZMORPHISM.
+
+
+
+
diff --git a/plugins/setoid_ring/Cring_tac.v b/plugins/setoid_ring/Cring_tac.v
new file mode 100644
index 000000000..c83dd4e8d
--- /dev/null
+++ b/plugins/setoid_ring/Cring_tac.v
@@ -0,0 +1,257 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import List.
+Require Import Setoid.
+Require Import BinPos.
+Require Import BinList.
+Require Import Znumtheory.
+Require Import Zdiv_def.
+Require Export Morphisms Setoid Bool.
+Require Import ZArith.
+Require Import Algebra_syntax.
+Require Import Ring_polynom.
+Require Export Cring.
+Require Import Cring_initial.
+
+
+Set Implicit Arguments.
+
+Class is_closed_list T (l:list T) := {}.
+Instance Iclosed_nil T 
+ : is_closed_list (T:=T) nil.
+Instance Iclosed_cons T t l 
+ `{is_closed_list (T:=T) l} 
+ : is_closed_list (T:=T) (t::l).
+
+Class is_in_list_at (R:Type) (t:R) (l:list R) (i:nat) := {}.
+Instance  Ifind0 (R:Type) (t:R) l
+ : is_in_list_at t (t::l) 0.
+Instance  IfindS (R:Type) (t2 t1:R) l i 
+ `{is_in_list_at R t1 l i} 
+ : is_in_list_at t1 (t2::l) (S i) | 1.
+
+Class reifyPE (R:Type) (e:PExpr Z) (lvar:list R) (t:R) := {}.
+Instance  reify_zero (R:Type) (RR:Cring R) lvar 
+ : reifyPE (PEc 0%Z) lvar cring0.
+Instance  reify_one (R:Type) (RR:Cring R) lvar 
+ : reifyPE (PEc 1%Z) lvar cring1.
+Instance  reify_plus (R:Type)  (RR:Cring R)
+  e1 lvar t1 e2 t2 
+ `{reifyPE R e1 lvar t1} 
+ `{reifyPE R e2 lvar t2} 
+ : reifyPE (PEadd e1 e2) lvar (cring_plus t1 t2).
+Instance  reify_mult (R:Type)  (RR:Cring R)
+  e1 lvar t1 e2 t2 
+ `{reifyPE R e1 lvar t1} 
+ `{reifyPE R e2 lvar t2}
+ : reifyPE (PEmul e1 e2) lvar (cring_mult t1 t2).
+Instance  reify_sub (R:Type) (RR:Cring R) 
+ e1 lvar t1 e2 t2 
+ `{reifyPE R e1 lvar t1} 
+ `{reifyPE R e2 lvar t2}
+ : reifyPE (PEsub e1 e2) lvar (cring_sub t1 t2).
+Instance  reify_opp (R:Type) (RR:Cring R) 
+ e1 lvar t1 
+ `{reifyPE R e1 lvar t1}
+ : reifyPE (PEopp e1) lvar (cring_opp t1).
+Instance  reify_pow (R:Type) (RR:Cring R) 
+ e1 lvar t1 n 
+ `{reifyPE R e1 lvar t1}
+ : reifyPE (PEpow e1 n) lvar (@Ring_theory.pow_N _ cring1 cring_mult t1 n).
+Instance  reify_var (R:Type) t lvar i 
+ `{is_in_list_at R t lvar i}
+ : reifyPE (PEX Z (P_of_succ_nat i)) lvar t 
+ | 100.
+
+Class reifyPElist (R:Type) (lexpr:list (PExpr Z)) (lvar:list R) 
+  (lterm:list R) := {}.
+Instance reifyPE_nil (R:Type) lvar 
+ : @reifyPElist R nil lvar (@nil R).
+Instance reifyPE_cons (R:Type) e1 lvar t1 lexpr2 lterm2
+ `{reifyPE R e1 lvar t1} `{reifyPElist R lexpr2 lvar lterm2} 
+ : reifyPElist (e1::lexpr2) lvar (t1::lterm2).
+
+Definition list_reifyl (R:Type) lexpr lvar lterm 
+ `{reifyPElist R lexpr lvar lterm}
+ `{is_closed_list (T:=R) lvar} := (lvar,lexpr).
+
+Unset Implicit Arguments.
+
+Instance multiplication_phi_cring{R:Type}{Rr:Cring R} : Multiplication  :=
+  {multiplication x y := cring_mult
+    (@gen_phiZ R Rr x) y}.
+
+(*
+Print HintDb typeclass_instances.
+*)
+(* Reification *)
+
+Ltac lterm_goal g :=
+  match g with
+  cring_eq ?t1 ?t2 => constr:(t1::t2::nil)
+  | cring_eq ?t1 ?t2 -> ?g => let lvar := lterm_goal g in constr:(t1::t2::lvar)     
+  end.
+
+Ltac reify_goal lvar lexpr lterm:=
+(*  idtac lvar; idtac lexpr; idtac lterm;*)
+  match lexpr with
+     nil => idtac
+   | ?e::?lexpr1 =>  
+        match lterm with
+         ?t::?lterm1 => (* idtac "t="; idtac t;*)
+           let x := fresh "T" in
+           set (x:= t);
+           change x with 
+             (@PEeval _ 0 addition multiplication subtraction opposite  Z
+               (@gen_phiZ _ _)
+               N (fun n:N => n) (@Ring_theory.pow_N _ 1 multiplication) lvar e); 
+           clear x;
+           reify_goal lvar lexpr1 lterm1
+        end
+  end.
+
+Existing Instance gen_phiZ_morph.
+Existing Instance Zr.
+
+Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y.
+ intros x y H. rewrite (Zeq_bool_eq x y H). rrefl. Qed. 
+
+
+Lemma cring_eq_ext: forall (R:Type)(Rr:Cring R),
+  ring_eq_ext addition multiplication opposite cring_eq.
+intros. apply mk_reqe; set_cring_notations;intros. 
+cring_rewrite H0. cring_rewrite H. rrefl.
+cring_rewrite H0. cring_rewrite H. rrefl.
+ cring_rewrite H. rrefl. Defined.
+
+Lemma cring_almost_ring_theory: forall (R:Type)(Rr:Cring R),
+   almost_ring_theory 0 1 addition multiplication subtraction opposite cring_eq.
+intros. apply mk_art ; set_cring_notations;intros.
+cring_rewrite cring_add_0_l; rrefl. 
+cring_rewrite cring_add_comm; rrefl. 
+cring_rewrite cring_add_assoc; rrefl. 
+cring_rewrite cring_mul_1_l; rrefl. 
+apply cring_mul_0_l.
+cring_rewrite cring_mul_comm; rrefl. 
+cring_rewrite cring_mul_assoc; rrefl. 
+cring_rewrite cring_distr_l; rrefl. 
+cring_rewrite cring_opp_mul_l; rrefl. 
+apply cring_opp_add.
+cring_rewrite cring_sub_def ; rrefl. Defined.
+
+Lemma cring_morph:  forall (R:Type)(Rr:Cring R),
+  ring_morph  0 1 addition multiplication subtraction opposite cring_eq
+             0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
+             (@gen_phiZ _ _).
+intros. apply mkmorph ; intros; simpl; try rrefl; set_cring_notations.
+cring_rewrite gen_phiZ_add; rrefl.
+cring_rewrite cring_sub_def. unfold Zminus. cring_rewrite gen_phiZ_add.
+cring_rewrite gen_phiZ_opp; rrefl.
+cring_rewrite gen_phiZ_mul; rrefl.
+cring_rewrite gen_phiZ_opp; rrefl.
+rewrite (Zeqb_ok x y H). rrefl. Defined.
+
+Lemma cring_power_theory :  forall (R:Type)(Rr:Cring R),
+  power_theory 1 (@multiplication _ _ (@multiplication_cring R Rr)) cring_eq (fun n:N => n)
+  (@Ring_theory.pow_N _  1 multiplication).
+intros; apply mkpow_th; set_cring_notations. rrefl. Defined.
+
+Lemma cring_div_theory: forall (R:Type)(Rr:Cring R),
+  div_theory cring_eq Zplus Zmult (gen_phiZ Rr) Zquotrem.
+intros. apply InitialRing.Ztriv_div_th. unfold Setoid_Theory.
+simpl.   apply (@cring_setoid R Rr). Defined.
+
+Ltac cring_gen :=
+  match goal with
+    |- ?g => let lterm := lterm_goal g in (* les variables *)
+        match eval red in (list_reifyl (lterm:=lterm)) with
+          | (?fv, ?lexpr) => 
+(*         idtac "variables:";idtac fv;
+           idtac "terms:"; idtac lterm;
+           idtac "reifications:"; idtac lexpr; 
+           *)
+            let lv := fresh "lvar" in
+              set (lv := fv);
+                reify_goal lv lexpr lterm;
+                match goal with 
+                  |- ?g => 
+                    set_cring_notations ; unfold lv;
+                      generalize (@ring_correct _ 0 1 addition multiplication subtraction opposite 
+                        cring_eq
+                        cring_setoid (@cring_eq_ext _ _) (@cring_almost_ring_theory _ _)
+                        Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
+                        (@gen_phiZ _ _) (@cring_morph _ _) N (fun n:N => n)
+                        (@Ring_theory.pow_N _  1 multiplication)
+                        (@cring_power_theory _ _) Zquotrem (@cring_div_theory _ _) O fv nil);
+                      set_cring_notations;
+                      let rc := fresh "rc"in
+                        intro rc; apply rc
+                end
+        end
+  end.
+
+Ltac cring_compute:= vm_compute; reflexivity.
+
+Ltac cring:= 
+  unset_cring_notations; intros;
+  unfold multiplication_phi_cring; simpl gen_phiZ;
+  match goal with
+    |- (@cring_eq ?r ?rd _ _ ) =>
+          cring_gen; cring_compute
+  end.
+
+(* Tests *)
+
+Variable R: Type.
+Variable Rr: Cring R.
+Existing Instance Rr.
+
+(* reification: 0,7s
+sinon, le reste de la tactique donne le même temps que ring 
+*)
+Goal forall x y z  t u :R, (x + y + z + t + u)^13%N == (u + t + z + y + x) ^13%N.
+Time cring. (*Finished transaction in 0. secs (0.410938u,0.s)*)
+Qed.
+(*
+Goal forall x y z  t u :R, (x + y + z + t + u)^16%N == (u + t + z + y + x) ^16%N.
+Time cring.(*Finished transaction in 1. secs (0.968852u,0.001s)*)
+Qed.
+*)
+(*
+Require Export Ring.
+Open Scope Z_scope.
+Goal forall x y z  t u :Z, (x + y + z + t + u)^13 = (u + t + z + y + x) ^13.
+intros.
+Time ring.(*Finished transaction in 0. secs (0.371944u,0.s)*)
+Qed.
+
+Goal forall x y z  t u :Z, (x + y + z + t + u)^16 = (u + t + z + y + x) ^16.
+intros.
+Time ring.(*Finished transaction in 1. secs (0.914861u,0.s)*)
+Qed.
+*)
+
+(*
+Goal forall x y z:R, x + y  == y + x + 0 .
+cring.
+Qed.
+
+Goal forall x y z:R, x * y * z == x * (y * z).
+cring.
+Qed.
+
+Goal forall x y z:R, 3%Z * x * (2%Z * y * z) == 6%Z * (x * y) * z.
+cring.
+Qed.
+
+Goal forall x y z:R, x ^ 2%N == x * x.
+cring.
+Qed.
+*)
+
diff --git a/plugins/setoid_ring/Ring2.v b/plugins/setoid_ring/Ring2.v
new file mode 100644
index 000000000..30a6128f1
--- /dev/null
+++ b/plugins/setoid_ring/Ring2.v
@@ -0,0 +1,373 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* non commutative rings *)
+
+Require Import Setoid.
+Require Import BinPos.
+Require Import BinNat.
+Require Export Morphisms Setoid Bool.
+Require Export Algebra_syntax.
+
+Set Implicit Arguments.
+
+Class Ring (R:Type) := {
+ ring0: R; ring1: R; 
+ ring_plus: R->R->R; ring_mult: R->R->R;
+ ring_sub:  R->R->R; ring_opp: R->R; 
+ ring_eq : R -> R -> Prop;
+ ring_setoid: Equivalence ring_eq;
+ ring_plus_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_plus;
+ ring_mult_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_mult;
+ ring_sub_comp: Proper (ring_eq==>ring_eq==>ring_eq) ring_sub;
+ ring_opp_comp: Proper (ring_eq==>ring_eq) ring_opp;
+
+ ring_add_0_l    : forall x, ring_eq (ring_plus ring0 x) x;
+ ring_add_comm    : forall x y, ring_eq (ring_plus x y) (ring_plus y x);
+ ring_add_assoc  : forall x y z, ring_eq (ring_plus x (ring_plus y z))
+                                         (ring_plus (ring_plus x y) z);
+ ring_mul_1_l    : forall x, ring_eq (ring_mult ring1 x) x;
+ ring_mul_1_r    : forall x, ring_eq (ring_mult x ring1) x;
+ ring_mul_assoc  : forall x y z, ring_eq (ring_mult x (ring_mult y z))
+                                         (ring_mult (ring_mult x y) z);
+ ring_distr_l    : forall x y z, ring_eq (ring_mult (ring_plus x y) z)
+                                   (ring_plus (ring_mult x z) (ring_mult y z));
+ ring_distr_r    : forall x y z, ring_eq (ring_mult z (ring_plus x y))
+                                  (ring_plus (ring_mult z x) (ring_mult z y));
+ ring_sub_def    : forall x y, ring_eq (ring_sub x y) (ring_plus x (ring_opp y));
+ ring_opp_def    : forall x, ring_eq (ring_plus x (ring_opp x)) ring0
+}.
+
+
+Instance zero_ring (R:Type)(Rr:Ring R) : Zero R := {zero := ring0}.
+Instance one_ring(R:Type)(Rr:Ring R) : One R := {one := ring1}.
+Instance addition_ring(R:Type)(Rr:Ring R) : Addition R :=
+  {addition x y := ring_plus x y}.
+Instance multiplication_ring(R:Type)(Rr:Ring R) : Multiplication:= 
+  {multiplication x y := ring_mult x y}.
+Instance subtraction_ring(R:Type)(Rr:Ring R) : Subtraction R :=
+  {subtraction x y := ring_sub x y}.
+Instance opposite_ring(R:Type)(Rr:Ring R) : Opposite R := 
+  {opposite x := ring_opp x}.
+Instance equality_ring(R:Type)(Rr:Ring R) : Equality :=
+  {equality x y := ring_eq x y}.
+
+Existing Instance ring_setoid.
+Existing Instance ring_plus_comp.
+Existing Instance ring_mult_comp.
+Existing Instance ring_sub_comp.
+Existing Instance ring_opp_comp.
+(** Interpretation morphisms definition*)
+
+Class Ring_morphism (C R:Type)`{Cr:Ring C} `{Rr:Ring R}:= {
+    ring_morphism_fun: C -> R;
+    ring_morphism0    : ring_morphism_fun 0 == 0;
+    ring_morphism1    : ring_morphism_fun 1 == 1;
+    ring_morphism_add : forall x y, ring_morphism_fun (x + y)
+                     == ring_morphism_fun x + ring_morphism_fun y;
+    ring_morphism_sub : forall x y, ring_morphism_fun (x - y)
+                     == ring_morphism_fun x - ring_morphism_fun y;
+    ring_morphism_mul : forall x y, ring_morphism_fun (x * y)
+                     == ring_morphism_fun x * ring_morphism_fun y;
+    ring_morphism_opp : forall x, ring_morphism_fun (-x)
+                          == -(ring_morphism_fun x);
+    ring_morphism_eq  : forall x y, x == y
+       -> ring_morphism_fun x == ring_morphism_fun y}.
+
+Instance bracket_ring (C R:Type)`{Cr:Ring C} `{Rr:Ring R}
+   `{phi:@Ring_morphism C R Cr Rr}
+  : Bracket C R  :=
+  {bracket x := ring_morphism_fun x}.
+
+(* Tactics for rings *)
+Axiom eta: forall (A B:Type) (f:A->B), (fun x:A => f x) = f.
+Axiom eta2: forall (A B C:Type) (f:A->B->C), (fun (x:A)(y:B) => f x y) = f.
+
+Ltac etarefl := try apply eta; try apply eta2; try reflexivity.
+
+Lemma ring_syntax1:forall (A:Type)(Ar:Ring A), (@ring_eq _ Ar) = equality.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma ring_syntax2:forall (A:Type)(Ar:Ring A), (@ring_plus _ Ar) = addition.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma ring_syntax3:forall (A:Type)(Ar:Ring A), (@ring_mult _ Ar) = multiplication.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma ring_syntax4:forall (A:Type)(Ar:Ring A), (@ring_sub _ Ar) = subtraction.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma ring_syntax5:forall (A:Type)(Ar:Ring A), (@ring_opp _ Ar) = opposite.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma ring_syntax6:forall (A:Type)(Ar:Ring A), (@ring0 _ Ar) = zero.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma ring_syntax7:forall (A:Type)(Ar:Ring A), (@ring1 _ Ar) = one.
+intros. symmetry. simpl; etarefl. Qed.
+Lemma ring_syntax8:forall (A:Type)(Ar:Ring A)(B:Type)(Br:Ring B)
+  (pM:@Ring_morphism A B Ar Br), (@ring_morphism_fun _ _ _ _ pM) = bracket.
+intros. symmetry. simpl; etarefl. Qed.
+
+Ltac set_ring_notations :=
+  repeat (rewrite ring_syntax1);
+  repeat (rewrite ring_syntax2);
+  repeat (rewrite ring_syntax3);
+  repeat (rewrite ring_syntax4);
+  repeat (rewrite ring_syntax5);
+  repeat (rewrite ring_syntax6);
+  repeat (rewrite ring_syntax7);
+  repeat (rewrite ring_syntax8).
+
+Ltac unset_ring_notations :=
+  unfold equality, equality_ring, addition, addition_ring,
+     multiplication, multiplication_ring, subtraction, subtraction_ring,
+     opposite, opposite_ring, one, one_ring, zero, zero_ring,
+     bracket, bracket_ring.
+
+Ltac ring_simpl := simpl; set_ring_notations.
+
+Ltac ring_rewrite H:=
+  generalize H;
+  let h := fresh "H" in
+  unset_ring_notations; intro h;
+  rewrite h; clear h;
+  set_ring_notations.
+
+Ltac ring_rewrite_rev H:=
+  generalize H;
+  let h := fresh "H" in
+  unset_ring_notations; intro h;
+  rewrite <- h; clear h;
+  set_ring_notations.
+
+Ltac rrefl := unset_ring_notations; reflexivity.
+
+Section Ring.
+
+Variable R: Type.
+Variable Rr: Ring R.
+
+(* Powers *)
+
+ Fixpoint pow_pos (x:R) (i:positive) {struct i}: R :=
+  match i with
+  | xH => x
+  | xO i => let p := pow_pos x i in p * p
+  | xI i => let p := pow_pos x i in x * (p * p)
+  end.
+Add Setoid R ring_eq ring_setoid as R_set_Power.
+ Add Morphism ring_mult : rmul_ext_Power. exact ring_mult_comp. Qed.
+
+ Lemma pow_pos_comm : forall x j,  x * pow_pos x j == pow_pos x j * x.
+induction j; ring_simpl. 
+ring_rewrite_rev ring_mul_assoc. ring_rewrite_rev ring_mul_assoc. 
+ring_rewrite_rev IHj. ring_rewrite (ring_mul_assoc (pow_pos x j) x (pow_pos x j)).
+ring_rewrite_rev IHj. ring_rewrite_rev ring_mul_assoc. rrefl.
+ring_rewrite_rev ring_mul_assoc. ring_rewrite_rev IHj.
+ring_rewrite ring_mul_assoc. ring_rewrite IHj.
+ring_rewrite_rev ring_mul_assoc. ring_rewrite IHj. rrefl. rrefl.
+Qed.
+
+ Lemma pow_pos_Psucc : forall x j, pow_pos x (Psucc j) == x * pow_pos x j.
+ Proof.
+  induction j; ring_simpl. 
+  ring_rewrite IHj. 
+ring_rewrite_rev (ring_mul_assoc x (pow_pos x j) (x * pow_pos x j)).
+ring_rewrite (ring_mul_assoc (pow_pos x j) x  (pow_pos x j)).
+  ring_rewrite_rev pow_pos_comm. unset_ring_notations.
+rewrite <- ring_mul_assoc. reflexivity.
+rrefl. rrefl.
+Qed.
+
+ Lemma pow_pos_Pplus : forall x i j, pow_pos x (i + j) == pow_pos x i * pow_pos x j.
+ Proof.
+  intro x;induction i;intros.
+  rewrite xI_succ_xO;rewrite Pplus_one_succ_r.
+  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
+  repeat ring_rewrite IHi.
+  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;
+  ring_rewrite pow_pos_Psucc.
+  ring_simpl;repeat ring_rewrite ring_mul_assoc. rrefl.
+  rewrite <- Pplus_diag;repeat rewrite <- Pplus_assoc.
+  repeat ring_rewrite IHi. ring_rewrite ring_mul_assoc. rrefl.
+  rewrite Pplus_comm;rewrite <- Pplus_one_succ_r;ring_rewrite pow_pos_Psucc.
+   simpl. reflexivity. 
+ Qed.
+
+ Definition pow_N (x:R) (p:N) :=
+  match p with
+  | N0 => 1
+  | Npos p => pow_pos x p
+  end.
+
+ Definition id_phi_N (x:N) : N := x.
+
+ Lemma pow_N_pow_N : forall x n, pow_N x (id_phi_N n) == pow_N x n.
+ Proof.
+  intros; rrefl.
+ Qed.
+
+End Ring.
+
+
+
+
+Section Ring2.
+Variable R: Type.
+Variable Rr: Ring R.
+ (** Identity is a morphism *)
+ Definition IDphi (x:R) := x.
+ Lemma IDmorph : @Ring_morphism R R Rr Rr.
+ Proof.
+  apply (Build_Ring_morphism Rr Rr IDphi);intros;unfold IDphi; try rrefl. trivial.
+ Qed.
+
+Ltac ring_replace a b :=
+  unset_ring_notations; setoid_replace a with b; set_ring_notations.
+
+ (** rings are almost rings*)
+ Lemma ring_mul_0_l : forall x, 0 * x == 0.
+ Proof.
+  intro x. ring_replace (0*x) ((0+1)*x + -x). 
+  ring_rewrite ring_add_0_l. ring_rewrite ring_mul_1_l .
+  ring_rewrite ring_opp_def ;rrefl.
+  ring_rewrite ring_distr_l ;ring_rewrite ring_mul_1_l .
+  ring_rewrite_rev ring_add_assoc ; ring_rewrite ring_opp_def .
+  ring_rewrite ring_add_comm ; ring_rewrite ring_add_0_l ;rrefl.
+ Qed.
+
+ Lemma ring_mul_0_r : forall x, x * 0 == 0.
+ Proof.
+  intro x; ring_replace (x*0)  (x*(0+1) + -x).
+  ring_rewrite ring_add_0_l ; ring_rewrite ring_mul_1_r .
+  ring_rewrite ring_opp_def ;rrefl.
+
+  ring_rewrite ring_distr_r ;ring_rewrite ring_mul_1_r .
+  ring_rewrite_rev ring_add_assoc ; ring_rewrite ring_opp_def .
+  ring_rewrite ring_add_comm ; ring_rewrite ring_add_0_l ;rrefl.
+ Qed.
+
+ Lemma ring_opp_mul_l : forall x y, -(x * y) == -x * y.
+ Proof.
+  intros x y;ring_rewrite_rev (ring_add_0_l (- x * y)).
+  ring_rewrite ring_add_comm .
+  ring_rewrite_rev (ring_opp_def (x*y)).
+  ring_rewrite ring_add_assoc .
+  ring_rewrite_rev ring_distr_l.
+  ring_rewrite (ring_add_comm (-x));ring_rewrite ring_opp_def .
+  ring_rewrite ring_mul_0_l;ring_rewrite ring_add_0_l ;rrefl.
+ Qed.
+
+Lemma ring_opp_mul_r : forall x y, -(x * y) == x * -y.
+ Proof.
+  intros x y;ring_rewrite_rev (ring_add_0_l (x * - y)).
+  ring_rewrite ring_add_comm .
+  ring_rewrite_rev (ring_opp_def (x*y)).
+  ring_rewrite ring_add_assoc .
+  ring_rewrite_rev ring_distr_r .
+  ring_rewrite (ring_add_comm (-y));ring_rewrite ring_opp_def .
+  ring_rewrite ring_mul_0_r;ring_rewrite ring_add_0_l ;rrefl.
+ Qed.
+
+ Lemma ring_opp_add : forall x y, -(x + y) == -x + -y.
+ Proof.
+  intros x y;ring_rewrite_rev (ring_add_0_l  (-(x+y))).
+  ring_rewrite_rev (ring_opp_def  x).
+  ring_rewrite_rev (ring_add_0_l  (x + - x + - (x + y))).
+  ring_rewrite_rev (ring_opp_def  y).
+  ring_rewrite (ring_add_comm  x).
+  ring_rewrite (ring_add_comm  y).
+  ring_rewrite_rev (ring_add_assoc  (-y)).
+  ring_rewrite_rev (ring_add_assoc  (- x)).
+  ring_rewrite (ring_add_assoc   y).
+  ring_rewrite (ring_add_comm  y).
+  ring_rewrite_rev (ring_add_assoc   (- x)).
+  ring_rewrite (ring_add_assoc  y).
+  ring_rewrite (ring_add_comm  y);ring_rewrite ring_opp_def .
+  ring_rewrite (ring_add_comm  (-x) 0);ring_rewrite ring_add_0_l .
+  ring_rewrite ring_add_comm; rrefl.
+ Qed.
+
+ Lemma ring_opp_opp : forall x, - -x == x.
+ Proof.
+  intros x; ring_rewrite_rev (ring_add_0_l (- -x)).
+  ring_rewrite_rev (ring_opp_def x).
+  ring_rewrite_rev ring_add_assoc ; ring_rewrite ring_opp_def .
+  ring_rewrite (ring_add_comm  x); ring_rewrite ring_add_0_l . rrefl.
+ Qed.
+
+ Lemma ring_sub_ext :
+      forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 - y1 == x2 - y2.
+ Proof.
+  intros.
+  ring_replace (x1 - y1)  (x1 + -y1).
+  ring_replace (x2 - y2)  (x2 + -y2).
+  ring_rewrite H;ring_rewrite H0;rrefl.
+  ring_rewrite ring_sub_def. rrefl.
+  ring_rewrite ring_sub_def. rrefl.
+ Qed.
+
+ Ltac mring_rewrite :=
+   repeat first
+     [ ring_rewrite ring_add_0_l
+     | ring_rewrite_rev (ring_add_comm 0)
+     | ring_rewrite ring_mul_1_l
+     | ring_rewrite ring_mul_0_l
+     | ring_rewrite ring_distr_l
+     | rrefl
+     ].
+
+ Lemma ring_add_0_r : forall x, (x + 0) == x.
+ Proof. intros; mring_rewrite. Qed.
+
+ 
+ Lemma ring_add_assoc1 : forall x y z, (x + y) + z == (y + z) + x.
+ Proof.
+  intros;ring_rewrite_rev (ring_add_assoc x).
+  ring_rewrite (ring_add_comm x);rrefl.
+ Qed.
+
+ Lemma ring_add_assoc2 : forall x y z, (y + x) + z == (y + z) + x.
+ Proof.
+  intros; repeat ring_rewrite_rev ring_add_assoc.
+   ring_rewrite (ring_add_comm x); rrefl.
+ Qed.
+
+ Lemma ring_opp_zero : -0 == 0.
+ Proof.
+  ring_rewrite_rev (ring_mul_0_r 0). ring_rewrite ring_opp_mul_l.
+  repeat ring_rewrite ring_mul_0_r. rrefl.
+ Qed.
+
+End Ring2.
+
+(** Some simplification tactics*)
+Ltac gen_reflexivity := rrefl.
+ 
+Ltac gen_ring_rewrite :=
+  repeat first
+     [ rrefl
+     | progress ring_rewrite ring_opp_zero
+     | ring_rewrite ring_add_0_l
+     | ring_rewrite ring_add_0_r
+     | ring_rewrite ring_mul_1_l 
+     | ring_rewrite ring_mul_1_r
+     | ring_rewrite ring_mul_0_l 
+     | ring_rewrite ring_mul_0_r 
+     | ring_rewrite ring_distr_l 
+     | ring_rewrite ring_distr_r 
+     | ring_rewrite ring_add_assoc 
+     | ring_rewrite ring_mul_assoc
+     | progress ring_rewrite ring_opp_add 
+     | progress ring_rewrite ring_sub_def 
+     | progress ring_rewrite_rev ring_opp_mul_l 
+     | progress ring_rewrite_rev ring_opp_mul_r ].
+
+Ltac gen_add_push x :=
+set_ring_notations;
+repeat (match goal with
+  | |- context [(?y + x) + ?z] =>
+     progress ring_rewrite (@ring_add_assoc2 _ _ x y z)
+  | |- context [(x + ?y) + ?z] =>
+     progress ring_rewrite  (@ring_add_assoc1 _ _ x y z)
+  end).
diff --git a/plugins/setoid_ring/Ring2_initial.v b/plugins/setoid_ring/Ring2_initial.v
new file mode 100644
index 000000000..38a300f71
--- /dev/null
+++ b/plugins/setoid_ring/Ring2_initial.v
@@ -0,0 +1,225 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import ZArith_base.
+Require Import Zpow_def.
+Require Import BinInt.
+Require Import BinNat.
+Require Import Ndiv_def Zdiv_def.
+Require Import Setoid.
+Require Export Ring2.
+Require Export Ring2_polynom.
+Import List.
+
+Set Implicit Arguments.
+
+(* An object to return when an expression is not recognized as a constant *)
+Definition NotConstant := false.
+
+(** Z is a ring and a setoid*)
+
+Lemma Zsth : Setoid_Theory Z (@eq Z).
+constructor;red;intros;subst;trivial.
+Qed.
+
+Definition Zr : Ring Z.
+apply (@Build_Ring Z Z0 (Zpos xH) Zplus Zmult Zminus Zopp (@eq Z)); 
+try apply Zsth; try (red; red; intros; rewrite H; reflexivity). 
+ exact Zplus_comm. exact Zplus_assoc.
+ exact Zmult_1_l.  exact Zmult_1_r. exact Zmult_assoc.
+ exact Zmult_plus_distr_l.  intros; apply Zmult_plus_distr_r. trivial. exact Zminus_diag.
+Defined.
+
+(** Two generic morphisms from Z to (abrbitrary) rings, *)
+(**second one is more convenient for proofs but they are ext. equal*)
+Section ZMORPHISM.
+ Variable R : Type.
+ Variable Rr: Ring R.
+Existing Instance Rr.
+ 
+ Ltac rrefl := gen_reflexivity Rr.
+
+(*
+Print HintDb typeclass_instances.
+Print Scopes.
+*)
+
+ Fixpoint gen_phiPOS1 (p:positive) : R :=
+  match p with
+  | xH => 1
+  | xO p => (1 + 1) * (gen_phiPOS1 p)
+  | xI p => 1 + ((1 + 1) * (gen_phiPOS1 p))
+  end.
+
+ Fixpoint gen_phiPOS (p:positive) : R :=
+  match p with
+  | xH => 1
+  | xO xH => (1 + 1)
+  | xO p => (1 + 1) * (gen_phiPOS p)
+  | xI xH => 1 + (1 +1)
+  | xI p => 1 + ((1 + 1) * (gen_phiPOS p))
+  end.
+
+ Definition gen_phiZ1 z :=
+  match z with
+  | Zpos p => gen_phiPOS1 p
+  | Z0 => 0
+  | Zneg p => -(gen_phiPOS1 p)
+  end.
+
+ Definition gen_phiZ z :=
+  match z with
+  | Zpos p => gen_phiPOS p
+  | Z0 => 0
+  | Zneg p => -(gen_phiPOS p)
+  end.
+ Notation "[ x ]" := (gen_phiZ x).
+
+ Definition get_signZ z :=
+  match z with
+  | Zneg p => Some (Zpos p)
+  | _ => None
+  end.
+
+   Ltac norm := gen_ring_rewrite.
+   Ltac add_push :=  gen_add_push.
+Ltac rsimpl := simpl;  set_ring_notations.
+
+ Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x.
+ Proof.
+  induction x;rsimpl.
+  ring_rewrite IHx. destruct x;simpl;norm.
+  ring_rewrite IHx;destruct x;simpl;norm.
+  gen_reflexivity.
+ Qed.
+
+ Lemma ARgen_phiPOS_Psucc : forall x,
+   gen_phiPOS1 (Psucc x) == 1 + (gen_phiPOS1 x).
+ Proof.
+  induction x;rsimpl;norm.
+  ring_rewrite IHx ;norm.
+  add_push 1;gen_reflexivity.
+ Qed.
+
+ Lemma ARgen_phiPOS_add : forall x y,
+   gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y).
+ Proof.
+  induction x;destruct y;simpl;norm.
+  ring_rewrite Pplus_carry_spec.
+  ring_rewrite ARgen_phiPOS_Psucc.
+  ring_rewrite IHx;norm.
+  add_push (gen_phiPOS1 y);add_push 1;gen_reflexivity.
+  ring_rewrite IHx;norm;add_push (gen_phiPOS1 y);gen_reflexivity.
+  ring_rewrite ARgen_phiPOS_Psucc;norm;add_push 1;gen_reflexivity.
+  ring_rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;gen_reflexivity.
+  ring_rewrite IHx;norm;add_push(gen_phiPOS1 y);gen_reflexivity.
+  add_push 1;gen_reflexivity.
+  ring_rewrite ARgen_phiPOS_Psucc;norm;add_push 1;gen_reflexivity.
+ Qed.
+
+ Lemma ARgen_phiPOS_mult :
+   forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y.
+ Proof.
+  induction x;intros;simpl;norm.
+  ring_rewrite ARgen_phiPOS_add;simpl;ring_rewrite IHx;norm.
+  ring_rewrite IHx;gen_reflexivity.
+ Qed.
+
+
+(*morphisms are extensionaly equal*)
+ Lemma same_genZ : forall x, [x] == gen_phiZ1 x.
+ Proof.
+  destruct x;rsimpl; try ring_rewrite same_gen; gen_reflexivity.
+ Qed.
+
+ Lemma gen_Zeqb_ok : forall x y,
+   Zeq_bool x y = true -> [x] == [y].
+ Proof.
+  intros x y H.
+  assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1.
+  ring_rewrite H1;gen_reflexivity.
+ Qed.
+
+ Lemma gen_phiZ1_add_pos_neg : forall x y,
+ gen_phiZ1
+    match (x ?= y)%positive Eq with
+    | Eq => Z0
+    | Lt => Zneg (y - x)
+    | Gt => Zpos (x - y)
+    end
+ == gen_phiPOS1 x + -gen_phiPOS1 y.
+ Proof.
+  intros x y.
+  assert (H:= (Pcompare_Eq_eq x y)); assert (H0 := Pminus_mask_Gt x y).
+  generalize (Pminus_mask_Gt y x).
+  replace Eq with (CompOpp Eq);[intro H1;simpl|trivial].
+  rewrite <- Pcompare_antisym in H1.
+  destruct ((x ?= y)%positive Eq).
+  ring_rewrite H;trivial. ring_rewrite ring_opp_def;gen_reflexivity.
+  destruct H1 as [h [Heq1 [Heq2 Hor]]];trivial.
+  unfold Pminus; ring_rewrite Heq1;rewrite <- Heq2.
+  ring_rewrite ARgen_phiPOS_add;simpl;norm.
+  ring_rewrite ring_opp_def;norm.
+  destruct H0 as [h [Heq1 [Heq2 Hor]]];trivial.
+  unfold Pminus; rewrite Heq1;rewrite <- Heq2.
+  ring_rewrite ARgen_phiPOS_add;simpl;norm.
+  set_ring_notations. add_push (gen_phiPOS1 h). ring_rewrite ring_opp_def ; norm.
+ Qed.
+
+ Lemma match_compOpp : forall x (B:Type) (be bl bg:B),
+  match CompOpp x with Eq => be | Lt => bl | Gt => bg end
+  = match x with Eq => be | Lt => bg | Gt => bl end.
+ Proof. destruct x;simpl;intros;trivial. Qed.
+
+ Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y].
+ Proof.
+  intros x y; repeat ring_rewrite same_genZ; generalize x y;clear x y.
+  induction x;destruct y;simpl;norm.
+  apply ARgen_phiPOS_add.
+  apply gen_phiZ1_add_pos_neg.
+  replace Eq with (CompOpp Eq);trivial.
+  rewrite <- Pcompare_antisym;simpl.
+  ring_rewrite match_compOpp.
+  ring_rewrite ring_add_comm.
+  apply gen_phiZ1_add_pos_neg.
+  ring_rewrite ARgen_phiPOS_add; norm.
+ Qed.
+
+Lemma gen_phiZ_opp : forall x, [- x] == - [x].
+ Proof.
+  intros x. repeat ring_rewrite same_genZ. generalize x ;clear x.
+  induction x;simpl;norm.
+  ring_rewrite ring_opp_opp.  gen_reflexivity.
+ Qed.
+
+ Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y].
+ Proof.
+  intros x y;repeat ring_rewrite same_genZ.
+  destruct x;destruct y;simpl;norm;
+  ring_rewrite  ARgen_phiPOS_mult;try (norm;fail).
+  ring_rewrite ring_opp_opp ;gen_reflexivity.
+ Qed.
+
+ Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y].
+ Proof. intros;subst;gen_reflexivity. Qed.
+
+(*proof that [.] satisfies morphism specifications*)
+ Lemma gen_phiZ_morph : @Ring_morphism Z R Zr Rr.
+ apply (Build_Ring_morphism Zr Rr gen_phiZ);simpl;try gen_reflexivity.
+   apply gen_phiZ_add. intros. ring_rewrite ring_sub_def. 
+replace (x-y)%Z with (x + (-y))%Z. ring_rewrite gen_phiZ_add. 
+ring_rewrite gen_phiZ_opp. gen_reflexivity.
+reflexivity.
+ apply gen_phiZ_mul. apply gen_phiZ_opp. apply gen_phiZ_ext. 
+ Defined.
+
+End ZMORPHISM.
+
+
+
+
diff --git a/plugins/setoid_ring/Ring2_polynom.v b/plugins/setoid_ring/Ring2_polynom.v
new file mode 100644
index 000000000..6fa0f200b
--- /dev/null
+++ b/plugins/setoid_ring/Ring2_polynom.v
@@ -0,0 +1,626 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*  A <X1,...,Xn>: non commutative polynomials on a commutative ring A *)
+
+Set Implicit Arguments.
+Require Import Setoid.
+Require Import BinList.
+Require Import BinPos.
+Require Import BinNat.
+Require Import BinInt.
+Require Export Ring2.
+
+Section MakeRingPol.
+
+Variable C:Type.
+Variable Cr:Ring C.
+Variable R:Type.
+Variable Rr:Ring R.
+
+Variable phi:@Ring_morphism C R Cr Rr.
+
+Existing Instance Rr.
+Existing Instance Cr.
+Existing Instance phi.
+(* marche pas avec x * [c] == [c] * x
+ou avec 
+Variable c:C.
+Variable x:C.
+Check [c]*x.
+ *)
+ Variable phiCR_comm: forall (c:C)(x:R), x * [c] == ring_mult [c] x.
+
+ Ltac rsimpl := repeat (gen_ring_rewrite || ring_rewrite phiCR_comm).
+ Ltac add_push := gen_add_push .
+
+(* Definition of non commutative multivariable polynomials 
+   with coefficients in C :
+ *)
+
+ Inductive Pol : Type :=
+  | Pc : C -> Pol
+  | PX : Pol -> positive -> positive -> Pol -> Pol. 
+    (* PX P i n Q represents P * X_i^n + Q *)
+Definition cO := @ring0 _ Cr.
+Definition cI := @ring1 _ Cr.
+
+ Definition P0 := Pc cO.
+ Definition P1 := Pc cI.
+
+Variable Ceqb:C->C->bool.
+Class Equalityb (A : Type):= {equalityb : A -> A -> bool}.
+Notation "x =? y" := (equalityb x y) (at level 70, no associativity).
+Variable Ceqb_eq: forall x y:C, Ceqb x y = true -> (x == y).
+
+Instance equalityb_coef : Equalityb C :=
+  {equalityb x y := Ceqb x y}.
+
+ Fixpoint Peq (P P' : Pol) {struct P'} : bool :=
+  match P, P' with
+  | Pc c, Pc c' => c =? c'
+  | PX P i n Q, PX P' i' n' Q' =>
+    match Pcompare i i' Eq, Pcompare n n' Eq with
+    | Eq, Eq => if Peq P P' then Peq Q Q' else false
+    | _,_ => false
+    end
+  | _, _ => false
+  end.
+
+Instance equalityb_pol : Equalityb Pol :=
+  {equalityb x y := Peq x y}.
+
+(* Q a ses variables de queue < i *)
+ Definition mkPX P i n Q :=
+  match P with
+  | Pc c => if c =? cO then Q else PX P i n Q 
+  | PX P' i' n' Q' => 
+       match Pcompare i i' Eq with
+        | Eq => if Q' =? P0 then PX P' i (n + n') Q else PX P i n Q
+        | _ => PX P i n Q
+       end
+  end.
+
+ Definition mkXi i n := PX P1 i n P0.
+
+ Definition mkX i := mkXi i 1.
+
+ (** Opposite of addition *)
+
+ Fixpoint Popp (P:Pol) : Pol :=
+  match P with
+  | Pc c => Pc (- c)
+  | PX P i n Q => PX (Popp P) i n (Popp Q)
+  end.
+
+ Notation "-- P" := (Popp P)(at level 30).
+
+ (** Addition et subtraction *)
+
+ Fixpoint PaddCl (c:C)(P:Pol) {struct P} : Pol :=
+  match P with
+  | Pc c1 => Pc (c + c1)
+  | PX P i n Q => PX P i n (PaddCl c Q)
+  end.
+
+(* Q quelconque *)
+
+Section PaddX.
+Variable Padd:Pol->Pol->Pol.
+Variable P:Pol.
+
+(* Xi^n * P + Q
+les variables de tete de Q ne sont pas forcement < i 
+mais Q est normalisé : variables de tete decroissantes *)
+
+Fixpoint PaddX (i n:positive)(Q:Pol){struct Q}:=
+  match Q with
+  | Pc c => mkPX P i n Q
+  | PX P' i' n' Q' => 
+      match Pcompare i i' Eq with
+      | (* i > i' *)
+        Gt => mkPX P i n Q
+      | (* i < i' *)
+        Lt => mkPX P' i' n' (PaddX i n Q')
+      | (* i = i' *)
+        Eq => match ZPminus n n' with
+              | (* n > n' *) 
+                Zpos k => mkPX (PaddX i k P') i' n' Q'
+              | (* n = n' *)
+                Z0 => mkPX (Padd P P') i n Q'
+              | (* n < n' *)
+                Zneg k => mkPX (Padd P (mkPX P' i k P0)) i n Q'
+              end
+      end
+  end.
+
+End PaddX.
+
+Fixpoint Padd (P1 P2: Pol) {struct P1} : Pol :=
+  match P1 with
+  | Pc c => PaddCl c P2
+  | PX P' i' n' Q' =>
+      PaddX Padd P' i' n' (Padd Q' P2)
+  end.
+
+ Notation "P ++ P'" := (Padd P P').
+
+Definition Psub(P P':Pol):= P ++ (--P').
+
+ Notation "P -- P'" := (Psub P P')(at level 50).
+
+ (** Multiplication *)
+
+ Fixpoint PmulC_aux (P:Pol) (c:C)  {struct P} : Pol :=
+  match P with
+  | Pc c' => Pc (c' * c)
+  | PX P i n Q => mkPX (PmulC_aux P c) i n (PmulC_aux Q c)
+  end.
+
+ Definition PmulC P c :=
+  if c =? cO then P0 else
+  if c =? cI then P else PmulC_aux P c.
+
+ Fixpoint Pmul (P1 P2 : Pol) {struct P2} : Pol :=
+   match P2 with
+   | Pc c => PmulC P1 c
+   | PX P i n Q =>
+     PaddX Padd (Pmul P1 P) i n (Pmul P1 Q)
+   end.
+
+ Notation "P ** P'" := (Pmul P P')(at level 40).
+
+ Definition Psquare (P:Pol) : Pol := P ** P.
+
+
+ (** Evaluation of a polynomial towards R *)
+
+ Fixpoint Pphi(l:list R) (P:Pol) {struct P} : R :=
+  match P with
+  | Pc c => [c]
+  | PX P i n Q =>
+     let x := nth 0 i l in
+     let xn := pow_pos Rr x n in
+   (Pphi l P) * xn + (Pphi l Q)
+  end.
+
+ Reserved Notation "P @ l " (at level 10, no associativity).
+ Notation "P @ l " := (Pphi l P).
+ (** Proofs *)
+ Lemma ZPminus_spec : forall x y,
+  match ZPminus x y with
+  | Z0 => x = y
+  | Zpos k => x = (y + k)%positive
+  | Zneg k => y = (x + k)%positive
+  end.
+ Proof.
+  induction x;destruct y.
+  replace (ZPminus (xI x) (xI y)) with (Zdouble (ZPminus x y));trivial.
+  assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite H;trivial.
+  replace (ZPminus (xI x) (xO y)) with (Zdouble_plus_one (ZPminus x y));trivial.
+  assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble_plus_one;rewrite H;trivial.
+  apply Pplus_xI_double_minus_one.
+  simpl;trivial.
+  replace (ZPminus (xO x) (xI y)) with (Zdouble_minus_one (ZPminus x y));trivial.
+  assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble_minus_one;rewrite H;trivial.
+  apply Pplus_xI_double_minus_one.
+  replace (ZPminus (xO x) (xO y)) with (Zdouble (ZPminus x y));trivial.
+  assert (H := IHx y);destruct (ZPminus x y);unfold Zdouble;rewrite H;trivial.
+  replace (ZPminus (xO x) xH) with (Zpos (Pdouble_minus_one x));trivial.
+  rewrite <- Pplus_one_succ_l.
+  rewrite Psucc_o_double_minus_one_eq_xO;trivial.
+  replace (ZPminus xH (xI y)) with (Zneg (xO y));trivial.
+  replace (ZPminus xH (xO y)) with (Zneg (Pdouble_minus_one y));trivial.
+  rewrite <- Pplus_one_succ_l.
+  rewrite Psucc_o_double_minus_one_eq_xO;trivial.
+  simpl;trivial.
+ Qed.
+
+ Lemma Peq_ok : forall P P',
+    (P =? P') = true -> forall l, P@l == P'@ l.
+ Proof.
+  induction P;destruct P';simpl;intros;try discriminate;trivial. apply ring_morphism_eq.
+ apply Ceqb_eq ;trivial.
+
+  assert (H1 := IHP1 P'1);assert (H2 := IHP2 P'2).
+   simpl in H1. destruct (Peq P2 P'1). simpl in H2; destruct (Peq P3 P'2).
+  ring_rewrite (H1);trivial . ring_rewrite (H2);trivial. 
+assert (H3 := Pcompare_Eq_eq p p1);
+ destruct ((p ?= p1)%positive Eq);
+assert (H4 := Pcompare_Eq_eq p0 p2);
+destruct ((p0 ?= p2)%positive Eq); try (discriminate H).
+ ring_rewrite H3;trivial. ring_rewrite H4;trivial. rrefl.
+ destruct ((p ?= p1)%positive Eq); destruct ((p0 ?= p2)%positive Eq);
+ try (discriminate H).
+ destruct ((p ?= p1)%positive Eq); destruct ((p0 ?= p2)%positive Eq);
+ try (discriminate H). 
+ Qed.
+
+ Lemma Pphi0 : forall l, P0@l == 0.
+ Proof.
+  intros;simpl. unfold cO. ring_rewrite ring_morphism0. rrefl.
+ Qed.
+
+ Lemma Pphi1 : forall l,  P1@l == 1.
+ Proof.
+  intros;simpl; unfold cI; ring_rewrite ring_morphism1. rrefl.
+ Qed.
+
+ Let pow_pos_Pplus :=
+    pow_pos_Pplus Rr.
+
+ Lemma mkPX_ok : forall l P i n Q,
+  (mkPX P i n Q)@l == P@l * (pow_pos Rr (nth 0 i l) n) + Q@l.
+ Proof.
+  intros l P i n Q;unfold mkPX.
+  destruct P;try (simpl;rrefl).
+  assert (H := ring_morphism_eq  c cO). simpl; case_eq (Ceqb c cO);simpl;try rrefl.
+intros.
+  ring_rewrite H. ring_rewrite ring_morphism0.
+  rsimpl. apply Ceqb_eq. trivial. assert (H1 := Pcompare_Eq_eq i p);
+destruct ((i ?= p)%positive Eq).
+  assert (H := @Peq_ok P3 P0). case_eq (P3=? P0). intro. simpl. 
+  ring_rewrite H. 
+  ring_rewrite Pphi0. rsimpl. ring_rewrite Pplus_comm. ring_rewrite pow_pos_Pplus;rsimpl.
+ring_rewrite H1;trivial. rrefl. trivial. intros. simpl. rrefl. simpl. rrefl.
+ simpl. rrefl.
+ Qed.
+
+Ltac Esimpl :=
+  repeat (progress (
+   match goal with
+   | |- context [?P@?l] =>
+       match P with
+       | P0 => ring_rewrite (Pphi0 l)
+       | P1 => ring_rewrite (Pphi1 l)
+       | (mkPX ?P ?i ?n ?Q) => ring_rewrite (mkPX_ok l P i n Q)
+       end
+   | |- context [[?c]] =>
+       match c with
+       | cO => ring_rewrite ring_morphism0
+       | cI => ring_rewrite ring_morphism1
+       | ?x + ?y => ring_rewrite ring_morphism_add
+       | ?x * ?y => ring_rewrite ring_morphism_mul
+       | ?x - ?y => ring_rewrite ring_morphism_sub
+       | - ?x => ring_rewrite ring_morphism_opp
+       end
+   end));
+  ring_simpl; rsimpl.
+
+ Lemma PaddCl_ok : forall c P l, (PaddCl c P)@l == [c] + P@l .
+ Proof.
+  induction P; ring_simpl; intros; Esimpl; try rrefl. 
+  ring_rewrite IHP2. rsimpl. 
+ring_rewrite (ring_add_comm  (P2 @ l * pow_pos Rr (nth 0 p l) p0) [c]).
+rrefl.
+ Qed.
+
+ Lemma PmulC_aux_ok : forall c P l, (PmulC_aux P c)@l ==  P@l * [c].
+ Proof.
+  induction P;ring_simpl;intros;Esimpl;try rrefl.
+  ring_rewrite IHP1;ring_rewrite IHP2;rsimpl. 
+ Qed.
+
+ Lemma PmulC_ok : forall c P l, (PmulC P c)@l ==  P@l * [c].
+ Proof.
+  intros c P l; unfold PmulC.
+  assert (H:= ring_morphism_eq c cO);case_eq (c =? cO). intros.
+  ring_rewrite H;Esimpl. apply Ceqb_eq;trivial. 
+  assert (H1:= ring_morphism_eq c cI);case_eq (c =? cI);intros.
+  ring_rewrite H1;Esimpl. apply Ceqb_eq;trivial.
+  apply PmulC_aux_ok.
+ Qed.
+
+ Lemma Popp_ok : forall P l, (--P)@l == - P@l.
+ Proof.
+  induction P;ring_simpl;intros.
+  Esimpl.
+  ring_rewrite IHP1;ring_rewrite IHP2;rsimpl.
+ Qed.
+
+ Ltac Esimpl2 :=
+  Esimpl;
+  repeat (progress (
+   match goal with
+   | |- context [(PaddCl ?c ?P)@?l] => ring_rewrite (PaddCl_ok c P l)
+   | |- context [(PmulC ?P ?c)@?l] => ring_rewrite (PmulC_ok c P l)
+   | |- context [(--?P)@?l] => ring_rewrite (Popp_ok P l)
+   end)); Esimpl.
+
+Lemma PaddXPX: forall P i n Q,
+  PaddX Padd P i n Q =
+  match Q with
+  | Pc c => mkPX P i n Q
+  | PX P' i' n' Q' => 
+      match Pcompare i i' Eq with
+      | (* i > i' *)
+        Gt => mkPX P i n Q
+      | (* i < i' *)
+        Lt => mkPX P' i' n' (PaddX Padd P i n Q')
+      | (* i = i' *)
+        Eq => match ZPminus n n' with
+              | (* n > n' *) 
+                Zpos k => mkPX (PaddX Padd P i k P') i' n' Q'
+              | (* n = n' *)
+                Z0 => mkPX (Padd P P') i n Q'
+              | (* n < n' *)
+                Zneg k => mkPX (Padd P (mkPX P' i k P0)) i n Q'
+              end
+      end
+  end.
+induction Q; reflexivity.
+Qed.
+
+Lemma PaddX_ok2 : forall P2,
+   (forall P l, (P2 ++ P) @ l == P2 @ l + P @ l)
+   /\
+   (forall P k n l,
+           (PaddX Padd P2 k n P) @ l == 
+             P2 @ l * pow_pos Rr (nth 0 k l) n  + P @ l).
+induction P2;ring_simpl;intros. split. intros. apply PaddCl_ok.
+ induction P.  unfold PaddX. intros. ring_rewrite mkPX_ok.
+ ring_simpl. rsimpl.
+intros. ring_simpl. assert (H := Pcompare_Eq_eq k p);
+ destruct ((k ?= p)%positive Eq).
+ assert (H1 := ZPminus_spec n p0);destruct (ZPminus n p0). Esimpl2.
+ring_rewrite H; trivial. rewrite H1. rrefl.
+ring_simpl. ring_rewrite mkPX_ok. ring_rewrite IHP1. Esimpl2.
+ rewrite Pplus_comm in H1.
+rewrite H1. 
+ring_rewrite pow_pos_Pplus.  Esimpl2.
+rewrite H; trivial. rrefl.
+ring_rewrite mkPX_ok. ring_rewrite PaddCl_ok. Esimpl2. rewrite Pplus_comm in H1.
+rewrite H1.  Esimpl2. ring_rewrite pow_pos_Pplus. Esimpl2.
+rewrite H; trivial. rrefl.
+ring_rewrite mkPX_ok. ring_rewrite IHP2. Esimpl2.
+ring_rewrite (ring_add_comm  (P2 @ l * pow_pos Rr (nth 0 p l) p0) 
+                             ([c] * pow_pos Rr (nth 0 k l) n)).
+rrefl.  assert (H1 := ring_morphism_eq c cO);case_eq (Ceqb c  cO); 
+ intros; ring_simpl.
+ring_rewrite H1;trivial. Esimpl2. apply Ceqb_eq; trivial. rrefl.
+decompose [and] IHP2_1. decompose [and] IHP2_2. clear IHP2_1 IHP2_2.
+split. intros. ring_rewrite H0. ring_rewrite H1.
+Esimpl2.
+induction P. unfold PaddX. intros. ring_rewrite mkPX_ok. ring_simpl. rrefl.
+intros. ring_rewrite PaddXPX. 
+assert (H3 := Pcompare_Eq_eq k p1);
+ destruct ((k ?= p1)%positive Eq).
+assert (H4 := ZPminus_spec n p2);destruct (ZPminus n p2). 
+ring_rewrite mkPX_ok. ring_simpl. ring_rewrite H0. ring_rewrite H1. Esimpl2.
+rewrite H4. rewrite H3;trivial. rrefl.
+ring_rewrite mkPX_ok. ring_rewrite IHP1. Esimpl2. rewrite H3;trivial.
+rewrite Pplus_comm in H4.
+rewrite H4. ring_rewrite pow_pos_Pplus. Esimpl2.
+ring_rewrite mkPX_ok. ring_simpl. ring_rewrite H0. ring_rewrite H1. 
+ring_rewrite mkPX_ok.
+ Esimpl2. rewrite H3;trivial.
+ rewrite Pplus_comm in H4.
+rewrite H4. ring_rewrite pow_pos_Pplus. Esimpl2.
+ring_rewrite mkPX_ok. ring_simpl. ring_rewrite IHP2. Esimpl2.
+gen_add_push (P2 @ l * pow_pos Rr (nth 0 p1 l) p2). try rrefl.
+ring_rewrite mkPX_ok. ring_simpl. rrefl.
+Qed.
+
+Lemma Padd_ok : forall P Q l, (P ++ Q) @ l == P @ l + Q @ l.
+intro P. elim (PaddX_ok2 P); auto.
+Qed.
+
+Lemma PaddX_ok : forall P2 P k n l,
+   (PaddX Padd P2 k n P) @ l ==  P2 @ l * pow_pos Rr (nth 0 k l) n  + P @ l.
+intro P2. elim (PaddX_ok2 P2); auto.
+Qed.
+
+ Lemma Psub_ok : forall P' P l, (P -- P')@l == P@l - P'@l.
+unfold Psub. intros. ring_rewrite Padd_ok. ring_rewrite Popp_ok. rsimpl.
+ Qed.
+
+ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
+induction P'; ring_simpl; intros. ring_rewrite PmulC_ok. rrefl.
+ring_rewrite PaddX_ok. ring_rewrite IHP'1. ring_rewrite IHP'2. Esimpl2.
+Qed.
+
+ Lemma Psquare_ok : forall P l, (Psquare P)@l == P@l * P@l.
+ Proof.
+  intros. unfold Psquare. apply Pmul_ok.
+ Qed.
+
+ (** Definition of polynomial expressions *)
+
+ Inductive PExpr : Type :=
+  | PEc : C -> PExpr
+  | PEX : positive -> PExpr
+  | PEadd : PExpr -> PExpr -> PExpr
+  | PEsub : PExpr -> PExpr -> PExpr
+  | PEmul : PExpr -> PExpr -> PExpr
+  | PEopp : PExpr -> PExpr
+  | PEpow : PExpr -> N -> PExpr.
+
+ (** Specification of the power function *)
+ Section POWER.
+  Variable Cpow : Set.
+  Variable Cp_phi : N -> Cpow.
+  Variable rpow : R -> Cpow -> R.
+
+  Record power_theory : Prop := mkpow_th {
+    rpow_pow_N : forall r n,  (rpow r (Cp_phi n))== (pow_N Rr r n)
+  }.
+
+ End POWER.
+ Variable Cpow : Set.
+ Variable Cp_phi : N -> Cpow.
+ Variable rpow : R -> Cpow -> R.
+ Variable pow_th : power_theory Cp_phi rpow.
+
+ (** evaluation of polynomial expressions towards R *)
+ Fixpoint PEeval (l:list R) (pe:PExpr) {struct pe} : R :=
+   match pe with
+   | PEc c => [c]
+   | PEX j => nth 0 j l
+   | PEadd pe1 pe2 => (PEeval l pe1) + (PEeval l pe2)
+   | PEsub pe1 pe2 => (PEeval l pe1) - (PEeval l pe2)
+   | PEmul pe1 pe2 => (PEeval l pe1) * (PEeval l pe2)
+   | PEopp pe1 => - (PEeval l pe1)
+   | PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n)
+   end.
+
+Strategy expand [PEeval].
+
+ Definition mk_X j := mkX j.
+
+ (** Correctness proofs *)
+
+ Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l.
+ Proof.
+  destruct p;ring_simpl;intros;Esimpl;trivial.
+ Qed.
+
+ Ltac Esimpl3 :=
+  repeat match goal with
+  | |- context [(?P1 ++ ?P2)@?l] => ring_rewrite (Padd_ok P1 P2 l)
+  | |- context [(?P1 -- ?P2)@?l] => ring_rewrite (Psub_ok P1 P2 l)
+  end;try Esimpl2;try rrefl;try apply ring_add_comm.
+
+(* Power using the chinise algorithm *)
+
+Section POWER2.
+  Variable subst_l : Pol -> Pol.
+  Fixpoint Ppow_pos (res P:Pol) (p:positive){struct p} : Pol :=
+   match p with
+   | xH => subst_l (Pmul P res)
+   | xO p => Ppow_pos (Ppow_pos res P p) P p
+   | xI p => subst_l (Pmul P (Ppow_pos (Ppow_pos res P p) P p))
+   end.
+
+  Definition Ppow_N P n :=
+   match n with
+   | N0 => P1
+   | Npos p => Ppow_pos P1 P p
+   end.
+
+  Fixpoint pow_pos_gen (R:Type)(m:R->R->R)(x:R) (i:positive) {struct i}: R :=
+  match i with
+  | xH => x
+  | xO i => let p := pow_pos_gen m x i in m p p
+  | xI i => let p := pow_pos_gen m x i in m x (m p p)
+  end.
+
+Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) ->
+         forall res P p, (Ppow_pos res P p)@l == (pow_pos_gen Pmul P p)@l * res@l.
+  Proof.
+   intros l subst_l_ok res P p. generalize res;clear res.
+   induction p;ring_simpl;intros. try ring_rewrite subst_l_ok.
+ repeat ring_rewrite Pmul_ok. repeat ring_rewrite IHp.
+   rsimpl. repeat ring_rewrite Pmul_ok. repeat ring_rewrite IHp. rsimpl.
+ try ring_rewrite subst_l_ok.
+ repeat ring_rewrite Pmul_ok. rrefl.
+  Qed.
+
+Definition pow_N_gen (R:Type)(x1:R)(m:R->R->R)(x:R) (p:N) :=
+  match p with
+  | N0 => x1
+  | Npos p => pow_pos_gen m x p
+  end.
+
+  Lemma Ppow_N_ok : forall l,  (forall P, subst_l P@l == P@l) ->
+         forall P n, (Ppow_N P n)@l == (pow_N_gen P1 Pmul P n)@l.
+  Proof.  destruct n;ring_simpl. rrefl. ring_rewrite Ppow_pos_ok; trivial. Esimpl.  Qed.
+
+ End POWER2.
+
+ (** Normalization and rewriting *)
+
+ Section NORM_SUBST_REC.
+  Let subst_l (P:Pol) := P.
+  Let Pmul_subst P1 P2 := subst_l (Pmul P1 P2).
+  Let Ppow_subst := Ppow_N subst_l.
+
+  Fixpoint norm_aux (pe:PExpr) : Pol :=
+   match pe with
+   | PEc c => Pc c
+   | PEX j => mk_X j
+   | PEadd pe1 (PEopp pe2) =>
+     Psub (norm_aux pe1) (norm_aux pe2)
+   | PEadd pe1 pe2 => Padd (norm_aux  pe1) (norm_aux pe2)
+   | PEsub pe1 pe2 => Psub (norm_aux pe1) (norm_aux pe2)
+   | PEmul pe1 pe2 => Pmul (norm_aux pe1) (norm_aux pe2)
+   | PEopp pe1 => Popp (norm_aux pe1)
+   | PEpow pe1 n => Ppow_N (fun p => p) (norm_aux pe1) n
+   end.
+
+  Definition norm_subst pe := subst_l (norm_aux pe).
+
+ 
+ Lemma norm_aux_spec :
+     forall l pe, 
+       PEeval l pe == (norm_aux pe)@l.
+  Proof.
+   intros.
+   induction pe.
+Esimpl3. Esimpl3. ring_simpl.
+ ring_rewrite IHpe1;ring_rewrite IHpe2.
+ destruct pe2; Esimpl3. 
+unfold Psub.
+destruct pe1. destruct pe2. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3.
+ Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3.
+ring_simpl. unfold Psub. ring_rewrite IHpe1;ring_rewrite IHpe2.
+destruct pe1. destruct pe2. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3.
+ Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3. Esimpl3.
+ring_simpl. ring_rewrite IHpe1;ring_rewrite IHpe2. ring_rewrite Pmul_ok. rrefl.
+ring_simpl. ring_rewrite IHpe; Esimpl3. 
+ring_simpl.
+   ring_rewrite Ppow_N_ok; (intros;try rrefl). 
+   ring_rewrite rpow_pow_N.  Esimpl3.
+   induction n;ring_simpl. Esimpl3. induction p; ring_simpl.
+  try ring_rewrite IHp;try ring_rewrite IHpe;
+ repeat ring_rewrite Pms_ok;
+      repeat ring_rewrite Pmul_ok;rrefl.
+ring_rewrite Pmul_ok. try ring_rewrite IHp;try ring_rewrite IHpe;
+ repeat ring_rewrite Pms_ok;
+      repeat ring_rewrite Pmul_ok;rrefl. trivial.
+exact pow_th.
+  Qed.
+
+ Lemma norm_subst_spec :
+     forall l pe, 
+       PEeval l pe == (norm_subst pe)@l.
+ Proof.
+  intros;unfold norm_subst.
+  unfold subst_l.  apply norm_aux_spec. 
+ Qed.
+
+ End NORM_SUBST_REC.
+
+ Fixpoint interp_PElist (l:list R) (lpe:list (PExpr*PExpr)) {struct lpe} : Prop :=
+   match lpe with
+   | nil => True
+   | (me,pe)::lpe =>
+     match lpe with
+     | nil => PEeval l me == PEeval l pe
+     | _ => PEeval l me == PEeval l pe /\ interp_PElist l lpe
+     end
+  end.
+
+
+ Lemma norm_subst_ok : forall l pe,
+   PEeval l pe == (norm_subst pe)@l.
+ Proof.
+   intros;apply norm_subst_spec. 
+  Qed.
+
+
+ Lemma ring_correct : forall l pe1 pe2,
+   (norm_subst pe1 =? norm_subst pe2) = true ->
+   PEeval l pe1 == PEeval l pe2.
+ Proof.
+  ring_simpl;intros.
+  do 2 (ring_rewrite (norm_subst_ok l);trivial).
+  apply Peq_ok;trivial.
+ Qed.
+
+
+End MakeRingPol.
\ No newline at end of file
diff --git a/plugins/setoid_ring/Ring2_tac.v b/plugins/setoid_ring/Ring2_tac.v
new file mode 100644
index 000000000..1df1b8e73
--- /dev/null
+++ b/plugins/setoid_ring/Ring2_tac.v
@@ -0,0 +1,189 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Import List.
+Require Import Setoid.
+Require Import BinPos.
+Require Import BinList.
+Require Import Znumtheory.
+Require Export Morphisms Setoid Bool.
+Require Import ZArith.
+Require Import Algebra_syntax.
+Require Export Ring2.
+Require Import Ring2_polynom.
+Require Import Ring2_initial.
+
+
+Set Implicit Arguments.
+
+(* Reification with Type Classes, inspired from B.Grégoire and A.Spiewack *)
+
+Class is_in_list_at (R:Type) (t:R) (l:list R) (i:nat) := {}.
+Instance  Ifind0 (R:Type) (t:R) l
+ : is_in_list_at t (t::l) 0.
+Instance  IfindS (R:Type) (t2 t1:R) l i 
+ `{is_in_list_at R t1 l i} 
+ : is_in_list_at t1 (t2::l) (S i) | 1.
+
+Class reifyPE (R:Type) (e:PExpr Z) (lvar:list R) (t:R) := {}.
+Instance  reify_zero (R:Type) (RR:Ring R) lvar 
+ : reifyPE (PEc 0%Z) lvar ring0.
+Instance  reify_one (R:Type) (RR:Ring R) lvar 
+ : reifyPE (PEc 1%Z) lvar ring1.
+Instance  reify_plus (R:Type)  (RR:Ring R)
+  e1 lvar t1 e2 t2 
+ `{reifyPE R e1 lvar t1} 
+ `{reifyPE R e2 lvar t2} 
+ : reifyPE (PEadd e1 e2) lvar (ring_plus t1 t2).
+Instance  reify_mult (R:Type)  (RR:Ring R)
+  e1 lvar t1 e2 t2 
+ `{reifyPE R e1 lvar t1} 
+ `{reifyPE R e2 lvar t2}
+ : reifyPE (PEmul e1 e2) lvar (ring_mult t1 t2).
+Instance  reify_sub (R:Type) (RR:Ring R) 
+ e1 lvar t1 e2 t2 
+ `{reifyPE R e1 lvar t1} 
+ `{reifyPE R e2 lvar t2}
+ : reifyPE (PEsub e1 e2) lvar (ring_sub t1 t2).
+Instance  reify_opp (R:Type) (RR:Ring R) 
+ e1 lvar t1 
+ `{reifyPE R e1 lvar t1}
+ : reifyPE (PEopp e1) lvar (ring_opp t1).
+Instance  reify_var (R:Type) t lvar i 
+ `{is_in_list_at R t lvar i}
+ : reifyPE (PEX Z (P_of_succ_nat i)) lvar t 
+ | 100.
+
+Class reifyPElist (R:Type) (lexpr:list (PExpr Z)) (lvar:list R) 
+  (lterm:list R) := {}.
+Instance reifyPE_nil (R:Type) lvar 
+ : @reifyPElist R nil lvar (@nil R).
+Instance reifyPE_cons (R:Type) e1 lvar t1 lexpr2 lterm2
+ `{reifyPE R e1 lvar t1} `{reifyPElist R lexpr2 lvar lterm2} 
+ : reifyPElist (e1::lexpr2) lvar (t1::lterm2).
+
+Class is_closed_list T (l:list T) := {}.
+Instance Iclosed_nil T 
+ : is_closed_list (T:=T) nil.
+Instance Iclosed_cons T t l 
+ `{is_closed_list (T:=T) l} 
+ : is_closed_list (T:=T) (t::l).
+
+Definition list_reifyl (R:Type) lexpr lvar lterm 
+ `{reifyPElist R lexpr lvar lterm}
+ `{is_closed_list (T:=R) lvar} := (lvar,lexpr).
+
+Unset Implicit Arguments.
+
+Instance multiplication_phi_ring{R:Type}{Rr:Ring R} : Multiplication  :=
+  {multiplication x y := ring_mult (gen_phiZ Rr x) y}.
+
+(*
+Print HintDb typeclass_instances.
+*)
+(* Reification *)
+
+Ltac lterm_goal g :=
+  match g with
+  ring_eq ?t1 ?t2 => constr:(t1::t2::nil)
+  | ring_eq ?t1 ?t2 -> ?g => let lvar :=
+    lterm_goal g in constr:(t1::t2::lvar)     
+  end.
+
+Ltac reify_goal lvar lexpr lterm:=
+(*  idtac lvar; idtac lexpr; idtac lterm;*)
+  match lexpr with
+     nil => idtac
+   | ?e::?lexpr1 =>  
+        match lterm with
+         ?t::?lterm1 => (* idtac "t="; idtac t;*)
+           let x := fresh "T" in
+           set (x:= t);
+           change x with 
+             (@PEeval Z Zr _ _ (@gen_phiZ_morph _ _) N
+                      (fun n:N => n) (@Ring_theory.pow_N _ ring1 ring_mult)
+                      lvar e); 
+           clear x;
+           reify_goal lvar lexpr1 lterm1
+        end
+  end.
+
+Existing Instance gen_phiZ_morph.
+Existing Instance Zr.
+
+Lemma comm: forall (R:Type)(Rr:Ring R)(c : Z) (x : R),
+  x * [c] == [c] * x.
+induction c. intros. ring_simpl. gen_ring_rewrite. simpl. intros.
+ring_rewrite_rev same_gen.
+induction p. simpl.  gen_ring_rewrite. ring_rewrite IHp. rrefl.
+simpl.  gen_ring_rewrite. ring_rewrite IHp. rrefl.
+simpl.  gen_ring_rewrite. 
+simpl. intros. ring_rewrite_rev same_gen.
+induction p. simpl. generalize IHp. clear IHp.
+gen_ring_rewrite. intro IHp.  ring_rewrite IHp. rrefl.
+simpl. generalize IHp. clear IHp.
+gen_ring_rewrite. intro IHp.  ring_rewrite IHp. rrefl.
+simpl.  gen_ring_rewrite. Qed.
+
+Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y.
+ intros x y H. rewrite (Zeq_bool_eq x y H). rrefl. Qed. 
+
+
+ Ltac ring_gen :=
+   match goal with
+     |- ?g => let lterm := lterm_goal g in (* les variables *)
+       match eval red in (list_reifyl (lterm:=lterm)) with
+         | (?fv, ?lexpr) => 
+(*         idtac "variables:";idtac fv;
+           idtac "terms:"; idtac lterm;
+           idtac "reifications:"; idtac lexpr; 
+*)
+           reify_goal fv lexpr lterm;
+           match goal with 
+             |- ?g => 
+               set_ring_notations;
+               apply (@ring_correct Z Zr _ _ (@gen_phiZ_morph _ _)
+                 (@comm _ _) Zeq_bool Zeqb_ok N (fun n:N => n)
+                 (@Ring_theory.pow_N _  1 multiplication));
+               [apply mkpow_th; rrefl
+                 |vm_compute; reflexivity]
+           end
+       end
+   end.
+ 
+Ltac ring2:= 
+  unset_ring_notations; intros;
+  match goal with
+    |- (@ring_eq ?r ?rd _ _ ) =>
+          simpl; ring_gen
+  end.
+Variable R: Type.
+Variable Rr: Ring R.
+Existing Instance Rr.
+
+Goal forall x y z:R, x  == x .
+ring2. 
+Qed.
+
+Goal forall x y z:R, x * y * z == x * (y * z).
+ring2.
+Qed.
+
+Goal forall x y z:R, [3%Z]* x *([2%Z]* y * z) == [6%Z] * (x * y) * z.
+ring2.
+Qed.
+
+Goal forall x y z:R, 3%Z * x * (2%Z * y * z) == 6%Z * (x * y) * z.
+ring2.
+Qed.
+
+
+(* Fails with Multiplication: A -> B -> C.
+Goal forall x:R,    2%Z * (x * x) == 3%Z * x.
+Admitted.
+*)
\ No newline at end of file
diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget
index 6934375bc..cccd21855 100644
--- a/plugins/setoid_ring/vo.itarget
+++ b/plugins/setoid_ring/vo.itarget
@@ -13,3 +13,11 @@ Ring_tac.vo
 Ring_theory.vo
 Ring.vo
 ZArithRing.vo
+Algebra_syntax.vo
+Cring.vo
+Cring_initial.vo
+Cring_tac.vo
+Ring2.vo
+Ring2_polynom.vo
+Ring2_initial.vo
+Ring2_tac.vo
\ No newline at end of file