proposition: Theorem discri1: (delta <= 2*(Fulp bo radix precision d))%R.
proof: Proof. apply Rle_trans with (1:=delta_inf). case (Rle_or_lt q p); intros H1. case (Rle_or_lt 0%R q); intros H2. cut (2*(Fulp bo radix precision q)<=(Fulp bo radix precision p))%R; try intros H3. cut ((Fulp bo radix precision p)<=2*(Fulp bo radix precision d))%R; try intros H4. apply Rle_trans with ((/ 2 * Fulp bo radix precision d + (/ 2 * (2*Fulp bo radix precision d) + / 2 * Fulp bo radix precision d)))%R. apply Rplus_le_compat; auto with real. apply Rplus_le_compat; auto with real. apply Rmult_le_compat_l; auto with real. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (1:=H3); auto with real. right; field; auto with real. apply Fulp_le_twice_r_round with (p-q)%R; auto. apply P_positive. apply Rplus_le_reg_l with (2*q-p)%R. ring_simplify. apply Rmult_le_reg_l with 2%R; auto with real. apply Rplus_le_reg_l with (p-3*q)%R. ring_simplify. apply Rle_trans with (1:=Firstcase); rewrite Rabs_right. right; ring. apply Rle_ge; apply Rplus_le_reg_l with q; ring_simplify; auto with real. apply Fulp_le_twice_l; auto. apply Rmult_le_reg_l with 2%R; auto with real. apply Rplus_le_reg_l with (p-3*q)%R. ring_simplify. apply Rle_trans with (1:=Firstcase); rewrite Rabs_right. right; ring. apply Rle_ge; apply Rplus_le_reg_l with q; ring_simplify; auto with real. apply Rle_trans with ((/ 2 * Fulp bo radix precision d + (/ 2 * (Fulp bo radix precision d) + / 2 * Fulp bo radix precision d)))%R. apply Rplus_le_compat; auto with real. apply Rplus_le_compat; auto with real. apply Rmult_le_compat; auto with real. unfold Fulp; auto with real zarith. apply powerRZ_le, IZR_lt; auto with zarith. apply LeFulpPos; auto with real. fold FtoRradix; apply P_positive. fold FtoRradix; apply EvenClosestMonotone2 with p (p-q)%R; auto. apply Rle_trans with (p-0)%R; unfold Rminus; auto with real; right;ring. unfold FtoRradix; apply RoundedModeProjectorIdem with (b:=bo) (P:=(EvenClosest bo radix precision)); auto. apply EvenClosestRoundedModeP; auto. apply Rmult_le_compat; auto with real. unfold Fulp; auto with real zarith. apply powerRZ_le, IZR_lt; auto with zarith. rewrite FulpFabs; auto. apply LeFulpPos; auto with real. apply absFBounded; easy. rewrite Fabs_correct; auto with real; apply Rabs_pos. fold FtoRradix; apply EvenClosestMonotone2 with (-q)%R (p-q)%R; auto. generalize P_positive; intros; auto with real. apply Rle_trans with (0-q)%R; unfold Rminus; auto with real; right;ring. replace (-q)%R with (FtoRradix (Fabs q)). unfold FtoRradix; apply RoundedModeProjectorIdem with (b:=bo) (P:=(EvenClosest bo radix precision)); auto. apply EvenClosestRoundedModeP; auto. apply absFBounded; easy. unfold FtoRradix;rewrite Fabs_correct; auto with real; rewrite Rabs_left; auto with real. apply Rle_trans with ((3*/2)*(Fulp bo radix precision d))%R. right; field; auto with real. apply Rmult_le_compat_r;auto with zarith real. unfold Fulp; auto with zarith real. apply powerRZ_le, IZR_lt; auto with zarith. apply Rmult_le_reg_l with 2%R;auto with real. apply Rle_trans with 3%R; auto with real. right; field; auto with real. rewrite <- mult_IZR; auto with real zarith. cut (2*(Fulp bo radix precision p)<=(Fulp bo radix precision q))%R; try intros H3. cut ((Fulp bo radix precision q)<=2*(Fulp bo radix precision d))%R; try intros H4. apply Rle_trans with ((/ 2 * Fulp bo radix precision d + (/ 2 * (Fulp bo radix precision d) + / 2 * (2*Fulp bo radix precision d))))%R. apply Rplus_le_compat; auto with real. apply Rplus_le_compat; auto with real. apply Rmult_le_compat_l; auto with real. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (1:=H3); auto with real. right; field; auto with real. assert (p-q <=0)%R. apply Rplus_le_reg_l with q. ring_simplify; auto with real. rewrite FulpFabs with bo radix precision d; auto. apply Fulp_le_twice_r_round with (Rabs (p-q))%R; auto. apply Rle_trans with p; auto with real; apply P_positive. apply FnormalFabs; auto. rewrite Rabs_left; auto with real. apply Rmult_le_reg_l with 2%R; auto with real. apply Rplus_le_reg_l with (p-q)%R. ring_simplify. apply Rle_trans with (1:=Firstcase); rewrite Rabs_left1; auto. right; ring. generalize EvenClosestSymmetric; unfold SymmetricP; intros. rewrite Rabs_left1; auto with real. replace (Fabs d) with (Fopp d). apply H0; auto. unfold Fabs, Fopp; replace (Z.abs (Fnum d)) with (-(Fnum d))%Z; auto. rewrite <- Zabs_Zopp; rewrite Z.abs_eq; auto with zarith. cut (Fnum d <= 0)%Z; auto with zarith. apply R0LeFnum with radix; auto. apply RleRoundedLessR0 with bo precision (EvenClosest bo radix precision) (p-q)%R; auto with real zarith. apply EvenClosestRoundedModeP; auto. apply Fulp_le_twice_l; auto. apply P_positive. apply Rmult_le_reg_l with 2%R; auto with real. apply Rplus_le_reg_l with (-3*p+q)%R. ring_simplify. apply Rle_trans with (1:=Firstcase); rewrite Rabs_left1; auto. right; ring. apply Rplus_le_reg_l with q. ring_simplify; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz