# 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 Qabsq<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<Qabsq

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

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