proposition: Theorem errorBoundedMultMin : forall p q fmin : float, Fbounded b p -> Fbounded b q -> (0 <= p)%R -> (0 <= q)%R -> (- dExp b <= Fexp p + Fexp q)%Z -> isMin b radix (p * q) fmin -> exists r : float, r = (p * q - fmin)%R :>R /\ Fbounded b r /\ Fexp r = (Fexp p + Fexp q)%Z.
proof: Proof. intros p q fmin Fp Fq H' H'0 H'1 H'2. cut (0 <= Fnum p * Fnum q)%Z; [ intros multPos | apply Z.mul_nonneg_nonneg; apply (LeR0Fnum radix); auto with arith ]. cut (ex (fun m : Z => FtoRradix fmin = Float m (Fexp (Fmult p q)))). 2: unfold FtoRradix in |- *; apply RoundedModeRep with (b := b) (precision := precision) (P := isMin b radix); auto. 2: apply MinRoundedModeP with (precision := precision); auto. 2: rewrite (Fmult_correct radix); auto with zarith. intros H'3; elim H'3; intros m E; clear H'3. exists (Fminus radix (Fmult p q) (Float m (Fexp (Fmult p q)))). split. rewrite E; unfold FtoRradix in |- *; repeat rewrite Fminus_correct; repeat rewrite Fmult_correct; auto with zarith. split. cut (fmin <= Fmult p q)%R; [ idtac | unfold FtoRradix in |- *; rewrite Fmult_correct; auto; case H'2; auto with real zarith; (intros H1 H2; case H2; auto with zarith) ]. rewrite E; unfold Fmult, Fminus, Fopp, Fplus in |- *; simpl in |- *; auto. repeat rewrite Zmin_n_n; repeat rewrite <- Zminus_diag_reverse; auto. simpl in |- *; repeat rewrite Zpower_nat_O; repeat rewrite Zmult_1_r. unfold FtoRradix, FtoR in |- *; simpl in |- *. intros H'3; (cut (m <= Fnum p * Fnum q)%Z; [ idtac | apply le_IZR; apply Rmult_le_reg_l with (r := powerRZ radix (Fexp p + Fexp q)); auto with real zarith; repeat rewrite (Rmult_comm (powerRZ radix (Fexp p + Fexp q))); auto with zarith; apply powerRZ_lt, IZR_lt; lia ]); intros H'4. repeat split; simpl in |- *; auto. case (ZquotientProp (Fnum p * Fnum q) (Zpower_nat radix precision)); try lia. intros x (H'5, (H'6, H'7)). cut (Zquotient (Fnum p * Fnum q) (Zpower_nat radix precision) * powerRZ radix (precision + (Fexp p + Fexp q)) <= fmin)%R; [ rewrite E; intros H'8 | idtac ]. cut (Zquotient (Fnum p * Fnum q) (Zpower_nat radix precision) * powerRZ radix precision <= m)%R; [ intros H'9 | idtac ]. rewrite Z.abs_eq; auto with zarith. apply Z.le_lt_trans with x; auto. replace x with (Fnum p * Fnum q + - (Zquotient (Fnum p * Fnum q) (Zpower_nat radix precision) * Zpower_nat radix precision))%Z. apply Zplus_le_compat_l; auto. apply Zle_Zopp. apply le_IZR; auto. rewrite mult_IZR. rewrite Zpower_nat_Z_powerRZ; auto with zarith. pattern (Fnum p * Fnum q)%Z at 1 in |- *; rewrite H'5; ring. rewrite pGivesBound. rewrite <- (Z.abs_eq (Zpower_nat radix precision)); lia. apply Rmult_le_reg_l with (r := powerRZ radix (Fexp p + Fexp q)); auto with real zarith. apply powerRZ_lt, IZR_lt; lia. repeat rewrite (Rmult_comm (powerRZ radix (Fexp p + Fexp q))); auto. rewrite Rmult_assoc; rewrite <- powerRZ_add. auto with real zarith. apply IZR_neq; lia. case (FboundedMbound _ radixMoreThanOne b precision) with (z := (precision + (Fexp p + Fexp q))%Z) (m := Zquotient (Fnum p * Fnum q) (Zpower_nat radix precision)); auto with zarith. apply Zmult_le_reg_r with (p := Zpower_nat radix precision); try lia. pattern (Zpower_nat radix precision) at 2 in |- *; rewrite <- (fun x => Z.abs_eq (Zpower_nat radix x)). rewrite <- Zabs_Zmult. apply Z.le_trans with (1 := H'6); auto with zarith. rewrite Zabs_Zmult. apply Z.le_trans with (Zpower_nat radix precision * Z.abs (Fnum q))%Z. apply Zle_Zmult_comp_r; auto with zarith. apply Zlt_le_weak; rewrite <- pGivesBound; apply Fp. apply Zle_Zmult_comp_l; try lia. apply Zlt_le_weak; rewrite <- pGivesBound; apply Fq. apply Zpower_NR0; lia. intros x0 (H'8, H'9); rewrite <- H'9. case H'2. intros H'10 (H'11, H'12); apply H'12; auto. rewrite H'9; auto. rewrite powerRZ_add. rewrite <- Rmult_assoc. unfold FtoRradix in |- *; rewrite <- Fmult_correct; auto with zarith. unfold Fmult, FtoR in |- *; simpl in |- *. repeat rewrite (fun x => Rmult_comm x (powerRZ radix (Fexp p + Fexp q))). apply Rmult_le_compat_l; auto with real zarith. apply powerRZ_le, IZR_lt; lia. rewrite <- Zpower_nat_Z_powerRZ. pattern (Fnum p * Fnum q)%Z at 2 in |- *; rewrite <- (Z.abs_eq (Fnum p * Fnum q)); auto. rewrite <- mult_IZR; apply IZR_le; apply Zle_Zabs_inv2; auto. apply IZR_neq; lia. simpl in |- *. apply Zmin_n_n. Qed.
imports: Reals ZArith List PeanoNat Psatz