proposition: Theorem round_DN_plus_eps_pos : forall x, (0 <= x)%R -> F x -> forall eps, (0 <= eps < ulp x)%R -> round beta fexp Zfloor (x + eps) = x.
proof: Proof. intros x Zx Fx eps Heps. destruct Zx as [Zx|Zx]. pattern x at 2 ; rewrite Fx. unfold round. unfold scaled_mantissa. simpl. unfold cexp at 1 2. rewrite mag_plus_eps ; trivial. apply (f_equal (fun m => F2R (Float beta m _))). rewrite Ztrunc_floor. apply Zfloor_imp. split. apply (Rle_trans _ _ _ (Zfloor_lb _)). apply Rmult_le_compat_r. apply bpow_ge_0. pattern x at 1 ; rewrite <- Rplus_0_r. now apply Rplus_le_compat_l. apply Rlt_le_trans with ((x + ulp x) * bpow (- cexp beta fexp x))%R. apply Rmult_lt_compat_r. apply bpow_gt_0. now apply Rplus_lt_compat_l. rewrite Rmult_plus_distr_r. rewrite plus_IZR. apply Rplus_le_compat. pattern x at 1 3 ; rewrite Fx. unfold F2R. simpl. rewrite Rmult_assoc. rewrite <- bpow_plus. rewrite Zplus_opp_r. rewrite Rmult_1_r. rewrite Zfloor_IZR. apply Rle_refl. rewrite ulp_neq_0. 2: now apply Rgt_not_eq. rewrite <- bpow_plus. rewrite Zplus_opp_r. apply Rle_refl. apply Rmult_le_pos. now apply Rlt_le. apply bpow_ge_0. rewrite <- Zx, Rplus_0_l; rewrite <- Zx in Heps. case (proj1 Heps); intros P. unfold round, scaled_mantissa, cexp. revert Heps; unfold ulp. rewrite Req_bool_true; trivial. case negligible_exp_spec. intros _ (H1,H2). exfalso ; lra. intros n Hn H. assert (fexp (mag beta eps) = fexp n). apply valid_exp; try assumption. cut (mag beta eps-1 < fexp n)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (2:=proj2 H). destruct (mag beta eps) as (e,He). simpl; rewrite Rabs_pos_eq in He. now apply He, Rgt_not_eq. now left. replace (Zfloor (eps * bpow (- fexp (mag beta eps)))) with 0%Z. unfold F2R; simpl; ring. apply sym_eq, Zfloor_imp. split. apply Rmult_le_pos. now left. apply bpow_ge_0. apply Rmult_lt_reg_r with (bpow (fexp n)). apply bpow_gt_0. rewrite Rmult_assoc, <- bpow_plus. rewrite H0; ring_simplify (-fexp n + fexp n)%Z. simpl; rewrite Rmult_1_l, Rmult_1_r. apply H. rewrite <- P, round_0; trivial. apply valid_rnd_DN. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop