proposition: Lemma pow2_UP_correct : forall p s, (valid_ub (pow2_UP p s) = true /\ le_upper (Xscale radix2 (Xreal 1) (StoZ s)) (toX (pow2_UP p s))).
proof: Proof. intros p s. unfold pow2_UP, emax. case Zle_bool_spec; [easy| ]; intro Hs1. destruct (Z.le_ge_cases s (- 1074)) as [Hs2 | Hs2]. { rewrite (Z.max_r _ _ Hs2). cbn -[FtoR]. split; [easy| ]. rewrite FtoR_split. simpl. rewrite Float_prop.F2R_bpow. rewrite Rmult_1_l. apply bpow_le. easy. } rewrite (Z.max_l _ _ Hs2). unfold scale, valid_ub, toX, toF. rewrite <- (B2Prim_Prim2B (ldshiftexp (fromZ 1) (of_Z s + of_Z FloatOps.shift))) at 1. rewrite <-B2SF_Prim2B. rewrite ldshiftexp_equiv. set (e := (to_Z (of_Z s + of_Z FloatOps.shift) - FloatOps.shift)%Z). generalize (Bldexp_correct _ _ _ _ mode_NE (Prim2B (fromZ 1)) e). unfold e. rewrite Int63.add_spec. rewrite 2!Int63.of_Z_spec. rewrite <-Z.add_mod by easy. rewrite Z.mod_small. 2: { change wB with 9223372036854775808%Z. unfold FloatOps.shift. lia. } ring_simplify (s + FloatOps.shift - FloatOps.shift)%Z. change (fromZ 1) with 1%float. replace (B2R (Prim2B 1)) with 1%R; [ |cbn; unfold Defs.F2R; cbn; unfold Prim2B; now apply Rinv_r_sym]. rewrite Rmult_1_l. rewrite Generic_fmt.round_generic. 2: apply valid_rnd_round_mode. 2: { apply Generic_fmt.generic_format_bpow. unfold fexp, FloatOps.prec, SpecFloat.emin, emax. lia. } rewrite Rlt_bool_true. 2: rewrite Rabs_pos_eq; [now apply bpow_lt | apply bpow_ge_0]. set (t := Bldexp mode_NE (Prim2B 1) s). intros [H1 [H2 H3]]. destruct t as [sg | | | sg mt ex] eqn:Ht ; try easy. { contradict H1. apply Rlt_not_eq. apply bpow_gt_0. } split. - rewrite neg_infinity_equiv. rewrite eqb_equiv. now rewrite 2Prim2B_B2Prim. - simpl. rewrite Rmult_1_l. unfold StoZ. rewrite <- H1. rewrite FtoR_split. apply Rle_refl. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig