proposition: Theorem errorBoundedMult : forall P, RoundedModeP b radix P -> forall p q f : float, Fbounded b p -> Fbounded b q -> (- dExp b <= Fexp p + Fexp q)%Z -> P (p * q)%R f -> exists r : float, r = (p * q - f)%R :>R /\ Fbounded b r /\ Fexp r = (Fexp p + Fexp q)%Z.
proof: Proof. intros P H p q f H0 H1 H2 H3. case (Rle_or_lt 0 p); intros H4; case (Rle_or_lt 0 q); intros H5. apply errorBoundedMultPos with P; auto. replace (Fexp p) with (Fexp (Fopp p)); auto with zarith. replace (Fexp q) with (Fexp (Fopp q)); auto with zarith. cut ((p * q)%R = (Fopp p * Fopp q)%R); [ intros H6; rewrite H6 | idtac ]. apply errorBoundedMultNeg with P; auto with real; try apply oppBounded; auto. unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real. unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real. rewrite <- H6; auto. unfold FtoRradix in |- *; repeat rewrite Fopp_correct; ring. apply errorBoundedMultNeg with P; auto with real. replace (Fexp p) with (Fexp (Fopp p)); auto. replace (Fexp q) with (Fexp (Fopp q)); auto. cut ((p * q)%R = (Fopp p * Fopp q)%R); [ intros H6; rewrite H6 | idtac ]. apply errorBoundedMultPos with P; try apply oppBounded; auto with real. unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real. unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real. rewrite <- H6; auto. unfold FtoRradix in |- *; repeat rewrite Fopp_correct; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz