Require Import Reals log2 Psatz. Open Scope R_scope. Definition ln_a_10p10_10_4 := Eval vm_compute in ln_approx (10 ^ 10) (10 * 10 ^ 10) 4. Lemma big_cmp1 : ln_approx (10 ^ 10) (10 * 10 ^ 10) 4 = ln_a_10p10_10_4. Proof. Time vm_compute; reflexivity. Qed. Definition ln_a_10p10_2_4 := Eval vm_compute in ln_approx (10 ^ 10) (2 * 10 ^ 10) 4. Lemma big_cmp2 : ln_approx (10 ^ 10) (2 * 10 ^ 10) 4 = ln_a_10p10_2_4. Proof. Time vm_compute; reflexivity. Qed. Lemma big_cmp : Rpower 10 (10 ^ 6 + 4) < Rpower 2 3321942. Proof. match goal with |- _ < Rpower _ ?a => set (p := a) end. unfold Rpower; apply exp_increasing. assert (p0 : 0 <= p). assert (h1 : forall x, 0 <= x -> 0 <= 1 + 2 * x) by (intros; psatzl R). assert (h2 : forall x, 0 <= x -> 0 <= 2 * x) by (intros; psatzl R). repeat (apply h1 || apply h2); simpl; psatzl R. assert (tp10gt1 : (1 < 10 ^ 10)%Z) by (apply Z.pow_gt_1; lia). assert (int10 : (10 ^ 10 < 10 * 10 ^ 10)%Z) by lia. assert (l1 := ln_approx_correct (10 ^ 10) tp10gt1 _ int10 4). replace (ln 10) with (ln (IZR 10)) by (replace 10 with (IZR 10) by (simpl; ring); reflexivity). rewrite big_cmp1 in l1; unfold ln_a_10p10_10_4 in l1. apply Rle_lt_trans with ((10 ^ 6 + 4) * hR (10 ^ 10) (snd ln_a_10p10_10_4)). replace (IZR 10) with (hR (10 ^ 10) (10 * 10 ^ 10)). apply Rmult_le_compat_l; [ | exact (proj2 l1)]. apply Rplus_le_le_0_compat; [apply pow_le; psatzl R | psatzl R]. unfold hR, Rdiv; rewrite mult_IZR, Rmult_assoc, Rinv_r. psatzl R. apply Rgt_not_eq, (IZR_lt 0); reflexivity. assert (int2 : (10 ^ 10 < 2 * 10 ^ 10)%Z) by lia. assert (l2 := ln_approx_correct (10 ^ 10) tp10gt1 _ int2 4). rewrite big_cmp2 in l2. replace (ln 2) with (ln (hR (10 ^ 10) (2 * 10 ^ 10))). apply Rlt_le_trans with (p * hR (10 ^ 10) (fst ln_a_10p10_2_4)); [|apply Rmult_le_compat_l;[assumption | destruct (ln_a_10p10_2_4)]]. unfold hR, Rdiv; rewrite <- !Rmult_assoc; apply Rmult_lt_compat_r. apply Rinv_0_lt_compat, (IZR_lt 0); lia. replace (10 ^ 6 + 4) with (IZR (10 ^ 6 + 4)). rewrite <- mult_IZR. unfold p; change 1%R with (IZR 1); repeat (rewrite <- plus_IZR || rewrite <- mult_IZR). apply IZR_lt; compute; reflexivity. replace 6%Z with (Z.of_nat 6) by (simpl; ring). rewrite plus_IZR, <- pow_IZR. replace (IZR 10) with 10 by (simpl; ring); simpl; ring. exact (proj1 l2). unfold hR, Rdiv; rewrite mult_IZR, Rmult_assoc, Rinv_r, Rmult_1_r. reflexivity. apply Rgt_not_eq, (IZR_lt 0); reflexivity. Qed. Lemma big_cmp' : Rpower 2 3321941 < Rpower 10 (10 ^ 6 + 4). Proof. match goal with |- Rpower _ ?a < _ => set (p := a) end. unfold Rpower; apply exp_increasing. assert (hRid : forall precision x, (0 < precision)%Z -> hR precision (x * precision) = IZR x). intros precision x p0; unfold hR, Rdiv; rewrite mult_IZR, Rmult_assoc, Rinv_r. psatzl R. apply Rgt_not_eq, (IZR_lt 0); assumption. assert (p0 : 0 <= p). assert (h1 : forall x, 0 <= x -> 0 <= 1 + 2 * x) by (intros; psatzl R). assert (h2 : forall x, 0 <= x -> 0 <= 2 * x) by (intros; psatzl R). repeat (apply h1 || apply h2); simpl; psatzl R. assert (tp10gt1 : (1 < 10 ^ 10)%Z) by (apply Z.pow_gt_1; lia). assert (int10 : (10 ^ 10 < 10 * 10 ^ 10)%Z) by lia. assert (l1 := ln_approx_correct (10 ^ 10) tp10gt1 _ int10 4). replace (ln 10) with (ln (hR (10 ^ 10) (10 * 10 ^ 10))); [| rewrite hRid; [replace (IZR 10) with 10 by (simpl; ring); reflexivity | lia]]. rewrite big_cmp1 in l1; unfold ln_a_10p10_10_4 in l1. apply Rlt_le_trans with ((10 ^ 6 + 4) * hR (10 ^ 10) (fst ln_a_10p10_10_4)); [ | apply Rmult_le_compat_l; [ apply Rplus_le_le_0_compat; [apply pow_le; psatzl R | psatzl R] | exact (proj1 l1)]]. assert (int2 : (10 ^ 10 < 2 * 10 ^ 10)%Z) by lia. assert (l2 := ln_approx_correct (10 ^ 10) tp10gt1 _ int2 4). rewrite big_cmp2 in l2. replace (ln 2) with (ln (hR (10 ^ 10) (2 * 10 ^ 10))); [| rewrite hRid;[ reflexivity | lia]]. apply Rle_lt_trans with (p * hR (10 ^ 10) (snd ln_a_10p10_2_4)). apply Rmult_le_compat_l;[assumption | destruct (ln_a_10p10_2_4); tauto]. unfold hR, Rdiv; rewrite <- !Rmult_assoc; apply Rmult_lt_compat_r. apply Rinv_0_lt_compat, (IZR_lt 0); lia. replace (10 ^ 6 + 4) with (IZR (10 ^ 6 + 4)). rewrite <- mult_IZR. unfold p; change 1%R with (IZR 1); repeat (rewrite <- plus_IZR || rewrite <- mult_IZR). apply IZR_lt; compute; reflexivity. replace 6%Z with (Z.of_nat 6) by (simpl; ring). rewrite plus_IZR, <- pow_IZR. replace (IZR 10) with 10 by (simpl; ring); simpl; ring. Qed. Lemma million_digit_ub_bin : (10 ^ (10 ^ 6 + 4) < 2 ^ 3321942)%Z. Proof. assert (0 <= 3321942)%Z by (compute; discriminate). assert (0 <= 10 ^ 6 + 4)%Z by (compute; discriminate). assert (0 < IZR 2) by (simpl; psatzl R). assert (0 < IZR 10) by (simpl; psatzl R). assert (0 <= 6)%Z by (compute; discriminate). apply lt_IZR. rewrite <- (Z2Nat.id (10 ^ 6 + 4)), <- (Z2Nat.id 3321942), <- !pow_IZR;auto. rewrite <- !Rpower_pow, !INR_IZR_INZ, !Z2Nat.id, plus_IZR; auto. rewrite <- (Z2Nat.id 6), <- pow_IZR; auto. replace (IZR 10) with 10 by (simpl; ring); simpl (IZR 2). replace (IZR 4) with 4 by (simpl; ring). replace (Z.to_nat 6) with 6%nat by reflexivity. replace (IZR 3321942) with 3321942; [apply big_cmp | ]. change 1 with (IZR 1); repeat (rewrite <- plus_IZR || rewrite <-mult_IZR). apply f_equal; compute; reflexivity. Qed. Lemma million_digit_lb_bin : (2 ^ 3321942 < 2 * 10 ^ (10 ^ 6 + 4))%Z. Proof. assert (0 <= 3321942)%Z by (compute; discriminate). assert (0 <= 10 ^ 6 + 4)%Z by (compute; discriminate). assert (0 < IZR 2) by (simpl; psatzl R). assert (0 < IZR 10) by (simpl; psatzl R). assert (0 <= 6)%Z by (compute; discriminate). apply lt_IZR. rewrite mult_IZR. rewrite <- (Z2Nat.id (10 ^ 6 + 4)), <- (Z2Nat.id 3321942), <- !pow_IZR;auto. rewrite <- !Rpower_pow, !INR_IZR_INZ, !Z2Nat.id, plus_IZR; auto. rewrite <- (Z2Nat.id 6), <- pow_IZR; auto. replace (IZR 10) with 10 by (simpl; ring); simpl (IZR 2). replace (IZR 4) with 4 by (simpl; ring). replace (Z.to_nat 6) with 6%nat by reflexivity. replace (IZR 3321942) with (1 + 3321941). rewrite Rpower_plus, Rpower_1; try psatzl R. apply Rmult_lt_compat_l; try psatzl R; apply big_cmp'. change 1 with (IZR 1); repeat (rewrite <- plus_IZR || rewrite <-mult_IZR). apply f_equal; compute; reflexivity. Qed.