Library Coq.Reals.Abstract.ConstructiveReals


An interface for constructive and computable real numbers. All of its instances are isomorphic (see file ConstructiveRealsMorphisms). For example it is implemented by the Cauchy reals in file ConstructivecauchyReals and also implemented by the sumbool-based Dedekind reals defined by
Structure R := { lower : Q -> Prop; upper : Q -> Prop; lower_proper : Proper (Qeq ==> iff) lower; upper_proper : Proper (Qeq ==> iff) upper; lower_bound : { q : Q | lower q }; upper_bound : { r : Q | upper r }; lower_lower : forall q r, q < r -> lower r -> lower q; lower_open : forall q, lower q -> exists r, q < r /\ lower r; upper_upper : forall q r, q < r -> upper q -> upper r; upper_open : forall r, upper r -> exists q, q < r /\ upper q; disjoint : forall q, ~ (lower q /\ upper q); located : forall q r, q < r -> { lower q } + { upper r } }.
see github.com/andrejbauer/dedekind-reals for the Prop-based version of those Dedekind reals (although Prop fails to make them an instance of ConstructiveReals).
Any computation about constructive reals can be worked in the fastest instance for it; we then transport the results to all other instances by the isomorphisms. This way of working is different from the usual interfaces, where we would rather prove things abstractly, by quantifying universally on the instance.
The functions of ConstructiveReals do not have a direct impact on performance, because algorithms will be extracted from instances, and because fast ConstructiveReals morphisms should be coded manually. However, since instances are forced to implement those functions, it is probable that they will also use them in their algorithms. So those functions hint at what we think will yield fast and small extracted programs.
Constructive reals are setoids, which custom equality is defined as x == y iff (x <= y /\ y <= x). It is hard to quotient constructively to get the Leibniz equality on the real numbers. In "Sheaves in Geometry and Logic", MacLane and Moerdijk show a topos in which all functions R -> Z are constant. Consequently all functions R -> Q are constant and it is not possible to approximate real numbers by rational numbers.
WARNING: this file is experimental and likely to change in future releases.

Require Import QArith Qabs Qround.

Definition isLinearOrder {X : Set} (Xlt : X -> X -> Set) : Set
  := (forall x y:X, Xlt x y -> Xlt y x -> False)
     * (forall x y z : X, Xlt x y -> Xlt y z -> Xlt x z)
     * (forall x y z : X, Xlt x z -> Xlt x y + Xlt y z).

Structure ConstructiveReals : Type :=
  {
    CRcarrier : Set;

    
    CRlt : CRcarrier -> CRcarrier -> Set;
    CRltLinear : isLinearOrder CRlt;

    CRle (x y : CRcarrier) := CRlt y x -> False;
    CReq (x y : CRcarrier) := CRle y x /\ CRle x y;
    CRapart (x y : CRcarrier) := sum (CRlt x y) (CRlt y x);

    
    CRltProp : CRcarrier -> CRcarrier -> Prop;
    
    CRltEpsilon : forall x y : CRcarrier, CRltProp x y -> CRlt x y;
    CRltForget : forall x y : CRcarrier, CRlt x y -> CRltProp x y;
    CRltDisjunctEpsilon : forall a b c d : CRcarrier,
        (CRltProp a b \/ CRltProp c d) -> CRlt a b + CRlt c d;

    
    CR_of_Q : Q -> CRcarrier;
    CR_of_Q_lt : forall q r : Q,
        Qlt q r -> CRlt (CR_of_Q q) (CR_of_Q r);
    lt_CR_of_Q : forall q r : Q,
        CRlt (CR_of_Q q) (CR_of_Q r) -> Qlt q r;

    
    CRplus : CRcarrier -> CRcarrier -> CRcarrier;
    CRopp : CRcarrier -> CRcarrier;
    CRmult : CRcarrier -> CRcarrier -> CRcarrier;

    CR_of_Q_plus : forall q r : Q, CReq (CR_of_Q (q+r))
                                           (CRplus (CR_of_Q q) (CR_of_Q r));
    CR_of_Q_mult : forall q r : Q, CReq (CR_of_Q (q*r))
                                           (CRmult (CR_of_Q q) (CR_of_Q r));
    CRisRing : ring_theory (CR_of_Q 0) (CR_of_Q 1) CRplus CRmult
                          (fun x y => CRplus x (CRopp y)) CRopp CReq;
    CRisRingExt : ring_eq_ext CRplus CRmult CRopp CReq;

    
    CRzero_lt_one : CRlt (CR_of_Q 0) (CR_of_Q 1);
    CRplus_lt_compat_l : forall r r1 r2 : CRcarrier,
        CRlt r1 r2 -> CRlt (CRplus r r1) (CRplus r r2);
    CRplus_lt_reg_l : forall r r1 r2 : CRcarrier,
        CRlt (CRplus r r1) (CRplus r r2) -> CRlt r1 r2;
    CRmult_lt_0_compat : forall x y : CRcarrier,
        CRlt (CR_of_Q 0) x -> CRlt (CR_of_Q 0) y -> CRlt (CR_of_Q 0) (CRmult x y);

    
    CRinv : forall x : CRcarrier, CRapart x (CR_of_Q 0) -> CRcarrier;
    CRinv_l : forall (r:CRcarrier) (rnz : CRapart r (CR_of_Q 0)),
        CReq (CRmult (CRinv r rnz) r) (CR_of_Q 1);
    CRinv_0_lt_compat : forall (r : CRcarrier) (rnz : CRapart r (CR_of_Q 0)),
        CRlt (CR_of_Q 0) r -> CRlt (CR_of_Q 0) (CRinv r rnz);

    
    CR_Q_dense : forall x y : CRcarrier, CRlt x y ->
       { q : Q & prod (CRlt x (CR_of_Q q))
                        (CRlt (CR_of_Q q) y) };
    CR_archimedean : forall x : CRcarrier,
        { n : positive & CRlt x (CR_of_Q (Z.pos n # 1)) };

    CRminus (x y : CRcarrier) : CRcarrier
    := CRplus x (CRopp y);

    
    CRabs : CRcarrier -> CRcarrier;
    CRabs_def : forall x y : CRcarrier,
        (CRle x y /\ CRle (CRopp x) y)
        <-> CRle (CRabs x) y;

    
    CR_cv (un : nat -> CRcarrier) (l : CRcarrier) : Set
    := forall p:positive,
        { n : nat | forall i:nat, le n i
                           -> CRle (CRabs (CRminus (un i) l))
                                  (CR_of_Q (1#p)) };
    CR_cauchy (un : nat -> CRcarrier) : Set
    := forall p : positive,
        { n : nat | forall i j:nat, le n i -> le n j
                             -> CRle (CRabs (CRminus (un i) (un j)))
                                    (CR_of_Q (1#p)) };

    
    CR_complete :
      forall xn : (nat -> CRcarrier),
        CR_cauchy xn -> { l : CRcarrier & CR_cv xn l };
  }.


Delimit Scope ConstructiveReals with ConstructiveReals.

Notation "x < y" := (CRlt _ x y) : ConstructiveReals.
Notation "x <= y" := (CRle _ x y) : ConstructiveReals.
Notation "x <= y <= z" := (CRle _ x y /\ CRle _ y z) : ConstructiveReals.
Notation "x < y < z" := (prod (CRlt _ x y) (CRlt _ y z)) : ConstructiveReals.
Notation "x == y" := (CReq _ x y) : ConstructiveReals.
Notation "x ≶ y" := (CRapart _ x y) (at level 70, no associativity) : ConstructiveReals.
Notation "0" := (CR_of_Q _ 0) : ConstructiveReals.
Notation "1" := (CR_of_Q _ 1) : ConstructiveReals.
Notation "2" := (CR_of_Q _ 2) : ConstructiveReals.
Notation "3" := (CR_of_Q _ 3) : ConstructiveReals.
Notation "4" := (CR_of_Q _ 4) : ConstructiveReals.
Notation "5" := (CR_of_Q _ 5) : ConstructiveReals.
Notation "6" := (CR_of_Q _ 6) : ConstructiveReals.
Notation "7" := (CR_of_Q _ 7) : ConstructiveReals.
Notation "8" := (CR_of_Q _ 8) : ConstructiveReals.
Notation "9" := (CR_of_Q _ 9) : ConstructiveReals.
Notation "10" := (CR_of_Q _ 10) : ConstructiveReals.
Notation "x + y" := (CRplus _ x y) : ConstructiveReals.
Notation "- x" := (CRopp _ x) : ConstructiveReals.
Notation "x - y" := (CRminus _ x y) : ConstructiveReals.
Notation "x * y" := (CRmult _ x y) : ConstructiveReals.
Notation "/ x" := (CRinv _ x) : ConstructiveReals.

Local Open Scope ConstructiveReals.

Lemma CRlt_asym : forall {R : ConstructiveReals} (x y : CRcarrier R),
    x < y -> x <= y.

Lemma CRlt_proper
  : forall R : ConstructiveReals,
    CMorphisms.Proper
      (CMorphisms.respectful (CReq R)
                             (CMorphisms.respectful (CReq R) CRelationClasses.iffT)) (CRlt R).

Lemma CRle_refl : forall {R : ConstructiveReals} (x : CRcarrier R),
    x <= x.

Lemma CRle_lt_trans : forall {R : ConstructiveReals} (r1 r2 r3 : CRcarrier R),
    r1 <= r2 -> r2 < r3 -> r1 < r3.

Lemma CRlt_le_trans : forall {R : ConstructiveReals} (r1 r2 r3 : CRcarrier R),
    r1 < r2 -> r2 <= r3 -> r1 < r3.

Lemma CRle_trans : forall {R : ConstructiveReals} (x y z : CRcarrier R),
    x <= y -> y <= z -> x <= z.

Lemma CRlt_trans : forall {R : ConstructiveReals} (x y z : CRcarrier R),
    x < y -> y < z -> x < z.

Lemma CRlt_trans_flip : forall {R : ConstructiveReals} (x y z : CRcarrier R),
    y < z -> x < y -> x < z.

Lemma CReq_refl : forall {R : ConstructiveReals} (x : CRcarrier R),
    x == x.

Lemma CReq_sym : forall {R : ConstructiveReals} (x y : CRcarrier R),
    x == y -> y == x.

Lemma CReq_trans : forall {R : ConstructiveReals} (x y z : CRcarrier R),
    x == y -> y == z -> x == z.

Add Parametric Relation {R : ConstructiveReals} : (CRcarrier R) (CReq R)
    reflexivity proved by (CReq_refl)
    symmetry proved by (CReq_sym)
    transitivity proved by (CReq_trans)
      as CReq_rel.

Instance CReq_relT : forall {R : ConstructiveReals},
    CRelationClasses.Equivalence (CReq R).

Instance CRlt_morph
  : forall {R : ConstructiveReals}, CMorphisms.Proper
      (CMorphisms.respectful (CReq R) (CMorphisms.respectful (CReq R) CRelationClasses.iffT)) (CRlt R).

Add Parametric Morphism {R : ConstructiveReals} : (CRle R)
    with signature CReq R ==> CReq R ==> iff
      as CRle_morph.

Lemma CRplus_0_l : forall {R : ConstructiveReals} (x : CRcarrier R),
    0 + x == x.

Lemma CRplus_0_r : forall {R : ConstructiveReals} (x : CRcarrier R),
    x + 0 == x.

Lemma CRplus_opp_l : forall {R : ConstructiveReals} (x : CRcarrier R),
    - x + x == 0.

Lemma CRplus_opp_r : forall {R : ConstructiveReals} (x : CRcarrier R),
    x + - x == 0.

Lemma CRopp_0 : forall {R : ConstructiveReals},
    CRopp R 0 == 0.

Lemma CRplus_lt_compat_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    r1 < r2 -> r1 + r < r2 + r.

Lemma CRplus_lt_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    r1 + r < r2 + r -> r1 < r2.

Lemma CRplus_le_compat_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    r1 <= r2 -> r + r1 <= r + r2.

Lemma CRplus_le_compat_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    r1 <= r2 -> r1 + r <= r2 + r.

Lemma CRplus_le_compat : forall {R : ConstructiveReals} (r1 r2 r3 r4 : CRcarrier R),
    r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4.

Lemma CRle_minus : forall {R : ConstructiveReals} (x y : CRcarrier R),
    x <= y -> 0 <= y - x.

Lemma CRplus_le_reg_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    r + r1 <= r + r2 -> r1 <= r2.

Lemma CRplus_le_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    r1 + r <= r2 + r -> r1 <= r2.

Lemma CRplus_lt_le_compat :
  forall {R : ConstructiveReals} (r1 r2 r3 r4 : CRcarrier R),
    r1 < r2
    -> r3 <= r4
    -> r1 + r3 < r2 + r4.

Lemma CRplus_le_lt_compat :
  forall {R : ConstructiveReals} (r1 r2 r3 r4 : CRcarrier R),
    r1 <= r2
    -> r3 < r4
    -> r1 + r3 < r2 + r4.

Lemma CRplus_eq_reg_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    r + r1 == r + r2 -> r1 == r2.

Lemma CRplus_eq_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    r1 + r == r2 + r -> r1 == r2.

Lemma CRplus_assoc : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    r + r1 + r2 == r + (r1 + r2).

Lemma CRplus_comm : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
    r1 + r2 == r2 + r1.

Add Parametric Morphism {R : ConstructiveReals} : (CRplus R)
    with signature CReq R ==> CReq R ==> CReq R
      as CRplus_morph.

Add Parametric Morphism {R : ConstructiveReals} : (CRopp R)
    with signature CReq R ==> CReq R
      as CRopp_morph.

Add Parametric Morphism {R : ConstructiveReals} : (CRmult R)
    with signature CReq R ==> CReq R ==> CReq R
      as CRmult_morph.

Instance CRplus_morph_T
  : forall {R : ConstructiveReals}, CMorphisms.Proper
      (CMorphisms.respectful (CReq R) (CMorphisms.respectful (CReq R) (CReq R))) (CRplus R).

Instance CRmult_morph_T
  : forall {R : ConstructiveReals}, CMorphisms.Proper
      (CMorphisms.respectful (CReq R) (CMorphisms.respectful (CReq R) (CReq R))) (CRmult R).

Instance CRopp_morph_T
  : forall {R : ConstructiveReals}, CMorphisms.Proper
      (CMorphisms.respectful (CReq R) (CReq R)) (CRopp R).

Add Parametric Morphism {R : ConstructiveReals} : (CRminus R)
    with signature (CReq R) ==> (CReq R) ==> (CReq R)
      as CRminus_morph.

Instance CRminus_morph_T
  : forall {R : ConstructiveReals}, CMorphisms.Proper
      (CMorphisms.respectful (CReq R) (CMorphisms.respectful (CReq R) (CReq R))) (CRminus R).

Lemma CRopp_involutive : forall {R : ConstructiveReals} (r : CRcarrier R),
    - - r == r.

Lemma CRopp_gt_lt_contravar
  : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
    r2 < r1 -> - r1 < - r2.

Lemma CRopp_lt_cancel : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
    - r2 < - r1 -> r1 < r2.

Lemma CRopp_ge_le_contravar
  : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
    r2 <= r1 -> - r1 <= - r2.

Lemma CRopp_plus_distr : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
    - (r1 + r2) == - r1 + - r2.

Lemma CRmult_1_l : forall {R : ConstructiveReals} (r : CRcarrier R),
    1 * r == r.

Lemma CRmult_1_r : forall {R : ConstructiveReals} (x : CRcarrier R),
    x * 1 == x.

Lemma CRmult_assoc : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    r * r1 * r2 == r * (r1 * r2).

Lemma CRmult_comm : forall {R : ConstructiveReals} (r s : CRcarrier R),
    r * s == s * r.

Lemma CRmult_plus_distr_l : forall {R : ConstructiveReals} (r1 r2 r3 : CRcarrier R),
    r1 * (r2 + r3) == (r1 * r2) + (r1 * r3).

Lemma CRmult_plus_distr_r : forall {R : ConstructiveReals} (r1 r2 r3 : CRcarrier R),
    (r2 + r3) * r1 == (r2 * r1) + (r3 * r1).

Lemma CRzero_double : forall {R : ConstructiveReals} (x : CRcarrier R),
    x == x + x -> x == 0.

Lemma CRmult_0_r : forall {R : ConstructiveReals} (x : CRcarrier R),
    x * 0 == 0.

Lemma CRmult_0_l : forall {R : ConstructiveReals} (r : CRcarrier R),
    0 * r == 0.

Lemma CRopp_mult_distr_r : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
    - (r1 * r2) == r1 * (- r2).

Lemma CRopp_mult_distr_l : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R),
    - (r1 * r2) == (- r1) * r2.

Lemma CRmult_lt_compat_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    0 < r -> r1 < r2 -> r1 * r < r2 * r.

Lemma CRmult_lt_compat_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    0 < r -> r1 < r2 -> r * r1 < r * r2.

Lemma CRinv_r : forall {R : ConstructiveReals} (r:CRcarrier R)
                  (rnz : r ≶ 0),
    r * (/ r) rnz == 1.

Lemma CRmult_lt_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    0 < r -> r1 * r < r2 * r -> r1 < r2.

Lemma CRmult_lt_reg_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    0 < r -> r * r1 < r * r2 -> r1 < r2.

Lemma CRmult_le_compat_l_half : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    0 < r -> r1 <= r2 -> r * r1 <= r * r2.

Lemma CRmult_le_compat_r_half : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    0 < r
    -> r1 <= r2
    -> r1 * r <= r2 * r.

Lemma CRmult_eq_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    0 ≶ r
    -> r1 * r == r2 * r
    -> r1 == r2.

Lemma CRinv_1 : forall {R : ConstructiveReals} (onz : CRapart R 1 0),
    (/ 1) onz == 1.

Lemma CRmult_eq_reg_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    r ≶ 0
    -> r * r1 == r * r2
    -> r1 == r2.

Lemma CRinv_mult_distr :
  forall {R : ConstructiveReals} (r1 r2 : CRcarrier R)
    (r1nz : r1 ≶ 0) (r2nz : r2 ≶ 0)
    (rmnz : (r1*r2) ≶ 0),
    (/ (r1 * r2)) rmnz == (/ r1) r1nz * (/ r2) r2nz.

Lemma CRinv_morph : forall {R : ConstructiveReals} (x y : CRcarrier R)
                      (rxnz : x ≶ 0) (rynz : y ≶ 0),
    x == y
    -> (/ x) rxnz == (/ y) rynz.

Lemma CRlt_minus : forall {R : ConstructiveReals} (x y : CRcarrier R),
    x < y -> 0 < y - x.

Lemma CR_of_Q_le : forall {R : ConstructiveReals} (r q : Q),
    Qle r q
    -> CR_of_Q R r <= CR_of_Q R q.

Add Parametric Morphism {R : ConstructiveReals} : (CR_of_Q R)
    with signature Qeq ==> CReq R
      as CR_of_Q_morph.

Lemma eq_inject_Q : forall {R : ConstructiveReals} (q r : Q),
    CR_of_Q R q == CR_of_Q R r -> Qeq q r.

Instance CR_of_Q_morph_T
  : forall {R : ConstructiveReals}, CMorphisms.Proper
      (CMorphisms.respectful Qeq (CReq R)) (CR_of_Q R).

Lemma CR_of_Q_opp : forall {R : ConstructiveReals} (q : Q),
    CR_of_Q R (-q) == - CR_of_Q R q.

Lemma CR_of_Q_pos : forall {R : ConstructiveReals} (q:Q),
    Qlt 0 q -> 0 < CR_of_Q R q.

Lemma CR_of_Q_inv : forall {R : ConstructiveReals} (q : Q) (qPos : Qlt 0 q),
    CR_of_Q R (/q)
    == (/ CR_of_Q R q) (inr (CR_of_Q_pos q qPos)).

Lemma CRmult_le_0_compat : forall {R : ConstructiveReals} (a b : CRcarrier R),
    0 <= a -> 0 <= b -> 0 <= a * b.

Lemma CRmult_le_compat_l : forall {R : ConstructiveReals} (r r1 r2:CRcarrier R),
    0 <= r -> r1 <= r2 -> r * r1 <= r * r2.

Lemma CRmult_le_compat_r : forall {R : ConstructiveReals} (r r1 r2:CRcarrier R),
    0 <= r -> r1 <= r2 -> r1 * r <= r2 * r.

Lemma CRmult_pos_pos
  : forall {R : ConstructiveReals} (x y : CRcarrier R),
    0 < x * y -> 0 <= x
    -> 0 <= y -> 0 < x.

Lemma CRmult_pos_appart_zero
  : forall {R : ConstructiveReals} (x y : CRcarrier R),
    0 < x * y -> 0 ≶ x.

Lemma CRmult_le_reg_l :
  forall {R : ConstructiveReals} (x y z : CRcarrier R),
    0 < x -> x * y <= x * z -> y <= z.

Lemma CRmult_le_reg_r :
  forall {R : ConstructiveReals} (x y z : CRcarrier R),
    0 < x -> y * x <= z * x -> y <= z.

Definition CRup_nat {R : ConstructiveReals} (x : CRcarrier R)
  : { n : nat & x < CR_of_Q R (Z.of_nat n #1) }.

Definition CRfloor {R : ConstructiveReals} (a : CRcarrier R)
  : { p : Z & prod (CR_of_Q R (p#1) < a)
                     (a < CR_of_Q R (p#1) + CR_of_Q R 2) }.

Lemma CRplus_appart_reg_l : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    (r + r1) ≶ (r + r2) -> r1 ≶ r2.

Lemma CRplus_appart_reg_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    (r1 + r) ≶ (r2 + r) -> r1 ≶ r2.

Lemma CRmult_appart_reg_l
  : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    0 < r -> (r * r1) ≶ (r * r2) -> r1 ≶ r2.

Lemma CRmult_appart_reg_r
  : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R),
    0 < r -> (r1 * r) ≶ (r2 * r) -> r1 ≶ r2.

Instance CRapart_morph
  : forall {R : ConstructiveReals}, CMorphisms.Proper
      (CMorphisms.respectful (CReq R) (CMorphisms.respectful (CReq R) CRelationClasses.iffT)) (CRapart R).