Library Stdlib.Reals.ClassicalConstructiveReals

Proof that classical reals are constructive reals with extra properties, namely total order, existence of all least upper bounds and setoid equivalence simplifying to Leibniz equality.

From this point of view, the quotient Rabst and Rrepr between classical Dedekind reals and constructive Cauchy reals becomes an isomorphism for the ConstructiveReals structure.

This allows to apply results from constructive reals to classical reals.

From Stdlib Require Import QArith_base.
From Stdlib Require Import Znat.
From Stdlib Require Import Rdefinitions.
From Stdlib Require Import Raxioms.
From Stdlib Require Import ConstructiveReals.
From Stdlib Require Import ConstructiveCauchyReals.
From Stdlib Require Import ConstructiveCauchyRealsMult.
From Stdlib Require Import ConstructiveRcomplete.
From Stdlib Require Import ConstructiveCauchyAbs.
From Stdlib Require Import ConstructiveRealsMorphisms.

Local Open Scope R_scope.

Lemma RisLinearOrder : isLinearOrder Rlt.

Lemma RdisjunctEpsilon
  : forall a b c d : R, (a < b)%R \/ (c < d)%R -> (a < b)%R + (c < d)%R.

Definition Req_constr (x y : R) : Prop
  := (x < y -> False ) /\ (y < x -> False ).

Lemma Req_constr_refl : forall x:R, Req_constr x x.

Lemma Req_constr_leibniz : forall x y:R, Req_constr x y -> x = y.

Definition IQR (q : Q) := Rabst (inject_Q q).

Lemma IQR_zero_quot : Req_constr (IQR 0) R0.

Lemma Rring : ring_theory (IQR 0) (IQR 1) Rplus Rmult
                          (fun x y : R => (x + - y)%R) Ropp Req_constr.

Lemma RringExt : ring_eq_ext Rplus Rmult Ropp Req_constr.

Lemma Rleft_inverse :
  forall r : R, (sum (r < IQR 0) (IQR 0 < r)) -> Req_constr (/ r * r) (IQR 1).

Lemma Rinv_pos : forall r : R, (sum (r < IQR 0) (IQR 0 < r)) -> IQR 0 < r -> IQR 0 < / r.

Lemma Rmult_pos : forall x y : R, IQR 0 < x -> IQR 0 < y -> IQR 0 < x * y.

Lemma Rplus_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2.

Lemma Rzero_lt_one : IQR 0 < IQR 1.

Lemma plus_IQR : forall q r : Q,
    IQR (q + r) = IQR q + IQR r.

Lemma mult_IQR : forall q r : Q,
    IQR (q * r) = IQR q * IQR r.

Lemma IQR_lt : forall n m:Q, (n < m)%Q -> IQR n < IQR m.

Lemma lt_IQR : forall n m:Q, IQR n < IQR m -> (n < m)%Q.

Lemma IQR_plus_quot : forall q r : Q, Req_constr (IQR (q + r)) (IQR q + IQR r).

Lemma IQR_mult_quot : forall q r : Q, Req_constr (IQR (q * r)) (IQR q * IQR r).

Lemma Rabove_pos : forall x : R, {n : positive & x < IQR (Z.pos n # 1)}.

Lemma Rarchimedean : forall x y : R, x < y -> {q : Q & ((x < IQR q ) * (IQR q < y ))%type}.

Lemma RabsLUB : forall x y : R, (y < x -> False ) /\ (y < - x -> False ) <-> (y < Rabst (CReal_abs (Rrepr x)) -> False ).

Lemma Rcomplete : forall xn : nat -> R,
  (forall p : positive,
   {n : nat |
   forall i j : nat,
   (n <= i)%nat -> (n <= j)%nat -> IQR (1 # p) < Rabst (CReal_abs (Rrepr (xn i + - xn j))) -> False }) ->
  {l : R &
  forall p : positive,
  {n : nat |
  forall i : nat, (n <= i)%nat -> IQR (1 # p) < Rabst (CReal_abs (Rrepr (xn i + - l))) -> False }}.

Definition Rabs_quot (x : R) := Rabst (CReal_abs (Rrepr x)).
Definition Rinv_quot (x : R) (xnz : sum (x < IQR 0) (IQR 0 < x)) := Rinv x.
Definition Rlt_epsilon (x y : R) (H : x < y) := H.

Definition DRealConstructive : ConstructiveReals
  := Build_ConstructiveReals
       R Rlt RisLinearOrder Rlt
       Rlt_epsilon Rlt_epsilon
       RdisjunctEpsilon IQR IQR_lt lt_IQR
       Rplus Ropp Rmult
       IQR_plus_quot IQR_mult_quot
       Rring RringExt Rzero_lt_one
       Rplus_lt_compat_l Rplus_reg_l Rmult_pos
       Rinv_quot Rleft_inverse Rinv_pos
       Rarchimedean Rabove_pos
       Rabs_quot RabsLUB Rcomplete.

Definition Rrepr_morphism
  : @ConstructiveRealsMorphism DRealConstructive CRealConstructive.

Definition Rabst_morphism
  : @ConstructiveRealsMorphism CRealConstructive DRealConstructive.