proposition: Lemma sqrt2_step_correct rec ih il j: 2 ^ (Z_of_nat (size - 2)) <= φ ih -> 0 < φ j -> Φ (WW ih il) < (φ j + 1) ^ 2 -> (forall j1, 0 < φ j1 < φ j -> Φ (WW ih il) < (φ j1 + 1) ^ 2 -> φ (rec ih il j1) ^ 2 <= Φ (WW ih il) < (φ (rec ih il j1) + 1) ^ 2) -> φ (sqrt2_step rec ih il j) ^ 2 <= Φ (WW ih il) < (φ (sqrt2_step rec ih il j) + 1) ^ 2.
proof: Proof. assert (Hp2: (0 < φ 2)%Z) by exact (refl_equal Lt). intros Hih Hj Hij Hrec; rewrite sqrt2_step_def. assert (H1: (φ ih <= φ j)%Z) by (apply sqrt2_lower_bound with il; auto). case (to_Z_bounded ih); intros Hih1 _. case (to_Z_bounded il); intros Hil1 _. case (to_Z_bounded j); intros _ Hj1. assert (Hp3: (0 < Φ (WW ih il))). { simpl zn2z_to_Z;apply Z.lt_le_trans with (φ ih * wB)%Z; auto with zarith. apply Zmult_lt_0_compat; auto with zarith. } cbv zeta. case_eq (ih <? j)%uint63;intros Heq. 2:{ rewrite <-not_true_iff_false, ltb_spec in Heq. split; auto. apply sqrt_test_true; auto with zarith. unfold zn2z_to_Z; replace φ ih with φ j; auto with zarith. assert (0 <= φ il/φ j) by (apply Z_div_pos; auto with zarith). rewrite Zmult_comm, Z_div_plus_full_l; unfold base; auto with zarith. } rewrite -> ltb_spec in Heq. case (Zle_or_lt (2^(Z_of_nat size -1)) φ j); intros Hjj. 1: case_eq (fst (diveucl_21 ih il j) <? j)%uint63;intros Heq0. 2:{ rewrite <-not_true_iff_false, ltb_spec, (div2_phi _ _ _ Hjj Heq) in Heq0. split; auto; apply sqrt_test_true; auto with zarith. } - rewrite -> ltb_spec, (div2_phi _ _ _ Hjj Heq) in Heq0. match goal with |- context[rec _ _ ?X] => set (u := X) end. assert (H: φ u = (φ j + (Φ (WW ih il))/(φ j))/2). { unfold u; generalize (addc_spec j (fst (diveucl_21 ih il j))); case addc;unfold interp_carry;rewrite (div2_phi _ _ _ Hjj Heq);simpl zn2z_to_Z. { intros i H;rewrite lsr_spec, H;trivial. } intros i H;rewrite <- H. case (to_Z_bounded i); intros H1i H2i. rewrite -> add_spec, Zmod_small, lsr_spec. { change (1 * wB) with (φ (1 << (digits -1)) * 2)%Z. rewrite Z_div_plus_full_l; auto with zarith. } change wB with (2 * (wB/2))%Z; auto. replace φ (1 << (digits - 1)) with (wB/2); auto. rewrite lsr_spec; auto. replace (2^φ 1) with 2%Z; auto. split; auto with zarith. assert (φ i/2 < wB/2); auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. } apply Hrec; rewrite H; clear u H. + assert (Hf1: 0 <= Φ (WW ih il) / φ j) by (apply Z_div_pos; auto with zarith). case (Zle_lt_or_eq 1 (φ j)); auto with zarith; intros Hf2. split. * replace (φ j + Φ (WW ih il) / φ j)%Z with (1 * 2 + ((φ j - 2) + Φ (WW ih il) / φ j)) by lia. rewrite Z_div_plus_full_l; auto with zarith. assert (0 <= (φ j - 2 + Φ (WW ih il) / φ j) / 2) ; auto with zarith. * apply sqrt_test_false; auto with zarith. + apply sqrt_main; auto with zarith. - contradict Hij; apply Zle_not_lt. assert ((1 + φ j) <= 2 ^ (Z_of_nat size - 1)); auto with zarith. apply Z.le_trans with ((2 ^ (Z_of_nat size - 1)) ^2); auto with zarith. + assert (0 <= 1 + φ j); auto with zarith. apply Zmult_le_compat; auto with zarith. + change ((2 ^ (Z_of_nat size - 1))^2) with (2 ^ (Z_of_nat size - 2) * wB). apply Z.le_trans with (φ ih * wB); auto with zarith. unfold zn2z_to_Z, wB; auto with zarith. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63