proposition: Theorem relative_error_round : (0 < p)%Z -> forall x, (bpow emin <= Rabs x)%R -> (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs (round beta fexp rnd x))%R.
proof: Proof. Proof with auto with typeclass_instances. intros Hp x Hx. assert (Hx': (x <> 0)%R). intros T; contradict Hx; rewrite T, Rabs_R0. apply Rlt_not_le, bpow_gt_0. apply Rlt_le_trans with (ulp beta fexp x)%R. now apply error_lt_ulp. rewrite ulp_neq_0; trivial. unfold cexp. destruct (mag beta x) as (ex, He). simpl. specialize (He Hx'). assert (He': (emin < ex)%Z). apply (lt_bpow beta). apply Rle_lt_trans with (2 := proj2 He). exact Hx. apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R. rewrite <- bpow_plus. apply bpow_le. generalize (Hmin ex). lia. apply Rmult_le_compat_l. apply bpow_ge_0. generalize He. apply round_abs_abs... clear rnd valid_rnd x Hx Hx' He. intros rnd valid_rnd x _ Hx. rewrite <- (round_generic beta fexp rnd (bpow (ex - 1))). now apply round_le. apply generic_format_bpow. ring_simplify (ex - 1 + 1)%Z. generalize (Hmin ex). lia. Qed.
imports: Coq(ZArith Reals Psatz) Core