# 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 }.