1
Require Import Setoid_ring_theory.
2
Require Import LegacyRing_theory.
3
Require Import Ring_theory.
5
Set Implicit Arguments.
11
Variable Aplus : A -> A -> A.
12
Variable Amult : A -> A -> A.
15
Variable Aopp : A -> A.
16
Variable Aeq : A -> A -> bool.
17
Variable R : Ring_Theory Aplus Amult Aone Azero Aopp Aeq.
19
Let Aminus := fun x y => Aplus x (Aopp y).
22
ring_theory Azero Aone Aplus Amult Aminus Aopp (eq (A:=A)).
32
Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
33
Variable Rth : ring_theory rO rI radd rmul rsub ropp (eq (A:=R)).
35
Variable reqb : R -> R -> bool.
36
Variable reqb_ok : forall x y, reqb x y = true -> x = y.
39
Ring_Theory radd rmul rI rO ropp reqb.
41
elim Rth; intros; constructor; eauto.
44
destruct (reqb x y); trivial; intros.
48
Definition default_eqb : R -> R -> bool := fun x y => false.
49
Lemma default_eqb_ok : forall x y, default_eqb x y = true -> x = y.
56
Section New2OldSemiRing.
58
Variable (rO rI : R) (radd rmul: R->R->R).
59
Variable SRth : semi_ring_theory rO rI radd rmul (eq (A:=R)).
61
Variable reqb : R -> R -> bool.
62
Variable reqb_ok : forall x y, reqb x y = true -> x = y.
65
Semi_Ring_Theory radd rmul rI rO reqb.
67
elim SRth; intros; constructor; eauto.
70
destruct (reqb x y); trivial; intros.