proposition: Theorem round_UP_plus_eps_pos : forall x, (0 <= x)%R -> F x -> forall eps, (0 < eps <= ulp x)%R -> round beta fexp Zceil (x + eps) = (x + ulp x)%R.
proof: Proof. Proof with auto with typeclass_instances. intros x Zx Fx eps. case Zx; intros Zx1. intros (Heps1,[Heps2|Heps2]). assert (Heps: (0 <= eps < ulp x)%R). split. now apply Rlt_le. exact Heps2. assert (Hd := round_DN_plus_eps_pos x Zx Fx eps Heps). rewrite round_UP_DN_ulp. rewrite Hd. rewrite 2!ulp_neq_0. unfold cexp. now rewrite mag_plus_eps. now apply Rgt_not_eq. now apply Rgt_not_eq, Rplus_lt_0_compat. intros Fs. rewrite round_generic in Hd... apply Rgt_not_eq with (2 := Hd). pattern x at 2 ; rewrite <- Rplus_0_r. now apply Rplus_lt_compat_l. rewrite Heps2. apply round_generic... now apply generic_format_succ_aux1. rewrite <- Zx1, 2!Rplus_0_l. intros Heps. case (proj2 Heps). unfold round, scaled_mantissa, cexp. unfold ulp. rewrite Req_bool_true; trivial. case negligible_exp_spec. lra. intros n Hn H. assert (fexp (mag beta eps) = fexp n). apply valid_exp; try assumption. cut (mag beta eps-1 < fexp n)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (2:=H). destruct (mag beta eps) as (e,He). simpl; rewrite Rabs_pos_eq in He. now apply He, Rgt_not_eq. now left. replace (Zceil (eps * bpow (- fexp (mag beta eps)))) with 1%Z. unfold F2R; simpl; rewrite H0; ring. apply sym_eq, Zceil_imp. split. simpl; apply Rmult_lt_0_compat. apply Heps. apply bpow_gt_0. apply Rmult_le_reg_r with (bpow (fexp n)). apply bpow_gt_0. rewrite Rmult_assoc, <- bpow_plus. rewrite H0; ring_simplify (-fexp n + fexp n)%Z. simpl; rewrite Rmult_1_l, Rmult_1_r. now left. intros P; rewrite P. apply round_generic... apply generic_format_ulp_0. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop