proposition: Theorem discri14: (delta <= 2*(Fulp bo radix precision d))%R.
proof: Proof. case (Rle_or_lt (p+q)%R (3*(Rabs (p-q)))%R); case (Rle_or_lt v u); intros. unfold delta, FtoRradix. apply discri9 with p q t dp dq s; auto; fold radix; fold FtoRradix; intros; absurd (p + q <= 3 * Rabs (p - q))%R; auto with real. unfold delta, FtoRradix. apply discri13 with p q t dp dq s u v; auto. apply Rle_trans with (Rsqr (FtoR 2 b)); auto with real. unfold delta, FtoRradix. apply discri11 with p q t u v dp dq; auto with zarith. left; auto. assert (exists s : float, Fbounded bo s /\ FtoR 2 s = (FtoR 2 b * FtoR 2 b - FtoR 2 p)%R /\ Fexp s = (Fexp p - precision)%Z /\ (Rabs (Fnum s) <= powerRZ (Zpos 2) (Z.pred precision))%R). apply errorBoundedMultClosest_Can; auto. elim Roundp; auto. left; auto. elim H1; intros s' T; elim T; intros T1 T2; elim T2; intros T3 T4; elim T4; intros. apply Z.le_trans with (Fexp s')%Z; auto with zarith. apply T. assert (exists s : float, Fbounded bo s /\ FtoR 2 s = (FtoR 2 a * FtoR 2 c - FtoR 2 q)%R /\ Fexp s = (Fexp q - precision)%Z /\ (Rabs (Fnum s) <= powerRZ (Zpos 2) (Z.pred precision))%R). apply errorBoundedMultClosest_Can; auto. elim Roundq; auto. left; auto. elim H1; intros s' T; elim T; intros T1 T2; elim T2; intros T3 T4; elim T4; intros. apply Z.le_trans with (Fexp s')%Z; auto with zarith. apply T. fold FtoRradix; apply Rle_trans with (Rsqr b); auto with real. apply FcanonicUnique with radix bo precision; auto with zarith. left; auto. left; auto. generalize EvenClosestUniqueP; unfold UniqueP; intros Y. apply Y with bo precision (p-q)%R; auto with real zarith. unfold delta, FtoRradix. apply discri9 with p q t dp dq s; auto. fold radix; fold FtoRradix; intros. absurd (p + q <= 3 * Rabs (p - q))%R; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz