proposition: Lemma equivFloat_FloatInj {Tl} : forall (t : ArithExpr Tl Integer) (lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in eqExprTypeFloat (evalFloat t lC md) (evalRounded t lM md) -> Rabs (IZR (evalRounded t lM md)) <= Rpow2 53 -> eqExprTypeFloat (evalFloat (FloatInj t) lC md) (evalRounded (FloatInj t) lM md).
proof: Proof. intros t lC md lM [bndt eqt] H. generalize (binary_normalize_correct _ _ HPrec_gt_0 HPrec_lt_emax mode_NE (evalRounded t lM md) 0%Z false). simpl. rewrite Rlt_bool_true. 2: { unfold F2R. simpl. rewrite Rmult_1_r. apply (Rle_lt_trans _ (IZR (Z.pow_pos 2 53))); [| now apply IZR_lt]. rewrite <-round_NE_abs; [| now apply fexp_correct]. unfold Rpow2 in H. apply round_le_generic; [now apply fexp_correct | apply valid_rnd_N | | apply H]. now apply generic_format_fexp_IZR. } unfold F2R, eqExprTypeFloat. simpl. rewrite Rmult_1_r. intros [H1 [H2 _]]. rewrite eqt. split; [easy | unfold binnorm; rewrite H1]. apply round_generic; [apply valid_rnd_N |]. rewrite <-abs_IZR in H. apply le_IZR in H. now apply generic_format_fexp_IZR. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)