proposition: Lemma equivFloat_FastNearbyintToInt {Tl} : forall (t : ArithExpr Tl BinFloat) (lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in eqExprTypeFloat (evalFloat t lC md) (evalRounded t lM md) -> (-2147483648 <= evalRounded t lM md <= 2147483647)%R -> eqExprTypeFloat (evalFloat (FastNearbyintToInt t) lC md) (evalRounded (FastNearbyintToInt t) lM md).
proof: Proof. intros t lC md lM [finx eqt] [Hx0 Hx1]. simpl. unfold eqExprTypeFloat, convertibleFloat, isConversionFloat in *. change Rrnd.prec with prec in *. change Rrnd.emax with emax in *. rewrite <-eqt in Hx0, Hx1 |- *. set (x := evalFloat t lC md). fold x in finx, Hx0, Hx1 |- *. generalize (Bplus_correct prec emax Hprec Hmax mode_NE x (Prim2B 6755399441055744) finx eq_refl). rewrite Rlt_bool_true; [intros [Hplus_1 [Hplus_2 _]] |]. 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 prec emax x + B2R (Prim2B 6755399441055744) <= Rpow2 53 - 1); [unfold bpow, Z.pow_pos; simpl; lra |]. apply aux_4. lra. } generalize (Bminus_correct prec emax Hprec Hmax mode_NE (@Bplus prec emax _ _ mode_NE x (Prim2B 6755399441055744)) (Prim2B 6755399441055744) Hplus_2 eq_refl). rewrite Rlt_bool_true; [intros [Hminus_1 _] |]. 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 prec emax x + B2R (Prim2B 6755399441055744) <= Rpow2 53 - 1); [unfold bpow, Z.pow_pos; simpl; lra |]. apply aux_4. lra. } 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; [apply Int32.in_bounds_norm |]. unfold FPsub, FPadd. change Rrnd.prec with prec. change Rrnd.emax with emax. unfold FPtrunc, HPrec_gt_0, HPrec_lt_emax. assert (H : @Btrunc Rrnd.prec Rrnd.emax (@Bminus prec emax Hprec Hmax mode_NE (@Bplus prec emax Hprec Hmax mode_NE x (Prim2B 6755399441055744)) (Prim2B 6755399441055744)) = ZnearestE (@B2R prec emax x)). { apply eq_IZR. rewrite Btrunc_correct by easy. change Rrnd.prec with prec. change Rrnd.emax with emax. rewrite 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 prec emax x + B2R (Prim2B 6755399441055744) <= Rpow2 53 - 1); [unfold bpow, Z.pow_pos; simpl; lra |]. apply aux_4. lra. } 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 prec emax x)) + 6755399441055744 - 6755399441055744 * 1). rewrite round_generic. 2: apply valid_rnd_ZR. { 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 prec emax x)) 0); [unfold F2R; simpl; ring | simpl; lia |]. } apply generic_round_generic; auto with typeclass_instances; [now apply fexp_correct |]. rewrite <-round_FIX_IZR. apply generic_format_round; auto with typeclass_instances. } rewrite Int32.norm_in_bounds; [easy |]. rewrite H. split; cbn. - apply Z.le_trans with (2 := Znearest_ge_floor _ _). now apply Zfloor_lub. - apply Z.le_trans with (1 := Znearest_le_ceil _ _). now apply Zceil_glb. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)