proposition: Theorem error_le_half_ulp_round : forall { Hm : Monotone_exp fexp }, forall choice x, (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * ulp (round beta fexp (Znearest choice) x))%R.
proof: Proof. Proof with auto with typeclass_instances. intros Hm choice x. case (Req_dec (round beta fexp (Znearest choice) x) 0); intros Hfx. case (Req_dec x 0); intros Hx. apply Rle_trans with (1:=error_le_half_ulp _ _). rewrite Hx, round_0... right; ring. generalize (error_le_half_ulp choice x). rewrite Hfx. unfold Rminus; rewrite Rplus_0_l, Rabs_Ropp. intros N. unfold ulp; rewrite Req_bool_true; trivial. case negligible_exp_spec'. intros (H1,H2). contradict Hfx. apply round_neq_0_negligible_exp... intros (n,(H1,Hn)); rewrite H1. apply Rle_trans with (1:=N). right; apply f_equal. rewrite ulp_neq_0; trivial. apply f_equal. unfold cexp. apply valid_exp; trivial. cut (mag beta x -1 < fexp n)%Z. lia. apply lt_bpow with beta. destruct (mag beta x) as (e,He). simpl. apply Rle_lt_trans with (Rabs x). now apply He. apply Rle_lt_trans with (Rabs (round beta fexp (Znearest choice) x - x)). right; rewrite Hfx; unfold Rminus; rewrite Rplus_0_l. apply sym_eq, Rabs_Ropp. apply Rlt_le_trans with (ulp 0). rewrite <- Hfx. apply error_lt_ulp_round... unfold ulp; rewrite Req_bool_true, H1; trivial. now right. case (round_DN_or_UP beta fexp (Znearest choice) x); intros Hx. destruct (Rle_or_lt 0 x) as [H|H]. rewrite Hx at 2. rewrite ulp_DN by easy. apply error_le_half_ulp. apply Rle_trans with (1:=error_le_half_ulp _ _). apply Rmult_le_compat_l. apply Rlt_le, pos_half_prf. apply ulp_le. rewrite Rabs_left1 by now apply Rlt_le. rewrite Hx. rewrite Rabs_left1. apply Ropp_le_contravar. apply round_DN_pt... apply round_le_generic... apply generic_format_0. now apply Rlt_le. destruct (Rle_or_lt 0 x) as [H|H]. apply Rle_trans with (1:=error_le_half_ulp _ _). apply Rmult_le_compat_l. apply Rlt_le, pos_half_prf. apply ulp_le_pos; trivial. rewrite Hx; apply (round_UP_pt beta fexp x). rewrite Hx at 2; rewrite <- (ulp_opp (round beta fexp Zceil x)). rewrite <- round_DN_opp. rewrite ulp_DN; trivial. pattern x at 1 2; rewrite <- Ropp_involutive. rewrite round_N_opp. unfold Rminus. rewrite <- Ropp_plus_distr, Rabs_Ropp. apply error_le_half_ulp. rewrite <- Ropp_0. apply Ropp_le_contravar. now apply Rlt_le. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop