Library Coq.Reals.ConstructiveRcomplete

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

Local Open Scope CReal_scope.

Definition absLe (a b : CReal) : Prop
  := -b <= a <= b.

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))))
    -> absLe y x.

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

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 p : positive,
    { n : nat | forall i j:nat, le n i -> le n j
                       -> absLe (un i - un j) (inject_Q (1#p)) }.

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

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

Definition RQ_limit : forall (x : CReal) (n:nat),
    { q:Q & x < inject_Q q < x + inject_Q (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
                                  -> Qle (-(1#n)) (xn p - xn q)
                                     /\ Qle (xn p - xn q) (1#n) }.

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

Lemma doubleLeCovariant : 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 => inject_Q (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:nat => inject_Q (qn n)) r }.

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

Definition CRealImplem : ConstructiveReals.