proposition: Theorem error_le_half_ulp : forall choice x, (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * ulp x)%R.
proof: Proof. Proof with auto with typeclass_instances. intros choice x. destruct (generic_format_EM beta fexp x) as [Hx|Hx]. rewrite round_generic... unfold Rminus. rewrite Rplus_opp_r, Rabs_R0. apply Rmult_le_pos. apply Rlt_le. apply Rinv_0_lt_compat. now apply IZR_lt. apply ulp_ge_0. set (d := round beta fexp Zfloor x). destruct (round_N_pt beta fexp choice x) as (Hr1, Hr2). destruct (Rle_or_lt (x - d) (d + ulp x - x)) as [H|H]. apply Rle_trans with (Rabs (d - x)). apply Hr2. apply (round_DN_pt beta fexp x). rewrite Rabs_left1. rewrite Ropp_minus_distr. apply Rmult_le_reg_r with 2%R. now apply IZR_lt. apply Rplus_le_reg_r with (d - x)%R. ring_simplify. apply Rle_trans with (1 := H). right. field. apply Rle_minus. apply (round_DN_pt beta fexp x). assert (Hu: (d + ulp x)%R = round beta fexp Zceil x). unfold d. now rewrite <- round_UP_DN_ulp. apply Rle_trans with (Rabs (d + ulp x - x)). apply Hr2. rewrite Hu. apply (round_UP_pt beta fexp x). rewrite Rabs_pos_eq. apply Rmult_le_reg_r with 2%R. now apply IZR_lt. apply Rplus_le_reg_r with (- (d + ulp x - x))%R. ring_simplify. apply Rlt_le. apply Rlt_le_trans with (1 := H). right. field. apply Rle_0_minus. rewrite Hu. apply (round_UP_pt beta fexp x). Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop