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.

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

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

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

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

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 DRealAbstr : CReal -> DReal.

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

Definition DRealRepr : DReal -> CReal.

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 lowerUpper : forall (f : Q -> bool) (q r : Q),
    isLowerCut f -> Qle q r -> f q = false -> f r = false.

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
    -> (proj1_sig x (S n) <= q + (1 # Pos.of_nat (S n)))%Q.

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