diff options
Diffstat (limited to 'plugins/setoid_ring/Ring_equiv.v')
-rw-r--r-- | plugins/setoid_ring/Ring_equiv.v | 74 |
1 files changed, 0 insertions, 74 deletions
diff --git a/plugins/setoid_ring/Ring_equiv.v b/plugins/setoid_ring/Ring_equiv.v deleted file mode 100644 index 945f6c68..00000000 --- a/plugins/setoid_ring/Ring_equiv.v +++ /dev/null @@ -1,74 +0,0 @@ -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. |