proposition: Lemma round_round_lt_mid_further_place : forall (fexp1 fexp2 : Z -> Z), Valid_exp fexp1 -> Valid_exp fexp2 -> forall (choice1 choice2 : Z -> bool), forall x, 0 < x -> (fexp2 (mag x) <= fexp1 (mag x) - 1)%Z -> (fexp1 (mag x) <= mag x)%Z -> x < midp fexp1 x - / 2 * ulp beta fexp2 x -> round_round_eq fexp1 fexp2 choice1 choice2 x.
proof: Proof. intros fexp1 fexp2 Vfexp1 Vfexp2 choice1 choice2 x Px Hf2f1 Hf1. intro Hx2'. assert (Hx2 : x - round beta fexp1 Zfloor x < / 2 * (ulp beta fexp1 x - ulp beta fexp2 x)). { now apply (Rplus_lt_reg_r (round beta fexp1 Zfloor x)); ring_simplify. } revert Hx2. unfold round_round_eq. set (x' := round beta fexp1 Zfloor x). intro Hx2. assert (Pxx' : 0 <= x - x'). { apply Rle_0_minus. apply round_DN_pt. exact Vfexp1. } assert (x < bpow (mag x) - / 2 * bpow (fexp2 (mag x))); [|apply round_round_lt_mid_further_place'; try assumption]... 2: rewrite ulp_neq_0;[assumption|now apply Rgt_not_eq]. destruct (Req_dec x' 0) as [Zx'|Nzx']. - rewrite Zx' in Hx2; rewrite Rminus_0_r in Hx2. apply (Rlt_le_trans _ _ _ Hx2). rewrite Rmult_minus_distr_l. rewrite 2!ulp_neq_0;[idtac|now apply Rgt_not_eq|now apply Rgt_not_eq]. apply Rplus_le_compat_r. apply (Rmult_le_reg_r (bpow (- mag x))); [now apply bpow_gt_0|]. unfold ulp, cexp; bpow_simplify. apply Rmult_le_reg_l with (1 := Rlt_0_2). replace (2 * (/ 2 * _)) with (bpow (fexp1 (mag x) - mag x)) by field. apply Rle_trans with 1; [|lra]. change 1 with (bpow 0); apply bpow_le. lia. - assert (Px' : 0 < x'). { assert (0 <= x'); [|lra]. unfold x'. apply (Rmult_le_reg_r (bpow (- fexp1 (mag x)))); [now apply bpow_gt_0|]. rewrite Rmult_0_l. unfold round, F2R, cexp; simpl; bpow_simplify. apply IZR_le. apply Zfloor_lub. rewrite <- (Rabs_right x); [|now apply Rle_ge; apply Rlt_le]. rewrite scaled_mantissa_abs. apply Rabs_pos. } assert (Hx' : x' <= bpow (mag x) - ulp beta fexp1 x). { apply (Rplus_le_reg_r (ulp beta fexp1 x)); ring_simplify. rewrite <- ulp_DN. - change (round _ _ _ _) with x'. apply id_p_ulp_le_bpow. + exact Px'. + change x' with (round beta fexp1 Zfloor x). now apply generic_format_round; [|apply valid_rnd_DN]. + apply Rle_lt_trans with x. * now apply round_DN_pt. * rewrite <- (Rabs_right x) at 1; [|now apply Rle_ge; apply Rlt_le]. apply bpow_mag_gt. - exact Vfexp1. - now apply Rlt_le. } fold (cexp beta fexp2 x); fold (ulp beta fexp2 x). assert (/ 2 * ulp beta fexp1 x <= ulp beta fexp1 x). rewrite <- (Rmult_1_l (ulp _ _ _)) at 2. apply Rmult_le_compat_r; [|lra]. apply ulp_ge_0. rewrite 2!ulp_neq_0 in Hx2;[|now apply Rgt_not_eq|now apply Rgt_not_eq]. rewrite ulp_neq_0 in Hx';[|now apply Rgt_not_eq]. rewrite ulp_neq_0 in H;[|now apply Rgt_not_eq]. lra. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ