proposition: Lemma round_round_plus_aux1_aux : forall k, (0 < k)%Z -> forall (fexp : Z -> Z), forall x y, 0 < x -> 0 < y -> (mag y <= fexp (mag x) - k)%Z -> (mag (x + y) = mag x :> Z) -> generic_format beta fexp x -> 0 < (x + y) - round beta fexp Zfloor (x + y) < bpow (fexp (mag x) - k).
proof: Proof. assert (Hbeta : (2 <= beta)%Z). { destruct beta as (beta_val,beta_prop). now apply Zle_bool_imp_le. } intros k Hk fexp x y Px Py Hln Hlxy Fx. revert Fx. unfold round, generic_format, F2R, scaled_mantissa, cexp; simpl. rewrite Hlxy. set (mx := Ztrunc (x * bpow (- fexp (mag x)))). intros Fx. assert (R : (x + y) * bpow (- fexp (mag x)) = IZR mx + y * bpow (- fexp (mag x))). { rewrite Fx at 1. rewrite Rmult_plus_distr_r. now bpow_simplify. } rewrite R. assert (LB : 0 < y * bpow (- fexp (mag x))). { rewrite <- (Rmult_0_r y). now apply Rmult_lt_compat_l; [|apply bpow_gt_0]. } assert (UB : y * bpow (- fexp (mag x)) < / IZR (beta ^ k)). { apply Rlt_le_trans with (bpow (mag y) * bpow (- fexp (mag x))). - apply Rmult_lt_compat_r; [now apply bpow_gt_0|]. rewrite <- (Rabs_right y) at 1; [|now apply Rle_ge; apply Rlt_le]. apply bpow_mag_gt. - apply Rle_trans with (bpow (fexp (mag x) - k) * bpow (- fexp (mag x)))%R. + apply Rmult_le_compat_r; [now apply bpow_ge_0|]. now apply bpow_le. + bpow_simplify. rewrite bpow_opp. destruct k. * lia. * simpl; unfold Raux.bpow, Z.pow_pos. now apply Rle_refl. * exfalso; apply (Z.lt_irrefl 0). apply (Z.lt_trans _ _ _ Hk). apply Zlt_neg_0. } rewrite (Zfloor_imp mx). { split; ring_simplify. - apply (Rmult_lt_reg_r (bpow (- fexp (mag x)))); [now apply bpow_gt_0|]. rewrite Rmult_minus_distr_r, Rmult_0_l. bpow_simplify. rewrite R; ring_simplify. now apply Rmult_lt_0_compat; [|apply bpow_gt_0]. - apply (Rmult_lt_reg_r (bpow (- fexp (mag x)))); [now apply bpow_gt_0|]. rewrite Rmult_minus_distr_r. bpow_simplify. rewrite R; ring_simplify. apply (Rlt_le_trans _ _ _ UB). rewrite bpow_opp. apply Rinv_le; [now apply bpow_gt_0|]. now rewrite IZR_Zpower; [right|lia]. } split. - rewrite <- Rplus_0_r at 1; apply Rplus_le_compat_l. now apply Rlt_le. - rewrite plus_IZR; apply Rplus_lt_compat_l. apply (Rmult_lt_reg_r (bpow (fexp (mag x)))); [now apply bpow_gt_0|]. rewrite Rmult_1_l. bpow_simplify. apply Rlt_trans with (bpow (mag y)). + rewrite <- Rabs_right at 1; [|now apply Rle_ge; apply Rlt_le]. apply bpow_mag_gt. + apply bpow_lt; lia. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ