proposition: Lemma VeltkampS: forall x p q hx:float, Fsubnormal 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) -> (Rabs (x-hx) <= (powerRZ radix (s+Fexp x)) /2)%R /\ (exists hx':float, (FtoRradix hx'=hx) /\ (Closest b' radix x hx')).
proof: Proof. intros x p q hx Sx pDef qDef hxDef. case (Req_dec 0%R x); intros Y. assert ((exists hx' : float, FtoRradix hx' = hx /\ Closest b' radix x hx' /\ (s + Fexp x <= Fexp hx')%Z /\ (FtoRradix hx'=0)%R)). exists (Fzero (s+Fexp x)). cut (Fbounded b (Fzero (s+Fexp x)));[intros KK|idtac]. split. cut (FtoR radix p=(Fzero (-(dExp b))))%R; [intros I1|idtac]. cut (FtoR radix q=(Fzero (-(dExp b))))%R; [intros I2|idtac]. unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (Closest b radix); auto with zarith. apply ClosestRoundedModeP with t; auto with zarith. replace (FtoR radix (Fzero (s+Fexp x))) with (q+p)%R; auto. unfold FtoRradix; rewrite I1; rewrite I2; unfold FtoRradix. repeat rewrite FzeroisZero. unfold Fzero, FtoR; simpl; ring. apply sym_eq; unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (Closest b radix); auto with zarith. apply ClosestRoundedModeP with t; auto with zarith. apply FboundedFzero. replace (FtoR radix (Fzero (- dExp b))) with (x -p)%R; auto. rewrite <- Y; unfold FtoRradix; rewrite I1; unfold FtoRradix. repeat rewrite FzeroisZero; ring. apply sym_eq; unfold FtoRradix; apply RoundedModeProjectorIdemEq with b t (Closest b radix); auto with zarith. apply ClosestRoundedModeP with t; auto with zarith. apply FboundedFzero. replace (FtoR radix (Fzero (- dExp b))) with (x * (powerRZ radix s + 1))%R; auto. rewrite <- Y; rewrite FzeroisZero; ring. split. rewrite <- Y; replace 0%R with (FtoR radix (Fzero (s + Fexp x))). apply RoundedModeProjectorIdem with (P:=(Closest b' radix)) (b:=b'). apply ClosestRoundedModeP with (t-s); auto with zarith. unfold b'; apply p'GivesBound; auto. unfold Fzero; split; auto with zarith. unfold b'; simpl; auto with zarith. elim Sx; intros T1 T2; elim T1; auto with zarith. unfold Fzero, FtoR; simpl; ring. split;[unfold Fzero; simpl; auto with zarith|idtac]. unfold Fzero, FtoRradix, FtoR; simpl; ring. unfold Fzero; split; auto with zarith. elim Sx; intros T1 T2; elim T1; simpl; auto with zarith. elim H; intros f T; elim T; intros H1 T'; elim T'; intros H2 T''; elim T''; intros; clear T T' T''. split. rewrite <- Y; rewrite <- H1; rewrite H3; ring_simplify (0-0)%R; rewrite Rabs_R0. unfold Rdiv; apply Rmult_le_pos; auto with real zarith. apply powerRZ_le, IZR_lt; lia. exists f; split; auto; split; auto. lapply (bimplybplusNorm x);[intros T|elim Sx; auto]. lapply T; clear T; [intros T; elim T; intros x' T'; elim T'; intros x'Eq Nx'; clear T T'|auto with real]. generalize VeltkampN; intros. elim H with radix (plusExp b) s t x' p q hx; auto with zarith; clear H. intros C T; elim T; intros f H; elim H; intros; clear H T. elim H1; clear H1; intros H1 C'. cut (Closest (plusExp b') radix x f);[clear H1; intros H1|idtac]. case (Zle_or_lt (-(dExp b)) (Fexp f)); intros H2. cut (Fbounded b' f);[intros H3|idtac]. split. rewrite <- x'Eq; 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 (plusExp b) t; auto with zarith. elim Sx; intros T1 T2; elim T1; intros. split; unfold plusExp; auto with zarith. cut (forall (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z). intros T; simpl; rewrite <- T; lia. intros;unfold Nplus. case x0; auto with zarith. left; auto. exists f; split;auto with real. apply Closestbplusb; auto. split; [idtac|unfold b'; simpl; auto]. elim H1; intros J1 J2; elim J1; intros; auto with zarith. split. rewrite <- x'Eq; 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 (plusExp b) t; auto with zarith. elim Sx; intros T1 T2; elim T1; intros. split; unfold plusExp; auto with zarith. cut (forall (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z). intros T; simpl; rewrite <- T; lia. intros;unfold Nplus. case x0; auto with zarith. left; auto. generalize RoundedModeRep; intros T. elim T with (plusExp b') radix (t-s) (Closest (plusExp b') radix) x f; auto with zarith. clear T;intros m H3. cut (Fbounded b' (Float m (Fexp x)));[intros H4|idtac]. exists (Float m (Fexp x)); split. unfold FtoRradix; rewrite <- H3; rewrite H0; auto with real. apply Closestbplusb; auto. apply (ClosestCompatible (plusExp b') radix x x f (Float m (Fexp x))); auto with real zarith. elim H4; intros; split; auto with zarith. cut (forall (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z). intros T; simpl; rewrite <- T. apply Z.le_trans with (-(dExp b))%Z; try easy; lia. intros;unfold Nplus. case x0; auto with zarith. unfold b'; simpl; auto with zarith. split. apply Z.le_lt_trans with (Z.abs (Fnum f)). apply Z.le_trans with ((Z.abs m)*1)%Z; auto with zarith. simpl; auto with zarith. apply Z.le_trans with ((Z.abs m)*(Zpower_nat radix (Z.abs_nat (Fexp x-Fexp f))))%Z. apply Zmult_le_compat_l; auto with zarith. apply Zpower_NR1; auto with zarith. replace (Fnum f) with (m*Zpower_nat radix (Z.abs_nat (Fexp x - Fexp f)))%Z. rewrite Zabs_Zmult; rewrite (Z.abs_eq (Zpower_nat radix (Z.abs_nat (Fexp x - Fexp f)))); auto with zarith. apply Zpower_NR0; lia. apply eq_IZR; rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ. apply Rmult_eq_reg_l with (powerRZ radix (Fexp f)); auto with real zarith. apply trans_eq with (FtoR radix f);[rewrite H3|unfold FtoR; ring]. unfold FtoR; simpl. apply trans_eq with (m*(powerRZ radix (Fexp f)* powerRZ radix (Z.abs_nat (Fexp x - Fexp f))))%R;[ring|idtac]. rewrite <- powerRZ_add. replace (Fexp f + Z.abs_nat (Fexp x - Fexp f))%Z with (Fexp x);[ring|idtac]. rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. elim Sx; intros J1 J2; elim J1; intros; auto with zarith. apply IZR_neq; lia. apply Rgt_not_eq, powerRZ_lt, IZR_lt; lia. elim H1; intros J1 J2; elim J1; unfold plusExp; simpl; auto with zarith. elim Sx; intros J1 J2; elim J1; intros ; unfold b'; simpl; auto. unfold plusExp; simpl. rewrite <- p'GivesBound with radix b s t; lia. apply ClosestRoundedModeP with (t-s); auto with zarith. unfold plusExp; simpl. rewrite <- p'GivesBound with radix b s t; lia. rewrite <- x'Eq; unfold FtoRradix;auto with zarith. replace (FtoR radix x' * (powerRZ radix s + 1))%R with (FtoRradix (Fplus radix x (Float (Fnum x) (s+Fexp x)%Z))). apply Closestbbplus with t; auto with zarith. unfold Fplus; simpl;apply Zmin_Zle. elim Sx; intros J1 J2; elim J1; auto. elim Sx; intros J1 J2; elim J1; auto with zarith. replace (FtoRradix (Fplus radix x (Float (Fnum x) (s + Fexp x)))) with (x * (powerRZ radix s + 1))%R; auto with real. unfold FtoRradix; rewrite Fplus_correct; auto. unfold FtoR; simpl; rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; ring. fold FtoRradix; rewrite x'Eq; unfold FtoRradix; rewrite Fplus_correct; auto. unfold FtoR; simpl; rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; ring. unfold FtoRradix in x'Eq; rewrite x'Eq; rewrite <- Fminus_correct; auto. apply Closestbbplus with t; auto with zarith. unfold Fplus; simpl;apply Zmin_Zle. elim Sx; intros J1 J2; elim J1; auto. elim pDef; intros J1 J2; elim J1; auto with zarith. replace (FtoRradix (Fminus radix x p)) with (x -p)%R; auto with real. unfold FtoRradix; rewrite Fminus_correct; auto with real. rewrite <- Fplus_correct; auto. apply Closestbbplus with t; auto with zarith. unfold Fplus; simpl;apply Zmin_Zle. elim qDef; intros J1 J2; elim J1; auto. elim pDef; intros J1 J2; elim J1; auto with zarith. replace (FtoRradix (Fplus radix q p)) with (q +p)%R; auto with real. unfold FtoRradix; rewrite Fplus_correct; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz