proposition: Theorem error_lt_ulp_round : forall { Hm : Monotone_exp fexp } rnd { Zrnd : Valid_rnd rnd } x, (x <> 0)%R -> (Rabs (round beta fexp rnd x - x) < ulp (round beta fexp rnd x))%R.
proof: Proof. Proof with auto with typeclass_instances. intros Hm. cut (forall rnd : R -> Z, Valid_rnd rnd -> forall x : R, (0 < x)%R -> (Rabs (round beta fexp rnd x - x) < ulp (round beta fexp rnd x))%R). intros M rnd Hrnd x Zx. case (Rle_or_lt 0 x). intros H; destruct H. now apply M. contradict H; now apply sym_not_eq. intros H. rewrite <- (Ropp_involutive x). rewrite round_opp, ulp_opp. replace (- round beta fexp (Zrnd_opp rnd) (- x) - - - x)%R with (-(round beta fexp (Zrnd_opp rnd) (- x) - (-x)))%R by ring. rewrite Rabs_Ropp. apply M. now apply valid_rnd_opp. now apply Ropp_0_gt_lt_contravar. intros rnd Hrnd x Hx. apply Rlt_le_trans with (ulp x). apply error_lt_ulp... now apply Rgt_not_eq. rewrite <- ulp_DN; trivial. apply ulp_le_pos. apply round_ge_generic... apply generic_format_0. now apply Rlt_le. case (round_DN_or_UP beta fexp rnd x); intros V; rewrite V. apply Rle_refl. apply Rle_trans with x. apply round_DN_pt... apply round_UP_pt... now apply Rlt_le. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop