proposition: Lemma equivPrim_FastNearbyint {Tl} : forall (t : ArithExpr Tl BinFloat) (lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in eqExprTypePrim (evalPrim t lP) (evalRounded t lM mode_NE) -> -2251799813685248 <= evalRounded t lM mode_NE <= 2251799813685247 -> eqExprTypePrim (evalPrim (FastNearbyint t) lP) (evalRounded (FastNearbyint t) lM mode_NE).
proof: Proof. intros t lP lM [finx eqt] [Hx0 Hx1]. simpl. unfold eqExprTypePrim, convertiblePrim, isConversionPrim in *. rewrite <-B2SF_Prim2B, is_finite_SF_B2SF in finx |- *. rewrite <-eqt, Prim2SF2R_Prim2B2R in Hx0, Hx1 |- *. set (x := (evalPrim t lP)). fold x in finx, Hx0, Hx1. rewrite sub_equiv, add_equiv. generalize (Bplus_correct prec emax Hprec Hmax mode_NE (Prim2B x) (Prim2B 6755399441055744) finx). 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. cut (Rpow2 52 <= B2R (Prim2B x) + B2R (Prim2B 6755399441055744) <= Rpow2 53 - 1); [unfold bpow, Z.pow_pos; simpl; lra |]. now apply aux_4. } generalize (Bminus_correct prec emax Hprec Hmax mode_NE (Bplus mode_NE (Prim2B x) (Prim2B 6755399441055744)) (Prim2B 6755399441055744) Hplus_2). rewrite Rlt_bool_true; [intros [Hminus_1 [Hminus_2 Hminus_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. rewrite Hplus_1. unfold round, F2R, scaled_mantissa, cexp. simpl Fnum. simpl Fexp. rewrite mag_unique_pos with (e := 53%Z); [cbn; unfold F2R; simpl; rewrite 3Rmult_1_r |]. 2: { cut (Rpow2 52 <= B2R (Prim2B x) + B2R (Prim2B 6755399441055744) <= Rpow2 53 - 1); [unfold bpow, Z.pow_pos; simpl; lra |]. now apply aux_4. } rewrite <-2minus_IZR; simpl. unfold Z.sub. rewrite ZnearestE_plus_even by easy. rewrite opp_IZR. rewrite Rplus_assoc, Rplus_opp_r, Rplus_0_r, <-opp_IZR. generalize (valid_rnd_N (fun n => negb (Z.even n))). intros Hmon. apply Hmon in Hx0, Hx1. rewrite Generic_proof.Znearest_IZR in Hx0, Hx1. split; apply IZR_le; lia. } split; [easy |]. rewrite SF2R_B2SF, Hminus_1, Hplus_1. set (x' := round _ _ _ (_ + _)). assert (Hx' : x' = x') by easy. unfold x' at 2 in Hx'. clearbody x'. unfold round, F2R, scaled_mantissa, cexp in Hx'. simpl in Hx'. rewrite mag_unique_pos with (e := 53%Z) in Hx'. 2: { cut (Rpow2 52 <= B2R (Prim2B x) + B2R (Prim2B 6755399441055744) <= Rpow2 53 - 1); [unfold bpow, Z.pow_pos; simpl; lra |]. now apply aux_4. } cbn in Hx' |- *. unfold F2R in Hx' |- *. simpl in Hx' |- *. rewrite 3Rmult_1_r in Hx'. rewrite <-ZnearestE_plus_even, plus_IZR in Hx' by easy. rewrite Hx'. ring_simplify (IZR (ZnearestE (B2R (Prim2B x))) + 6755399441055744 - 6755399441055744 * 1). unfold Rrnd.nearbyint. unfold round at 2. unfold F2R, scaled_mantissa; simpl. rewrite 2Rmult_1_r. apply round_generic; [apply valid_rnd_N |]. clear -Hx0 Hx1. apply (valid_rnd_N (fun n => negb (Z.even n))) in Hx0, Hx1. rewrite Generic_proof.Znearest_IZR in Hx0, Hx1. apply generic_format_FLT. now exists (Float radix2 (ZnearestE (B2R (Prim2B x))) 0); [unfold F2R; simpl; ring | simpl; lia |]. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)