proposition: Lemma equivPrim_FloatInj {Tl} : forall (t : ArithExpr Tl Integer) (lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in eqExprTypePrim (evalPrim t lP) (evalRounded t lM mode_NE) -> Rabs (IZR (evalRounded t lM mode_NE)) <= Rpow2 53 -> eqExprTypePrim (evalPrim (FloatInj t) lP) (evalRounded (FloatInj t) lM mode_NE).
proof: Proof. intros t lP lM [bndt eqt] H. generalize (binary_normalize_correct _ _ HPrec_gt_0 HPrec_lt_emax mode_NE (evalRounded t lM mode_NE) 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, eqExprTypePrim. simpl. rewrite Rmult_1_r. revert H. rewrite <-eqt. unfold to_Z, Sint63.abs. rewrite lesb_ltb. rewrite <-is_finite_SF_B2SF. intros H [H1 [H2 _]]. rewrite <-B2SF_Prim2B, SF2R_B2SF. destruct Uint63.ltb eqn:Haux'. - apply Uint63.ltb_spec in Haux'. rewrite of_int63_equiv. change prec with Rrnd.prec. change emax with Rrnd.emax. split; [assumption |]. unfold HPrec_gt_0, HPrec_lt_emax in H1. 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. - rewrite is_finite_SF_B2SF in H2 |- *. rewrite opp_equiv, is_finite_Bopp, B2R_Bopp, of_int63_equiv. generalize (binary_normalize_correct prec emax Hprec Hmax mode_NE (Uint63.to_Z ((- evalPrim t lP)%sint63)%uint63) 0 false). unfold F2R. simpl. rewrite Rmult_1_r. rewrite Rlt_bool_true. 2: { rewrite <-Rabs_Ropp, <-round_NE_opp, <-opp_IZR, <-round_NE_abs; [| now apply fexp_correct]. apply (Rle_lt_trans _ (Rpow2 53)); [| now apply IZR_lt]. apply round_le_generic; [now apply fexp_correct | apply valid_rnd_N | | assumption]. now apply generic_format_fexp_IZR. } intros [H'1 [H'2 _]]. split; [easy |]. change Rrnd.prec with prec. change Rrnd.emax with emax. rewrite H'1, opp_IZR. apply f_equal. rewrite opp_IZR, <-Rabs_Ropp, Ropp_involutive, <-abs_IZR in H. apply le_IZR in H. apply round_generic; [apply valid_rnd_N |]. now apply generic_format_fexp_IZR. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)