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.