Library Flocq.Prop.Fprop_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-2013 Sylvie Boldo
Copyright (C) 2010-2013 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.
Copyright (C) 2010-2013 Guillaume Melquiond
Remainder of the division and square root are in the FLX format
Require Import Fcore.
Require Import Fcalc_ops.
Require Import Fprop_relative.
Section Fprop_divsqrt_error.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable prec : Z.
Theorem 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.
Theorem ex_Fexp_canonic: ∀ fexp, ∀ x, generic_format beta fexp x
→ ∃ fx:float beta, (x=F2R fx)%R ∧ Fexp fx = canonic_exp beta fexp x.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Notation format := (generic_format beta (FLX_exp prec)).
Notation cexp := (canonic_exp beta (FLX_exp prec)).
Variable choice : Z → bool.
Require Import Fcalc_ops.
Require Import Fprop_relative.
Section Fprop_divsqrt_error.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable prec : Z.
Theorem 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.
Theorem ex_Fexp_canonic: ∀ fexp, ∀ x, generic_format beta fexp x
→ ∃ fx:float beta, (x=F2R fx)%R ∧ Fexp fx = canonic_exp beta fexp x.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Notation format := (generic_format beta (FLX_exp prec)).
Notation cexp := (canonic_exp 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.
∀ 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