Library Flocq.Prop.Div_sqrt_error

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

Remainder of the division and square root are in the FLX format


Require Import Psatz.
Require Import Core Operations Relative Sterbenz.

Section Fprop_divsqrt_error.

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

Variable prec : Z.

Lemma generic_format_plus_prec :
   fexp, ( e, (fexp e e - prec)%Z)
   x y (fx fy: float beta),
  (x = F2R fx)%R (y = F2R fy)%R (Rabs (x+y) < bpow (prec+Fexp fx))%R
  (Rabs (x+y) < bpow (prec+Fexp fy))%R
  generic_format beta fexp (x+y)%R.

Context { prec_gt_0_ : Prec_gt_0 prec }.

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

Variable choice : Z bool.

Remainder of the division in FLX
Theorem div_error_FLX :
   rnd { Zrnd : Valid_rnd rnd } x y,
  format x format y
  format (x - round beta (FLX_exp prec) rnd (x/y) × y)%R.

Remainder of the square in FLX (with p>1) and rounding to nearest
Variable Hp1 : Zlt 1 prec.

Theorem sqrt_error_FLX_N :
   x, format x
  format (x - Rsqr (round beta (FLX_exp prec) (Znearest choice) (sqrt x)))%R.

End Fprop_divsqrt_error.

Section format_REM_aux.

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

Variable fexp : Z Z.
Context { valid_exp : Valid_exp fexp }.
Context { monotone_exp : Monotone_exp fexp }.

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

Notation format := (generic_format beta fexp).

Lemma format_REM_aux:
   x y : R,
  format x format y (0 x)%R (0 < y)%R
  ((0 < x/y < /2)%R rnd (x/y) = 0%Z)
  format (x - IZR (rnd (x/y))×y).

End format_REM_aux.

Section format_REM.

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

Variable fexp : Z Z.
Context { valid_exp : Valid_exp fexp }.
Context { monotone_exp : Monotone_exp fexp }.

Notation format := (generic_format beta fexp).

Theorem format_REM :
   rnd : R Z, Valid_rnd rnd
   x y : R,
  ((Rabs (x/y) < /2)%R rnd (x/y)%R = 0%Z)
  format x format y
  format (x - IZR (rnd (x/y)%R) × y).

Theorem format_REM_ZR:
   x y : R,
  format x format y
  format (x - IZR (Ztrunc (x/y)) × y).

Theorem format_REM_N :
   choice,
   x y : R,
  format x format y
  format (x - IZR (Znearest choice (x/y)) × y).

End format_REM.