proposition: Lemma round_round_really_zero : forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> Valid_exp fexp2 -> forall (choice1 choice2 : Z -> bool), forall x, 0 < x -> (mag x <= fexp1 (mag x) - 2)%Z -> round_round_eq fexp1 fexp2 choice1 choice2 x.
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf1. 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. } unfold round_round_eq. rewrite (round_N_small_pos beta fexp1 _ x (mag x)); [|exact Hlx|lia]. set (x'' := round beta fexp2 (Znearest choice2) x). destruct (Req_dec x'' 0) as [Zx''|Nzx'']; [now rewrite Zx''; rewrite round_0; [|apply valid_rnd_N]|]. destruct (Zle_or_lt (fexp2 (mag x)) (mag x)). - destruct (Rlt_or_le x'' (bpow (mag x))). + rewrite (round_N_small_pos beta fexp1 _ _ (mag x)); [reflexivity|split; [|exact H0]|lia]. apply round_large_pos_ge_bpow; [now apply valid_rnd_N| |now apply Hlx]. fold x''; assert (0 <= x''); [|lra]; unfold x''. rewrite <- (round_0 beta fexp2 (Znearest choice2)). now apply round_le; [|apply valid_rnd_N|apply Rlt_le]. + assert (Hx'' : x'' = bpow (mag x)). { apply Rle_antisym; [|exact H0]. rewrite <- (round_generic beta fexp2 (Znearest choice2) (bpow _)). - now apply round_le; [|apply valid_rnd_N|apply Rlt_le]. - now apply generic_format_bpow'. } rewrite Hx''. unfold round, F2R, scaled_mantissa, cexp; simpl. rewrite mag_bpow. assert (Hf11 : (fexp1 (mag x + 1) = fexp1 (mag x) :> Z)%Z); [apply Vfexp1; lia|]. rewrite Hf11. apply (Rmult_eq_reg_r (bpow (- fexp1 (mag x)))); [|now apply Rgt_not_eq; apply bpow_gt_0]. rewrite Rmult_0_l; bpow_simplify. apply IZR_eq. apply Znearest_imp. simpl; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r. rewrite Rabs_right; [|now apply Rle_ge; apply bpow_ge_0]. apply Rle_lt_trans with (bpow (- 2)); [now apply bpow_le; lia|]. unfold Raux.bpow, Z.pow_pos; simpl; rewrite Zmult_1_r. assert (Hbeta : (2 <= beta)%Z). { destruct beta as (beta_val,beta_prop); simpl. now apply Zle_bool_imp_le. } apply Rinv_lt_contravar. * apply Rmult_lt_0_compat; [lra|]. rewrite mult_IZR; apply Rmult_lt_0_compat; apply IZR_lt; lia. * apply IZR_lt. apply (Z.le_lt_trans _ _ _ Hbeta). rewrite <- (Zmult_1_r beta) at 1. apply Zmult_lt_compat_l; lia. - exfalso; apply Nzx''. now apply (round_N_small_pos beta _ _ _ (mag x)). Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ