<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> <html xmlns="http://www.w3.org/1999/xhtml"> <head> <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> <link href="coqdoc.css" rel="stylesheet" type="text/css" /> <title>Flocq.Prop.Fprop_plus_error</title> </head> <body> <div id="page"> <div id="header"> </div> <div id="main"> <h1 class="libtitle">Library Flocq.Prop.Fprop_plus_error</h1> <div class="code"> </div> <div class="doc"> This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ <div class="paragraph"> </div> Copyright (C) 2010-2013 Sylvie Boldo <br /> Copyright (C) 2010-2013 Guillaume Melquiond <div class="paragraph"> </div> 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. <div class="paragraph"> </div> 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. <div class="paragraph"> </div> <a name="lab20"></a><h1 class="section">Error of the rounded-to-nearest addition is representable.</h1> </div> <div class="code"> <br/> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Core.Fcore_Raux.html#"><span class="id" title="library">Fcore_Raux</span></a>.<br/> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Core.Fcore_defs.html#"><span class="id" title="library">Fcore_defs</span></a>.<br/> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Core.Fcore_float_prop.html#"><span class="id" title="library">Fcore_float_prop</span></a>.<br/> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#"><span class="id" title="library">Fcore_generic_fmt</span></a>.<br/> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Core.Fcore_FIX.html#"><span class="id" title="library">Fcore_FIX</span></a>.<br/> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Core.Fcore_FLX.html#"><span class="id" title="library">Fcore_FLX</span></a>.<br/> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Core.Fcore_FLT.html#"><span class="id" title="library">Fcore_FLT</span></a>.<br/> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#"><span class="id" title="library">Fcalc_ops</span></a>.<br/> <br/> <span class="id" title="keyword">Section</span> <a name="Fprop_plus_error"><span class="id" title="section">Fprop_plus_error</span></a>.<br/> <br/> <span class="id" title="keyword">Variable</span> <span class="id" title="keyword">beta</span> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#radix"><span class="id" title="record">radix</span></a>.<br/> <span class="id" title="keyword">Notation</span> <a name="bpow"><span class="id" title="abbreviation">bpow</span></a> <span class="id" title="var">e</span> := (<a class="idref" href="Flocq.Core.Fcore_Raux.html#bpow"><span class="id" title="definition">bpow</span></a> <span class="id" title="keyword">beta</span> <span class="id" title="var">e</span>).<br/> <br/> <span class="id" title="keyword">Variable</span> <a name="Fprop_plus_error.fexp"><span class="id" title="variable">fexp</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/> <span class="id" title="keyword">Context</span> { <span class="id" title="var">valid_exp</span> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Valid_exp"><span class="id" title="class">Valid_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_error.fexp"><span class="id" title="variable">fexp</span></a> }.<br/> <br/> <span class="id" title="keyword">Section</span> <a name="Fprop_plus_error.round_repr_same_exp"><span class="id" title="section">round_repr_same_exp</span></a>.<br/> <br/> <span class="id" title="keyword">Variable</span> <a name="Fprop_plus_error.round_repr_same_exp.rnd"><span class="id" title="variable">rnd</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/> <span class="id" title="keyword">Context</span> { <span class="id" title="var">valid_rnd</span> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Valid_rnd"><span class="id" title="class">Valid_rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_error.round_repr_same_exp.rnd"><span class="id" title="variable">rnd</span></a> }.<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="round_repr_same_exp"><span class="id" title="lemma">round_repr_same_exp</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">m</span> <span class="id" title="var">e</span>,<br/> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">m'</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_error.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_error.round_repr_same_exp.rnd"><span class="id" title="variable">rnd</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#e"><span class="id" title="variable">e</span></a>)) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#m'"><span class="id" title="variable">m'</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#e"><span class="id" title="variable">e</span></a>).<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_error.round_repr_same_exp"><span class="id" title="section">round_repr_same_exp</span></a>.<br/> <br/> <span class="id" title="keyword">Context</span> { <span class="id" title="var">monotone_exp</span> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Monotone_exp"><span class="id" title="class">Monotone_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_error.fexp"><span class="id" title="variable">fexp</span></a> }.<br/> <span class="id" title="keyword">Notation</span> <a name="format"><span class="id" title="abbreviation">format</span></a> := (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#generic_format"><span class="id" title="definition">generic_format</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_error.fexp"><span class="id" title="variable">fexp</span></a>).<br/> <br/> <span class="id" title="keyword">Variable</span> <a name="Fprop_plus_error.choice"><span class="id" title="variable">choice</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/> <br/> <span class="id" title="keyword">Lemma</span> <a name="plus_error_aux"><span class="id" title="lemma">plus_error_aux</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>,<br/> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#canonic_exp"><span class="id" title="definition">canonic_exp</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_error.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#canonic_exp"><span class="id" title="definition">canonic_exp</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_error.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#format"><span class="id" title="abbreviation">format</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#format"><span class="id" title="abbreviation">format</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#format"><span class="id" title="abbreviation">format</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_error.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_error.choice"><span class="id" title="variable">choice</span></a>) (<a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">R</span>.<br/> <br/> </div> <div class="doc"> Error of the addition </div> <div class="code"> <span class="id" title="keyword">Theorem</span> <a name="plus_error"><span class="id" title="lemma">plus_error</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>,<br/> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#format"><span class="id" title="abbreviation">format</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#format"><span class="id" title="abbreviation">format</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#format"><span class="id" title="abbreviation">format</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_error.fexp"><span class="id" title="variable">fexp</span></a> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Znearest"><span class="id" title="definition">Znearest</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_error.choice"><span class="id" title="variable">choice</span></a>) (<a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">-</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0f8d5ec6876eafaec2dca3581c24e3a0"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">R</span>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_error"><span class="id" title="section">Fprop_plus_error</span></a>.<br/> <br/> <span class="id" title="keyword">Section</span> <a name="Fprop_plus_zero"><span class="id" title="section">Fprop_plus_zero</span></a>.<br/> <br/> <span class="id" title="keyword">Variable</span> <span class="id" title="keyword">beta</span> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#radix"><span class="id" title="record">radix</span></a>.<br/> <span class="id" title="keyword">Notation</span> <a name="bpow"><span class="id" title="abbreviation">bpow</span></a> <span class="id" title="var">e</span> := (<a class="idref" href="Flocq.Core.Fcore_Raux.html#bpow"><span class="id" title="definition">bpow</span></a> <span class="id" title="keyword">beta</span> <span class="id" title="var">e</span>).<br/> <br/> <span class="id" title="keyword">Variable</span> <a name="Fprop_plus_zero.fexp"><span class="id" title="variable">fexp</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/> <span class="id" title="keyword">Context</span> { <span class="id" title="var">valid_exp</span> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Valid_exp"><span class="id" title="class">Valid_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_zero.fexp"><span class="id" title="variable">fexp</span></a> }.<br/> <span class="id" title="keyword">Context</span> { <span class="id" title="var">exp_not_FTZ</span> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Exp_not_FTZ"><span class="id" title="class">Exp_not_FTZ</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_zero.fexp"><span class="id" title="variable">fexp</span></a> }.<br/> <span class="id" title="keyword">Notation</span> <a name="format"><span class="id" title="abbreviation">format</span></a> := (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#generic_format"><span class="id" title="definition">generic_format</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_zero.fexp"><span class="id" title="variable">fexp</span></a>).<br/> <br/> <span class="id" title="keyword">Section</span> <a name="Fprop_plus_zero.round_plus_eq_zero_aux"><span class="id" title="section">round_plus_eq_zero_aux</span></a>.<br/> <br/> <span class="id" title="keyword">Variable</span> <a name="Fprop_plus_zero.round_plus_eq_zero_aux.rnd"><span class="id" title="variable">rnd</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/> <span class="id" title="keyword">Context</span> { <span class="id" title="var">valid_rnd</span> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Valid_rnd"><span class="id" title="class">Valid_rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_zero.round_plus_eq_zero_aux.rnd"><span class="id" title="variable">rnd</span></a> }.<br/> <br/> <span class="id" title="keyword">Lemma</span> <a name="round_plus_eq_zero_aux"><span class="id" title="lemma">round_plus_eq_zero_aux</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>,<br/> (<a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#canonic_exp"><span class="id" title="definition">canonic_exp</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_zero.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#208bafb0e148fe7fb7dcd812c227f4ee"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#canonic_exp"><span class="id" title="definition">canonic_exp</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_zero.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#format"><span class="id" title="abbreviation">format</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#format"><span class="id" title="abbreviation">format</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a>)%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_zero.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_zero.round_plus_eq_zero_aux.rnd"><span class="id" title="variable">rnd</span></a> (<a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R0"><span class="id" title="axiom">R0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> (<a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0)%<span class="id" title="var">R</span>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_zero.round_plus_eq_zero_aux"><span class="id" title="section">round_plus_eq_zero_aux</span></a>.<br/> <br/> <span class="id" title="keyword">Variable</span> <a name="Fprop_plus_zero.rnd"><span class="id" title="variable">rnd</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" title="axiom">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/> <span class="id" title="keyword">Context</span> { <span class="id" title="var">valid_rnd</span> : <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#Valid_rnd"><span class="id" title="class">Valid_rnd</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_zero.rnd"><span class="id" title="variable">rnd</span></a> }.<br/> <br/> </div> <div class="doc"> rnd(x+y)=0 -> x+y = 0 provided this is not a FTZ format </div> <div class="code"> <span class="id" title="keyword">Theorem</span> <a name="round_plus_eq_zero"><span class="id" title="lemma">round_plus_eq_zero</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>,<br/> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#format"><span class="id" title="abbreviation">format</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#format"><span class="id" title="abbreviation">format</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#round"><span class="id" title="definition">round</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_zero.fexp"><span class="id" title="variable">fexp</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_zero.rnd"><span class="id" title="variable">rnd</span></a> (<a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#R0"><span class="id" title="axiom">R0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> (<a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0)%<span class="id" title="var">R</span>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_zero"><span class="id" title="section">Fprop_plus_zero</span></a>.<br/> <br/> <span class="id" title="keyword">Section</span> <a name="Fprop_plus_FLT"><span class="id" title="section">Fprop_plus_FLT</span></a>.<br/> <span class="id" title="keyword">Variable</span> <span class="id" title="keyword">beta</span> : <a class="idref" href="Flocq.Core.Fcore_Zaux.html#radix"><span class="id" title="record">radix</span></a>.<br/> <br/> <span class="id" title="keyword">Notation</span> <a name="bpow"><span class="id" title="abbreviation">bpow</span></a> <span class="id" title="var">e</span> := (<a class="idref" href="Flocq.Core.Fcore_Raux.html#bpow"><span class="id" title="definition">bpow</span></a> <span class="id" title="keyword">beta</span> <span class="id" title="var">e</span>).<br/> <br/> <span class="id" title="keyword">Variable</span> <a name="Fprop_plus_FLT.emin"><span class="id" title="variable">emin</span></a> <a name="Fprop_plus_FLT.prec"><span class="id" title="variable">prec</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Z"><span class="id" title="inductive">Z</span></a>.<br/> <span class="id" title="keyword">Context</span> { <span class="id" title="var">prec_gt_0_</span> : <a class="idref" href="Flocq.Core.Fcore_FLX.html#Prec_gt_0"><span class="id" title="class">Prec_gt_0</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_FLT.prec"><span class="id" title="variable">prec</span></a> }.<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="FLT_format_plus_small"><span class="id" title="lemma">FLT_format_plus_small</span></a>: <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>,<br/> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#generic_format"><span class="id" title="definition">generic_format</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_FLT.prec"><span class="id" title="variable">prec</span></a>) <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#generic_format"><span class="id" title="definition">generic_format</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_FLT.prec"><span class="id" title="variable">prec</span></a>) <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</span></a> (<a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a><a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#39ab57f76c1eb2e6d107f9799a31545a"><span class="id" title="notation">≤</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#bpow"><span class="id" title="abbreviation">bpow</span></a> (<a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_FLT.prec"><span class="id" title="variable">prec</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a><a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_FLT.emin"><span class="id" title="variable">emin</span></a>))%<span class="id" title="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> <a class="idref" href="Flocq.Core.Fcore_generic_fmt.html#generic_format"><span class="id" title="definition">generic_format</span></a> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_FLT.html#FLT_exp"><span class="id" title="definition">FLT_exp</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_FLT.emin"><span class="id" title="variable">emin</span></a> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_FLT.prec"><span class="id" title="variable">prec</span></a>) (<a class="idref" href="Flocq.Prop.Fprop_plus_error.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#7de2d195108bdf12ab090711a555a032"><span class="id" title="notation">+</span></a><a class="idref" href="Flocq.Prop.Fprop_plus_error.html#y"><span class="id" title="variable">y</span></a>).<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Prop.Fprop_plus_error.html#Fprop_plus_FLT"><span class="id" title="section">Fprop_plus_FLT</span></a>.<br/> </div> </div> <div id="footer"> <hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> </div> </div> </body> </html>