proposition: Lemma round_round_all_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 + 1 :> Z)%Z -> bpow (mag x) - / 2 * ulp beta fexp2 x <= x -> round_round_eq fexp1 fexp2 choice1 choice2 x) -> ((fexp1 (mag x) <= mag x)%Z -> midp fexp1 x - / 2 * ulp beta fexp2 x <= x < midp fexp1 x -> round_round_eq fexp1 fexp2 choice1 choice2 x) -> ((fexp1 (mag x) <= mag x)%Z -> x = midp fexp1 x -> round_round_eq fexp1 fexp2 choice1 choice2 x) -> ((fexp1 (mag x) <= mag x)%Z -> midp fexp1 x < 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 Hf2. set (x' := round beta fexp1 Zfloor x). set (u1 := ulp beta fexp1 x). set (u2 := ulp beta fexp2 x). intros Cz Clt Ceq Cgt. destruct (Ztrichotomy (mag x) (fexp1 (mag x) - 1)) as [Hlt|[Heq|Hgt]]. - assert (H : (mag x <= fexp1 (mag x) - 2)%Z) by lia. now apply round_round_really_zero. - assert (H : (fexp1 (mag x) = (mag x + 1))%Z) by lia. destruct (Rlt_or_le x (bpow (mag x) - / 2 * u2)) as [Hlt'|Hge']. + now apply round_round_zero. + now apply Cz. - assert (H : (fexp1 (mag x) <= mag x)%Z) by lia. destruct (Rtotal_order x (midp fexp1 x)) as [Hlt'|[Heq'|Hgt']]. + destruct (Rlt_or_le x (midp fexp1 x - / 2 * u2)) as [Hlt''|Hle'']. * now apply round_round_lt_mid_further_place; [| | |lia| |]. * now apply Clt; [|split]. + now apply Ceq. + destruct (Rle_or_lt x (midp fexp1 x + / 2 * u2)) as [Hlt''|Hle'']. * now apply Cgt; [|split]. * { destruct (generic_format_EM beta fexp1 x) as [Fx|Nfx]. - unfold round_round_eq; 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 = x' + u1); [now apply round_UP_DN_ulp|]. assert (Hf2' : (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z) by lia. assert (midp' fexp1 x + / 2 * ulp beta fexp2 x < x); [|now apply round_round_gt_mid_further_place]. revert Hle''; unfold midp, midp'; fold x'. rewrite Hceil; fold u1; fold u2. lra. } Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ