Library Coq.Reals.ConstructiveRcomplete


Require Import QArith_base.
Require Import Qabs.
Require Import ConstructiveCauchyReals.
Require Import Logic.ConstructiveEpsilon.

Local Open Scope CReal_scope.

Lemma CReal_absSmall : forall (x y : CReal) (n : positive),
    (Qlt (2 # n)
         (proj1_sig x (Pos.to_nat n) - Qabs (proj1_sig y (Pos.to_nat n))))
    -> (CRealLt (CReal_opp x) y * CRealLt y x).

Definition absSmall (a b : CReal) : Set
  := -b < a < b.

Definition Un_cv_mod (un : nat -> CReal) (l : CReal) : Set
  := forall n : positive,
    { p : nat & forall i:nat, le p i -> absSmall (un i - l) (IQR (1#n)) }.

Lemma Un_cv_mod_eq : forall (v u : nat -> CReal) (s : CReal),
    (forall n:nat, u n == v n)
    -> Un_cv_mod u s -> Un_cv_mod v s.

Definition Un_cauchy_mod (un : nat -> CReal) : Set
  := forall n : positive,
    { p : nat & forall i j:nat, le p i
                       -> le p j
                       -> -IQR (1#n) < un i - un j < IQR (1#n) }.

Fixpoint Rfloor_pos (a : CReal) (n : nat) { struct n }
  : 0 < a
    -> a < INR n
    -> { p : nat & INR p < a < INR p + 2 }.

Definition Rfloor (a : CReal)
  : { p : Z & IZR p < a < IZR p + 2 }.

Definition Rup_nat (x : CReal)
  : { n : nat & x < INR n }.

Definition FQ_dense_pos (a b : CReal)
  : 0 < b
    -> a < b -> { q : Q & a < IQR q < b }.

Definition FQ_dense (a b : CReal)
  : a < b
    -> { q : Q & a < IQR q < b }.

Definition RQ_limit : forall (x : CReal) (n:nat),
    { q:Q & x < IQR q < x + IQR (1 # Pos.of_nat n) }.

Definition Un_cauchy_Q (xn : nat -> Q) : Set
  := forall n : positive,
    { k : nat | forall p q : nat, le k p -> le k q
                                  -> Qlt (-(1#n)) (xn p - xn q)
                                     /\ Qlt (xn p - xn q) (1#n) }.

Lemma Rdiag_cauchy_sequence : forall (xn : nat -> CReal),
    Un_cauchy_mod xn
    -> Un_cauchy_Q (fun n => let (l,_) := RQ_limit (xn n) n in l).

Lemma doubleLtCovariant : forall a b c d e f : CReal,
    a == b -> c == d -> e == f
    -> (a < c < e)
    -> (b < d < f).

Lemma CReal_cv_self : forall (qn : nat -> Q) (x : CReal) (cvmod : positive -> nat),
    QSeqEquiv qn (fun n => proj1_sig x n) cvmod
    -> Un_cv_mod (fun n => IQR (qn n)) x.

Lemma Un_cv_extens : forall (xn yn : nat -> CReal) (l : CReal),
    Un_cv_mod xn l
    -> (forall n : nat, xn n == yn n)
    -> Un_cv_mod yn l.

Lemma R_has_all_rational_limits : forall qn : nat -> Q,
    Un_cauchy_Q qn
    -> { r : CReal & Un_cv_mod (fun n => IQR (qn n)) r }.

Lemma Rcauchy_complete : forall (xn : nat -> CReal),
    Un_cauchy_mod xn
    -> { l : CReal & Un_cv_mod xn l }.