proposition: Theorem Veltkamp: forall x p q hx: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) -> (Rabs (x-hx) <= (powerRZ radix (s+Fexp x)) /2)%R /\ (exists hx':float, (FtoRradix hx'=hx) /\ (Closest b' radix x hx') /\ ((Fnormal radix b x) -> (s+Fexp x <= Fexp hx')%Z)).
proof: Proof. intros. cut (Fcanonic radix b (Fnormalize radix b t x)); [intros C|apply FnormalizeCanonic; auto with zarith]. case C; clear C; intros. generalize VeltkampN; intros T. elim T with radix b s t (Fnormalize radix b t x) p q hx; auto. intros C TT; elim TT; intros v T'; elim T'; intros ; clear T T' TT. rewrite FnormalizeCorrect in H5; auto. rewrite FnormalizeCorrect in C; auto. split. unfold FtoRradix; apply Rle_trans with (1:=C). unfold Rdiv; apply Rmult_le_compat_r; auto with real. apply Rle_powerRZ; try apply IZR_le; auto with real zarith. apply Zplus_le_compat_l. apply FcanonicLeastExp with radix b t; auto with zarith. rewrite FnormalizeCorrect; auto with zarith real. left; auto. elim H5; intros. exists v; split; auto with zarith. split; auto with zarith. intros; replace x with (Fnormalize radix b t x); auto with zarith. rewrite FcanonicFnormalizeEq; auto with zarith. left; auto. rewrite FnormalizeCorrect; auto with real. rewrite FnormalizeCorrect; auto with real. generalize VeltkampS; intros T. elim T with radix b s t (Fnormalize radix b t x) p q hx; auto; clear T. intros C TT; elim TT; intros v T'; elim T'; intros ; clear T' TT. rewrite FnormalizeCorrect in H5; auto. rewrite FnormalizeCorrect in C; auto. split. unfold FtoRradix; apply Rle_trans with (1:=C). unfold Rdiv; apply Rmult_le_compat_r; auto with real. apply Rle_powerRZ; try apply IZR_le; auto with real zarith. apply Zplus_le_compat_l. apply FcanonicLeastExp with radix b t; auto with zarith. rewrite FnormalizeCorrect; auto with zarith real. right; auto. exists v; split; auto with zarith. split; auto with zarith. intros T; absurd (FtoRradix x=(Fnormalize radix b t x))%R. unfold FtoRradix; apply NormalAndSubNormalNotEq with b t; auto with zarith. unfold FtoRradix; rewrite FnormalizeCorrect; auto with real zarith. rewrite FnormalizeCorrect; auto with real. rewrite FnormalizeCorrect; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz