proposition: Theorem Veltkamp_tail: forall x p q hx tx:float, (Fbounded b x) -> (Closest b radix (x*((powerRZ radix s)+1))%R p) -> (Closest b radix (x-p)%R q) -> (Closest b radix (q+p)%R hx) -> (Closest b radix (x-hx)%R tx) -> (exists tx':float, (FtoRradix tx'=tx) /\ (hx+tx'=x)%R /\ (Fbounded bt tx') /\ (Fexp (Fnormalize radix b t x) <= Fexp tx')%Z).
proof: Proof. intros. generalize Veltkamp_tail_aux; intros T. elim T with (Fnormalize radix b t x) p q hx tx; auto; clear T. intros v T; elim T; intros H4 T'; elim T'; intros H5 H6; clear T T'. 2: apply FnormalizeCanonic; auto with zarith. 2: unfold FtoRradix; rewrite FnormalizeCorrect; auto with real. 2: unfold FtoRradix; rewrite FnormalizeCorrect; auto with real. 2: unfold FtoRradix; rewrite FnormalizeCorrect; auto with real. exists (Fminus radix (Fnormalize radix b t x) v). split. unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (Closest b radix); auto with zarith. apply ClosestRoundedModeP with t; auto with zarith. split. apply lt_IZR. apply Rle_lt_trans with (1:=H6); rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ. apply Rlt_le_trans with (powerRZ radix s*1)%R; [unfold Rdiv; apply Rmult_lt_compat_l; auto with real zarith| ring_simplify (powerRZ radix s*1)%R; apply Rle_powerRZ; auto with real zarith]. apply powerRZ_lt, IZR_lt; lia. apply Rlt_le_trans with (/1)%R; auto with real. apply IZR_le; lia. rewrite H5; cut (Fbounded b (Fnormalize radix b t x)); [intros T; elim T; auto|apply FnormalizeBounded; auto with zarith]. rewrite Fminus_correct; auto; rewrite FnormalizeCorrect; auto with real. fold FtoRradix; rewrite H4; auto. split. unfold FtoRradix; rewrite Fminus_correct; auto. rewrite FnormalizeCorrect; auto with real. fold FtoRradix; rewrite H4; ring. split. split. apply Z.lt_le_trans with (Zpower_nat radix s). apply lt_IZR. apply Rle_lt_trans with (1:=H6). rewrite Zpower_nat_Z_powerRZ; apply Rlt_le_trans with (powerRZ radix s*1)%R; auto with real. unfold Rdiv; apply Rmult_lt_compat_l; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. apply Rlt_le_trans with (/1)%R; auto with real. apply Zeq_le; apply sym_eq. unfold bt in |- *; 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))))))). 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. rewrite Nat.lt_succ_pred with 0 (Z.abs_nat (Zpower_nat radix (s))); auto with zarith. rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. apply Zpower_NR0; auto with zarith. cut ( 0 < Z.abs_nat (Zpower_nat radix s))%Z; auto with zarith. simpl; rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. apply Zpower_nat_less; lia. apply Zpower_NR0; auto with zarith. rewrite H5; unfold bt; simpl. cut (Fbounded b (Fnormalize radix b t x)); [intros T; elim T; auto|apply FnormalizeBounded; auto with zarith]. rewrite H5; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz