diff options
author | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-26 11:18:22 +0000 |
---|---|---|
committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-26 11:18:22 +0000 |
commit | 351a500eada776832ac9b09657e42f5d6cd7210f (patch) | |
tree | af45a745540e1154eab8955c17e03cbbe2e6b878 /contrib/setoid_ring/Ring_equiv.v | |
parent | 5155de9ee4bd01127a57c36cebbd01c5d903d048 (diff) |
mise a jour du nouveau ring et ajout du nouveau field, avant renommages
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/setoid_ring/Ring_equiv.v')
-rw-r--r-- | contrib/setoid_ring/Ring_equiv.v | 74 |
1 files changed, 74 insertions, 0 deletions
diff --git a/contrib/setoid_ring/Ring_equiv.v b/contrib/setoid_ring/Ring_equiv.v new file mode 100644 index 000000000..135a59e01 --- /dev/null +++ b/contrib/setoid_ring/Ring_equiv.v @@ -0,0 +1,74 @@ +Require Import Ring_theory. +Require Import Coq.ring.Setoid_ring_theory. +Require Import Ring_th. + +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. |