proposition: Lemma round_round_plus_radix_ge_3_aux1 : (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 < x -> 0 < y -> (mag y <= fexp1 (mag x) - 1)%Z -> generic_format beta fexp1 x -> round_round_eq fexp1 fexp2 choice1 choice2 (x + y).
proof: Proof. intros Hbeta fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Px Py Hly Fx. assert (Lxy : mag (x + y) = mag x :> Z); [now apply (mag_plus_separated fexp1); [|apply Rlt_le| |lia]|]. destruct Hexp as (_,(_,(_,Hexp4))). assert (Hf2 : (fexp2 (mag x) <= fexp1 (mag x))%Z); [now apply Hexp4; lia|]. 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 (P1 : (0 < 1)%Z) by lia. unfold round_round_eq. apply round_round_lt_mid. - exact Vfexp1. - exact Vfexp2. - lra. - now rewrite Lxy. - rewrite Lxy. cut (fexp1 (mag x) < mag x)%Z. lia. now apply mag_generic_gt; [|apply Rgt_not_eq|]. - unfold midp. apply (Rplus_lt_reg_r (- round beta fexp1 Zfloor (x + y))). apply (Rlt_le_trans _ _ _ (proj2 (round_round_plus_aux1_aux 1 P1 fexp1 x y Px Py Hly Lxy Fx))). ring_simplify. rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat]. unfold cexp; rewrite Lxy. apply (Rmult_le_reg_r (bpow (- fexp1 (mag x)))); [now apply bpow_gt_0|]. bpow_simplify. apply (Rle_trans _ _ _ Bpow3); lra. - rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat]. unfold round, F2R, scaled_mantissa, cexp; simpl; rewrite Lxy. intro Hf2'. unfold midp. apply (Rplus_lt_reg_r (- round beta fexp1 Zfloor (x + y))); ring_simplify. rewrite <- Rmult_minus_distr_l. apply (Rlt_le_trans _ _ _ (proj2 (round_round_plus_aux1_aux 1 P1 fexp1 x y Px Py Hly Lxy Fx))). rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat]. unfold cexp; rewrite Lxy. apply (Rmult_le_reg_r (bpow (- fexp1 (mag x)))); [now apply bpow_gt_0|]. rewrite (Rmult_assoc (/ 2)). rewrite Rmult_minus_distr_r. bpow_simplify. apply (Rle_trans _ _ _ Bpow3). apply Rle_trans with (/ 2 * (2 / 3)); [lra|]. apply Rmult_le_compat_l; [lra|]. apply (Rplus_le_reg_r (- 1)); ring_simplify. replace (_ - _) with (- (/ 3)) by lra. apply Ropp_le_contravar. now apply Rle_trans with (bpow (- 1)); [apply bpow_le; lia|]. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ