proposition: Lemma round_round_eq_mid_beta_odd_rna_aux1 : forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> Valid_exp fexp2 -> forall x, 0 < x -> (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z -> (fexp1 (mag x) <= 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 Hf1. unfold midp. rewrite ulp_neq_0; try now apply Rgt_not_eq. set (rd := round beta fexp1 Zfloor x). set (u := bpow (fexp1 (mag x))). intro Xmid. apply (Rplus_eq_compat_l (- rd)) in Xmid; ring_simplify in Xmid. rewrite Rplus_comm in Xmid; fold (x - rd) in Xmid. assert (Xmid' : x = rd + / 2 * u); [now apply (Rplus_eq_reg_r (- rd)); ring_simplify|]. destruct (Req_dec rd 0) as [Zrd|Nzrd]. - set (rd1 := round beta fexp1 ZnearestA x). rewrite Zrd in Xmid'; rewrite Rplus_0_l in Xmid'. rewrite Xmid'. replace u with (IZR beta * bpow (fexp1 (mag x) - 1)); [|now rewrite <- bpow_1; unfold u, ulp, cexp; bpow_simplify]. rewrite <- Rmult_assoc. elim Obeta; intros m Hm. rewrite Hm. rewrite plus_IZR; rewrite mult_IZR. rewrite Rmult_plus_distr_l; rewrite <- Rmult_assoc; simpl. replace (/ 2 * 2) with 1 by field; rewrite Rmult_1_l; rewrite Rmult_1_r. rewrite Rmult_plus_distr_r. set (x'' := IZR m * bpow (fexp1 (mag x) - 1)). assert (Hbeta : (2 <= beta)%Z). { destruct beta as (beta_val,beta_prop). now apply Zle_bool_imp_le. } assert (Pm : (1 <= m)%Z) by lia. assert (Px'' : 0 < x''). { unfold x''. apply Rmult_lt_0_compat. - apply IZR_lt; lia. - now apply bpow_gt_0. } assert (Hx'' : x'' = IZR (Zfloor (x'' * bpow (- (fexp1 (mag x) - 1)))) * bpow (fexp1 (mag x) - 1)). { unfold x''; bpow_simplify. now rewrite Zfloor_IZR. } destruct (midpoint_beta_odd_remains_pos x'' Px'' (fexp1 (mag x) - 1) (fexp2 (mag x)) Hf2 Hx'') as (x2,(Hx2_0,(Hx2_1,(Hx2_2,Hx2_3)))). rewrite Hx2_3. assert (Hlx : mag x = fexp1 (mag x) :> Z). { apply mag_unique; split. - apply Rabs_ge; right. apply Rle_trans with (/2 * u); [|now rewrite Xmid'; apply Rle_refl]. unfold Zminus; rewrite Zplus_comm; rewrite bpow_plus. rewrite bpow_opp; rewrite bpow_1. apply Rmult_le_compat. + apply Rlt_le; apply Rinv_0_lt_compat. apply IZR_lt; lia. + apply bpow_ge_0. + apply Rinv_le; [lra|]. now apply IZR_le. + unfold u, ulp, cexp; apply Rle_refl. - rewrite Rabs_right; [|now apply Rle_ge; apply Rlt_le]. rewrite Xmid' at 1. unfold u, ulp, cexp. rewrite <- Rmult_1_l. apply Rmult_lt_compat_r; [|lra]. apply bpow_gt_0. } assert (Hlx'' : mag x'' = mag x :> Z). { apply mag_unique; split. - apply Rabs_ge; right. unfold x''; rewrite <- Hlx. rewrite <- (Rmult_1_l (bpow _)) at 1. apply Rmult_le_compat_r. + apply bpow_ge_0. + now apply IZR_le. - rewrite Rabs_right; [|now apply Rle_ge; apply Rlt_le]. unfold x''; rewrite <- Hlx. unfold Zminus; rewrite Zplus_comm; rewrite bpow_plus; rewrite <- Rmult_assoc. rewrite <- Rmult_1_l; apply Rmult_lt_compat_r; [now apply bpow_gt_0|]. apply (Rmult_lt_reg_r (bpow 1)); bpow_simplify; rewrite bpow_1. + apply IZR_lt; lia. + rewrite Rmult_1_l; apply IZR_lt. lia. } assert (Hl2 : mag (x2 + / 2 * bpow (fexp2 (mag x))) = mag x2 :> Z). { apply (mag_plus_eps beta fexp2); [| |split]. - exact Hx2_0. - unfold generic_format, F2R, scaled_mantissa, cexp; simpl. rewrite Hx2_1, Hlx'', Ztrunc_floor; [exact Hx2_2|]. now apply Rmult_le_pos; [apply Rlt_le|apply bpow_ge_0]. - apply Rmult_le_pos; [lra|apply bpow_ge_0]. - rewrite ulp_neq_0; try now apply Rgt_not_eq. unfold cexp; rewrite Hx2_1; rewrite Hlx''. rewrite <- Rmult_1_l; apply Rmult_lt_compat_r; [|lra]. apply bpow_gt_0. } unfold round at 2, F2R, scaled_mantissa, cexp; simpl. rewrite Hl2; rewrite Hx2_1; rewrite Hlx''. rewrite Rmult_plus_distr_r; bpow_simplify. rewrite Hx2_2; bpow_simplify. assert (Hfl : (Zfloor (IZR (Zfloor (x2 * bpow (- fexp2 (mag x)))) + / 2) = Zfloor (x2 * bpow (- fexp2 (mag x))))%Z). { apply Zfloor_imp; split. - rewrite <- (Rplus_0_r (IZR _)) at 1. apply Rplus_le_compat_l; lra. - rewrite plus_IZR. apply Rplus_lt_compat_l; simpl; lra. } unfold Znearest at 2. rewrite Hfl; replace (_ + / 2 - _) with (/ 2) by ring. rewrite Rcompare_Eq; [|reflexivity]. assert (H : (0 <=? Zfloor (x2 * bpow (- fexp2 (mag x))))%Z = true); [|rewrite H; simpl; clear H]. { apply Zle_bool_true. apply le_IZR; simpl. apply (Rmult_le_reg_r (bpow (fexp2 (mag x)))); [now apply bpow_gt_0|rewrite Rmult_0_l]. now rewrite <- Hx2_2; apply Rlt_le. } assert (Hce : (Zceil (IZR (Zfloor (x2 * bpow (- fexp2 (mag x)))) + / 2) = Zfloor (x2 * bpow (- fexp2 (mag x))) + 1)%Z). { apply Zceil_imp; split. - unfold Zminus; rewrite <- Zplus_assoc; rewrite plus_IZR. apply Rplus_lt_compat_l; simpl; lra. - rewrite plus_IZR. apply Rplus_le_compat_l; simpl; lra. } rewrite Hce. rewrite plus_IZR; rewrite Rmult_plus_distr_r; simpl. rewrite <- Hx2_2; rewrite Rmult_1_l. replace (x2 + _) with (x2 + / 2 * bpow (fexp2 (mag x)) + / 2 * bpow (fexp2 (mag x))) by field. rewrite <- Hx2_3; unfold x''. rewrite <- Rmult_plus_distr_r. replace (IZR m) with (/ 2 * (2 * IZR m)) by field. rewrite <- (Rmult_1_r (/ 2)) at 2; rewrite <- Rmult_plus_distr_l. rewrite <- mult_IZR, <- plus_IZR. rewrite <- Hm. unfold Zminus; rewrite Zplus_comm; rewrite bpow_plus. rewrite <- Rmult_assoc; rewrite (Rmult_assoc (/ 2)). rewrite <- bpow_1; bpow_simplify. replace (/ 2 * _) with x. set (rd2 := round beta fexp1 ZnearestA (x + / 2 * bpow (fexp2 (mag x)))). unfold rd1; rewrite Xmid'. unfold round, F2R, scaled_mantissa, cexp; simpl. replace (fexp1 _) with (fexp1 (mag x)); [|now rewrite Xmid']. unfold u, ulp, cexp; bpow_simplify. unfold Znearest. assert (Zfh : (Zfloor (/ 2) = 0)%Z); [now apply Zfloor_imp; split; simpl; lra|]. rewrite Zfh; simpl. unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r. rewrite Rcompare_Eq; [|reflexivity]; simpl. assert (Zch : (Zceil (/ 2) = 1)%Z); [now apply Zceil_imp; split; simpl; lra|]. rewrite Zch; simpl; rewrite Rmult_1_l. unfold rd2; clear rd2. assert (Hlx' : mag (x + / 2 * bpow (fexp2 (mag x))) = fexp1 (mag x) :> Z). { apply mag_unique; split. - apply Rabs_ge; right. apply Rle_trans with (/2 * u). + unfold Zminus; rewrite Zplus_comm; rewrite bpow_plus. rewrite bpow_opp; rewrite bpow_1. apply Rmult_le_compat. * apply Rlt_le; apply Rinv_0_lt_compat. apply IZR_lt; lia. * apply bpow_ge_0. * apply Rinv_le; [lra|]. now apply IZR_le. * unfold u, ulp, cexp; apply Rle_refl. + rewrite <- (Rplus_0_r (/ 2 * u)). rewrite Xmid'. apply Rplus_le_compat_l. apply Rmult_le_pos; [lra|]. apply bpow_ge_0. - rewrite Rabs_right. + rewrite Xmid' at 1. rewrite <- Rmult_plus_distr_l. apply Rlt_le_trans with (/ 2 * (2 * u)). * apply Rmult_lt_compat_l; [lra|]. replace (2 * u) with (u + u) by ring. apply Rplus_lt_compat_l. unfold u, ulp, cexp; apply bpow_lt. lia. * replace (/ 2 * _) with u by field. unfold u, ulp, cexp; apply Rle_refl. + apply Rle_ge. apply Rplus_le_le_0_compat. * now apply Rlt_le. * apply Rmult_le_pos; [lra|]. apply bpow_ge_0. } unfold round, F2R, scaled_mantissa, cexp; simpl. rewrite Hlx'. do 2 rewrite <- Hlx. rewrite <- Rmult_1_l; apply Rmult_eq_compat_r. unfold Znearest. assert (Hfl' : (Zfloor ((x + / 2 * bpow (fexp2 (mag x))) * bpow (- mag x)) = 0)%Z). { apply Zfloor_imp; split; simpl. - apply (Rmult_le_reg_r (bpow (mag x))); [now apply bpow_gt_0|]. rewrite Rmult_0_l; bpow_simplify. apply Rplus_le_le_0_compat. + now apply Rlt_le. + apply Rmult_le_pos; [lra|]. apply bpow_ge_0. - apply (Rmult_lt_reg_r (bpow (mag x))); [now apply bpow_gt_0|]. rewrite Rmult_1_l; bpow_simplify. apply Rlt_le_trans with (/ 2 * (2 * u)). * rewrite Xmid' at 1. rewrite <- Rmult_plus_distr_l. apply Rmult_lt_compat_l; [lra|]. replace (2 * u) with (u + u) by ring. apply Rplus_lt_compat_l. unfold u, ulp, cexp; apply bpow_lt. lia. * replace (/ 2 * _) with u by field. unfold u, ulp, cexp; rewrite <- Hlx; apply Rle_refl. } rewrite Hfl'; simpl; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r. assert (H : Rcompare ((x + / 2 * bpow (fexp2 (mag x))) * bpow (- mag x)) (/ 2) = Gt); [|rewrite H; clear H; simpl]. { apply Rcompare_Gt. apply (Rmult_lt_reg_r (bpow (mag x))); [now apply bpow_gt_0|]. bpow_simplify. rewrite Hlx at 1; change (bpow (fexp1 _)) with u. rewrite <- Xmid'. rewrite <- (Rplus_0_r x) at 1. apply Rplus_lt_compat_l. apply Rmult_lt_0_compat; [lra|]. apply bpow_gt_0. } apply f_equal; apply Zceil_imp; simpl; split. + apply Rmult_lt_0_compat; [|now apply bpow_gt_0]. apply Rplus_lt_0_compat; [exact Px|]. apply Rmult_lt_0_compat; [lra|]. apply bpow_gt_0. + apply (Rmult_le_reg_r (bpow (mag x))); [now apply bpow_gt_0|]. rewrite Rmult_1_l; bpow_simplify. rewrite Xmid' at 1; rewrite <- Rmult_plus_distr_l. apply (Rmult_le_reg_l 2); [lra|]. rewrite <- Rmult_assoc; replace (2 * _) with 1 by field; rewrite Rmult_1_l. rewrite double. unfold u, ulp, cexp; rewrite <- Hlx. apply Rplus_le_compat_l; apply bpow_le; lia. - assert (Prd : 0 < rd). { assert (H : 0 <= rd); [|lra]. rewrite <- (round_0 beta fexp1 Zfloor); unfold rd. apply round_le. - exact Vfexp1. - apply valid_rnd_DN. - now apply Rlt_le. } assert (Hlr : mag x = mag rd :> Z). { apply eq_sym. apply mag_DN; [exact Vfexp1|]. exact Prd. } destruct (midpoint_beta_odd_remains_pos rd Prd (fexp1 (mag x)) (fexp2 (mag x))) as (x2,(Hx2_0,(Hx2_1,(Hx2_2,Hx2_3)))); [lia| |]. { rewrite Hlr. rewrite <- Ztrunc_floor. - apply generic_format_round; [exact Vfexp1|]. apply valid_rnd_DN. - now apply Rmult_le_pos; [apply Rlt_le|apply bpow_ge_0]. } change (bpow (fexp1 _)) with u in Hx2_3. rewrite <- Xmid' in Hx2_3. set (rd1 := round beta fexp1 ZnearestA x). rewrite Hx2_3. unfold round at 2, F2R, scaled_mantissa, cexp; simpl. rewrite <- Hx2_3. assert (Hfl : IZR (Zfloor (x * bpow (- fexp2 (mag x)))) = x2 * bpow (- fexp2 (mag x))). { rewrite Hx2_3 at 1. rewrite Rmult_plus_distr_r; bpow_simplify. rewrite Hx2_2; bpow_simplify. apply f_equal. apply Zfloor_imp; split. - rewrite <- (Rplus_0_r (IZR _)) at 1. apply Rplus_le_compat_l; lra. - rewrite plus_IZR; simpl. apply Rplus_lt_compat_l; lra. } unfold Znearest at 2. rewrite Hfl. replace (x * _ - x2 * _) with (/ 2); [|now rewrite Hx2_3 at 1; rewrite Rmult_plus_distr_r; bpow_simplify; ring]. rewrite Rcompare_Eq; [|reflexivity]. rewrite Zle_bool_true; [|now apply le_IZR; simpl; rewrite Hfl; apply Rmult_le_pos; [apply Rlt_le|apply bpow_ge_0]]. assert (Hce : IZR (Zceil (x * bpow (- fexp2 (mag x)))) * bpow (fexp2 (mag x)) = x2 + bpow (fexp2 (mag x))). { apply (Rmult_eq_reg_r (bpow (- fexp2 (mag x)))); [|now apply Rgt_not_eq; apply bpow_gt_0]. rewrite Rmult_plus_distr_r; bpow_simplify. rewrite Hx2_2; bpow_simplify. rewrite <- plus_IZR; apply f_equal. rewrite Hx2_3 at 1. rewrite Rmult_plus_distr_r; bpow_simplify. rewrite Hx2_2 at 1; bpow_simplify. set (x2b := Zfloor (x2 * bpow (- fexp2 (mag x)))). apply Zceil_imp; split. - replace (_ - _)%Z with x2b by ring. rewrite <- (Rplus_0_r (IZR _)) at 1; apply Rplus_lt_compat_l; lra. - rewrite plus_IZR; simpl; apply Rplus_le_compat_l; lra. } rewrite Hce. unfold round, F2R, scaled_mantissa, cexp; simpl. set (f1 := fexp1 (mag x)). set (f2 := fexp2 (mag x)). assert (Hx2b2 : x2 + bpow f2 = x + / 2 * bpow f2). { apply (Rplus_eq_reg_r (- / 2 * bpow f2)); field_simplify. unfold Rdiv; apply Rmult_eq_compat_r. now rewrite Hx2_3; field_simplify. } assert (Hl2 : mag (x2 + bpow f2) = mag x :> Z). { rewrite Hx2b2. rewrite Hlr; rewrite Xmid'. rewrite Rplus_assoc. apply (mag_plus_eps beta fexp1 rd Prd); [|split]. - apply generic_format_round; [exact Vfexp1|apply valid_rnd_DN]. - apply Rplus_le_le_0_compat; (apply Rmult_le_pos; [lra|apply bpow_ge_0]). - rewrite <- Rmult_plus_distr_l. apply (Rmult_lt_reg_l 2); [lra|]. rewrite <- Rmult_assoc; replace (2 * / 2) with 1 by field; rewrite Rmult_1_l. rewrite ulp_neq_0; trivial. unfold cexp; rewrite <- Hlr; change (bpow (fexp1 _)) with u. rewrite double. apply Rplus_lt_compat_l; unfold u, ulp, cexp, f2; apply bpow_lt. lia. } rewrite Hl2. rewrite Hx2b2. rewrite Xmid' at 1; rewrite Rplus_assoc. fold f1. assert (Hrd : rd * bpow (- f1) = IZR (Zfloor (x * bpow (- f1)))). { unfold rd, round, F2R, scaled_mantissa, cexp; simpl. now fold f1; bpow_simplify. } assert (Hfld : IZR (Zfloor ((rd + (/ 2 * u + / 2 * bpow f2)) * bpow (- f1))) = rd * bpow (- f1)). { rewrite Rmult_plus_distr_r; rewrite Hrd. apply f_equal. apply Zfloor_imp; split. - rewrite <- (Rplus_0_r (IZR _)) at 1; apply Rplus_le_compat_l. apply Rmult_le_pos; [|now apply bpow_ge_0]. apply Rplus_le_le_0_compat; (apply Rmult_le_pos; [lra|apply bpow_ge_0]). - rewrite plus_IZR; apply Rplus_lt_compat_l; simpl. apply (Rmult_lt_reg_r (bpow (f1))); [now apply bpow_gt_0|]; rewrite Rmult_1_l; bpow_simplify. rewrite <- Rmult_plus_distr_l. apply (Rmult_lt_reg_l 2); [lra|]; rewrite <- Rmult_assoc. replace (2 * / 2) with 1 by field; rewrite Rmult_1_l. change (bpow f1) with u. rewrite double. apply Rplus_lt_compat_l. unfold f2, u, ulp, cexp; apply bpow_lt; lia. } unfold Znearest. rewrite Hfld. replace (_ - rd * bpow _) with (/ 2 * (u + bpow f2) * bpow (- f1)) by ring. assert (H : / 2 < / 2 * (u + bpow f2) * bpow (- f1)). { unfold u, ulp, cexp; fold f1. rewrite Rmult_assoc. rewrite <- (Rmult_1_r (/ 2)) at 1; apply Rmult_lt_compat_l; [lra|]. rewrite Rmult_plus_distr_r; bpow_simplify. rewrite <- (Rplus_0_r 1) at 1; apply Rplus_lt_compat_l. apply bpow_gt_0. } rewrite Rcompare_Gt; [clear H|exact H]. unfold rd1, round, F2R, scaled_mantissa, cexp; simpl; fold f1. apply Rmult_eq_compat_r; apply f_equal. unfold Znearest. rewrite <- Hrd. rewrite <- Rmult_minus_distr_r. replace (x - rd) with (/ 2 * u). rewrite Rmult_assoc; unfold u, ulp, cexp; fold f1; bpow_simplify. rewrite Rcompare_Eq; [|reflexivity]. rewrite Zle_bool_true; [|now apply Zfloor_lub; simpl; apply Rmult_le_pos; [apply Rlt_le|apply bpow_ge_0]]. rewrite Xmid'; do 3 rewrite Rmult_plus_distr_r. rewrite Hrd. bpow_simplify. apply eq_trans with (Zfloor (x * bpow (- f1)) + 1)%Z; [|apply eq_sym]; apply Zceil_imp; split. + unfold Zminus; rewrite <- Zplus_assoc; rewrite plus_IZR. replace (1 + _)%Z with Z0 by ring; simpl; apply Rplus_lt_compat_l. apply Rplus_lt_0_compat; [lra|]. apply Rmult_lt_0_compat; [lra|apply bpow_gt_0]. + rewrite plus_IZR; apply Rplus_le_compat_l; simpl. apply (Rplus_le_reg_r (- / 2)); ring_simplify. apply (Rmult_le_reg_l (/ 2)); [lra|]. field_simplify; unfold Rdiv; apply Rmult_le_compat_r; [lra|]. change 1 with (bpow 0); apply bpow_le; unfold f1, f2; lia. + unfold Zminus; rewrite <- Zplus_assoc; rewrite plus_IZR. replace (1 + _)%Z with Z0 by ring; simpl; apply Rplus_lt_compat_l. apply Rmult_lt_0_compat; [|now apply bpow_gt_0]. apply Rmult_lt_0_compat; [lra|apply bpow_gt_0]. + rewrite plus_IZR; apply Rplus_le_compat_l; simpl. unfold u, ulp, cexp; fold f1; bpow_simplify; lra. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core FTZ Double_rounding)