proposition: Theorem relative_error_N_FLX' : forall x, (Rabs (round beta (FLX_exp prec) (Znearest choice) x - x) <= u_ro / (1 + u_ro) * Rabs x)%R.
proof: Proof. Proof with auto with typeclass_instances. intro x. assert (Pu_ro : (0 <= u_ro)%R). { apply Rmult_le_pos; [lra|apply bpow_ge_0]. } destruct (Req_dec x 0) as [Zx|Nzx]. { rewrite Zx, Rabs_R0, Rmult_0_r, round_0... now unfold Rminus; rewrite Rplus_0_l, Rabs_Ropp, Rabs_R0; right. } set (ufpx := bpow (mag beta x - 1)%Z). set (rx := round _ _ _ _). assert (Pufpx : (0 <= ufpx)%R); [now apply bpow_ge_0|]. assert (H_2_1 : (Rabs (rx - x) <= u_ro * ufpx)%R). { refine (Rle_trans _ _ _ (error_le_half_ulp _ _ _ _) _); [now apply FLX_exp_valid|right]. unfold ulp, cexp, FLX_exp, u_ro, ufpx; rewrite (Req_bool_false _ _ Nzx). rewrite Rmult_assoc, <-bpow_plus; do 2 f_equal; ring. } assert (H_2_3 : (ufpx + Rabs (rx - x) <= Rabs x)%R). { apply (Rplus_le_reg_r (- ufpx)); ring_simplify. destruct (Rle_or_lt 0 x) as [Sx|Sx]. { apply (Rle_trans _ (Rabs (ufpx - x))). { apply round_N_pt; [now apply FLX_exp_valid|]. apply generic_format_bpow; unfold FLX_exp; lia. } rewrite Rabs_minus_sym, Rabs_pos_eq. { now rewrite Rabs_pos_eq; [right; ring|]. } apply (Rplus_le_reg_r ufpx); ring_simplify. now rewrite <-(Rabs_pos_eq _ Sx); apply bpow_mag_le. } apply (Rle_trans _ (Rabs (- ufpx - x))). { apply round_N_pt; [now apply FLX_exp_valid|]. apply generic_format_opp, generic_format_bpow; unfold FLX_exp; lia. } rewrite Rabs_pos_eq; [now rewrite Rabs_left; [right|]|]. apply (Rplus_le_reg_r x); ring_simplify. rewrite <-(Ropp_involutive x); apply Ropp_le_contravar; unfold ufpx. rewrite <-mag_opp, <-Rabs_pos_eq; [apply bpow_mag_le|]; lra. } assert (H : (Rabs ((rx - x) / x) <= u_ro / (1 + u_ro))%R). { assert (H : (0 < ufpx + Rabs (rx - x))%R). { apply Rplus_lt_le_0_compat; [apply bpow_gt_0|apply Rabs_pos]. } apply (Rle_trans _ (Rabs (rx - x) / (ufpx + Rabs (rx - x)))). { unfold Rdiv; rewrite Rabs_mult; apply Rmult_le_compat_l; [apply Rabs_pos|]. now rewrite (Rabs_Rinv _ Nzx); apply Rinv_le. } apply (Rmult_le_reg_r ((ufpx + Rabs (rx - x)) * (1 + u_ro))). { apply Rmult_lt_0_compat; lra. } field_simplify; [try unfold Rdiv; rewrite ?Rinv_1, ?Rmult_1_r| |]; lra. } revert H; unfold Rdiv; rewrite Rabs_mult, (Rabs_Rinv _ Nzx); intro H. apply (Rmult_le_reg_r (/ Rabs x)); [now apply Rinv_0_lt_compat, Rabs_pos_lt|]. now apply (Rle_trans _ _ _ H); right; field; split; [apply Rabs_no_R0|lra]. Qed.
imports: Coq(ZArith Reals Psatz) Core