Library Coq.Reals.Cauchy.ConstructiveRcomplete
Require
Import
QArith_base
.
Require
Import
Qabs
.
Require
Import
ConstructiveReals
.
Require
Import
ConstructiveCauchyRealsMult
.
Require
Import
Logic.ConstructiveEpsilon
.
Require
Import
ConstructiveCauchyAbs
.
Proof that Cauchy reals are Cauchy-complete.
WARNING: this file is experimental and likely to change in future releases.
Local Open
Scope
CReal_scope
.
Definition
seq_cv
(
un
:
nat
->
CReal
) (
l
:
CReal
) :
Set
:=
forall
p
:
positive
,
{
n
:
nat
|
forall
i
:
nat
,
le
n
i
->
CReal_abs
(
un
i
-
l
)
<=
inject_Q
(1
#
p
)
}
.
Definition
Un_cauchy_mod
(
un
:
nat
->
CReal
) :
Set
:=
forall
p
:
positive
,
{
n
:
nat
|
forall
i
j
:
nat
,
le
n
i
->
le
n
j
->
CReal_abs
(
un
i
-
un
j
)
<=
inject_Q
(1
#
p
)
}
.
Lemma
seq_cv_proper
:
forall
(
un
:
nat
->
CReal
) (
a
b
:
CReal
),
seq_cv
un
a
->
a
==
b
->
seq_cv
un
b
.
Instance
seq_cv_morph
:
forall
(
un
:
nat
->
CReal
),
CMorphisms.Proper
(
CMorphisms.respectful
CRealEq
CRelationClasses.iffT
) (
seq_cv
un
).
Definition
Rfloor
(
a
:
CReal
)
:
{
p
:
Z
&
inject_Q
(
p
#
1)
<
a
<
inject_Q
(
p
#
1)
+
2
}
.
Definition
FQ_dense
(
a
b
:
CReal
)
:
a
<
b
->
{
q
:
Q
&
a
<
inject_Q
q
<
b
}
.
Lemma
Qabs_Rabs
:
forall
q
:
Q
,
inject_Q
(
Qabs
q
)
==
CReal_abs
(
inject_Q
q
).
Lemma
CReal_cv_self
:
forall
(
x
:
CReal
) (
n
:
positive
),
CReal_abs
(
x
-
inject_Q
(
proj1_sig
x
n
))
<=
inject_Q
(1
#
n
).
Lemma
Rcauchy_limit
:
forall
(
xn
:
nat
->
CReal
) (
xcau
:
Un_cauchy_mod
xn
),
QCauchySeq
(
fun
n
:
positive
=>
let
(
p
,
_
) :=
xcau
(4
*
n
)%
positive
in
proj1_sig
(
xn
p
) (4
*
n
)%
positive
).
Lemma
Rcauchy_complete
:
forall
(
xn
:
nat
->
CReal
),
Un_cauchy_mod
xn
->
{
l
:
CReal
&
seq_cv
xn
l
}
.
Lemma
CRealLtIsLinear
:
isLinearOrder
CRealLt
.
Lemma
CRealAbsLUB
:
forall
x
y
:
CReal
,
x
<=
y
/\
(
-
x
)
<=
y
<->
(
CReal_abs
x
)
<=
y
.
Lemma
CRealComplete
:
forall
xn
:
nat
->
CReal
,
(
forall
p
:
positive
,
{
n
:
nat
|
forall
i
j
:
nat
,
(
n
<=
i
)%
nat
->
(
n
<=
j
)%
nat
->
(
CReal_abs
(
xn
i
+
-
xn
j
)
)
<=
(
inject_Q
(1
#
p
)
)
}
)
->
{
l
:
CReal
&
forall
p
:
positive
,
{
n
:
nat
|
forall
i
:
nat
, (
n
<=
i
)%
nat
->
(
CReal_abs
(
xn
i
+
-
l
)
)
<=
(
inject_Q
(1
#
p
)
)
}
}
.
Definition
CRealConstructive
:
ConstructiveReals
:=
Build_ConstructiveReals
CReal
CRealLt
CRealLtIsLinear
CRealLtProp
CRealLtEpsilon
CRealLtForget
CRealLtDisjunctEpsilon
inject_Q
inject_Q_lt
lt_inject_Q
CReal_plus
CReal_opp
CReal_mult
inject_Q_plus
inject_Q_mult
CReal_isRing
CReal_isRingExt
CRealLt_0_1
CReal_plus_lt_compat_l
CReal_plus_lt_reg_l
CReal_mult_lt_0_compat
CReal_inv
CReal_inv_l
CReal_inv_0_lt_compat
CRealQ_dense
Rup_pos
CReal_abs
CRealAbsLUB
CRealComplete
.