Library Coq.Reals.ConstructiveRealsMorphisms


Morphisms used to transport results from any instance of ConstructiveReals to any other. Between any two constructive reals structures R1 and R2, all morphisms R1 -> R2 are extensionally equal. We will further show that they exist, and so are isomorphisms. The difference between two morphisms R1 -> R2 is therefore the speed of computation.
The canonical isomorphisms we provide here are often very slow, when a new implementation of constructive reals is added, it should define its own ad hoc isomorphisms for better speed.
Apart from the speed, those unique isomorphisms also serve as sanity checks of the interface ConstructiveReals : it captures a concept with a strong notion of uniqueness.

Require Import QArith.
Require Import Qabs.
Require Import ConstructiveReals.
Require Import ConstructiveCauchyRealsMult.
Require Import ConstructiveRcomplete.

Record ConstructiveRealsMorphism (R1 R2 : ConstructiveReals) : Set :=
  {
    CRmorph : CRcarrier R1 -> CRcarrier R2;
    CRmorph_rat : forall q : Q,
        orderEq _ (CRlt R2) (CRmorph (CR_of_Q R1 q)) (CR_of_Q R2 q);
    CRmorph_increasing : forall x y : CRcarrier R1,
        CRlt R1 x y -> CRlt R2 (CRmorph x) (CRmorph y);
  }.

Lemma CRmorph_increasing_inv
  : forall (R1 R2 : ConstructiveReals)
      (f : ConstructiveRealsMorphism R1 R2)
      (x y : CRcarrier R1),
    CRlt R2 (CRmorph _ _ f x) (CRmorph _ _ f y)
    -> CRlt R1 x y.

Lemma CRmorph_unique : forall (R1 R2 : ConstructiveReals)
                         (f g : ConstructiveRealsMorphism R1 R2)
                         (x : CRcarrier R1),
    orderEq _ (CRlt R2) (CRmorph _ _ f x) (CRmorph _ _ g x).

Lemma Endomorph_id : forall (R : ConstructiveReals) (f : ConstructiveRealsMorphism R R)
                       (x : CRcarrier R),
    orderEq _ (CRlt R) (CRmorph _ _ f x) x.

Lemma CRmorph_proper : forall (R1 R2 : ConstructiveReals)
                         (f : ConstructiveRealsMorphism R1 R2)
                         (x y : CRcarrier R1),
    orderEq _ (CRlt R1) x y
    -> orderEq _ (CRlt R2) (CRmorph _ _ f x) (CRmorph _ _ f y).

Definition CRmorph_compose (R1 R2 R3 : ConstructiveReals)
           (f : ConstructiveRealsMorphism R1 R2)
           (g : ConstructiveRealsMorphism R2 R3)
  : ConstructiveRealsMorphism R1 R3.

Lemma CRmorph_le : forall (R1 R2 : ConstructiveReals)
                     (f : ConstructiveRealsMorphism R1 R2)
                     (x y : CRcarrier R1),
    orderLe _ (CRlt R1) x y
    -> orderLe _ (CRlt R2) (CRmorph _ _ f x) (CRmorph _ _ f y).

Lemma CRmorph_le_inv : forall (R1 R2 : ConstructiveReals)
                         (f : ConstructiveRealsMorphism R1 R2)
                         (x y : CRcarrier R1),
    orderLe _ (CRlt R2) (CRmorph _ _ f x) (CRmorph _ _ f y)
    -> orderLe _ (CRlt R1) x y.

Lemma CRmorph_zero : forall (R1 R2 : ConstructiveReals)
                       (f : ConstructiveRealsMorphism R1 R2),
    orderEq _ (CRlt R2) (CRmorph _ _ f (CRzero R1)) (CRzero R2).

Lemma CRmorph_one : forall (R1 R2 : ConstructiveReals)
                      (f : ConstructiveRealsMorphism R1 R2),
    orderEq _ (CRlt R2) (CRmorph _ _ f (CRone R1)) (CRone R2).

Lemma CRmorph_opp : forall (R1 R2 : ConstructiveReals)
                      (f : ConstructiveRealsMorphism R1 R2)
                      (x : CRcarrier R1),
    orderEq _ (CRlt R2) (CRmorph _ _ f (CRopp R1 x))
            (CRopp R2 (CRmorph _ _ f x)).

Lemma CRplus_pos_rat_lt : forall (R : ConstructiveReals) (x : CRcarrier R) (q : Q),
    Qlt 0 q -> CRlt R x (CRplus R x (CR_of_Q R q)).

Lemma CRplus_neg_rat_lt : forall (R : ConstructiveReals) (x : CRcarrier R) (q : Q),
    Qlt q 0 -> CRlt R (CRplus R x (CR_of_Q R q)) x.

Lemma CRmorph_plus_rat : forall (R1 R2 : ConstructiveReals)
                                (f : ConstructiveRealsMorphism R1 R2)
                                (x : CRcarrier R1) (q : Q),
    orderEq _ (CRlt R2) (CRmorph _ _ f (CRplus R1 x (CR_of_Q R1 q)))
            (CRplus R2 (CRmorph _ _ f x) (CR_of_Q R2 q)).

Lemma CRmorph_plus : forall (R1 R2 : ConstructiveReals)
                            (f : ConstructiveRealsMorphism R1 R2)
                            (x y : CRcarrier R1),
    orderEq _ (CRlt R2) (CRmorph _ _ f (CRplus R1 x y))
            (CRplus R2 (CRmorph _ _ f x) (CRmorph _ _ f y)).

Lemma CRmorph_mult_pos : forall (R1 R2 : ConstructiveReals)
                           (f : ConstructiveRealsMorphism R1 R2)
                           (x : CRcarrier R1) (n : nat),
    orderEq _ (CRlt R2) (CRmorph _ _ f (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1))))
            (CRmult R2 (CRmorph _ _ f x) (CR_of_Q R2 (Z.of_nat n # 1))).

Lemma NatOfZ : forall n : Z, { p : nat | n = Z.of_nat p \/ n = Z.opp (Z.of_nat p) }.

Lemma CRmorph_mult_int : forall (R1 R2 : ConstructiveReals)
                           (f : ConstructiveRealsMorphism R1 R2)
                           (x : CRcarrier R1) (n : Z),
    orderEq _ (CRlt R2) (CRmorph _ _ f (CRmult R1 x (CR_of_Q R1 (n # 1))))
            (CRmult R2 (CRmorph _ _ f x) (CR_of_Q R2 (n # 1))).

Lemma CRmorph_mult_inv : forall (R1 R2 : ConstructiveReals)
                           (f : ConstructiveRealsMorphism R1 R2)
                           (x : CRcarrier R1) (p : positive),
    orderEq _ (CRlt R2) (CRmorph _ _ f (CRmult R1 x (CR_of_Q R1 (1 # p))))
            (CRmult R2 (CRmorph _ _ f x) (CR_of_Q R2 (1 # p))).

Lemma CRmorph_mult_rat : forall (R1 R2 : ConstructiveReals)
                           (f : ConstructiveRealsMorphism R1 R2)
                           (x : CRcarrier R1) (q : Q),
    orderEq _ (CRlt R2) (CRmorph _ _ f (CRmult R1 x (CR_of_Q R1 q)))
            (CRmult R2 (CRmorph _ _ f x) (CR_of_Q R2 q)).

Lemma CRmorph_mult_pos_pos_le : forall (R1 R2 : ConstructiveReals)
                                  (f : ConstructiveRealsMorphism R1 R2)
                                  (x y : CRcarrier R1),
    CRlt R1 (CRzero R1) y
    -> orderLe _ (CRlt R2) (CRmult R2 (CRmorph _ _ f x) (CRmorph _ _ f y))
              (CRmorph _ _ f (CRmult R1 x y)).

Lemma CRmorph_mult_pos_pos : forall (R1 R2 : ConstructiveReals)
                               (f : ConstructiveRealsMorphism R1 R2)
                               (x y : CRcarrier R1),
    CRlt R1 (CRzero R1) y
    -> orderEq _ (CRlt R2) (CRmorph _ _ f (CRmult R1 x y))
              (CRmult R2 (CRmorph _ _ f x) (CRmorph _ _ f y)).

Lemma CRmorph_mult : forall (R1 R2 : ConstructiveReals)
                       (f : ConstructiveRealsMorphism R1 R2)
                       (x y : CRcarrier R1),
    orderEq _ (CRlt R2) (CRmorph _ _ f (CRmult R1 x y))
            (CRmult R2 (CRmorph _ _ f x) (CRmorph _ _ f y)).

Lemma CRmorph_appart : forall (R1 R2 : ConstructiveReals)
                         (f : ConstructiveRealsMorphism R1 R2)
                         (x y : CRcarrier R1)
                         (app : orderAppart _ (CRlt R1) x y),
    orderAppart _ (CRlt R2) (CRmorph _ _ f x) (CRmorph _ _ f y).

Lemma CRmorph_appart_zero : forall (R1 R2 : ConstructiveReals)
                              (f : ConstructiveRealsMorphism R1 R2)
                              (x : CRcarrier R1)
                              (app : orderAppart _ (CRlt R1) x (CRzero R1)),
    orderAppart _ (CRlt R2) (CRmorph _ _ f x) (CRzero R2).

Lemma CRmorph_inv : forall (R1 R2 : ConstructiveReals)
                      (f : ConstructiveRealsMorphism R1 R2)
                      (x : CRcarrier R1)
                      (xnz : orderAppart _ (CRlt R1) x (CRzero R1))
                      (fxnz : orderAppart _ (CRlt R2) (CRmorph _ _ f x) (CRzero R2)),
    orderEq _ (CRlt R2) (CRmorph _ _ f (CRinv R1 x xnz))
            (CRinv R2 (CRmorph _ _ f x) fxnz).

Definition CauchyMorph (R : ConstructiveReals)
  : CReal -> CRcarrier R.

Lemma CauchyMorph_rat : forall (R : ConstructiveReals) (q : Q),
    orderEq _ (CRlt R) (CauchyMorph R (inject_Q q)) (CR_of_Q R q).

Lemma CauchyMorph_increasing_Ql : forall (R : ConstructiveReals) (x : CReal) (q : Q),
    CRealLt x (inject_Q q) -> CRlt R (CauchyMorph R x) (CR_of_Q R q).

Lemma CauchyMorph_increasing_Qr : forall (R : ConstructiveReals) (x : CReal) (q : Q),
    CRealLt (inject_Q q) x -> CRlt R (CR_of_Q R q) (CauchyMorph R x).

Lemma CauchyMorph_increasing : forall (R : ConstructiveReals) (x y : CReal),
    CRealLt x y -> CRlt R (CauchyMorph R x) (CauchyMorph R y).

Definition CauchyMorphism (R : ConstructiveReals) : ConstructiveRealsMorphism CRealImplem R.

Lemma RightBound : forall (R : ConstructiveReals) (x : CRcarrier R) (p q r : Q),
    CRlt R x (CR_of_Q R q)
    -> CRlt R x (CR_of_Q R r)
    -> CRlt R (CR_of_Q R q) (CRplus R x (CR_of_Q R p))
    -> CRlt R (CR_of_Q R r) (CRplus R x (CR_of_Q R p))
    -> Qlt (Qabs (q - r)) p.

Definition CauchyMorph_inv (R : ConstructiveReals)
  : CRcarrier R -> CReal.

Lemma CauchyMorph_inv_rat : forall (R : ConstructiveReals) (q : Q),
    CRealEq (CauchyMorph_inv R (CR_of_Q R q)) (inject_Q q).

Lemma CauchyMorph_inv_increasing_Qr
  : forall (R : ConstructiveReals) (x : CRcarrier R) (q : Q),
    CRlt R (CR_of_Q R q) x -> CRealLt (inject_Q q) (CauchyMorph_inv R x).

Lemma CauchyMorph_inv_increasing : forall (R : ConstructiveReals) (x y : CRcarrier R),
    CRlt R x y -> CRealLt (CauchyMorph_inv R x) (CauchyMorph_inv R y).

Definition CauchyMorphismInv (R : ConstructiveReals)
  : ConstructiveRealsMorphism R CRealImplem.

Lemma CauchyMorph_surject : forall (R : ConstructiveReals) (x : CRcarrier R),
    orderEq _ (CRlt R) (CauchyMorph R (CauchyMorph_inv R x)) x.

Lemma CauchyMorph_inject : forall (R : ConstructiveReals) (x : CReal),
    CRealEq (CauchyMorph_inv R (CauchyMorph R x)) x.

Definition SlowConstructiveRealsMorphism (R1 R2 : ConstructiveReals)
  : ConstructiveRealsMorphism R1 R2
  := CRmorph_compose R1 CRealImplem R2
                     (CauchyMorphismInv R1) (CauchyMorphism R2).