proposition: Lemma equivFloat_TruncToInt {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) -> (- Int32.N / 2 <= Ztrunc (evalRounded t lM md) <= Int32.N / 2 - 1)%Z -> eqExprTypeFloat (evalFloat (TruncToInt t) lC md) (evalRounded (TruncToInt t) lM md).
proof: Proof. intros t lC md lM [fint eqt] H. generalize (Btrunc_correct _ _ HPrec_lt_emax (evalFloat t lC md)). unfold eqExprTypeFloat. simpl. rewrite round_FIX_IZR. intros H0. apply eq_IZR in H0. rewrite <-eqt, <-H0 in H |- *. unfold FPtrunc. rewrite Int32.norm_in_bounds; [| easy]. now split. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)