proposition: Theorem Veltkamp_tail2: forall x p q hx tx:float, (radix=2)%Z -> (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 bt2 tx') /\ (Fexp (Fnormalize radix b t x) <= Fexp tx')%Z).
proof: Proof. intros x p q hx tx I; 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. generalize FboundedMbound2; intros T. elim T with bt2 radix (s-1) (Fexp (Fminus radix (Fnormalize radix b t x) v)) (Fnum (Fminus radix (Fnormalize radix b t x) v)); auto with zarith. clear T; intros c T'; elim T'; intros H7 T''; elim T''; intros H8 H9; clear T' T''. cut (FtoRradix c=x-hx)%R;[intros J|idtac]. exists c; split. unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (Closest b radix); auto with zarith. apply ClosestRoundedModeP with t; auto with zarith. elim H7; intros. split. apply Z.lt_le_trans with (1:=H10); rewrite pGivesBound. unfold bt2; simpl; auto with zarith. apply Z.le_trans with (Zpower_nat radix (s-1)); auto with zarith. apply Zeq_le. 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. rewrite Nat.lt_succ_pred with 0 (Z.abs_nat (Zpower_nat radix (s-1))); auto with zarith. rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. apply Zpower_NR0; lia. cut ( 0 < Z.abs_nat (Zpower_nat radix (s-1)))%Z; auto with zarith. simpl; rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. apply Zpower_nat_less; lia. apply Zpower_NR0; lia. apply Zpower_nat_monotone_le; lia. generalize H11; unfold bt2; simpl; auto. fold FtoRradix; rewrite J; auto with real. split; [rewrite J; ring|split; auto]. rewrite <- H5; auto. apply trans_eq with (FtoRradix (Fminus radix (Fnormalize radix b t x) v)). unfold FtoRradix; rewrite H8; unfold FtoR; simpl; ring. unfold FtoRradix; rewrite Fminus_correct; auto; rewrite FnormalizeCorrect; auto; fold FtoRradix; rewrite H4; ring. unfold bt2; simpl. 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. rewrite Nat.lt_succ_pred with 0 (Z.abs_nat (Zpower_nat radix (s-1))); auto with zarith. rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. apply Zpower_NR0; lia. cut ( 0 < Z.abs_nat (Zpower_nat radix (s-1)))%Z; auto with zarith. simpl; rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. apply Zpower_nat_less; lia. apply Zpower_NR0; lia. apply le_IZR; clear T. apply Rle_trans with (1:=H6); rewrite Zpower_nat_Z_powerRZ. rewrite inj_minus1; auto with zarith. unfold Zminus; rewrite powerRZ_add. rewrite I; simpl; right; field. apply IZR_neq; lia. clear T; rewrite H5; unfold bt; simpl. cut (Fbounded b (Fnormalize radix b t x)); [intros T; elim T; auto|apply FnormalizeBounded; auto with zarith]. Qed.
imports: Reals ZArith List PeanoNat Psatz