Library Stdlib.Reals.Cauchy.ConstructiveRcomplete

Require Import QArith_base.
Require Import Qabs.
Require Import ConstructiveReals.
Require Import ConstructiveCauchyRealsMult.
Require Import Logic.ConstructiveEpsilon.
Require Import ConstructiveCauchyAbs.
Require Import Lia.
Require Import Lqa.
Require Import Qpower.
Require Import QExtra.
Require Import PosExtra.
Require Import ConstructiveExtra.

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.

#[global]
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 }.

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

Lemma Qlt_trans_swap_hyp: forall x y z : Q,
  (y < z)%Q -> (x < y)%Q -> (x < z)%Q.

Lemma Qle_trans_swap_hyp: forall x y z : Q,
  (y <= z)%Q -> (x <= y)%Q -> (x <= z)%Q.

Lemma Qpower_2powneg_le_inv: forall (n : positive),
    (2 * 2 ^ Z.neg n <= 1 # n)%Q.

Lemma Pospow_lin_le_2pow: forall (n : positive),
    (2 * n <= 2 ^ n)%positive.

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

Lemma CReal_cv_self' : forall (x : CReal) (n : Z),
    CReal_abs (x - inject_Q (seq x n)) <= inject_Q (2^n).

Definition QCauchySeqLin (un : positive -> Q)
  : Prop
  := forall (k : positive) (p q : positive),
      Pos.le k p
      -> Pos.le k q
      -> Qlt (Qabs (un p - un q)) (1 # k).

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

Definition CReal_from_cauchy_cm (n : Z) : positive :=
  match n with
    | Z0
    | Zpos _ => 1%positive
    | Zneg p => p
    end.

Lemma CReal_from_cauchy_cm_mono : forall (n p : Z),
    (p <= n)%Z
 -> (CReal_from_cauchy_cm n <= CReal_from_cauchy_cm p)%positive.

Definition CReal_from_cauchy_seq (xn : nat -> CReal) (xcau : Un_cauchy_mod xn) (n : Z) : Q :=
  let p := CReal_from_cauchy_cm n in
  let (q, _) := xcau (4 * 2^p)%positive in
  seq (xn q) (Z.neg p - 2)%Z.

Lemma CReal_from_cauchy_cauchy : forall (xn : nat -> CReal) (xcau : Un_cauchy_mod xn),
    QCauchySeq (CReal_from_cauchy_seq xn xcau).

Lemma Rup_pos (x : CReal)
  : { n : positive & x < inject_Q (Z.pos n # 1) }.

Lemma CReal_abs_upper_bound (x : CReal)
  : { n : positive & CReal_abs x < inject_Q (Z.pos n # 1) }.

Require Import Qminmax.

Lemma CRealLt_QR_from_single_dist : forall (q : Q) (r : CReal) (n :Z),
    (2^n < seq r n - q)%Q
 -> inject_Q q < r .

Lemma CReal_abs_Qabs: forall (x : CReal) (q : Q) (n : Z),
    CReal_abs x <= inject_Q q
 -> (Qabs (seq x n) <= q + 2^n)%Q.

Lemma CReal_abs_Qabs_seq: forall (x : CReal) (n : Z),
    (seq (CReal_abs x) n == Qabs (seq x n))%Q.

Lemma CReal_abs_Qabs_diff: forall (x y : CReal) (q : Q) (n : Z),
    CReal_abs (x - y) <= inject_Q q
 -> (Qabs (seq x n - seq y n) <= q + 2*2^n)%Q.

Lemma CRealLt_QR_to_single_dist : forall (q : Q) (x : CReal) (n : Z),
    inject_Q q < x -> (-(2^n) <= seq x n - q)%Q.

Lemma CRealLt_RQ_to_single_dist : forall (x : CReal) (q : Q) (n : Z),
    x < inject_Q q -> (-(2^n) <= q - seq x n)%Q.

Lemma Pos2Z_pos_is_pos : forall (p : positive),
    (1 <= Z.pos p)%Z.

Lemma Qabs_Qgt_condition: forall x y : Q,
  (x < Qabs y)%Q <-> (x < y \/ x < -y)%Q.

Lemma CReal_from_cauchy_seq_bound :
  forall (xn : nat -> CReal) (xcau : Un_cauchy_mod xn) (i j : Z),
    (Qabs (CReal_from_cauchy_seq xn xcau i - CReal_from_cauchy_seq xn xcau j) <= 1)%Q.

Definition CReal_from_cauchy_scale (xn : nat -> CReal) (xcau : Un_cauchy_mod xn) : Z :=
  Qbound_lt_ZExp2 (Qabs (CReal_from_cauchy_seq xn xcau (-1)) + 2)%Q.

Lemma CReal_from_cauchy_bound : forall (xn : nat -> CReal) (xcau : Un_cauchy_mod xn),
  QBound (CReal_from_cauchy_seq xn xcau) (CReal_from_cauchy_scale xn xcau).

Definition CReal_from_cauchy (xn : nat -> CReal) (xcau : Un_cauchy_mod xn) : CReal :=
{|
  seq := CReal_from_cauchy_seq xn xcau;
  scale := CReal_from_cauchy_scale xn xcau;
  cauchy := CReal_from_cauchy_cauchy xn xcau;
  bound := CReal_from_cauchy_bound xn xcau
|}.

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

Lemma Qnot_le_iff_lt: forall x y : Q,
  ~ (x <= y)%Q <-> (y < x)%Q.

Lemma Qnot_lt_iff_le: forall x y : Q,
  ~ (x < y)%Q <-> (y <= x)%Q.

Lemma CRealLtDisjunctEpsilon : forall a b c d : CReal,
    (CRealLtProp a b \/ CRealLtProp c d) -> CRealLt a b + CRealLt c d.

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.