<!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_ops</title> </head> <body> <div id="page"> <div id="header"> </div> <div id="main"> <h1 class="libtitle">Library Flocq.Calc.Fcalc_ops</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> Basic operations on floats: alignment, addition, multiplication </div> <div class="code"> <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/> <br/> <span class="id" title="keyword">Section</span> <a name="Float_ops"><span class="id" title="section">Float_ops</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/> <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">Implicit Arguments</span> <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>]].<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="Falign"><span class="id" title="definition">Falign</span></a> (<span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span>) :=<br/> <span class="id" title="keyword">let</span> '(<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="var">m1</span> <span class="id" title="var">e1</span>) := <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</span></a> <span class="id" title="keyword">in</span><br/> <span class="id" title="keyword">let</span> '(<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="var">m2</span> <span class="id" title="var">e2</span>) := <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f2"><span class="id" title="variable">f2</span></a> <span class="id" title="keyword">in</span><br/> <span class="id" title="keyword">if</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.Zbool.html#Zle_bool"><span class="id" title="abbreviation">Zle_bool</span></a> <span class="id" title="var">e1</span> <span class="id" title="var">e2</span><br/> <span class="id" title="keyword">then</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">m1</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">m2</span> <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"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> (<span class="id" title="var">e2</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <span class="id" title="var">e1</span>))%<span class="id" title="var">Z</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">e1</span><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">else</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">m1</span> <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"><span class="id" title="abbreviation">Zpower</span></a> <span class="id" title="keyword">beta</span> (<span class="id" title="var">e1</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <span class="id" title="var">e2</span>))%<span class="id" title="var">Z</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">m2</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">e2</span><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="Falign_spec"><span class="id" title="lemma">Falign_spec</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</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">m1</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">m2</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> := <a class="idref" href="Flocq.Calc.Fcalc_ops.html#Falign"><span class="id" title="definition">Falign</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f2"><span class="id" title="variable">f2</span></a> <span class="id" title="keyword">in</span><br/> <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</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> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="var">m1</span> <span class="id" title="var">e</span>) <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><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.Calc.Fcalc_ops.html#f2"><span class="id" title="variable">f2</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> <span class="id" title="keyword">beta</span> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="var">m2</span> <span class="id" title="var">e</span>).<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="Falign_spec_exp"><span class="id" title="lemma">Falign_spec_exp</span></a>:<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span>,<br/> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Init.Datatypes.html#snd"><span class="id" title="definition">snd</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_ops.html#Falign"><span class="id" title="definition">Falign</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f2"><span class="id" title="variable">f2</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.ZArith.BinInt.html#Zmin"><span class="id" title="abbreviation">Zmin</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Fexp"><span class="id" title="projection">Fexp</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</span></a>) (<a class="idref" href="Flocq.Core.Fcore_defs.html#Fexp"><span class="id" title="projection">Fexp</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f2"><span class="id" title="variable">f2</span></a>).<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="Fopp"><span class="id" title="definition">Fopp</span></a> (<span class="id" title="var">f1</span> : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span>) : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span> :=<br/> <span class="id" title="keyword">let</span> '(<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="var">m1</span> <span class="id" title="var">e1</span>) := <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</span></a> <span class="id" title="keyword">in</span><br/> <a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#0a3978eabdacce0a128118074de19651"><span class="id" title="notation">-</span></a><span class="id" title="var">m1</span>)%<span class="id" title="var">Z</span> <span class="id" title="var">e1</span>.<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="F2R_opp"><span class="id" title="lemma">F2R_opp</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">f1</span> : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span>,<br/> (<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_ops.html#Fopp"><span class="id" title="definition">Fopp</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</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#0575b33c544988081e4e30ee15f09d84"><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.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</span></a>)%<span class="id" title="var">R</span>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="Fabs"><span class="id" title="definition">Fabs</span></a> (<span class="id" title="var">f1</span> : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span>) : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span> :=<br/> <span class="id" title="keyword">let</span> '(<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="var">m1</span> <span class="id" title="var">e1</span>) := <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</span></a> <span class="id" title="keyword">in</span><br/> <a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#Zabs"><span class="id" title="abbreviation">Zabs</span></a> <span class="id" title="var">m1</span>)%<span class="id" title="var">Z</span> <span class="id" title="var">e1</span>.<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="F2R_abs"><span class="id" title="lemma">F2R_abs</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">f1</span> : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span>,<br/> (<a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_ops.html#Fabs"><span class="id" title="definition">Fabs</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</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.Rbasic_fun.html#Rabs"><span class="id" title="definition">Rabs</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.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</span></a>))%<span class="id" title="var">R</span>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="Fplus"><span class="id" title="definition">Fplus</span></a> (<span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span>) : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</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">m1</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">m2</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> := <a class="idref" href="Flocq.Calc.Fcalc_ops.html#Falign"><span class="id" title="definition">Falign</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f2"><span class="id" title="variable">f2</span></a> <span class="id" title="keyword">in</span><br/> <a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> (<span class="id" title="var">m1</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <span class="id" title="var">m2</span>) <span class="id" title="var">e</span>.<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="F2R_plus"><span class="id" title="lemma">F2R_plus</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span>,<br/> <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_ops.html#Fplus"><span class="id" title="definition">Fplus</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f2"><span class="id" title="variable">f2</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.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</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.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f2"><span class="id" title="variable">f2</span></a>)%<span class="id" title="var">R</span>.<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="Fplus_same_exp"><span class="id" title="lemma">Fplus_same_exp</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">m1</span> <span class="id" title="var">m2</span> <span class="id" title="var">e</span>,<br/> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#Fplus"><span class="id" title="definition">Fplus</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#m1"><span class="id" title="variable">m1</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#e"><span class="id" title="variable">e</span></a>) (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#m2"><span class="id" title="variable">m2</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.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#Float"><span class="id" title="constructor">Float</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_ops.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#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#m2"><span class="id" title="variable">m2</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_ops.html#e"><span class="id" title="variable">e</span></a>.<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="Fexp_Fplus"><span class="id" title="lemma">Fexp_Fplus</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span>,<br/> <a class="idref" href="Flocq.Core.Fcore_defs.html#Fexp"><span class="id" title="projection">Fexp</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_ops.html#Fplus"><span class="id" title="definition">Fplus</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f2"><span class="id" title="variable">f2</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.ZArith.BinInt.html#Zmin"><span class="id" title="abbreviation">Zmin</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Fexp"><span class="id" title="projection">Fexp</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</span></a>) (<a class="idref" href="Flocq.Core.Fcore_defs.html#Fexp"><span class="id" title="projection">Fexp</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f2"><span class="id" title="variable">f2</span></a>).<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="Fminus"><span class="id" title="definition">Fminus</span></a> (<span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span>) :=<br/> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#Fplus"><span class="id" title="definition">Fplus</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_ops.html#Fopp"><span class="id" title="definition">Fopp</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f2"><span class="id" title="variable">f2</span></a>).<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="F2R_minus"><span class="id" title="lemma">F2R_minus</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span>,<br/> <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_ops.html#Fminus"><span class="id" title="definition">Fminus</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f2"><span class="id" title="variable">f2</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.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</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.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f2"><span class="id" title="variable">f2</span></a>)%<span class="id" title="var">R</span>.<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="Fminus_same_exp"><span class="id" title="lemma">Fminus_same_exp</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">m1</span> <span class="id" title="var">m2</span> <span class="id" title="var">e</span>,<br/> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#Fminus"><span class="id" title="definition">Fminus</span></a> (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#m1"><span class="id" title="variable">m1</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#e"><span class="id" title="variable">e</span></a>) (<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#m2"><span class="id" title="variable">m2</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.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#Float"><span class="id" title="constructor">Float</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_ops.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#239a40728d107295b3cb2c790f57f9e9"><span class="id" title="notation">-</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#m2"><span class="id" title="variable">m2</span></a>) <a class="idref" href="Flocq.Calc.Fcalc_ops.html#e"><span class="id" title="variable">e</span></a>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="Fmult"><span class="id" title="definition">Fmult</span></a> (<span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span>) : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span> :=<br/> <span class="id" title="keyword">let</span> '(<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="var">m1</span> <span class="id" title="var">e1</span>) := <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</span></a> <span class="id" title="keyword">in</span><br/> <span class="id" title="keyword">let</span> '(<a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> <span class="id" title="var">m2</span> <span class="id" title="var">e2</span>) := <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f2"><span class="id" title="variable">f2</span></a> <span class="id" title="keyword">in</span><br/> <a class="idref" href="Flocq.Core.Fcore_defs.html#Float"><span class="id" title="constructor">Float</span></a> (<span class="id" title="var">m1</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#88e34ed7a73f02772126289867960764"><span class="id" title="notation">×</span></a> <span class="id" title="var">m2</span>) (<span class="id" title="var">e1</span> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.ZArith.BinInt.html#a3448b794f7a26d611ad36492b5d640b"><span class="id" title="notation">+</span></a> <span class="id" title="var">e2</span>).<br/> <br/> <span class="id" title="keyword">Theorem</span> <a name="F2R_mult"><span class="id" title="lemma">F2R_mult</span></a> :<br/> <span class="id" title="keyword">∀</span> <span class="id" title="var">f1</span> <span class="id" title="var">f2</span> : <a class="idref" href="Flocq.Core.Fcore_defs.html#float"><span class="id" title="record">float</span></a> <span class="id" title="keyword">beta</span>,<br/> <a class="idref" href="Flocq.Core.Fcore_defs.html#F2R"><span class="id" title="definition">F2R</span></a> (<a class="idref" href="Flocq.Calc.Fcalc_ops.html#Fmult"><span class="id" title="definition">Fmult</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#f2"><span class="id" title="variable">f2</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.Calc.Fcalc_ops.html#f1"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/current/stdlib/Coq.Reals.Rdefinitions.html#361afbb9b173fae6251865f2da226003"><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.Calc.Fcalc_ops.html#f2"><span class="id" title="variable">f2</span></a>)%<span class="id" title="var">R</span>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="Flocq.Calc.Fcalc_ops.html#Float_ops"><span class="id" title="section">Float_ops</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
>
79
