proposition: Theorem multExpUpperBound : forall P, RoundedModeP b radix P -> forall p q pq : float, P (p * q)%R pq -> Fbounded b p -> Fbounded b q -> (- dExp b <= Fexp p + Fexp q)%Z -> exists r : float, Fbounded b r /\ r = pq :>R /\ (Fexp r <= precision + (Fexp p + Fexp q))%Z.
proof: Proof. intros P H' p q pq H'0 H'1 H'2 H'3. replace (precision + (Fexp p + Fexp q))%Z with (Fexp (Float (pPred (vNum b)) (precision + (Fexp p + Fexp q)))); [ idtac | simpl in |- *; auto ]. unfold FtoRradix in |- *; apply eqExpMax; auto. apply RoundedModeBounded with (radix := radix) (P := P) (r := (p * q)%R); auto; auto. unfold pPred in |- *; apply maxFbounded; auto. apply Z.le_trans with (1 := H'3); auto with zarith. replace (FtoR radix (Float (pPred (vNum b)) (precision + (Fexp p + Fexp q)))) with (radix * Float (pPred (vNum b)) (pred precision + (Fexp p + Fexp q)))%R. rewrite Fabs_correct; auto with zarith. unfold FtoRradix in |- *; apply RoundedModeMultAbs with (b := b) (precision := precision) (P := P) (r := (p * q)%R); auto. unfold pPred in |- *; apply maxFbounded; auto with zarith. rewrite Rabs_mult; auto. apply Rle_trans with (FtoR radix (Fmult (Float (pPred (vNum b)) (Fexp p)) (Float (pPred (vNum b)) (Fexp q)))). rewrite Fmult_correct; auto with arith. apply Rmult_le_compat; auto with real; try apply Rabs_pos. rewrite <- (Fabs_correct radix); try apply maxMax1; auto with zarith. rewrite <- (Fabs_correct radix); try apply maxMax1; auto with zarith. unfold Fmult, FtoR in |- *; simpl in |- *; auto. rewrite powerRZ_add with (n := Z_of_nat (pred precision)); auto with real arith. repeat rewrite <- Rmult_assoc. repeat rewrite (fun (z : Z) (x : R) => Rmult_comm x (powerRZ radix z)); auto. apply Rmult_le_compat_l; auto with real arith. apply powerRZ_le, IZR_lt; lia. rewrite <- Rmult_assoc. rewrite (fun x : R => Rmult_comm x radix). rewrite <- powerRZ_Zs; auto with real arith. replace (Z.succ (pred precision)) with (Z_of_nat precision). rewrite mult_IZR; auto. apply Rmult_le_compat; auto with real arith. apply IZR_le, Zle_Zpred; auto with zarith. apply IZR_le, Zle_Zpred; auto with zarith. unfold pPred in |- *; rewrite pGivesBound; rewrite <- Zpower_nat_Z_powerRZ; apply IZR_le; auto with real zarith. rewrite inj_pred; auto with arith zarith. apply IZR_neq; auto with real zarith. apply IZR_neq; auto with real zarith. unfold FtoRradix, FtoR in |- *; simpl in |- *. repeat rewrite (Rmult_comm (pPred (vNum b))). rewrite <- Rmult_assoc. rewrite <- powerRZ_Zs. rewrite inj_pred; auto with arith zarith. replace (Z.succ (Z.pred precision + (Fexp p + Fexp q))) with (precision + (Fexp p + Fexp q))%Z; auto; unfold Z.succ, Z.pred in |- *; ring. apply IZR_neq; auto with real zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz