Library Coq.setoid_ring.Ring_equiv
Require
Import
Setoid_ring_theory
.
Require
Import
LegacyRing_theory
.
Require
Import
Ring_theory
.
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
)).
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
.
Definition
default_eqb
:
R
->
R
->
bool
:=
fun
x
y
=>
false
.
Lemma
default_eqb_ok
:
forall
x
y
,
default_eqb
x
y
=
true
->
x
=
y
.
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
.
End
New2OldSemiRing
.