diff options
Diffstat (limited to 'theories/Reals/Cauchy/QExtra.v')
| -rw-r--r-- | theories/Reals/Cauchy/QExtra.v | 637 |
1 files changed, 637 insertions, 0 deletions
diff --git a/theories/Reals/Cauchy/QExtra.v b/theories/Reals/Cauchy/QExtra.v new file mode 100644 index 0000000000..8b39c056e4 --- /dev/null +++ b/theories/Reals/Cauchy/QExtra.v @@ -0,0 +1,637 @@ +Require Import QArith. +Require Import Qpower. +Require Import Qabs. +Require Import Qround. +Require Import Lia. +Require Import Lqa. (* This is only used in a few places and could be avoided *) +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). +Proof. + intros. unfold Qeq. simpl. destruct a; reflexivity. +Qed. + +Lemma Q_factorNum_l : forall (a b : Z) (c : positive), + (a*b # c == (a # 1) * (b # c))%Q. +Proof. + intros a b c. + unfold Qeq; cbn; lia. +Qed. + +Lemma Q_factorNum : forall (a : Z) (b : positive), + (a # b == (a # 1) * (1 # b))%Q. +Proof. + intros a b. + unfold Qeq; cbn; lia. +Qed. + +Lemma Q_reduce_fl : forall (a b : positive), + (Z.pos a # a * b == (1 # b))%Q. +Proof. + intros a b. + unfold Qeq; cbn; lia. +Qed. + +(** * Lemmas on Q comparison *) + +Lemma Qle_neq: forall p q : Q, p < q <-> p <= q /\ ~ (p == q). +Proof. + intros p q; split; intros H. + - rewrite Qlt_alt in H; rewrite Qle_alt, Qeq_alt. + rewrite H; split; intros H1; inversion H1. + - rewrite Qlt_alt; rewrite Qle_alt, Qeq_alt in H. + destruct (p ?= q); tauto. +Qed. + +Lemma Qplus_lt_compat : forall x y z t : Q, + (x < y)%Q -> (z < t)%Q -> (x + z < y + t)%Q. +Proof. + intros x y z t H1 H2. + apply Qplus_lt_le_compat. + - assumption. + - apply Qle_lteq; left; assumption. +Qed. + +(* Qgt is just a notation, but one might now know this and search for this lemma *) + +Lemma Qgt_lt: forall p q : Q, p > q -> q < p. +Proof. + intros p q H; assumption. +Qed. + +Lemma Qlt_gt: forall p q : Q, p < q -> q > p. +Proof. + intros p q H; assumption. +Qed. + +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. +Proof. + intros a b Ha Hb. + destruct a,b. unfold Qlt, Qmult, QArith_base.Qnum, QArith_base.Qden in *. + rewrite Pos2Z.inj_mul. + rewrite Z.mul_0_l, Z.mul_1_r in *. + apply Z.mul_pos_pos; assumption. +Qed. + +Lemma Qmult_lt_1_compat: + forall a b : Q, (1 < a)%Q -> (1 < b)%Q -> (1 < a * b)%Q. +Proof. + intros a b Ha Hb. + pose proof Qmult_lt_0_compat (a-1) (b-1) ltac:(lra) ltac:(lra). + lra. +Qed. + +Lemma Qmult_le_1_compat: + forall a b : Q, (1 <= a)%Q -> (1 <= b)%Q -> (1 <= a * b)%Q. +Proof. + intros a b Ha Hb. + pose proof Qmult_le_0_compat (a-1) (b-1) ltac:(lra) ltac:(lra). + lra. +Qed. + +Lemma Qmult_lt_compat_nonneg: forall x y z t : Q, + (0 <= x < y)%Q -> (0 <= z < t)%Q -> (x * z < y * t)%Q. +Proof. + intros [xn xd] [yn yd] [zn zd] [tn td] [H0lex Hxlty] [H0lez Hzltt]. + (* ToDo: why do I need path qualification to Qnum? It is exported by QArith *) + unfold Qmult, Qlt, Qle, QArith_base.Qnum, QArith_base.Qden in *. + do 2 rewrite Pos2Z.inj_mul. + setoid_replace (xn * zn * (Z.pos yd * Z.pos td))%Z with ((xn * Z.pos yd) * (zn * Z.pos td))%Z by ring. + setoid_replace (yn * tn * (Z.pos xd * Z.pos zd))%Z with ((yn * Z.pos xd) * (tn * Z.pos zd))%Z by ring. + apply Z.mul_lt_mono_nonneg. + - rewrite <- (Z.mul_0_l 0); apply Z.mul_le_mono_nonneg; lia. + - exact Hxlty. + - rewrite <- (Z.mul_0_l 0); apply Z.mul_le_mono_nonneg; lia. + - exact Hzltt. +Qed. + +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. +Proof. + intros [xn xd] [yn yd] [zn zd] [tn td] [H0lex Hxlty] [H0lez Hzltt]. + (* ToDo: why do I need path qualification to Qnum? It is exported by QArith *) + unfold Qmult, Qlt, Qle, QArith_base.Qnum, QArith_base.Qden in *. + do 2 rewrite Pos2Z.inj_mul. + setoid_replace (xn * zn * (Z.pos yd * Z.pos td))%Z with ((xn * Z.pos yd) * (zn * Z.pos td))%Z by ring. + setoid_replace (yn * tn * (Z.pos xd * Z.pos zd))%Z with ((yn * Z.pos xd) * (tn * Z.pos zd))%Z by ring. + apply Zmult_lt_compat2; split. + - rewrite <- (Z.mul_0_l 0). apply Z.mul_lt_mono_nonneg; lia. + - exact Hxlty. + - rewrite <- (Z.mul_0_l 0). apply Z.mul_lt_mono_nonneg; lia. + - exact Hzltt. +Qed. + +Lemma Qmult_le_compat_nonneg: forall x y z t : Q, + (0 <= x <= y)%Q -> (0 <= z <= t)%Q -> (x * z <= y * t)%Q. +Proof. + intros [xn xd] [yn yd] [zn zd] [tn td] [H0lex Hxlty] [H0lez Hzltt]. + (* ToDo: why do I need path qualification to Qnum? It is exported by QArith *) + unfold Qmult, Qlt, Qle, QArith_base.Qnum, QArith_base.Qden in *. + do 2 rewrite Pos2Z.inj_mul. + setoid_replace (xn * zn * (Z.pos yd * Z.pos td))%Z with ((xn * Z.pos yd) * (zn * Z.pos td))%Z by ring. + setoid_replace (yn * tn * (Z.pos xd * Z.pos zd))%Z with ((yn * Z.pos xd) * (tn * Z.pos zd))%Z by ring. + apply Z.mul_le_mono_nonneg. + - rewrite <- (Z.mul_0_l 0); apply Z.mul_le_mono_nonneg; lia. + - exact Hxlty. + - rewrite <- (Z.mul_0_l 0); apply Z.mul_le_mono_nonneg; lia. + - exact Hzltt. +Qed. + +(** * Lemmas on Qinv *) + +Lemma Qinv_swap_pos: forall (a b : positive), + Z.pos a # b == / (Z.pos b # a). +Proof. + intros a b. + reflexivity. +Qed. + +Lemma Qinv_swap_neg: forall (a b : positive), + Z.neg a # b == / (Z.neg b # a). +Proof. + intros a b. + reflexivity. +Qed. + +(** * Lemmas on Qabs *) + +Lemma Qabs_Qlt_condition: forall x y : Q, + Qabs x < y <-> -y < x < y. +Proof. + split. + split. + rewrite <- (Qopp_opp x). + apply Qopp_lt_compat. + apply Qle_lt_trans with (Qabs (-x)). + apply Qle_Qabs. + now rewrite Qabs_opp. + apply Qle_lt_trans with (Qabs x); auto using Qle_Qabs. + intros (H,H'). + apply Qabs_case; trivial. + intros. rewrite <- (Qopp_opp y). now apply Qopp_lt_compat. +Qed. + +Lemma Qabs_gt: forall r s : Q, + (r < s)%Q -> (r < Qabs s)%Q. +Proof. + intros r s Hrlts. + apply Qabs_case; intros; lra. +Qed. + +(** * Lemmas on Qpower *) + +Lemma Qpower_0_r: forall q:Q, + q^0 == 1. +Proof. + intros q. + reflexivity. +Qed. + +Lemma Qpower_1_r: forall q:Q, + q^1 == q. +Proof. + intros q. + reflexivity. +Qed. + +Lemma Qpower_not_0: forall (a : Q) (z : Z), + ~ a == 0 -> ~ Qpower a z == 0. +Proof. + intros a z H; destruct z. + - discriminate. + - apply Qpower_not_0_positive; assumption. + - cbn. intros H1. + pose proof Qmult_inv_r (Qpower_positive a p) as H2. + specialize (H2 (Qpower_not_0_positive _ _ H)). + rewrite H1, Qmult_0_r in H2. + discriminate H2. +Qed. + +(* Actually Qpower_pos should be named Qpower_nonneg *) + +Lemma Qpower_pos_lt: forall (a : Q) (z : Z), + a > 0 -> Qpower a z > 0. +Proof. + intros q z Hpos. + pose proof Qpower_pos q z (Qlt_le_weak 0 q Hpos) as H1. + pose proof Qpower_not_0 q z as H2. + pose proof Qlt_not_eq 0 q Hpos as H3. + specialize (H2 (Qnot_eq_sym _ _ H3)); clear H3. + apply Qnot_eq_sym in H2. + apply Qle_neq; split; assumption. +Qed. + +Lemma Qpower_minus: forall (a : Q) (n m : Z), + ~ a == 0 -> a ^ (n - m) == a ^ n / a ^ m. +Proof. + intros a n m Hnz. + rewrite <- Z.add_opp_r. + rewrite Qpower_plus by assumption. + rewrite Qpower_opp. + field. + apply Qpower_not_0; assumption. +Qed. + +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. +Proof. + intros a b n m. + rewrite Qpower_minus by discriminate. + rewrite (Qinv_swap_pos b a), Qinv_power. + reflexivity. +Qed. + +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. +Proof. + intros a b n m. + rewrite Qpower_minus by discriminate. + rewrite (Qinv_swap_neg b a), Qinv_power. + reflexivity. +Qed. + +Lemma Qpower_lt_1_increasing: + forall (q : Q) (n : positive), (1<q)%Q -> (1 < q ^ (Z.pos n))%Q. +Proof. + intros q n Hq. + induction n. + - cbn in *. + apply Qmult_lt_1_compat. assumption. + apply Qmult_lt_1_compat; assumption. + - cbn in *. + apply Qmult_lt_1_compat; assumption. + - cbn; assumption. +Qed. + +Lemma Qpower_lt_1_increasing': + forall (q : Q) (n : Z), (1<q)%Q -> (0<n)%Z -> (1 < q ^ n)%Q. +Proof. + intros q n Hq Hn. + destruct n. + - inversion Hn. + - apply Qpower_lt_1_increasing; assumption. + - lia. +Qed. + +Lemma Qzero_eq: forall (d : positive), + (0#d == 0)%Q. +Proof. + intros d. + unfold Qeq, Qnum, Qden; reflexivity. +Qed. + +Lemma Qpower_le_1_increasing: + forall (q : Q) (n : positive), (1<=q)%Q -> (1 <= q ^ (Z.pos n))%Q. +Proof. + intros q n Hq. + induction n. + - cbn in *. + apply Qmult_le_1_compat. assumption. + apply Qmult_le_1_compat; assumption. + - cbn in *. + apply Qmult_le_1_compat; assumption. + - cbn; assumption. +Qed. + +Lemma Qpower_le_1_increasing': + forall (q : Q) (n : Z), (1<=q)%Q -> (0<=n)%Z -> (1 <= q ^ n)%Q. +Proof. + intros q n Hq Hn. + destruct n. + - apply Qle_refl. + - apply Qpower_le_1_increasing; assumption. + - lia. +Qed. + +(* ToDo: check if name compat_r is more appropriate *) + +Lemma Qpower_lt_compat: + forall (q : Q) (n m : Z), (n < m)%Z -> (1<q)%Q -> (q ^ n < q ^ m)%Q. +Proof. + intros q n m Hnm Hq. + replace m with (n+(m-n))%Z by ring. + rewrite Qpower_plus, <- Qmult_1_r, <- Qmult_assoc. + 2: lra. + rewrite Qmult_lt_l, Qmult_1_l. + 2: apply Qpower_pos_lt; lra. + remember (m-n)%Z as k. + apply Qpower_lt_1_increasing'. + - exact Hq. + - lia. +Qed. + +Lemma Qpower_le_compat: + forall (q : Q) (n m : Z), (n <= m)%Z -> (1<=q)%Q -> (q ^ n <= q ^ m)%Q. +Proof. + intros q n m Hnm Hq. + replace m with (n+(m-n))%Z by ring. + rewrite Qpower_plus, <- Qmult_1_r, <- Qmult_assoc. + 2: lra. + rewrite Qmult_le_l, Qmult_1_l. + 2: apply Qpower_pos_lt; lra. + remember (m-n)%Z as k. + apply Qpower_le_1_increasing'. + - exact Hq. + - lia. +Qed. + +Lemma Qpower_lt_compat_inv: + forall (q : Q) (n m : Z), (q ^ n < q ^ m)%Q -> (1<q)%Q -> (n < m)%Z. +Proof. + intros q n m Hnm Hq. + destruct (Z_lt_le_dec n m) as [Hd|Hd]. + - assumption. + - pose proof Qpower_le_compat q m n Hd ltac:(lra). + lra. +Qed. + +Lemma Qpower_le_compat_inv: + forall (q : Q) (n m : Z), (q ^ n <= q ^ m)%Q -> (1<q)%Q -> (n <= m)%Z. +Proof. + intros q n m Hnm Hq. + destruct (Z_lt_le_dec m n) as [Hd|Hd]. + - pose proof Qpower_lt_compat q m n Hd Hq. + lra. + - assumption. +Qed. + +Lemma Qpower_decomp': forall (p : positive) (a : Z) (b : positive), + (a # b) ^ (Z.pos p) == a ^ (Z.pos p) # (b ^ p)%positive. +Proof. + intros p a b. + pose proof Qpower_decomp p a b. + cbn; rewrite H; reflexivity. +Qed. + + +(** * 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}. +Proof. + intros q. + destruct (Qarchimedean q) as [pexp Hpexp]. + exists (Pos.size pexp). + pose proof Pos.size_gt pexp as H1. + unfold Qlt in *. cbn in *; Zify.zify. + apply (Z.mul_lt_mono_pos_r (QDen q)) in H1; [|assumption]. + apply (Z.lt_trans _ _ _ Hpexp H1). +Qed. + +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. +Proof. + intros p. + split. + - induction p. + + cbn. rewrite Pos.pow_succ_r. lia. + + cbn. rewrite Pos.pow_succ_r. lia. + + cbn. lia. + - induction p. + + cbn. rewrite Pos.pow_succ_r. lia. + + cbn. rewrite Pos.pow_succ_r. lia. + + cbn. lia. +Qed. + +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. +Proof. + intros p. + split. + - induction p. + + cbn. do 2 rewrite Pos.pow_succ_r. + pose proof Pos_log2floor_plus1_spec p. lia. + + cbn. rewrite Pos.pow_succ_r. lia. + + cbn. lia. + - induction p. + + cbn. do 2 rewrite Pos.pow_succ_r. + pose proof Pos_log2floor_plus1_spec p. lia. + + cbn. rewrite Pos.pow_succ_r. lia. + + cbn. lia. +Qed. + +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 + (* The -1000 is a compromise between a tight Archimedian and avoiding too large numbers *) + | 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. +Proof. + intros q. + destruct q as [num den]; unfold Qbound_le_ZExp2, Qnum; destruct num. + - intros contra; inversion contra. + - rewrite Qpower_minus by lra. + apply Qle_shift_div_l. + apply Qpower_pos_lt; lra. + do 2 rewrite Qpower_decomp', Pos_pow_1_r. + unfold Qle, Qmult, Qnum, Qden. + rewrite Pos.mul_1_r, Z.mul_1_r. + pose proof Pos_log2ceil_plus1_spec p as Hnom. + pose proof Pos_log2floor_plus1_spec den as Hden. + + apply (Zmult_le_reg_r _ _ 2). + lia. + replace (Z.pos p * 2 ^ Z.pos (Pos_log2floor_plus1 den) * 2)%Z + with ((Z.pos p * 2) * 2 ^ Z.pos (Pos_log2floor_plus1 den))%Z by ring. + replace (2 ^ Z.pos (Pos_log2ceil_plus1 p) * Z.pos den * 2)%Z + with (2 ^ Z.pos (Pos_log2ceil_plus1 p) * (Z.pos den * 2))%Z by ring. + apply Z.mul_le_mono_nonneg; lia. + - intros contra; inversion contra. +Qed. + +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. +Proof. + intros q. + unfold Qbound_leabs_ZExp2; apply Qabs_case; intros. + 1,2: apply Qbound_le_ZExp2_spec. +Qed. + +(** ** 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 + (* The -1000 is a compromise between a tight Archimedian and avoiding too large numbers *) + | 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. reflexivity. Qed. +Remark Qbound_lt_ZExp2_test_2 : Qbound_lt_ZExp2 (5#4) = 1%Z. reflexivity. Qed. +Remark Qbound_lt_ZExp2_test_3 : Qbound_lt_ZExp2 (4#5) = 1%Z. reflexivity. Qed. +Remark Qbound_lt_ZExp2_test_4 : Qbound_lt_ZExp2 (7#5) = 1%Z. reflexivity. Qed. + +Lemma Qbound_lt_ZExp2_spec : forall (q : Q), + (q < 2^(Qbound_lt_ZExp2 q))%Q. +Proof. + intros q. + destruct q as [num den]; unfold Qbound_lt_ZExp2, Qnum; destruct num. + - reflexivity. + - (* Todo: A lemma like Pos2Z.add_neg_pos for minus would be nice *) + change + (Z.pos_sub (Pos.succ (Pos_log2floor_plus1 p)) (Pos_log2floor_plus1 (Qden (Z.pos p # den))))%Z + with + ((Z.pos (Pos.succ (Pos_log2floor_plus1 p)) - Z.pos (Pos_log2floor_plus1 (Qden (Z.pos p # den)))))%Z. + rewrite Qpower_minus by lra. + apply Qlt_shift_div_l. + apply Qpower_pos_lt; lra. + do 2 rewrite Qpower_decomp', Pos_pow_1_r. + unfold Qlt, Qmult, Qnum, Qden. + rewrite Pos.mul_1_r, Z.mul_1_r. + pose proof Pos_log2floor_plus1_spec p as Hnom. + pose proof Pos_log2floor_plus1_spec den as Hden. + apply (Zmult_lt_reg_r _ _ 2). + lia. + rewrite Pos2Z.inj_succ, <- Z.add_1_r. + rewrite Z.pow_add_r by lia. + + replace (Z.pos p * 2 ^ Z.pos (Pos_log2floor_plus1 den) * 2)%Z + with (2 ^ Z.pos (Pos_log2floor_plus1 den) * (Z.pos p * 2))%Z by ring. + replace (2 ^ Z.pos (Pos_log2floor_plus1 p) * 2 ^ 1 * Z.pos den * 2)%Z + with ((Z.pos den * 2) * (2 * 2 ^ Z.pos (Pos_log2floor_plus1 p)))%Z by ring. + + (* ToDo: this is weaker than neccessary: Z.mul_lt_mono_nonneg. *) + apply Zmult_lt_compat2; lia. + - cbn. + (* ToDo: lra could know that negative fractions are negative *) + assert (Z.neg p # den < 0) as Hnegfrac by (unfold Qlt, Qnum, Qden; lia). + lra. +Qed. + +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. +Proof. + intros q. + unfold Qbound_ltabs_ZExp2; apply Qabs_case; intros. + 1,2: apply Qbound_lt_ZExp2_spec. +Qed. + +(** ** 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. +Proof. + intros q Hqgt0. + destruct q as [n d]. + unfold Qlowbound_ltabs_ZExp2, Qbound_ltabs_ZExp2, Qbound_lt_ZExp2, Qnum. + destruct n. + - inversion Hqgt0. + - unfold Qabs, Z.abs, Qinv, Qnum, Qden. + rewrite -> Z.pos_sub_opp. + do 2 rewrite <- Pos2Z.add_pos_neg. + lia. + - inversion Hqgt0. +Qed. + +Lemma Qlowbound_ltabs_ZExp2_opp: forall q : Q, + (Qlowbound_ltabs_ZExp2 q = Qlowbound_ltabs_ZExp2 (-q))%Z. +Proof. + intros q. + destruct q as [[|n|n] d]; reflexivity. +Qed. + +Lemma Qlowbound_lt_ZExp2_spec : forall (q : Q) (Hqgt0 : q > 0), + (2^(Qlowbound_ltabs_ZExp2 q) < q)%Q. +Proof. + intros q Hqgt0. + pose proof Qbound_ltabs_ZExp2_spec (/q) as Hspecub. + rewrite Qlowbound_ltabs_ZExp2_inv by exact Hqgt0. + rewrite Qpower_opp. + setoid_rewrite <- (Qinv_involutive q) at 2. + apply -> Qinv_lt_contravar. + - rewrite Qabs_pos in Hspecub. + + exact Hspecub. + + apply Qlt_le_weak, Qinv_lt_0_compat, Hqgt0. + - apply Qpower_pos_lt; lra. + - apply Qinv_lt_0_compat, Hqgt0. +Qed. + +Lemma Qlowbound_ltabs_ZExp2_spec : forall (q : Q) (Hqgt0 : ~ q == 0), + (2^(Qlowbound_ltabs_ZExp2 q) < Qabs q)%Q. +Proof. + intros q Hqgt0. + destruct (Q_dec 0 q) as [[H|H]|H]. + - rewrite Qabs_pos by lra. + apply Qlowbound_lt_ZExp2_spec, H. + - rewrite Qabs_neg by lra. + rewrite Qlowbound_ltabs_ZExp2_opp. + apply Qlowbound_lt_ZExp2_spec. + lra. + - lra. +Qed. + +(** ** 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). |