proposition: Theorem error_lt_ulp : forall rnd { Zrnd : Valid_rnd rnd } x, (x <> 0)%R -> (Rabs (round beta fexp rnd x - x) < ulp x)%R.
proof: Proof. Proof with auto with typeclass_instances. intros rnd Zrnd x Zx. destruct (generic_format_EM beta fexp x) as [Hx|Hx]. rewrite round_generic... unfold Rminus. rewrite Rplus_opp_r, Rabs_R0. rewrite ulp_neq_0; trivial. apply bpow_gt_0. destruct (round_DN_or_UP beta fexp rnd x) as [H|H] ; rewrite H ; clear H. rewrite Rabs_left1. rewrite Ropp_minus_distr. apply Rplus_lt_reg_l with (round beta fexp Zfloor x). rewrite <- round_UP_DN_ulp with (1 := Hx). ring_simplify. assert (Hu: (x <= round beta fexp Zceil x)%R). apply round_UP_pt... destruct Hu as [Hu|Hu]. exact Hu. elim Hx. rewrite Hu. apply generic_format_round... apply Rle_minus. apply round_DN_pt... rewrite Rabs_pos_eq. rewrite round_UP_DN_ulp with (1 := Hx). apply Rplus_lt_reg_r with (x - ulp x)%R. ring_simplify. assert (Hd: (round beta fexp Zfloor x <= x)%R). apply round_DN_pt... destruct Hd as [Hd|Hd]. exact Hd. elim Hx. rewrite <- Hd. apply generic_format_round... apply Rle_0_minus. apply round_UP_pt... Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop