proposition: Lemma fastnearbyint_correct : forall x, is_finite (Prim2B x) = true -> -2251799813685248 <= B2R (Prim2B x) <= 2251799813685247 -> Uint63.to_Z (normfr_mantissa (fst (frshiftexp (x + 6755399441055744)))) = (ZnearestE (SF2R radix2 (Prim2SF x)) + 6755399441055744)%Z.
proof: Proof. intros x Hfinx Hx. destruct frshiftexp as (m, e) eqn:Heqaux. simpl. rewrite normfr_mantissa_equiv. assert (Hbndexpr_aux : Rpow2 52 <= B2R (Prim2B x) + B2R (Prim2B 6755399441055744) <= Rpow2 53 - 1) by now apply aux_4. generalize (Bplus_correct prec emax Hprec Hmax mode_NE (Prim2B x) (Prim2B 6755399441055744) Hfinx). rewrite Rlt_bool_true; [intros [Hplus_1 [Hplus_2 Hplus_3]]; [easy |] |]. 2: { apply Rlt_trans with (Rpow2 53); [| now apply bpow_lt]. rewrite <-round_NE_abs by now apply FLT_exp_valid. apply aux_3, Rabs_le. generalize (aux_4 _ Hx); cbn -[Rle Rplus IZR Prim2B]. lra. } assert (Hx' : Rpow2 52 <= B2R (Prim2B (x + 6755399441055744)) < Rpow2 53). { rewrite add_equiv, Hplus_1. split. - now apply round_ge_generic; [apply FLT_exp_valid | apply valid_rnd_N | apply generic_format_bpow | apply aux_4]. - now apply aux_3, aux_4. } assert (Hfinsx : is_finite_strict (Prim2B (x + 6755399441055744)) = true). { unfold is_finite_strict. destruct (Prim2B (x + 6755399441055744)); [.. | easy]; simpl in Hx'; lra. } generalize (frshiftexp_equiv (x + 6755399441055744)). rewrite Heqaux. intros Hfrexp_aux. simpl. generalize (Bfrexp_correct prec emax Hprec (Prim2B (x + 6755399441055744)) Hfinsx). rewrite <-Hfrexp_aux. intros [Hfrexp_1 [Hfrexp_2 Hfrexp_3]]; [easy |]. clear Hfinsx Heqaux Hfrexp_aux . generalize (Bnormfr_mantissa_correct prec emax Hprec (Prim2B m) Hfrexp_2). intros Hnormfr. destruct (Prim2B m) as [| | | sm mm em Hem]; [easy.. |]. destruct Hnormfr as [Hnormfr_1 [Hnormfr_2 ->]]. rewrite Hnormfr_1. simpl. set (e' := mag_val _ _ (mag radix2 (B2R (Prim2B (x + 6755399441055744))))). fold e' in Hfrexp_3. rewrite add_equiv in Hx', Hfrexp_1. rewrite Hfrexp_3 in Hfrexp_1. rewrite Hfrexp_1 in Hplus_1, Hx'. assert (He' : e' = 53%Z). { clear -Hx' Hfrexp_2. rewrite <-(Rabs_pos_eq (B2R _)) in Hx'. 2: { clear Hfrexp_2. clearbody e'. generalize (bpow_gt_0 radix2 e'). cbn -[Rle Rlt Rmult B2R prec] in Hx'. nra. } revert Hx' Hfrexp_2. generalize (Rabs (B2R (B754_finite sm mm (- prec) Hem))). intros r H0 Hr. generalize H0; intros H1. destruct H0 as [H00 H01]. destruct H1 as [H10 H11]. apply (Rmult_le_compat_r (Rpow2 (-54))) in H00; [| now apply bpow_ge_0]. apply (Rmult_lt_compat_r (Rpow2 (-54))) in H01; [| now apply bpow_gt_0]. apply (Rmult_le_compat_r (Rpow2 (-52))) in H10; [| now apply bpow_ge_0]. apply (Rmult_lt_compat_r (Rpow2 (-52))) in H11; [| now apply bpow_gt_0]. rewrite <-bpow_plus in H00, H01, H10, H11. simpl Z.add in H00, H01, H10, H11. assert (Hr' : 0 < r) by lra. change (/ 2) with (Rpow2 (-1)) in Hr. change 1 with (Rpow2 0) in Hr. assert (Haux: Rpow2 (-54) * Rpow2 (e') < 1 < Rpow2 (-52) * Rpow2 (e')) by nra. change 1 with (Rpow2 0) in Haux. rewrite <-2bpow_plus in Haux. destruct Haux as [Hauxl Hauxr]. apply lt_bpow in Hauxl, Hauxr. lia. } rewrite He' in Hplus_1. rewrite <-2Prim2SF2R_Prim2B2R in Hplus_1. unfold B2R, F2R in Hplus_1. simpl in Hplus_1. field_simplify in Hplus_1; [| lra]. clear -Hbndexpr_aux Hplus_1 Hx'. destruct sm; [unfold B2R, F2R in Hx'; simpl in Hx' |]. { assert (IZR (Z.neg mm) < 0) by now apply IZR_lt. cbn -[IZR Rle Rmult Rinv bpow] in Hx'. generalize (bpow_gt_0 radix2 e'). nra. } simpl in Hplus_1. apply eq_IZR. rewrite Hplus_1. unfold round, F2R, scaled_mantissa; simpl. unfold cexp. rewrite <-2Prim2SF2R_Prim2B2R in Hbndexpr_aux. rewrite mag_unique_pos with (e := 53%Z) by (simpl Z.sub; lra). cbn. unfold F2R. simpl. rewrite 3Rmult_1_r. f_equal. symmetry. now apply ZnearestE_plus_even. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)