proposition: Theorem Veltkamp_tail_aux: forall x p q hx tx:float, (Fcanonic radix 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 v:float, (FtoRradix v=hx) /\ (Fexp (Fminus radix x v) = Fexp x) /\ (Z.abs (Fnum (Fminus radix x v)) <= (powerRZ radix s)/2)%R).
proof: Proof. intros. cut (Zpos (vNum b') = Zpower_nat radix (t - s));[intros I|idtac]. 2: unfold b'; apply p'GivesBound; auto with zarith. generalize Veltkamp; intros W. elim W with radix b s t x p q hx; auto. 2: apply FcanonicBound with radix; auto. intros C TT; elim TT; intros v' W'; elim W'; fold FtoRradix; fold b'; intros W1 T; elim T; intros W2 W3; clear W W' TT T. cut (exists v:float, (Fcanonic radix b' v) /\ (FtoRradix v=v')). 2: exists (Fnormalize radix b' (t-s) v'); unfold b'; elim W2; intros; split. 2:apply FnormalizeCanonic; auto with zarith. 2: simpl. 2: rewrite <- p'GivesBound with radix b s t; simpl; auto with zarith. 2: rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto with zarith. 2: unfold FtoRradix; apply FnormalizeCorrect; auto. intros W; elim W; intros v W'; elim W'; intros; clear W W'. exists v; split. rewrite H5; auto. cut (Rabs (x-v) <= (powerRZ radix (s+Fexp x)) /2)%R;[intros T1|idtac]. cut (Fexp (Fminus radix x v) = Fexp x);[intros T2|idtac]. split; auto. apply Rmult_le_reg_l with (powerRZ radix (Fexp x)); auto with real zarith. apply powerRZ_lt, IZR_lt; lia. apply Rle_trans with (Rabs (x-v))%R;[right|idtac]. unfold FtoRradix; rewrite <- Fminus_correct; auto; rewrite <- Fabs_correct; auto. rewrite <- T2; unfold FtoR, Fabs; simpl; ring. apply Rle_trans with (1:= T1); rewrite powerRZ_add. unfold Rdiv; right; ring. apply IZR_neq; lia. unfold Fminus; simpl. apply Z.min_l. case H; intros. apply Z.le_trans with (Fexp (Float (nNormMin radix (t-s)) (Fexp x))); [simpl; auto with zarith|idtac]. apply Fcanonic_Rle_Zle with radix b' (t-s); auto with zarith. apply FcanonicNnormMin; auto with zarith. cut (Fbounded b x); [intros T; elim T; intros; unfold b'; simpl; auto with zarith| apply FcanonicBound with radix; auto]. rewrite Rabs_right. apply RoundAbsMonotonel with b' (t-s) (Closest b' radix) x; auto with zarith. apply ClosestRoundedModeP with (t-s); auto with zarith. apply FcanonicBound with radix; auto. apply FcanonicNnormMin; auto with zarith. elim H6; intros T2 T3; elim T2; intros; unfold b'; simpl; auto. apply ClosestCompatible with (1:=W2); auto. apply FcanonicBound with radix; auto. unfold FtoRradix; rewrite <- Fabs_correct; auto. unfold FtoR; simpl. apply Rmult_le_compat_r; auto with real zarith. apply powerRZ_le, IZR_lt; lia. elim H6; intros; apply IZR_le. apply Zmult_le_reg_r with radix; auto with zarith. apply Z.le_trans with (Z.abs (radix * Fnum x))%Z; [idtac|rewrite Zabs_Zmult; rewrite Z.abs_eq; auto with zarith]. apply Z.le_trans with (2:=H8). unfold nNormMin; rewrite pGivesBound. apply Z.le_trans with (Zpower_nat radix (t-s)); auto with zarith. pattern (t-s) at 2; replace (t-s) with (pred (t-s)+1); auto with zarith. rewrite Zpower_nat_is_exp; unfold Zpower_nat; simpl; auto with zarith. ring_simplify (radix*1)%Z; auto with zarith. apply Zpower_nat_monotone_le; auto with zarith. apply Rle_ge; apply LeFnumZERO; simpl; unfold nNormMin; auto with real zarith. apply Zpower_NR0; auto with zarith. cut (Fbounded b' v);[intros T; elim T; unfold b'; simpl; intros| apply FcanonicBound with radix; auto]. elim H6; auto with zarith. rewrite H5; rewrite W1;auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz