Library Coq.Reals.Cauchy.ConstructiveCauchyRealsMult

The multiplication and division of Cauchy reals.

WARNING: this file is experimental and likely to change in future releases.

Require Import QArith Qabs Qround Qpower.
Require Import Logic.ConstructiveEpsilon.
Require Export ConstructiveCauchyReals.
Require CMorphisms.
Require Import Lia.
Require Import Lqa.
Require Import QExtra.

Local Open Scope CReal_scope.

Definition CReal_mult_seq (x y : CReal) :=
  (fun n : Z => seq x (n - scale y - 1)%Z
              * seq y (n - scale x - 1)%Z).

Definition CReal_mult_scale (x y : CReal) : Z :=
  x.(scale) + y.(scale).

Local Ltac simplify_Qpower_exponent :=
  match goal with |- context [(_ ^ ?a)%Q] => ring_simplify a end.

Local Ltac simplify_Qabs :=
  match goal with |- context [(Qabs ?a)%Q] => ring_simplify a end.

Local Ltac simplify_Qabs_in H :=
  match type of H with context [(Qabs ?a)%Q] => ring_simplify a in H end.

Local Ltac field_simplify_Qabs :=
  match goal with |- context [(Qabs ?a)%Q] => field_simplify a end.

Local Ltac pose_Qabs_pos :=
  match goal with |- context [(Qabs ?a)%Q] => pose proof Qabs_nonneg a end.

Local Ltac simplify_Qle :=
  match goal with |- (?l <= ?r)%Q => ring_simplify l; ring_simplify r end.

Local Ltac simplify_Qle_in H :=
  match type of H with (?l <= ?r)%Q => ring_simplify l in H; ring_simplify r in H end.

Local Ltac simplify_Qlt :=
  match goal with |- (?l < ?r)%Q => ring_simplify l; ring_simplify r end.

Local Ltac simplify_Qlt_in H :=
  match type of H with (?l < ?r)%Q => ring_simplify l in H; ring_simplify r in H end.

Local Ltac simplify_seq_idx :=
  match goal with |- context [seq ?x ?n] => progress ring_simplify n end.

Local Lemma Weaken_Qle_QpowerAddExp: forall (q : Q) (n m : Z),
    (m >= 0)%Z
-> (q <= 2^n)%Q
-> (q <= 2^(n +m ))%Q.

Local Lemma Weaken_Qle_QpowerRemSubExp: forall (q : Q) (n m : Z),
    (m >= 0)%Z
-> (q <= 2^(n -m ))%Q
-> (q <= 2^n)%Q.

Local Lemma Weaken_Qle_QpowerFac: forall (q r : Q) (n : Z),
    (r >= 1)%Q
-> (q <= 2^n)%Q
-> (q <= r * 2^n)%Q.

Lemma CReal_mult_cauchy: forall (x y : CReal),
  QCauchySeq (CReal_mult_seq x y).

Lemma CReal_mult_bound : forall (x y : CReal),
  QBound (CReal_mult_seq x y) (CReal_mult_scale x y).

Definition CReal_mult (x y : CReal) : CReal :=
{|
  seq := CReal_mult_seq x y;
  scale := CReal_mult_scale x y;
  cauchy := CReal_mult_cauchy x y;
  bound := CReal_mult_bound x y
|}.

Infix "*" := CReal_mult : CReal_scope.

Lemma CReal_mult_comm : forall x y : CReal, x * y == y * x.

Lemma CReal_red_scale: forall (a : Z -> Q) (b : Z) (c : QCauchySeq a) (d : QBound a b),
  scale (mkCReal a b c d) = b.

Lemma CReal_mult_proper_0_l : forall x y : CReal,
    y == 0 -> x * y == 0.

Lemma CReal_mult_0_r : forall r, r * 0 == 0.

Lemma CReal_mult_0_l : forall r, 0 * r == 0.

Lemma CReal_scale_sep0_limit : forall (x : CReal) (n : Z),
    (2 * (2^n)%Q < seq x n)%Q
-> (n <= scale x - 2)%Z.

Lemma CReal_mult_lt_0_compat_correct
  : forall (x y : CReal) (Hx : 0 < x) (Hy : 0 < y),
    (2 * 2^(proj1_sig Hx + proj1_sig Hy - 1)%Z <
     seq (x * y)%CReal (proj1_sig Hx + proj1_sig Hy - 1)%Z -
     seq (inject_Q 0) (proj1_sig Hx + proj1_sig Hy - 1)%Z)%Q.

Definition CReal_mult_lt_0_compat : forall x y : CReal,
    0 < x -> 0 < y -> 0 < x * y
  := fun x y Hx Hy => exist _ (proj1_sig Hx + proj1_sig Hy - 1)%Z
                        (CReal_mult_lt_0_compat_correct
                           x y Hx Hy).

Lemma CReal_mult_plus_distr_l : forall r1 r2 r3 : CReal,
    r1 * (r2 + r3 ) == (r1 * r2 ) + (r1 * r3 ).

Lemma CReal_mult_plus_distr_r : forall r1 r2 r3 : CReal,
    (r2 + r3 ) * r1 == (r2 * r1 ) + (r3 * r1 ).

Lemma CReal_opp_mult_distr_r
  : forall r1 r2 : CReal, - (r1 * r2 ) == r1 * (- r2 ).

Lemma CReal_mult_proper_l : forall x y z : CReal,
    y == z -> x * y == x * z.

Lemma CReal_mult_proper_r : forall x y z : CReal,
    y == z -> y * x == z * x.

Lemma CReal_mult_assoc : forall x y z : CReal,
  (x * y ) * z == x * (y * z ).

Lemma CReal_mult_1_l : forall r: CReal,
  1 * r == r.

Lemma CReal_isRingExt : ring_eq_ext CReal_plus CReal_mult CReal_opp CRealEq.

Lemma CReal_isRing : ring_theory (inject_Q 0) (inject_Q 1)
                                 CReal_plus CReal_mult
                                 CReal_minus CReal_opp
                                 CRealEq.

Add Parametric Morphism : CReal_mult
    with signature CRealEq ==> CRealEq ==> CRealEq
      as CReal_mult_morph.

#[global]
Instance CReal_mult_morph_T
  : CMorphisms.Proper
      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRealEq)) CReal_mult.

Add Parametric Morphism : CReal_opp
    with signature CRealEq ==> CRealEq
      as CReal_opp_morph.

#[global]
Instance CReal_opp_morph_T
  : CMorphisms.Proper
      (CMorphisms.respectful CRealEq CRealEq) CReal_opp.

Add Parametric Morphism : CReal_minus
    with signature CRealEq ==> CRealEq ==> CRealEq
      as CReal_minus_morph.

#[global]
Instance CReal_minus_morph_T
  : CMorphisms.Proper
      (CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRealEq)) CReal_minus.

Add Ring CRealRing : CReal_isRing.

Lemma CReal_mult_1_r : forall r, r * 1 == r.

Lemma CReal_opp_mult_distr_l
  : forall r1 r2 : CReal, - (r1 * r2 ) == (- r1 ) * r2.

Lemma CReal_mult_lt_compat_l : forall x y z : CReal,
    0 < x -> y < z -> x *y < x *z.

Lemma CReal_mult_lt_compat_r : forall x y z : CReal,
    0 < x -> y < z -> y *x < z *x.

Lemma CReal_mult_eq_reg_l : forall (r r1 r2 : CReal),
    r # 0
    -> r * r1 == r * r2
    -> r1 == r2.

Lemma CReal_abs_appart_zero : forall (x : CReal) (n : Z),
    (2*2^n < Qabs (seq x n))%Q
    -> 0 # x.

Field

Lemma CRealArchimedean
  : forall x:CReal, { n :Z & x < inject_Z n < x +2 }.

Definition CRealLowerBound (x : CReal) (xPos : 0<x) : Z :=
  proj1_sig (xPos).

Lemma CRealLowerBoundSpec: forall (x : CReal) (xPos : 0<x),
    forall p : Z, (p <= (CRealLowerBound x xPos ))%Z
-> (seq x p > 2^(CRealLowerBound x xPos ))%Q.

Lemma CRealLowerBound_lt_scale: forall (r : CReal) (Hrpos : 0 < r),
    (CRealLowerBound r Hrpos < scale r)%Z.

Note on the convergence modulus for x when computing 1/x: Thinking in terms of absolute and relative errors and scales we get:

2^n is absolute error of 1/x (the requested error)
2^k is a lower bound of x -> 2^-k is an upper bound of 1/x

For simplicity lets’ say 2^k is the scale of x and 2^-k is the scale of 1/x.

With this we get:

relative error of 1/x = absolute error of 1/x / scale of 1/x = 2^n / 2^-k = 2^(n+k)
1/x maintains relative error
relative error of x = relative error 1/x = 2^(n+k)
absolute error of x = relative error x * scale of x = 2^(n+k) * 2^k
absolute error of x = 2^(n+2*k)

Definition CReal_inv_pos_cm (x : CReal) (xPos : 0 < x) (n : Z):=
  (Z.min (CRealLowerBound x xPos) (n + 2 * (CRealLowerBound x xPos )))%Z.

Definition CReal_inv_pos_seq (x : CReal) (xPos : 0 < x) (n : Z) :=
  (/ seq x (CReal_inv_pos_cm x xPos n))%Q.

Definition CReal_inv_pos_scale (x : CReal) (xPos : 0 < x) : Z :=
  (- (CRealLowerBound x xPos ))%Z.

Lemma CReal_inv_pos_cauchy: forall (x : CReal) (xPos : 0 < x),
    QCauchySeq (CReal_inv_pos_seq x xPos).

Lemma CReal_inv_pos_bound : forall (x : CReal) (Hxpos : 0 < x),
  QBound (CReal_inv_pos_seq x Hxpos) (CReal_inv_pos_scale x Hxpos).

Definition CReal_inv_pos (x : CReal) (Hxpos : 0 < x) : CReal :=
{|
  seq := CReal_inv_pos_seq x Hxpos;
  scale := CReal_inv_pos_scale x Hxpos;
  cauchy := CReal_inv_pos_cauchy x Hxpos;
  bound := CReal_inv_pos_bound x Hxpos
|}.

Definition CReal_neg_lt_pos : forall x : CReal, x < 0 -> 0 < -x.

Definition CReal_inv (x : CReal) (xnz : x # 0) : CReal
  := match xnz with
     | inl xNeg => - CReal_inv_pos (-x) (CReal_neg_lt_pos x xNeg)
     | inr xPos => CReal_inv_pos x xPos
     end.

Notation "/ x" := (CReal_inv x) (at level 35, right associativity) : CReal_scope.

Lemma CReal_inv_0_lt_compat
  : forall (r : CReal) (rnz : r # 0),
    0 < r -> 0 < ((/ r ) rnz ).

Lemma CReal_inv_l_pos : forall (r:CReal) (Hrpos : 0 < r),
    (CReal_inv_pos r Hrpos ) * r == 1.

Lemma CReal_inv_l : forall (r:CReal) (rnz : r # 0),
        ((/ r ) rnz ) * r == 1.

Lemma CReal_inv_r : forall (r:CReal) (rnz : r # 0),
    r * ((/ r ) rnz ) == 1.

Lemma CReal_inv_1 : forall nz : 1 # 0, (/ 1) nz == 1.

Lemma CReal_inv_mult_distr :
  forall r1 r2 (r1nz : r1 # 0) (r2nz : r2 # 0) (rmnz : (r1 *r2 ) # 0),
    (/ (r1 * r2 )) rmnz == (/ r1 ) r1nz * (/ r2 ) r2nz.

Lemma Rinv_eq_compat : forall x y (rxnz : x # 0) (rynz : y # 0),
    x == y
    -> (/ x ) rxnz == (/ y ) rynz.

Lemma CReal_mult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.

Lemma CReal_mult_lt_reg_r : forall r r1 r2, 0 < r -> r1 * r < r2 * r -> r1 < r2.

Lemma CReal_mult_eq_reg_r : forall r r1 r2, r1 * r == r2 * r -> r # 0 -> r1 == r2.

Lemma CReal_mult_eq_compat_l : forall r r1 r2, r1 == r2 -> r * r1 == r * r2.

Lemma CReal_mult_eq_compat_r : forall r r1 r2, r1 == r2 -> r1 * r == r2 * r.

Lemma CReal_mult_pos_appart_zero : forall x y : CReal, 0 < x * y -> 0 # x.

Fixpoint pow (r:CReal) (n:nat) : CReal :=
  match n with
    | O => 1
    | S n => r * (pow r n )
  end.

Lemma CReal_mult_le_compat_l_half : forall r r1 r2,
    0 < r -> r1 <= r2 -> r * r1 <= r * r2.

Lemma CReal_invQ : forall (b : positive) (pos : Qlt 0 (Z.pos b # 1)),
    CReal_inv (inject_Q (Z.pos b # 1)) (inr (CReal_injectQPos (Z.pos b # 1) pos))
    == inject_Q (1 # b).

Definition CRealQ_dense (a b : CReal)
  : a < b -> { q : Q & a < inject_Q q < b }.

Lemma inject_Q_mult : forall q r : Q,
    inject_Q (q * r) == inject_Q q * inject_Q r.

Definition Rup_nat (x : CReal)
  : { n : nat & x < inject_Q (Z.of_nat n #1) }.

Lemma CReal_mult_le_0_compat : forall (a b : CReal),
    0 <= a -> 0 <= b -> 0 <= a * b.

Lemma CReal_mult_le_compat_l : forall (r r1 r2:CReal),
    0 <= r -> r1 <= r2 -> r * r1 <= r * r2.

Lemma CReal_mult_le_compat_r : forall (r r1 r2:CReal),
    0 <= r -> r1 <= r2 -> r1 * r <= r2 * r.

Lemma CReal_mult_le_reg_l :
  forall x y z : CReal,
    0 < x -> x * y <= x * z -> y <= z.

Lemma CReal_mult_le_reg_r :
  forall x y z : CReal,
    0 < x -> y * x <= z * x -> y <= z.