Library Coq.Reals.ConstructiveRealsLUB

Require Import QArith_base.
Require Import Qabs.
Require Import ConstructiveReals.
Require Import ConstructiveCauchyRealsMult.
Require Import ConstructiveRealsMorphisms.
Require Import ConstructiveRcomplete.
Require Import Logic.ConstructiveEpsilon.

Local Open Scope CReal_scope.

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 (E:CReal -> Prop) (m:CReal)
  := forall x:CReal, E x -> x <= m.

Definition is_lub (E:CReal -> Prop) (m:CReal) :=
  is_upper_bound E m /\ (forall b:CReal, is_upper_bound E b -> m <= b).

Lemma is_upper_bound_dec :
  forall (E:CReal -> Prop) (x:CReal),
    sig_forall_dec_T
    -> sig_not_dec_T
    -> { is_upper_bound E x } + { ~is_upper_bound E x }.

Lemma is_upper_bound_epsilon :
  forall (E:CReal -> Prop),
    sig_forall_dec_T
    -> sig_not_dec_T
    -> (exists x:CReal, is_upper_bound E x)
    -> { n:nat | is_upper_bound E (inject_Q (Z.of_nat n # 1)) }.

Lemma is_upper_bound_not_epsilon :
  forall E:CReal -> Prop,
    sig_forall_dec_T
    -> sig_not_dec_T
    -> (exists x : CReal, E x)
    -> { m:nat | ~is_upper_bound E (-inject_Q (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 upcut : DedekindDecCut,
    { x : CReal | forall r:Q, (x < inject_Q r -> DDupcut upcut r)
                         /\ (inject_Q r < x -> ~DDupcut upcut r) }.

Lemma is_upper_bound_glb :
  forall (E:CReal -> Prop),
    sig_not_dec_T
    -> sig_forall_dec_T
    -> (exists x : CReal, E x)
    -> (exists x : CReal, is_upper_bound E x)
    -> { x : CReal | forall r:Q, (x < inject_Q r -> is_upper_bound E (inject_Q r))
                           /\ (inject_Q r < x -> ~is_upper_bound E (inject_Q r)) }.

Lemma is_upper_bound_closed :
  forall (E:CReal -> Prop) (sig_forall_dec : sig_forall_dec_T)
    (sig_not_dec : sig_not_dec_T)
    (Einhab : exists x : CReal, E x)
    (Ebound : exists x : CReal, 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 (E:CReal -> Prop),
    sig_forall_dec_T
    -> sig_not_dec_T
    -> (exists x : CReal, E x)
    -> (exists x : CReal, is_upper_bound E x)
    -> { u : CReal | 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, orderEq _ (CRlt 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 R E x)
    -> { u : CRcarrier R | CRis_upper_bound R E u /\
                           forall y:CRcarrier R, CRis_upper_bound R E y -> CRlt R y u -> False }.