proposition: Theorem discri3: (exists f:float, (Fbounded bo f) /\ (FtoRradix f)=(dp-dq)%R) -> (delta <= 2*(Fulp bo radix precision d))%R.
proof: Proof. intros T; elim T; intros f T1; elim T1; intros H1 H2; clear T T1. unfold delta. replace (d - (b * b' - a * c))%R with (-((t+s)-d))%R. apply Rmult_le_reg_l with 2%R; auto with arith real. apply Rle_trans with (Fulp bo radix precision d). rewrite Rabs_Ropp; unfold FtoRradix; apply ClosestUlp; auto. elim Roundd; auto. simpl; apply Rle_trans with (1*(1*(Fulp bo radix precision d)))%R; unfold Fulp; auto with real zarith. right; ring. apply Rmult_le_compat; auto with real zarith. ring_simplify (1 * powerRZ radix (Fexp (Fnormalize radix bo precision d)))%R; auto with real zarith. apply powerRZ_le, IZR_lt; auto with zarith. apply Rmult_le_compat_r; auto with real. apply powerRZ_le, IZR_lt; auto with zarith. replace (FtoRradix s) with (dp-dq)%R. rewrite dpEq; rewrite dqEq; rewrite t_exact; ring. rewrite <- H2. unfold FtoRradix; apply RoundedModeProjectorIdemEq with (b:=bo) (P:=(EvenClosest bo radix precision)) (precision:=precision); auto with real. apply EvenClosestRoundedModeP; auto. fold FtoRradix; rewrite H2; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz