proposition: Lemma spec_ww_sqrt : forall x, [[ww_sqrt x]] ^ 2 <= [[x]] < ([[ww_sqrt x]] + 1) ^ 2.
proof: Proof. clear spec_w_Bm1. assert (fake_use := (w_1, w_Bm1)); clear fake_use. assert (U := wB_pos w_digits). intro x; unfold ww_sqrt. generalize (spec_ww_is_zero x); case (ww_is_zero x). simpl ww_to_Z; simpl Z.pow; unfold Z.pow_pos; simpl; zarith. intros H1. rewrite spec_ww_compare. case Z.compare_spec; simpl ww_to_Z; autorewrite with rm10. generalize H1; case x. intros HH; contradict HH; simpl ww_to_Z; zarith. intros w0 w1; simpl ww_to_Z; autorewrite with w_rewrite rm10. intros H2; case (spec_ww_head1 (WW w0 w1)); intros H3 H4 H5. generalize (H4 H2); clear H4; rewrite H5; clear H5; autorewrite with rm10. intros (H4, H5). assert (V: wB/4 <= [|w0|]). { apply beta_lex with 0 [|w1|] wB. 2-3: zarith. autorewrite with rm10. rewrite <- wwB_4_wB_4; auto. } generalize (@spec_w_sqrt2 w0 w1 V). case (w_sqrt2 w0 w1); intros w2 c. simpl ww_to_Z; simpl @fst. case c; unfold interp_carry; autorewrite with rm10. intros w3 (H6, H7); rewrite H6. assert (V1 := spec_to_Z w3). split. zarith. apply Z.le_lt_trans with ([|w2|] ^2 + 2 * [|w2|]). zarith. match goal with |- ?X < ?Z => replace Z with (X + 1); lia end. intros w3 (H6, H7); rewrite H6. assert (V1 := spec_to_Z w3). split. zarith. apply Z.le_lt_trans with ([|w2|] ^2 + 2 * [|w2|]). zarith. match goal with |- ?X < ?Z => replace Z with (X + 1); lia end. intros HH; case (spec_to_w_Z (ww_head1 x)); zarith. intros Hv1. case (spec_ww_head1 x); intros Hp1 Hp2. generalize (Hp2 H1); clear Hp2; intros Hp2. assert (Hv2: [[ww_head1 x]] <= Zpos (xO w_digits)). case (Z.le_gt_cases (Zpos (xO w_digits)) [[ww_head1 x]]). 2: zarith. intros HH1. case Hp2; intros _ HH2; contradict HH2. apply Z.le_ngt; unfold base. apply Z.le_trans with (2 ^ [[ww_head1 x]]). apply Zpower_le_monotone; zarith. pattern (2 ^ [[ww_head1 x]]) at 1; rewrite <- (Z.mul_1_r (2 ^ [[ww_head1 x]])). apply Z.mul_le_mono_nonneg_l; zarith. generalize (spec_ww_add_mul_div x W0 (ww_head1 x) Hv2); case ww_add_mul_div. simpl ww_to_Z; autorewrite with w_rewrite rm10. rewrite Zmod_small. intros H2. symmetry in H2. rewrite Z.mul_eq_0 in H2. destruct H2 as [H2|H2]. rewrite H2; unfold Z.pow, Z.pow_pos; simpl; zarith. match type of H2 with ?X = ?Y => absurd (Y < X); [ rewrite H2; zarith | ] end. apply Z.pow_pos_nonneg; zarith. split. zarith. case Hp2; intros _ tmp; apply Z.le_lt_trans with (2 := tmp); clear tmp. rewrite Z.mul_comm; apply Z.mul_le_mono_nonneg_r; zarith. assert (Hv0: [[ww_head1 x]] = 2 * ([[ww_head1 x]]/2)). pattern [[ww_head1 x]] at 1; rewrite (Z_div_mod_eq_full [[ww_head1 x]] 2) by zarith. generalize (spec_ww_is_even (ww_head1 x)); rewrite Hp1; intros tmp; rewrite tmp; rewrite Z.add_0_r; auto. intros w0 w1; autorewrite with w_rewrite rm10. rewrite Zmod_small by (rewrite Z.mul_comm; zarith). intros H2. assert (V: wB/4 <= [|w0|]). { apply beta_lex with 0 [|w1|] wB. 2: zarith. autorewrite with rm10. simpl ww_to_Z in H2; rewrite H2. rewrite <- wwB_4_wB_4 by zarith. rewrite Z.mul_comm; zarith. assert (V1 := spec_to_Z w1);zarith. } generalize (@spec_w_sqrt2 w0 w1 V). case (w_sqrt2 w0 w1); intros w2 c. case (spec_to_Z w2); intros HH1 HH2. simpl ww_to_Z; simpl @fst. assert (Hv3: [[ww_pred ww_zdigits]] = Zpos (xO w_digits) - 1). { rewrite spec_ww_pred; rewrite spec_ww_zdigits. rewrite Zmod_small. reflexivity. split. zarith. apply Z.lt_le_trans with (Zpos (xO w_digits)). zarith. unfold base; apply Zpower2_le_lin; zarith. } assert (Hv4: [[ww_head1 x]]/2 < wB). apply Z.le_lt_trans with (Zpos w_digits). apply Z.mul_le_mono_pos_r with 2. zarith. repeat rewrite (fun x => Z.mul_comm x 2). rewrite <- Hv0; rewrite <- Pos2Z.inj_xO; auto. unfold base; apply Zpower2_lt_lin; zarith. assert (Hv5: [[(ww_add_mul_div (ww_pred ww_zdigits) W0 (ww_head1 x))]] = [[ww_head1 x]]/2). rewrite spec_ww_add_mul_div. simpl ww_to_Z; autorewrite with rm10. rewrite Hv3. ring_simplify (Zpos (xO w_digits) - (Zpos (xO w_digits) - 1)). rewrite Z.pow_1_r. rewrite Zmod_small. reflexivity. split. zarith. apply Z.lt_le_trans with (1 := Hv4). 2: zarith. unfold base; apply Zpower_le_monotone. zarith. split; unfold ww_digits; try rewrite Pos2Z.inj_xO; zarith. assert (Hv6: [|low(ww_add_mul_div (ww_pred ww_zdigits) W0 (ww_head1 x))|] = [[ww_head1 x]]/2). rewrite spec_low. rewrite Hv5; rewrite Zmod_small; zarith. rewrite spec_w_add_mul_div. rewrite spec_w_sub. rewrite spec_w_0. simpl ww_to_Z; autorewrite with rm10. rewrite Hv6; rewrite spec_w_zdigits. rewrite (fun x y => Zmod_small (x - y)). ring_simplify (Zpos w_digits - (Zpos w_digits - [[ww_head1 x]] / 2)). rewrite Zmod_small. simpl ww_to_Z in H2; rewrite H2. intros (H4, H5); split. apply Z.mul_le_mono_pos_r with (2 ^ [[ww_head1 x]]). zarith. rewrite H4. apply Z.le_trans with ([|w2|] ^ 2). rewrite Z.mul_comm. pattern [[ww_head1 x]] at 1; rewrite Hv0. rewrite (Z.mul_comm 2); rewrite Z.pow_mul_r by zarith. assert (tmp: forall p q, p ^ 2 * q ^ 2 = (p * q) ^2); try (intros; repeat rewrite Zsquare_mult; ring); rewrite tmp; clear tmp. apply Zpower_le_monotone3. zarith. split. zarith. pattern [|w2|] at 2; rewrite (Z_div_mod_eq_full [|w2|] (2 ^ ([[ww_head1 x]] / 2))) by zarith. match goal with |- ?X <= ?X + ?Y => enough (0 <= Y) by zarith end. case (Z_mod_lt [|w2|] (2 ^ ([[ww_head1 x]] / 2))); zarith. case c; unfold interp_carry; autorewrite with rm10; intros w3; assert (V3 := spec_to_Z w3);zarith. apply Z.mul_lt_mono_pos_r with (2 ^ [[ww_head1 x]]). zarith. rewrite H4. apply Z.le_lt_trans with ([|w2|] ^ 2 + 2 * [|w2|]). zarith. apply Z.lt_le_trans with (([|w2|] + 1) ^ 2). match goal with |- ?X < ?Y => replace Y with (X + 1); [ zarith | ] end. repeat rewrite (Zsquare_mult); ring. rewrite Z.mul_comm. pattern [[ww_head1 x]] at 1; rewrite Hv0. rewrite (Z.mul_comm 2); rewrite Z.pow_mul_r by zarith. assert (tmp: forall p q, p ^ 2 * q ^ 2 = (p * q) ^2); try (intros; repeat rewrite Zsquare_mult; ring); rewrite tmp; clear tmp. apply Zpower_le_monotone3. zarith. split. zarith. pattern [|w2|] at 1; rewrite (Z_div_mod_eq_full [|w2|] (2 ^ ([[ww_head1 x]]/2))) by zarith. rewrite <- Z.add_assoc; rewrite Z.mul_add_distr_l. autorewrite with rm10; apply Z.add_le_mono_l. case (Z_mod_lt [|w2|] (2 ^ ([[ww_head1 x]]/2))); zarith. split. zarith. apply Z.le_lt_trans with ([|w2|]). 2: zarith. apply Zdiv_le_upper_bound. zarith. pattern [|w2|] at 1; replace [|w2|] with ([|w2|] * 2 ^0). apply Z.mul_le_mono_nonneg_l. zarith. apply Zpower_le_monotone; zarith. rewrite Z.pow_0_r; autorewrite with rm10; auto. split. rewrite Hv0 in Hv2; rewrite (Pos2Z.inj_xO w_digits) in Hv2; zarith. apply Z.le_lt_trans with (Zpos w_digits). zarith. unfold base; apply Zpower2_lt_lin; zarith. rewrite spec_w_sub by zarith. rewrite Hv6; rewrite spec_w_zdigits by zarith. assert (Hv7: 0 < [[ww_head1 x]]/2) by zarith. rewrite Zmod_small. zarith. split. enough ([[ww_head1 x]]/2 <= Zpos w_digits) by zarith. apply Z.mul_le_mono_pos_r with 2. zarith. repeat rewrite (fun x => Z.mul_comm x 2). rewrite <- Hv0; rewrite <- Pos2Z.inj_xO; zarith. apply Z.le_lt_trans with (Zpos w_digits). zarith. unfold base; apply Zpower2_lt_lin; zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase