Library Coq.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.

Require Import QArith_base.
Require Import Rdefinitions.
Require Import Raxioms.
Require Import ConstructiveReals.
Require Import ConstructiveCauchyReals.
Require Import ConstructiveCauchyRealsMult.
Require Import ConstructiveRcomplete.
Require Import ConstructiveCauchyAbs.
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.

Library Coq.Reals.ClassicalConstructiveReals

Navigation