proposition: Lemma round_round_div_aux0 : 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) + 1)%Z -> ~ (bpow (mag (x / y)) - / 2 * ulp beta fexp2 (x / y) <= 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|]|]. set (p := bpow (mag (x / y))). set (u2 := bpow (fexp2 (mag (x / y)))). 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. rewrite ulp_neq_0. 2: apply Rmult_integral_contrapositive_currified; [now apply Rgt_not_eq|idtac]. 2: now apply Rinv_neq_0_compat, Rgt_not_eq. intro Hl. assert (Hr : x / y < p); [now apply Rabs_lt_inv; apply bpow_mag_gt|]. apply (Rlt_irrefl (p - / 2 * u2)). apply (Rle_lt_trans _ _ _ Hl). apply (Rmult_lt_reg_r y _ _ Py). unfold Rdiv; rewrite Rmult_assoc. rewrite Rinv_l; [|now apply Rgt_not_eq]; rewrite Rmult_1_r. destruct (Zle_or_lt Z0 (fexp1 (mag x) - mag (x / y) - fexp1 (mag y))%Z) as [He|He]. - apply Rle_lt_trans with (p * y - p * bpow (fexp1 (mag y))). + rewrite Fx; rewrite Fy at 1. rewrite <- Rmult_assoc. rewrite (Rmult_comm p). unfold p; bpow_simplify. apply (Rmult_le_reg_r (bpow (- mag (x / y) - fexp1 (mag y)))); [now apply bpow_gt_0|]. rewrite Rmult_minus_distr_r. bpow_simplify. rewrite <- IZR_Zpower; [|exact He]. rewrite <- mult_IZR. rewrite <- minus_IZR. apply IZR_le. apply (Zplus_le_reg_r _ _ 1); ring_simplify. apply Zlt_le_succ. apply lt_IZR. rewrite mult_IZR. rewrite IZR_Zpower; [|exact He]. apply (Rmult_lt_reg_r (bpow (fexp1 (mag y) + mag (x / y)))); [now apply bpow_gt_0|]. bpow_simplify. rewrite <- Fx. rewrite bpow_plus. rewrite <- Rmult_assoc; rewrite <- Fy. fold p. apply (Rmult_lt_reg_r (/ y)); [now apply Rinv_0_lt_compat|]. field_simplify; lra. + rewrite Rmult_minus_distr_r. unfold Rminus; apply Rplus_lt_compat_l. apply Ropp_lt_contravar. apply Rlt_le_trans with (u2 * bpow (mag y)). * rewrite <- (Rmult_1_l (u2 * _)). rewrite Rmult_assoc. { apply Rmult_lt_compat. - lra. - now apply Rmult_le_pos; [apply bpow_ge_0|apply Rlt_le]. - lra. - apply Rmult_lt_compat_l; [now apply bpow_gt_0|]. apply Rabs_lt_inv. apply bpow_mag_gt. } * unfold u2, p, ulp, cexp; bpow_simplify; apply bpow_le. apply (Zplus_le_reg_r _ _ (- mag y)); ring_simplify. rewrite (Zplus_comm (- _)); fold (Zminus (mag (x / y)) (mag y)). 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 Rle_lt_trans with (p * y - bpow (fexp1 (mag x))). + rewrite Fx at 1; rewrite Fy at 1. apply (Rmult_le_reg_r (bpow (- fexp1 (mag x)))); [now apply bpow_gt_0|]. rewrite Rmult_minus_distr_r. bpow_simplify. rewrite (Rmult_comm p). unfold p; bpow_simplify. rewrite <- IZR_Zpower by lia. rewrite <- mult_IZR. rewrite <- minus_IZR. apply IZR_le. apply (Zplus_le_reg_r _ _ 1); ring_simplify. apply Zlt_le_succ. apply lt_IZR. rewrite mult_IZR. rewrite IZR_Zpower by lia. apply (Rmult_lt_reg_r (bpow (fexp1 (mag x)))); [now apply bpow_gt_0|bpow_simplify]. rewrite <- Fx. rewrite Zplus_comm; rewrite bpow_plus. rewrite <- Rmult_assoc; rewrite <- Fy. fold p. apply (Rmult_lt_reg_r (/ y)); [now apply Rinv_0_lt_compat|]. field_simplify; lra. + rewrite Rmult_minus_distr_r. unfold Rminus; apply Rplus_lt_compat_l. apply Ropp_lt_contravar. apply Rlt_le_trans with (u2 * bpow (mag y)). * rewrite <- (Rmult_1_l (u2 * _)). rewrite Rmult_assoc. { apply Rmult_lt_compat. - lra. - now apply Rmult_le_pos; [apply bpow_ge_0|apply Rlt_le]. - lra. - apply Rmult_lt_compat_l; [now apply bpow_gt_0|]. apply Rabs_lt_inv. apply bpow_mag_gt. } * unfold u2, p, ulp, cexp; bpow_simplify; apply bpow_le. apply (Zplus_le_reg_r _ _ (- mag y)); ring_simplify. rewrite (Zplus_comm (- _)); fold (Zminus (mag (x / y)) (mag y)). destruct (mag_div_disj x y Px Py) as [Hxy|Hxy]; rewrite Hxy; apply Hexp; try assumption; rewrite <- Hxy; rewrite Hf1; apply Z.le_refl. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ