diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /plugins/setoid_ring/Ring_equiv.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
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. |