proposition: Theorem ClosestErrorBoundNormal_aux : forall (x : R) (p : float), Closest b radix x p -> Fnormal radix b (Fnormalize radix b precision p) -> (Rabs (x - p) <= Rabs p * (/ 2 * (radix * / Zpos (vNum b))))%R.
proof: Proof. intros x p H H'. apply Rle_trans with (/ 2 * Fulp b radix precision p)%R. replace (Rabs (x - FtoRradix p)) with (/ 2 * (2 * Rabs (x - FtoRradix p)))%R. apply Rmult_le_compat_l; [simpl; auto with real|idtac]. apply ClosestUlp; auto. rewrite <- Rmult_assoc; rewrite Rinv_l; simpl in |- *; auto with real. apply Rle_trans with (/ 2 * (Rabs p * (radix * / Zpos (vNum b))))%R; [ apply Rmult_le_compat_l | right; ring; ring ]. apply Rlt_le; apply Rinv_0_lt_compat; auto with real arith. unfold Fulp in |- *. replace (Fexp (Fnormalize radix b precision p)) with (Fexp (Fnormalize radix b precision p) + precision + - precision)%Z; [ idtac | ring ]. rewrite powerRZ_add; auto with real zarith. 2: apply IZR_neq; lia. apply Rle_trans with (Rabs p * radix * powerRZ radix (- precision))%R; [ apply Rmult_le_compat_r | right ]; auto with real zarith. apply powerRZ_le, IZR_lt; lia. 2: rewrite pGivesBound; simpl in |- *. 2: rewrite powerRZ_Zopp; auto with real zarith. 2: rewrite Zpower_nat_Z_powerRZ; auto with real zarith; ring. 2: apply IZR_neq; lia. replace (FtoRradix p) with (FtoRradix (Fnormalize radix b precision p)); [ idtac | apply (FnormalizeCorrect radix) ]; auto. rewrite <- (Fabs_correct radix); unfold FtoR in |- *; simpl in |- *; auto with arith. rewrite powerRZ_add; auto with real zarith. 2: apply IZR_neq; lia. replace (Z.abs (Fnum (Fnormalize radix b precision p)) * powerRZ radix (Fexp (Fnormalize radix b precision p)) * radix)%R with (powerRZ radix (Fexp (Fnormalize radix b precision p)) * (Z.abs (Fnum (Fnormalize radix b precision p)) * radix))%R; [ idtac | ring ]. apply Rmult_le_compat_l; auto with arith real. apply powerRZ_le, IZR_lt; lia. rewrite <- Zpower_nat_Z_powerRZ; auto with real zarith. rewrite <- mult_IZR; apply IZR_le. rewrite <- pGivesBound; pattern radix at 2 in |- *; rewrite <- (Z.abs_eq radix); auto with zarith. rewrite <- Zabs_Zmult. rewrite Zmult_comm; elim H'; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz