Library Coq.micromega.ZCoeff
Require
Import
OrderedRing
.
Require
Import
RingMicromega
.
Require
Import
ZArith_base
.
Require
Import
InitialRing
.
Require
Import
Setoid
.
Require
Import
ZArithRing
.
Import
OrderedRingSyntax
.
Set Implicit Arguments
.
Section
InitialMorphism
.
Variable
R
:
Type
.
Variables
rO
rI
:
R
.
Variables
rplus
rtimes
rminus
:
R
->
R
->
R
.
Variable
ropp
:
R
->
R
.
Variables
req
rle
rlt
:
R
->
R
->
Prop
.
Variable
sor
:
SOR
rO
rI
rplus
rtimes
rminus
ropp
req
rle
rlt
.
Notation
"
0" :=
rO
.
Notation
"
1" :=
rI
.
Notation
"
x + y" := (
rplus
x
y
).
Notation
"
x * y " := (
rtimes
x
y
).
Notation
"
x - y " := (
rminus
x
y
).
Notation
"
- x" := (
ropp
x
).
Notation
"
x == y" := (
req
x
y
).
Notation
"
x ~= y" := (
~
req
x
y
).
Notation
"
x <= y" := (
rle
x
y
).
Notation
"
x < y" := (
rlt
x
y
).
Lemma
req_refl
:
forall
x
,
req
x
x
.
Lemma
req_sym
:
forall
x
y
,
req
x
y
->
req
y
x
.
Lemma
req_trans
:
forall
x
y
z
,
req
x
y
->
req
y
z
->
req
x
z
.
Add
Relation
R
req
reflexivity
proved
by
(@
Equivalence_Reflexive
_
_
(
SORsetoid
sor
))
symmetry
proved
by
(@
Equivalence_Symmetric
_
_
(
SORsetoid
sor
))
transitivity
proved
by
(@
Equivalence_Transitive
_
_
(
SORsetoid
sor
))
as
sor_setoid
.
Add
Morphism
rplus
with
signature
req
==>
req
==>
req
as
rplus_morph
.
Add
Morphism
rtimes
with
signature
req
==>
req
==>
req
as
rtimes_morph
.
Add
Morphism
ropp
with
signature
req
==>
req
as
ropp_morph
.
Add
Morphism
rle
with
signature
req
==>
req
==>
iff
as
rle_morph
.
Add
Morphism
rlt
with
signature
req
==>
req
==>
iff
as
rlt_morph
.
Add
Morphism
rminus
with
signature
req
==>
req
==>
req
as
rminus_morph
.
Ltac
le_less
:=
rewrite
(
Rle_lt_eq
sor
);
left
;
try
assumption
.
Ltac
le_equal
:=
rewrite
(
Rle_lt_eq
sor
);
right
;
try
reflexivity
;
try
assumption
.
Definition
gen_order_phi_Z
:
Z
->
R
:=
gen_phiZ
0 1
rplus
rtimes
ropp
.
Notation
phi_pos
:= (
gen_phiPOS
1
rplus
rtimes
).
Notation
phi_pos1
:= (
gen_phiPOS1
1
rplus
rtimes
).
Notation
"
[ x ]" := (
gen_order_phi_Z
x
).
Lemma
ring_ops_wd
:
ring_eq_ext
rplus
rtimes
ropp
req
.
Lemma
Zring_morph
:
ring_morph
0 1
rplus
rtimes
rminus
ropp
req
0%
Z
1%
Z
Z.add
Z.mul
Z.sub
Z.opp
Zeq_bool
gen_order_phi_Z
.
Lemma
phi_pos1_pos
:
forall
x
:
positive
, 0
<
phi_pos1
x
.
Lemma
phi_pos1_succ
:
forall
x
:
positive
,
phi_pos1
(
Pos.succ
x
)
==
1
+
phi_pos1
x
.
Lemma
clt_pos_morph
:
forall
x
y
:
positive
, (
x
<
y
)%
positive
->
phi_pos1
x
<
phi_pos1
y
.
Lemma
clt_morph
:
forall
x
y
:
Z
, (
x
<
y
)%
Z
->
[
x
]
<
[
y
]
.
Lemma
Zcleb_morph
:
forall
x
y
:
Z
,
Z.leb
x
y
=
true
->
[
x
]
<=
[
y
]
.
Lemma
Zcneqb_morph
:
forall
x
y
:
Z
,
Zeq_bool
x
y
=
false
->
[
x
]
~=
[
y
]
.
End
InitialMorphism
.