proposition: Theorem Boundedx2y2: (radix=2)%Z \/ (Nat.Even t) -> (exists x':float, (FtoRradix x'=tx*ty)%R /\ (Fbounded b x') /\ (Fexp x+Fexp y <= Fexp x')%Z).
proof: Proof. intros H; case H; clear H; intros H. generalize SLe; intros Sle; generalize SGe; intros Sge. elim Veltkamp_tail2 with radix b s t x p q hx tx; auto. 2: elim Cx; auto. intros x2 T; elim T; intros G1 T'; elim T'; intros G2 T''; elim T''; intros G3 G4; clear T T' T''. elim Veltkamp_tail2 with radix b s t y p' q' hy ty; auto. 2: elim Cy; auto. intros y2 T; elim T; intros J1 T'; elim T'; intros J2 T''; elim T''; intros J3 J4; clear T T' T''. exists (Fmult x2 y2). split;[unfold FtoRradix; rewrite Fmult_correct; auto with real zarith|idtac]. rewrite G1; rewrite J1; ring. split. unfold Fmult; split; simpl; auto with zarith. rewrite Zabs_Zmult. elim J3; elim G3; replace (Zpos (vNum (Bound (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (s - 1))))) (dExp b))))%Z with (Zpower_nat radix (s - 1)); intros. apply Z.lt_le_trans with (Zpower_nat radix (s - 1)*Zpower_nat radix (s - 1))%Z. case (Zle_lt_or_eq 0%Z (Z.abs (Fnum x2))). auto with zarith. intros I; apply Z.lt_le_trans with (Z.abs (Fnum x2) * Zpower_nat radix (s-1))%Z; auto with zarith. apply Zmult_lt_compat_l; auto with zarith. intros I; rewrite <- I. rewrite Zmult_0_l; apply Z.mul_pos_pos; apply Zpower_nat_less; lia. rewrite pGivesBound; rewrite <- Zpower_nat_is_exp; auto with zarith. apply Zpower_nat_monotone_le; auto with zarith. generalize s2Le; auto with zarith. apply sym_eq; unfold vNum in |- *. apply trans_eq with (Z_of_nat (nat_of_P (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (s-1))))))). unfold Z_of_nat in |- *; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with zarith. rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with arith zarith. cut (Z.abs (Zpower_nat radix (s-1)) = Zpower_nat radix (s-1)). intros HA; pattern (Zpower_nat radix (s-1)) at 2 in |- *; rewrite <- HA. rewrite Zabs_absolu. rewrite (Nat.lt_succ_pred 0 (Z.abs_nat (Zpower_nat radix (s-1)))); auto with arith zarith. apply lt_Zlt_inv; simpl in |- *; auto with zarith arith. rewrite <- Zabs_absolu; rewrite HA; auto with arith zarith. apply Zpower_nat_less; lia. apply Z.abs_eq; auto with arith zarith. apply Zpower_NR0; lia. apply Z.le_trans with (Fexp (Fnormalize radix b t x)+Fexp (Fnormalize radix b t y))%Z; auto with zarith. rewrite FcanonicFnormalizeEq; auto with zarith. rewrite FcanonicFnormalizeEq; auto with zarith. left; auto. left; auto. apply Z.le_trans with (Fexp (Fnormalize radix b t x)+Fexp (Fnormalize radix b t y))%Z; simpl; auto with zarith. rewrite FcanonicFnormalizeEq; auto with zarith. rewrite FcanonicFnormalizeEq; auto with zarith. left; auto. left; auto. generalize SLe; intros Sle; generalize SGe; intros Sge. elim Veltkamp_tail with radix b s t x p q hx tx; auto. 2: elim Cx; auto. intros x2 T; elim T; intros G1 T'; elim T'; intros G2 T''; elim T''; intros G3 G4; clear T T' T''. elim Veltkamp_tail with radix b s t y p' q' hy ty; auto. 2: elim Cy; auto. intros y2 T; elim T; intros J1 T'; elim T'; intros J2 T''; elim T''; intros J3 J4; clear T T' T''. exists (Fmult x2 y2). split;[unfold FtoRradix; rewrite Fmult_correct; auto with real zarith|idtac]. rewrite G1; rewrite J1; auto with real. split. unfold Fmult; split; simpl; auto with zarith. rewrite Zabs_Zmult. elim J3; elim G3; replace (Zpos (vNum (Bound (P_of_succ_nat (pred (Z.abs_nat (Zpower_nat radix (s))))) (dExp b))))%Z with (Zpower_nat radix (s)); intros. apply Z.lt_le_trans with (Zpower_nat radix s*Zpower_nat radix s)%Z. case (Zle_lt_or_eq 0%Z (Z.abs (Fnum x2))). auto with zarith. intros I; apply Z.lt_le_trans with (Z.abs (Fnum x2) * Zpower_nat radix s)%Z; auto with zarith. apply Zmult_lt_compat_l; auto with zarith. intros I; rewrite <- I. rewrite Zmult_0_l; apply Z.mul_pos_pos; apply Zpower_nat_less; lia. rewrite <- Zpower_nat_is_exp; rewrite pGivesBound; auto with zarith. apply Zpower_nat_monotone_le; auto with zarith. assert (2*s <= t)%Z; auto with zarith. unfold s. rewrite inj_minus1 by (generalize (Nat.lt_div2 t); auto with zarith). assert (t <= 2*(Nat.div2 t))%Z; auto with zarith. apply Z.le_trans with (Nat.double (Nat.div2 t)). 2: unfold Nat.double; rewrite inj_plus; auto with zarith. rewrite <- Even_double; auto with zarith. apply sym_eq; apply p''GivesBound; auto. apply Z.le_trans with (Fexp (Fnormalize radix b t x)+Fexp (Fnormalize radix b t y))%Z; auto with zarith. rewrite FcanonicFnormalizeEq; auto with zarith. rewrite FcanonicFnormalizeEq; auto with zarith. left; auto. left; auto. apply Z.le_trans with (Fexp (Fnormalize radix b t x)+Fexp (Fnormalize radix b t y))%Z; auto with zarith. rewrite FcanonicFnormalizeEq; auto with zarith. rewrite FcanonicFnormalizeEq; auto with zarith. left; auto. left; auto. simpl; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz