Library Coq.Reals.ConstructiveReals


An interface for constructive and computable real numbers. All of its instances are isomorphic (see file ConstructiveRealsMorphisms). For example it contains the Cauchy reals implemented in file ConstructivecauchyReals and 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.

Require Import QArith.

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).

Definition orderEq (X : Set) (Xlt : X -> X -> Set) (x y : X) : Prop
  := (Xlt x y -> False) /\ (Xlt y x -> False).

Definition orderAppart (X : Set) (Xlt : X -> X -> Set) (x y : X) : Set
  := Xlt x y + Xlt y x.

Definition orderLe (X : Set) (Xlt : X -> X -> Set) (x y : X) : Prop
  := Xlt y x -> False.

Definition sig_forall_dec_T : Type
  := forall (P : nat -> Prop), (forall n, {P n} + {~P n})
                   -> {n | ~P n} + {forall n, P n}.

Definition sig_not_dec_T : Type := forall P : Prop, { ~~P } + { ~P }.

Record ConstructiveReals : Type :=
  {
    CRcarrier : Set;

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

    
    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;

    
    CRzero : CRcarrier;
    CRone : CRcarrier;

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

    CRisRing : ring_theory CRzero CRone CRplus CRmult
                          (fun x y => CRplus x (CRopp y)) CRopp (orderEq CRcarrier CRlt);
    CRisRingExt : ring_eq_ext CRplus CRmult CRopp (orderEq CRcarrier CRlt);

    
    CRzero_lt_one : CRlt CRzero CRone;
    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 CRzero x -> CRlt CRzero y -> CRlt CRzero (CRmult x y);

    
    CRinv : forall x : CRcarrier, orderAppart _ CRlt x CRzero -> CRcarrier;
    CRinv_l : forall (r:CRcarrier) (rnz : orderAppart _ CRlt r CRzero),
        orderEq _ CRlt (CRmult (CRinv r rnz) r) CRone;
    CRinv_0_lt_compat : forall (r : CRcarrier) (rnz : orderAppart _ CRlt r CRzero),
        CRlt CRzero r -> CRlt CRzero (CRinv r rnz);

    
    CR_of_Q : Q -> CRcarrier;
    CR_of_Q_plus : forall q r : Q, orderEq _ CRlt (CR_of_Q (q+r))
                                           (CRplus (CR_of_Q q) (CR_of_Q r));
    CR_of_Q_mult : forall q r : Q, orderEq _ CRlt (CR_of_Q (q*r))
                                           (CRmult (CR_of_Q q) (CR_of_Q r));
    CR_of_Q_one : orderEq _ CRlt (CR_of_Q 1) CRone;
    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;

    
    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);

    
    CR_cv (un : nat -> CRcarrier) (l : CRcarrier) : Set
    := forall p:positive,
        { n : nat | forall i:nat, le n i
                           -> orderLe _ CRlt (CR_of_Q (-1#p)) (CRminus (un i) l)
                             /\ orderLe _ CRlt (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
                             -> orderLe _ CRlt (CR_of_Q (-1#p)) (CRminus (un i) (un j))
                               /\ orderLe _ CRlt (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 };
  }.

Lemma CRlt_asym : forall (R : ConstructiveReals) (x y : CRcarrier R),
    CRlt R x y -> CRlt R y x -> False.

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

Lemma CRle_refl : forall (R : ConstructiveReals) (x : CRcarrier R),
    CRlt R x x -> False.

Lemma CRle_lt_trans : forall (R : ConstructiveReals) (r1 r2 r3 : CRcarrier R),
    (CRlt R r2 r1 -> False) -> CRlt R r2 r3 -> CRlt R r1 r3.

Lemma CRlt_le_trans : forall (R : ConstructiveReals) (r1 r2 r3 : CRcarrier R),
    CRlt R r1 r2 -> (CRlt R r3 r2 -> False) -> CRlt R r1 r3.

Lemma CRle_trans : forall (R : ConstructiveReals) (x y z : CRcarrier R),
    orderLe _ (CRlt R) x y -> orderLe _ (CRlt R) y z -> orderLe _ (CRlt R) x z.

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

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

Lemma CReq_refl : forall (R : ConstructiveReals) (x : CRcarrier R),
    orderEq _ (CRlt R) x x.

Lemma CReq_sym : forall (R : ConstructiveReals) (x y : CRcarrier R),
    orderEq _ (CRlt R) x y
    -> orderEq _ (CRlt R) y x.

Lemma CReq_trans : forall (R : ConstructiveReals) (x y z : CRcarrier R),
    orderEq _ (CRlt R) x y
    -> orderEq _ (CRlt R) y z
    -> orderEq _ (CRlt R) x z.

Lemma CR_setoid : forall R : ConstructiveReals,
    Setoid_Theory (CRcarrier R) (orderEq _ (CRlt R)).

Lemma CRplus_0_r : forall (R : ConstructiveReals) (x : CRcarrier R),
    orderEq _ (CRlt R) (CRplus R x (CRzero R)) x.

Lemma CRmult_1_r : forall (R : ConstructiveReals) (x : CRcarrier R),
    orderEq _ (CRlt R) (CRmult R x (CRone R)) x.

Lemma CRplus_opp_l : forall (R : ConstructiveReals) (x : CRcarrier R),
    orderEq _ (CRlt R) (CRplus R (CRopp R x) x) (CRzero R).

Lemma CRplus_lt_compat_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R),
    CRlt R r1 r2 -> CRlt R (CRplus R r1 r) (CRplus R r2 r).

Lemma CRplus_lt_reg_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R),
    CRlt R (CRplus R r1 r) (CRplus R r2 r) -> CRlt R r1 r2.

Lemma CRplus_le_compat_l : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R),
    orderLe _ (CRlt R) r1 r2
    -> orderLe _ (CRlt R) (CRplus R r r1) (CRplus R r r2).

Lemma CRplus_le_compat_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R),
    orderLe _ (CRlt R) r1 r2
    -> orderLe _ (CRlt R) (CRplus R r1 r) (CRplus R r2 r).

Lemma CRplus_le_reg_l : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R),
    orderLe _ (CRlt R) (CRplus R r r1) (CRplus R r r2)
    -> orderLe _ (CRlt R) r1 r2.

Lemma CRplus_le_reg_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R),
    orderLe _ (CRlt R) (CRplus R r1 r) (CRplus R r2 r)
    -> orderLe _ (CRlt R) r1 r2.

Lemma CRplus_lt_le_compat :
  forall (R : ConstructiveReals) (r1 r2 r3 r4 : CRcarrier R),
    CRlt R r1 r2
    -> (CRlt R r4 r3 -> False)
    -> CRlt R (CRplus R r1 r3) (CRplus R r2 r4).

Lemma CRplus_eq_reg_l : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R),
    orderEq _ (CRlt R) (CRplus R r r1) (CRplus R r r2)
    -> orderEq _ (CRlt R) r1 r2.

Lemma CRplus_eq_reg_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R),
    orderEq _ (CRlt R) (CRplus R r1 r) (CRplus R r2 r)
    -> orderEq _ (CRlt R) r1 r2.

Lemma CRopp_involutive : forall (R : ConstructiveReals) (r : CRcarrier R),
    orderEq _ (CRlt R) (CRopp R (CRopp R r)) r.

Lemma CRopp_gt_lt_contravar
  : forall (R : ConstructiveReals) (r1 r2 : CRcarrier R),
    CRlt R r2 r1 -> CRlt R (CRopp R r1) (CRopp R r2).

Lemma CRopp_lt_cancel : forall (R : ConstructiveReals) (r1 r2 : CRcarrier R),
    CRlt R (CRopp R r2) (CRopp R r1) -> CRlt R r1 r2.

Lemma CRopp_plus_distr : forall (R : ConstructiveReals) (r1 r2 : CRcarrier R),
    orderEq _ (CRlt R) (CRopp R (CRplus R r1 r2)) (CRplus R (CRopp R r1) (CRopp R r2)).

Lemma CRmult_plus_distr_l : forall (R : ConstructiveReals) (r1 r2 r3 : CRcarrier R),
    orderEq _ (CRlt R) (CRmult R r1 (CRplus R r2 r3))
            (CRplus R (CRmult R r1 r2) (CRmult R r1 r3)).

Lemma CRzero_double : forall (R : ConstructiveReals) (x : CRcarrier R),
    orderEq _ (CRlt R) x (CRplus R x x)
    -> orderEq _ (CRlt R) x (CRzero R).

Lemma CRmult_0_r : forall (R : ConstructiveReals) (x : CRcarrier R),
    orderEq _ (CRlt R) (CRmult R x (CRzero R)) (CRzero R).

Lemma CRopp_mult_distr_r : forall (R : ConstructiveReals) (r1 r2 : CRcarrier R),
    orderEq _ (CRlt R) (CRopp R (CRmult R r1 r2))
            (CRmult R r1 (CRopp R r2)).

Lemma CRopp_mult_distr_l : forall (R : ConstructiveReals) (r1 r2 : CRcarrier R),
    orderEq _ (CRlt R) (CRopp R (CRmult R r1 r2))
            (CRmult R (CRopp R r1) r2).

Lemma CRmult_lt_compat_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R),
    CRlt R (CRzero R) r
    -> CRlt R r1 r2
    -> CRlt R (CRmult R r1 r) (CRmult R r2 r).

Lemma CRinv_r : forall (R : ConstructiveReals) (r:CRcarrier R)
                  (rnz : orderAppart _ (CRlt R) r (CRzero R)),
    orderEq _ (CRlt R) (CRmult R r (CRinv R r rnz)) (CRone R).

Lemma CRmult_lt_reg_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R),
    CRlt R (CRzero R) r
    -> CRlt R (CRmult R r1 r) (CRmult R r2 r)
    -> CRlt R r1 r2.

Lemma CRmult_lt_reg_l : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R),
    CRlt R (CRzero R) r
    -> CRlt R (CRmult R r r1) (CRmult R r r2)
    -> CRlt R r1 r2.

Lemma CRmult_le_compat_l : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R),
    CRlt R (CRzero R) r
    -> orderLe _ (CRlt R) r1 r2
    -> orderLe _ (CRlt R) (CRmult R r r1) (CRmult R r r2).

Lemma CRmult_le_compat_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R),
    CRlt R (CRzero R) r
    -> orderLe _ (CRlt R) r1 r2
    -> orderLe _ (CRlt R) (CRmult R r1 r) (CRmult R r2 r).

Lemma CRmult_eq_reg_r : forall (R : ConstructiveReals) (r r1 r2 : CRcarrier R),
    orderAppart _ (CRlt R) (CRzero R) r
    -> orderEq _ (CRlt R) (CRmult R r1 r) (CRmult R r2 r)
    -> orderEq _ (CRlt R) r1 r2.

Lemma CR_of_Q_proper : forall (R : ConstructiveReals) (q r : Q),
    q == r -> orderEq _ (CRlt R) (CR_of_Q R q) (CR_of_Q R r).

Lemma CR_of_Q_zero : forall (R : ConstructiveReals),
    orderEq _ (CRlt R) (CR_of_Q R 0) (CRzero R).

Lemma CR_of_Q_opp : forall (R : ConstructiveReals) (q : Q),
    orderEq _ (CRlt R) (CR_of_Q R (-q)) (CRopp R (CR_of_Q R q)).

Lemma CR_of_Q_le : forall (R : ConstructiveReals) (r q : Q),
    Qle r q
    -> orderLe _ (CRlt R) (CR_of_Q R r) (CR_of_Q R q).

Lemma CR_of_Q_pos : forall (R : ConstructiveReals) (q:Q),
    Qlt 0 q -> CRlt R (CRzero R) (CR_of_Q R q).

Lemma CR_cv_above_rat
  : forall (R : ConstructiveReals) (xn : nat -> Q) (x : CRcarrier R) (q : Q),
    CR_cv R (fun n : nat => CR_of_Q R (xn n)) x
    -> CRlt R (CR_of_Q R q) x
    -> { n : nat | forall p:nat, le n p -> Qlt q (xn p) }.

Lemma CR_cv_below_rat
  : forall (R : ConstructiveReals) (xn : nat -> Q) (x : CRcarrier R) (q : Q),
    CR_cv R (fun n : nat => CR_of_Q R (xn n)) x
    -> CRlt R x (CR_of_Q R q)
    -> { n : nat | forall p:nat, le n p -> Qlt (xn p) q }.

Lemma CR_cv_const : forall (R : ConstructiveReals) (x y : CRcarrier R),
    CR_cv R (fun _ => x) y -> orderEq _ (CRlt R) x y.