proposition: Lemma sqrt2_spec : forall x y, wB/ 4 <= φ x -> let (s,r) := sqrt2 x y in Φ (WW x y) = φ s ^ 2 + [+|r|] /\ [+|r|] <= 2 * φ s.
proof: Proof. intros ih il Hih; unfold sqrt2. change Φ (WW ih il) with (Φ(WW ih il)). assert (Hbin: forall s, s * s + 2* s + 1 = (s + 1) ^ 2) by (intros s; ring). assert (Hb: 0 <= wB) by (red; intros HH; discriminate). assert (Hi2: Φ(WW ih il ) < (φ max_int + 1) ^ 2). { apply Z.le_lt_trans with ((wB - 1) * wB + (wB - 1)); auto with zarith. case (to_Z_bounded ih); case (to_Z_bounded il); intros H1 H2 H3 H4. unfold zn2z_to_Z; auto with zarith. } case (iter2_sqrt_correct size (fun _ _ j => j) ih il max_int); auto with zarith. - apply refl_equal. - intros j1 _ HH; contradict HH. apply Zlt_not_le. case (to_Z_bounded j1); auto with zarith. change (2 ^ Z_of_nat size) with (φ max_int+1)%Z; auto with zarith. - set (s := iter2_sqrt size (fun _ _ j : int=> j) ih il max_int). intros Hs1 Hs2. generalize (mulc_spec s s); case mulc. simpl fst; simpl snd; intros ih1 il1 Hihl1. generalize (subc_spec il il1). case subc; intros il2 Hil2. + simpl interp_carry in Hil2. case_eq (ih1 <? ih)%uint63; [idtac | rewrite <- not_true_iff_false]; rewrite ltb_spec; intros Heq. * unfold interp_carry; rewrite Zmult_1_l. rewrite -> Z.pow_2_r, Hihl1, Hil2. case (Zle_lt_or_eq (φ ih1 + 1) (φ ih)); auto with zarith. -- intros H2; contradict Hs2; apply Zle_not_lt. replace ((φ s + 1) ^ 2) with (Φ(WW ih1 il1) + 2 * φ s + 1). ++ unfold zn2z_to_Z. case (to_Z_bounded il); intros Hpil _. assert (Hl1l: φ il1 <= φ il). ** case (to_Z_bounded il2); rewrite Hil2; auto with zarith. ** enough (φ ih1 * wB + 2 * φ s + 1 <= φ ih * wB) by lia. case (to_Z_bounded s); intros _ Hps. case (to_Z_bounded ih1); intros Hpih1 _. apply Z.le_trans with ((φ ih1 + 2) * wB). { lia. } auto with zarith. ++ unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto. -- intros H2; split. ++ unfold zn2z_to_Z; rewrite <- H2; ring. ++ replace (wB + (φ il - φ il1)) with (Φ(WW ih il) - (φ s * φ s)). { rewrite <-Hbin in Hs2; auto with zarith. } rewrite Hihl1; unfold zn2z_to_Z; rewrite <- H2; ring. * unfold interp_carry. case (Zle_lt_or_eq φ ih φ ih1); auto with zarith; intros H. -- contradict Hs1. apply Zlt_not_le; rewrite Z.pow_2_r, Hihl1. unfold zn2z_to_Z. case (to_Z_bounded il); intros _ H2. apply Z.lt_le_trans with ((φ ih + 1) * wB + 0). ++ rewrite Zmult_plus_distr_l, Zplus_0_r; auto with zarith. ++ case (to_Z_bounded il1); intros H3 _. apply Zplus_le_compat; auto with zarith. -- split. ++ rewrite Z.pow_2_r, Hihl1. unfold zn2z_to_Z; ring[Hil2 H]. ++ replace φ il2 with (Φ(WW ih il) - Φ(WW ih1 il1)). { unfold zn2z_to_Z at 2; rewrite <-Hihl1. rewrite <-Hbin in Hs2; auto with zarith. } unfold zn2z_to_Z; rewrite H, Hil2; ring. + unfold interp_carry in Hil2 |- *. assert (Hsih: φ (ih - 1) = φ ih - 1). { rewrite sub_spec, Zmod_small; auto; replace φ 1 with 1; auto. case (to_Z_bounded ih); intros H1 H2. split; auto with zarith. apply Z.le_trans with (wB/4 - 1); auto with zarith. } case_eq (ih1 <? ih - 1)%uint63; [idtac | rewrite <- not_true_iff_false]; rewrite ltb_spec, Hsih; intros Heq. * rewrite Z.pow_2_r, Hihl1. case (Zle_lt_or_eq (φ ih1 + 2) φ ih); auto with zarith. -- intros H2; contradict Hs2; apply Zle_not_lt. replace ((φ s + 1) ^ 2) with (Φ(WW ih1 il1) + 2 * φ s + 1). ++ unfold zn2z_to_Z. assert (φ ih1 * wB + 2 * φ s + 1 <= φ ih * wB + (φ il - φ il1)); auto with zarith. rewrite <-Hil2. case (to_Z_bounded il2); intros Hpil2 _. apply Z.le_trans with (φ ih * wB + - wB); auto with zarith. case (to_Z_bounded s); intros _ Hps. assert (2 * φ s + 1 <= 2 * wB); auto with zarith. apply Z.le_trans with (φ ih1 * wB + 2 * wB); auto with zarith. assert (Hi: (φ ih1 + 3) * wB <= φ ih * wB) by auto with zarith. lia. ++ unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto. -- intros H2; unfold zn2z_to_Z; rewrite <-H2. split. ++ replace φ il with ((φ il - φ il1) + φ il1) by ring. rewrite <-Hil2; ring. ++ replace (1 * wB + φ il2) with (Φ(WW ih il) - Φ(WW ih1 il1)). { unfold zn2z_to_Z at 2; rewrite <-Hihl1. rewrite <-Hbin in Hs2; auto with zarith. } unfold zn2z_to_Z; rewrite <-H2. replace φ il with ((φ il - φ il1) + φ il1); try ring. rewrite <-Hil2; ring. * case (Zle_lt_or_eq (φ ih - 1) (φ ih1)); auto with zarith; intros H1. -- assert (He: φ ih = φ ih1). { apply Zle_antisym; auto with zarith. case (Zle_or_lt φ ih1 φ ih); auto; intros H2. contradict Hs1; apply Zlt_not_le; rewrite Z.pow_2_r, Hihl1. unfold zn2z_to_Z. case (to_Z_bounded il); intros _ Hpil1. apply Z.lt_le_trans with ((φ ih + 1) * wB). - rewrite Zmult_plus_distr_l, Zmult_1_l; auto with zarith. - case (to_Z_bounded il1); intros Hpil2 _. apply Z.le_trans with ((φ ih1) * wB); auto with zarith. } contradict Hs1; apply Zlt_not_le; rewrite Z.pow_2_r, Hihl1. unfold zn2z_to_Z; rewrite He. assert (φ il - φ il1 < 0); auto with zarith. rewrite <-Hil2. case (to_Z_bounded il2); auto with zarith. -- split. ++ rewrite Z.pow_2_r, Hihl1. unfold zn2z_to_Z; rewrite <-H1. apply trans_equal with (φ ih * wB + φ il1 + (φ il - φ il1)). ** ring. ** rewrite <-Hil2; ring. ++ replace φ il2 with (Φ(WW ih il) - Φ(WW ih1 il1)). ** unfold zn2z_to_Z at 2; rewrite <- Hihl1. rewrite <-Hbin in Hs2; auto with zarith. ** unfold zn2z_to_Z. rewrite <-H1. ring_simplify. apply trans_equal with (wB + (φ il - φ il1)). 1:ring. rewrite <-Hil2; ring. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63