diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/setoid_ring/Ring_equiv.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'plugins/setoid_ring/Ring_equiv.v')
-rw-r--r-- | plugins/setoid_ring/Ring_equiv.v | 74 |
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. |