Library Coq.Reals.ClassicalDedekindReals


Require Import Coq.Logic.Eqdep_dec.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.HLevels.
Require Import QArith.
Require Import Qabs.
Require Import ConstructiveCauchyReals.
Require Import ConstructiveRcomplete.
Require Import Lia.
Require Import Lqa.
Require Import Qpower.
Require Import QExtra.
Require CMorphisms.

Q Auxiliary Lemmas



Local Lemma Qpower_2_neg_eq_natpow_inv : forall n : nat,
    (2 ^ (- Z.of_nat n) == 1#(Pos.of_nat (2^n)%nat))%Q.

Local Lemma Qpower_2_invneg_le_pow : forall n : Z,
    (1 # Pos.of_nat (2 ^ Z.to_nat (- n)) <= 2 ^ n)%Q.

Local Lemma Qpower_2_neg_le_one : forall n : nat,
    (2 ^ (- Z.of_nat n) <= 1)%Q.

Dedekind cuts

Definition

Classical Dedekind reals. With the 3 logical axioms funext, sig_forall_dec and sig_not_dec, the lower cuts defined as functions Q -> bool have all the classical properties of the real numbers.
We could prove operations and theorems about them directly, but instead we notice that they are a quotient of the constructive Cauchy reals, from which they inherit many properties.

Axiom sig_forall_dec
  : forall (P : nat -> Prop),
    (forall n, {P n} + {~P n})
    -> {n | ~P n} + {forall n, P n}.

Axiom sig_not_dec : forall P : Prop, { ~~P } + { ~P }.

Definition isLowerCut (f : Q -> bool) : Prop
  := (forall q r:Q, Qle q r -> f r = true -> f q = true)
     /\ ~(forall q:Q, f q = true)
     /\ ~(forall q:Q, f q = false)
     
     /\ (forall q:Q, f q = true -> ~(forall r:Q, Qle r q \/ f r = false)).

Properties


Lemma isLowerCut_hprop : forall (f : Q -> bool),
    IsHProp (isLowerCut f).

Lemma lowerCutBelow : forall f : Q -> bool,
    isLowerCut f -> { q : Q | f q = true }.

Lemma lowerCutAbove : forall f : Q -> bool,
    isLowerCut f -> { q : Q | f q = false }.

Lemma lowerUpper : forall (f : Q -> bool) (q r : Q),
    isLowerCut f -> Qle q r -> f q = false -> f r = false.

Lemma UpperAboveLower : forall (f : Q -> bool) (q r : Q),
    isLowerCut f
    -> f q = true
    -> f r = false
    -> Qlt q r.

Classical Dedekind reals

Definition


Definition DReal : Set
  := { f : Q -> bool | isLowerCut f }.

Induction principle


Fixpoint DRealQlim_rec (f : Q -> bool) (low : isLowerCut f) (n p : nat) { struct p }
  : f (proj1_sig (lowerCutBelow f low) + (Z.of_nat p # Pos.of_nat (S n)))%Q = false
    -> { q : Q | f q = true /\ f (q + (1 # Pos.of_nat (S n)))%Q = false }.

Conversion to and from constructive Cauchy real CReal

Conversion from CReal to DReal


Lemma DRealAbstr_aux :
  forall x H,
  isLowerCut (fun q : Q =>
    if sig_forall_dec (fun n : nat => seq x (- Z.of_nat n) <= q + 2 ^ (- Z.of_nat n)) (H q)
    then true else false).

Definition DRealAbstr : CReal -> DReal.

Conversion from DReal to CReal


Definition DRealQlim (x : DReal) (n : nat)
  : { q : Q | proj1_sig x q = true /\ proj1_sig x (q + (1# Pos.of_nat (S n)))%Q = false }.

Definition DRealQlimExp2 (x : DReal) (n : nat)
  : { q : Q | proj1_sig x q = true /\ proj1_sig x (q + (1#(Pos.of_nat (2^n)%nat)))%Q = false }.

Definition CReal_of_DReal_seq (x : DReal) (n : Z) :=
    proj1_sig (DRealQlimExp2 x (Z.to_nat (-n))).

Lemma CReal_of_DReal_cauchy (x : DReal) :
    QCauchySeq (CReal_of_DReal_seq x).

Lemma CReal_of_DReal_seq_max_prec_1 : forall (x : DReal) (n : Z),
   (n>=0)%Z -> CReal_of_DReal_seq x n = CReal_of_DReal_seq x 0.

Lemma CReal_of_DReal_seq_bound :
  forall (x : DReal) (i j : Z),
    (Qabs (CReal_of_DReal_seq x i - CReal_of_DReal_seq x j) <= 1)%Q.

Definition CReal_of_DReal_scale (x : DReal) : Z :=
  Qbound_lt_ZExp2 (Qabs (CReal_of_DReal_seq x (-1)) + 2)%Q.

Lemma CReal_of_DReal_bound : forall (x : DReal),
  QBound (CReal_of_DReal_seq x) (CReal_of_DReal_scale x).

Definition DRealRepr (x : DReal) : CReal :=
{|
  seq := CReal_of_DReal_seq x;
  scale := CReal_of_DReal_scale x;
  cauchy := CReal_of_DReal_cauchy x;
  bound := CReal_of_DReal_bound x
|}.

Order for DReal


Definition Rle (x y : DReal)
  := forall q:Q, proj1_sig x q = true -> proj1_sig y q = true.

Lemma Rle_antisym : forall x y : DReal,
    Rle x y
    -> Rle y x
    -> x = y.

Lemma DRealOpen : forall (x : DReal) (q : Q),
    proj1_sig x q = true
    -> { r : Q | Qlt q r /\ proj1_sig x r = true }.

Lemma DRealReprQ : forall (x : DReal) (q : Q),
    proj1_sig x q = true
    -> CRealLt (inject_Q q) (DRealRepr x).

Lemma DRealReprQup : forall (x : DReal) (q : Q),
    proj1_sig x q = false
    -> CRealLe (DRealRepr x) (inject_Q q).

Lemma DRealQuot1 : forall x y:DReal, CRealEq (DRealRepr x) (DRealRepr y) -> x = y.

Lemma DRealAbstrFalse : forall (x : CReal) (q : Q) (n : nat),
    proj1_sig (DRealAbstr x) q = false
    -> (seq x (- Z.of_nat n) <= q + 2 ^ (- Z.of_nat n))%Q.

For arbitrary n:Z, we need to relaxe the bound

Lemma DRealAbstrFalse' : forall (x : CReal) (q : Q) (n : Z),
    proj1_sig (DRealAbstr x) q = false
    -> (seq x n <= q + 2*2^n)%Q.

Lemma DRealAbstrFalse'' : forall (x : CReal) (q : Q) (n : Z),
    proj1_sig (DRealAbstr x) q = false
    -> (seq x n <= q + 2^n + 1)%Q.

Lemma DRealQuot2 : forall x:CReal, CRealEq (DRealRepr (DRealAbstr x)) x.