proposition: Theorem errorBoundedMultExp_aux : forall n1 n2 : Z, (Z.abs n1 < Zpos (vNum b))%Z -> (Z.abs n2 < Zpos (vNum b))%Z -> (exists ny : Z, (exists ey : Z, (n1 * n2)%R = (ny * powerRZ radix ey)%R :>R /\ (Z.abs ny < Zpos (vNum b))%Z)) -> exists nx : Z, (exists ex : Z, (n1 * n2)%R = (nx * powerRZ radix ex)%R :>R /\ (Z.abs nx < Zpos (vNum b))%Z /\ (0 <= ex)%Z /\ (ex <= precision)%Z).
proof: Proof. intros n1 n2 H H0 H1. case H1; intros ny (ey, (H2, H3)). case (Zle_or_lt 0 ey); intros Zl1. case (Zle_or_lt ey precision); intros Zl2. exists ny; exists ey; repeat (split; auto). exists (ny * Zpower_nat radix (Z.abs_nat (ey - precision)))%Z; exists (Z_of_nat precision); repeat (split; auto with zarith). replace (IZR (ny * Zpower_nat radix (Z.abs_nat (ey - precision)))) with (ny * powerRZ radix (ey - precision))%R. rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with zarith real. replace (ey - precision + precision)%Z with ey; [ auto | ring ]. apply IZR_neq; lia. rewrite mult_IZR. rewrite Zpower_nat_powerRZ_absolu; auto with real zarith. rewrite Zabs_Zmult. apply lt_IZR; apply Rmult_lt_reg_l with (r := powerRZ radix precision); auto with real zarith. apply powerRZ_lt, IZR_lt; lia. repeat rewrite (fun x y => Rmult_comm (powerRZ x y)). rewrite mult_IZR. rewrite Rmult_assoc. rewrite (Z.abs_eq (Zpower_nat radix (Z.abs_nat (ey - precision)))); auto with zarith. rewrite Zpower_nat_powerRZ_absolu; auto with real zarith. rewrite <- powerRZ_add; auto with real zarith. replace (ey - precision + precision)%Z with ey; [ idtac | ring ]. replace (powerRZ radix precision) with (IZR (Zpos (vNum b))); [ idtac | rewrite pGivesBound; rewrite <- Zpower_nat_powerRZ_absolu; try rewrite Zabs2Nat.id; auto with zarith ]. rewrite <- (fun x y => Rabs_pos_eq (powerRZ x y)); auto with real zarith. rewrite <- Rabs_Zabs; rewrite <- Rabs_mult; rewrite <- H2. rewrite Rabs_mult; repeat rewrite Rabs_Zabs; auto with real zarith. case (Zle_lt_or_eq 0 (Z.abs n2)); auto with zarith; intros Z1. apply Rlt_trans with (Zpos (vNum b) * Z.abs n2)%R; auto with real zarith. apply Rmult_lt_compat_r; apply IZR_lt; try easy. apply Rmult_lt_compat_l; apply IZR_lt; try easy. rewrite <- Z1; auto with real zarith. replace (Z.abs n1 * 0%Z)%R with (0 * Zpos (vNum b))%R; [ auto with real zarith | simpl; ring ]. apply powerRZ_le, IZR_lt; lia. apply IZR_neq; lia. apply Zpower_NR0; lia. exists (n1 * n2)%Z; exists 0%Z; repeat (split; auto with zarith). rewrite mult_IZR; rewrite powerRZ_O; ring. apply lt_IZR. rewrite <- Rabs_Zabs; rewrite mult_IZR; rewrite H2. rewrite Rabs_mult. apply Rle_lt_trans with (Rabs ny). pattern (Rabs ny) at 2 in |- *; replace (Rabs ny) with (Rabs ny * 1)%R; [ apply Rmult_le_compat_l | ring ]; auto with arith real. apply Rabs_pos. rewrite (Rabs_pos_eq (powerRZ radix ey)); [ idtac | apply powerRZ_le, IZR_lt; auto with arith real ]. replace 1%R with (powerRZ radix 0); [ apply Rle_powerRZ; try apply IZR_lt | simpl in |- * ]; auto with real arith zarith. apply IZR_le; lia. rewrite Rabs_Zabs; try apply IZR_lt; auto with real zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz