proposition: Theorem Fsqrt_core_correct : forall m1 e1 e, (0 < m1)%Z -> (2 * e <= e1)%Z -> let '(m, l) := Fsqrt_core m1 e1 e in inbetween_float beta m e (sqrt (F2R (Float beta m1 e1))) l.
proof: Proof. intros m1 e1 e Hm1 He. unfold Fsqrt_core. set (m' := Zmult _ _). assert (0 <= m')%Z as Hm'. { apply Z.mul_nonneg_nonneg. now apply Zlt_le_weak. apply Zpower_ge_0. } assert (sqrt (F2R (Float beta m1 e1)) = sqrt (IZR m') * bpow e)%R as Hf. { rewrite <- (sqrt_Rsqr (bpow e)) by apply bpow_ge_0. rewrite <- sqrt_mult. unfold Rsqr, m'. rewrite mult_IZR, IZR_Zpower by lia. rewrite Rmult_assoc, <- 2!bpow_plus. now replace (_ + _)%Z with e1 by ring. now apply IZR_le. apply Rle_0_sqr. } generalize (Z.sqrtrem_spec m' Hm'). destruct Z.sqrtrem as [q r]. intros [Hq Hr]. rewrite Hf. unfold inbetween_float, F2R. simpl Fnum. apply inbetween_mult_compat. apply bpow_gt_0. rewrite Hq. case Zeq_bool_spec ; intros Hr'. rewrite Hr', Zplus_0_r, mult_IZR. fold (Rsqr (IZR q)). rewrite sqrt_Rsqr. now constructor. apply IZR_le. clear -Hr ; lia. constructor. split. apply Rle_lt_trans with (sqrt (IZR (q * q))). rewrite mult_IZR. fold (Rsqr (IZR q)). rewrite sqrt_Rsqr. apply Rle_refl. apply IZR_le. clear -Hr ; lia. apply sqrt_lt_1. rewrite mult_IZR. apply Rle_0_sqr. rewrite <- Hq. now apply IZR_le. apply IZR_lt. lia. apply Rlt_le_trans with (sqrt (IZR ((q + 1) * (q + 1)))). apply sqrt_lt_1. rewrite <- Hq. now apply IZR_le. rewrite mult_IZR. apply Rle_0_sqr. apply IZR_lt. ring_simplify. lia. rewrite mult_IZR. fold (Rsqr (IZR (q + 1))). rewrite sqrt_Rsqr. apply Rle_refl. apply IZR_le. clear -Hr ; lia. rewrite Rcompare_half_r. generalize (Rcompare_sqr (2 * sqrt (IZR (q * q + r))) (IZR q + IZR (q + 1))). rewrite 2!Rabs_pos_eq. intros <-. replace ((2 * sqrt (IZR (q * q + r))) * (2 * sqrt (IZR (q * q + r))))%R with (4 * Rsqr (sqrt (IZR (q * q + r))))%R by (unfold Rsqr ; ring). rewrite Rsqr_sqrt. rewrite <- plus_IZR, <- 2!mult_IZR. rewrite Rcompare_IZR. replace ((q + (q + 1)) * (q + (q + 1)))%Z with (4 * (q * q) + 4 * q + 1)%Z by ring. generalize (Zle_cases r q). case (Zle_bool r q) ; intros Hr''. change (4 * (q * q + r) < 4 * (q * q) + 4 * q + 1)%Z. lia. change (4 * (q * q + r) > 4 * (q * q) + 4 * q + 1)%Z. lia. rewrite <- Hq. now apply IZR_le. rewrite <- plus_IZR. apply IZR_le. clear -Hr ; lia. apply Rmult_le_pos. now apply IZR_le. apply sqrt_ge_0. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits Generic_fmt Float_prop Bracket