proposition: Lemma round_round_minus_radix_ge_3_aux2 : (3 <= beta)%Z -> forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> Valid_exp fexp2 -> forall (choice1 choice2 : Z -> bool), round_round_plus_radix_ge_3_hyp fexp1 fexp2 -> forall x y, 0 < y -> y < x -> (mag y <= fexp1 (mag x) - 1)%Z -> (mag y <= fexp1 (mag (x - y)) - 1)%Z -> generic_format beta fexp1 x -> generic_format beta fexp1 y -> round_round_eq fexp1 fexp2 choice1 choice2 (x - y).
proof: Proof. intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Py Hxy Hly Hly' Fx Fy. assert (Px := Rlt_trans 0 y x Py Hxy). destruct Hexp as (_,(_,(_,Hexp4))). assert (Hf2 : (fexp2 (mag x) <= fexp1 (mag x))%Z); [now apply Hexp4; lia|]. assert (Hfx : (fexp1 (mag x) < mag x)%Z); [now apply mag_generic_gt; [|apply Rgt_not_eq|]|]. assert (Bpow3 : bpow (- 1) <= / 3). { unfold Raux.bpow, Z.pow_pos; simpl. rewrite Zmult_1_r. apply Rinv_le; [lra|]. now apply IZR_le. } assert (Ly : y < bpow (mag y)). { apply Rabs_lt_inv. apply bpow_mag_gt. } unfold round_round_eq. apply round_round_gt_mid. - exact Vfexp1. - exact Vfexp2. - lra. - apply Hexp4; lia. - cut (fexp1 (mag (x - y)) < mag (x - y))%Z. lia. apply (valid_exp_large fexp1 (mag x - 1)). + apply (valid_exp_large fexp1 (mag y)); [|lia]. now apply mag_generic_gt; [|apply Rgt_not_eq|]. + now apply mag_minus_lb; [| |lia]. - unfold midp'. apply (Rplus_lt_reg_r (/ 2 * ulp beta fexp1 (x - y) - (x - y))). ring_simplify. replace (_ + _) with (round beta fexp1 Zceil (x - y) - (x - y)) by ring. apply Rlt_le_trans with (bpow (fexp1 (mag (x - y)) - 1)). + apply Rle_lt_trans with y; [now apply round_round_minus_aux2_aux|]. apply (Rlt_le_trans _ _ _ Ly). now apply bpow_le. + rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rgt_minus]. unfold cexp. unfold Zminus at 1; rewrite bpow_plus. rewrite Rmult_comm. apply Rmult_le_compat_r; [now apply bpow_ge_0|]. unfold Raux.bpow, Z.pow_pos; simpl. rewrite Zmult_1_r; apply Rinv_le; [lra|]. now apply IZR_le; lia. - intro Hf2'. unfold midp'. apply (Rplus_lt_reg_r (/ 2 * (ulp beta fexp1 (x - y) - ulp beta fexp2 (x - y)) - (x - y))). ring_simplify; rewrite <- Rmult_minus_distr_l. replace (_ + _) with (round beta fexp1 Zceil (x - y) - (x - y)) by ring. apply Rle_lt_trans with y; [now apply round_round_minus_aux2_aux|]. apply (Rlt_le_trans _ _ _ Ly). apply Rle_trans with (bpow (fexp1 (mag (x - y)) - 1)); [now apply bpow_le|]. rewrite 2!ulp_neq_0; try now apply Rgt_not_eq, Rgt_minus. unfold cexp. apply (Rmult_le_reg_r (bpow (- fexp1 (mag (x - y))))); [now apply bpow_gt_0|]. rewrite Rmult_assoc. rewrite Rmult_minus_distr_r. bpow_simplify. apply Rle_trans with (/ 3). + unfold Raux.bpow, Z.pow_pos; simpl. rewrite Zmult_1_r; apply Rinv_le; [lra|]. now apply IZR_le. + replace (/ 3) with (/ 2 * (2 / 3)) by field. apply Rmult_le_compat_l; [lra|]. apply (Rplus_le_reg_r (- 1)); ring_simplify. replace (_ - _) with (- / 3) by field. apply Ropp_le_contravar. apply Rle_trans with (bpow (- 1)). * apply bpow_le; lia. * unfold Raux.bpow, Z.pow_pos; simpl. rewrite Zmult_1_r; apply Rinv_le; [lra|]. now apply IZR_le. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ