proposition: Theorem errorBoundedMultClosest_aux : forall p q pq : float, Fbounded b p -> Fbounded b q -> Closest b radix (p * q) pq -> (- dExp b <= Fexp p + Fexp q)%Z -> (p * q - pq)%R <> 0%R :>R -> ex (fun r : float => ex (fun s : float => Fcanonic radix b r /\ Fbounded b r /\ Fbounded b s /\ r = pq :>R /\ s = (p * q - r)%R :>R /\ Fexp s = (Fexp p + Fexp q)%Z :>Z /\ (Fexp s <= Fexp r)%Z /\ (Fexp r <= precision + (Fexp p + Fexp q))%Z)).
proof: Proof. intros p q pq Hp Hq H1 H2 H3. cut (RoundedModeP b radix (Closest b radix)); [ intros H4 | apply ClosestRoundedModeP with precision; auto ]. lapply (errorBoundedMultExp b radix precision); [ intros H'2; lapply H'2; [ intros H'3; lapply H'3; [ intros H'4; lapply (H'4 (Closest b radix)); [ intros H'7; elim (H'7 p q pq); [ intros r E; elim E; intros s E0; elim E0; intros H'15 H'16; elim H'16; intros H'17 H'18; elim H'18; intros H'19 H'20; elim H'20; intros H'21 H'22; elim H'22; intros H'23 H'24; elim H'24; intros H'25 H'26; clear H'24 H'22 H'20 H'18 H'16 E0 E H'3 H'2 | clear H'3 H'2 | clear H'3 H'2 | clear H'3 H'2 | clear H'3 H'2 ] | clear H'3 H'2 ] | clear H'3 H'2 ] | clear H'2 ] | idtac]; auto. exists (Fnormalize radix b precision r); exists s. cut (Fbounded b (Fnormalize radix b precision r)); [ intros H5 | apply FnormalizeBounded; auto with zarith ]. split; [ apply FnormalizeCanonic; auto with zarith | idtac ]. repeat (split; auto). unfold FtoRradix in |- *; rewrite <- H'19; unfold FtoRradix in |- *; apply FnormalizeCorrect; auto. unfold FtoRradix in |- *; rewrite FnormalizeCorrect; auto with arith. apply Zlt_le_weak. apply RoundedModeErrorExpStrict with b radix precision (Closest b radix) (p * q)%R; auto with arith. generalize ClosestCompatible; unfold CompatibleP in |- *; intros H6. generalize (H6 b radix (FtoRradix p * FtoRradix q)%R (FtoRradix p * FtoRradix q)%R pq); intros H9; apply H9; auto. rewrite FnormalizeCorrect; auto with real arith. rewrite FnormalizeCorrect; auto with real arith. rewrite H'21; rewrite H'19; auto. apply Z.le_trans with (Fexp r); auto. apply FcanonicLeastExp with radix b precision; auto with zarith. rewrite FnormalizeCorrect; auto with real arith. apply FnormalizeCanonic; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz