Library Coq.Reals.Rdefinitions
Require
Export
ZArith_base
.
Require
Import
QArith_base
.
Require
Import
ConstructiveCauchyReals
.
Require
Import
ConstructiveCauchyRealsMult
.
Require
Import
ClassicalDedekindReals
.
Delimit
Scope
R_scope
with
R
.
Local Open
Scope
R_scope
.
Module
Type
RbaseSymbolsSig
.
Parameter
R
:
Set
.
Axiom
Rabst
:
CReal
->
R
.
Axiom
Rrepr
:
R
->
CReal
.
Axiom
Rquot1
:
forall
x
y
:
R
,
CRealEq
(
Rrepr
x
) (
Rrepr
y
)
->
x
=
y
.
Axiom
Rquot2
:
forall
x
:
CReal
,
CRealEq
(
Rrepr
(
Rabst
x
))
x
.
Parameter
R0
:
R
.
Parameter
R1
:
R
.
Parameter
Rplus
:
R
->
R
->
R
.
Parameter
Rmult
:
R
->
R
->
R
.
Parameter
Ropp
:
R
->
R
.
Parameter
Rlt
:
R
->
R
->
Prop
.
Parameter
R0_def
:
R0
=
Rabst
(
inject_Q
0).
Parameter
R1_def
:
R1
=
Rabst
(
inject_Q
1).
Parameter
Rplus_def
:
forall
x
y
:
R
,
Rplus
x
y
=
Rabst
(
CReal_plus
(
Rrepr
x
) (
Rrepr
y
)).
Parameter
Rmult_def
:
forall
x
y
:
R
,
Rmult
x
y
=
Rabst
(
CReal_mult
(
Rrepr
x
) (
Rrepr
y
)).
Parameter
Ropp_def
:
forall
x
:
R
,
Ropp
x
=
Rabst
(
CReal_opp
(
Rrepr
x
)).
Parameter
Rlt_def
:
forall
x
y
:
R
,
Rlt
x
y
=
CRealLtProp
(
Rrepr
x
) (
Rrepr
y
).
End
RbaseSymbolsSig
.
Module
RbaseSymbolsImpl
:
RbaseSymbolsSig
.
Definition
R
:=
DReal
.
Definition
Rabst
:=
DRealAbstr
.
Definition
Rrepr
:=
DRealRepr
.
Definition
Rquot1
:=
DRealQuot1
.
Definition
Rquot2
:=
DRealQuot2
.
Definition
R0
:
R
:=
Rabst
(
inject_Q
0).
Definition
R1
:
R
:=
Rabst
(
inject_Q
1).
Definition
Rplus
:
R
->
R
->
R
:=
fun
x
y
:
R
=>
Rabst
(
CReal_plus
(
Rrepr
x
) (
Rrepr
y
)).
Definition
Rmult
:
R
->
R
->
R
:=
fun
x
y
:
R
=>
Rabst
(
CReal_mult
(
Rrepr
x
) (
Rrepr
y
)).
Definition
Ropp
:
R
->
R
:=
fun
x
:
R
=>
Rabst
(
CReal_opp
(
Rrepr
x
)).
Definition
Rlt
:
R
->
R
->
Prop
:=
fun
x
y
:
R
=>
CRealLtProp
(
Rrepr
x
) (
Rrepr
y
).
Definition
R0_def
:=
eq_refl
R0
.
Definition
R1_def
:=
eq_refl
R1
.
Definition
Rplus_def
:=
fun
x
y
=>
eq_refl
(
Rplus
x
y
).
Definition
Rmult_def
:=
fun
x
y
=>
eq_refl
(
Rmult
x
y
).
Definition
Ropp_def
:=
fun
x
=>
eq_refl
(
Ropp
x
).
Definition
Rlt_def
:=
fun
x
y
=>
eq_refl
(
Rlt
x
y
).
End
RbaseSymbolsImpl
.
Export
RbaseSymbolsImpl
.
Notation
R
:=
RbaseSymbolsImpl.R
(
only
parsing
).
Notation
R0
:=
RbaseSymbolsImpl.R0
(
only
parsing
).
Notation
R1
:=
RbaseSymbolsImpl.R1
(
only
parsing
).
Notation
Rplus
:=
RbaseSymbolsImpl.Rplus
(
only
parsing
).
Notation
Rmult
:=
RbaseSymbolsImpl.Rmult
(
only
parsing
).
Notation
Ropp
:=
RbaseSymbolsImpl.Ropp
(
only
parsing
).
Notation
Rlt
:=
RbaseSymbolsImpl.Rlt
(
only
parsing
).
Infix
"
+" :=
Rplus
:
R_scope
.
Infix
"
*" :=
Rmult
:
R_scope
.
Notation
"
- x" := (
Ropp
x
) :
R_scope
.
Infix
"
<" :=
Rlt
:
R_scope
.
Definition
Rgt
(
r1
r2
:
R
) :
Prop
:=
r2
<
r1
.
Definition
Rle
(
r1
r2
:
R
) :
Prop
:=
r1
<
r2
\/
r1
=
r2
.
Definition
Rge
(
r1
r2
:
R
) :
Prop
:=
Rgt
r1
r2
\/
r1
=
r2
.
Definition
Rminus
(
r1
r2
:
R
) :
R
:=
r1
+
-
r2
.
Infix
"
-" :=
Rminus
:
R_scope
.
Infix
"
<=" :=
Rle
:
R_scope
.
Infix
"
>=" :=
Rge
:
R_scope
.
Infix
"
>" :=
Rgt
:
R_scope
.
Notation
"
x <= y <= z" := (
x
<=
y
/\
y
<=
z
) :
R_scope
.
Notation
"
x <= y < z" := (
x
<=
y
/\
y
<
z
) :
R_scope
.
Notation
"
x < y < z" := (
x
<
y
/\
y
<
z
) :
R_scope
.
Notation
"
x < y <= z" := (
x
<
y
/\
y
<=
z
) :
R_scope
.
Injection from
Z
to
R
Fixpoint
IPR_2
(
p
:
positive
) :
R
:=
match
p
with
|
xH
=>
R1
+
R1
|
xO
p
=>
(
R1
+
R1
)
*
IPR_2
p
|
xI
p
=>
(
R1
+
R1
)
*
(
R1
+
IPR_2
p
)
end
.
Definition
IPR
(
p
:
positive
) :
R
:=
match
p
with
|
xH
=>
R1
|
xO
p
=>
IPR_2
p
|
xI
p
=>
R1
+
IPR_2
p
end
.
Definition
IZR
(
z
:
Z
) :
R
:=
match
z
with
|
Z0
=>
R0
|
Zpos
n
=>
IPR
n
|
Zneg
n
=>
-
IPR
n
end
.
Lemma
total_order_T
:
forall
r1
r2
:
R
,
{
Rlt
r1
r2
}
+
{
r1
=
r2
}
+
{
Rlt
r2
r1
}
.
Lemma
Req_appart_dec
:
forall
x
y
:
R
,
{
x
=
y
}
+
{
x
<
y
\/
y
<
x
}
.
Lemma
Rrepr_appart_0
:
forall
x
:
R
,
(
x
<
R0
\/
R0
<
x
)
->
CReal_appart
(
Rrepr
x
) (
inject_Q
0).
Module
Type
RinvSig
.
Parameter
Rinv
:
R
->
R
.
Parameter
Rinv_def
:
forall
x
:
R
,
Rinv
x
=
match
Req_appart_dec
x
R0
with
|
left
_
=>
R0
|
right
r
=>
Rabst
((
CReal_inv
(
Rrepr
x
) (
Rrepr_appart_0
x
r
)))
end
.
End
RinvSig
.
Module
RinvImpl
:
RinvSig
.
Definition
Rinv
:
R
->
R
:=
fun
x
=>
match
Req_appart_dec
x
R0
with
|
left
_
=>
R0
|
right
r
=>
Rabst
((
CReal_inv
(
Rrepr
x
) (
Rrepr_appart_0
x
r
)))
end
.
Definition
Rinv_def
:=
fun
x
=>
eq_refl
(
Rinv
x
).
End
RinvImpl
.
Notation
Rinv
:=
RinvImpl.Rinv
(
only
parsing
).
Notation
"
/ x" := (
Rinv
x
) :
R_scope
.
Definition
Rdiv
(
r1
r2
:
R
) :
R
:=
r1
*
/
r2
.
Infix
"
/" :=
Rdiv
:
R_scope
.
Definition
up
(
x
:
R
) :
Z
.