Library Flocq.Core.Fcore_ulp

This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2010-2011 Sylvie Boldo
Copyright (C) 2010-2011 Guillaume Melquiond

This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Unit in the Last Place: our definition using fexp and its properties, successor and predecessor

Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_generic_fmt.
Require Import Fcore_float_prop.

Section Fcore_ulp.

Variable beta : radix.

Notation bpow e := (bpow beta e).

Variable fexp : Z -> Z.

Context { valid_exp : Valid_exp fexp }.

Definition ulp x := bpow (canonic_exp beta fexp x).

Notation F := (generic_format beta fexp).

Theorem ulp_opp :
  forall x, ulp (- x) = ulp x.

Theorem ulp_abs :
  forall x, ulp (Rabs x) = ulp x.

Theorem ulp_le_id:
  forall x,
    (0 < x)%R ->
    F x ->
    (ulp x <= x)%R.

Theorem ulp_le_abs:
  forall x,
    (x <> 0)%R ->
    F x ->
    (ulp x <= Rabs x)%R.

Theorem ulp_DN_UP :
  forall x, ~ F x ->
  round beta fexp Zceil x = (round beta fexp Zfloor x + ulp x)%R.

The successor of x is x + ulp x
Theorem succ_le_bpow :
  forall x e, (0 < x)%R -> F x ->
  (x < bpow e)%R ->
  (x + ulp x <= bpow e)%R.

Theorem ln_beta_succ :
  forall x, (0 < x)%R -> F x ->
  forall eps, (0 <= eps < ulp x)%R ->
  ln_beta beta (x + eps) = ln_beta beta x :> Z.

Theorem round_DN_succ :
  forall x, (0 < x)%R -> F x ->
  forall eps, (0 <= eps < ulp x)%R ->
  round beta fexp Zfloor (x + eps) = x.

Theorem generic_format_succ :
  forall x, (0 < x)%R -> F x ->
  F (x + ulp x).

Theorem round_UP_succ :
  forall x, (0 < x)%R -> F x ->
  forall eps, (0 < eps <= ulp x)%R ->
  round beta fexp Zceil (x + eps) = (x + ulp x)%R.

Theorem succ_le_lt:
  forall x y,
  F x -> F y ->
  (0 < x < y)%R ->
  (x + ulp x <= y)%R.

Error of a rounding, expressed in number of ulps
Theorem ulp_error :
  forall rnd { Zrnd : Valid_rnd rnd } x,
  (Rabs (round beta fexp rnd x - x) < ulp x)%R.

Theorem ulp_half_error :
  forall choice x,
  (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * ulp x)%R.

Theorem ulp_le :
  forall { Hm : Monotone_exp fexp },
  forall x y: R,
  (0 < x)%R -> (x <= y)%R ->
  (ulp x <= ulp y)%R.

Theorem ulp_bpow :
  forall e, ulp (bpow e) = bpow (fexp (e + 1)).

Theorem ulp_DN :
  forall x,
  (0 < round beta fexp Zfloor x)%R ->
  ulp (round beta fexp Zfloor x) = ulp x.

Theorem ulp_error_f :
  forall { Hm : Monotone_exp fexp } rnd { Zrnd : Valid_rnd rnd } x,
  (round beta fexp rnd x <> 0)%R ->
  (Rabs (round beta fexp rnd x - x) < ulp (round beta fexp rnd x))%R.

Theorem ulp_half_error_f :
  forall { Hm : Monotone_exp fexp },
  forall choice x,
  (round beta fexp (Znearest choice) x <> 0)%R ->
  (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * ulp (round beta fexp (Znearest choice) x))%R.

Predecessor
Definition pred x :=
  if Req_bool x (bpow (ln_beta beta x - 1)) then
    (x - bpow (fexp (ln_beta beta x - 1)))%R
  else
    (x - ulp x)%R.

Theorem pred_ge_bpow :
  forall x e, F x ->
  x <> ulp x ->
  (bpow e < x)%R ->
  (bpow e <= x - ulp x)%R.

Lemma generic_format_pred_1:
  forall x, (0 < x)%R -> F x ->
  x <> bpow (ln_beta beta x - 1) ->
  F (x - ulp x).

Lemma generic_format_pred_2 :
  forall x, (0 < x)%R -> F x ->
  let e := ln_beta_val beta x (ln_beta beta x) in
  x = bpow (e - 1) ->
  F (x - bpow (fexp (e - 1))).

Theorem generic_format_pred :
  forall x, (0 < x)%R -> F x ->
  F (pred x).

Lemma pred_plus_ulp_1 :
  forall x, (0 < x)%R -> F x ->
  x <> bpow (ln_beta beta x - 1) ->
  ((x - ulp x) + ulp (x-ulp x) = x)%R.

Lemma pred_plus_ulp_2 :
  forall x, (0 < x)%R -> F x ->
  let e := ln_beta_val beta x (ln_beta beta x) in
  x = bpow (e - 1) ->
  (x - bpow (fexp (e-1)) <> 0)%R ->
  ((x - bpow (fexp (e-1))) + ulp (x - bpow (fexp (e-1))) = x)%R.

Theorem pred_plus_ulp :
  forall x, (0 < x)%R -> F x ->
  (pred x <> 0)%R ->
  (pred x + ulp (pred x) = x)%R.

Theorem pred_lt_id :
  forall x,
  (pred x < x)%R.

Theorem pred_ge_0 :
  forall x,
  (0 < x)%R -> F x -> (0 <= pred x)%R.

Theorem round_UP_pred :
  forall x, (0 < pred x)%R -> F x ->
  forall eps, (0 < eps <= ulp (pred x) )%R ->
  round beta fexp Zceil (pred x + eps) = x.

Theorem round_DN_pred :
  forall x, (0 < pred x)%R -> F x ->
  forall eps, (0 < eps <= ulp (pred x))%R ->
  round beta fexp Zfloor (x - eps) = pred x.

Lemma le_pred_lt_aux :
  forall x y,
  F x -> F y ->
  (0 < x < y)%R ->
  (x <= pred y)%R.

Theorem le_pred_lt :
  forall x y,
  F x -> F y ->
  (0 < y)%R ->
  (x < y)%R ->
  (x <= pred y)%R.

End Fcore_ulp.