# Library Coq.Reals.Cauchy.ConstructiveRcomplete

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

Proof that Cauchy reals are Cauchy-complete.
WARNING: this file is experimental and likely to change in future releases.

Local Open Scope CReal_scope.

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

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

Lemma seq_cv_proper : forall (un : nat -> CReal) (a b : CReal),
seq_cv un a
-> a == b
-> seq_cv un b.

Instance seq_cv_morph
: forall (un : nat -> CReal), CMorphisms.Proper
(CMorphisms.respectful CRealEq CRelationClasses.iffT) (seq_cv un).

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

Lemma Qabs_Rabs : forall q : Q,
inject_Q (Qabs q) == CReal_abs (inject_Q q).

Lemma CReal_cv_self : forall (x : CReal) (n : positive),
CReal_abs (x - inject_Q (proj1_sig x n)) <= inject_Q (1#n).

Lemma Rcauchy_limit : forall (xn : nat -> CReal) (xcau : Un_cauchy_mod xn),
QCauchySeq
(fun n : positive =>
let (p, _) := xcau (4 * n)%positive in proj1_sig (xn p) (4 * n)%positive).

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

Lemma CRealLtIsLinear : isLinearOrder CRealLt.

Lemma CRealAbsLUB : forall x y : CReal,
x <= y /\ (- x) <= y <-> (CReal_abs x) <= y.

Lemma CRealComplete : forall xn : nat -> CReal,
(forall p : positive,
{n : nat |
forall i j : nat,
(n <= i)%nat -> (n <= j)%nat -> (CReal_abs (xn i + - xn j)) <= (inject_Q (1 # p))}) ->
{l : CReal &
forall p : positive,
{n : nat |
forall i : nat, (n <= i)%nat -> (CReal_abs (xn i + - l)) <= (inject_Q (1 # p))}}.

Definition CRealConstructive : ConstructiveReals
:= Build_ConstructiveReals
CReal CRealLt CRealLtIsLinear CRealLtProp
CRealLtEpsilon CRealLtForget CRealLtDisjunctEpsilon
inject_Q inject_Q_lt lt_inject_Q
CReal_plus CReal_opp CReal_mult
inject_Q_plus inject_Q_mult
CReal_isRing CReal_isRingExt CRealLt_0_1
CReal_plus_lt_compat_l CReal_plus_lt_reg_l
CReal_mult_lt_0_compat
CReal_inv CReal_inv_l CReal_inv_0_lt_compat
CRealQ_dense Rup_pos CReal_abs CRealAbsLUB CRealComplete.