proposition: Lemma generic_format_pred_aux1: forall x, (0 < x)%R -> F x -> x <> bpow (mag beta x - 1) -> F (x - ulp x).
proof: Proof. intros x Zx Fx Hx. destruct (mag beta x) as (ex, Ex). simpl in Hx. specialize (Ex (Rgt_not_eq _ _ Zx)). assert (Ex' : (bpow (ex - 1) < x < bpow ex)%R). rewrite Rabs_pos_eq in Ex. destruct Ex as (H,H'); destruct H; split; trivial. contradict Hx; easy. now apply Rlt_le. unfold generic_format, scaled_mantissa, cexp. rewrite mag_unique with beta (x - ulp x)%R ex. pattern x at 1 3 ; rewrite Fx. rewrite ulp_neq_0. unfold scaled_mantissa. rewrite cexp_fexp with (1 := Ex). unfold F2R. simpl. rewrite Rmult_minus_distr_r. rewrite Rmult_assoc. rewrite <- bpow_plus, Zplus_opp_r, Rmult_1_r. change (bpow 0) with 1%R. rewrite <- minus_IZR. rewrite Ztrunc_IZR. rewrite minus_IZR. rewrite Rmult_minus_distr_r. now rewrite Rmult_1_l. now apply Rgt_not_eq. rewrite Rabs_pos_eq. split. apply id_m_ulp_ge_bpow; trivial. rewrite ulp_neq_0. intro H. assert (ex-1 < cexp beta fexp x < ex)%Z. split ; apply (lt_bpow beta) ; rewrite <- H ; easy. clear -H0. lia. now apply Rgt_not_eq. apply Ex'. apply Rle_lt_trans with (2 := proj2 Ex'). pattern x at 3 ; rewrite <- Rplus_0_r. apply Rplus_le_compat_l. rewrite <-Ropp_0. apply Ropp_le_contravar. apply ulp_ge_0. apply Rle_0_minus. pattern x at 2; rewrite Fx. rewrite ulp_neq_0. unfold F2R; simpl. pattern (bpow (cexp beta fexp x)) at 1; rewrite <- Rmult_1_l. apply Rmult_le_compat_r. apply bpow_ge_0. apply IZR_le. assert (0 < Ztrunc (scaled_mantissa beta fexp x))%Z. apply gt_0_F2R with beta (cexp beta fexp x). rewrite <- Fx. apply Rle_lt_trans with (2:=proj1 Ex'). apply bpow_ge_0. lia. now apply Rgt_not_eq. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop