Library Coq.Reals.ConstructiveCauchyReals

Require Import QArith.
Require Import Qabs.
Require Import Qround.
Require Import Logic.ConstructiveEpsilon.
Require CMorphisms.

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.

Definition QSeqEquiv (un vn : nat -> Q) (cvmod : positive -> nat)
  : Prop
  := forall (k : positive) (p q : nat),
      le (cvmod k) p
      -> le (cvmod k) q
      -> Qlt (Qabs (un p - vn q)) (1 # k).

Definition QCauchySeq (un : nat -> Q) (cvmod : positive -> nat) : Prop
  := QSeqEquiv un un cvmod.

Lemma QSeqEquiv_sym : forall (un vn : nat -> Q) (cvmod : positive -> nat),
    QSeqEquiv un vn cvmod
    -> QSeqEquiv vn un cvmod.

Lemma factorDenom : forall (a:Z) (b d:positive), (a # (d * b )) == (1#d ) * (a #b ).

Lemma QSeqEquiv_trans : forall (un vn wn : nat -> Q)
                          (cvmod cvmodw : positive -> nat),
    QSeqEquiv un vn cvmod
    -> QSeqEquiv vn wn cvmodw
    -> QSeqEquiv un wn (fun q => max (cvmod (2 * q)%positive) (cvmodw (2 * q)%positive)).

Definition QSeqEquivEx (un vn : nat -> Q) : Prop
  := exists (cvmod : positive -> nat ), QSeqEquiv un vn cvmod.

Lemma QSeqEquivEx_sym : forall (un vn : nat -> Q), QSeqEquivEx un vn -> QSeqEquivEx vn un.

Lemma QSeqEquivEx_trans : forall un vn wn : nat -> Q,
    QSeqEquivEx un vn
    -> QSeqEquivEx vn wn
    -> QSeqEquivEx un wn.

Lemma QSeqEquiv_cau_r : forall (un vn : nat -> Q) (cvmod : positive -> nat),
    QSeqEquiv un vn cvmod
    -> QCauchySeq vn (fun k => cvmod (2 * k)%positive).

Fixpoint increasing_modulus (modulus : positive -> nat) (n : nat)
  := match n with
     | O => modulus xH
     | S p => max (modulus (Pos.of_nat n)) (increasing_modulus modulus p)
     end.

Lemma increasing_modulus_inc : forall (modulus : positive -> nat) (n p : nat),
    le (increasing_modulus modulus n)
       (increasing_modulus modulus (p + n)).

Lemma increasing_modulus_max : forall (modulus : positive -> nat) (p n : nat),
    le n p -> le (modulus (Pos.of_nat n))
                 (increasing_modulus modulus p).

Lemma standard_modulus : forall (un : nat -> Q) (cvmod : positive -> nat),
    QCauchySeq un cvmod
    -> (QCauchySeq (fun n => un (increasing_modulus cvmod n)) Pos.to_nat
       /\ QSeqEquiv un (fun n => un (increasing_modulus cvmod n))
                   (fun p => max (cvmod p) (Pos.to_nat p))).

Definition CReal : Set
  := { x : (nat -> Q ) | QCauchySeq x Pos.to_nat }.

Delimit Scope CReal_scope with CReal.

Local Open Scope CReal_scope.

Definition CRealLt (x y : CReal) : Set
  := { n : positive | Qlt (2 # n)
                           (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n)) }.

Definition CRealLtProp (x y : CReal) : Prop
  := exists n : positive , Qlt (2 # n)
                         (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat 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, {P n } + {~P n })
                    -> {n | ~P n } + {forall n, P n })
    -> CRealLt x y + (CRealLt x y -> False ).

Definition CRealEq (x y : CReal) : Prop
  := (CRealLt x y -> False ) /\ (CRealLt y x -> False ).

Infix "==" := CRealEq : CReal_scope.

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.

Lemma CRealLe_not_lt : forall x y : CReal,
    (forall n:positive, Qle (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n))
                       (2 # n))
    <-> x <= y.

Lemma CRealEq_diff : forall (x y : CReal),
    CRealEq x y
    <-> forall n:positive, Qle (Qabs (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n)))
                        (2 # n).

Lemma CRealEq_modindep : forall (x y : CReal),
    QSeqEquivEx (proj1_sig x) (proj1_sig y)
    <-> forall n:positive,
      Qle (Qabs (proj1_sig x (Pos.to_nat n) - proj1_sig y (Pos.to_nat n))) (2 # n).

Lemma CRealLt_aboveSig : forall (x y : CReal) (n : positive),
    (Qlt (2 # n)
         (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n)))
    -> let (k, _) := Qarchimedean (/(proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n) - (2#n )))
      in forall p:positive,
          Pos.le (Pos.max n (2*k)) p
          -> Qlt (2 # (Pos.max n (2*k)))
                (proj1_sig y (Pos.to_nat p) - proj1_sig x (Pos.to_nat p)).

Lemma CRealLt_above : forall (x y : CReal),
    CRealLt x y
    -> { k : positive | forall p:positive,
          Pos.le k p -> Qlt (2 # k) (proj1_sig y (Pos.to_nat p)
                                    - proj1_sig x (Pos.to_nat p)) }.

Lemma CRealLt_above_same : forall (x y : CReal) (n : positive),
    Qlt (2 # n)
        (proj1_sig y (Pos.to_nat n) - proj1_sig x (Pos.to_nat n))
    -> forall p:positive, Pos.le n p
                    -> Qlt (proj1_sig x (Pos.to_nat p)) (proj1_sig y (Pos.to_nat 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.

Instance CRealEq_relT : CRelationClasses.Equivalence CRealEq.

Instance CRealLt_morph
  : CMorphisms.Proper
      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CRealLt.

Instance CRealGt_morph
  : CMorphisms.Proper
      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRelationClasses.iffT)) CRealGt.

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 ConstCauchy : forall q : Q,
    QCauchySeq (fun _ => q) Pos.to_nat.

Definition inject_Q : Q -> CReal.

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,
    Qlt 0 q -> CRealLt (inject_Q 0) (inject_Q q).

Lemma CRealLtQ : forall (x : CReal) (q : Q),
    CRealLt x (inject_Q q)
    -> forall p:positive, Qlt (proj1_sig x (Pos.to_nat p)) (q + (1#p )).

Lemma CRealLtQopp : forall (x : CReal) (q : Q),
    CRealLt (inject_Q q) x
    -> forall p:positive, Qlt (q - (1#p )) (proj1_sig x (Pos.to_nat p)).

Lemma inject_Q_compare : forall (x : CReal) (p : positive),
    x <= inject_Q (proj1_sig x (Pos.to_nat p) + (1#p )).

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

Instance inject_Q_morph_T
  : CMorphisms.Proper
      (CMorphisms.respectful Qeq CRealEq) inject_Q.

Lemma CReal_plus_cauchy
  : forall (xn yn zn : nat -> Q) (cvmod : positive -> nat),
    QSeqEquiv xn yn cvmod
    -> QCauchySeq zn Pos.to_nat
    -> QSeqEquiv (fun n:nat => xn n + zn n) (fun n:nat => yn n + zn n)
                (fun p => max (cvmod (2 * p)%positive)
                           (Pos.to_nat (2 * p)%positive)).

Definition CReal_plus (x y : CReal) : CReal.

Infix "+" := CReal_plus : CReal_scope.

Lemma CReal_plus_nth : forall (x y : CReal) (n : nat),
    proj1_sig (x + y) n = Qplus (proj1_sig x (2*n)%nat) (proj1_sig y (2*n)%nat).

Lemma CReal_plus_unfold : forall (x y : CReal),
    QSeqEquiv (proj1_sig (CReal_plus x y))
              (fun n : nat => proj1_sig x n + proj1_sig y n)%Q
              (fun p => Pos.to_nat (2 * p)).

Definition CReal_opp (x : CReal) : CReal.

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 belowMultiple : forall n p : nat, lt 0 p -> le n (p * n).

Lemma CReal_plus_assoc : forall (x y z : CReal),
    CRealEq (CReal_plus (CReal_plus x y) z)
            (CReal_plus x (CReal_plus y z)).

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

Lemma CReal_plus_0_l : forall r : CReal,
    CRealEq (CReal_plus (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.

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 -> Qlt q r.

Lemma le_inject_Q : forall q r : Q,
    inject_Q q <= inject_Q r -> Qle q r.

Lemma inject_Q_le : forall q r : Q,
    Qle q r -> 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.ConstructiveCauchyReals

Navigation