<!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.Calc.Fcalc_div</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library Flocq.Calc.Fcalc_div</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="lab14"></a><h1 class="section">Helper function and theorem for computing the rounded quotient of two floating-point numbers.</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_digits.html#"><span class="id" title="library">Fcore_digits</span></a>.<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#"><span class="id" title="library">Fcalc_bracket</span></a>.<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Flocq.Calc.Fcalc_digits.html#"><span class="id" title="library">Fcalc_digits</span></a>.<br/>
<br/>
<span class="id" title="keyword">Section</span> <a name="Fcalc_div"><span class="id" title="section">Fcalc_div</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/>
</div>
<div class="doc">
Computes a mantissa of precision p, the corresponding exponent,
and the position with respect to the real quotient of the
input floating-point numbers.
<div class="paragraph"> </div>
The algorithm performs the following steps:
<div class="paragraph"> </div>
<ul class="doclist">
<li> Shift dividend mantissa so that it has at least p2 + p digits.
</li>
<li> Perform the Euclidean division.
</li>
<li> Compute the position according to the division remainder.
</li>
</ul>
Complexity is fine as long as p1 <= 2p and p2 <= p.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="Fdiv_core"><span class="id" title="definition">Fdiv_core</span></a> <span class="id" title="var">prec</span> <span class="id" title="var">m1</span> <span class="id" title="var">e1</span> <span class="id" title="var">m2</span> <span class="id" title="var">e2</span> :=<br/>
<span class="id" title="keyword">let</span> <span class="id" title="var">d1</span> := <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Calc.Fcalc_div.html#m1"><span class="id" title="variable">m1</span></a> <span class="id" title="keyword">in</span><br/>
<span class="id" title="keyword">let</span> <span class="id" title="var">d2</span> := <a class="idref" href="Flocq.Core.Fcore_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <span class="id" title="keyword">beta</span> <a class="idref" href="Flocq.Calc.Fcalc_div.html#m2"><span class="id" title="variable">m2</span></a> <span class="id" title="keyword">in</span><br/>
<span class="id" title="keyword">let</span> <span class="id" title="var">e</span> := (<a class="idref" href="Flocq.Calc.Fcalc_div.html#e1"><span class="id" title="variable">e1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#e2"><span class="id" title="variable">e2</span></a>)%<span class="id" title="var">Z</span> <span class="id" title="keyword">in</span><br/>
<span class="id" title="keyword">let</span> (<span class="id" title="var">m</span>, <span class="id" title="var">e'</span>) :=<br/>
<span class="id" title="keyword">match</span> (<a class="idref" href="Flocq.Calc.Fcalc_div.html#d2"><span class="id" title="variable">d2</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.Calc.Fcalc_div.html#prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#d1"><span class="id" title="variable">d1</span></a>)%<span class="id" title="var">Z</span> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" title="constructor">Zpos</span></a> <span class="id" title="var">p</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Calc.Fcalc_div.html#m1"><span class="id" title="variable">m1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zpow_def.html#Zpower_pos"><span class="id" title="abbreviation">Zpower_pos</span></a> <span class="id" title="keyword">beta</span> <span class="id" title="var">p</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#e"><span class="id" title="variable">e</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="http://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.BinNums.html#Zneg"><span class="id" title="constructor">Zneg</span></a> <span class="id" title="var">p</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>%<span class="id" title="var">Z</span><br/>
| <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="Flocq.Calc.Fcalc_div.html#m1"><span class="id" title="variable">m1</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a><br/>
<span class="id" title="keyword">end</span> <span class="id" title="keyword">in</span><br/>
<span class="id" title="keyword">let</span> '<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">q</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">r</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zdiv.html#Zdiv_eucl"><span class="id" title="abbreviation">Zdiv_eucl</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#m2"><span class="id" title="variable">m2</span></a> <span class="id" title="keyword">in</span><br/>
<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">q</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#e'"><span class="id" title="variable">e'</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#new_location"><span class="id" title="definition">new_location</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#m2"><span class="id" title="variable">m2</span></a> <span class="id" title="var">r</span> <a class="idref" href="Flocq.Calc.Fcalc_bracket.html#loc_Exact"><span class="id" title="constructor">loc_Exact</span></a><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>.<br/>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="Fdiv_core_correct"><span class="id" title="lemma">Fdiv_core_correct</span></a> :<br/>
<span class="id" title="keyword">∀</span> <span class="id" title="var">prec</span> <span class="id" title="var">m1</span> <span class="id" title="var">e1</span> <span class="id" title="var">m2</span> <span class="id" title="var">e2</span>,<br/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#prec"><span class="id" title="variable">prec</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/>
(0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#m1"><span class="id" title="variable">m1</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> (0 <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#273beba4f3453dbb29192b3ac740bb71"><span class="id" title="notation"><</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#m2"><span class="id" title="variable">m2</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/>
<span class="id" title="keyword">let</span> '<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><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.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">e</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">l</span><a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> := <a class="idref" href="Flocq.Calc.Fcalc_div.html#Fdiv_core"><span class="id" title="definition">Fdiv_core</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#prec"><span class="id" title="variable">prec</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#m1"><span class="id" title="variable">m1</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#e1"><span class="id" title="variable">e1</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#m2"><span class="id" title="variable">m2</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#e2"><span class="id" title="variable">e2</span></a> <span class="id" title="keyword">in</span><br/>
(<a class="idref" href="Flocq.Calc.Fcalc_div.html#prec"><span class="id" title="variable">prec</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_digits.html#Zdigits"><span class="id" title="definition">Zdigits</span></a> <span class="id" title="keyword">beta</span> <span class="id" title="var">m</span>)%<span class="id" title="var">Z</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a><br/>
<a class="idref" href="Flocq.Calc.Fcalc_bracket.html#inbetween_float"><span class="id" title="definition">inbetween_float</span></a> <span class="id" title="keyword">beta</span> <span class="id" title="var">m</span> <span class="id" title="var">e</span> (<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.Calc.Fcalc_div.html#m1"><span class="id" title="variable">m1</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#e1"><span class="id" title="variable">e1</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#0c0207ff801f7c795ce431f130ae670a"><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.Calc.Fcalc_div.html#m2"><span class="id" title="variable">m2</span></a> <a class="idref" href="Flocq.Calc.Fcalc_div.html#e2"><span class="id" title="variable">e2</span></a>)) <span class="id" title="var">l</span>.<br/>
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Calc.Fcalc_div.html#Fcalc_div"><span class="id" title="section">Fcalc_div</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>
distrib
>
Mageia
>
6
>
armv5tl
>
media
>
core-release
>
by-pkgid
>
3c7997fe0e8405f6d7b5563e63d17a78
>
files
>
78
