proposition: Theorem errorBoundedMultMax : forall p q fmax : float, Fbounded b p -> Fbounded b q -> (0 <= p)%R -> (0 <= q)%R -> (- dExp b <= Fexp p + Fexp q)%Z -> isMax b radix (p * q) fmax -> exists r : float, FtoRradix r = (p * q - fmax)%R /\ Fbounded b r /\ Fexp r = (Fexp p + Fexp q)%Z.
proof: Proof. intros p q fmax 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 ]. case (ZquotientProp (Fnum p * Fnum q) (Zpower_nat radix precision)). lia. intros r; intros (H'3, (H'4, H'5)). cut (0 <= Zquotient (Fnum p * Fnum q) (Zpower_nat radix precision))%Z; [ intros Z2 | apply ZquotientPos; lia ]. cut (0 <= r)%Z; [ intros Z3 | replace r with (Fnum p * Fnum q - Zquotient (Fnum p * Fnum q) (Zpower_nat radix precision) * Zpower_nat radix precision)%Z; [ idtac | pattern (Fnum p * Fnum q)%Z at 1 in |- *; rewrite H'3; ring ]; auto ]. 2: apply Zle_minus_le_0, Zle_Zabs_inv2 ; now rewrite (Z.abs_eq _ multPos) in H'4. case (Z.eq_dec r 0); intros Z4. exists (Fzero (Fexp p + Fexp q)); repeat (split; auto with zarith). replace (FtoRradix (Fzero (Fexp p + Fexp q))) with 0%R; [ idtac | unfold Fzero, FtoRradix, FtoR in |- *; simpl in |- *; ring ]. apply Rplus_eq_reg_l with (r := FtoRradix fmax). replace (fmax + 0)%R with (FtoRradix fmax); [ idtac | ring ]. replace (fmax + (p * q - fmax))%R with (p * q)%R; [ idtac | ring ]. unfold FtoRradix in |- *; rewrite <- (Fmult_correct radix); auto with zarith. 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). 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'4); 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. lia. apply Zlt_le_weak; rewrite <- pGivesBound; apply Fq. apply Zpower_NR0; lia. intros x (H'6, H'7). cut (FtoR radix (Fmult p q) = FtoR radix x). intros H'8; rewrite H'8. apply sym_eq; apply (ProjectMax b radix); auto. rewrite <- H'8; auto. rewrite Fmult_correct; auto with zarith. rewrite H'7. unfold FtoRradix, FtoR in |- *; simpl in |- *. rewrite powerRZ_add with (n := Z_of_nat precision). pattern (Fnum p * Fnum q)%Z at 1 in |- *; rewrite H'3. rewrite plus_IZR; rewrite mult_IZR. repeat rewrite Zpower_nat_Z_powerRZ; auto with real zarith. rewrite Z4; simpl;ring. apply IZR_neq; lia. cut (ex (fun m : Z => FtoRradix fmax = Float m (Fexp (Fmult p q)))); [ intros Z5 | idtac ]. 2: unfold FtoRradix in |- *; apply RoundedModeRep with (b := b) (precision := precision) (P := isMax b radix); auto. 2: apply MaxRoundedModeP with (precision := precision); auto. 2: rewrite (Fmult_correct radix); auto with zarith. elim Z5; intros m E; clear Z5. exists (Fopp (Fminus radix (Float m (Fexp (Fmult p q))) (Fmult p q))). split. rewrite E; unfold FtoRradix in |- *; repeat rewrite Fopp_correct; repeat rewrite Fminus_correct; repeat rewrite Fmult_correct; auto with zarith; ring. cut (Fexp (Fopp (Fminus radix (Float m (Fexp (Fmult p q))) (Fmult p q))) = (Fexp p + Fexp q)%Z); [ intros Z5 | idtac ]. split; auto. split; [ idtac | rewrite Z5; auto ]. cut (Fmult p q <= fmax)%R; [ idtac | unfold FtoRradix in |- *; rewrite Fmult_correct; auto; case H'2; auto with real zarith; (intros H1 H2; case H2; auto) ]. cut (fmax <= Z.succ (Zquotient (Fnum p * Fnum q) (Zpower_nat radix precision)) * powerRZ radix (precision + (Fexp p + Fexp q)))%R. rewrite E; repeat rewrite Zmin_n_n; repeat rewrite <- Zminus_diag_reverse; repeat rewrite Zpower_nat_O; repeat rewrite Zmult_1_r; auto. unfold Fmult, Fminus, Fplus, Fopp in |- *; simpl in |- *. repeat rewrite Zmin_n_n; repeat rewrite <- Zminus_diag_reverse; repeat rewrite Zpower_nat_O; repeat rewrite Zmult_1_r; auto. intros H1 H2; rewrite Zabs_Zopp; apply Zlt_Zabs_intro. apply Z.lt_le_trans with 0%Z; try lia. cut (Fnum p * Fnum q <= m)%Z; auto with zarith. apply le_IZR; apply (Rle_monotony_contra_exp radix) with (z := (Fexp p + Fexp q)%Z); auto with zarith. cut (m <= Z.succ (Zquotient (Fnum p * Fnum q) (Zpower_nat radix precision)) * Zpower_nat radix precision)%Z; [ intros H'9 | idtac ]. apply Z.le_lt_trans with (Zpower_nat radix precision - r)%Z; [ idtac | rewrite pGivesBound; auto with zarith ]. replace r with (Fnum p * Fnum q - Zquotient (Fnum p * Fnum q) (Zpower_nat radix precision) * Zpower_nat radix precision)%Z. replace (Zpower_nat radix precision - (Fnum p * Fnum q - Zquotient (Fnum p * Fnum q) (Zpower_nat radix precision) * Zpower_nat radix precision))%Z with (Z.succ (Zquotient (Fnum p * Fnum q) (Zpower_nat radix precision)) * Zpower_nat radix precision - Fnum p * Fnum q)%Z; lia. pattern (Fnum p * Fnum q)%Z at 1 in |- *; rewrite H'3; ring. apply le_IZR; apply (Rle_monotony_contra_exp radix) with (z := (Fexp p + Fexp q)%Z); auto with zarith. replace (IZR (Z.succ (Zquotient (Fnum p * Fnum q) (Zpower_nat radix precision)) * Zpower_nat radix precision) * powerRZ radix (Fexp p + Fexp q))%R with (Z.succ (Zquotient (Fnum p * Fnum q) (Zpower_nat radix precision)) * powerRZ radix (precision + (Fexp p + Fexp q)))%R; [ auto | idtac ]. rewrite powerRZ_add. repeat rewrite mult_IZR; repeat rewrite Zpower_nat_Z_powerRZ. ring. apply IZR_neq; lia. case (FboundedMbound _ radixMoreThanOne b precision) with (z := (precision + (Fexp p + Fexp q))%Z) (m := Z.succ (Zquotient (Fnum p * Fnum q) (Zpower_nat radix precision))); auto with zarith. rewrite Z.abs_eq; auto with zarith. apply Zlt_le_succ. case (Zle_lt_or_eq _ _ multPos); intros Eq1. cut (0 < Z.abs (Fnum p))%Z; [ intros Eq2 | idtac ]. cut (0 < Z.abs (Fnum q))%Z; [ intros Eq3 | idtac ]. apply Zlt_mult_simpl_l with (c := Zpower_nat radix precision); try lia. rewrite (fun x y z => Zmult_comm x (Zquotient y z)). apply Z.le_lt_trans with (Fnum p * Fnum q)%Z. rewrite Z.abs_eq in H'4; auto with zarith; rewrite Z.abs_eq in H'4; auto with zarith. cut (Z.abs (Fnum q) < Zpower_nat radix precision)%Z; [ intros Eq4| rewrite <- pGivesBound; apply Fq ]; auto with zarith. cut (Z.abs (Fnum p) < Zpower_nat radix precision)%Z; [ intros Eq4' | rewrite <- pGivesBound; case Fp ]; auto with zarith. apply Z.le_lt_trans with (Z.abs (Fnum p*Fnum q)). apply Zle_Zabs. rewrite Zabs_Zmult. apply Z.lt_trans with (Z.abs (Fnum p) * Zpower_nat radix precision)%Z. apply Zmult_gt_0_lt_compat_l. lia. unfold Fbounded in Fq; lia. apply Zmult_gt_0_lt_compat_r. lia. unfold Fbounded in Fp; lia. case (Zle_lt_or_eq _ _ (Z.abs_nonneg (Fnum q))); auto. intros Eq3; contradict Eq1; replace (Fnum q) with 0%Z; lia. case (Zle_lt_or_eq _ _ (Z.abs_nonneg (Fnum p))); auto. intros Eq3; contradict Eq1; replace (Fnum p) with 0%Z; lia. rewrite <- Eq1; replace (Zquotient 0 (Zpower_nat radix precision)) with 0%Z; lia. intros f1 (Hf1, Hf2); rewrite <- Hf2. case H'2; intros L1 (L2, L3); apply L3; auto. rewrite Hf2; unfold Fmult, FtoRradix, FtoR in |- *. replace (Fnum p * powerRZ radix (Fexp p) * (Fnum q * powerRZ radix (Fexp q)))%R with (Fnum p * Fnum q * powerRZ radix (Fexp p + Fexp q))%R. replace (Z.succ (Zquotient (Fnum p * Fnum q) (Zpower_nat radix precision)) * powerRZ radix (precision + (Fexp p + Fexp q)))%R with ((Zquotient (Fnum p * Fnum q) (Zpower_nat radix precision) * Zpower_nat radix precision + Zpower_nat radix precision)%Z * powerRZ radix (Fexp p + Fexp q))%R. apply Rle_monotone_exp; auto with real zarith. rewrite <- mult_IZR; apply IZR_le. lia. unfold Z.succ in |- *; repeat rewrite mult_IZR || rewrite plus_IZR; simpl in |- *. rewrite (powerRZ_add radix precision). rewrite <- (Zpower_nat_Z_powerRZ radix precision); auto with real zarith; ring. apply IZR_neq; lia. rewrite powerRZ_add. auto with real zarith; try ring. apply IZR_neq; lia. unfold Fopp, Fminus, Fmult in |- *; simpl in |- *; auto. apply Zmin_n_n. Qed.
imports: Reals ZArith List PeanoNat Psatz