proposition: Theorem UlpFlessuGe2 : Fcanonic radix b u -> (powerRZ radix (Z.pred (Z.pred (- precision))) * (1 - powerRZ radix (Z.succ (- precision))) * Rabs y + - (powerRZ radix (Z.pred (Z.pred (- precision))) * Rabs (a * x)) + - powerRZ radix (Z.pred (Z.pred (- dExp b))) < / 4 * Fulp b radix precision (FLess u))%R.
proof: Proof. intros H. apply Rlt_le_trans with (/ (4 * (powerRZ radix precision - 1) * (1 + powerRZ radix (- precision))) * ((1 - powerRZ radix (Z.succ (- precision))) * Rabs (FtoRradix y)) + - (/ (4 * (powerRZ radix precision - 1) * (1 + powerRZ radix (- precision)) * (1 - powerRZ radix (- precision))) * ((1 - powerRZ radix (Z.succ (- precision))) * Rabs (FtoRradix a * FtoRradix 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))))))%R; [ idtac | apply UlpFlessuGe; auto ]. 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; 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. apply Rle_lt_trans with (/ (4 * (powerRZ radix precision - 1) * (1 + powerRZ radix (- precision))) * ((1 - powerRZ radix (Z.succ (- precision))) * Rabs (FtoRradix y)) + - (/ (4 * (powerRZ radix precision - 1) * (1 + powerRZ radix (- precision)) * (1 - powerRZ radix (- precision))) * ((1 - powerRZ radix (Z.succ (- precision))) * Rabs (FtoRradix a * FtoRradix x))) + - powerRZ radix (Z.pred (Z.pred (- dExp b))))%R; [ apply Rplus_le_compat_r | apply Rplus_lt_compat_l ]. apply Rplus_le_compat. repeat rewrite <- Rmult_assoc. apply Rmult_le_compat_r; auto with real. apply Rabs_pos. rewrite Rmult_assoc. ring_simplify ((powerRZ radix precision - 1) * (1 + powerRZ radix (- precision)))%R. rewrite <- powerRZ_add; auto with real zarith. replace (powerRZ radix (- precision + precision)) with 1%R; [ idtac | ring_simplify (- precision + precision)%Z; simpl in |- *; auto with real zarith ]. ring_simplify (-1 + (- powerRZ radix (- precision) + (powerRZ radix precision + 1)))%R. apply Rmult_le_compat_r; auto with real. apply Rle_trans with (/ (4 * powerRZ radix precision))%R; [ right | idtac ]. unfold Z.pred in |- *. replace (- precision + -1 + -1)%Z with (- 2 + - precision)%Z; [ rewrite powerRZ_add | ring ]; auto with zarith real. rewrite Rinv_mult_distr; auto with real zarith. replace (powerRZ radix (- 2)) with (/ 4)%R. replace (/ powerRZ radix precision)%R with (powerRZ radix (- precision)); auto with real. apply powerRZ_Zopp; auto with zarith real. simpl; unfold radix. field. now apply Rgt_not_eq, powerRZ_lt, IZR_lt. apply Rle_Rinv; auto with real. apply Rlt_le_trans with (4 * (powerRZ radix precision - 1 + (1 - powerRZ radix (- precision))))%R. apply Rle_lt_trans with (4 * (0 + 0))%R; [ right; ring | auto with real ]. ring_simplify (precision+-precision)%Z; simpl; right;ring. apply Rmult_le_compat_l; auto with real zarith. ring_simplify (precision+-precision)%Z. apply Rle_trans with (powerRZ radix precision + - powerRZ radix (- precision))%R; [ right; simpl; ring | idtac ]; auto with real zarith. apply Rle_trans with (powerRZ radix precision + -0)%R; [ idtac | right; ring ]; auto with real zarith. apply Rplus_le_compat_l, Ropp_le_contravar. apply powerRZ_le; auto with zarith; now apply IZR_lt. apply Ropp_le_contravar. repeat rewrite <- Rmult_assoc. apply Rmult_le_compat_r; auto with real. apply Rabs_pos. unfold Z.pred in |- *. replace (- precision + -1 + -1)%Z with (- 2 + - precision)%Z; [ rewrite powerRZ_add | ring ]; auto with zarith real. repeat rewrite Rmult_assoc; rewrite Rinv_mult_distr. 2: auto with real. 2: apply Rmult_integral_contrapositive; split; auto with real. replace (powerRZ radix (- 2)) with (/ 4)%R. 2: simpl; unfold radix; field. 2: replace (powerRZ radix 2) with 4%R; [ auto with zarith real | unfold radix; simpl in |- *; ring ]. repeat rewrite Rmult_assoc; apply Rmult_le_compat_l; auto with real. apply Rmult_le_reg_l with ((powerRZ radix precision - 1) * ((1 + powerRZ radix (- precision)) * (1 - powerRZ radix (- precision))))%R; auto with real. apply Rmult_lt_0_compat; auto with real. apply Rmult_lt_0_compat; auto with real. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real. 2: apply Rmult_integral_contrapositive; split; auto with real. unfold Rminus; repeat rewrite Rmult_plus_distr_r. rewrite Ropp_mult_distr_l_reverse. repeat rewrite Rmult_1_l. repeat rewrite Rmult_plus_distr_l. repeat rewrite Rmult_1_r. repeat rewrite <- Ropp_mult_distr_r. rewrite <- Ropp_mult_distr_l. repeat rewrite <- powerRZ_add; auto with real zarith. replace (powerRZ radix (precision + - precision)) with 1%R; [ idtac | ring_simplify ( precision +- precision)%Z; simpl in |- *; auto ]. apply Rle_trans with (1 + (- powerRZ radix (- precision) + (- powerRZ radix (- precision) + 0)))%R; [ right | idtac ]. unfold Z.succ; rewrite powerRZ_add; auto with real zarith; simpl; unfold radix; ring. apply Rle_trans with (1 + (- powerRZ radix (- precision) + (- powerRZ radix (-2 * precision) + powerRZ radix (-3 * precision))))%R; [ idtac | right]. apply Rplus_le_compat_l; apply Rplus_le_compat_l. apply Rplus_le_compat; auto with real zarith. apply Ropp_le_contravar, Rle_powerRZ; auto with zarith; left; now apply IZR_lt. now apply powerRZ_le, IZR_lt. apply trans_eq with (powerRZ radix (- precision) * powerRZ radix precision +( - powerRZ radix (- precision) * powerRZ radix (precision + (- precision + - precision)) + powerRZ radix (- precision) * powerRZ radix (- precision + - precision) - powerRZ radix (- precision)))%R;[idtac|ring]. repeat rewrite <- powerRZ_add; auto with real zarith. f_equal. ring_simplify (-precision+precision)%Z; easy. rewrite <- Ropp_mult_distr_l. rewrite <- powerRZ_add; auto with real zarith. replace (- precision + (precision + (- precision + - precision)))%Z with (-2*precision)%Z by ring. replace (- precision + (- precision + - precision))%Z with (-3*precision)%Z by ring. ring. apply Ropp_lt_contravar. apply Rmult_lt_reg_l with (powerRZ radix (2 + dExp b)); auto with real zarith. now apply powerRZ_lt, IZR_lt. rewrite <- Rmult_assoc; unfold Z.pred in |- *. repeat rewrite <- powerRZ_add; auto with real zarith. replace (2 + dExp b + (- dExp b + -1 + -1))%Z with 0%Z by ring. replace (2 + dExp b + (- dExp b + -1))%Z with 1%Z by ring. replace (powerRZ radix 0) with 1%R; [ idtac | simpl in |- *; auto with real zarith ]. replace (powerRZ radix 1) with 2%R; [ idtac | unfold radix; simpl in |- *; ring; auto with real zarith ]. rewrite Rmult_plus_distr_l. apply Rlt_le_trans with (/ 3 + 2 * / 3)%R. 2: simpl; right;field; auto with real. apply Rle_lt_trans with (/ 3 + 2 * (/ (4 * (powerRZ radix precision - 1) * (1 + powerRZ radix (- precision)) * (1 - powerRZ radix (- precision))) * (1 - powerRZ radix (- precision + 1))))%R; [ apply Rplus_le_compat_r | apply Rplus_lt_compat_l ]. rewrite Rinv_mult_distr; auto with arith real. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with arith real. rewrite Rmult_1_l; replace 3%R with (powerRZ radix 2 - 1)%R; auto with real zarith arith. apply Rle_Rinv; auto with real arith. replace 0%R with (powerRZ radix 0 - 1)%R; [ unfold Rminus in |- *; auto with real arith zarith | simpl in |- *; ring ]. apply Rplus_lt_compat_r. apply Rlt_powerRZ; auto with zarith; now apply IZR_lt. unfold Rminus in |- *; apply Rplus_le_compat_r; apply Rle_powerRZ; try lia. auto with real arith zarith. unfold radix; simpl in |- *; ring; auto with arith zarith real. apply Rmult_lt_compat_l; auto with real arith. repeat rewrite Rinv_mult_distr; auto with real. 2: apply Rmult_integral_contrapositive; split; auto with real. apply Rle_lt_trans with (/ 4 * / (powerRZ radix 2 - 1) * / (1 + 0) * / (1 - powerRZ radix (- 2)) * (1 - 0))%R. repeat rewrite Rmult_assoc. apply Rmult_le_compat_l; auto with real arith. apply Rmult_le_compat; auto with real arith zarith. apply Rmult_le_pos; auto with real. apply Rmult_le_pos; auto with real. apply Rle_Rinv; auto with real arith zarith. apply Rle_lt_trans with (powerRZ radix 0 - 1)%R; [ right; simpl in |- *; ring | auto with real arith zarith ]. unfold Rminus in |- *; apply Rplus_lt_compat_r; auto with real arith zarith. apply Rlt_powerRZ; auto with zarith; try (simpl; lia); now apply IZR_lt. unfold Rminus in |- *; apply Rplus_le_compat_r; apply Rle_powerRZ; try lia. auto with real arith zarith. apply Rmult_le_compat; auto with real arith zarith. apply Rmult_le_pos; auto with real. apply Rle_Rinv. ring_simplify; auto with real. apply Rplus_le_compat_l. now apply powerRZ_le, IZR_lt. apply Rmult_le_compat; auto with real arith zarith. apply Rle_Rinv; auto with real arith zarith. apply Rle_lt_trans with (1 - powerRZ radix 0)%R; [ simpl in |- *; right; ring | auto with real arith zarith ]. unfold Rminus in |- *; apply Rplus_lt_compat_l; apply Ropp_lt_contravar; auto with real arith zarith. apply Rlt_powerRZ; simpl; auto with zarith. now apply IZR_lt. unfold Rminus in |- *; apply Rplus_le_compat_l; apply Ropp_le_contravar; apply Rle_powerRZ; try lia. auto with real arith zarith. unfold Rminus in |- *; apply Rplus_le_compat_l; apply Ropp_le_contravar; auto with real arith zarith. now apply powerRZ_le, IZR_lt. ring_simplify (1 - 0)%R; rewrite Rmult_1_r. ring_simplify (1 + 0)%R; rewrite Rinv_1; rewrite Rmult_1_r. change (-2)%Z with (-(2))%Z. rewrite powerRZ_Zopp; auto with real arith zarith. replace (powerRZ radix 2) with 4%R; [ idtac | simpl in |- *; unfold radix; ring; auto with arith real zarith ]. lra. Qed.
imports: Reals ZArith List PeanoNat Psatz