proposition: Theorem discri6: (0< dp)%R -> (dq < 0)%R -> (delta <= 2*(Fulp bo radix precision d))%R.
proof: Proof. intros;unfold delta. replace (d - (b * b' - a * c))%R with (-((t+s)-d)+-((dp-dq)-s))%R. 2: rewrite dpEq; rewrite dqEq; unfold FtoRradix, radix; rewrite t_exact with bo precision b b' p q t; auto; ring. apply Rle_trans with (1:=Rabs_triang (-(t+s-d))%R (-(dp-dq-s))%R). apply Rmult_le_reg_l with 2%R; auto with real zarith;rewrite Rmult_plus_distr_l. apply Rle_trans with ((Fulp bo radix precision d)+(Fulp bo radix precision s))%R;[apply Rplus_le_compat|idtac]. rewrite Rabs_Ropp; unfold FtoRradix; apply ClosestUlp; auto. elim Roundd; auto. rewrite Rabs_Ropp; unfold FtoRradix; apply ClosestUlp; auto. elim Rounds; auto. apply Rle_trans with ((Fulp bo radix precision d+ 3* Fulp bo radix precision d))%R;[apply Rplus_le_compat_l|simpl;right;ring]. apply Rle_trans with (2*Fulp bo radix precision d)%R;[idtac|unfold Fulp; auto with real zarith]. rewrite FulpFabs; auto; rewrite FulpFabs with bo radix precision d; auto. assert (2*(Fabs d)=(Float (Fnum (Fabs d)) (Z.succ (Fexp (Fabs d)))))%R. unfold FtoRradix, FtoR, Z.succ; simpl; rewrite powerRZ_add; auto with real zarith. rewrite powerRZ_1; unfold radix; ring. apply Rle_trans with (Fulp bo radix precision (Float (Fnum (Fabs d)) (Z.succ (Fexp (Fabs d))))). 2:assert (Fnormal radix bo (Fabs d));[apply FnormalFabs; auto|idtac]. 2:right; rewrite CanonicFulp; auto; [rewrite CanonicFulp|left]; auto. 2:unfold FtoR, Z.succ; simpl; rewrite powerRZ_add; auto with real zarith. 2:rewrite powerRZ_1; unfold radix; ring. 2:left; auto. 2:elim H2; intros H6 H5; elim H6; intros. 2:split; simpl; auto with zarith. 2:split; simpl; auto with zarith. apply LeFulpPos; auto with real. apply absFBounded; auto. assert (Fnormal radix bo (Fabs d));[apply FnormalFabs; auto|idtac]. elim H2; intros H6 H5; elim H6; intros;split; simpl; auto with zarith. rewrite Fabs_correct; auto with real zarith; apply Rabs_pos. 2: apply Rmult_le_compat_r; auto with real. 2: apply powerRZ_le, IZR_lt; auto with zarith. apply EvenClosestMonotone2 with bo precision (Rabs (dp-dq))%R (2*Rabs (t+s))%R; auto. 2: apply EvenClosestFabs; auto; left; auto. 2: apply Twice_EvenClosest_Round; auto. 2: apply FnormalFabs; auto. 2: apply EvenClosestFabs; auto; left; auto. unfold Rminus; apply Rle_trans with (1:=Rabs_triang dp (-dq)%R). apply Rmult_le_reg_l with 2%R; auto with real zarith; rewrite Rmult_plus_distr_l. apply Rle_trans with (Fulp bo radix precision p+Fulp bo radix precision q)%R;[apply Rplus_le_compat|idtac]. rewrite dpEq; unfold FtoRradix; apply ClosestUlp; auto. elim Roundp; auto. rewrite Rabs_Ropp; rewrite dqEq; unfold FtoRradix; apply ClosestUlp; auto. elim Roundq; auto. rewrite CanonicFulp; auto;[idtac|left; auto]. rewrite CanonicFulp; auto;[idtac|left; auto]. apply Rle_trans with (3*(powerRZ radix e))%R;[right|idtac]. unfold FtoRradix, FtoR; simpl; rewrite q_eqExp; rewrite p_eqF; simpl. unfold Z.succ; rewrite powerRZ_add; auto with real zarith. rewrite powerRZ_1; unfold radix ;ring. assert ((powerRZ radix e <= t))%R. unfold FtoRradix, radix; rewrite t_exact with bo precision b b' p q t; auto. fold radix; fold FtoRradix; rewrite p_eqR. apply Rle_trans with (powerRZ radix (precision + e) - ((powerRZ radix precision - 1) * powerRZ radix e))%R; auto with real. rewrite powerRZ_add; auto with real zarith; right;ring. unfold Rminus; apply Rplus_le_compat_l; auto with real. apply Ropp_le_contravar. unfold FtoRradix, FtoR; rewrite q_eqExp; apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; auto with zarith. apply Rle_trans with (1:=(RRle_abs (Fnum q))). assert (Z.abs (Fnum q) < Zpower_nat radix precision)%Z; auto with real zarith. rewrite <- pGivesBound; auto with zarith; apply Nq. rewrite Rabs_Zabs; apply Rle_trans with (Z.pred (Zpower_nat radix precision)); auto with real zarith. apply IZR_le; auto with zarith. unfold Z.pred; rewrite plus_IZR. rewrite Zpower_nat_Z_powerRZ; right; simpl; ring. assert (0<=s)%R. unfold FtoRradix; apply RleRoundedR0 with bo precision (EvenClosest bo radix precision) (dp-dq)%R; auto with real. apply EvenClosestRoundedModeP; auto. apply Rle_trans with (0-0)%R; unfold Rminus; auto with real. apply Rplus_le_compat; auto with real. rewrite Rabs_right; auto with real. 2: apply Rle_ge; apply Rle_trans with (0+0)%R; auto with real. 2: apply Rplus_le_compat; auto with real zarith. 2: apply Rle_trans with (2:=H2); auto with real zarith. 2: apply powerRZ_le, IZR_lt; auto with zarith. apply Rle_trans with (4*powerRZ radix e)%R;[apply Rmult_le_compat_r; auto with real zarith|idtac]. apply powerRZ_le, IZR_lt; auto with zarith. apply Rle_trans with (4*(t+s))%R;[apply Rmult_le_compat_l; auto with real|simpl; right; ring]. apply Rle_trans with (powerRZ radix e+0)%R;[idtac|apply Rplus_le_compat];auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz