proposition: Theorem errorBoundedMultClosest : forall p q pq : float, Fbounded b p -> Fbounded b q -> Closest b radix (p * q) pq -> (- dExp b <= Fexp p + Fexp q)%Z -> (- dExp b <= Fexp (Fnormalize radix b precision pq) - precision)%Z -> 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 r - precision)%Z :>Z)).
proof: Proof. intros. cut (RoundedModeP b radix (Closest b radix)); [ intros G1 | apply ClosestRoundedModeP with precision; auto ]. case (Req_dec (p * q - pq) 0); intros U. exists (Fnormalize radix b precision pq); exists (Fzero (Fexp (Fnormalize radix b precision pq) - precision)). cut (Fbounded b pq); [ intros G2 | apply RoundedModeBounded with radix (Closest b radix) (p * q)%R; auto ]. cut (Fcanonic radix b (Fnormalize radix b precision pq)); [ intros G3 | apply FnormalizeCanonic; auto with zarith ]. cut (Fbounded b (Fnormalize radix b precision pq)); [ intros G4 | apply FnormalizeBounded; auto with zarith ]. cut (Fnormalize radix b precision pq = pq :>R); [ intros G5 | unfold FtoRradix in |- *; apply FnormalizeCorrect; auto with arith ]. repeat (split; auto). rewrite G5; unfold FtoRradix in |- *; rewrite FzeroisReallyZero; auto with real. lapply (errorBoundedMultClosest_aux p q pq); auto; intros H5. lapply H5; auto; intros H6; clear H5. lapply H6; auto; intros H5; clear H6. lapply H5; auto; intros H6; clear H5. lapply H6; auto; intros H5; clear H6. elim H5; intros r H6; clear H5. elim H6; intros s H5; clear H6. elim H5; intros H7 H6; clear H5. elim H6; intros H8 H9; clear H6. elim H9; intros H6 H10; clear H9. elim H10; intros H9 H11; clear H10. elim H11; intros H10 H12; clear H11. elim H12; intros H11 H13; clear H12. elim H13; intros H12 H14; clear H13. cut (ex (fun m : Z => s = Float m (Fexp r - precision) :>R /\ (Z.abs m <= pPred (vNum b))%Z)). intros H13; elim H13; intros m H15; elim H15; intros H16 H17; clear H15 H13. exists r; exists (Float m (Fexp r - precision)). split; auto. split; auto. split. 2: repeat (split; auto). 2: rewrite <- H16; auto. split; simpl in |- *. generalize H17; unfold pPred in |- *; apply Zle_Zpred_inv. replace r with (Fnormalize radix b precision pq); auto with zarith. apply FcanonicUnique with radix b precision; auto with zarith. apply FnormalizeCanonic; auto with zarith; elim H1; auto. rewrite FnormalizeCorrect; auto with real zarith. cut (radix <> 0%Z :>Z); [ intros V | auto with arith real zarith ]. cut (0 < radix)%Z; [ intros V2 | auto with arith real zarith ]. rewrite H10; unfold FtoRradix in |- *; rewrite <- Fmult_correct; auto. rewrite <- Fminus_correct; fold FtoRradix in |- *; auto. unfold Fmult in |- *; unfold Fminus in |- *; unfold Fopp in |- *; unfold Fplus in |- *; simpl in |- *. unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- *. rewrite Z.min_l; auto with zarith. replace (Fnum p * Fnum q * Zpower_nat radix (Z.abs_nat (Fexp p + Fexp q - (Fexp p + Fexp q))))%Z with (Fnum p * Fnum q)%Z. 2: replace (Fexp p + Fexp q - (Fexp p + Fexp q))%Z with 0%Z; auto with zarith arith; simpl in |- *. 2: auto with zarith. exists ((Fnum p * Fnum q + - Fnum r * Zpower_nat radix (Z.abs_nat (Fexp r - (Fexp p + Fexp q)))) * Zpower_nat radix (Z.abs_nat (Fexp p + Fexp q + (precision - Fexp r))))%Z; split. rewrite plus_IZR. repeat rewrite mult_IZR. rewrite plus_IZR. repeat rewrite mult_IZR. rewrite (Zpower_nat_powerRZ_absolu radix (Fexp r - (Fexp p + Fexp q))). 2: auto with zarith arith. rewrite (Zpower_nat_powerRZ_absolu radix (Fexp p + Fexp q + (precision - Fexp r))) . 2: auto with zarith arith. cut (radix <> 0%R :>R). intros W. unfold Zminus in |- *. repeat rewrite powerRZ_add; auto. apply trans_eq with ((Fnum p * Fnum q + (- Fnum r)%Z * (powerRZ radix (Fexp r) * powerRZ radix (- (Fexp p + Fexp q)))) * (powerRZ radix (Fexp p) * powerRZ radix (Fexp q)))%R. ring; ring. apply trans_eq with ((Fnum p * Fnum q + (- Fnum r)%Z * (powerRZ radix (Fexp r) * powerRZ radix (- (Fexp p + Fexp q)))) * (powerRZ radix (Fexp p) * powerRZ radix (Fexp q) * (powerRZ radix precision * powerRZ radix (- precision))) * (powerRZ radix (Fexp r) * powerRZ radix (- Fexp r)))%R. 2: ring; ring. replace (powerRZ radix precision * powerRZ radix (- precision))%R with 1%R. replace (powerRZ radix (Fexp r) * powerRZ radix (- Fexp r))%R with 1%R; try ring. rewrite <- powerRZ_add; auto. rewrite Zplus_opp_r; simpl in |- *; auto. rewrite <- powerRZ_add; auto. rewrite Zplus_opp_r; simpl in |- *; auto. apply IZR_neq; lia. apply le_IZR; rewrite <- Rabs_Zabs. rewrite mult_IZR; rewrite plus_IZR. repeat rewrite mult_IZR. rewrite (Zpower_nat_powerRZ_absolu radix (Fexp p + Fexp q + (precision - Fexp r))) . 2: auto with zarith arith. rewrite (Zpower_nat_powerRZ_absolu radix (Fexp r - (Fexp p + Fexp q))). 2: auto with zarith arith. rewrite powerRZ_add; auto with real arith. replace ((Fnum p * Fnum q + (- Fnum r)%Z * powerRZ radix (Fexp r - (Fexp p + Fexp q))) * (powerRZ radix (Fexp p + Fexp q) * powerRZ radix (precision - Fexp r)))%R with ((Fnum p * Fnum q + (- Fnum r)%Z * powerRZ radix (Fexp r - (Fexp p + Fexp q))) * powerRZ radix (Fexp p + Fexp q) * powerRZ radix (precision - Fexp r))%R; [ idtac | ring; ring ]. rewrite Rabs_mult. rewrite (Rabs_right (powerRZ radix (precision - Fexp r))). 2: apply Rle_ge; apply powerRZ_le; auto with real zarith. apply Rmult_le_reg_l with (powerRZ radix (Fexp r - precision)). apply powerRZ_lt, IZR_lt; auto with real arith. rewrite Rmult_comm; rewrite Rmult_assoc; rewrite <- powerRZ_add. 2: apply IZR_neq; auto with zarith arith real. 2: apply IZR_lt; auto with zarith arith real. 2: apply IZR_neq; auto with zarith arith real. replace (precision - Fexp r + (Fexp r - precision))%Z with 0%Z; [ simpl in |- * | ring ]. apply Rle_trans with (Rabs ((Fnum p * Fnum q + (- Fnum r)%Z * powerRZ radix (Fexp r - (Fexp p + Fexp q))) * powerRZ radix (Fexp p + Fexp q))); [ right; ring | idtac ]. replace ((Fnum p * Fnum q + (- Fnum r)%Z * powerRZ radix (Fexp r - (Fexp p + Fexp q))) * powerRZ radix (Fexp p + Fexp q))%R with (p * q - r)%R. 2: unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- *; unfold Rminus in |- *. 2: unfold Zminus in |- *; repeat rewrite Ropp_Ropp_IZR. 2: repeat rewrite powerRZ_add; auto with real arith. 2: apply trans_eq with (Fnum p * Fnum q * (powerRZ radix (Fexp p) * powerRZ radix (Fexp q)) + - Fnum r * (powerRZ radix (Fexp r) * (powerRZ radix (- (Fexp p + Fexp q)) * (powerRZ radix (Fexp p) * powerRZ radix (Fexp q)))))%R; [ idtac | ring ]. 2: replace (powerRZ radix (- (Fexp p + Fexp q)) * (powerRZ radix (Fexp p) * powerRZ radix (Fexp q)))%R with 1%R; try ring. 2: repeat rewrite <- powerRZ_add; auto with real arith. 2: replace (- (Fexp p + Fexp q) + (Fexp p + Fexp q))%Z with 0%Z; simpl in |- *; simpl; ring. apply Rle_trans with (powerRZ radix (Fexp r) * / 2)%R. rewrite <- H10; replace (powerRZ radix (Fexp r)) with (FtoRradix (Float 1 (Fexp r))); unfold FtoRradix in |- *; [ idtac | unfold FtoR in |- *; simpl in |- *; ring ]. apply ClosestErrorBound with b precision (p * q)%R; auto. apply (ClosestCompatible b radix (p * q)%R (p * q)%R pq); auto. unfold Zminus in |- *; rewrite powerRZ_add; auto with real arith. rewrite Rmult_assoc; apply Rmult_le_compat_l. apply powerRZ_le; auto with real arith. apply IZR_lt; lia. unfold pPred, Z.pred in |- *; rewrite pGivesBound. rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ. replace (powerRZ radix (- precision) * (powerRZ radix precision + (-1)%Z))%R with (1 + - powerRZ radix (- precision))%R. apply Rle_trans with (1 + - powerRZ radix (- 1))%R. simpl in |- *. replace (radix * 1)%R with (IZR radix); [ idtac | ring ]. replace (/ 2)%R with (1 + - / 2)%R. apply Rplus_le_compat_l; apply Ropp_le_contravar. apply Rle_Rinv; auto with real arith zarith. apply IZR_le; lia. field. apply Rplus_le_compat_l; apply Ropp_le_contravar. apply Rle_powerRZ; try lia. apply IZR_le; lia. rewrite Rmult_plus_distr_l. rewrite <- powerRZ_add. replace (- precision + precision)%Z with 0%Z; simpl in |- *; ring. now apply IZR_neq. now apply IZR_neq. now apply IZR_neq. now apply IZR_neq. now apply IZR_neq. now apply IZR_neq. Qed.
imports: Reals ZArith List PeanoNat Psatz