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-2013 Sylvie Boldo
Copyright (C) 2010-2013 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.
Copyright (C) 2010-2013 Guillaume Melquiond
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 :
∀ x, ulp (- x) = ulp x.
Theorem ulp_abs :
∀ x, ulp (Rabs x) = ulp x.
Theorem ulp_le_id:
∀ x,
(0 < x)%R →
F x →
(ulp x ≤ x)%R.
Theorem ulp_le_abs:
∀ x,
(x ≠ 0)%R →
F x →
(ulp x ≤ Rabs x)%R.
Theorem ulp_DN_UP :
∀ x, ¬ F x →
round beta fexp Zceil x = (round beta fexp Zfloor x + ulp x)%R.
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 :
∀ x, ulp (- x) = ulp x.
Theorem ulp_abs :
∀ x, ulp (Rabs x) = ulp x.
Theorem ulp_le_id:
∀ x,
(0 < x)%R →
F x →
(ulp x ≤ x)%R.
Theorem ulp_le_abs:
∀ x,
(x ≠ 0)%R →
F x →
(ulp x ≤ Rabs x)%R.
Theorem ulp_DN_UP :
∀ 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 :
∀ x e, (0 < x)%R → F x →
(x < bpow e)%R →
(x + ulp x ≤ bpow e)%R.
Theorem ln_beta_succ :
∀ x, (0 < x)%R → F x →
∀ eps, (0 ≤ eps < ulp x)%R →
ln_beta beta (x + eps) = ln_beta beta x :> Z.
Theorem round_DN_succ :
∀ x, (0 < x)%R → F x →
∀ eps, (0 ≤ eps < ulp x)%R →
round beta fexp Zfloor (x + eps) = x.
Theorem generic_format_succ :
∀ x, (0 < x)%R → F x →
F (x + ulp x).
Theorem round_UP_succ :
∀ x, (0 < x)%R → F x →
∀ eps, (0 < eps ≤ ulp x)%R →
round beta fexp Zceil (x + eps) = (x + ulp x)%R.
Theorem succ_le_lt:
∀ x y,
F x → F y →
(0 < x < y)%R →
(x + ulp x ≤ y)%R.
∀ x e, (0 < x)%R → F x →
(x < bpow e)%R →
(x + ulp x ≤ bpow e)%R.
Theorem ln_beta_succ :
∀ x, (0 < x)%R → F x →
∀ eps, (0 ≤ eps < ulp x)%R →
ln_beta beta (x + eps) = ln_beta beta x :> Z.
Theorem round_DN_succ :
∀ x, (0 < x)%R → F x →
∀ eps, (0 ≤ eps < ulp x)%R →
round beta fexp Zfloor (x + eps) = x.
Theorem generic_format_succ :
∀ x, (0 < x)%R → F x →
F (x + ulp x).
Theorem round_UP_succ :
∀ x, (0 < x)%R → F x →
∀ eps, (0 < eps ≤ ulp x)%R →
round beta fexp Zceil (x + eps) = (x + ulp x)%R.
Theorem succ_le_lt:
∀ 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 :
∀ rnd { Zrnd : Valid_rnd rnd } x,
(Rabs (round beta fexp rnd x - x) < ulp x)%R.
Theorem ulp_half_error :
∀ choice x,
(Rabs (round beta fexp (Znearest choice) x - x) ≤ /2 × ulp x)%R.
Theorem ulp_le :
∀ { Hm : Monotone_exp fexp },
∀ x y: R,
(0 < x)%R → (x ≤ y)%R →
(ulp x ≤ ulp y)%R.
Theorem ulp_bpow :
∀ e, ulp (bpow e) = bpow (fexp (e + 1)).
Theorem ulp_DN :
∀ x,
(0 < round beta fexp Zfloor x)%R →
ulp (round beta fexp Zfloor x) = ulp x.
Theorem ulp_error_f :
∀ { 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 :
∀ { Hm : Monotone_exp fexp },
∀ 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.
∀ rnd { Zrnd : Valid_rnd rnd } x,
(Rabs (round beta fexp rnd x - x) < ulp x)%R.
Theorem ulp_half_error :
∀ choice x,
(Rabs (round beta fexp (Znearest choice) x - x) ≤ /2 × ulp x)%R.
Theorem ulp_le :
∀ { Hm : Monotone_exp fexp },
∀ x y: R,
(0 < x)%R → (x ≤ y)%R →
(ulp x ≤ ulp y)%R.
Theorem ulp_bpow :
∀ e, ulp (bpow e) = bpow (fexp (e + 1)).
Theorem ulp_DN :
∀ x,
(0 < round beta fexp Zfloor x)%R →
ulp (round beta fexp Zfloor x) = ulp x.
Theorem ulp_error_f :
∀ { 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 :
∀ { Hm : Monotone_exp fexp },
∀ 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 :
∀ x e, F x →
x ≠ ulp x →
(bpow e < x)%R →
(bpow e ≤ x - ulp x)%R.
Lemma generic_format_pred_1:
∀ x, (0 < x)%R → F x →
x ≠ bpow (ln_beta beta x - 1) →
F (x - ulp x).
Lemma generic_format_pred_2 :
∀ 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 :
∀ x, (0 < x)%R → F x →
F (pred x).
Theorem generic_format_plus_ulp :
∀ { monotone_exp : Monotone_exp fexp },
∀ x, (x ≠ 0)%R →
F x → F (x + ulp x).
Theorem generic_format_minus_ulp :
∀ { monotone_exp : Monotone_exp fexp },
∀ x, (x ≠ 0)%R →
F x → F (x - ulp x).
Lemma pred_plus_ulp_1 :
∀ 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 :
∀ 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 :
∀ x, (0 < x)%R → F x →
(pred x ≠ 0)%R →
(pred x + ulp (pred x) = x)%R.
Theorem pred_lt_id :
∀ x,
(pred x < x)%R.
Theorem pred_ge_0 :
∀ x,
(0 < x)%R → F x → (0 ≤ pred x)%R.
Theorem round_UP_pred :
∀ x, (0 < pred x)%R → F x →
∀ eps, (0 < eps ≤ ulp (pred x) )%R →
round beta fexp Zceil (pred x + eps) = x.
Theorem round_DN_pred :
∀ x, (0 < pred x)%R → F x →
∀ eps, (0 < eps ≤ ulp (pred x))%R →
round beta fexp Zfloor (x - eps) = pred x.
Lemma le_pred_lt_aux :
∀ x y,
F x → F y →
(0 < x < y)%R →
(x ≤ pred y)%R.
Theorem le_pred_lt :
∀ x y,
F x → F y →
(0 < y)%R →
(x < y)%R →
(x ≤ pred y)%R.
Theorem pred_succ : ∀ { monotone_exp : Monotone_exp fexp },
∀ x, F x → (0 < x)%R → pred (x + ulp x)=x.
Theorem lt_UP_le_DN :
∀ x y, F y →
(y < round beta fexp Zceil x → y ≤ round beta fexp Zfloor x)%R.
Theorem pred_UP_le_DN :
∀ x, (0 < round beta fexp Zceil x)%R →
(pred (round beta fexp Zceil x) ≤ round beta fexp Zfloor x)%R.
Theorem pred_UP_eq_DN :
∀ x, (0 < round beta fexp Zceil x)%R → ¬ F x →
(pred (round beta fexp Zceil x) = round beta fexp Zfloor x)%R.
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 :
∀ x e, F x →
x ≠ ulp x →
(bpow e < x)%R →
(bpow e ≤ x - ulp x)%R.
Lemma generic_format_pred_1:
∀ x, (0 < x)%R → F x →
x ≠ bpow (ln_beta beta x - 1) →
F (x - ulp x).
Lemma generic_format_pred_2 :
∀ 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 :
∀ x, (0 < x)%R → F x →
F (pred x).
Theorem generic_format_plus_ulp :
∀ { monotone_exp : Monotone_exp fexp },
∀ x, (x ≠ 0)%R →
F x → F (x + ulp x).
Theorem generic_format_minus_ulp :
∀ { monotone_exp : Monotone_exp fexp },
∀ x, (x ≠ 0)%R →
F x → F (x - ulp x).
Lemma pred_plus_ulp_1 :
∀ 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 :
∀ 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 :
∀ x, (0 < x)%R → F x →
(pred x ≠ 0)%R →
(pred x + ulp (pred x) = x)%R.
Theorem pred_lt_id :
∀ x,
(pred x < x)%R.
Theorem pred_ge_0 :
∀ x,
(0 < x)%R → F x → (0 ≤ pred x)%R.
Theorem round_UP_pred :
∀ x, (0 < pred x)%R → F x →
∀ eps, (0 < eps ≤ ulp (pred x) )%R →
round beta fexp Zceil (pred x + eps) = x.
Theorem round_DN_pred :
∀ x, (0 < pred x)%R → F x →
∀ eps, (0 < eps ≤ ulp (pred x))%R →
round beta fexp Zfloor (x - eps) = pred x.
Lemma le_pred_lt_aux :
∀ x y,
F x → F y →
(0 < x < y)%R →
(x ≤ pred y)%R.
Theorem le_pred_lt :
∀ x y,
F x → F y →
(0 < y)%R →
(x < y)%R →
(x ≤ pred y)%R.
Theorem pred_succ : ∀ { monotone_exp : Monotone_exp fexp },
∀ x, F x → (0 < x)%R → pred (x + ulp x)=x.
Theorem lt_UP_le_DN :
∀ x y, F y →
(y < round beta fexp Zceil x → y ≤ round beta fexp Zfloor x)%R.
Theorem pred_UP_le_DN :
∀ x, (0 < round beta fexp Zceil x)%R →
(pred (round beta fexp Zceil x) ≤ round beta fexp Zfloor x)%R.
Theorem pred_UP_eq_DN :
∀ x, (0 < round beta fexp Zceil x)%R → ¬ F x →
(pred (round beta fexp Zceil x) = round beta fexp Zfloor x)%R.
Properties of rounding to nearest and ulp
Theorem rnd_N_le_half_an_ulp: ∀ choice u v,
F u → (0 < u)%R → (v < u + (ulp u)/2)%R
→ (round beta fexp (Znearest choice) v ≤ u)%R.
Theorem rnd_N_ge_half_an_ulp_pred: ∀ choice u v,
F u → (0 < pred u)%R → (u - (ulp (pred u))/2 < v)%R
→ (u ≤ round beta fexp (Znearest choice) v)%R.
Theorem rnd_N_ge_half_an_ulp: ∀ choice u v,
F u → (0 < u)%R → (u ≠ bpow (ln_beta beta u - 1))%R
→ (u - (ulp u)/2 < v)%R
→ (u ≤ round beta fexp (Znearest choice) v)%R.
Lemma round_N_DN_betw: ∀ choice x d u,
Rnd_DN_pt (generic_format beta fexp) x d →
Rnd_UP_pt (generic_format beta fexp) x u →
(d≤x<(d+u)/2)%R →
round beta fexp (Znearest choice) x = d.
Lemma round_N_UP_betw: ∀ choice x d u,
Rnd_DN_pt (generic_format beta fexp) x d →
Rnd_UP_pt (generic_format beta fexp) x u →
((d+u)/2 < x ≤ u)%R →
round beta fexp (Znearest choice) x = u.
End Fcore_ulp.