proposition: Lemma Bsqrt_correct_aux : forall m mx ex (Hx : bounded mx ex = true), let x := F2R (Float radix2 (Zpos mx) ex) in let z := let '(mz, ez, lz) := SFsqrt_core_binary prec emax (Zpos mx) ex in binary_round_aux m false mz ez lz in valid_binary z = true /\ SF2R radix2 z = round radix2 fexp (round_mode m) (sqrt x) /\ is_finite_SF z = true /\ sign_SF z = false.
proof: Proof. Proof with auto with typeclass_instances. intros m mx ex Hx. unfold SFsqrt_core_binary. rewrite Zdigits2_Zdigits. set (e' := Z.min _ _). assert (2 * e' <= ex)%Z as He. { assert (e' <= Z.div2 ex)%Z by apply Z.le_min_r. rewrite (Zdiv2_odd_eqn ex). destruct Z.odd ; lia. } generalize (Fsqrt_core_correct radix2 (Zpos mx) ex e' eq_refl He). unfold Fsqrt_core. set (mx' := match (ex - 2 * e')%Z with Z0 => _ | _ => _ end). assert (mx' = Zpos mx * Zpower radix2 (ex - 2 * e'))%Z as <-. { unfold mx'. destruct (ex - 2 * e')%Z as [|p|p]. now rewrite Zmult_1_r. now rewrite Z.shiftl_mul_pow2. easy. } clearbody mx'. destruct Z.sqrtrem as [mz r]. set (lz := if Zeq_bool r 0 then _ else _). clearbody lz. intros Bz. refine (_ (binary_round_aux_correct' m (sqrt (F2R (Float radix2 (Zpos mx) ex))) mz e' lz _ _ _)) ; cycle 1. now apply Rgt_not_eq, sqrt_lt_R0, F2R_gt_0. rewrite Rabs_pos_eq. exact Bz. apply sqrt_ge_0. apply Z.le_trans with (1 := Z.le_min_l _ _). apply FLT_exp_monotone. rewrite mag_sqrt_F2R by easy. apply Z.le_refl. rewrite Rlt_bool_false by apply sqrt_ge_0. rewrite Rlt_bool_true. easy. rewrite Rabs_pos_eq. refine (_ (relative_error_FLT_ex radix2 emin prec (prec_gt_0 prec) (round_mode m) (sqrt (F2R (Float radix2 (Zpos mx) ex))) _)). fold fexp. intros (eps, (Heps, Hr)). change fexp with (FLT_exp emin prec). rewrite Hr. assert (Heps': (Rabs eps < 1)%R). apply Rlt_le_trans with (1 := Heps). fold (bpow radix2 0). apply bpow_le. generalize (prec_gt_0 prec). clear ; lia. apply Rsqr_incrst_0. 3: apply bpow_ge_0. rewrite Rsqr_mult. rewrite Rsqr_sqrt. 2: now apply F2R_ge_0. unfold Rsqr. apply Rmult_ge_0_gt_0_lt_compat. apply Rle_ge. apply Rle_0_sqr. apply bpow_gt_0. now apply bounded_lt_emax. apply Rlt_le_trans with 4%R. apply (Rsqr_incrst_1 _ 2). apply Rplus_lt_compat_l. apply (Rabs_lt_inv _ _ Heps'). rewrite <- (Rplus_opp_r 1). apply Rplus_le_compat_l. apply Rlt_le. apply (Rabs_lt_inv _ _ Heps'). now apply IZR_le. change 4%R with (bpow radix2 2). apply bpow_le. generalize (prec_gt_0 prec) (prec_lt_emax prec emax). clear ; lia. apply Rmult_le_pos. apply sqrt_ge_0. rewrite <- (Rplus_opp_r 1). apply Rplus_le_compat_l. apply Rlt_le. apply (Rabs_lt_inv _ _ Heps'). rewrite Rabs_pos_eq. 2: apply sqrt_ge_0. apply Rsqr_incr_0. 2: apply bpow_ge_0. 2: apply sqrt_ge_0. rewrite Rsqr_sqrt. 2: now apply F2R_ge_0. apply Rle_trans with (bpow radix2 emin). unfold Rsqr. rewrite <- bpow_plus. apply bpow_le. unfold emin. generalize (prec_lt_emax prec emax). clear ; lia. apply generic_format_ge_bpow with fexp. intros. apply Z.le_max_r. now apply F2R_gt_0. apply generic_format_canonical. now apply (canonical_bounded false). apply round_ge_generic... apply generic_format_0. apply sqrt_ge_0. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative