/usr/share/doc/libfloat-coq/html/Float.Closest2Prop.html is in libfloat-coq 1:8.4-5build1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 | <!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>Float.Closest2Prop</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library Float.Closest2Prop</h1>
<div class="code">
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <a class="idref" href="Float.ClosestProp.html#"><span class="id" type="library">ClosestProp</span></a>.<br/>
<span class="id" type="keyword">Section</span> <a name="F2"><span class="id" type="section">F2</span></a>.<br/>
<span class="id" type="keyword">Variable</span> <a name="F2.b"><span class="id" type="variable">b</span></a> : <a class="idref" href="Float.Fbound.html#Fbound"><span class="id" type="record">Fbound</span></a>.<br/>
<span class="id" type="keyword">Variable</span> <a name="F2.precision"><span class="id" type="variable">precision</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" type="inductive">nat</span></a>.<br/>
<br/>
<span class="id" type="keyword">Let</span> <a name="F2.radix"><span class="id" type="variable">radix</span></a> := 2%<span class="id" type="var">Z</span>.<br/>
<br/>
<span class="id" type="keyword">Coercion</span> <span class="id" type="keyword">Local</span> <span class="id" type="var">FtoRradix</span> := <a class="idref" href="Float.Float.html#FtoR"><span class="id" type="definition">FtoR</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.radix"><span class="id" type="variable">radix</span></a>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <a name="TwoMoreThanOne"><span class="id" type="lemma">TwoMoreThanOne</span></a> : (1 <a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.ZArith.BinInt.html#:Z_scope:x_'<'_x"><span class="id" type="notation"><</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.radix"><span class="id" type="variable">radix</span></a>)%<span class="id" type="var">Z</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">radix</span> <span class="id" type="keyword">in</span> |- *; <span class="id" type="tactic">red</span> <span class="id" type="keyword">in</span> |- *; <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> |- *; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<span class="id" type="keyword">Hint Resolve</span> <a class="idref" href="Float.Closest2Prop.html#TwoMoreThanOne"><span class="id" type="lemma">TwoMoreThanOne</span></a>.<br/>
<span class="id" type="keyword">Hypothesis</span> <a name="F2.precisionNotZero"><span class="id" type="variable">precisionNotZero</span></a> : 1 <a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Init.Peano.html#:nat_scope:x_'<'_x"><span class="id" type="notation"><</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.precision"><span class="id" type="variable">precision</span></a>.<br/>
<span class="id" type="keyword">Hypothesis</span> <a name="F2.pGivesBound"><span class="id" type="variable">pGivesBound</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Numbers.BinNums.html#Zpos"><span class="id" type="constructor">Zpos</span></a> (<a class="idref" href="Float.Fbound.html#vNum"><span class="id" type="projection">vNum</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.b"><span class="id" type="variable">b</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Init.Logic.html#:type_scope:x_'='_x"><span class="id" type="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.ZArith.Zpower.html#Zpower_nat"><span class="id" type="definition">Zpower_nat</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.radix"><span class="id" type="variable">radix</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.precision"><span class="id" type="variable">precision</span></a>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <a name="FevenNormMin"><span class="id" type="lemma">FevenNormMin</span></a> : <a class="idref" href="Float.Fodd.html#Even"><span class="id" type="definition">Even</span></a> (<a class="idref" href="Float.Fnorm.html#nNormMin"><span class="id" type="definition">nNormMin</span></a> 2%<span class="id" type="var">nat</span> <a class="idref" href="Float.Closest2Prop.html#F2.precision"><span class="id" type="variable">precision</span></a>).<br/>
<span class="id" type="tactic">unfold</span> <a class="idref" href="Float.Fnorm.html#nNormMin"><span class="id" type="definition">nNormMin</span></a> <span class="id" type="keyword">in</span> |- ×.<br/>
<span class="id" type="tactic">generalize</span> <a class="idref" href="Float.Closest2Prop.html#F2.precisionNotZero"><span class="id" type="variable">precisionNotZero</span></a>; <span class="id" type="tactic">case</span> <a class="idref" href="Float.Closest2Prop.html#F2.precision"><span class="id" type="variable">precision</span></a>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">H'2</span>; <span class="id" type="var">Contradict</span> <span class="id" type="var">H'2</span>; <span class="id" type="tactic">auto</span> <span class="id" type="keyword">with</span> <span class="id" type="var">zarith</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span>; <span class="id" type="tactic">case</span> <span class="id" type="var">n</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">H'2</span>; <span class="id" type="var">Contradict</span> <span class="id" type="var">H'2</span>; <span class="id" type="tactic">auto</span> <span class="id" type="keyword">with</span> <span class="id" type="var">zarith</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">n0</span> <span class="id" type="var">H'2</span>; <span class="id" type="tactic">replace</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Init.Peano.html#pred"><span class="id" type="definition">pred</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Init.Datatypes.html#S"><span class="id" type="constructor">S</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Init.Datatypes.html#S"><span class="id" type="constructor">S</span></a> <span class="id" type="var">n0</span>))) <span class="id" type="keyword">with</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Init.Datatypes.html#S"><span class="id" type="constructor">S</span></a> <span class="id" type="var">n0</span>).<br/>
<span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> |- *; <span class="id" type="tactic">apply</span> <a class="idref" href="Float.Fodd.html#EvenExp"><span class="id" type="lemma">EvenExp</span></a>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">∃</span> 1%<span class="id" type="var">Z</span>; <span class="id" type="tactic">ring</span>.<br/>
<span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> |- *; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <a name="EvenFNSuccFNSuccMid"><span class="id" type="lemma">EvenFNSuccFNSuccMid</span></a> :<br/>
<span class="id" type="keyword">∀</span> <span class="id" type="var">p</span> : <a class="idref" href="Float.Float.html#float"><span class="id" type="record">float</span></a>,<br/>
<a class="idref" href="Float.Fbound.html#Fbounded"><span class="id" type="definition">Fbounded</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.b"><span class="id" type="variable">b</span></a> <a class="idref" href="Float.Closest2Prop.html#p"><span class="id" type="variable">p</span></a> →<br/>
<a class="idref" href="Float.Fodd.html#FNeven"><span class="id" type="definition">FNeven</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.b"><span class="id" type="variable">b</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.radix"><span class="id" type="variable">radix</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.precision"><span class="id" type="variable">precision</span></a> <a class="idref" href="Float.Closest2Prop.html#p"><span class="id" type="variable">p</span></a> →<br/>
<a class="idref" href="Float.Fop.html#Fminus"><span class="id" type="definition">Fminus</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.radix"><span class="id" type="variable">radix</span></a> (<a class="idref" href="Float.FSucc.html#FNSucc"><span class="id" type="definition">FNSucc</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.b"><span class="id" type="variable">b</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.radix"><span class="id" type="variable">radix</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.precision"><span class="id" type="variable">precision</span></a> (<a class="idref" href="Float.FSucc.html#FNSucc"><span class="id" type="definition">FNSucc</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.b"><span class="id" type="variable">b</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.radix"><span class="id" type="variable">radix</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.precision"><span class="id" type="variable">precision</span></a> <a class="idref" href="Float.Closest2Prop.html#p"><span class="id" type="variable">p</span></a>))<br/>
(<a class="idref" href="Float.FSucc.html#FNSucc"><span class="id" type="definition">FNSucc</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.b"><span class="id" type="variable">b</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.radix"><span class="id" type="variable">radix</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.precision"><span class="id" type="variable">precision</span></a> <a class="idref" href="Float.Closest2Prop.html#p"><span class="id" type="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Init.Logic.html#:type_scope:x_'='_x_':>'_x"><span class="id" type="notation">=</span></a> <a class="idref" href="Float.Fop.html#Fminus"><span class="id" type="definition">Fminus</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.radix"><span class="id" type="variable">radix</span></a> (<a class="idref" href="Float.FSucc.html#FNSucc"><span class="id" type="definition">FNSucc</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.b"><span class="id" type="variable">b</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.radix"><span class="id" type="variable">radix</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.precision"><span class="id" type="variable">precision</span></a> <a class="idref" href="Float.Closest2Prop.html#p"><span class="id" type="variable">p</span></a>) <a class="idref" href="Float.Closest2Prop.html#p"><span class="id" type="variable">p</span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Init.Logic.html#:type_scope:x_'='_x_':>'_x"><span class="id" type="notation">:></span></a><a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" type="axiom">R</span></a>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">p</span> <span class="id" type="var">H'</span> <span class="id" type="var">H'0</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">FtoRradix</span> <span class="id" type="keyword">in</span> |- *; <span class="id" type="tactic">apply</span> <a class="idref" href="Float.FSucc.html#FNSuccFNSuccMid"><span class="id" type="lemma">FNSuccFNSuccMid</span></a>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">red</span> <span class="id" type="keyword">in</span> |- *; <span class="id" type="tactic">intros</span> <span class="id" type="var">H'1</span>;<br/>
<span class="id" type="var">absurd</span> (<a class="idref" href="Float.Fodd.html#FNodd"><span class="id" type="definition">FNodd</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.b"><span class="id" type="variable">b</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.radix"><span class="id" type="variable">radix</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.precision"><span class="id" type="variable">precision</span></a> (<a class="idref" href="Float.FSucc.html#FNSucc"><span class="id" type="definition">FNSucc</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.b"><span class="id" type="variable">b</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.radix"><span class="id" type="variable">radix</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.precision"><span class="id" type="variable">precision</span></a> <span class="id" type="var">p</span>)); <br/>
<span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">unfold</span> <a class="idref" href="Float.Fodd.html#FNodd"><span class="id" type="definition">FNodd</span></a> <span class="id" type="keyword">in</span> |- ×.<br/>
<span class="id" type="tactic">rewrite</span> <a class="idref" href="Float.Fnorm.html#FcanonicFnormalizeEq"><span class="id" type="lemma">FcanonicFnormalizeEq</span></a>; <span class="id" type="tactic">auto</span> <span class="id" type="keyword">with</span> <span class="id" type="var">float</span> <span class="id" type="var">arith</span>.<br/>
<span class="id" type="tactic">unfold</span> <a class="idref" href="Float.Fodd.html#Fodd"><span class="id" type="definition">Fodd</span></a> <span class="id" type="keyword">in</span> |- ×.<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H'1</span>.<br/>
<span class="id" type="tactic">apply</span> <a class="idref" href="Float.Fodd.html#EvenNOdd"><span class="id" type="lemma">EvenNOdd</span></a>; <span class="id" type="tactic">auto</span> <span class="id" type="keyword">with</span> <span class="id" type="var">float</span> <span class="id" type="var">arith</span>.<br/>
<span class="id" type="tactic">apply</span> <a class="idref" href="Float.Closest2Prop.html#FevenNormMin"><span class="id" type="lemma">FevenNormMin</span></a>; <span class="id" type="tactic">auto</span> <span class="id" type="keyword">with</span> <span class="id" type="var">float</span> <span class="id" type="var">arith</span>.<br/>
<span class="id" type="tactic">apply</span> <a class="idref" href="Float.Fodd.html#FNevenSuc"><span class="id" type="lemma">FNevenSuc</span></a>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">red</span> <span class="id" type="keyword">in</span> |- *; <span class="id" type="tactic">intros</span> <span class="id" type="var">H'1</span>;<br/>
<span class="id" type="var">absurd</span> (<a class="idref" href="Float.Fodd.html#FNodd"><span class="id" type="definition">FNodd</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.b"><span class="id" type="variable">b</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.radix"><span class="id" type="variable">radix</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.precision"><span class="id" type="variable">precision</span></a> (<a class="idref" href="Float.FSucc.html#FNSucc"><span class="id" type="definition">FNSucc</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.b"><span class="id" type="variable">b</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.radix"><span class="id" type="variable">radix</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.precision"><span class="id" type="variable">precision</span></a> <span class="id" type="var">p</span>));<br/>
<span class="id" type="tactic">auto</span> <span class="id" type="keyword">with</span> <span class="id" type="var">float</span> <span class="id" type="var">arith</span>.<br/>
<span class="id" type="tactic">unfold</span> <a class="idref" href="Float.Fodd.html#FNodd"><span class="id" type="definition">FNodd</span></a> <span class="id" type="keyword">in</span> |- ×.<br/>
<span class="id" type="tactic">rewrite</span> <a class="idref" href="Float.Fnorm.html#FcanonicFnormalizeEq"><span class="id" type="lemma">FcanonicFnormalizeEq</span></a>; <span class="id" type="tactic">auto</span> <span class="id" type="keyword">with</span> <span class="id" type="var">float</span> <span class="id" type="var">arith</span>.<br/>
<span class="id" type="tactic">unfold</span> <a class="idref" href="Float.Fodd.html#Fodd"><span class="id" type="definition">Fodd</span></a> <span class="id" type="keyword">in</span> |- ×.<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H'1</span>.<br/>
<span class="id" type="tactic">apply</span> <a class="idref" href="Float.Fodd.html#EvenNOdd"><span class="id" type="lemma">EvenNOdd</span></a>.<br/>
<span class="id" type="tactic">apply</span> <a class="idref" href="Float.Fodd.html#EvenOpp"><span class="id" type="lemma">EvenOpp</span></a>; <span class="id" type="tactic">apply</span> <a class="idref" href="Float.Closest2Prop.html#FevenNormMin"><span class="id" type="lemma">FevenNormMin</span></a>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <a name="AScal2"><span class="id" type="lemma">AScal2</span></a> :<br/>
<span class="id" type="keyword">∀</span> <span class="id" type="var">p</span> : <a class="idref" href="Float.Float.html#float"><span class="id" type="record">float</span></a>, <a class="idref" href="Float.Float.html#Float"><span class="id" type="constructor">Float</span></a> (<a class="idref" href="Float.Float.html#Fnum"><span class="id" type="projection">Fnum</span></a> <a class="idref" href="Float.Closest2Prop.html#p"><span class="id" type="variable">p</span></a>) (<a class="idref" href="Float.Float.html#Fexp"><span class="id" type="projection">Fexp</span></a> <a class="idref" href="Float.Closest2Prop.html#p"><span class="id" type="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.ZArith.BinInt.html#:Z_scope:x_'+'_x"><span class="id" type="notation">+</span></a> 1%<span class="id" type="var">nat</span>) <a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Init.Logic.html#:type_scope:x_'='_x_':>'_x"><span class="id" type="notation">=</span></a> (<a class="idref" href="Float.Closest2Prop.html#F2.radix"><span class="id" type="variable">radix</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Reals.Rdefinitions.html#:R_scope:x_'*'_x"><span class="id" type="notation">×</span></a> <a class="idref" href="Float.Closest2Prop.html#p"><span class="id" type="variable">p</span></a>)%<span class="id" type="var">R</span> <a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Init.Logic.html#:type_scope:x_'='_x_':>'_x"><span class="id" type="notation">:></span></a><a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Reals.Rdefinitions.html#R"><span class="id" type="axiom">R</span></a>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">p</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">FtoRradix</span> <span class="id" type="keyword">in</span> |- *; <span class="id" type="tactic">rewrite</span> <a class="idref" href="Float.Fbound.html#FvalScale"><span class="id" type="lemma">FvalScale</span></a>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">replace</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Reals.Rfunctions.html#powerRZ"><span class="id" type="definition">powerRZ</span></a> <a class="idref" href="Float.Closest2Prop.html#F2.radix"><span class="id" type="variable">radix</span></a> 1%<span class="id" type="var">nat</span>) <span class="id" type="keyword">with</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.4pl4/stdlib/Coq.Reals.Raxioms.html#INR"><span class="id" type="definition">INR</span></a> 2); [ <span class="id" type="tactic">idtac</span> | <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> |- *; <span class="id" type="tactic">ring</span> ];<br/>
<span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<span class="id" type="keyword">End</span> <a class="idref" href="Float.Closest2Prop.html#F2"><span class="id" type="section">F2</span></a>.<br/>
<span class="id" type="keyword">Hint Resolve</span> <a class="idref" href="Float.Closest2Prop.html#FevenNormMin"><span class="id" type="lemma">FevenNormMin</span></a>: <span class="id" type="var">float</span>.<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>
|