Library Flocq.Prop.Relative

This file is part of the Flocq formalization of floating-point arithmetic in Coq: https://flocq.gitlabpages.inria.fr/
Copyright (C) 2010-2018 Sylvie Boldo
Copyright (C) 2010-2018 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.

Relative error of the roundings


From Coq Require Import ZArith Reals Psatz.

Require Import Core.

Section Fprop_relative.

Variable beta : radix.
Notation bpow e := (bpow beta e).

Section Fprop_relative_generic.

Variable fexp : Z Z.
Context { prop_exp : Valid_exp fexp }.

Section relative_error_conversion.

Variable rnd : R Z.
Context { valid_rnd : Valid_rnd rnd }.

Lemma relative_error_lt_conversion :
   x b, (0 < b)%R
  (x 0 Rabs (round beta fexp rnd x - x) < b × Rabs x)%R
   eps,
  (Rabs eps < b)%R round beta fexp rnd x = (x × (1 + eps))%R.

Lemma relative_error_le_conversion :
   x b, (0 b)%R
  (Rabs (round beta fexp rnd x - x) b × Rabs x)%R
   eps,
  (Rabs eps b)%R round beta fexp rnd x = (x × (1 + eps))%R.

Lemma relative_error_le_conversion_inv :
   x b,
  ( eps,
   (Rabs eps b)%R round beta fexp rnd x = (x × (1 + eps))%R)
  (Rabs (round beta fexp rnd x - x) b × Rabs x)%R.

Lemma relative_error_le_conversion_round_inv :
   x b,
  ( eps,
   (Rabs eps b)%R x = (round beta fexp rnd x × (1 + eps))%R)
  (Rabs (round beta fexp rnd x - x) b × Rabs (round beta fexp rnd x))%R.

End relative_error_conversion.

Variable emin p : Z.
Hypothesis Hmin : k, (emin < k)%Z (p k - fexp k)%Z.

Variable rnd : R Z.
Context { valid_rnd : Valid_rnd rnd }.

Theorem relative_error :
   x,
  (bpow emin Rabs x)%R
  (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) × Rabs x)%R.

1+ε property in any rounding
Theorem relative_error_ex :
   x,
  (bpow emin Rabs x)%R
   eps,
  (Rabs eps < bpow (-p + 1))%R round beta fexp rnd x = (x × (1 + eps))%R.

Theorem relative_error_F2R_emin :
   m, let x := F2R (Float beta m emin) in
  (x 0)%R
  (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) × Rabs x)%R.

Theorem relative_error_F2R_emin_ex :
   m, let x := F2R (Float beta m emin) in
   eps,
  (Rabs eps < bpow (-p + 1))%R round beta fexp rnd x = (x × (1 + eps))%R.

Theorem relative_error_round :
  (0 < p)%Z
   x,
  (bpow emin Rabs x)%R
  (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) × Rabs (round beta fexp rnd x))%R.

Theorem relative_error_round_F2R_emin :
  (0 < p)%Z
   m, let x := F2R (Float beta m emin) in
  (x 0)%R
  (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) × Rabs (round beta fexp rnd x))%R.

Variable choice : Z bool.

Theorem relative_error_N :
   x,
  (bpow emin Rabs x)%R
  (Rabs (round beta fexp (Znearest choice) x - x) /2 × bpow (-p + 1) × Rabs x)%R.

1+ε property in rounding to nearest
Theorem relative_error_N_ex :
   x,
  (bpow emin Rabs x)%R
   eps,
  (Rabs eps /2 × bpow (-p + 1))%R round beta fexp (Znearest choice) x = (x × (1 + eps))%R.

Theorem relative_error_N_F2R_emin :
   m, let x := F2R (Float beta m emin) in
  (Rabs (round beta fexp (Znearest choice) x - x) /2 × bpow (-p + 1) × Rabs x)%R.

Theorem relative_error_N_F2R_emin_ex :
   m, let x := F2R (Float beta m emin) in
   eps,
  (Rabs eps /2 × bpow (-p + 1))%R round beta fexp (Znearest choice) x = (x × (1 + eps))%R.

Theorem relative_error_N_round :
  (0 < p)%Z
   x,
  (bpow emin Rabs x)%R
  (Rabs (round beta fexp (Znearest choice) x - x) /2 × bpow (-p + 1) × Rabs (round beta fexp (Znearest choice) x))%R.

Theorem relative_error_N_round_F2R_emin :
  (0 < p)%Z
   m, let x := F2R (Float beta m emin) in
  (Rabs (round beta fexp (Znearest choice) x - x) /2 × bpow (-p + 1) × Rabs (round beta fexp (Znearest choice) x))%R.

End Fprop_relative_generic.

Section Fprop_relative_FLX.

Variable prec : Z.
Variable Hp : Z.lt 0 prec.

Lemma relative_error_FLX_aux :
   k, (prec k - FLX_exp prec k)%Z.

Variable rnd : R Z.
Context { valid_rnd : Valid_rnd rnd }.

Theorem relative_error_FLX :
   x,
  (x 0)%R
  (Rabs (round beta (FLX_exp prec) rnd x - x) < bpow (-prec + 1) × Rabs x)%R.

1+ε property in any rounding in FLX
Theorem relative_error_FLX_ex :
   x,
   eps,
  (Rabs eps < bpow (-prec + 1))%R round beta (FLX_exp prec) rnd x = (x × (1 + eps))%R.

Theorem relative_error_FLX_round :
   x,
  (x 0)%R
  (Rabs (round beta (FLX_exp prec) rnd x - x) < bpow (-prec + 1) × Rabs (round beta (FLX_exp prec) rnd x))%R.

Variable choice : Z bool.

Theorem relative_error_N_FLX :
   x,
  (Rabs (round beta (FLX_exp prec) (Znearest choice) x - x) /2 × bpow (-prec + 1) × Rabs x)%R.

unit roundoff
Definition u_ro := (/2 × bpow (-prec + 1))%R.

Lemma u_ro_pos : (0 u_ro)%R.

Lemma u_ro_lt_1 : (u_ro < 1)%R.

Lemma u_rod1pu_ro_pos : (0 u_ro / (1 + u_ro))%R.

Lemma u_rod1pu_ro_le_u_ro : (u_ro / (1 + u_ro) u_ro)%R.

Theorem relative_error_N_FLX' :
   x,
  (Rabs (round beta (FLX_exp prec) (Znearest choice) x - x)
    u_ro / (1 + u_ro) × Rabs x)%R.

1+ε property in rounding to nearest in FLX
Theorem relative_error_N_FLX_ex :
   x,
   eps,
  (Rabs eps /2 × bpow (-prec + 1))%R round beta (FLX_exp prec) (Znearest choice) x = (x × (1 + eps))%R.

Theorem relative_error_N_FLX'_ex :
   x,
   eps,
  (Rabs eps u_ro / (1 + u_ro))%R
  round beta (FLX_exp prec) (Znearest choice) x = (x × (1 + eps))%R.

Lemma relative_error_N_round_ex_derive :
   x rx,
  ( eps, (Rabs eps u_ro / (1 + u_ro))%R rx = (x × (1 + eps))%R)
   eps, (Rabs eps u_ro)%R x = (rx × (1 + eps))%R.

Theorem relative_error_N_FLX_round_ex :
   x,
   eps,
  (Rabs eps u_ro)%R
  x = (round beta (FLX_exp prec) (Znearest choice) x × (1 + eps))%R.

Theorem relative_error_N_FLX_round :
   x,
  (Rabs (round beta (FLX_exp prec) (Znearest choice) x - x) /2 × bpow (-prec + 1) × Rabs(round beta (FLX_exp prec) (Znearest choice) x))%R.

End Fprop_relative_FLX.

Section Fprop_relative_FLT.

Variable emin prec : Z.
Variable Hp : Z.lt 0 prec.

Lemma relative_error_FLT_aux :
   k, (emin + prec - 1 < k)%Z (prec k - FLT_exp emin prec k)%Z.

Variable rnd : R Z.
Context { valid_rnd : Valid_rnd rnd }.

Theorem relative_error_FLT :
   x,
  (bpow (emin + prec - 1) Rabs x)%R
  (Rabs (round beta (FLT_exp emin prec) rnd x - x) < bpow (-prec + 1) × Rabs x)%R.

Theorem relative_error_FLT_F2R_emin :
   m, let x := F2R (Float beta m emin) in
  (x 0)%R
  (Rabs (round beta (FLT_exp emin prec) rnd x - x) < bpow (-prec + 1) × Rabs x)%R.

Theorem relative_error_FLT_F2R_emin_ex :
   m, let x := F2R (Float beta m emin) in
   eps,
  (Rabs eps < bpow (-prec + 1))%R round beta (FLT_exp emin prec) rnd x = (x × (1 + eps))%R.

1+ε property in any rounding in FLT
Theorem relative_error_FLT_ex :
   x,
  (bpow (emin + prec - 1) Rabs x)%R
   eps,
  (Rabs eps < bpow (-prec + 1))%R round beta (FLT_exp emin prec) rnd x = (x × (1 + eps))%R.

Variable choice : Z bool.

Theorem relative_error_N_FLT :
   x,
  (bpow (emin + prec - 1) Rabs x)%R
  (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) /2 × bpow (-prec + 1) × Rabs x)%R.

1+ε property in rounding to nearest in FLT
Theorem relative_error_N_FLT_ex :
   x,
  (bpow (emin + prec - 1) Rabs x)%R
   eps,
  (Rabs eps /2 × bpow (-prec + 1))%R round beta (FLT_exp emin prec) (Znearest choice) x = (x × (1 + eps))%R.

Theorem relative_error_N_FLT_round :
   x,
  (bpow (emin + prec - 1) Rabs x)%R
  (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) /2 × bpow (-prec + 1) × Rabs (round beta (FLT_exp emin prec) (Znearest choice) x))%R.

Theorem relative_error_N_FLT_F2R_emin :
   m, let x := F2R (Float beta m emin) in
  (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) /2 × bpow (-prec + 1) × Rabs x)%R.

Theorem relative_error_N_FLT_F2R_emin_ex :
   m, let x := F2R (Float beta m emin) in
   eps,
  (Rabs eps /2 × bpow (-prec + 1))%R round beta (FLT_exp emin prec) (Znearest choice) x = (x × (1 + eps))%R.

Theorem relative_error_N_FLT_round_F2R_emin :
   m, let x := F2R (Float beta m emin) in
  (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) /2 × bpow (-prec + 1) × Rabs (round beta (FLT_exp emin prec) (Znearest choice) x))%R.

Lemma error_N_FLT_aux :
   x,
  (0 < x)%R
   eps, eta,
  (Rabs eps /2 × bpow (-prec + 1))%R
  (Rabs eta /2 × bpow (emin))%R
  (eps×eta=0)%R
  round beta (FLT_exp emin prec) (Znearest choice) x = (x × (1 + eps) + eta)%R.

Theorem relative_error_N_FLT'_ex :
   x,
   eps eta : R,
  (Rabs eps u_ro prec / (1 + u_ro prec))%R
  (Rabs eta /2 × bpow emin)%R
  (eps × eta = 0)%R
  round beta (FLT_exp emin prec) (Znearest choice) x
  = (x × (1 + eps) + eta)%R.

Theorem relative_error_N_FLT'_ex_separate :
   x,
   x' : R,
  round beta (FLT_exp emin prec) (Znearest choice) x'
  = round beta (FLT_exp emin prec) (Znearest choice) x
  ( eta, Rabs eta /2 × bpow emin x' = x + eta)%R
  ( eps, Rabs eps u_ro prec / (1 + u_ro prec)
               round beta (FLT_exp emin prec) (Znearest choice) x'
               = x' × (1 + eps))%R.

End Fprop_relative_FLT.

Theorem error_N_FLT :
   (emin prec : Z), (0 < prec)%Z
   (choice : Z bool),
   (x : R),
   eps eta : R,
  (Rabs eps /2 × bpow (-prec + 1))%R
  (Rabs eta /2 × bpow emin)%R
  (eps × eta = 0)%R
  (round beta (FLT_exp emin prec) (Znearest choice) x
   = x × (1 + eps) + eta)%R.

End Fprop_relative.