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

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