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 -> round beta fexp2 (Znearest choice2) x < bpow (mag x) -> 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. intros Hx1 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 Hx1 Hx2. unfold round_round_eq. set (x' := round beta fexp1 Zceil x). set (x'' := round beta fexp2 (Znearest choice2) x). intros Hx1 Hx2. assert (Hr1 : Rabs (x'' - x) <= / 2 * bpow (fexp2 (mag x))). apply Rle_trans with (/2* ulp beta fexp2 x). now unfold x''; apply error_le_half_ulp... rewrite ulp_neq_0;[now right|now apply Rgt_not_eq]. assert (Px'x : 0 <= x' - x). { apply Rle_0_minus. apply round_UP_pt. exact Vfexp1. } assert (Hr2 : Rabs (x'' - x') < / 2 * bpow (fexp1 (mag x))). { replace (x'' - x') with (x'' - x + (x - x')) by ring. apply (Rle_lt_trans _ _ _ (Rabs_triang _ _)). replace (/ 2 * _) with (/ 2 * bpow (fexp2 (mag x)) + (/ 2 * (bpow (fexp1 (mag x)) - bpow (fexp2 (mag x))))) by ring. apply Rplus_le_lt_compat. - exact Hr1. - rewrite Rabs_minus_sym. rewrite 2!ulp_neq_0 in Hx2; try (apply Rgt_not_eq; assumption). now rewrite Rabs_right; [|now apply Rle_ge]; apply Hx2. } destruct (Req_dec x'' 0) as [Zx''|Nzx'']. - rewrite Zx'' in Hr1 |- *. rewrite round_0; [|now apply valid_rnd_N]. unfold round, F2R, scaled_mantissa, cexp; simpl. rewrite (Znearest_imp _ _ 0); [now simpl; rewrite Rmult_0_l|]. 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. rewrite Rmult_0_l. bpow_simplify. rewrite Rabs_minus_sym. apply (Rle_lt_trans _ _ _ Hr1). apply Rmult_lt_compat_l; [lra|]. apply bpow_lt. lia. - assert (Lx'' : mag x'' = mag x :> Z). { apply Zle_antisym. - apply mag_le_bpow; [exact Nzx''|]. rewrite Rabs_right; [exact Hx1|apply Rle_ge]. apply round_ge_generic. + exact Vfexp2. + now apply valid_rnd_N. + apply generic_format_0. + now apply Rlt_le. - unfold x'' in Nzx'' |- *. now apply mag_round_ge; [|apply valid_rnd_N|]. } unfold round, F2R, scaled_mantissa, cexp; simpl. rewrite Lx''. rewrite (Znearest_imp _ _ (Zceil (scaled_mantissa beta fexp1 x))). + rewrite (Znearest_imp _ _ (Zceil (scaled_mantissa beta fexp1 x))); [reflexivity|]. 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. fold x'. bpow_simplify. rewrite Rabs_minus_sym. rewrite Rabs_right; [|now apply Rle_ge]. apply (Rlt_le_trans _ _ _ Hx2). apply Rmult_le_compat_l; [lra|]. generalize (bpow_ge_0 beta (fexp2 (mag x))). rewrite 2!ulp_neq_0; try (apply Rgt_not_eq; assumption). unfold cexp; lra. + 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. fold x'. now bpow_simplify. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ