proposition: Theorem errorBoundedMultNeg : forall P, RoundedModeP b radix P -> forall p q f : float, Fbounded b p -> Fbounded b q -> (p <= 0)%R -> (0 <= q)%R -> (- 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 H4 H5. generalize errorBoundedMultMin errorBoundedMultMax; intros H6 H7. cut (MinOrMaxP b radix P); [ intros | case H; intros H'1 (H'2, (H'3, H'4)); auto ]. case (H8 (p * q)%R f); auto; intros H9. generalize (H7 (Fopp p) q (Fopp f)); intros H12. lapply H12; auto. 2: now apply oppBounded. intros H10; clear H12. lapply H10; auto; intros H12; clear H10. lapply H12; [ intros H10 | unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real ]; clear H12. lapply H10; auto; intros H12; clear H10. lapply H12; [ intros H10 | simpl in |- *; auto ]; clear H12. lapply H10; [ intros H12 | idtac ]; clear H10. 2: replace (Fopp p * q)%R with (- (p * q))%R; [ apply MinOppMax; auto | idtac ]. 2: unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real. elim H12; intros r H10; clear H12; elim H10; intros H11 H12; clear H10. elim H12; clear H12; intros H10 H12. exists (Fopp r); split; [ generalize H11 | split; auto with zarith ]. 2: now apply oppBounded. unfold FtoRradix in |- *; repeat rewrite Fopp_correct; intros H13; rewrite H13; ring. generalize (H6 (Fopp p) q (Fopp f)); intros H12. lapply H12; auto. 2: now apply oppBounded. intros H10; clear H12. lapply H10; auto; intros H12; clear H10. lapply H12; [ intros H10 | unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real ]; clear H12. lapply H10; auto; intros H12; clear H10. lapply H12; [ intros H10 | simpl in |- *; auto ]; clear H12. lapply H10; [ intros H12 | idtac ]; clear H10. 2: replace (Fopp p * q)%R with (- (p * q))%R; [ apply MaxOppMin; auto | idtac ]. 2: unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real. elim H12; intros r H10; clear H12; elim H10; intros H11 H12; clear H10. elim H12; clear H12; intros H10 H12. exists (Fopp r); split; [ generalize H11 | split; auto with zarith ]. unfold FtoRradix in |- *; repeat rewrite Fopp_correct; intros H13; rewrite H13; ring. now apply oppBounded. Qed.
imports: Reals ZArith List PeanoNat Psatz