proposition: Lemma equivPrim_TruncToInt {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) -> (- Int32.N / 2 <= Ztrunc (evalRounded t lM mode_NE) <= Int32.N / 2 - 1)%Z -> eqExprTypePrim (evalPrim (TruncToInt t) lP) (evalRounded (TruncToInt t) lM mode_NE).
proof: Proof. intros t lP lM [fint eqt] H. generalize (Btrunc_correct _ _ HPrec_lt_emax (P2C (evalPrim t lP))). unfold eqExprTypePrim. simpl. rewrite round_FIX_IZR. intros H0. apply eq_IZR in H0. revert H. rewrite <-eqt, <-B2SF_Prim2B, SF2R_B2SF. change prec with Rrnd.prec. change emax with Rrnd.emax. rewrite <-H0. unfold FPtrunc. intros H. now rewrite Sint63.of_Z_spec, Sint63.cmod_small; [| clear -H; cbn in *; lia]. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)