proposition: Lemma round_round_minus_aux2_aux : forall (fexp : Z -> Z), Valid_exp fexp -> forall x y, 0 < y -> y < x -> (mag y <= fexp (mag x) - 1)%Z -> generic_format beta fexp x -> generic_format beta fexp y -> round beta fexp Zceil (x - y) - (x - y) <= y.
proof: Proof. intros fexp Vfexp x y Py Hxy Hly Fx Fy. assert (Px := Rlt_trans 0 y x Py Hxy). revert Fx. unfold generic_format, F2R, scaled_mantissa, cexp; simpl. set (mx := Ztrunc (x * bpow (- fexp (mag x)))). intro Fx. assert (Hfx : (fexp (mag x) < mag x)%Z); [now apply mag_generic_gt; [|apply Rgt_not_eq|]|]. assert (Hfy : (fexp (mag y) < mag y)%Z); [now apply mag_generic_gt; [|apply Rgt_not_eq|]|]. destruct (Rlt_or_le (bpow (mag x - 1)) x) as [Hx|Hx]. - assert (Lxy : mag (x - y) = mag x :> Z); [now apply (mag_minus_separated fexp); [| | | | | |lia]|]. assert (Rxy : round beta fexp Zceil (x - y) = x). { unfold round, F2R, scaled_mantissa, cexp; simpl. rewrite Lxy. apply eq_sym; rewrite Fx at 1; apply eq_sym. apply Rmult_eq_compat_r. apply f_equal. rewrite Fx at 1. rewrite Rmult_minus_distr_r. bpow_simplify. apply Zceil_imp. split. - unfold Zminus; rewrite plus_IZR. apply Rplus_lt_compat_l. apply Ropp_lt_contravar; simpl. apply (Rmult_lt_reg_r (bpow (fexp (mag x)))); [now apply bpow_gt_0|]. rewrite Rmult_1_l; bpow_simplify. apply Rlt_le_trans with (bpow (mag y)). + rewrite <- Rabs_right at 1; [|now apply Rle_ge; apply Rlt_le]. apply bpow_mag_gt. + apply bpow_le. lia. - rewrite <- (Rplus_0_r (IZR _)) at 2. apply Rplus_le_compat_l. rewrite <- Ropp_0; apply Ropp_le_contravar. rewrite <- (Rmult_0_r y). apply Rmult_le_compat_l; [now apply Rlt_le|]. now apply bpow_ge_0. } rewrite Rxy; ring_simplify. apply Rle_refl. - assert (Xpow : x = bpow (mag x - 1)). { apply Rle_antisym; [exact Hx|]. destruct (mag x) as (ex, Hex); simpl. rewrite <- (Rabs_right x); [|now apply Rle_ge; apply Rlt_le]. apply Hex. now apply Rgt_not_eq. } assert (Lxy : (mag (x - y) = mag x - 1 :> Z)%Z). { apply Zle_antisym. - apply mag_le_bpow. + apply Rminus_eq_contra. now intro Hx'; rewrite Hx' in Hxy; apply (Rlt_irrefl y). + rewrite Rabs_right; lra. - apply (mag_minus_lb beta x y Px Py). lia. } assert (Hfx1 : (fexp (mag x - 1) < mag x - 1)%Z); [now apply (valid_exp_large fexp (mag y)); [|lia]|]. assert (Rxy : round beta fexp Zceil (x - y) <= x). { rewrite Xpow at 2. unfold round, F2R, scaled_mantissa, cexp; simpl. rewrite Lxy. apply (Rmult_le_reg_r (bpow (- fexp (mag x - 1)%Z))); [now apply bpow_gt_0|]. bpow_simplify. rewrite <- (IZR_Zpower beta (_ - _ - _)) by lia. apply IZR_le. apply Zceil_glb. rewrite IZR_Zpower by lia. rewrite Xpow at 1. rewrite Rmult_minus_distr_r. bpow_simplify. rewrite <- (Rplus_0_r (bpow _)) at 2. apply Rplus_le_compat_l. rewrite <- Ropp_0; apply Ropp_le_contravar. rewrite <- (Rmult_0_r y). apply Rmult_le_compat_l; [now apply Rlt_le|]. now apply bpow_ge_0. } lra. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ