proposition: Theorem UlpFlessuGe : Fcanonic radix b u -> (/ (4 * (powerRZ radix precision - 1) * (1 + powerRZ radix (- precision))) * ((1 - powerRZ radix (Z.succ (- precision))) * Rabs y) + - (/ (4 * (powerRZ radix precision - 1) * (1 + powerRZ radix (- precision)) * (1 - powerRZ radix (- precision))) * ((1 - powerRZ radix (Z.succ (- precision))) * Rabs (a * x))) + - (powerRZ radix (Z.pred (- dExp b)) * (/ (2 * (powerRZ radix precision - 1)) + / (4 * (powerRZ radix precision - 1) * (1 + powerRZ radix (- precision)) * (1 - powerRZ radix (- precision))) * (1 - powerRZ radix (Z.succ (- precision))))) <= / 4 * Fulp b radix precision (FLess u))%R.
proof: Proof. intros Cu. cut (0 < 1 - powerRZ radix (- precision))%R; [ intros H'1 | idtac ]. 2: apply Rplus_lt_reg_r with (powerRZ radix (- precision)). 2: ring_simplify. 2: replace 1%R with (powerRZ radix 0); [ auto with real zarith | simpl in |- *; auto ]. 2: apply Rlt_powerRZ; auto with zarith. 2: now apply IZR_lt. cut (0 < 1 + powerRZ radix (- precision))%R; [ intros H'2 | idtac ]. 2: apply Rlt_le_trans with 1%R; auto with real. 2: apply Rle_trans with (1 + 0)%R; auto with real zarith. 2: apply Rplus_le_compat_l. 2: now apply powerRZ_le, IZR_lt. cut (0 < powerRZ radix precision - 1)%R; [ intros H'3 | idtac ]. 2: apply Rplus_lt_reg_r with 1%R. 2: ring_simplify. 2: replace 1%R with (powerRZ radix 0); [ auto with real zarith | simpl in |- *; auto ]. 2: apply Rlt_powerRZ; auto with zarith; now apply IZR_lt. cut (0 < 1 - powerRZ radix (Z.succ (- precision)))%R; [ intros H'4 | idtac ]. 2: apply Rplus_lt_reg_r with (powerRZ radix (Z.succ (- precision))). 2: ring_simplify. 2: replace 1%R with (powerRZ radix 0); [ auto with real zarith | simpl in |- *; auto ]. 2: apply Rlt_powerRZ; auto with zarith; now apply IZR_lt. rewrite (Rinv_mult_distr (4 * (powerRZ radix precision - 1) * (1 + powerRZ radix (- precision))) (1 - powerRZ radix (- precision))) ; auto with real. 2: apply Rmult_integral_contrapositive; split; auto with real. apply Rle_trans with (/ (4 * (powerRZ radix precision - 1) * (1 + powerRZ radix (- precision))) * (1 - powerRZ radix (Z.succ (- precision))) * (Rabs y - (Rabs (FtoRradix a * FtoRradix x) * / (1 - powerRZ radix (- precision)) + powerRZ radix (Z.pred (- dExp b)) * / (1 - powerRZ radix (- precision)))) + - (powerRZ radix (Z.pred (- dExp b)) * / (2 * (powerRZ radix precision - 1))))%R; [ right; ring; ring | idtac ]. apply Rle_trans with (/ (4 * (powerRZ radix precision - 1) * (1 + powerRZ radix (- precision))) * (1 - powerRZ radix (Z.succ (- precision))) * (Rabs (FtoRradix y) - Rabs t) + - (powerRZ radix (Z.pred (- dExp b)) * / (2 * (powerRZ radix precision - 1))))%R; [ apply Rplus_le_compat_r | idtac ]. apply Rmult_le_compat_l. apply Rlt_le; apply Rmult_lt_0_compat; auto with real. apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; auto with real; apply Rmult_lt_0_compat; auto with real. unfold Rminus in |- *; apply Rplus_le_compat_l; apply Ropp_le_contravar. apply Rle_trans with (Rabs (FtoRradix a * FtoRradix x) * / (1 - powerRZ 2%Z (- precision)) + powerRZ 2%Z (Z.pred (- dExp b)) * / (1 - powerRZ 2%Z (- precision)))%R; [ idtac | right; unfold FtoRradix, radix, Rminus in |- *; auto with real ]. apply RoundLeGeneral; auto with zarith. rewrite (Rinv_mult_distr (4 * (powerRZ radix precision - 1)) (1 + powerRZ radix (- precision))); auto with real. apply Rle_trans with (/ (4 * (powerRZ radix precision - 1)) * (1 - powerRZ radix (Z.succ (- precision))) * (/ (1 + powerRZ radix (- precision)) * (Rabs (FtoRradix y) - Rabs (FtoRradix t))) + - (powerRZ radix (Z.pred (- dExp b)) * / (2 * (powerRZ radix precision - 1))))%R; [ right; ring | idtac ]. apply Rle_trans with (/ (4 * (powerRZ radix precision - 1)) * (1 - powerRZ radix (Z.succ (- precision))) * Rabs u + - (powerRZ radix (Z.pred (- dExp b)) * / (2 * (powerRZ radix precision - 1))))%R. apply Rplus_le_compat_r; apply Rmult_le_compat_l. apply Rlt_le; apply Rmult_lt_0_compat; auto with real. apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; auto with real. apply Rle_trans with (/ (1 + powerRZ radix (- precision)) * Rabs (FtoRradix y + FtoRradix t))%R. apply Rmult_le_compat_l; auto with real. rewrite <- (Rabs_Ropp (FtoRradix t)). replace (FtoRradix y + FtoRradix t)%R with (FtoRradix y - - FtoRradix t)%R; [ apply Rabs_triang_inv | ring ]. case Cu; intros H1. apply Rmult_le_reg_l with (1 + powerRZ radix (- precision))%R; auto. apply Rle_trans with (Rabs (FtoRradix y + FtoRradix t) * ((1 + powerRZ radix (- precision)) * / (1 + powerRZ radix (- precision))))%R; [ right; ring; ring | idtac ]. rewrite Rinv_r; auto with real. ring_simplify. apply Rle_trans with (Rabs u + / radix * Fulp b radix precision u)%R. apply Rplus_le_reg_l with (- Rabs u)%R. ring_simplify. apply Rle_trans with (Rabs (FtoRradix y + FtoRradix t - FtoRradix u)). apply Rle_trans with (Rabs (FtoRradix y + FtoRradix t) - Rabs (FtoRradix u))%R; [ right; ring | apply Rabs_triang_inv ]. apply Rmult_le_reg_l with (IZR radix); auto with real zarith. apply Rle_trans with (Fulp b radix precision u * (radix * / radix))%R; [ rewrite Rinv_r; auto with real zarith | right; ring ]. ring_simplify (Fulp b radix precision u * 1)%R. unfold FtoRradix in |- *; apply ClosestUlp; auto with real zarith. rewrite Rplus_comm; auto. rewrite Rplus_comm; apply Rplus_le_compat_r. apply Rmult_le_reg_l with (IZR radix); auto with real zarith. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real zarith. ring_simplify (1 * Fulp b radix precision u)%R. apply Rle_trans with (Rabs (FtoRradix u) * powerRZ radix (Z.succ (- precision)))%R. unfold FtoRradix in |- *; apply FulpLe2; auto with zarith. replace (Fnormalize radix b precision u) with u; [ idtac | apply FcanonicUnique with (radix := radix) (precision := precision) (b := b) ]; auto with zarith real. apply FnormalizeCanonic; auto with zarith. apply sym_eq; apply FnormalizeCorrect; auto with zarith. unfold Z.succ in |- *; rewrite powerRZ_add; auto with zarith real; simpl in |- *; auto with zarith real; right; ring. replace (FtoRradix y + FtoRradix t)%R with (FtoRradix u); auto with real. apply Rle_trans with (1 * Rabs (FtoRradix u))%R; [ apply Rmult_le_compat_r | right; ring ]; auto with real. apply Rabs_pos. pattern 1%R at 2 in |- *; replace 1%R with (/ 1)%R; auto with real zarith. apply Rle_Rinv; auto with real zarith. pattern 1%R at 1 in |- *; replace 1%R with (1 + 0)%R; auto with real zarith. apply Rplus_le_compat_l. now apply powerRZ_le, IZR_lt. unfold FtoRradix in |- *; apply plusExact1 with b precision; auto with real zarith. rewrite Rplus_comm; auto. elim H1; intros H5 H6; elim H6; intros H7 H8; rewrite H7; apply Zmin_Zle; elim Fy; elim Ft; auto with zarith. apply Rle_trans with (/ (4 * (powerRZ radix precision - 1)) * (Rabs (FtoRradix u) - (Rabs u * powerRZ radix (Z.succ (- precision)) + powerRZ radix (- dExp b))))%R. right; simpl; ring_simplify. unfold Z.pred, Z.succ; rewrite 2!powerRZ_add; auto with zarith real. unfold radix; simpl; field; auto with real. apply Rle_trans with (/ (4 * (powerRZ radix precision - 1)) * (Rabs (FtoRradix u) - Fulp b radix precision u))%R. apply Rmult_le_compat_l; auto with real. apply Rlt_le; apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; auto with real. unfold Rminus in |- *; apply Rplus_le_compat_l; apply Ropp_le_contravar. apply FulpLeGeneral; auto. apply Rle_trans with (/ (4 * (powerRZ radix precision - 1)) * Rabs (FLess u))%R. apply Rmult_le_compat_l; auto with real. apply Rlt_le; apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; auto with real. apply UlpFlessuGe_aux; auto. rewrite Rinv_mult_distr; auto with real. rewrite Rmult_assoc; apply Rmult_le_compat_l; auto with real. apply Rmult_le_reg_l with (powerRZ radix precision - 1)%R; auto. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real. rewrite Rmult_1_l; unfold FtoRradix in |- *; apply FulpGe; auto with zarith. unfold FLess in |- *; case (Rcase_abs u); intros H. apply FBoundedSuc; auto with zarith. apply FBoundedPred; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz