proposition: Theorem errorBoundedMultExpPos : forall P, RoundedModeP b radix P -> forall p q pq : float, Fbounded b p -> Fbounded b q -> (0 <= p)%R -> (0 <= q)%R -> P (p * q)%R pq -> (- dExp b <= Fexp p + Fexp q)%Z -> ex (fun r : float => ex (fun s : float => 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 H p q pq H0 H1 H2 H3 H4 H5. case (multExpUpperBound P H p q pq); auto; intros r (H'1, (H'2, H'3)). case (Req_dec (p * q - pq) 0); intros H6. case (Req_dec pq 0); intros H7. cut (Fbounded b (Fzero (Fexp p + Fexp q))); [ intros Fb1 | idtac ]. exists (Fzero (Fexp p + Fexp q)); exists (Fzero (Fexp p + Fexp q)); repeat (split; simpl in |- *; auto with zarith). rewrite H7; unfold FtoRradix in |- *; apply FzeroisReallyZero. unfold FtoRradix in |- *; rewrite FzeroisReallyZero; rewrite <- H7. pattern (FtoRradix pq) at 1 in |- *; rewrite H7; auto with real. repeat (split; auto); simpl in |- *; auto with arith zarith. case (errorBoundedMultExp_aux (Fnum p) (Fnum q)); auto with real zarith. apply H0. apply H1. exists (Fnum pq); exists (Fexp pq - (Fexp p + Fexp q))%Z; split. apply Rmult_eq_reg_l with (powerRZ radix (Fexp p + Fexp q)); auto with real zarith. repeat rewrite (fun x y => Rmult_comm (powerRZ x y)). apply trans_eq with (p * q)%R; auto. rewrite <- (Fmult_correct radix); auto with real zarith; unfold FtoRradix, FtoR, Fmult in |- *; simpl in |- *; rewrite mult_IZR; auto. apply trans_eq with (FtoRradix pq); auto with real. rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith. replace (Fexp pq - (Fexp p + Fexp q) + (Fexp p + Fexp q))%Z with (Fexp pq); auto; ring. apply IZR_neq; lia. apply Rgt_not_eq, powerRZ_lt, IZR_lt; lia. cut (Fbounded b pq); [ intros Z1; case Z1 | idtac ]; auto with real zarith. apply (RoundedModeBounded b radix P (p * q)); auto. intros nx (ex, (H'4, (H'5, (H'6, H'7)))). cut (FtoRradix pq = FtoRradix (Float nx (ex + (Fexp p + Fexp q))) :>R); [ intros Eq1 | idtac ]. exists (Float nx (ex + (Fexp p + Fexp q))); exists (Fzero (Fexp p + Fexp q)); repeat (split; simpl in |- *; auto with real zarith). rewrite <- Eq1; rewrite H6; apply (FzeroisReallyZero radix). replace (FtoRradix pq) with (p * q)%R. unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- *. rewrite powerRZ_add. 2: apply IZR_neq; lia. repeat rewrite <- Rmult_assoc; rewrite <- H'4; rewrite powerRZ_add. ring. apply IZR_neq; lia. replace (FtoRradix p * FtoRradix q)%R with (pq + (FtoRradix p * FtoRradix q - FtoRradix pq))%R; [ rewrite H6 | idtac ]; ring. case (errorBoundedMultPos P H p q pq); auto. intros s (H'4, (H'5, H'6)). exists r; exists s; repeat (split; auto with zarith). rewrite H'2; auto. apply Zlt_le_weak; apply RoundedModeErrorExpStrict with b radix precision P (p * q)%R; auto. cut (CompatibleP b radix P); [ intros H'7 | case H; try intros H'7 (H'8, (H'9, H'10)); auto ]. apply H'7 with (p * q)%R pq; auto with real. fold FtoRradix in |- *; rewrite H'2; auto with real. fold FtoRradix in |- *; rewrite H'4; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz