Library Coq.Reals.Abstract.ConstructiveLUB
Proof that LPO and the excluded middle for negations imply the existence of least upper bounds for all non-empty and bounded subsets of the real numbers.
WARNING: this file is experimental and likely to change in future releases.
Require
Import
QArith_base
Qabs
.
Require
Import
ConstructiveReals
.
Require
Import
ConstructiveAbs
.
Require
Import
ConstructiveLimits
.
Require
Import
Logic.ConstructiveEpsilon
.
Local Open
Scope
ConstructiveReals
.
Definition
sig_forall_dec_T
:
Type
:=
forall
(
P
:
nat
->
Prop
),
(
forall
n
,
{
P
n
}
+
{
~
P
n
}
)
->
{
n
|
~
P
n
}
+
{
forall
n
,
P
n
}
.
Definition
sig_not_dec_T
:
Type
:=
forall
P
:
Prop
,
{
~~
P
}
+
{
~
P
}
.
Definition
is_upper_bound
{
R
:
ConstructiveReals
}
(
E
:
CRcarrier
R
->
Prop
) (
m
:
CRcarrier
R
)
:=
forall
x
:
CRcarrier
R
,
E
x
->
x
<=
m
.
Definition
is_lub
{
R
:
ConstructiveReals
}
(
E
:
CRcarrier
R
->
Prop
) (
m
:
CRcarrier
R
) :=
is_upper_bound
E
m
/\
(
forall
b
:
CRcarrier
R
,
is_upper_bound
E
b
->
m
<=
b
)
.
Lemma
CRlt_lpo_dec
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
(
forall
(
P
:
nat
->
Prop
),
(
forall
n
,
{
P
n
}
+
{
~
P
n
}
)
->
{
n
|
~
P
n
}
+
{
forall
n
,
P
n
}
)
->
sum
(
x
<
y
) (
y
<=
x
).
Lemma
is_upper_bound_dec
:
forall
{
R
:
ConstructiveReals
} (
E
:
CRcarrier
R
->
Prop
) (
x
:
CRcarrier
R
),
sig_forall_dec_T
->
sig_not_dec_T
->
{
is_upper_bound
E
x
}
+
{
~
is_upper_bound
E
x
}
.
Lemma
is_upper_bound_epsilon
:
forall
{
R
:
ConstructiveReals
} (
E
:
CRcarrier
R
->
Prop
),
sig_forall_dec_T
->
sig_not_dec_T
->
(
exists
x
:
CRcarrier
R
,
is_upper_bound
E
x
)
->
{
n
:
nat
|
is_upper_bound
E
(
CR_of_Q
R
(
Z.of_nat
n
#
1))
}
.
Lemma
is_upper_bound_not_epsilon
:
forall
{
R
:
ConstructiveReals
} (
E
:
CRcarrier
R
->
Prop
),
sig_forall_dec_T
->
sig_not_dec_T
->
(
exists
x
:
CRcarrier
R
,
E
x
)
->
{
m
:
nat
|
~
is_upper_bound
E
(
-
CR_of_Q
R
(
Z.of_nat
m
#
1))
}
.
Record
DedekindDecCut
:
Type
:=
{
DDupcut
:
Q
->
Prop
;
DDproper
:
forall
q
r
:
Q
, (
q
==
r
->
DDupcut
q
->
DDupcut
r
)%
Q
;
DDlow
:
Q
;
DDhigh
:
Q
;
DDdec
:
forall
q
:
Q
,
{
DDupcut
q
}
+
{
~
DDupcut
q
}
;
DDinterval
:
forall
q
r
:
Q
,
Qle
q
r
->
DDupcut
q
->
DDupcut
r
;
DDhighProp
:
DDupcut
DDhigh
;
DDlowProp
:
~
DDupcut
DDlow
;
}.
Lemma
DDlow_below_up
:
forall
(
upcut
:
DedekindDecCut
) (
a
b
:
Q
),
DDupcut
upcut
a
->
~
DDupcut
upcut
b
->
Qlt
b
a
.
Fixpoint
DDcut_limit_fix
(
upcut
:
DedekindDecCut
) (
r
:
Q
) (
n
:
nat
) :
Qlt
0
r
->
(
DDupcut
upcut
(
DDlow
upcut
+
(
Z.of_nat
n
#
1
)
*
r
)
)
->
{
q
:
Q
|
DDupcut
upcut
q
/\
~
DDupcut
upcut
(
q
-
r
)
}
.
Lemma
DDcut_limit
:
forall
(
upcut
:
DedekindDecCut
) (
r
:
Q
),
Qlt
0
r
->
{
q
:
Q
|
DDupcut
upcut
q
/\
~
DDupcut
upcut
(
q
-
r
)
}
.
Lemma
glb_dec_Q
:
forall
{
R
:
ConstructiveReals
} (
upcut
:
DedekindDecCut
),
{
x
:
CRcarrier
R
|
forall
r
:
Q
,
(
x
<
CR_of_Q
R
r
->
DDupcut
upcut
r
)
/\
(
CR_of_Q
R
r
<
x
->
~
DDupcut
upcut
r
)
}
.
Lemma
is_upper_bound_glb
:
forall
{
R
:
ConstructiveReals
} (
E
:
CRcarrier
R
->
Prop
),
sig_not_dec_T
->
sig_forall_dec_T
->
(
exists
x
:
CRcarrier
R
,
E
x
)
->
(
exists
x
:
CRcarrier
R
,
is_upper_bound
E
x
)
->
{
x
:
CRcarrier
R
|
forall
r
:
Q
,
(
x
<
CR_of_Q
R
r
->
is_upper_bound
E
(
CR_of_Q
R
r
)
)
/\
(
CR_of_Q
R
r
<
x
->
~
is_upper_bound
E
(
CR_of_Q
R
r
)
)
}
.
Lemma
is_upper_bound_closed
:
forall
{
R
:
ConstructiveReals
}
(
E
:
CRcarrier
R
->
Prop
) (
sig_forall_dec
:
sig_forall_dec_T
)
(
sig_not_dec
:
sig_not_dec_T
)
(
Einhab
:
exists
x
:
CRcarrier
R
,
E
x
)
(
Ebound
:
exists
x
:
CRcarrier
R
,
is_upper_bound
E
x
),
is_lub
E
(
proj1_sig
(
is_upper_bound_glb
E
sig_not_dec
sig_forall_dec
Einhab
Ebound
)).
Lemma
sig_lub
:
forall
{
R
:
ConstructiveReals
} (
E
:
CRcarrier
R
->
Prop
),
sig_forall_dec_T
->
sig_not_dec_T
->
(
exists
x
:
CRcarrier
R
,
E
x
)
->
(
exists
x
:
CRcarrier
R
,
is_upper_bound
E
x
)
->
{
u
:
CRcarrier
R
|
is_lub
E
u
}
.
Definition
CRis_upper_bound
{
R
:
ConstructiveReals
} (
E
:
CRcarrier
R
->
Prop
) (
m
:
CRcarrier
R
)
:=
forall
x
:
CRcarrier
R
,
E
x
->
CRlt
R
m
x
->
False
.
Lemma
CR_sig_lub
:
forall
{
R
:
ConstructiveReals
} (
E
:
CRcarrier
R
->
Prop
),
(
forall
x
y
:
CRcarrier
R
,
CReq
R
x
y
->
(
E
x
<->
E
y
))
->
sig_forall_dec_T
->
sig_not_dec_T
->
(
exists
x
:
CRcarrier
R
,
E
x
)
->
(
exists
x
:
CRcarrier
R
,
CRis_upper_bound
E
x
)
->
{
u
:
CRcarrier
R
|
CRis_upper_bound
E
u
/\
forall
y
:
CRcarrier
R
,
CRis_upper_bound
E
y
->
CRlt
R
y
u
->
False
}
.