proposition: Lemma round_round_plus_aux1 : 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 < x -> 0 < y -> (mag y <= fexp1 (mag x) - 2)%Z -> generic_format beta fexp1 x -> 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 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 (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 (P2 : (0 < 2)%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 2 P2 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 _ _ _ Bpow2). rewrite <- (Rmult_1_r (/ 2)) at 3. apply Rmult_le_compat_l; 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'. apply (Rmult_lt_reg_r (bpow (- fexp1 (mag x)))); [now apply bpow_gt_0|]. apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|]. bpow_simplify. apply (Rplus_lt_reg_r (- round beta fexp1 Zfloor (x + y))). unfold midp; ring_simplify. apply (Rlt_le_trans _ _ _ (proj2 (round_round_plus_aux1_aux 2 P2 fexp1 x y Px Py Hly Lxy Fx))). apply (Rmult_le_reg_r (bpow (- fexp1 (mag x)))); [now apply bpow_gt_0|]. rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq, Rplus_lt_0_compat]. unfold cexp; rewrite Lxy, Rmult_minus_distr_r; bpow_simplify. apply (Rle_trans _ _ _ Bpow2). rewrite <- (Rmult_1_r (/ 2)) at 3; rewrite <- Rmult_minus_distr_l. apply Rmult_le_compat_l; [lra|]. apply (Rplus_le_reg_r (- 1)); ring_simplify. replace (_ - _) with (- (/ 2)) by lra. apply Ropp_le_contravar. { apply Rle_trans with (bpow (- 1)). - apply bpow_le; lia. - unfold Raux.bpow, Z.pow_pos; simpl. apply Rinv_le; [lra|]. apply IZR_le; lia. } Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ