Library Flocq.Prop.Mult_error

This file is part of the Flocq formalization of floating-point arithmetic in Coq: https://flocq.gitlabpages.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.

Error of the multiplication is in the FLX/FLT format

From Coq Require Import ZArith Reals Lia.

Require Import Core Operations Plus_error.

Section Fprop_mult_error.

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

Variable prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.

Notation format := (generic_format beta (FLX_exp prec)).
Notation cexp := (cexp beta (FLX_exp prec)).

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

Auxiliary result that provides the exponent

Lemma mult_error_FLX_aux:
  ∀ x y,
  format x → format y →
  (round beta (FLX_exp prec) rnd (x × y) - (x × y ) ≠ 0)%R →
  ∃ f:float beta ,
    (F2R f = round beta (FLX_exp prec) rnd (x × y) - (x × y ))%R
    ∧ (cexp (F2R f) ≤ Fexp f)%Z
    ∧ (Fexp f = cexp x + cexp y)%Z.

Error of the multiplication in FLX

Theorem mult_error_FLX :
  ∀ x y,
  format x → format y →
  format (round beta (FLX_exp prec) rnd (x × y) - (x × y ))%R.

Lemma mult_bpow_exact_FLX :
  ∀ x e,
  format x →
  format (x × bpow e)%R.

End Fprop_mult_error.

Section Fprop_mult_error_FLT.

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

Variable emin prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.

Notation format := (generic_format beta (FLT_exp emin prec)).
Notation cexp := (cexp beta (FLT_exp emin prec)).

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

Error of the multiplication in FLT with underflow requirements

Theorem mult_error_FLT :
  ∀ x y,
  format x → format y →
  (x × y ≠ 0 → bpow (emin + 2×prec - 1) ≤ Rabs (x × y))%R →
  format (round beta (FLT_exp emin prec) rnd (x × y) - (x × y ))%R.

Lemma F2R_ge: ∀ (y:float beta),
   (F2R y ≠ 0)%R → (bpow (Fexp y) ≤ Rabs (F2R y))%R.

Theorem mult_error_FLT_ge_bpow :
  ∀ x y e,
  format x → format y →
  (bpow (e +2×prec -1) ≤ Rabs (x × y))%R →
  (round beta (FLT_exp emin prec) rnd (x × y) - (x × y ) ≠ 0)%R →
  (bpow e ≤ Rabs (round beta (FLT_exp emin prec) rnd (x × y) - (x × y )))%R.

Lemma mult_bpow_exact_FLT :
  ∀ x e,
  format x →
  (emin + prec - mag beta x ≤ e)%Z →
  format (x × bpow e)%R.

Lemma mult_bpow_pos_exact_FLT :
  ∀ x e,
  format x →
  (0 ≤ e)%Z →
  format (x × bpow e)%R.

End Fprop_mult_error_FLT.