proposition: Lemma round_round_gt_mid_same_place : forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> forall (choice1 choice2 : Z -> bool), forall x, 0 < x -> (fexp2 (mag x) = fexp1 (mag x))%Z -> midp' fexp1 x < x -> round_round_eq fexp1 fexp2 choice1 choice2 x.
proof: Proof. intros fexp1 fexp2 Vfexp1 choice1 choice2 x Px Hf2f1 Hx'. assert (Hx : round beta fexp1 Zceil x - x < / 2 * ulp beta fexp1 x). { apply (Rplus_lt_reg_r (- / 2 * ulp beta fexp1 x + x)); ring_simplify. now unfold midp' in Hx'. } assert (H : Rabs (IZR (Zceil (x * bpow (- fexp1 (mag x)))) - x * bpow (- fexp1 (mag x))) < / 2). { apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|]. unfold scaled_mantissa, cexp in Hx. 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. apply Rabs_lt. split. - apply Rlt_le_trans with 0. + rewrite <- Ropp_0; apply Ropp_lt_contravar. rewrite <- (Rmult_0_r (/ 2)). apply Rmult_lt_compat_l; [lra|]. apply bpow_gt_0. + apply Rle_0_minus. apply round_UP_pt. exact Vfexp1. - rewrite ulp_neq_0 in Hx;[exact Hx|now apply Rgt_not_eq]. } unfold round_round_eq, round at 2. unfold F2R, scaled_mantissa, cexp; simpl. rewrite Hf2f1. rewrite (Znearest_imp _ _ (Zceil (scaled_mantissa beta fexp1 x))). - rewrite round_generic. + unfold round, F2R, scaled_mantissa, cexp; simpl. now rewrite (Znearest_imp _ _ (Zceil (x * bpow (- fexp1 (mag x))))); [|rewrite Rabs_minus_sym]. + now apply valid_rnd_N. + fold (cexp beta fexp1 x). change (IZR _ * bpow _) with (round beta fexp1 Zceil x). apply generic_format_round. exact Vfexp1. now apply valid_rnd_UP. - now rewrite Rabs_minus_sym. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ