proposition: Lemma equivPrim_FastNearbyintToInt {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) -> -2147483648 <= evalRounded t lM mode_NE <= 2147483647 -> eqExprTypePrim (evalPrim (FastNearbyintToInt t) lP) (evalRounded (FastNearbyintToInt t) lM mode_NE).
proof: Proof. intros t lP lM [finx eqt] H. simpl. unfold eqExprTypePrim, convertiblePrim, isConversionPrim in *. rewrite <-B2SF_Prim2B, is_finite_SF_B2SF in finx. rewrite <-eqt, Prim2SF2R_Prim2B2R in H |- *. set (x := evalPrim t lP). generalize (fastnearbyint_correct x). set (i := normfr_mantissa _). intros Hx. rewrite Sint63.sub_spec. unfold to_Z. cbn in H. fold x in H. destruct H as [Hx0 Hx1]. set (Rx := B2R (Prim2B x)). fold Rx in Hx0, Hx1. assert (HRx : (-2147483648 <= ZnearestE Rx <= 2147483647)%Z). { 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. } assert (Hi : (φ (i)%uint63 < φ (min_int)%uint63)%Z). { rewrite Hx; [| easy | unfold Rx in Hx0, Hx1; lra]. unfold min_int, Uint63.to_Z, x. simpl. rewrite Prim2SF2R_Prim2B2R. fold x Rx. lia. } destruct (Uint63.ltbP i min_int) as [_ | Hi_]; [| easy]. rewrite Hx; [| easy | unfold Rx in Hx0, Hx1; lra]. cbn. unfold Z.sub. rewrite <-Z.add_assoc. simpl. rewrite Z.add_0_r. rewrite cmod_small; [| rewrite Prim2SF2R_Prim2B2R; fold Rx; cbn; lia]. rewrite Prim2SF2R_Prim2B2R. now fold Rx. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)