Library Coq.Reals.Cauchy.QExtra

Require Import QArith.
Require Import Qpower.
Require Import Qabs.
Require Import Qround.
Require Import Lia.
Require Import Lqa. Require Import PosExtra.

Lemmas on Q numerator denominator operations

Lemma Q_factorDenom : forall (a:Z) (b d:positive), (a # (d * b )) == (1#d ) * (a #b ).

Lemma Q_factorNum_l : forall (a b : Z) (c : positive),
  (a *b # c == (a # 1) * (b # c ))%Q.

Lemma Q_factorNum : forall (a : Z) (b : positive),
  (a # b == (a # 1) * (1 # b ))%Q.

Lemma Q_reduce_fl : forall (a b : positive),
  (Z.pos a # a * b == (1 # b ))%Q.

Lemmas on Q comparison

Lemma Qle_neq: forall p q : Q, p < q <-> p <= q /\ ~ (p == q ).

Lemma Qplus_lt_compat : forall x y z t : Q,
(x < y)%Q -> (z < t)%Q -> (x + z < y + t)%Q.

Lemma Qgt_lt: forall p q : Q, p > q -> q < p.

Lemma Qlt_gt: forall p q : Q, p < q -> q > p.

Notation "x <= y < z" := (x<=y/\y<z) : Q_scope.
Notation "x < y <= z" := (x<y/\y<=z) : Q_scope.
Notation "x < y < z" := (x<y/\y<z) : Q_scope.

Lemmas on Qmult

Lemma Qmult_lt_0_compat : forall a b : Q,
    0 < a
-> 0 < b
-> 0 < a * b.

Lemma Qmult_lt_1_compat:
  forall a b : Q, (1 < a)%Q -> (1 < b)%Q -> (1 < a * b)%Q.

Lemma Qmult_le_1_compat:
  forall a b : Q, (1 <= a)%Q -> (1 <= b)%Q -> (1 <= a * b)%Q.

Lemma Qmult_lt_compat_nonneg: forall x y z t : Q,
  (0 <= x < y)%Q -> (0 <= z < t)%Q -> (x * z < y * t)%Q.

Lemma Qmult_lt_le_compat_nonneg: forall x y z t : Q,
  (0 < x <= y)%Q -> (0 < z < t)%Q -> (x * z < y * t)%Q.

Lemma Qmult_le_compat_nonneg: forall x y z t : Q,
  (0 <= x <= y)%Q -> (0 <= z <= t)%Q -> (x * z <= y * t)%Q.

Lemmas on Qinv

Lemma Qinv_swap_pos: forall (a b : positive),
Z.pos a # b == / (Z.pos b # a ).

Lemma Qinv_swap_neg: forall (a b : positive),
Z.neg a # b == / (Z.neg b # a ).

Lemmas on Qabs

Lemma Qabs_Qlt_condition: forall x y : Q,
Qabs x < y <-> -y < x < y.

Lemma Qabs_gt: forall r s : Q,
(r < s)%Q -> (r < Qabs s)%Q.

Lemmas on Qpower

Lemma Qpower_0_r: forall q:Q,
  q ^0 == 1.

Lemma Qpower_1_r: forall q:Q,
  q ^1 == q.

Lemma Qpower_not_0: forall (a : Q) (z : Z),
  ~ a == 0 -> ~ Qpower a z == 0.

Lemma Qpower_pos_lt: forall (a : Q) (z : Z),
  a > 0 -> Qpower a z > 0.

Lemma Qpower_minus: forall (a : Q) (n m : Z),
  ~ a == 0 -> a ^ (n - m ) == a ^ n / a ^ m.

Lemma Qpower_minus_pos: forall (a b : positive) (n m : Z),
  (Z.pos a #b ) ^ (n - m ) == (Z.pos a #b ) ^ n * (Z.pos b #a ) ^ m.

Lemma Qpower_minus_neg: forall (a b : positive) (n m : Z),
  (Z.neg a #b ) ^ (n - m ) == (Z.neg a #b ) ^ n * (Z.neg b #a ) ^ m.

Lemma Qpower_lt_1_increasing:
  forall (q : Q) (n : positive), (1<q)%Q -> (1 < q ^ (Z.pos n ))%Q.

Lemma Qpower_lt_1_increasing':
  forall (q : Q) (n : Z), (1<q)%Q -> (0<n)%Z -> (1 < q ^ n)%Q.

Lemma Qzero_eq: forall (d : positive),
  (0#d == 0)%Q.

Lemma Qpower_le_1_increasing:
  forall (q : Q) (n : positive), (1<=q)%Q -> (1 <= q ^ (Z.pos n ))%Q.

Lemma Qpower_le_1_increasing':
  forall (q : Q) (n : Z), (1<=q)%Q -> (0<=n)%Z -> (1 <= q ^ n)%Q.

Lemma Qpower_lt_compat:
  forall (q : Q) (n m : Z), (n < m)%Z -> (1<q)%Q -> (q ^ n < q ^ m)%Q.

Lemma Qpower_le_compat:
  forall (q : Q) (n m : Z), (n <= m)%Z -> (1<=q)%Q -> (q ^ n <= q ^ m)%Q.

Lemma Qpower_lt_compat_inv:
  forall (q : Q) (n m : Z), (q ^ n < q ^ m)%Q -> (1<q)%Q -> (n < m)%Z.

Lemma Qpower_le_compat_inv:
  forall (q : Q) (n m : Z), (q ^ n <= q ^ m)%Q -> (1<q)%Q -> (n <= m)%Z.

Lemma Qpower_decomp': forall (p : positive) (a : Z) (b : positive),
  (a # b ) ^ (Z.pos p ) == a ^ (Z.pos p ) # (b ^ p)%positive.

Power of 2 open and closed upper and lower bounds for q : Q

Lemma QarchimedeanExp2_Pos : forall q : Q,
  {p : positive | (q < Z.pos (2^p) # 1)%Q}.

Fixpoint Pos_log2floor_plus1 (p : positive) : positive :=
  match p with
  | (p'~1)%positive => Pos.succ (Pos_log2floor_plus1 p')
  | (p'~0)%positive => Pos.succ (Pos_log2floor_plus1 p')
  | 1%positive => 1
  end.

Lemma Pos_log2floor_plus1_spec : forall (p : positive),
  (Pos.pow 2 (Pos_log2floor_plus1 p) <= 2 * p < 2 * Pos.pow 2 (Pos_log2floor_plus1 p))%positive.

Fixpoint Pos_log2ceil_plus1 (p : positive) : positive :=
  match p with
  | (p'~1)%positive => Pos.succ (Pos.succ (Pos_log2floor_plus1 p'))
  | (p'~0)%positive => Pos.succ (Pos_log2ceil_plus1 p')
  | 1%positive => 1
  end.

Lemma Pos_log2ceil_plus1_spec : forall (p : positive),
  (Pos.pow 2 (Pos_log2ceil_plus1 p) < 4 * p <= 2 * Pos.pow 2 (Pos_log2ceil_plus1 p))%positive.

Fixpoint Pos_is_pow2 (p : positive) : bool :=
  match p with
  | (p'~1)%positive => false
  | (p'~0)%positive => Pos_is_pow2 p'
  | 1%positive => true
  end.

Power of two closed upper bound q <= 2^z

Definition Qbound_le_ZExp2 (q : Q) : Z :=
  match Qnum q with

  | Z0 => -1000
  | Zneg p => 0
  | Zpos p => (Z.pos (Pos_log2ceil_plus1 p) - Z.pos (Pos_log2floor_plus1 (Qden q)))%Z
  end.

Lemma Qbound_le_ZExp2_spec : forall (q : Q),
  (q <= 2^(Qbound_le_ZExp2 q ))%Q.

Definition Qbound_leabs_ZExp2 (q : Q) : Z := Qbound_le_ZExp2 (Qabs q).

Lemma Qbound_leabs_ZExp2_spec : forall (q : Q),
  (Qabs q <= 2^(Qbound_leabs_ZExp2 q ))%Q.

Power of two open upper bound q < 2^z and Qabs q < 2^z

Compute a z such that q<2^z. z shall be close to as small as possible, but we need a compromise between the tighness of the bound and the computation speed and proof complexity. Looking just at the log2 of the numerator and denominator, this is a tight bound except when the numerator is a power of 2 and the denomintor is not. E.g. this return 4/5 < 2^1 instead of 4/5< 2^0. If q==0, we return -1000, because as binary integer this has just 10 bits but 2^-1000 should be smaller than almost any number in practice. If numbers are much smaller, computations might be inefficient.

Definition Qbound_lt_ZExp2 (q : Q) : Z :=
  match Qnum q with

  | Z0 => -1000
  | Zneg p => 0
  | Zpos p => Z.pos_sub (Pos.succ (Pos_log2floor_plus1 p)) (Pos_log2floor_plus1 (Qden q))
  end.

Remark Qbound_lt_ZExp2_test_1 : Qbound_lt_ZExp2 (4#4) = 1%Z.
Remark Qbound_lt_ZExp2_test_2 : Qbound_lt_ZExp2 (5#4) = 1%Z.
Remark Qbound_lt_ZExp2_test_3 : Qbound_lt_ZExp2 (4#5) = 1%Z.
Remark Qbound_lt_ZExp2_test_4 : Qbound_lt_ZExp2 (7#5) = 1%Z.

Lemma Qbound_lt_ZExp2_spec : forall (q : Q),
  (q < 2^(Qbound_lt_ZExp2 q ))%Q.

Definition Qbound_ltabs_ZExp2 (q : Q) : Z := Qbound_lt_ZExp2 (Qabs q).

Lemma Qbound_ltabs_ZExp2_spec : forall (q : Q),
  (Qabs q < 2^(Qbound_ltabs_ZExp2 q ))%Q.

Power of 2 open lower bounds for 2^z < q and 2^z < Qabs q

Note: the -2 is required cause of the Qlt limit. In case q is a power of two, the lower and upper bound must be a factor of 4 apart

Definition Qlowbound_ltabs_ZExp2 (q : Q) : Z := -2 + Qbound_ltabs_ZExp2 q.

Lemma Qlowbound_ltabs_ZExp2_inv: forall q : Q,
    q > 0
-> Qlowbound_ltabs_ZExp2 q = (- Qbound_ltabs_ZExp2 (/q))%Z.

Lemma Qlowbound_ltabs_ZExp2_opp: forall q : Q,
  (Qlowbound_ltabs_ZExp2 q = Qlowbound_ltabs_ZExp2 (-q))%Z.

Lemma Qlowbound_lt_ZExp2_spec : forall (q : Q) (Hqgt0 : q > 0),
  (2^(Qlowbound_ltabs_ZExp2 q ) < q)%Q.

Lemma Qlowbound_ltabs_ZExp2_spec : forall (q : Q) (Hqgt0 : ~ q == 0),
  (2^(Qlowbound_ltabs_ZExp2 q ) < Qabs q)%Q.

Existential formulations of power of 2 lower and upper bounds

Definition QarchimedeanExp2_Z (q : Q)
  : {z : Z | (q < 2^z)%Q}
  := exist _ (Qbound_lt_ZExp2 q) (Qbound_lt_ZExp2_spec q).

Definition QarchimedeanAbsExp2_Z (q : Q)
  : {z : Z | (Qabs q < 2^z)%Q}
  := exist _ (Qbound_ltabs_ZExp2 q) (Qbound_ltabs_ZExp2_spec q).

Definition QarchimedeanLowExp2_Z (q : Q) (Hqgt0 : q > 0)
  : {z : Z | (2^z < q)%Q}
  := exist _ (Qlowbound_ltabs_ZExp2 q) (Qlowbound_lt_ZExp2_spec q Hqgt0).

Definition QarchimedeanLowAbsExp2_Z (q : Q) (Hqgt0 : ~ q == 0)
  : {z : Z | (2^z < Qabs q)%Q}
  := exist _ (Qlowbound_ltabs_ZExp2 q) (Qlowbound_ltabs_ZExp2_spec q Hqgt0).