Library Stdlib.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 }.