proposition: Lemma round_round_zero : forall fexp1 fexp2 : Z -> Z, Valid_exp fexp1 -> Valid_exp fexp2 -> forall (choice1 choice2 : Z -> bool), forall x, 0 < x -> (fexp1 (mag x) = mag x + 1 :> Z)%Z -> x < bpow (mag x) - / 2 * ulp beta fexp2 x -> round_round_eq fexp1 fexp2 choice1 choice2 x.
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf1. unfold round_round_eq. set (x'' := round beta fexp2 (Znearest choice2) x). set (u1 := ulp beta fexp1 x). set (u2 := ulp beta fexp2 x). intro Hx. assert (Hlx : bpow (mag x - 1) <= x < bpow (mag x)). { destruct (mag x) as (ex,Hex); simpl. rewrite <- (Rabs_right x); [|now apply Rle_ge; apply Rlt_le]. apply Hex. now apply Rgt_not_eq. } rewrite (round_N_small_pos beta fexp1 choice1 x (mag x)); [|exact Hlx|lia]. destruct (Req_dec x'' 0) as [Zx''|Nzx'']; [now rewrite Zx''; rewrite round_0; [reflexivity|apply valid_rnd_N]|]. rewrite (round_N_small_pos beta _ _ x'' (mag x)); [reflexivity| |lia]. split. - apply round_large_pos_ge_bpow. + now apply valid_rnd_N. + assert (0 <= x''); [|now fold x''; lra]. rewrite <- (round_0 beta fexp2 (Znearest choice2)). now apply round_le; [|apply valid_rnd_N|apply Rlt_le]. + apply Rle_trans with (Rabs x); [|now rewrite Rabs_right; [apply Rle_refl|apply Rle_ge; apply Rlt_le]]. destruct (mag x) as (ex,Hex); simpl; apply Hex. now apply Rgt_not_eq. - replace x'' with (x + (x'' - x)) by ring. replace (bpow _) with (bpow (mag x) - / 2 * u2 + / 2 * u2) by ring. apply Rplus_lt_le_compat; [exact Hx|]. apply Rabs_le_inv. now apply error_le_half_ulp. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ