proposition: Lemma round_round_gt_mid_further_place : forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> Valid_exp fexp2 -> forall (choice1 choice2 : Z -> bool), forall x, 0 < x -> (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z -> (fexp1 (mag x) <= mag x)%Z -> midp' fexp1 x + / 2 * ulp beta fexp2 x < x -> round_round_eq fexp1 fexp2 choice1 choice2 x.
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1 Hx2'. assert (Hx2 : round beta fexp1 Zceil x - x < / 2 * (ulp beta fexp1 x - ulp beta fexp2 x)). { apply (Rplus_lt_reg_r (- / 2 * ulp beta fexp1 x + x + / 2 * ulp beta fexp2 x)); ring_simplify. now unfold midp' in Hx2'. } revert Hx2. unfold round_round_eq. set (x' := round beta fexp1 Zfloor x). intro Hx2. set (x'' := round beta fexp2 (Znearest choice2) x). destruct (Rlt_or_le x'' (bpow (mag x))) as [Hx''|Hx'']; [now apply round_round_gt_mid_further_place'|]. assert (Hx''pow : x'' = bpow (mag x)). { assert (H'x'' : x'' < bpow (mag x) + / 2 * ulp beta fexp2 x). { apply Rle_lt_trans with (x + / 2 * ulp beta fexp2 x). - apply (Rplus_le_reg_r (- x)); ring_simplify. apply Rabs_le_inv. apply error_le_half_ulp. exact Vfexp2. - apply Rplus_lt_compat_r. rewrite <- Rabs_right at 1; [|now apply Rle_ge; apply Rlt_le]. apply bpow_mag_gt. } apply Rle_antisym; [|exact Hx'']. unfold x'', round, F2R, scaled_mantissa, cexp; simpl. apply (Rmult_le_reg_r (bpow (- fexp2 (mag x)))); [now apply bpow_gt_0|]. bpow_simplify. rewrite <- (IZR_Zpower _ (_ - _)) by lia. apply IZR_le. apply Zlt_succ_le; unfold Z.succ. apply lt_IZR. rewrite plus_IZR; rewrite IZR_Zpower by lia. apply (Rmult_lt_reg_r (bpow (fexp2 (mag x)))); [now apply bpow_gt_0|]. rewrite Rmult_plus_distr_r; rewrite Rmult_1_l. bpow_simplify. apply (Rlt_le_trans _ _ _ H'x''). apply Rplus_le_compat_l. rewrite <- (Rmult_1_l (Raux.bpow _ _)). rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. apply Rmult_le_compat_r; [now apply bpow_ge_0|]. lra. } assert (Hr : Rabs (x - x'') < / 2 * ulp beta fexp1 x). { apply Rle_lt_trans with (/ 2 * ulp beta fexp2 x). - rewrite Rabs_minus_sym. apply error_le_half_ulp. exact Vfexp2. - apply Rmult_lt_compat_l; [lra|]. rewrite 2!ulp_neq_0; try now apply Rgt_not_eq. unfold cexp; apply bpow_lt. lia. } unfold round, F2R, scaled_mantissa, cexp; simpl. assert (Hf : (0 <= mag x - fexp1 (mag x''))%Z). { rewrite Hx''pow. rewrite mag_bpow. cut (fexp1 (mag x + 1) <= mag x)%Z. lia. destruct (Zle_or_lt (mag x) (fexp1 (mag x))) as [Hle|Hlt]; [|now apply Vfexp1]. assert (H : (mag x = fexp1 (mag x) :> Z)%Z); [now apply Zle_antisym|]. rewrite H. now apply Vfexp1. } rewrite (Znearest_imp _ _ (beta ^ (mag x - fexp1 (mag x'')))%Z). - rewrite (Znearest_imp _ _ (beta ^ (mag x - fexp1 (mag x)))%Z). + rewrite IZR_Zpower by exact Hf. rewrite IZR_Zpower by lia. now bpow_simplify. + rewrite IZR_Zpower by lia. apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|]. rewrite <- (Rabs_right (bpow (fexp1 _))) at 1; [|now apply Rle_ge; apply bpow_ge_0]. rewrite <- Rabs_mult. rewrite Rmult_minus_distr_r. bpow_simplify. rewrite ulp_neq_0 in Hr;[idtac|now apply Rgt_not_eq]. rewrite <- Hx''pow; exact Hr. - rewrite IZR_Zpower; [|exact Hf]. apply (Rmult_lt_reg_r (bpow (fexp1 (mag x'')))); [now apply bpow_gt_0|]. rewrite <- (Rabs_right (bpow (fexp1 _))) at 1; [|now apply Rle_ge; apply bpow_ge_0]. rewrite <- Rabs_mult. rewrite Rmult_minus_distr_r. bpow_simplify. rewrite Rminus_diag_eq; [|exact Hx''pow]. rewrite Rabs_R0. rewrite <- (Rmult_0_r (/ 2)). apply Rmult_lt_compat_l; [lra|apply bpow_gt_0]. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ