proposition: Lemma round_NE_pt_pos : forall x, (0 < x)%R -> Rnd_NE_pt x (round beta fexp ZnearestE x).
proof: Proof. Proof with auto with typeclass_instances. intros x Hx. split. now apply round_N_pt. unfold NE_prop. set (mx := scaled_mantissa beta fexp x). set (xr := round beta fexp ZnearestE x). destruct (Req_dec (mx - IZR (Zfloor mx)) (/2)) as [Hm|Hm]. left. exists (Float beta (Ztrunc (scaled_mantissa beta fexp xr)) (cexp beta fexp xr)). split. apply round_N_pt... split. unfold Generic_fmt.canonical. simpl. apply f_equal. apply round_N_pt... simpl. unfold xr, round, Znearest. fold mx. rewrite Hm. rewrite Rcompare_Eq. 2: apply refl_equal. case_eq (Z.even (Zfloor mx)) ; intros Hmx. change (Z.even (Ztrunc (scaled_mantissa beta fexp (round beta fexp Zfloor x))) = true). destruct (Rle_or_lt (round beta fexp Zfloor x) 0) as [Hr|Hr]. rewrite (Rle_antisym _ _ Hr). unfold scaled_mantissa. rewrite Rmult_0_l. now rewrite Ztrunc_IZR. rewrite <- (round_0 beta fexp Zfloor). apply round_le... now apply Rlt_le. rewrite scaled_mantissa_DN... now rewrite Ztrunc_IZR. change (Z.even (Ztrunc (scaled_mantissa beta fexp (round beta fexp Zceil x))) = true). destruct (mag beta x) as (ex, Hex). specialize (Hex (Rgt_not_eq _ _ Hx)). rewrite (Rabs_pos_eq _ (Rlt_le _ _ Hx)) in Hex. destruct (Z_lt_le_dec (fexp ex) ex) as [He|He]. assert (Hu := round_bounded_large_pos _ _ Zceil _ _ He Hex). assert (Hfc: Zceil mx = (Zfloor mx + 1)%Z). apply Zceil_floor_neq. intros H. rewrite H in Hm. unfold Rminus in Hm. rewrite Rplus_opp_r in Hm. elim (Rlt_irrefl 0). rewrite Hm at 2. apply Rinv_0_lt_compat. now apply IZR_lt. destruct (proj2 Hu) as [Hu'|Hu']. unfold scaled_mantissa. rewrite cexp_fexp_pos with (1 := conj (proj1 Hu) Hu'). unfold round, F2R. simpl. rewrite cexp_fexp_pos with (1 := Hex). rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r. rewrite Ztrunc_IZR. fold mx. rewrite Hfc. now rewrite Z.even_add, Hmx. rewrite Hu'. unfold scaled_mantissa, cexp. rewrite mag_bpow. rewrite <- bpow_plus, <- IZR_Zpower. rewrite Ztrunc_IZR. case_eq (Z.even beta) ; intros Hr. destruct exists_NE_ as [Hs|Hs]. now rewrite Hs in Hr. destruct (Hs ex) as (H,_). rewrite Z.even_pow. exact Hr. lia. assert (Z.even (Zfloor mx) = true). 2: now rewrite H in Hmx. replace (Zfloor mx) with (Zceil mx + -1)%Z by lia. rewrite Z.even_add. apply eqb_true. unfold mx. replace (Zceil (scaled_mantissa beta fexp x)) with (Zpower beta (ex - fexp ex)). rewrite Zeven_Zpower_odd with (2 := Hr). easy. lia. apply eq_IZR. rewrite IZR_Zpower by lia. apply Rmult_eq_reg_r with (bpow (fexp ex)). unfold Zminus. rewrite bpow_plus. rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_l, Rmult_1_r. pattern (fexp ex) ; rewrite <- cexp_fexp_pos with (1 := Hex). now apply sym_eq. apply Rgt_not_eq. apply bpow_gt_0. generalize (proj1 (valid_exp ex) He). lia. assert (Z.even (Zfloor mx) = true). 2: now rewrite H in Hmx. unfold mx, scaled_mantissa. rewrite cexp_fexp_pos with (1 := Hex). now rewrite mantissa_DN_small_pos. right. intros g Hg. destruct (Req_dec x g) as [Hxg|Hxg]. rewrite <- Hxg. apply sym_eq. apply round_generic... rewrite Hxg. apply Hg. set (d := round beta fexp Zfloor x). set (u := round beta fexp Zceil x). apply Rnd_N_pt_unique with (d := d) (u := u) (4 := Hg). now apply round_DN_pt. now apply round_UP_pt. 2: now apply round_N_pt. rewrite <- (scaled_mantissa_mult_bpow beta fexp x). unfold d, u, round, F2R. simpl. fold mx. rewrite <- 2!Rmult_minus_distr_r. intros H. apply Rmult_eq_reg_r in H. apply Hm. apply Rcompare_Eq_inv. rewrite Rcompare_floor_ceil_middle. now apply Rcompare_Eq. contradict Hxg. apply sym_eq. apply Rnd_N_pt_idempotent with (1 := Hg). rewrite <- (scaled_mantissa_mult_bpow beta fexp x). fold mx. rewrite <- Hxg. change (IZR (Zfloor mx) * bpow (cexp beta fexp x))%R with d. now eapply round_DN_pt. apply Rgt_not_eq. apply bpow_gt_0. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp