proposition: Theorem errorBoundedMultExp : forall P, (RoundedModeP b radix P) -> forall p q pq : float, (Fbounded b p) -> (Fbounded b q) -> (P (p * q)%R pq) -> (-(dExp b) <= Fexp p + Fexp q)%Z -> exists r : float, exists s : float, (Fbounded b r) /\ (Fbounded b s) /\ r = pq :>R /\ s = (p * q - r)%R :>R /\ (Fexp s = Fexp p + Fexp q)%Z /\ (Fexp s <= Fexp r)%Z /\ (Fexp r <= precision + (Fexp p + Fexp q))%Z.
proof: Proof. intros P H p q pq H1 H2 H3 H4. cut (MinOrMaxP b radix P); [ intros | case H; intros H'1 (H'2, (H'3, H'4)); auto ]. case H0 with (p*q)%R pq; auto; intros H0'; clear H0. case (Rle_or_lt 0 p); intros Rl1. case (Rle_or_lt 0 q); intros Rl2. apply (errorBoundedMultExpPos P); auto. case errorBoundedMultExpPos with (isMax b radix) p (Fopp q) (Fopp pq); auto with zarith real. apply MaxRoundedModeP with precision; auto. apply oppBounded; easy. rewrite (Fopp_correct radix); auto with real. replace (FtoRradix p * FtoRradix (Fopp q))%R with (- (FtoRradix p * FtoRradix q))%R; [apply MinOppMax;auto|idtac]. rewrite (Fopp_correct radix); fold FtoRradix in |- *; auto with zarith; ring. intros r (s, (H5, (H6, (H7, (H8, H9))))); exists (Fopp r); exists (Fopp s). split; try now apply oppBounded. split; try now apply oppBounded. split. generalize H7; unfold FtoRradix; rewrite 2!Fopp_correct. intros Y; rewrite Y; ring. split. generalize H8; unfold FtoRradix; rewrite 3!Fopp_correct. intros Y; rewrite Y; ring. split; simpl; try apply H9. case (Rle_or_lt 0 q); intros Rl2. case errorBoundedMultExpPos with (isMax b radix) (Fopp p) q (Fopp pq); auto with zarith real. apply MaxRoundedModeP with precision; auto. now apply oppBounded. rewrite (Fopp_correct radix); auto with real. replace (FtoRradix (Fopp p) * FtoRradix q)%R with (- (FtoRradix p * FtoRradix q))%R; [apply MinOppMax;auto|idtac]. rewrite (Fopp_correct radix); fold FtoRradix in |- *; auto with zarith; ring. intros r (s, (H5, (H6, (H7, (H8, H9))))); exists (Fopp r); exists (Fopp s); repeat (split; try apply oppBounded; simpl in |- *; auto with real zarith). repeat rewrite (Fopp_correct radix); auto with zarith; fold FtoRradix in |- *; rewrite H7; repeat rewrite (Fopp_correct radix); auto with zarith; fold FtoRradix; ring. repeat rewrite (Fopp_correct radix); auto with zarith; fold FtoRradix in |- *; rewrite H8; repeat rewrite (Fopp_correct radix); auto with zarith; fold FtoRradix;ring. case (errorBoundedMultExpPos P H (Fopp p) (Fopp q) pq); auto with zarith real. apply oppBounded; easy. apply oppBounded; easy. rewrite (Fopp_correct radix); auto with real. rewrite (Fopp_correct radix); auto with real. replace (FtoRradix (Fopp p) * FtoRradix (Fopp q))%R with (FtoRradix p * FtoRradix q)%R; auto; repeat rewrite (Fopp_correct radix); fold FtoRradix in |- *; auto with zarith; ring. intros r (s, (H5, (H6, (H7, (H8, (H9, (H10, H11))))))); exists r; exists s; repeat (split; simpl in |- *; auto with real zarith). fold FtoRradix in |- *; rewrite H8; repeat rewrite (Fopp_correct radix); auto with zarith; fold FtoRradix; try ring. case (Rle_or_lt 0 p); intros Rl1. case (Rle_or_lt 0 q); intros Rl2. apply (errorBoundedMultExpPos P); auto. case errorBoundedMultExpPos with (isMin b radix) p (Fopp q) (Fopp pq); auto with zarith real. apply MinRoundedModeP with precision; auto. now apply oppBounded. rewrite (Fopp_correct radix); auto with real. replace (FtoRradix p * FtoRradix (Fopp q))%R with (- (FtoRradix p * FtoRradix q))%R; [apply MaxOppMin;auto|idtac]. rewrite (Fopp_correct radix); fold FtoRradix in |- *; auto with zarith; ring. intros r (s, (H5, (H6, (H7, (H8, H9))))); exists (Fopp r); exists (Fopp s); repeat (split; try apply oppBounded; simpl in |- *; auto with real zarith). repeat rewrite (Fopp_correct radix); auto with zarith; fold FtoRradix in |- *; rewrite H7; repeat rewrite (Fopp_correct radix); auto with zarith; fold FtoRradix; ring. repeat rewrite (Fopp_correct radix); auto with zarith; fold FtoRradix in |- *; rewrite H8; repeat rewrite (Fopp_correct radix); auto with zarith; fold FtoRradix; ring. case (Rle_or_lt 0 q); intros Rl2. case errorBoundedMultExpPos with (isMin b radix) (Fopp p) q (Fopp pq); auto with zarith real. apply MinRoundedModeP with precision; auto. now apply oppBounded. rewrite (Fopp_correct radix); auto with real. replace (FtoRradix (Fopp p) * FtoRradix q)%R with (- (FtoRradix p * FtoRradix q))%R; [apply MaxOppMin;auto|idtac]. rewrite (Fopp_correct radix); fold FtoRradix in |- *; auto with zarith; ring. intros r (s, (H5, (H6, (H7, (H8, H9))))); exists (Fopp r); exists (Fopp s); repeat (split; try apply oppBounded; simpl in |- *; auto with real zarith). repeat rewrite (Fopp_correct radix); auto with zarith; fold FtoRradix in |- *; rewrite H7; repeat rewrite (Fopp_correct radix); auto with zarith; fold FtoRradix; ring. repeat rewrite (Fopp_correct radix); auto with zarith; fold FtoRradix in |- *; rewrite H8; repeat rewrite (Fopp_correct radix); auto with zarith; fold FtoRradix;ring. case (errorBoundedMultExpPos P H (Fopp p) (Fopp q) pq); auto with zarith real. now apply oppBounded. now apply oppBounded. rewrite (Fopp_correct radix); auto with real. rewrite (Fopp_correct radix); auto with real. replace (FtoRradix (Fopp p) * FtoRradix (Fopp q))%R with (FtoRradix p * FtoRradix q)%R; auto; repeat rewrite (Fopp_correct radix); fold FtoRradix in |- *; auto with zarith; ring. intros r (s, (H5, (H6, (H7, (H8, (H9, (H10, H11))))))); exists r; exists s; repeat (split; try apply oppBounded; simpl in |- *; auto with real zarith). fold FtoRradix in |- *; rewrite H8; repeat rewrite (Fopp_correct radix); auto with zarith; fold FtoRradix; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz