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-2011 Sylvie Boldo
Copyright (C) 2010-2011 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-2011 Sylvie Boldo
Copyright (C) 2010-2011 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.
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:
forall fexp, (forall e, (fexp e <= e - prec)%Z) ->
forall 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: forall fexp, forall x, generic_format beta fexp x
-> exists 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:
forall fexp, (forall e, (fexp e <= e - prec)%Z) ->
forall 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: forall fexp, forall x, generic_format beta fexp x
-> exists 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 :
forall rnd { Zrnd : Valid_rnd rnd } x y,
format x -> format y ->
format (x - round beta (FLX_exp prec) rnd (x/y) * y)%R.
forall 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