Library Coq.Reals.Cauchy.ConstructiveCauchyReals

Require Import QArith.
Require Import Qpower.
Require Import Qabs.
Require Import Qround.
Require Import Logic.ConstructiveEpsilon.
Require CMorphisms.
Require Import Lia.
Require Import Lqa.
Require Import QExtra.
Require Import ConstructiveExtra.

The constructive Cauchy real numbers, ie the Cauchy sequences of rational numbers.

Cauchy reals are Cauchy sequences of rational numbers, equipped with explicit moduli of convergence and an equivalence relation (the difference converges to zero).

Without convergence moduli, we would fail to prove that a Cauchy sequence of constructive reals converges.

Because of the Specker sequences (increasing, computable and bounded sequences of rationals that do not converge to a computable real number), constructive reals do not follow the least upper bound principle.

The double quantification on p q is needed to avoid forall un, QSeqEquiv un (fun _ => un O) (fun q => O) which says nothing about the limit of un.

We define sequences as Z -> Q instead of nat -> Q, so that we can compute arguments like 2^n fast.

Todo: doc for Z->Q

WARNING: this module is not meant to be imported directly, please import `Reals.Abstract.ConstructiveReals` instead.

WARNING: this file is experimental and likely to change in future releases.

Definition QCauchySeq (xn : Z -> Q)
  : Prop
  := forall (k : Z) (p q : Z),
      Z.le p k
   -> Z.le q k
   -> Qabs (xn p - xn q) < 2 ^ k.

Definition QBound (xn : Z -> Q) (scale : Z)
  : Prop
  := forall (k : Z),
      Qabs (xn k) < 2 ^ scale.

Record CReal := mkCReal {
  seq : Z -> Q;
  scale : Z;
  cauchy : QCauchySeq seq;
  bound : QBound seq scale
}.

Declare Scope CReal_scope.

Delimit Scope CReal_scope with CReal.

Bind Scope CReal_scope with CReal.

Local Open Scope CReal_scope.

Definition CRealLt (x y : CReal) : Set
  := { n : Z | Qlt (2 * 2 ^ n) (seq y n - seq x n) }.

Definition CRealLtProp (x y : CReal) : Prop
  := exists n : Z , Qlt (2 * 2 ^ n)(seq y n - seq x n).

Definition CRealGt (x y : CReal) := CRealLt y x.
Definition CReal_appart (x y : CReal) := sum (CRealLt x y) (CRealLt y x).

Infix "<" := CRealLt : CReal_scope.
Infix ">" := CRealGt : CReal_scope.
Infix "#" := CReal_appart : CReal_scope.

Lemma CRealLtEpsilon : forall x y : CReal,
    CRealLtProp x y -> x < y.

Lemma CRealLtForget : forall x y : CReal,
    x < y -> CRealLtProp x y.

Lemma CRealLt_lpo_dec : forall x y : CReal,
    (forall (P : nat -> Prop), (forall n:nat, {P n } + {~P n })
                    -> {n | ~P n } + {forall n, P n })
    -> CRealLt x y + (CRealLt x y -> False ).

Definition CRealLe (x y : CReal) : Prop
  := CRealLt y x -> False.

Definition CRealGe (x y : CReal) := CRealLe y x.

Infix "<=" := CRealLe : CReal_scope.
Infix ">=" := CRealGe : CReal_scope.

Notation "x <= y <= z" := (x <= y /\ y <= z) : CReal_scope.
Notation "x <= y < z" := (prod (x <= y) (y < z)) : CReal_scope.
Notation "x < y < z" := (prod (x < y) (y < z)) : CReal_scope.
Notation "x < y <= z" := (prod (x < y) (y <= z)) : CReal_scope.

Definition CRealEq (x y : CReal) : Prop
  := (CRealLe y x ) /\ (CRealLe x y ).

Infix "==" := CRealEq : CReal_scope.

Lemma CRealLe_not_lt : forall x y : CReal,
    (forall n : Z, (seq x n - seq y n <= 2 * 2 ^ n)%Q)
    <-> x <= y.

Lemma CRealEq_diff : forall (x y : CReal),
    CRealEq x y
    <-> forall n:Z, ((Qabs (seq x n - seq y n)) <= (2 * 2 ^ n ))%Q.

If the elements x(n) and y(n) of two Cauchy sequences x and are apart by at least 2*eps(n), we can find a k such that all further elements of the sequences are apart by at least 2*eps(k)

Lemma CRealLt_aboveSig : forall (x y : CReal) (n : Z),
    (2 * 2^n < seq y n - seq x n)%Q
-> let (k, _) := QarchimedeanExp2_Z (/(seq y n - seq x n - (2 * 2 ^ n)%Q))
    in forall p:Z,
        (p <= n)%Z
     -> (2^(-k ) < seq y p - seq x p)%Q.

This is a weakened form of CRealLt_aboveSig which a special shape of eps needed below

Lemma CRealLt_aboveSig' : forall (x y : CReal) (n : Z),
    (2 * 2^n < seq y n - seq x n)%Q
-> let (k, _) := QarchimedeanExp2_Z (/(seq y n - seq x n - (2 * 2 ^ n)%Q))
    in forall p:Z,
        (p <= n)%Z
     -> (2 * 2^(Z.min (-k -1) n ) < seq y p - seq x p)%Q.

Lemma CRealLt_above : forall (x y : CReal),
    CRealLt x y
    -> { n : Z | forall p : Z,
          (p <= n)%Z -> (2 * 2 ^ n < seq y p - seq x p)%Q }.

Lemma CRealLt_above_same : forall (x y : CReal) (n : Z),
    (2 * 2 ^ n < seq y n - seq x n)%Q
-> forall p:Z, (p <= n)%Z -> Qlt (seq x p) (seq y p).

Lemma CRealLt_asym : forall x y : CReal, x < y -> x <= y.

Lemma CRealLt_irrefl : forall x:CReal, x < x -> False.

Lemma CRealLe_refl : forall x : CReal, x <= x.

Lemma CRealEq_refl : forall x : CReal, x == x.

Lemma CRealEq_sym : forall x y : CReal, CRealEq x y -> CRealEq y x.

Lemma CRealLt_dec : forall x y z : CReal,
    x < y -> sum (x < z) (z < y).

Definition linear_order_T x y z := CRealLt_dec x z y.

Lemma CReal_le_lt_trans : forall x y z : CReal,
    x <= y -> y < z -> x < z.

Lemma CReal_lt_le_trans : forall x y z : CReal,
    x < y -> y <= z -> x < z.

Lemma CReal_le_trans : forall x y z : CReal,
    x <= y -> y <= z -> x <= z.

Lemma CReal_lt_trans : forall x y z : CReal,
    x < y -> y < z -> x < z.

Lemma CRealEq_trans : forall x y z : CReal,
    CRealEq x y -> CRealEq y z -> CRealEq x z.

Add Parametric Relation : CReal CRealEq
    reflexivity proved by CRealEq_refl
    symmetry proved by CRealEq_sym
    transitivity proved by CRealEq_trans
      as CRealEq_rel.

#[global]
Instance CRealEq_relT : CRelationClasses.Equivalence CRealEq.

#[global]
Instance CRealLt_morph
  : CMorphisms.Proper
      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CRealLt.

#[global]
Instance CRealGt_morph
  : CMorphisms.Proper
      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CRealGt.

#[global]
Instance CReal_appart_morph
  : CMorphisms.Proper
      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CReal_appart.

Add Parametric Morphism : CRealLtProp
    with signature CRealEq ==> CRealEq ==> iff
      as CRealLtProp_morph.

Add Parametric Morphism : CRealLe
    with signature CRealEq ==> CRealEq ==> iff
      as CRealLe_morph.

Add Parametric Morphism : CRealGe
    with signature CRealEq ==> CRealEq ==> iff
      as CRealGe_morph.

Lemma CRealLt_proper_l : forall x y z : CReal,
    CRealEq x y
    -> CRealLt x z -> CRealLt y z.

Lemma CRealLt_proper_r : forall x y z : CReal,
    CRealEq x y
    -> CRealLt z x -> CRealLt z y.

Lemma CRealLe_proper_l : forall x y z : CReal,
    CRealEq x y
    -> CRealLe x z -> CRealLe y z.

Lemma CRealLe_proper_r : forall x y z : CReal,
    CRealEq x y
    -> CRealLe z x -> CRealLe z y.

Lemma inject_Q_cauchy : forall q : Q, QCauchySeq (fun _ => q).

Definition inject_Q (q : Q) : CReal :=
{|
  seq := (fun n : Z => q);
  scale := Qbound_ltabs_ZExp2 q;
  cauchy := inject_Q_cauchy q;
  bound := (fun _ : Z => Qbound_ltabs_ZExp2_spec q)
|}.

Definition inject_Z : Z -> CReal
  := fun n => inject_Q (n # 1).

Notation "0" := (inject_Q 0) : CReal_scope.
Notation "1" := (inject_Q 1) : CReal_scope.
Notation "2" := (inject_Q 2) : CReal_scope.

Lemma CRealLt_0_1 : CRealLt (inject_Q 0) (inject_Q 1).

Lemma CReal_injectQPos : forall q : Q,
    (0 < q)%Q -> CRealLt (inject_Q 0) (inject_Q q).

Lemma inject_Q_compare : forall (x : CReal) (p : Z),
    x <= inject_Q (seq x p + (2^p )).

Add Parametric Morphism : inject_Q
    with signature Qeq ==> CRealEq
      as inject_Q_morph.

#[global]
Instance inject_Q_morph_T
  : CMorphisms.Proper
      (CMorphisms.respectful Qeq CRealEq) inject_Q.

Algebraic operations

We reduce the rational numbers to accelerate calculations.

Definition CReal_plus_seq (x y : CReal) :=
  (fun n : Z => Qred (seq x (n -1)%Z + seq y (n -1)%Z)).

Definition CReal_plus_scale (x y : CReal) : Z :=
  Z.max x.(scale) y.(scale) + 1.

Lemma CReal_plus_cauchy : forall (x y : CReal),
  QCauchySeq (CReal_plus_seq x y).

Lemma CReal_plus_bound : forall (x y : CReal),
  QBound (CReal_plus_seq x y) (CReal_plus_scale x y).

Definition CReal_plus (x y : CReal) : CReal :=
{|
  seq := CReal_plus_seq x y;
  scale := CReal_plus_scale x y;
  cauchy := CReal_plus_cauchy x y;
  bound := CReal_plus_bound x y
|}.

Infix "+" := CReal_plus : CReal_scope.

Definition CReal_opp_seq (x : CReal) :=
  (fun n : Z => - seq x n).

Definition CReal_opp_scale (x : CReal) : Z :=
  x.(scale).

Lemma CReal_opp_cauchy : forall (x : CReal),
  QCauchySeq (CReal_opp_seq x).

Lemma CReal_opp_bound : forall (x : CReal),
  QBound (CReal_opp_seq x) (CReal_opp_scale x).

Definition CReal_opp (x : CReal) : CReal :=
{|
  seq := CReal_opp_seq x;
  scale := CReal_opp_scale x;
  cauchy := CReal_opp_cauchy x;
  bound := CReal_opp_bound x
|}.

Notation "- x" := (CReal_opp x) : CReal_scope.

Definition CReal_minus (x y : CReal) : CReal
  := CReal_plus x (CReal_opp y).

Infix "-" := CReal_minus : CReal_scope.

Lemma CReal_red_seq: forall (a : Z -> Q) (b : Z) (c : QCauchySeq a) (d : QBound a b),
  seq (mkCReal a b c d) = a.

Lemma CReal_plus_assoc : forall (x y z : CReal),
    (x + y ) + z == x + (y + z ).

Lemma CReal_plus_comm : forall x y : CReal,
    x + y == y + x.

Lemma CReal_plus_0_l : forall r : CReal,
    inject_Q 0 + r == r.

Lemma CReal_plus_0_r : forall r : CReal,
    r + 0 == r.

Lemma CReal_plus_lt_compat_l :
  forall x y z : CReal, y < z -> x + y < x + z.

Lemma CReal_plus_lt_compat_r :
  forall x y z : CReal, y < z -> y + x < z + x.

Lemma CReal_plus_lt_reg_l :
  forall x y z : CReal, x + y < x + z -> y < z.

Lemma CReal_plus_lt_reg_r :
  forall x y z : CReal, y + x < z + x -> y < z.

Lemma CReal_plus_le_reg_l :
  forall x y z : CReal, x + y <= x + z -> y <= z.

Lemma CReal_plus_le_reg_r :
  forall x y z : CReal, y + x <= z + x -> y <= z.

Lemma CReal_plus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2.

Lemma CReal_plus_le_lt_compat :
  forall r1 r2 r3 r4 : CReal, r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4.

Lemma CReal_plus_le_compat :
  forall r1 r2 r3 r4 : CReal, r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4.

Lemma CReal_plus_opp_r : forall x : CReal,
    x + - x == 0.

Lemma CReal_plus_opp_l : forall x : CReal,
    - x + x == 0.

Lemma CReal_plus_proper_r : forall x y z : CReal,
    CRealEq x y -> CRealEq (CReal_plus x z) (CReal_plus y z).

Lemma CReal_plus_proper_l : forall x y z : CReal,
    CRealEq x y -> CRealEq (CReal_plus z x) (CReal_plus z y).

Add Parametric Morphism : CReal_plus
    with signature CRealEq ==> CRealEq ==> CRealEq
      as CReal_plus_morph.

#[global]
Instance CReal_plus_morph_T
  : CMorphisms.Proper
      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRealEq)) CReal_plus.

Lemma CReal_plus_eq_reg_l : forall (r r1 r2 : CReal),
    r + r1 == r + r2 -> r1 == r2.

Lemma CReal_opp_0 : -0 == 0.

Lemma CReal_opp_plus_distr : forall r1 r2, - (r1 + r2 ) == - r1 + - r2.

Lemma CReal_opp_involutive : forall x:CReal, --x == x.

Lemma CReal_opp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2.

Lemma CReal_opp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2.

Lemma inject_Q_plus : forall q r : Q,
    inject_Q (q + r) == inject_Q q + inject_Q r.

Lemma inject_Q_one : inject_Q 1 == 1.

Lemma inject_Q_lt : forall q r : Q,
    Qlt q r -> inject_Q q < inject_Q r.

Lemma opp_inject_Q : forall q : Q,
    inject_Q (-q) == - inject_Q q.

Lemma lt_inject_Q : forall q r : Q,
    inject_Q q < inject_Q r -> (q < r)%Q.

Lemma le_inject_Q : forall q r : Q,
    inject_Q q <= inject_Q r -> (q <= r)%Q.

Lemma inject_Q_le : forall q r : Q,
    (q <= r)%Q -> inject_Q q <= inject_Q r.

Lemma inject_Z_plus : forall q r : Z,
    inject_Z (q + r) == inject_Z q + inject_Z r.

Lemma opp_inject_Z : forall n : Z,
    inject_Z (-n) == - inject_Z n.

Library Coq.Reals.Cauchy.ConstructiveCauchyReals

Algebraic operations

Navigation