proposition: Lemma round_round_div_aux2 : forall fexp1 fexp2 : Z -> Z, Valid_exp fexp1 -> Valid_exp fexp2 -> forall (choice1 choice2 : Z -> bool), round_round_div_hyp fexp1 fexp2 -> forall x y, 0 < x -> 0 < y -> generic_format beta fexp1 x -> generic_format beta fexp1 y -> (fexp1 (mag (x / y)) <= mag (x / y))%Z -> ~ (midp fexp1 (x / y) < x / y <= midp fexp1 (x / y) + / 2 * ulp beta fexp2 (x / y)).
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 Hexp x y Px Py Fx Fy Hf1. assert (Hfx : (fexp1 (mag x) < mag x)%Z); [now apply mag_generic_gt; [|apply Rgt_not_eq|]|]. assert (Hfy : (fexp1 (mag y) < mag y)%Z); [now apply mag_generic_gt; [|apply Rgt_not_eq|]|]. cut (~ (/ 2 * ulp beta fexp1 (x / y) < x / y - round beta fexp1 Zfloor (x / y) <= / 2 * (ulp beta fexp1 (x / y) + ulp beta fexp2 (x / y)))). { intro H; intro H'; apply H; split. - apply (Rplus_lt_reg_l (round beta fexp1 Zfloor (x / y))). ring_simplify. apply H'. - apply (Rplus_le_reg_l (round beta fexp1 Zfloor (x / y))). ring_simplify. apply H'. } set (u1 := bpow (fexp1 (mag (x / y)))). set (u2 := bpow (fexp2 (mag (x / y)))). set (x' := round beta fexp1 Zfloor (x / y)). assert (S : (x / y <> 0)%R). apply Rmult_integral_contrapositive_currified; [now apply Rgt_not_eq|idtac]. now apply Rinv_neq_0_compat, Rgt_not_eq. rewrite 2!ulp_neq_0; trivial. revert Fx Fy. unfold generic_format, F2R, scaled_mantissa, cexp; simpl. set (mx := Ztrunc (x * bpow (- fexp1 (mag x)))). set (my := Ztrunc (y * bpow (- fexp1 (mag y)))). intros Fx Fy. intro Hlr. apply (Rlt_irrefl (/ 2 * (u1 + u2))). apply Rlt_le_trans with (x / y - x'); [|now apply Hlr]. apply (Rplus_lt_reg_r x'); ring_simplify. apply (Rmult_lt_reg_r y _ _ Py). unfold Rdiv; rewrite Rmult_assoc. rewrite Rinv_l; [|now apply Rgt_not_eq]; rewrite Rmult_1_r. do 2 rewrite Rmult_plus_distr_r. apply (Rmult_lt_reg_l 2); [lra|]. do 2 rewrite Rmult_plus_distr_l. do 5 rewrite <- Rmult_assoc. rewrite Rinv_r; [|lra]; do 2 rewrite Rmult_1_l. destruct (Zle_or_lt Z0 (fexp1 (mag x) - fexp1 (mag (x / y)) - fexp1 (mag y))%Z) as [He|He]. - apply Rlt_le_trans with (u1 * y + bpow (fexp1 (mag (x / y)) + fexp1 (mag y)) + 2 * x' * y). + apply Rplus_lt_compat_r, Rplus_lt_compat_l. apply Rlt_le_trans with (u2 * bpow (mag y)). * { apply Rmult_lt_compat_l. - apply bpow_gt_0. - apply Rabs_lt_inv. apply bpow_mag_gt. } * unfold u2, ulp, cexp; bpow_simplify; apply bpow_le. apply (Zplus_le_reg_r _ _ (- mag y)); ring_simplify. rewrite <- Zplus_assoc; rewrite (Zplus_comm (- _)). destruct (mag_div_disj x y Px Py) as [Hxy|Hxy]; rewrite Hxy; [now apply Hexp; [| |rewrite <- Hxy]|]. replace (_ - _ + 1)%Z with ((mag x + 1) - mag y)%Z by ring. apply Hexp. { now assert (fexp1 (mag x + 1) <= mag x)%Z; [apply valid_exp|lia]. } { assumption. } replace (_ + 1 - _)%Z with (mag x - mag y + 1)%Z by ring. now rewrite <- Hxy. + apply Rge_le; rewrite Fx at 1; apply Rle_ge. replace (u1 * y) with (u1 * (IZR my * bpow (fexp1 (mag y)))); [|now apply eq_sym; rewrite Fy at 1]. replace (2 * x' * y) with (2 * x' * (IZR my * bpow (fexp1 (mag y)))); [|now apply eq_sym; rewrite Fy at 1]. apply (Rmult_le_reg_r (bpow (- fexp1 (mag (x / y)) - fexp1 (mag y)))); [now apply bpow_gt_0|]. do 2 rewrite Rmult_plus_distr_r. bpow_simplify. rewrite (Rmult_comm u1). unfold u1, ulp, cexp; bpow_simplify. rewrite (Rmult_assoc 2). rewrite (Rmult_comm x'). rewrite (Rmult_assoc 2). unfold x', round, F2R, scaled_mantissa, cexp; simpl. bpow_simplify. rewrite <- (IZR_Zpower _ (_ - _)%Z); [|exact He]. do 4 rewrite <- mult_IZR. do 2 rewrite <- plus_IZR. apply IZR_le. rewrite Zplus_comm, Zplus_assoc. apply Zlt_le_succ. apply lt_IZR. rewrite plus_IZR. do 4 rewrite mult_IZR; simpl. rewrite IZR_Zpower; [|exact He]. apply (Rmult_lt_reg_r (bpow (fexp1 (mag y)))); [now apply bpow_gt_0|]. rewrite Rmult_plus_distr_r. rewrite (Rmult_comm _ (IZR _)). do 2 rewrite Rmult_assoc. rewrite <- Fy. bpow_simplify. unfold Zminus; rewrite bpow_plus. rewrite (Rmult_assoc _ (IZR mx)). rewrite <- (Rmult_assoc (IZR mx)). rewrite <- Fx. apply (Rmult_lt_reg_r (bpow (fexp1 (mag (x / y))))); [now apply bpow_gt_0|]. rewrite Rmult_plus_distr_r. bpow_simplify. rewrite (Rmult_comm _ y). do 2 rewrite Rmult_assoc. change (IZR (Zfloor _) * _) with x'. change (bpow _) with u1. apply (Rmult_lt_reg_l (/ 2)); [lra|]. rewrite Rmult_plus_distr_l. do 4 rewrite <- Rmult_assoc. rewrite Rinv_l; [|lra]; do 2 rewrite Rmult_1_l. apply (Rplus_lt_reg_r (- y * x')); ring_simplify. apply (Rmult_lt_reg_l (/ y)); [now apply Rinv_0_lt_compat|]. rewrite Rmult_plus_distr_l. do 3 rewrite <- Rmult_assoc. rewrite Ropp_mult_distr_r_reverse. rewrite Ropp_mult_distr_l_reverse. rewrite Rinv_l; [|now apply Rgt_not_eq]; do 2 rewrite Rmult_1_l. rewrite (Rmult_comm (/ y)). now rewrite (Rplus_comm (- x')). - apply Rlt_le_trans with (2 * x' * y + u1 * y + bpow (fexp1 (mag x))). + rewrite Rplus_comm, Rplus_assoc; do 2 apply Rplus_lt_compat_l. apply Rlt_le_trans with (u2 * bpow (mag y)). * apply Rmult_lt_compat_l. now apply bpow_gt_0. now apply Rabs_lt_inv; apply bpow_mag_gt. * unfold u2, ulp, cexp; bpow_simplify; apply bpow_le. apply (Zplus_le_reg_r _ _ (- mag y)); ring_simplify. rewrite (Zplus_comm (- _)). destruct (mag_div_disj x y Px Py) as [Hxy|Hxy]; rewrite Hxy; apply Hexp; try assumption; rewrite <- Hxy; lia. + apply Rge_le; rewrite Fx at 1; apply Rle_ge. rewrite Fy at 1 2. apply (Rmult_le_reg_r (bpow (- fexp1 (mag x)))); [now apply bpow_gt_0|]. do 2 rewrite Rmult_plus_distr_r. bpow_simplify. replace (2 * x' * _ * _) with (2 * IZR my * x' * bpow (fexp1 (mag y) - fexp1 (mag x))) by ring. rewrite (Rmult_comm u1). unfold x', u1, round, F2R, ulp, scaled_mantissa, cexp; simpl. bpow_simplify. rewrite <- (IZR_Zpower _ (_ - _)%Z) by lia. do 5 rewrite <- mult_IZR. do 2 rewrite <- plus_IZR. apply IZR_le. apply Zlt_le_succ. apply lt_IZR. rewrite plus_IZR. do 5 rewrite mult_IZR; simpl. rewrite IZR_Zpower by lia. apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|]. rewrite (Rmult_assoc _ (IZR mx)). rewrite <- Fx. rewrite Rmult_plus_distr_r. bpow_simplify. rewrite bpow_plus. rewrite Rmult_assoc. rewrite <- (Rmult_assoc (IZR _)). change (IZR _ * bpow _) with x'. do 2 rewrite (Rmult_comm _ (bpow (fexp1 (mag y)))). rewrite Rmult_assoc. do 2 rewrite <- (Rmult_assoc (IZR my)). rewrite <- Fy. change (bpow _) with u1. apply (Rmult_lt_reg_l (/ 2)); [lra|]. rewrite Rmult_plus_distr_l. do 4 rewrite <- Rmult_assoc. rewrite Rinv_l; [|lra]; do 2 rewrite Rmult_1_l. apply (Rplus_lt_reg_r (- y * x')); ring_simplify. apply (Rmult_lt_reg_l (/ y)); [now apply Rinv_0_lt_compat|]. rewrite Rmult_plus_distr_l. do 3 rewrite <- Rmult_assoc. rewrite Ropp_mult_distr_r_reverse. rewrite Ropp_mult_distr_l_reverse. rewrite Rinv_l; [|now apply Rgt_not_eq]; do 2 rewrite Rmult_1_l. rewrite (Rmult_comm (/ y)). now rewrite (Rplus_comm (- x')). Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ