proposition: Theorem round_N_pt : forall x, Rnd_N_pt generic_format x (round Znearest x).
proof: Proof. intros x. set (d := round Zfloor x). set (u := round Zceil x). set (mx := scaled_mantissa x). set (bx := bpow (cexp x)). assert (H: (Rabs (round Znearest x - x) <= Rmin (x - d) (u - x))%R). pattern x at -1 ; rewrite <- scaled_mantissa_mult_bpow. unfold d, u, round, F2R. simpl. fold mx bx. rewrite <- 3!Rmult_minus_distr_r. rewrite Rabs_mult, (Rabs_pos_eq bx). 2: apply bpow_ge_0. rewrite <- Rmult_min_distr_r. 2: apply bpow_ge_0. apply Rmult_le_compat_r. apply bpow_ge_0. unfold Znearest. destruct (Req_dec (IZR (Zfloor mx)) mx) as [Hm|Hm]. rewrite Hm. unfold Rminus at 2. rewrite Rplus_opp_r. rewrite Rcompare_Lt. rewrite Hm. unfold Rminus at -3. rewrite Rplus_opp_r. rewrite Rabs_R0. unfold Rmin. destruct (Rle_dec 0 (IZR (Zceil mx) - mx)) as [H|H]. apply Rle_refl. apply Rle_0_minus. apply Zceil_ub. apply Rinv_0_lt_compat. now apply IZR_lt. rewrite Rcompare_floor_ceil_middle with (1 := Hm). rewrite Rmin_compare. assert (H: (Rabs (mx - IZR (Zfloor mx)) <= mx - IZR (Zfloor mx))%R). rewrite Rabs_pos_eq. apply Rle_refl. apply Rle_0_minus. apply Zfloor_lb. case Rcompare_spec ; intros Hm'. now rewrite Rabs_minus_sym. case choice. rewrite <- Hm'. exact H. now rewrite Rabs_minus_sym. rewrite Rabs_pos_eq. apply Rle_refl. apply Rle_0_minus. apply Zceil_ub. apply Rnd_N_pt_DN_UP with d u. apply generic_format_round. auto with typeclass_instances. now apply round_DN_pt. now apply round_UP_pt. apply Rle_trans with (1 := H). apply Rmin_l. apply Rle_trans with (1 := H). apply Rmin_r. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop