proposition: Lemma ulp_round_pos : forall { Not_FTZ_ : Exp_not_FTZ fexp}, forall rnd { Zrnd : Valid_rnd rnd } x, (0 < x)%R -> ulp (round beta fexp rnd x) = ulp x \/ round beta fexp rnd x = bpow (mag beta x).
proof: Proof. Proof with auto with typeclass_instances. intros Not_FTZ_ rnd Zrnd x Hx. case (generic_format_EM beta fexp x); intros Fx. rewrite round_generic... case (round_DN_or_UP beta fexp rnd x); intros Hr; rewrite Hr. left. apply ulp_DN; now left... assert (M:(0 <= round beta fexp Zfloor x)%R). apply round_ge_generic... apply generic_format_0... apply Rlt_le... destruct M as [M|M]. rewrite <- (succ_DN_eq_UP x)... case (ulp_succ_pos (round beta fexp Zfloor x)); try intros Y. apply generic_format_round... assumption. rewrite ulp_DN in Y... now apply Rlt_le. right; rewrite Y. apply f_equal, mag_DN... left; rewrite <- (succ_DN_eq_UP x)... rewrite <- M, succ_0. rewrite ulp_ulp_0... case (negligible_exp_spec'). intros (K1,K2). absurd (x = 0)%R. now apply Rgt_not_eq. apply eq_0_round_0_negligible_exp with Zfloor... intros (n,(Hn1,Hn2)). replace (ulp 0) with (bpow (fexp n)). 2: unfold ulp; rewrite Req_bool_true; try easy. 2: now rewrite Hn1. rewrite ulp_neq_0. 2: apply Rgt_not_eq... unfold cexp; f_equal. destruct (mag beta x) as (e,He); simpl. apply sym_eq, valid_exp... assert (e <= fexp e)%Z. apply exp_small_round_0_pos with beta Zfloor x... rewrite <- (Rabs_pos_eq x). apply He, Rgt_not_eq... apply Rlt_le... replace (fexp n) with (fexp e); try assumption. now apply fexp_negligible_exp_eq. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop