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