proposition: Lemma of_int63_exact i : (Int63.to_Z i <= 2^53)%Z -> toX (of_int63 i) = Xreal (IZR (Int63.to_Z i)).
proof: Proof. rewrite toX_Prim2B, of_int63_equiv. rewrite Z.le_lteq; intros [Hi| ->]; [ |now compute]. generalize (binary_normalize_correct _ _ Hprec Hmax mode_NE (Int63.to_Z i) 0 false). simpl. rewrite Generic_fmt.round_generic. 2:{ apply Generic_fmt.valid_rnd_N. } 2:{ apply FLT.generic_format_FLT. set (f := Defs.Float _ _ _). apply (FLT.FLT_spec _ _ _ _ f); [reflexivity| |now simpl]. now rewrite Z.abs_eq; [ |apply to_Z_bounded]. } unfold Defs.F2R; simpl; rewrite Rmult_1_r. rewrite Rlt_bool_true. 2:{ rewrite Rabs_pos_eq; [ |now apply IZR_le, to_Z_bounded]. apply IZR_lt, (Z.lt_trans _ _ _ Hi). fold (2 ^ 1024)%Z; apply Zpow_facts.Zpower_lt_monotone; lia. } intros [H [H' _]]; revert H H'. case binary_normalize as [s|s| |s m e B]; [now intros <-|now simpl..| ]. now intros <- _; simpl; rewrite FtoR_split. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig