proposition: Theorem round_DN_plus_eps: forall x, F x -> forall eps, (0 <= eps < if (Rle_bool 0 x) then (ulp x) else (ulp (pred (-x))))%R -> round beta fexp Zfloor (x + eps) = x.
proof: Proof. intros x Fx eps Heps. case (Rle_or_lt 0 x); intros Zx. apply round_DN_plus_eps_pos; try assumption. split; try apply Heps. rewrite Rle_bool_true in Heps; trivial. now apply Heps. rewrite Rle_bool_false in Heps; trivial. rewrite <- (Ropp_involutive (x+eps)). pattern x at 2; rewrite <- (Ropp_involutive x). rewrite round_DN_opp. apply f_equal. replace (-(x+eps))%R with (pred (-x) + (ulp (pred (-x)) - eps))%R. rewrite round_UP_pred_plus_eps_pos; try reflexivity. now apply Ropp_0_gt_lt_contravar. now apply generic_format_opp. split. apply Rplus_lt_reg_l with eps; ring_simplify. apply Heps. apply Rplus_le_reg_l with (eps-ulp (pred (- x)))%R; ring_simplify. apply Heps. unfold pred. rewrite Ropp_involutive. unfold succ; rewrite Rle_bool_false; try assumption. rewrite Ropp_involutive; unfold Rminus. rewrite <- Rplus_assoc, pred_pos_plus_ulp. ring. now apply Ropp_0_gt_lt_contravar. now apply generic_format_opp. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop