proposition: Lemma round_round_mid_cases : 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 -> (Rabs (x - midp fexp1 x) <= / 2 * (ulp beta fexp2 x) -> round_round_eq fexp1 fexp2 choice1 choice2 x) -> round_round_eq fexp1 fexp2 choice1 choice2 x.
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1. unfold round_round_eq, midp. set (rd := round beta fexp1 Zfloor x). set (u1 := ulp beta fexp1 x). set (u2 := ulp beta fexp2 x). intros Cmid. destruct (generic_format_EM beta fexp1 x) as [Fx|Nfx]. - rewrite (round_generic beta fexp2); [reflexivity|now apply valid_rnd_N|]. now apply (generic_inclusion_mag beta fexp1); [lia|]. - assert (Hceil : round beta fexp1 Zceil x = rd + u1); [now apply round_UP_DN_ulp|]. assert (Hf2' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z) by lia. destruct (Rlt_or_le (x - rd) (/ 2 * (u1 - u2))). + apply round_round_lt_mid_further_place; try assumption. unfold midp. fold rd; fold u1; fold u2. apply (Rplus_lt_reg_r (- rd)); ring_simplify. now rewrite <- Rmult_minus_distr_l. + { destruct (Rlt_or_le (/ 2 * (u1 + u2)) (x - rd)). - assert (round beta fexp1 Zceil x - x < / 2 * (ulp beta fexp1 x - ulp beta fexp2 x)). { rewrite Hceil; fold u1; fold u2. lra. } apply round_round_gt_mid_further_place; try assumption. unfold midp'; lra. - apply Cmid, Rabs_le; split; lra. } Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ