proposition: Lemma equivPrim_Nearbyint {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) -> eqExprTypePrim (evalPrim (Nearbyint t) lP) (evalRounded (Nearbyint t) lM mode_NE).
proof: Proof. intros t lP lM [fint eqt]. generalize (Bnearbyint_correct _ _ HPrec_lt_emax mode_NE (P2C (evalPrim t lP))). unfold eqExprTypePrim. simpl. rewrite <-2is_finite_SF_B2SF. intros [H0 [H1 _]]. unfold FPnearbyint. rewrite <-B2SF_Prim2B, SF2R_B2SF, Prim2B_B2Prim. change prec with Rrnd.prec. change emax with Rrnd.emax. rewrite <-eqt, H1, H0. rewrite B2SF_Prim2B. split; [easy |]. now rewrite <-B2SF_Prim2B, SF2R_B2SF. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)