proposition: Lemma exp_aux_correct : forall x, is_finite (Prim2B x) = true -> (let lb := fst (exp_aux x) in F.valid_lb lb = true /\ match F.toX lb with | Xreal.Xnan => True | Xreal.Xreal r => r <= Rtrigo_def.exp (B2R (Prim2B x)) end) /\ (let ub := snd (exp_aux x) in F.valid_ub ub = true /\ match F.toX ub with | Xreal.Xnan => True | Xreal.Xreal r => Rtrigo_def.exp (B2R (Prim2B x)) <= r end).
proof: Proof. intros x Fx. unfold exp_aux. rewrite 2ltb_equiv, 2Bltb_correct by easy. set (xr := B2R (Prim2B x)). fold xr in Fx. case Rlt_bool_spec. { intros. change ((true = true /\ 0 <= Rtrigo_def.exp xr) /\ true = true /\ Rtrigo_def.exp xr <= 1 * Rpow2 (-1074)). clearbody xr. cbv -[Rinv Rmult Rlt IZR]in H. refine ((fun J => conj (conj eq_refl (proj1 J)) (conj eq_refl (proj2 J))) _). interval with (i_prec 80). } case Rlt_bool_spec. { intros. change ((true = true /\ IZR (9007199254740778 * 2 ^ 971) <= Rtrigo_def.exp xr) /\ true = true /\ True). clearbody xr. cbv -[Rinv Rmult Rlt IZR] in H. refine ((fun J => conj (conj eq_refl J) (conj eq_refl I)) _). interval with (i_prec 80). } intros H0 H1. assert (Hx : -6548164122079684 * Rpow2 (-43) <= xr <= 6243314768165359 * Rpow2 (-43)). { clearbody xr. cbv -[Rinv Rmult Rle IZR] in H0, H1 |- *. lra. } clear H0 H1. change 6755399440921280%uint63 with (PrimInt63.sub 6755399441055744 134464). rewrite sub_sub_assoc. set (ki := (normfr_mantissa _ - _)%uint63). replace (PrimInt63.land _ _) with (PrimInt63.land ki 63). 2: { rewrite <-(Uint63.of_to_Z (PrimInt63.land ki 63)), <-(Uint63.of_to_Z (PrimInt63.land (ki + 134464) 63)). rewrite 2land_spec', Uint63.add_spec. change (_ 63%uint63) with (Z.ones 6). rewrite 2Z.land_ones by easy. rewrite <-Znumtheory.Zmod_div_mod; [| easy | easy |]. 2: { now exists (2 ^ 57)%Z. } change (_ 134464%uint63) with (2101 * 64)%Z. now rewrite Z.mod_add by easy. } set (kr := PrimInt63.land ki 63). set (dlb := (-0x1.8p-57)%float). set (dub := 0x1.8p-57%float). set (d := 0x1.8p-57). assert (d = Rabs (SF2R radix2 (Prim2SF dlb)) /\ d = Rabs (SF2R radix2 (Prim2SF dub))) as [Hdlb Hdub]. { cbn. unfold F2R, d. cbn. change (Z.neg 6755399441055744) with (Z.opp 6755399441055744)%Z. rewrite opp_IZR, <-Ropp_mult_distr_l, Rabs_Ropp, Rabs_pos_eq; lra. } change (_ * _ + dlb)%float with (Pexp_no_const x kr dlb). change (_ * _ + dub)%float with (Pexp_no_const x kr dub). unfold xr in Hx |- *. clear xr. rewrite <-is_finite_SF_B2SF, B2SF_Prim2B in Fx. rewrite <-Prim2SF2R_Prim2B2R in Hx |- *. assert (Hxr_ : -746 <= SF2R radix2 (Prim2SF x) <= 710) by interval. unfold Interval.contains, I.convert. simpl. rewrite 2PrimitiveFloat.toX_Prim2B. unfold I.F.valid_lb, I.F.valid_ub. rewrite 2eqb_equiv, next_down_equiv, next_up_equiv, 2ldshiftexp_equiv. assert (Hki0 : -68736 <= IZR (to_Z ki) <= 65536). { change ki with (evalPrim (@k_64' nil) (x, tt)). remove_floats. split. { now simplify_wb. } cbn -[bpow]; unfold F2R; cbn -[bpow]. unfold Rrnd.rnd, round_mode. interval. } assert (Hki1 : (-68736 <= to_Z ki <= 65536)%Z). { destruct Hki0 as [Hki00 Hki01]. now apply le_IZR in Hki00, Hki01. } assert (Hki2 : (-1074 <= to_Z (asr ki 6) <= 1024)%Z). { rewrite asr_spec. destruct Hki1 as [Hki10 Hki11]. apply (Z.div_le_mono _ _ 64 ltac:(easy)) in Hki10, Hki11. cbn -[ki] in Hki10, Hki11 |- *. lia. } replace (Uint63.to_Z _) with ((to_Z (asr ki 6)) + 2101)%Z. 2: { rewrite asr_spec. rewrite <- Zdiv.Z_div_plus by easy. rewrite <-(cmod_small (_ + _)%Z wB) by (cbn -[ki]; lia). change (_ * _)%Z with (to_Z 134464). rewrite <-Sint63.add_spec, <-asr_spec. rewrite <-to_Z_mod_Uint63to_Z. rewrite Z.mod_small; [easy |]. rewrite asr_spec, Sint63.add_spec. rewrite cmod_small by (cbn -[ki]; lia). destruct Hki1 as [Hki10 Hki11]. apply (Z.div_le_mono _ _ 64 ltac:(easy)) in Hki10, Hki11. cbn -[ki] in Hki10, Hki11 |- *. change 134464%Z with (2101 * 64)%Z. rewrite Zdiv.Z_div_plus by easy. lia. } rewrite Z.add_simpl_r. assert (Hkr0 : (0 <= to_Z kr <= 63)%Z). { unfold kr. unfold to_Z. rewrite (proj2 (Uint63.ltb_spec _ _)). - rewrite land_spec'. change (Uint63.to_Z 63) with (Z.ones 6). rewrite Z.land_ones by easy. generalize (Z.mod_pos_bound (Uint63.to_Z ki) (2 ^ 6)%Z ltac:(easy)). lia. - rewrite land_spec'. change (Uint63.to_Z 63) with (Z.ones 6). rewrite Z.land_ones by easy. generalize (Z.mod_pos_bound (Uint63.to_Z ki) (2 ^ 6)%Z ltac:(easy)). change (Uint63.to_Z min_int) with 4611686018427387904%Z. lia. } assert (Hkr1 : to_Z kr = Uint63.to_Z kr). { rewrite <-(Z.mod_small (to_Z _) wB), <-to_Z_mod_Uint63to_Z; [easy |]. cbn -[kr]. lia. } assert (Hkr2 : (-2147483648 <= to_Z kr <= 2147483647)%Z) by lia. assert (Hkr3 : (0 <= IZR (to_Z kr) <= 63)) by (now split; apply IZR_le). set (k0 := (x * InvLog2_64 + 6755399441055744)%float). fold k0 in ki. set (C := SF2R radix2 (Prim2SF consts.[of_Z (to_Z kr)])). assert (0.984375 <= C <= 1.984375 /\ (Uint63.to_Z kr = 0%Z -> C = 1) /\ Rabs (C - Rtrigo_def.exp (IZR (Uint63.to_Z kr) * (Rpower.ln 2 / 64))) <= Rpow2 (-53)) as [bnd_C [HC1 HC2]]. { rewrite <-Hkr1. split; [| split]. 3: { now apply exp_consts_correct. } 2: { unfold C. intros ->. cbv -[IZR]. now apply Rinv_r, IZR_neq. } simpl. unfold C. replace (SF2R _ _) with (SF2R radix2 (Prim2SF consts.[of_Z (to_Z kr)]) - Rtrigo_def.exp (IZR (to_Z kr) * (Rpower.ln 2 / 64)) + Rtrigo_def.exp (IZR (to_Z kr) * (Rpower.ln 2 / 64))) by ring. generalize (exp_consts_correct (to_Z kr) Hkr0). generalize (SF2R radix2 (Prim2SF consts.[of_Z (to_Z kr)]) - Rtrigo_def.exp (IZR (to_Z kr) * (Rpower.ln 2 / 64))). intros; interval. } assert (Hb : forall d, is_finite_SF (Prim2SF d) = true -> Rabs (SF2R radix2 (Prim2SF d)) = 0x1.8p-57 -> Rabs (Generic_fmt.round radix2 (fexp prec emax) (round_mode mode_NE) (@evalRounded (BinFloat :: BinFloat :: Integer :: nil) _ (Op ADD (Var 0) (Var 1)) (SF2R radix2 (Prim2SF consts.[of_Z (to_Z kr)]), (SF2R radix2 (Prim2SF (Pexp_no_const x kr d)), (to_Z kr, tt))) mode_NE * Rpow2 (to_Z (ki >> 6)))) < 9007199254740991 * Rpow2 971). { intros d' Hd1 Hd2. refine (_ (exp_no_const_correct x d' Fx Hxr_ Hd1 _)). 2: rewrite Hd2 ; interval. intros [_ [_ [Hb2 [_ Hb3]]]]. fold k0 ki kr in Hb2, Hb3. cbn -[Pexp_no_const ki kr bpow consts]. revert Hx Hd2 Hb2 Hb3 Hki2 HC2. clear. fold C. set (Y := Rtrigo_def.exp _ + _). set (delt := C - _). set (kq := asr ki 6). intros [_ Hx] Hd2 HY'' HY' [_ Hkq] Hdelt. unfold Rrnd.rnd, round_mode. replace (C + _) with (Y + delt) by (unfold Y, delt; ring). unfold Rminus at 2 in HY'. rewrite exp_plus, exp_Ropp in HY'. replace (Rtrigo_def.exp (_ * _)) with (Rpow2 (to_Z kq)) in HY' by now rewrite bpow_exp. generalize (bpow_gt_0 radix2 (to_Z kq)). intros Haux. replace (Y - _) with ((Y * Rpow2 (to_Z kq) - Rtrigo_def.exp (SF2R radix2 (Prim2SF x))) / Rpow2 (to_Z kq) - SF2R radix2 (Prim2SF d')) in HY' by (field; lra). refine (_ (Rle_trans _ _ _ ltac:(apply Rabs_triang_inv) HY')). intros HY. clear HY'. apply Rcomplements.Rle_minus_l in HY. rewrite Hd2, Rcomplements.Rabs_div in HY by apply Rgt_not_eq, bpow_gt_0. assert (Hkq' : 0 <= Rpow2 (to_Z kq) <= Rpow2 1024). { split. apply bpow_ge_0. now apply bpow_le. } apply -> Rcomplements.Rle_div_l in HY ; [| now apply Rabs_gt; right]. apply (Rle_trans _ _ (0x1.8p-56 * Rpow2 1024)) in HY. 2: { apply Rmult_le_compat; [ interval | apply Rabs_pos | interval |]. now rewrite Rabs_pos_eq by lra. } unfold emax. assert (Hx' : 0 <= Rtrigo_def.exp (SF2R radix2 (Prim2SF x)) <= Rpow2 1024 - Rpow2 978) by interval with (i_prec 60). change (Generic_fmt.round _ _ _) with Rrnd.rnd. set (delt1 := Rrnd.rnd (Y + delt) - (Y + delt)). set (delt2 := Rrnd.rnd (Rrnd.rnd (Y + delt) * Rpow2 (to_Z kq)) - Rrnd.rnd (Y + delt) * Rpow2 (to_Z kq)). replace (Rrnd.rnd (_ * _)) with (delt2 + delt1 * Rpow2 (to_Z kq) + (Y * Rpow2 (to_Z kq) - Rtrigo_def.exp (SF2R radix2 (Prim2SF x))) + Rtrigo_def.exp (SF2R radix2 (Prim2SF x)) + delt * Rpow2 (to_Z kq)) by (unfold delt1, delt2; ring). revert HY. generalize (Y * Rpow2 (to_Z kq) - Rtrigo_def.exp (SF2R radix2 (Prim2SF x))). intros r Hr. unfold Rrnd.rnd, round_mode in delt1, delt2. interval with (i_prec 60). } assert (Haux_ : forall d, is_finite_SF (Prim2SF d) = true -> Rabs (SF2R radix2 (Prim2SF d)) <= 0x1p-52 -> Uint63.to_Z kr <> 0%Z -> 1.001 <= C + SF2R radix2 (Prim2SF (Pexp_no_const x kr d)) <= 1.999). { intros d' Hd1 Hd2 Hk. refine (_ (exp_no_const_correct x d' Fx Hxr_ Hd1 _)). 2: interval. intros [_ [_ [_ [Hb5 Hb3]]]]. fold k0 ki kr in Hb5, Hb3. replace (_ + _) with (C - Rtrigo_def.exp (IZR φ (kr)%uint63 * (Rpower.ln 2 / 64)) + (Rtrigo_def.exp (IZR φ (kr)%uint63 * (Rpower.ln 2 / 64)) + SF2R radix2 (Prim2SF (Pexp_no_const x kr d')) - (Rtrigo_def.exp (SF2R radix2 (Prim2SF x) - IZR (to_Z (ki >> 6)) * Rpower.ln 2) + SF2R radix2 (Prim2SF d'))) + Rtrigo_def.exp (SF2R radix2 (Prim2SF x) - IZR (to_Z (ki >> 6)) * Rpower.ln 2) + SF2R radix2 (Prim2SF d')) by ring. revert Hb3 HC2. generalize (C - Rtrigo_def.exp (IZR φ (kr)%uint63 * (Rpower.ln 2 / 64))). generalize (Rtrigo_def.exp (IZR φ (kr)%uint63 * (Rpower.ln 2 / 64)) + SF2R radix2 (Prim2SF (Pexp_no_const x kr d')) - (Rtrigo_def.exp (SF2R radix2 (Prim2SF x) - IZR (to_Z (ki >> 6)) * Rpower.ln 2) + SF2R radix2 (Prim2SF d'))). intros r0 r1 Hr0 Hr1. replace (SF2R radix2 (Prim2SF x) - IZR (to_Z (ki >> 6)) * Rpower.ln 2) with (SF2R radix2 (Prim2SF x) - IZR (to_Z (ki >> 6)) * Rpower.ln 2 - IZR φ (kr)%uint63 * (Rpower.ln 2 / 64) + IZR φ (kr)%uint63 * (Rpower.ln 2 / 64)) by ring. revert Hb5. generalize (SF2R radix2 (Prim2SF x) - IZR (to_Z (ki >> 6)) * Rpower.ln 2 - IZR φ (kr)%uint63 * (Rpower.ln 2 / 64)). intros r2 Hr2. assert (Hkr_ : 1 <= IZR (Uint63.to_Z kr) <= 63). { rewrite Hkr1 in Hkr0. split; apply IZR_le; [lia | easy]. } interval. } split. { generalize (exp_no_const_correct x dlb Fx Hxr_ eq_refl ltac:(cbn; interval)). intros [Hlb1 [Hlb4 [Hlb2 [Hlb5 Hlb3]]]]. fold k0 in Hlb1, Hlb2, Hlb3, Hlb4, Hlb5. fold ki in Hlb1, Hlb2, Hlb3, Hlb4, Hlb5. fold kr in Hlb1, Hlb2, Hlb3, Hlb4, Hlb5. generalize (Bldexp_correct _ _ Hprec Hmax mode_NE (Prim2B (consts.[kr] + Pexp_no_const x kr dlb)) (to_Z (ki >> 6))). specialize (Hb dlb eq_refl (eq_sym Hdlb)). change (consts.[kr] + Pexp_no_const x kr dlb)%float with (@evalPrim (BinFloat :: Integer :: nil) BinFloat (Op ADD (ArrayAcc consts (Var 1)) (Var 0)) (Pexp_no_const x kr dlb, (kr, tt))). rewrite <-Prim2SF2R_Prim2B2R. remove_floats. split. { split. split. split. cbn -[to_Z kr]. lia. split. easy. simpl. fold C. unfold Rrnd.rnd, round_mode. interval. } intros [Hconv _]. rewrite Rlt_bool_true. 2: { apply Rlt_le_trans with (1 := Hb). interval with (i_prec 60). } set (f := Bldexp _ _ _). intros [Heq [Hfin _]]. generalize (Bpred_correct prec emax Hprec Hmax f). rewrite Hfin, Heq. rewrite <-is_finite_SF_B2SF, B2SF_Prim2B. intros H. specialize (H Hconv). revert H. case Rlt_bool_spec. 2: { intros _ H. now rewrite <- (SF2B'_B2SF (Bpred f)), H. } intros _ [Heqpred [Hfinpred _]]. replace (Beqb _ _) with false. 2: { simpl. unfold Beqb, SFeqb, SFcompare. now destruct Bpred. } rewrite PrimitiveFloat.B2R_BtoX, Heqpred by easy. split; [easy |]. clear Hb Hconv. clear dependent f. simpl evalRounded. fold C. clearbody C. eapply Rle_trans. apply pred_FLT_shift_le. easy. apply valid_rnd_round_mode. apply generic_format_round. now apply FLT_exp_valid. apply valid_rnd_round_mode. unfold Rrnd.rnd, round_mode. interval. apply Rmult_le_reg_r with (Rpow2 (- to_Z (asr ki 6))). { apply bpow_gt_0. } rewrite Rmult_assoc. rewrite <-bpow_plus. rewrite Z.add_opp_diag_r, Rmult_1_r. rewrite bpow_exp, <-exp_plus, opp_IZR. change (IZR radix2) with 2. replace (Rtrigo_def.exp _) with (C + SF2R radix2 (Prim2SF (Pexp_no_const x kr dlb)) - (C - Rtrigo_def.exp (IZR φ (kr)%uint63 * (Rpower.ln 2 / 64))) - (Rtrigo_def.exp (IZR φ (kr)%uint63 * (Rpower.ln 2 / 64)) + SF2R radix2 (Prim2SF (Pexp_no_const x kr dlb)) - (Rtrigo_def.exp (SF2R radix2 (Prim2SF x) + - IZR (to_Z (ki >> 6)) * Rpower.ln 2) + SF2R radix2 (Prim2SF dlb))) - SF2R radix2 (Prim2SF dlb)) by ring. generalize Hlb3. unfold Rminus at 2. rewrite Ropp_mult_distr_l. generalize (Rtrigo_def.exp (IZR φ (kr)%uint63 * (Rpower.ln 2 / 64)) + SF2R radix2 (Prim2SF (Pexp_no_const x kr dlb)) - (Rtrigo_def.exp (SF2R radix2 (Prim2SF x) + - IZR (to_Z (ki >> 6)) * Rpower.ln 2) + SF2R radix2 (Prim2SF dlb))). intros r Hr. unfold Rrnd.rnd, round_mode. destruct (Z.eq_dec (Uint63.to_Z kr) 0) as [Hkr | Hkr]. - rewrite Hkr at 1. rewrite HC1 at 1 2 3 by easy. rewrite Rmult_0_l, exp_0, Rminus_eq_0, Rminus_0_r. apply Rle_trans with (1 + SF2R radix2 (Prim2SF (Pexp_no_const x kr dlb))). { apply pred_round_le_id. now apply FLT_exp_valid. apply valid_rnd_N. } apply Rabs_le_inv in Hr. change (SF2R radix2 (Prim2SF dlb)) with (-0x18000000000000p-109). lra. - apply Rle_trans with (C + SF2R radix2 (Prim2SF (Pexp_no_const x kr dlb)) - Rpow2 (-53)). 2: { revert HC2. generalize (C - Rtrigo_def.exp (IZR φ (kr)%uint63 * (Rpower.ln 2 / 64))). intros r0 Hr0. apply Rabs_le_inv in Hr, Hr0. change (SF2R radix2 (Prim2SF dlb)) with (-0x18000000000000p-109). lra. } specialize (Haux_ dlb eq_refl ltac:(rewrite <- Hdlb; interval) Hkr). revert Haux_. generalize (C + SF2R radix2 (Prim2SF (Pexp_no_const x kr dlb))). intros r0 Hr0. unfold pred, succ. rewrite Rle_bool_false by interval. rewrite 2Ropp_involutive. unfold pred_pos. unfold ulp, cexp. rewrite (mag_unique _ _ 1) by interval. rewrite Req_bool_false by interval. rewrite Req_bool_false by interval. cut (Generic_fmt.round radix2 (FLT_exp Rrnd.emin Rrnd.prec) ZnearestE r0 - r0 <= Rpow2 (FLT_exp emin prec 1) - Rpow2 (-53)). lra. interval. } clear dlb Hdlb. generalize (exp_no_const_correct x dub Fx Hxr_ eq_refl ltac:(cbn; interval)). intros [Hub1 [Hub4 [Hub2 [Hub5 Hub3]]]]. fold k0 in Hub1, Hub2, Hub3, Hub4, Hub5. fold ki in Hub1, Hub2, Hub3, Hub4, Hub5. fold kr in Hub1, Hub2, Hub3, Hub4, Hub5. generalize (Bldexp_correct _ _ Hprec Hmax mode_NE (Prim2B (consts.[kr] + Pexp_no_const x kr dub)) (to_Z (ki >> 6))). specialize (Hb dub eq_refl (eq_sym Hdub)). change (consts.[kr] + Pexp_no_const x kr dub)%float with (@evalPrim (BinFloat :: Integer :: nil) BinFloat (Op ADD (ArrayAcc consts (Var 1)) (Var 0)) (Pexp_no_const x kr dub, (kr, tt))). rewrite <-Prim2SF2R_Prim2B2R. remove_floats. split. { split. split. split. cbn -[to_Z kr]. lia. split. easy. simpl. fold C. unfold Rrnd.rnd, round_mode. interval. } intros [Hconv _]. rewrite Rlt_bool_true. 2: { apply Rlt_le_trans with (1 := Hb). interval with (i_prec 60). } set (f := Bldexp _ _ _). intros [Heq [Hfin _]]. generalize (Bsucc_correct prec emax Hprec Hmax f). rewrite Hfin, Heq. rewrite <-is_finite_SF_B2SF, B2SF_Prim2B. intros H. specialize (H Hconv). revert H. case Rlt_bool_spec. 2: { intros _ H. now rewrite <- (SF2B'_B2SF (Bsucc f)), H. } intros _ [Heqsucc [Hfinsucc _]]. replace (Beqb _ _) with false. 2: { simpl. unfold Beqb, SFeqb, SFcompare. simpl. simpl in Hfin, Hfinsucc. simpl in Hconv. rewrite <-B2SF_Prim2B, is_finite_SF_B2SF in Hconv. rewrite Hconv in Hfin. clear -Hfin Hfinsucc. now destruct (Bsucc f). } rewrite PrimitiveFloat.B2R_BtoX, Heqsucc by easy. split; [easy |]. clear Hb Hconv. clear dependent f. simpl evalRounded. fold C. clearbody C. eapply Rle_trans ; cycle 1. apply succ_FLT_shift_ge. easy. apply valid_rnd_round_mode. apply generic_format_round. now apply FLT_exp_valid. apply valid_rnd_round_mode. unfold Rrnd.rnd, round_mode. interval. apply Rmult_le_reg_r with (Rpow2 (- to_Z (asr ki 6))). { apply bpow_gt_0. } rewrite Rmult_assoc. rewrite <-bpow_plus. rewrite Z.add_opp_diag_r, Rmult_1_r. rewrite bpow_exp, <-exp_plus, opp_IZR. change (IZR radix2) with 2. replace (Rtrigo_def.exp _) with (C + SF2R radix2 (Prim2SF (Pexp_no_const x kr dub)) - (C - Rtrigo_def.exp (IZR φ (kr)%uint63 * (Rpower.ln 2 / 64))) - (Rtrigo_def.exp (IZR φ (kr)%uint63 * (Rpower.ln 2 / 64)) + SF2R radix2 (Prim2SF (Pexp_no_const x kr dub)) - (Rtrigo_def.exp (SF2R radix2 (Prim2SF x) + - IZR (to_Z (ki >> 6)) * Rpower.ln 2) + SF2R radix2 (Prim2SF dub))) - SF2R radix2 (Prim2SF dub)) by ring. generalize Hub3. unfold Rminus at 2. rewrite Ropp_mult_distr_l. generalize (Rtrigo_def.exp (IZR φ (kr)%uint63 * (Rpower.ln 2 / 64)) + SF2R radix2 (Prim2SF (Pexp_no_const x kr dub)) - (Rtrigo_def.exp (SF2R radix2 (Prim2SF x) + - IZR (to_Z (ki >> 6)) * Rpower.ln 2) + SF2R radix2 (Prim2SF dub))). intros r Hr. unfold Rrnd.rnd, round_mode. destruct (Z.eq_dec (Uint63.to_Z kr) 0) as [Hkr | Hkr]. - rewrite Hkr at 1. rewrite HC1 at 1 2 3 by easy. rewrite Rmult_0_l, exp_0, Rminus_eq_0, Rminus_0_r. apply Rle_trans with (1 + SF2R radix2 (Prim2SF (Pexp_no_const x kr dub))). 2: { apply succ_round_ge_id. now apply FLT_exp_valid. apply valid_rnd_N. } apply Rabs_le_inv in Hr. change (SF2R radix2 (Prim2SF dub)) with 0x18000000000000p-109. lra. - apply Rle_trans with (C + SF2R radix2 (Prim2SF (Pexp_no_const x kr dub)) + Rpow2 (-53)). { revert HC2. generalize (C - Rtrigo_def.exp (IZR φ (kr)%uint63 * (Rpower.ln 2 / 64))). intros r0 Hr0. apply Rabs_le_inv in Hr, Hr0. change (SF2R radix2 (Prim2SF dub)) with 0x18000000000000p-109. lra. } specialize (Haux_ dub eq_refl ltac:(rewrite <- Hdub; interval) Hkr). revert Haux_. generalize (C + SF2R radix2 (Prim2SF (Pexp_no_const x kr dub))). intros r0 Hr0. unfold pred, succ. rewrite Rle_bool_true by interval. unfold ulp, cexp. rewrite (mag_unique _ _ 1) by interval. rewrite Req_bool_false by interval. cut (- (Generic_fmt.round radix2 (FLT_exp Rrnd.emin Rrnd.prec) ZnearestE r0 - r0) <= Rpow2 (FLT_exp emin prec 1) - Rpow2 (-53)). lra. interval. Qed.
imports: Coq(Reals Psatz PrimInt63 Uint63 Sint63 PArray Floats) Flocq(Core PrimFloat BinarySingleNaN) Missing.Flocq Xreal Basic Sig Interval Float Float_full Specific_bigint Specific_ops Primitive_ops Lang_expr Lang_tac Interval_helper