1 files changed, 74 insertions, 0 deletions
diff --git a/plugins/setoid_ring/Ring_equiv.v b/plugins/setoid_ring/Ring_equiv.v
new file mode 100644
index 00000000..945f6c68
--- /dev/null
+++ b/plugins/setoid_ring/Ring_equiv.v
@@ -0,0 +1,74 @@
+Require Import Setoid_ring_theory.
+Require Import LegacyRing_theory.
+Require Import Ring_theory.
+
+Set Implicit Arguments.
+
+Section Old2New.
+
+Variable A : Type.
+
+Variable Aplus : A -> A -> A.
+Variable Amult : A -> A -> A.
+Variable Aone : A.
+Variable Azero : A.
+Variable Aopp : A -> A.
+Variable Aeq : A -> A -> bool.
+Variable R : Ring_Theory Aplus Amult Aone Azero Aopp Aeq.
+
+Let Aminus := fun x y => Aplus x (Aopp y).
+
+Lemma ring_equiv1 :
+  ring_theory Azero Aone Aplus Amult Aminus Aopp (eq (A:=A)).
+Proof.
+destruct R.
+split;  eauto.
+Qed.
+
+End Old2New.
+
+Section New2OldRing.
+ Variable R : Type.
+ Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
+ Variable Rth : ring_theory rO rI radd rmul rsub ropp (eq (A:=R)).
+
+ Variable reqb : R -> R -> bool.
+ Variable reqb_ok : forall x y, reqb x y = true -> x = y.
+
+ Lemma ring_equiv2 :
+   Ring_Theory radd  rmul rI rO ropp reqb.
+Proof.
+elim Rth; intros; constructor;  eauto.
+intros.
+apply reqb_ok.
+destruct (reqb x y); trivial; intros.
+elim H.
+Qed.
+
+ Definition default_eqb : R -> R -> bool := fun x y => false.
+ Lemma default_eqb_ok : forall x y, default_eqb x y = true -> x = y.
+Proof.
+discriminate 1.
+Qed.
+
+End New2OldRing.
+
+Section New2OldSemiRing.
+ Variable R : Type.
+ Variable (rO rI : R) (radd rmul: R->R->R).
+ Variable SRth : semi_ring_theory rO rI radd rmul (eq (A:=R)).
+
+ Variable reqb : R -> R -> bool.
+ Variable reqb_ok : forall x y, reqb x y = true -> x = y.
+
+ Lemma sring_equiv2 :
+   Semi_Ring_Theory radd rmul rI rO reqb.
+Proof.
+elim SRth; intros; constructor;  eauto.
+intros.
+apply reqb_ok.
+destruct (reqb x y); trivial; intros.
+elim H.
+Qed.
+
+End New2OldSemiRing.