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.