Library Coq.setoid_ring.RealField
Require
Import
Nnat
.
Require
Import
ArithRing
.
Require
Export
Ring
Field
.
Require
Import
Rdefinitions
.
Require
Import
Rpow_def
.
Require
Import
Raxioms
.
Local Open
Scope
R_scope
.
Lemma
RTheory
:
ring_theory
0 1
Rplus
Rmult
Rminus
Ropp
(
eq
(
A
:=
R
)).
Lemma
Rfield
:
field_theory
0 1
Rplus
Rmult
Rminus
Ropp
Rdiv
Rinv
(
eq
(
A
:=
R
)).
Lemma
Rlt_n_Sn
:
forall
x
,
x
<
x
+
1.
Notation
Rset
:= (
Eqsth
R
).
Notation
Rext
:= (
Eq_ext
Rplus
Rmult
Ropp
).
Lemma
Rlt_0_2
: 0
<
2.
Lemma
Rgen_phiPOS
:
forall
x
,
InitialRing.gen_phiPOS1
1
Rplus
Rmult
x
>
0.
Lemma
Rgen_phiPOS_not_0
:
forall
x
,
InitialRing.gen_phiPOS1
1
Rplus
Rmult
x
<>
0.
Lemma
Zeq_bool_complete
:
forall
x
y
,
InitialRing.gen_phiZ
0%
R
1%
R
Rplus
Rmult
Ropp
x
=
InitialRing.gen_phiZ
0%
R
1%
R
Rplus
Rmult
Ropp
y
->
Zeq_bool
x
y
=
true
.
Lemma
Rdef_pow_add
:
forall
(
x
:
R
) (
n
m
:
nat
),
pow
x
(
n
+
m
)
=
pow
x
n
*
pow
x
m
.
Lemma
R_power_theory
:
power_theory
1%
R
Rmult
(@
eq
R
)
N.to_nat
pow
.
Ltac
Rpow_tac
t
:=
match
isnatcst
t
with
|
false
=>
constr
:(
InitialRing.NotConstant
)
|
_
=>
constr
:(
N.of_nat
t
)
end
.
Ltac
IZR_tac
t
:=
match
t
with
|
R0
=>
constr
:(0%
Z
)
|
R1
=>
constr
:(1%
Z
)
|
IZR
(
Z.pow_pos
10 ?
p
) =>
match
isPcst
p
with
|
true
=>
constr
:(
Z.pow_pos
10
p
)
|
_
=>
constr
:(
InitialRing.NotConstant
)
end
|
IZR
?
u
=>
match
isZcst
u
with
|
true
=>
u
|
_
=>
constr
:(
InitialRing.NotConstant
)
end
|
_
=>
constr
:(
InitialRing.NotConstant
)
end
.
Add
Field
RField
:
Rfield
(
completeness
Zeq_bool_complete
,
constants
[
IZR_tac
],
power_tac
R_power_theory
[
Rpow_tac
]).