Library Stdlib.Reals.ClassicalDedekindReals

From Stdlib.Logic Require Import Eqdep_dec.
From Stdlib.Logic Require Import FunctionalExtensionality.
From Stdlib.Logic Require Import HLevels.
From Stdlib Require Import QArith.
From Stdlib Require Import Qabs.
From Stdlib Require Import ConstructiveCauchyReals.
From Stdlib Require Import ConstructiveRcomplete.
From Stdlib Require Import Lia.
From Stdlib Require Import Lqa.
From Stdlib Require Import Qpower.
From Stdlib Require Import QExtra.
From Stdlib Require Import Znat.
From Stdlib Require Import ZArith_dec.
From Stdlib 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.