Library Flocq.Core.Fcore_ulp

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

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.

Definition and basic properties about the minimal exponent, when it exists

Lemma Z_le_dec_aux: ∀ x y : Z, (x ≤ y)%Z ∨ ¬ (x ≤ y)%Z.

negligible_exp is either none (as in FLX) or Some n such that n <= fexp n.

Definition negligible_exp: option Z :=
  match (LPO_Z _ (fun z ⇒ Z_le_dec_aux z (fexp z))) with
   | inleft N ⇒ Some (proj1_sig N)
   | inright _ ⇒ None
end.

Inductive negligible_exp_prop: option Z → Prop :=
  | negligible_None: (∀ n, (fexp n < n)%Z) → negligible_exp_prop None
  | negligible_Some: ∀ n, (n ≤ fexp n)%Z → negligible_exp_prop (Some n).

Lemma negligible_exp_spec: negligible_exp_prop negligible_exp.

Lemma negligible_exp_spec': (negligible_exp = None ∧ ∀ n, (fexp n < n)%Z)
           ∨ ∃ n, (negligible_exp = Some n ∧ (n ≤ fexp n)%Z).

Context { valid_exp : Valid_exp fexp }.

Lemma fexp_negligible_exp_eq: ∀ n m, (n ≤ fexp n)%Z → (m ≤ fexp m)%Z → fexp n = fexp m.

Definition and basic properties about the ulp Now includes a nice ulp(0): ulp(0) is now 0 when there is no minimal exponent, such as in FLX, and beta^(fexp n) when there is a n such that n <= fexp n. For instance, the value of ulp(O) is then beta^emin in FIX and FLT. The main lemma to use is ulp_neq_0 that is equivalent to the previous "unfold ulp" provided the value is not zero.

Definition ulp x := match Req_bool x 0 with
  | true ⇒ match negligible_exp with
            | Some n ⇒ bpow (fexp n)
            | None ⇒ 0%R
            end
  | false ⇒ bpow (canonic_exp beta fexp x)
end.

Lemma ulp_neq_0 : ∀ x:R, (x ≠ 0)%R → 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_ge_0:
  ∀ x, (0 ≤ ulp x)%R.

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 round_UP_DN_ulp :
  ∀ x, ¬ F x →
  round beta fexp Zceil x = (round beta fexp Zfloor x + ulp x)%R.

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

Lemma generic_format_ulp_0:
  F (ulp 0).

Lemma generic_format_bpow_ge_ulp_0: ∀ e,
    (ulp 0 ≤ bpow e)%R → F (bpow e).

The three following properties are equivalent: Exp_not_FTZ ; forall x, F (ulp x) ; forall x, ulp 0 <= ulp x

Lemma generic_format_ulp: Exp_not_FTZ fexp →
  ∀ x, F (ulp x).

Lemma not_FTZ_generic_format_ulp:
   (∀ x, F (ulp x)) → Exp_not_FTZ fexp.

Lemma ulp_ge_ulp_0: Exp_not_FTZ fexp →
  ∀ x, (ulp 0 ≤ ulp x)%R.

Lemma not_FTZ_ulp_ge_ulp_0:
   (∀ x, (ulp 0 ≤ ulp x)%R) → Exp_not_FTZ fexp.

Theorem ulp_le_pos :
  ∀ { Hm : Monotone_exp fexp },
  ∀ x y: R,
  (0 ≤ x)%R → (x ≤ y)%R →
  (ulp x ≤ ulp y)%R.

Theorem ulp_le :
  ∀ { Hm : Monotone_exp fexp },
  ∀ x y: R,
  (Rabs x ≤ Rabs y)%R →
  (ulp x ≤ ulp y)%R.

Definition and properties of pred and succ

Definition pred_pos 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.

Definition succ x :=
   if (Rle_bool 0 x) then
          (x +ulp x)%R
   else
     (- pred_pos (-x))%R.

Definition pred x := (- succ (-x))%R.

Theorem pred_eq_pos:
  ∀ x, (0 ≤ x)%R → (pred x = pred_pos x)%R.

Theorem succ_eq_pos:
  ∀ x, (0 ≤ x)%R → (succ x = x + ulp x)%R.

Lemma pred_eq_opp_succ_opp: ∀ x, pred x = (- succ (-x))%R.

Lemma succ_eq_opp_pred_opp: ∀ x, succ x = (- pred (-x))%R.

Lemma succ_opp: ∀ x, (succ (-x) = - pred x)%R.

Lemma pred_opp: ∀ x, (pred (-x) = - succ x)%R.

pred and succ are in the format

Theorem id_m_ulp_ge_bpow :
  ∀ x e, F x →
  x ≠ ulp x →
  (bpow e < x)%R →
  (bpow e ≤ x - ulp x)%R.

Theorem id_p_ulp_le_bpow :
  ∀ x e, (0 < x)%R → F x →
  (x < bpow e)%R →
  (x + ulp x ≤ bpow e)%R.

Lemma generic_format_pred_aux1:
  ∀ x, (0 < x)%R → F x →
  x ≠ bpow (ln_beta beta x - 1) →
  F (x - ulp x).

Lemma generic_format_pred_aux2 :
  ∀ 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_succ_aux1 :
  ∀ x, (0 < x)%R → F x →
  F (x + ulp x).

Theorem generic_format_pred_pos :
  ∀ x, F x → (0 < x)%R →
  F (pred_pos x).

Theorem generic_format_succ :
  ∀ x, F x →
  F (succ x).

Theorem generic_format_pred :
  ∀ x, F x →
  F (pred x).

Theorem pred_pos_lt_id :
  ∀ x, (x ≠ 0)%R →
  (pred_pos x < x)%R.

Theorem succ_gt_id :
  ∀ x, (x ≠ 0)%R →
  (x < succ x)%R.

Theorem pred_lt_id :
  ∀ x, (x ≠ 0)%R →
  (pred x < x)%R.

Theorem succ_ge_id :
  ∀ x, (x ≤ succ x)%R.

Theorem pred_le_id :
  ∀ x, (pred x ≤ x)%R.

Theorem pred_pos_ge_0 :
  ∀ x,
  (0 < x)%R → F x → (0 ≤ pred_pos x)%R.

Theorem pred_ge_0 :
  ∀ x,
  (0 < x)%R → F x → (0 ≤ pred x)%R.

Lemma pred_pos_plus_ulp_aux1 :
  ∀ x, (0 < x)%R → F x →
  x ≠ bpow (ln_beta beta x - 1) →
  ((x - ulp x ) + ulp (x -ulp x) = x)%R.

Lemma pred_pos_plus_ulp_aux2 :
  ∀ 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.

Lemma pred_pos_plus_ulp_aux3 :
  ∀ 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 →
  (ulp 0 = x)%R.

The following one is false for x = 0 in FTZ

Theorem pred_pos_plus_ulp :
∀ x, (0 < x)%R → F x →
(pred_pos x + ulp (pred_pos x) = x)%R.

Rounding x + small epsilon

Theorem ln_beta_plus_eps:
  ∀ 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_plus_eps_pos:
  ∀ x, (0 ≤ x)%R → F x →
  ∀ eps, (0 ≤ eps < ulp x)%R →
  round beta fexp Zfloor (x + eps) = x.

Theorem round_UP_plus_eps_pos :
  ∀ x, (0 ≤ x)%R → F x →
  ∀ eps, (0 < eps ≤ ulp x)%R →
  round beta fexp Zceil (x + eps) = (x + ulp x)%R.

Theorem round_UP_pred_plus_eps_pos :
  ∀ x, (0 < x)%R → F x →
  ∀ eps, (0 < eps ≤ ulp (pred x) )%R →
  round beta fexp Zceil (pred x + eps) = x.

Theorem round_DN_minus_eps_pos :
  ∀ x, (0 < x)%R → F x →
  ∀ eps, (0 < eps ≤ ulp (pred x))%R →
  round beta fexp Zfloor (x - eps) = pred x.

Theorem round_DN_plus_eps:
  ∀ x, F x →
  ∀ eps, (0 ≤ eps < if (Rle_bool 0 x) then (ulp x)
                                     else (ulp (pred (-x))))%R →
  round beta fexp Zfloor (x + eps) = x.

Theorem round_UP_plus_eps :
  ∀ x, F x →
  ∀ eps, (0 < eps ≤ if (Rle_bool 0 x) then (ulp x)
                                     else (ulp (pred (-x))))%R →
  round beta fexp Zceil (x + eps) = (succ x)%R.

Lemma le_pred_pos_lt :
  ∀ x y,
  F x → F y →
  (0 ≤ x < y)%R →
  (x ≤ pred_pos y)%R.

Theorem succ_le_lt_aux:
  ∀ x y,
  F x → F y →
  (0 ≤ x)%R → (x < y)%R →
  (succ x ≤ y)%R.

Theorem succ_le_lt:
  ∀ x y,
  F x → F y →
  (x < y)%R →
  (succ x ≤ y)%R.

Theorem le_pred_lt :
  ∀ x y,
  F x → F y →
  (x < y)%R →
  (x ≤ pred y)%R.

Theorem lt_succ_le:
  ∀ x y,
  F x → F y → (y ≠ 0)%R →
  (x ≤ y)%R →
  (x < succ y)%R.

Theorem succ_pred_aux : ∀ x, F x → (0 < x)%R → succ (pred x)=x.

Theorem pred_succ_aux_0 : (pred (succ 0)=0)%R.

Theorem pred_succ_aux : ∀ x, F x → (0 < x)%R → pred (succ x)=x.

Theorem succ_pred : ∀ x, F x → succ (pred x)=x.

Theorem pred_succ : ∀ x, F x → pred (succ x)=x.

Theorem round_UP_pred_plus_eps :
  ∀ x, F x →
  ∀ eps, (0 < eps ≤ if (Rle_bool x 0) then (ulp x)
                                     else (ulp (pred x)))%R →
  round beta fexp Zceil (pred x + eps) = x.

Theorem round_DN_minus_eps:
  ∀ x, F x →
  ∀ eps, (0 < eps ≤ if (Rle_bool x 0) then (ulp x)
                                     else (ulp (pred x)))%R →
  round beta fexp Zfloor (x - eps) = pred x.

Error of a rounding, expressed in number of ulps false for x=0 in the FLX format

Theorem error_lt_ulp :
  ∀ rnd { Zrnd : Valid_rnd rnd } x,
   (x ≠ 0)%R →
  (Rabs (round beta fexp rnd x - x) < ulp x)%R.

Theorem error_le_ulp :
  ∀ rnd { Zrnd : Valid_rnd rnd } x,
  (Rabs (round beta fexp rnd x - x) ≤ ulp x)%R.

Theorem error_le_half_ulp :
  ∀ choice x,
  (Rabs (round beta fexp (Znearest choice) x - x) ≤ /2 × ulp x)%R.

Theorem ulp_DN :
  ∀ x,
  (0 < round beta fexp Zfloor x)%R →
  ulp (round beta fexp Zfloor x) = ulp x.

Theorem round_neq_0_negligible_exp:
    negligible_exp =None → ∀ rnd { Zrnd : Valid_rnd rnd } x,
   (x ≠ 0)%R → (round beta fexp rnd x ≠ 0)%R.

allows rnd x to be 0

Theorem error_lt_ulp_round :
  ∀ { Hm : Monotone_exp fexp } rnd { Zrnd : Valid_rnd rnd } x,
  ( x ≠ 0)%R →
  (Rabs (round beta fexp rnd x - x) < ulp (round beta fexp rnd x))%R.

allows both x and rnd x to be 0

Theorem error_le_half_ulp_round :
  ∀ { Hm : Monotone_exp fexp },
  ∀ choice x,
  (Rabs (round beta fexp (Znearest choice) x - x) ≤ /2 × ulp (round beta fexp (Znearest choice) x))%R.

Theorem pred_le: ∀ x y,
   F x → F y → (x ≤ y)%R → (pred x ≤ pred y)%R.

Theorem succ_le: ∀ x y,
   F x → F y → (x ≤ y)%R → (succ x ≤ succ y)%R.

Theorem pred_le_inv: ∀ x y, F x → F y
   → (pred x ≤ pred y)%R → (x ≤ y)%R.

Theorem succ_le_inv: ∀ x y, F x → F y
   → (succ x ≤ succ y)%R → (x ≤ y)%R.

Theorem le_round_DN_lt_UP :
  ∀ x y, F y →
  (y < round beta fexp Zceil x → y ≤ round beta fexp Zfloor x)%R.

Theorem round_UP_le_gt_DN :
  ∀ x y, F y →
   (round beta fexp Zfloor x < y → round beta fexp Zceil x ≤ y)%R.

Theorem pred_UP_le_DN :
  ∀ x, (pred (round beta fexp Zceil x) ≤ round beta fexp Zfloor x)%R.

Theorem pred_UP_eq_DN :
  ∀ x, ¬ F x →
  (pred (round beta fexp Zceil x) = round beta fexp Zfloor x)%R.

Theorem succ_DN_eq_UP :
  ∀ x, ¬ F x →
  (succ (round beta fexp Zfloor x) = round beta fexp Zceil x)%R.

Theorem round_DN_eq_betw: ∀ x d, F d
     → (d ≤ x < succ d)%R
        → round beta fexp Zfloor x = d.

Theorem round_UP_eq_betw: ∀ x u, F u
    → (pred u < x ≤ u)%R
    → round beta fexp Zceil x = u.

Properties of rounding to nearest and ulp

Theorem round_N_le_midp: ∀ choice u v,
  F u → (v < (u + succ u )/2)%R
      → (round beta fexp (Znearest choice) v ≤ u)%R.

Theorem round_N_ge_midp: ∀ choice u v,
F u → ((u + pred u )/2 < v)%R
      → (u ≤ round beta fexp (Znearest choice) v)%R.

Lemma round_N_eq_DN: ∀ choice x,
       let d:=round beta fexp Zfloor x in
       let u:=round beta fexp Zceil x in
      (x <(d +u )/2)%R →
     round beta fexp (Znearest choice) x = d.

Lemma round_N_eq_DN_pt: ∀ choice x d u,
      Rnd_DN_pt F x d → Rnd_UP_pt F x u →
      (x <(d +u )/2)%R →
     round beta fexp (Znearest choice) x = d.

Lemma round_N_eq_UP: ∀ choice x,
      let d:=round beta fexp Zfloor x in
      let u:=round beta fexp Zceil x in
     ((d +u )/2 < x)%R →
     round beta fexp (Znearest choice) x = u.

Lemma round_N_eq_UP_pt: ∀ choice x d u,
      Rnd_DN_pt F x d → Rnd_UP_pt F x u →
      ((d +u )/2 < x)%R →
     round beta fexp (Znearest choice) x = u.

End Fcore_ulp.