Library Stdlib.Reals.Cauchy.QExtra

From Stdlib Require Import QArith.
From Stdlib Require Import Qpower.
From Stdlib Require Import Qabs.
From Stdlib Require Import Qround.
From Stdlib Require Import Zorder.
From Stdlib Require Import Lia.
From Stdlib Require Import Lqa. From Stdlib Require Import PosExtra.

Power of 2 open and closed upper and lower bounds for q : 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).