proposition: Theorem ImplyClosest: (Rabs(z-f) <= (powerRZ radix e)/2)%R -> Closest b radix z f.
proof: Proof. intros; apply ClosestSuccPred; auto. apply Rle_trans with (1:=H). apply Rle_trans with (powerRZ radix e - (powerRZ radix e)/2)%R. right; field; auto with real. apply Rle_trans with (Rabs (f - FSucc b radix p f) - Rabs(z-f))%R. unfold Rminus; apply Rplus_le_compat. rewrite <- Rabs_Ropp. replace (- (f + - FSucc b radix p f))%R with (FSucc b radix p f - f)%R;[idtac|ring]. unfold FtoRradix; rewrite <- Fminus_correct; auto;rewrite FSuccDiffPos; auto with real zarith. unfold FtoR; simpl; ring_simplify (1 * powerRZ radix (Fexp f))%R; rewrite Rabs_right. apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. replace e with (Fexp (Float (nNormMin radix p) e)); auto. apply Fcanonic_Rle_Zle with radix b p; auto with real zarith. apply FcanonicNnormMin; auto with zarith. apply Rle_trans with (powerRZ radix (e + p - 1))%R;[right|fold FtoRradix]. unfold nNormMin, FtoR; simpl;rewrite Zpower_nat_Z_powerRZ. rewrite <- powerRZ_add; auto with real zarith. rewrite Rabs_right. replace (pred p+e)%Z with (e+p-1)%Z; auto with real zarith. rewrite inj_pred; unfold Z.pred; auto with zarith arith. apply Rle_ge, powerRZ_le, IZR_lt; lia. apply IZR_neq; lia. rewrite Rabs_right; auto. apply Rle_ge; apply Rle_trans with (2:=fGe); auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rle_ge, powerRZ_le, IZR_lt; lia. apply Rle_trans with (2:=fGe); auto with real zarith. apply powerRZ_le, IZR_lt; lia. auto with real. rewrite <- Rabs_Ropp with (z-f)%R. apply Rle_trans with (Rabs ((f - FSucc b radix p f) - (-(z - f))))%R. apply Rabs_triang_inv. ring_simplify ((f - FSucc b radix p f - - (z - f)))%R; auto with real. right; unfold Rminus; auto with real. case fGe; intros. cut ((powerRZ radix (e + p - 1) <= FPred b radix p f))%R;[intros|idtac]. apply Rle_trans with (1:=H). apply Rle_trans with (powerRZ radix e - (powerRZ radix e)/2)%R. right; field; auto with real. apply Rle_trans with (Rabs (f - FPred b radix p f) - Rabs(z-f))%R. unfold Rminus; apply Rplus_le_compat. replace ( (f + - FPred b radix p f))%R with (FSucc b radix p (FPred b radix p f) - (FPred b radix p f))%R;[idtac|ring_simplify]. unfold FtoRradix; rewrite <- Fminus_correct; auto;rewrite FSuccDiffPos; auto with real zarith. unfold FtoR; simpl; ring_simplify (1 * powerRZ radix (Fexp (FPred b radix p f)))%R; rewrite Rabs_right. apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. replace e with (Fexp (Float (nNormMin radix p) e)); auto. apply Fcanonic_Rle_Zle with radix b p; auto with real zarith. apply FcanonicNnormMin; auto with zarith. apply FPredCanonic; auto with zarith. apply Rle_trans with (powerRZ radix (e + p - 1))%R;[right|fold FtoRradix]. unfold nNormMin, FtoR; simpl;rewrite Zpower_nat_Z_powerRZ. rewrite <- powerRZ_add; auto with real zarith. rewrite Rabs_right. replace (pred p+e)%Z with (e+p-1)%Z; auto with real zarith. rewrite inj_pred; unfold Z.pred; auto with zarith arith. apply Rle_ge; apply powerRZ_le, IZR_lt; lia. apply IZR_neq; lia. rewrite Rabs_right; auto. apply Rle_ge; apply Rle_trans with (2:=H1); auto with real zarith. apply powerRZ_le, IZR_lt; lia. apply Rle_ge; apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (2:=H1); auto with real zarith. apply powerRZ_le, IZR_lt; lia. rewrite FSucPred; auto with zarith. ring. fold Rminus; auto with real. rewrite <- Rabs_Ropp with (z-f)%R. apply Rle_trans with (Rabs ((f - FPred b radix p f) - (-(z - f))))%R. apply Rabs_triang_inv. ring_simplify ((f - FPred b radix p f - - (z - f)))%R. right; unfold Rminus; auto with real. cut ((powerRZ radix (e + p - 1)= (Float (nNormMin radix p) e)))%R. intros T; rewrite T. unfold FtoRradix; apply FPredProp; auto with zarith. apply FcanonicNnormMin; auto with zarith. fold FtoRradix; rewrite <- T; auto. unfold nNormMin, FtoRradix, FtoR; simpl;rewrite Zpower_nat_Z_powerRZ. rewrite <- powerRZ_add; auto with real zarith. replace (pred p+e)%Z with (e+p-1)%Z; try easy. lia. apply IZR_neq; lia. cut (FPred b radix p f < f)%R; [intros|unfold FtoRradix; apply FPredLt; auto with zarith]. rewrite Rabs_right. rewrite Rabs_right. unfold Rminus;auto with real zarith. apply Rle_ge; apply Rle_trans with (z-z)%R; auto with real. right; ring. apply Rle_trans with (z-f)%R; unfold Rminus; auto with real. rewrite <- H0; auto with real. apply Rle_ge; rewrite <- H0; apply Rle_trans with (z-z)%R; unfold Rminus; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz