proposition: Lemma round_round_eq_mid_beta_even : forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> Valid_exp fexp2 -> forall (choice1 choice2 : Z -> bool), (exists n, (beta = 2 * n :> Z)%Z) -> forall x, 0 < x -> (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z -> (fexp1 (mag x) <= mag x)%Z -> x = midp fexp1 x -> round_round_eq fexp1 fexp2 choice1 choice2 x.
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Ebeta x Px Hf2 Hf1. unfold round_round_eq. unfold midp. set (rd := round beta fexp1 Zfloor x). set (u := ulp beta fexp1 x). intro H; apply (Rplus_eq_compat_l (- rd)) in H. ring_simplify in H; revert H. rewrite Rplus_comm; fold (Rminus x rd). intro Xmid. destruct Ebeta as (n,Ebeta). assert (Hbeta : (2 <= beta)%Z). { destruct beta as (beta_val,beta_prop). now apply Zle_bool_imp_le. } apply (Rplus_eq_compat_l rd) in Xmid; ring_simplify in Xmid. rewrite (round_generic beta fexp2); [reflexivity|now apply valid_rnd_N|]. set (f := Float beta (Zfloor (scaled_mantissa beta fexp2 rd) + n * beta ^ (fexp1 (mag x) - 1 - fexp2 (mag x))) (cexp beta fexp2 x)). assert (Hf : F2R f = x). { unfold f, F2R; simpl. rewrite plus_IZR. rewrite Rmult_plus_distr_r. rewrite mult_IZR. rewrite IZR_Zpower by lia. unfold cexp at 2; bpow_simplify. unfold Zminus; rewrite bpow_plus. rewrite (Rmult_comm _ (bpow (- 1))). rewrite <- (Rmult_assoc (IZR n)). change (bpow (- 1)) with (/ IZR (beta * 1)). rewrite Zmult_1_r. rewrite Ebeta. rewrite (mult_IZR 2). rewrite Rinv_mult_distr; [|simpl; lra | apply IZR_neq; lia]. rewrite <- Rmult_assoc; rewrite (Rmult_comm (IZR n)); rewrite (Rmult_assoc _ (IZR n)). rewrite Rinv_r; [rewrite Rmult_1_r | apply IZR_neq; lia]. simpl; fold (cexp beta fexp1 x). rewrite <- 2!ulp_neq_0; try now apply Rgt_not_eq. fold u; rewrite Xmid at 2. apply f_equal2; [|reflexivity]. rewrite ulp_neq_0; try now apply Rgt_not_eq. destruct (Req_dec rd 0) as [Zrd|Nzrd]. - rewrite Zrd. rewrite scaled_mantissa_0. rewrite Zfloor_IZR. now rewrite Rmult_0_l. - assert (Nnrd : 0 <= rd). { apply round_DN_pt. - exact Vfexp1. - apply generic_format_0. - now apply Rlt_le. } assert (Prd : 0 < rd); [lra|]. assert (Lrd : (mag rd = mag x :> Z)). { apply Zle_antisym. - apply mag_le; [exact Prd|]. now apply round_DN_pt. - apply mag_round_ge. + exact Vfexp1. + now apply valid_rnd_DN. + exact Nzrd. } unfold scaled_mantissa. unfold rd at 1. unfold round, F2R, scaled_mantissa, cexp; simpl. bpow_simplify. rewrite Lrd. rewrite <- (IZR_Zpower _ (_ - _)) by lia. rewrite <- mult_IZR. rewrite (Zfloor_imp (Zfloor (x * bpow (- fexp1 (mag x))) * beta ^ (fexp1 (mag x) - fexp2 (mag x)))). + rewrite mult_IZR. rewrite IZR_Zpower by lia. bpow_simplify. now unfold rd. + split; [now apply Rle_refl|]. rewrite plus_IZR. simpl; lra. } apply (generic_format_F2R' _ _ x f Hf). intros _. apply Z.le_refl. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ