proposition: Lemma round_round_minus_aux2 : forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> Valid_exp fexp2 -> forall (choice1 choice2 : Z -> bool), round_round_plus_hyp fexp1 fexp2 -> forall x y, 0 < y -> y < x -> (mag y <= fexp1 (mag x) - 2)%Z -> (mag y <= fexp1 (mag (x - y)) - 2)%Z -> generic_format beta fexp1 x -> generic_format beta fexp1 y -> round_round_eq fexp1 fexp2 choice1 choice2 (x - y).
proof: Proof. assert (Hbeta : (2 <= beta)%Z). { destruct beta as (beta_val,beta_prop). now apply Zle_bool_imp_le. } intros 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 (Bpow2 : bpow (- 2) <= / 2 * / 2). { replace (/2 * /2) with (/4) by field. rewrite (bpow_opp _ 2). apply Rinv_le; [lra|]. apply (IZR_le (2 * 2) (beta * (beta * 1))). rewrite Zmult_1_r. now apply Zmult_le_compat; lia. } 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)) - 2)). + apply Rle_lt_trans with y; [now apply round_round_minus_aux2_aux; try assumption; lia|]. apply (Rlt_le_trans _ _ _ Ly). now apply bpow_le. + rewrite ulp_neq_0;[idtac|now apply sym_not_eq, Rlt_not_eq, Rgt_minus]. unfold cexp. replace (_ - 2)%Z with (fexp1 (mag (x - y)) - 1 - 1)%Z by ring. unfold Zminus at 1; rewrite bpow_plus. rewrite Rmult_comm. apply Rmult_le_compat. * now apply bpow_ge_0. * now apply bpow_ge_0. * unfold Raux.bpow, Z.pow_pos; simpl. rewrite Zmult_1_r; apply Rinv_le. lra. now apply IZR_le. * apply bpow_le; lia. - intro Hf2'. unfold midp'. apply (Rplus_lt_reg_r (/ 2 * ulp beta fexp1 (x - y) - (x - y) - / 2 * ulp beta fexp2 (x - y))). ring_simplify. 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; try assumption; lia|]. apply (Rlt_le_trans _ _ _ Ly). apply Rle_trans with (bpow (fexp1 (mag (x - y)) - 2)); [now apply bpow_le|]. replace (_ - 2)%Z with (fexp1 (mag (x - y)) - 1 - 1)%Z by ring. unfold Zminus at 1; rewrite bpow_plus. rewrite <- Rmult_minus_distr_l. rewrite Rmult_comm; apply Rmult_le_compat. + apply bpow_ge_0. + apply bpow_ge_0. + unfold Raux.bpow, Z.pow_pos; simpl. rewrite Zmult_1_r; apply Rinv_le; [lra|]. now apply IZR_le. + rewrite 2!ulp_neq_0; try now apply Rgt_not_eq, Rgt_minus. unfold cexp. apply (Rplus_le_reg_r (bpow (fexp2 (mag (x - y))))); ring_simplify. apply Rle_trans with (2 * bpow (fexp1 (mag (x - y)) - 1)). * rewrite double. apply Rplus_le_compat_l. now apply bpow_le. * unfold Zminus; rewrite bpow_plus. rewrite Rmult_comm; rewrite Rmult_assoc. rewrite <- Rmult_1_r. apply Rmult_le_compat_l; [now apply bpow_ge_0|]. unfold Raux.bpow, Z.pow_pos; simpl. rewrite Zmult_1_r. apply IZR_le, Rinv_le in Hbeta. simpl in Hbeta. lra. apply Rlt_0_2. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ