proposition: Lemma round_round_eq_mid_beta_odd_rna_aux4 : forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> Valid_exp fexp2 -> forall x, 0 < x -> (fexp2 (mag x) <= fexp1 (mag x))%Z -> x = midp beta fexp1 x -> round beta fexp1 ZnearestA (round beta fexp2 ZnearestA x) = round beta fexp1 ZnearestA x.
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 x Px Hf2 Xmid. destruct (Zle_or_lt (fexp1 (mag x)) (mag x)) as [H1|H1]. { now apply round_round_eq_mid_beta_odd_rna_aux3. } revert Hf2 H1. destruct (mag x) as (ex,Hex); simpl. specialize (Hex (Rgt_not_eq _ _ Px)). intros Hf2 H1. rewrite Rabs_right in Hex; [|now apply Rle_ge, Rlt_le]. rewrite (round_N_small_pos _ fexp1 _ x ex Hex H1). destruct (Zle_or_lt (fexp1 ex) (fexp2 ex)) as [H2|H2]. - replace (fexp1 ex) with (fexp2 ex) in H1; [|now apply Zle_antisym]. rewrite (round_N_small_pos _ fexp2 _ x ex Hex H1). now rewrite round_0; [|apply valid_rnd_N]. - set (r2 := round beta fexp2 ZnearestA x). destruct (Req_dec r2 0) as [Zr2|Nzr2]. { now rewrite Zr2, round_0; [|apply valid_rnd_N]. } assert (B1 : Rabs (r2 - x) <= / 2 * ulp beta fexp2 x); [now apply error_le_half_ulp|]. unfold round, F2R, scaled_mantissa, cexp; simpl. apply (Rmult_eq_reg_r (bpow (- fexp1 (mag r2)))); [|now apply Rgt_not_eq, bpow_gt_0]. rewrite Rmult_0_l; bpow_simplify. apply IZR_eq, Znearest_imp. simpl; unfold Rminus; rewrite Ropp_0, Rplus_0_r. rewrite Rabs_mult, (Rabs_right (bpow _)); [|now apply Rle_ge, bpow_ge_0]. apply (Rmult_lt_reg_r (bpow (fexp1 (mag r2)))); [now apply bpow_gt_0|]. bpow_simplify. replace r2 with (r2 - x + x) by ring. apply (Rle_lt_trans _ _ _ (Rabs_triang _ _)). apply Rlt_le_trans with (/ 2 * ulp beta fexp2 x + bpow ex); [now apply Rplus_le_lt_compat; [|rewrite Rabs_right; [|apply Rle_ge, Rlt_le]]|]. replace (_ - _ + _) with r2 by ring. assert (Hbeta : (2 <= beta)%Z). { destruct beta as (beta_val,beta_prop). now apply Zle_bool_imp_le. } assert (Hex' : mag x = ex :> Z). { now apply mag_unique; rewrite Rabs_right; [|apply Rle_ge, Rlt_le]. } assert (Hl2 : (mag r2 <= fexp1 ex)%Z). { apply (mag_le_bpow _ _ _ Nzr2). replace r2 with (r2 - x + x) by ring. apply (Rle_lt_trans _ _ _ (Rabs_triang _ _)). apply Rlt_le_trans with (/ 2 * ulp beta fexp2 x + bpow ex); [now apply Rplus_le_lt_compat; [|rewrite Rabs_right; [|apply Rle_ge, Rlt_le]]|]. apply Rle_trans with (2 * bpow (fexp1 ex - 1)). - replace (2 * bpow (fexp1 ex - 1)) with (bpow (fexp1 ex - 1) + bpow (fexp1 ex - 1)) by ring. apply Rplus_le_compat; [|now apply bpow_le; lia]. apply Rle_trans with (bpow (fexp2 ex)); [|now apply bpow_le; lia]. rewrite <- (Rmult_1_l (bpow _)). rewrite ulp_neq_0; try now apply Rgt_not_eq. unfold cexp. rewrite Hex'; apply Rmult_le_compat_r; [apply bpow_ge_0|lra]. - rewrite <- (Rmult_1_l (bpow (fexp1 _))). unfold Zminus; rewrite Zplus_comm, bpow_plus, <- Rmult_assoc. apply Rmult_le_compat_r; [now apply bpow_ge_0|]. apply (Rmult_le_reg_r (bpow 1)); [now apply bpow_gt_0|]. rewrite Rmult_1_l; bpow_simplify. simpl; unfold Z.pow_pos; simpl; rewrite Zmult_1_r. now apply IZR_le. } assert (Hf1r2 : fexp1 (mag r2) = fexp1 ex). { now apply (proj2 (Vfexp1 ex)); [lia|]. } rewrite Hf1r2. replace (bpow ex) with (/ 2 * (2 * bpow ex)) by field. rewrite <- Rmult_plus_distr_l; apply Rmult_le_compat_l; [lra|]. apply Rle_trans with (3 * bpow (fexp1 ex - 1)). + replace (3 * bpow (fexp1 ex - 1)) with (bpow (fexp1 ex - 1) + 2 * bpow (fexp1 ex - 1)) by ring. apply Rplus_le_compat. * rewrite ulp_neq_0; try now apply Rgt_not_eq. apply bpow_le; unfold cexp; rewrite Hex'; lia. * apply Rmult_le_compat_l; [lra|]; apply bpow_le; lia. + rewrite <- (Rmult_1_l (bpow (fexp1 _))). unfold Zminus; rewrite Zplus_comm, bpow_plus, <- Rmult_assoc. apply Rmult_le_compat_r; [now apply bpow_ge_0|]. apply (Rmult_le_reg_r (bpow 1)); [now apply bpow_gt_0|]. rewrite Rmult_1_l; bpow_simplify. simpl; unfold Z.pow_pos; simpl; rewrite Zmult_1_r. apply IZR_le. destruct (Zle_or_lt beta 2) as [Hb2|Hb2]; [|lia]. assert (Hbeta' : beta = 2%Z :> Z); [now apply Zle_antisym|]. exfalso. rewrite <- Zodd_ex_iff in Obeta. apply (Zodd_not_Zeven _ Obeta). now rewrite Hbeta'. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)