proposition: Lemma spec_ww_sqrt2 : forall x y, wwB/ 4 <= [[x]] -> let (s,r) := ww_sqrt2 x y in [||WW x y||] = [[s]] ^ 2 + [+[r]] /\ [+[r]] <= 2 * [[s]].
proof: Proof. assert (fake_use := ww_zdigits); clear fake_use. intros x y H; unfold ww_sqrt2. repeat match goal with |- context[split ?x] => generalize (spec_split x); case (split x) end; simpl @fst; simpl @snd. intros w0 w1 Hw0 w2 w3 Hw1. assert (U: wB/4 <= [|w2|]). { case (Z.le_gt_cases (wB / 4) [|w2|]); auto; intros H1. contradict H; apply Z.lt_nge. rewrite wwB_wBwB; rewrite Z.pow_2_r. pattern wB at 1; rewrite <- wB_div_4; rewrite <- Z.mul_assoc; rewrite Z.mul_comm. rewrite Z_div_mult by zarith. rewrite <- Hw1. match goal with |- _ < ?X => pattern X; rewrite <- Z.add_0_r; apply beta_lex_inv end. 1-2: zarith. destruct (spec_to_Z w3);zarith. } generalize (@spec_w_sqrt2 w2 w3 U); case (w_sqrt2 w2 w3). intros w4 c (H1, H2). assert (U1: wB/2 <= [|w4|]). { case (Z.le_gt_cases (wB/2) [|w4|]). zarith. intros U1. assert (U2 : [|w4|] <= wB/2 -1) by zarith. assert (U3 : [|w4|] ^ 2 <= wB/4 * wB - wB + 1). match goal with |- ?X ^ 2 <= ?Y => rewrite Zsquare_mult; replace Y with ((wB/2 - 1) * (wB/2 -1)) end. apply Z.mul_le_mono_nonneg. 2, 4: zarith. 1-2: destruct (spec_to_Z w4);zarith. pattern wB at 4 5; rewrite <- wB_div_2. rewrite Z.mul_assoc. replace ((wB / 4) * 2) with (wB / 2). ring. pattern wB at 1; rewrite <- wB_div_4. change 4 with (2 * 2). rewrite <- Z.mul_assoc; rewrite (Z.mul_comm 2). rewrite Z_div_mult; try ring; zarith. assert (U4 : [+|c|] <= wB -2). apply Z.le_trans with (1 := H2). match goal with |- ?X <= ?Y => replace Y with (2 * (wB/ 2 - 1)) end. zarith. pattern wB at 2; rewrite <- wB_div_2; zarith. match type of H1 with ?X = _ => assert (U5: X < wB / 4 * wB) end. rewrite H1; zarith. contradict U; apply Z.lt_nge. apply Z.mul_lt_mono_pos_r with wB. destruct (spec_to_Z w4);zarith. apply Z.le_lt_trans with (2 := U5). unfold ww_to_Z, zn2z_to_Z. destruct (spec_to_Z w3);zarith. } generalize (@spec_w_div2s c w0 w4 U1 H2). case (w_div2s c w0 w4). intros c0; case c0; intros w5; repeat (rewrite C0_id || rewrite C1_plus_wB). - intros c1; case c1; intros w6; repeat (rewrite C0_id || rewrite C1_plus_wB). + intros (H3, H4). match goal with |- context [ww_sub_c ?y ?z] => generalize (spec_ww_sub_c y z); case (ww_sub_c y z) end. * intros z; change [-[C0 z]] with ([[z]]). change [+[C0 z]] with ([[z]]). intros H5; rewrite spec_w_square_c in H5; auto. split. unfold zn2z_to_Z; rewrite <- Hw1. unfold ww_to_Z, zn2z_to_Z in H1. rewrite H1. rewrite <- Hw0. match goal with |- (?X ^2 + ?Y) * wwB + (?Z * wB + ?T) = ?U => transitivity ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) end. repeat rewrite Zsquare_mult. rewrite wwB_wBwB; ring. rewrite H3. rewrite H5. unfold ww_to_Z, zn2z_to_Z. repeat rewrite Zsquare_mult; ring. rewrite H5. unfold ww_to_Z, zn2z_to_Z. match goal with |- ?X - ?Y * ?Y <= _ => assert (V := Zsquare_pos Y); rewrite Zsquare_mult in V; apply Z.le_trans with X; [ zarith | ]; clear V end. match goal with |- ?X * wB + ?Y <= 2 * (?Z * wB + ?T) => apply Z.le_trans with ((2 * Z - 1) * wB + wB) end. destruct (spec_to_Z w1);zarith. match goal with |- ?X <= _ => replace X with (2 * [|w4|] * wB) by ring end. rewrite Z.mul_add_distr_l; rewrite Z.mul_assoc. destruct (spec_to_Z w5); zarith. * intros z; replace [-[C1 z]] with (- wwB + [[z]]). 2: simpl; case wwB; zarith. intros H5; rewrite spec_w_square_c in H5; auto. match goal with |- context [ww_pred_c ?y] => generalize (spec_ww_pred_c y); case (ww_pred_c y) end. intros z1; change [-[C0 z1]] with ([[z1]]). rewrite ww_add_mult_mult_2. rewrite spec_ww_add_c. rewrite spec_ww_pred. rewrite <- Zmod_unique with (q := 1) (r := -wwB + 2 * [[WW w4 w5]]). 3: zarith. intros Hz1; rewrite Zmod_small. match type of H5 with -?X + ?Y = ?Z => assert (V: Y = Z + X) by (rewrite <- H5; ring) end. split. unfold zn2z_to_Z; rewrite <- Hw1. unfold ww_to_Z, zn2z_to_Z in H1; rewrite H1. rewrite <- Hw0. match goal with |- (?X ^2 + ?Y) * wwB + (?Z * wB + ?T) = ?U => transitivity ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) end. repeat rewrite Zsquare_mult. rewrite wwB_wBwB; ring. rewrite H3. rewrite V. rewrite Hz1. unfold ww_to_Z; simpl zn2z_to_Z. repeat rewrite Zsquare_mult; ring. rewrite Hz1. destruct (spec_ww_to_Z w_digits w_to_Z spec_to_Z z);zarith. assert (V1 := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW w4 w5)). enough (0 < [[WW w4 w5]]) by zarith. apply Z.lt_le_trans with (wB/ 2 * wB + 0). autorewrite with rm10; apply Z.mul_pos_pos. apply Z.mul_lt_mono_pos_r with 2. zarith. autorewrite with rm10. rewrite Z.mul_comm; rewrite wB_div_2. case (spec_to_Z w5);zarith. case (spec_to_Z w5);zarith. simpl. assert (V2 := spec_to_Z w5); zarith. assert (V1 := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW w4 w5)). split. 2: zarith. enough (wwB <= 2 * [[WW w4 w5]]) by zarith. apply Z.le_trans with (2 * ([|w4|] * wB)). rewrite wwB_wBwB; rewrite Z.pow_2_r. rewrite Z.mul_assoc. apply Z.mul_le_mono_nonneg_r. assert (V2 := spec_to_Z w5);zarith. rewrite <- wB_div_2; zarith. simpl ww_to_Z; assert (V2 := spec_to_Z w5);zarith. assert (V1 := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW w4 w5)). intros z1; change [-[C1 z1]] with (-wwB + [[z1]]). match goal with |- context[([+[C0 ?z]])] => change [+[C0 z]] with ([[z]]) end. rewrite spec_ww_add by zarith. rewrite spec_ww_pred by zarith. rewrite ww_add_mult_mult_2. rename V1 into VV1. assert (VV2: 0 < [[WW w4 w5]]). apply Z.lt_le_trans with (wB/ 2 * wB + 0). autorewrite with rm10; apply Z.mul_pos_pos. apply Z.mul_lt_mono_pos_r with 2. zarith. autorewrite with rm10. rewrite Z.mul_comm, wB_div_2. assert (VV3 := spec_to_Z w5);zarith. assert (VV3 := spec_to_Z w5);zarith. simpl. assert (VV3 := spec_to_Z w5);zarith. assert (VV3: wwB <= 2 * [[WW w4 w5]]). apply Z.le_trans with (2 * ([|w4|] * wB)). rewrite wwB_wBwB; rewrite Z.pow_2_r. rewrite Z.mul_assoc; apply Z.mul_le_mono_nonneg_r. case (spec_to_Z w5);zarith. rewrite <- wB_div_2; zarith. simpl ww_to_Z; assert (V4 := spec_to_Z w5);zarith. rewrite <- Zmod_unique with (q := 1) (r := -wwB + 2 * [[WW w4 w5]]) by zarith. intros Hz1; rewrite Zmod_small by zarith. match type of H5 with -?X + ?Y = ?Z => assert (V: Y = Z + X) by (rewrite <- H5; ring) end. match type of Hz1 with -?X + ?Y = -?X + ?Z - 1 => assert (V1: Y = Z - 1); [replace (Z - 1) with (X + (-X + Z -1)); [rewrite <- Hz1 | idtac]; ring | idtac] end. rewrite <- Zmod_unique with (q := 1) (r := -wwB + [[z1]] + [[z]]). 3: zarith. unfold zn2z_to_Z; rewrite <- Hw1. unfold ww_to_Z, zn2z_to_Z in H1; rewrite H1. rewrite <- Hw0. split. match goal with |- (?X ^2 + ?Y) * wwB + (?Z * wB + ?T) = ?U => transitivity ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) end. repeat rewrite Zsquare_mult. rewrite wwB_wBwB; ring. rewrite H3. rewrite V. rewrite Hz1. unfold ww_to_Z; simpl zn2z_to_Z. repeat rewrite Zsquare_mult; ring. assert (V2 := spec_ww_to_Z w_digits w_to_Z spec_to_Z z);zarith. assert (V2 := spec_ww_to_Z w_digits w_to_Z spec_to_Z z). assert (V3 := spec_ww_to_Z w_digits w_to_Z spec_to_Z z1). split. 2: zarith. rewrite (Z.add_comm (-wwB)); rewrite <- Z.add_assoc. rewrite H5. match goal with |- 0 <= ?X + (?Y - ?Z) => apply Z.le_trans with (X - Z) end. 2: generalize (spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW w6 w1)); unfold ww_to_Z; zarith. rewrite V1. match goal with |- 0 <= ?X - 1 - ?Y => enough (Y < X) by zarith end. apply Z.lt_le_trans with wwB; zarith. + intros (H3, H4). match goal with |- context [ww_sub_c ?y ?z] => generalize (spec_ww_sub_c y z); case (ww_sub_c y z) end. * intros z; change [-[C0 z]] with ([[z]]). match goal with |- context[([+[C1 ?z]])] => replace [+[C1 z]] with (wwB + [[z]]) end. 2: simpl; case wwB; auto. intros H5; rewrite spec_w_square_c in H5; auto. split. change ([||WW x y||]) with ([[x]] * wwB + [[y]]). rewrite <- Hw1. unfold ww_to_Z, zn2z_to_Z in H1; rewrite H1. rewrite <- Hw0. match goal with |- (?X ^2 + ?Y) * wwB + (?Z * wB + ?T) = ?U => transitivity ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) end. repeat rewrite Zsquare_mult. rewrite wwB_wBwB; ring. rewrite H3. rewrite H5. unfold ww_to_Z; simpl zn2z_to_Z. rewrite wwB_wBwB. repeat rewrite Zsquare_mult; ring. simpl ww_to_Z. rewrite H5. simpl ww_to_Z. rewrite wwB_wBwB; rewrite Z.pow_2_r. match goal with |- ?X * ?Y + (?Z * ?Y + ?T - ?U) <= _ => apply Z.le_trans with (X * Y + (Z * Y + T - 0)) end. assert (V := Zsquare_pos [|w5|]); rewrite Zsquare_mult in V; zarith. autorewrite with rm10. match goal with |- _ <= 2 * (?U * ?V + ?W) => apply Z.le_trans with (2 * U * V + 0) end. match goal with |- ?X * ?Y + (?Z * ?Y + ?T) <= _ => replace (X * Y + (Z * Y + T)) with ((X + Z) * Y + T) by ring end. apply Z.lt_le_incl; apply beta_lex_inv. lia. zarith. destruct (spec_to_Z w1); lia. destruct (spec_to_Z w5); lia. * intros z; replace [-[C1 z]] with (- wwB + [[z]]). 2: simpl; case wwB; zarith. intros H5; rewrite spec_w_square_c in H5; auto. match goal with |- context[([+[C0 ?z]])] => change [+[C0 z]] with ([[z]]) end. match type of H5 with -?X + ?Y = ?Z => assert (V: Y = Z + X); try (rewrite <- H5; ring) end. change ([||WW x y||]) with ([[x]] * wwB + [[y]]). simpl ww_to_Z. rewrite <- Hw1. simpl ww_to_Z in H1; rewrite H1. rewrite <- Hw0. split. match goal with |- (?X ^2 + ?Y) * wwB + (?Z * wB + ?T) = ?U => transitivity ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) end. repeat rewrite Zsquare_mult. rewrite wwB_wBwB; ring. rewrite H3. rewrite V. simpl ww_to_Z. rewrite wwB_wBwB. repeat rewrite Zsquare_mult; ring. rewrite V. simpl ww_to_Z. rewrite wwB_wBwB; rewrite Z.pow_2_r. match goal with |- (?Z * ?Y + ?T - ?U) + ?X * ?Y <= _ => apply Z.le_trans with ((Z * Y + T - 0) + X * Y) end. assert (V1 := Zsquare_pos [|w5|]); rewrite Zsquare_mult in V1; zarith. autorewrite with rm10. match goal with |- _ <= 2 * (?U * ?V + ?W) => apply Z.le_trans with (2 * U * V + 0) end. match goal with |- (?Z * ?Y + ?T) + ?X * ?Y <= _ => replace ((Z * Y + T) + X * Y) with ((X + Z) * Y + T) by ring end. apply Z.lt_le_incl; apply beta_lex_inv. lia. zarith. destruct (spec_to_Z w1); lia. destruct (spec_to_Z w5); lia. - Z.le_elim H2. + intros c1 (H3, H4). match type of H3 with ?X = ?Y => absurd (X < Y) end. * apply Z.le_ngt; rewrite <- H3; zarith. * rewrite Z.mul_add_distr_r. apply Z.lt_le_trans with ((2 * [|w4|]) * wB + 0). apply beta_lex_inv. 1-2: zarith. destruct (spec_to_Z w0);zarith. assert (V1 := spec_to_Z w5). rewrite (Z.mul_comm wB) by zarith. assert (0 <= [|w5|] * (2 * [|w4|])); zarith. + intros c1 (H3, H4); rewrite H2 in H3. match type of H3 with ?X + ?Y = (?Z + ?T) * ?U + ?V => assert (VV: (Y = (T * U) + V)); [replace Y with ((X + Y) - X); [rewrite H3; ring | ring] | idtac] end. assert (V1 := spec_to_Z w0). assert (V2 := spec_to_Z w5). case V2; intros V3 _. Z.le_elim V3. * match type of VV with ?X = ?Y => absurd (X < Y) end. apply Z.le_ngt; rewrite <- VV; zarith. apply Z.lt_le_trans with wB. zarith. match goal with |- _ <= ?X + _ => apply Z.le_trans with X; [ | zarith ] end. match goal with |- _ <= _ * ?X => apply Z.le_trans with (1 * X); [ | zarith ] end. autorewrite with rm10. rewrite <- wB_div_2; apply Z.mul_le_mono_nonneg_l; zarith. * rewrite <- V3 in VV; generalize VV; autorewrite with rm10; clear VV; intros VV. rewrite spec_ww_add_c by zarith. rewrite ww_add_mult_mult_2_plus_1. match goal with |- context[?X mod wwB] => rewrite <- Zmod_unique with (q := 1) (r := -wwB + X) end. 3: zarith. simpl ww_to_Z. rewrite spec_w_Bm1 by zarith. split. change ([||WW x y||]) with ([[x]] * wwB + [[y]]). rewrite <- Hw1. simpl ww_to_Z in H1; rewrite H1. rewrite <- Hw0. match goal with |- (?X ^2 + ?Y) * wwB + (?Z * wB + ?T) = ?U => transitivity ((X * wB) ^ 2 + (Y * wB + Z) * wB + T) end. repeat rewrite Zsquare_mult. rewrite wwB_wBwB; ring. rewrite H2. rewrite wwB_wBwB. repeat rewrite Zsquare_mult; ring. assert (V4 := spec_ww_to_Z w_digits w_to_Z spec_to_Z y);zarith. assert (V4 := spec_ww_to_Z w_digits w_to_Z spec_to_Z y). simpl ww_to_Z; unfold ww_to_Z. rewrite spec_w_Bm1 by zarith. split. rewrite wwB_wBwB; rewrite Z.pow_2_r. match goal with |- _ <= -?X + (2 * (?Z * ?T + ?U) + ?V) => assert (X <= 2 * Z * T) end. apply Z.mul_le_mono_nonneg_r. zarith. rewrite <- wB_div_2; apply Z.mul_le_mono_nonneg_l; zarith. rewrite Z.mul_add_distr_l by zarith. rewrite Z.mul_assoc; zarith. match goal with |- _ + ?X < _ => replace X with ((2 * (([|w4|]) + 1) * wB) - 1) by ring end. enough (2 * ([|w4|] + 1) * wB <= 2 * wwB) by zarith. rewrite <- Z.mul_assoc; apply Z.mul_le_mono_nonneg_l. zarith. rewrite wwB_wBwB; rewrite Z.pow_2_r. apply Z.mul_le_mono_nonneg_r. zarith. case (spec_to_Z w4);zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase