binary_ieeePropsScript.sml
1Theory binary_ieeeProps
2Ancestors binary_ieee real words arithmetic
3Libs realSimps RealArith
4
5val _ = augment_srw_ss[REAL_ARITH_ss]
6
7Overload precision[local] = “fcp$dimindex”
8Overload f2r[local] = “float_to_real”
9Overload bias[local] = “words$INT_MAX”
10Overload sign[local] = “fsign”
11
12Theorem Sign_cases:
13 ∀f. f.Sign = 0w ∨ f.Sign = 1w
14Proof
15 gen_tac >>
16 qspec_then ‘f.Sign’ strip_assume_tac ranged_word_nchotomy >>
17 fs[dimword_1]
18QED
19
20Theorem float_value_eq_float_to_real:
21 float_is_finite f ⇒ float_value f = Float (float_to_real f)
22Proof
23 simp[float_is_finite_thm, float_value_def, PULL_EXISTS, AllCaseEqs()]
24QED
25
26Theorem float_value_float_to_real:
27 float_value f = Float r ⇒ float_to_real f = r
28Proof
29 metis_tac[float_is_finite_thm,float_value_eq_float_to_real,float_value_11]
30QED
31
32Definition mantissa_def:
33 mantissa (x: (τ, χ) float):num =
34 if x.Exponent = 0w
35 then w2n x.Significand
36 else 2 ** precision (:τ) + w2n x.Significand
37End
38
39Theorem abs_next_hi_EQN:
40 float_is_finite f ⇒ abs (f2r (next_hi f)) = abs (f2r f) + ulpᶠ f
41Proof
42 simp[GSYM next_hi_difference, float_ulp_def] >> strip_tac >>
43 Cases_on ‘f2r f = 0’ >> simp[] >>
44 ‘abs (f2r f) < abs (f2r (next_hi f)) ∧ (0 ≤ f2r (next_hi f) ⇔ 0 ≤ f2r f)’
45 suffices_by
46 simp[REAL_ARITH “abs x < abs y ∧ (0 ≤ x ⇔ 0 ≤ y) ⇒
47 abs (y - x) = abs y - abs x”] >>
48 simp[next_hi_larger] >> simp[EQ_IMP_THM] >> rpt strip_tac >> gvs[]
49QED
50
51Theorem float_to_real_ulp:
52 f2r f = sign f * &mantissa f * ulpᶠ f
53Proof
54 simp[float_to_real_def] >>
55 rw[mantissa_def, float_ulp_def, ULP_def, REAL_POW_ADD] >>
56 gvs[real_div, REAL_LDISTRIB, REAL_OF_NUM_POW]
57QED
58
59Theorem realsub_lemma[local]: x ≤ y ⇒ (real_of_num (y - x) = &y - &x)
60Proof simp[REAL_SUB] >> rw[]
61QED
62
63Theorem ABS_REFL'[local] = iffRL ABS_REFL
64
65Theorem positive_representable:
66 r = (2r pow k * &(x:num)) / (2 pow (bias (:χ) + precision(:τ))) ∧
67 0 < k ∧
68 k < 2 ** dimindex(:χ) - 1 ∧
69 x < 2 ** (precision(:τ) + 1)
70⇒
71 ∃f:(τ,χ)float. float_value f = Float r
72Proof
73 strip_tac >>
74 Cases_on ‘x = 0’ >- (gvs[] >> qexists_tac ‘POS0’ >> simp[]) >>
75 Cases_on ‘2 ** precision(:τ) ≤ x’
76 >- (qexists_tac ‘
77 <| Significand := n2w (x - 2 ** precision(:τ));
78 Exponent := n2w k;
79 Sign := n2w 0 |>’ >>
80 simp[float_value_def, word_T_def, dimword_def, UINT_MAX_def,
81 float_to_real_def, dimword_def, real_div, REAL_POW_ADD] >>
82 ‘x - 2 ** precision(:τ) < 2 ** precision(:τ)’ by fs[EXP_ADD] >>
83 simp[REAL_INV_MUL, REAL_SUB_RDISTRIB, realsub_lemma,
84 GSYM REAL_OF_NUM_POW] >>
85 ‘∀r:real. 1 + (r - 1) = r’ by simp[] >> simp[]) >>
86 gvs[NOT_LESS_EQUAL] >>
87 qabbrev_tac ‘lx = LOG 2 x’ >>
88 ‘0 < x’ by simp[] >>
89 ‘2 ** lx ≤ x ∧ x < 2 ** (lx + 1)’
90 by simp[logrootTheory.LOG,GSYM ADD1,Abbr‘lx’] >>
91 qabbrev_tac ‘P = 2n ** precision (:τ)’ >>
92 Cases_on ‘precision (:τ) < k + lx’
93 >- (qexists_tac ‘
94 <| Significand := n2w (x * 2 ** (precision(:τ) - lx) - P) ;
95 Exponent := n2w (k + lx - precision(:τ)) ;
96 Sign := n2w 0 |>’ >>
97 simp[float_value_def, word_T_def, dimword_def, UINT_MAX_def] >>
98 ‘lx ≤ precision(:τ)’
99 by (spose_not_then strip_assume_tac >> fs[NOT_LESS_EQUAL] >>
100 ‘2n ** precision(:τ) < 2 ** lx’ by simp[] >>
101 simp[Abbr‘P’]) >>
102 ‘k + lx - precision(:τ) ≤ k’ by simp[] >>
103 ‘k + lx - precision(:τ) < 2 ** precision(:χ)’ by simp[] >>
104 simp[] >>
105 simp[float_to_real_def, dimword_def] >>
106 simp[REAL_POW_ADD, real_div, REAL_INV_MUL] >>
107 simp[GSYM pow_inv_mul_invlt, REAL_POW_ADD] >>
108 ‘x * 2 ** (precision(:τ) - lx) - P < P’
109 by (qabbrev_tac ‘Q = precision(:τ) - lx’ >>
110 ‘x * 2 ** Q < 2 ** (lx + 1) * 2 ** Q’ by simp[] >>
111 ‘lx + Q = precision(:τ)’ by simp[Abbr‘Q’] >>
112 ‘x * 2 ** Q < 2 ** (lx + 1 + Q)’ by metis_tac[EXP_ADD] >>
113 ‘lx + 1 + Q = precision(:τ) + 1’ by simp[] >>
114 pop_assum SUBST_ALL_TAC >>
115 fs[EXP_ADD, Abbr‘P’]) >>
116 simp[] >>
117 ‘P ≤ x * 2 ** (precision(:τ) - lx)’
118 by (qabbrev_tac ‘Q = precision(:τ) - lx’ >>
119 ‘2 ** lx * 2 ** Q ≤ x * 2 ** Q’ by simp[] >>
120 ‘P = 2 ** lx * 2 ** Q’ suffices_by simp[] >>
121 simp[GSYM EXP_ADD, Abbr‘Q’]) >>
122 simp[realsub_lemma, REAL_SUB_RDISTRIB] >>
123 ‘&P = 2 pow precision(:τ)’ by simp[GSYM REAL_OF_NUM_POW, Abbr‘P’]>>
124 simp[] >>
125 ‘∀x:real. 1 + (x - 1) = x’ by simp[] >> simp[] >>
126 simp_tac bool_ss [GSYM REAL_OF_NUM_POW, GSYM REAL_MUL,
127 REAL_MUL_ASSOC] >>
128 simp[GSYM pow_inv_mul_invlt] >>
129 Cases_on ‘lx = precision(:τ)’ >> simp[] >>
130 simp[GSYM pow_inv_mul_invlt] >> gs[REAL_POW_ADD]) >>
131 gvs[NOT_LESS] >>
132 qexists_tac‘
133 <| Sign := 0w; Significand := n2w (x * 2 ** (k-1)); Exponent := 0w
134 |>’ >>
135 simp[float_value_def, float_to_real_def, word_T_def, UINT_MAX_def,
136 dimword_def] >>
137 simp[real_div, REAL_POW_ADD,REAL_INV_MUL] >>
138 ‘∃k0. k = k0 + 1’ by (Cases_on ‘k’ >> fs[ADD1]) >>
139 pop_assum SUBST_ALL_TAC >> simp[] >>
140 simp[REAL_MUL, REAL_OF_NUM_POW] >>
141 ‘x * 2 ** k0 < P’
142 by (‘x * 2 ** k0 < 2 ** (lx + 1) * 2 ** k0’ by simp[] >>
143 ‘x * 2 ** k0 < 2 ** (lx + 1 + k0)’ by metis_tac[EXP_ADD] >>
144 irule (DECIDE “x:num < y ∧ y ≤ z ⇒ x < z”) >>
145 qexists_tac ‘2n ** (lx + 1 + k0)’ >> simp[] >>
146 simp[Abbr‘P’]) >>
147 simp[] >>
148 gs[REAL_POW_ADD, Abbr‘P’, REAL_OF_NUM_POW, EXP_ADD] >>
149 RULE_ASSUM_TAC (REWRITE_RULE [GSYM REAL_MUL, REAL_MUL_ASSOC]) >>
150 simp[]
151QED
152
153Theorem negative_representable:
154 r = -(2r pow k * &(x:num)) / (2 pow (bias (:χ) + precision(:τ))) ∧
155 0 < k ∧ k < 2 ** precision(:χ) - 1 ∧
156 x < 2 ** (precision(:τ) + 1)
157 ⇒
158 ∃f:(τ,χ)float. float_value f = Float r
159Proof
160 strip_tac >>
161 mp_tac (Q.INST [‘r’ |-> ‘-r’] positive_representable) >>
162 impl_tac >- simp[neg_rat] >>
163 strip_tac >>
164 qexists_tac ‘float_negate f’ >>
165 simp[float_negate]
166QED
167
168Theorem representables:
169 abs r = (2r pow k * &(x:num)) / (2 pow (bias (:χ) + precision(:τ))) ∧
170 0 < k ∧ k < 2 ** precision(:χ) - 1 ∧
171 x < 2 ** (precision(:τ) + 1)
172 ⇒
173 ∃f:(τ,χ)float. float_value f = Float r
174Proof
175 rw[abs, Excl "REALMULCANON", Excl "RMUL_EQNORM3", Excl "RMUL_EQNORM4"]
176 >- metis_tac[positive_representable] >>
177 fs[Once REAL_NEG_EQ, Excl "REALMULCANON"] >>
178 fs[Excl "REALMULCANON", neg_rat] >> metis_tac[negative_representable]
179QED
180
181Theorem mantissa_UB:
182 mantissa (f:(α,β)float) < 2 * 2 ** precision(:α)
183Proof
184 rw[mantissa_def] >> Cases_on ‘f.Significand’ >> gvs[dimword_def]
185QED
186
187Theorem smaller_floats_representable_lemma:
188 2 ≤ precision (:τ) ∧
189 float_value (b:(χ,τ)float) = Float rb ∧
190 rr = real_of_int i * ulpᶠ b ∧
191 abs rr ≤ abs rb
192 ⇒
193 ∃r:(χ, τ) float. float_value r = Float rr
194Proof
195 rpt strip_tac >>
196 Cases_on ‘rb = 0’ >- (gvs[REAL_ABS_LE0] >> qexists_tac ‘POS0’ >> simp[]) >>
197 wlog_tac ‘0 < rb’ [‘b’, ‘rb’]
198 >- (first_x_assum $ qspecl_then [‘float_negate b’, ‘-rb’] mp_tac >>
199 simp[float_negate]) >>
200 gs[ABS_REFL'] >>
201 Cases_on ‘i = 0’ >- (qexists_tac ‘POS0’ >> simp[]) >>
202 wlog_tac ‘0 < rr’ [‘rr’, ‘i’]
203 >- (first_x_assum $ qspecl_then [‘-rr’, ‘-i’] mp_tac >> simp[] >>
204 gs[REAL_NOT_LT] >> impl_tac
205 >- gvs[REAL_LE_LT] >>
206 simp[GSYM float_negate, REAL_MUL_LNEG] >> metis_tac[]) >>
207 gs[ABS_REFL'] >>
208 ‘∃n. i = &n’
209 by (Cases_on ‘i’ using integerTheory.INT_NUM_CASES>> gs[] >>
210 gs[REAL_MUL_RNEG] >>
211 ‘0 < ulpᶠ b * &n’ by simp[REAL_LT_MUL] >>
212 gs[]) >> gvs[] >>
213 drule_then (SUBST_ALL_TAC o SYM) float_value_float_to_real >>
214 gvs[float_to_real_ulp] >>
215 ‘sign b = 1’
216 by (qspec_then ‘b’ strip_assume_tac Sign_cases >> simp[] >>
217 ‘float_is_finite b ∧ ¬float_is_zero b’
218 by (simp[float_is_finite_thm, float_is_zero_float_value_EQ0] >>
219 rpt strip_tac >> gvs[]) >>
220 gvs[]) >>
221 gvs[] >>
222 irule representables >> simp[ABS_MUL, float_ulp_def, ULP_def] >>
223 irule_at (Pos last) EQ_REFL >> rw[]
224 >- (irule LESS_EQ_LESS_TRANS >> qexists_tac ‘mantissa b’ >> simp[] >>
225 REWRITE_TAC [GSYM REAL_LT, GSYM REAL_OF_NUM_POW, REAL_POW_ADD,
226 POW_1] >>
227 simp[REAL_OF_NUM_POW,mantissa_UB])
228 >- simp[DECIDE “x:num < y - z ⇔ x + z < y”]
229 >- (gs[float_value_def, AllCaseEqs()] >>
230 gvs[word_T_def, UINT_MAX_def] >>
231 Cases_on ‘b.Exponent’ >> gvs[dimword_def])
232 >- (Cases_on ‘b.Exponent’ >> gvs[dimword_def])
233QED
234
235Theorem ulp_multiples_representable:
236 float_is_finite f ∧ 2 ≤ precision(:τ) ∧
237 abs r = &n * ulpᶠ (f:(χ,τ) float) ∧ n ≤ 2 ** precision(:χ) ⇒
238 ∃f':(χ,τ)float. float_value f' = Float r
239Proof
240 reverse (Cases_on ‘f.Exponent = 0w’)
241 >- (strip_tac >> irule smaller_floats_representable_lemma >> simp[] >>
242 gs[float_is_finite_thm] >> first_assum $ irule_at (Pos hd) >>
243 qexists_tac ‘if 0 < r then &n else -&n’ >> conj_tac >- rw[] >>
244 drule float_value_float_to_real >>
245 simp[float_to_real_ulp] >> rw[] >> simp[ABS_MUL] >>
246 rw[mantissa_def]) >>
247 strip_tac >>
248 qabbrev_tac ‘sn = if 0 < r then 0w : word1 else 1w’ >>
249 qabbrev_tac ‘ex = if n = 2 ** precision(:χ) then 1w : bool[τ] else 0w’ >>
250 qabbrev_tac ‘m = if n = 2 ** precision(:χ) then 0w : bool[χ] else n2w n’>>
251 qexists_tac ‘<| Sign := sn; Significand := m; Exponent := ex|>’ >>
252 simp[float_to_real_def, float_value_def, AllCaseEqs()] >>
253 simp[Abbr‘ex’] >> rw[] >>
254 gvs[word_T_def, UINT_MAX_def, dimword_def,
255 DECIDE “x:num ≠ y - x ⇔ 2 * x ≠ y”] >>
256 simp[Abbr‘m’] >>
257 Cases_on ‘0 < r’ >>
258 gs[Abbr‘sn’, ABS_REFL', float_ulp_def, ULP_def, dimword_def, REAL_POW_ADD,
259 REAL_OF_NUM_POW, EXP_ADD] >>
260 full_simp_tac (bool_ss ++ RMULCANON_ss ++ RMULRELNORM_ss) [GSYM REAL_MUL] >>
261 gvs[] >>
262 ‘abs r = -r’ by simp[] >> gvs[]
263QED
264
265Theorem largest_props[simp]:
266 ¬(largest (:α # β) < 0) ∧ largest (:α # β) ≠ 0 ∧ 0 < largest(:α # β) ∧
267 0 ≤ largest (:α # β) ∧ ¬(largest(:α # β) ≤ 0)
268Proof
269 ‘0 < largest(:α # β)’ suffices_by simp[] >>
270 simp[largest_def, UINT_MAX_def, dimword_def] >>
271 irule REAL_LT_MUL >> simp[REAL_ARITH “0r < x - y ⇔ y < x”] >>
272 simp[REAL_OF_NUM_POW, DECIDE “1n < 2 * c ⇔ 1 ≤ c”]
273QED
274
275Theorem threshold_props[simp]:
276 ¬(threshold (:α # β) < 0) ∧ threshold (:α # β) ≠ 0 ∧ 0 < threshold(:α # β) ∧
277 0 ≤ threshold (:α # β) ∧ ¬(threshold(:α # β) ≤ 0)
278Proof
279 ‘0 < threshold(:α # β)’ suffices_by REAL_ARITH_TAC >>
280 irule REAL_LT_TRANS >> qexists ‘largest(:α#β)’ >>
281 simp[largest_lt_threshold]
282QED
283
284Theorem is_closest_0_float_to_real:
285 is_closest float_is_finite 0 (b:(α,β)float) ⇔ float_to_real b = 0
286Proof
287 simp[is_closest_def, float_is_finite_def, IN_DEF] >>
288 Cases_on ‘float_value b’ >> fs[float_value_def, CaseEq "bool"]
289 >- (reverse eq_tac >> rw[] >>
290 first_x_assum (qspec_then ‘float_plus_zero(:α#β)’ mp_tac) >>
291 simp[float_plus_zero_def, word_T_def, UINT_MAX_def, dimword_def] >>
292 assume_tac (DIMINDEX_GT_0 |> INST_TYPE [alpha |-> beta]) >> simp[]) >>
293 simp[float_to_real_def, word_T_def, UINT_MAX_def, NOT_LESS_EQUAL,
294 dimword_def, AllCaseEqs(), real_div] >>
295 irule (REAL_ARITH “0 ≤ y ⇒ 1 + y ≠ 0”) >> simp[REAL_LE_MUL]
296QED
297
298Theorem round_representable:
299 2 ≤ precision(:β) ∧ float_is_finite (f:(α,β)float) ⇒
300 ∃f':(α,β)float. float_is_finite f' ∧ round m (f2r f) = f' ∧ f2r f' = f2r f
301Proof
302 strip_tac >>
303 Cases_on ‘f2r f = 0’
304 >- (simp [] >> simp[round_def, real_gt, real_ge] >>
305 Cases_on ‘m’ >>
306 simp[closest_def, closest_such_def] >>
307 SELECT_ELIM_TAC >> simp[] >>
308 conj_tac >>~-
309 ([‘$? _’], qexists ‘POS0’ >> simp[is_closest_def, word_lsb_n2w, IN_DEF]) >>
310 simp[is_closest_def, IN_DEF]) >>
311 qexists ‘f’ >> simp[] >>
312 simp[round_def] >>
313 ‘float_value f = Float (f2r f)’ by simp[float_value_eq_float_to_real] >>
314 assume_tac (INST_TYPE [“:χ” |-> “:β”, “:τ” |-> “:α”] largest_lt_threshold) >>
315 drule_all_then strip_assume_tac float_bounds >> simp[] >>
316 Cases_on ‘m’ >> simp[closest_such_def, closest_def] >>
317 SELECT_ELIM_TAC >> simp[is_closestP_finite_float_exists] >> rpt conj_tac >>~-
318 ([‘$? _’], qexists ‘f’ >> simp[is_closest_def]) >> rpt strip_tac >>
319 qpat_x_assum ‘is_closest _ _ _ (* a *)’ mp_tac >>
320 simp[is_closest_def, IN_DEF] >> rpt strip_tac >>
321 first_x_assum $ qspec_then ‘f’ mp_tac >> simp[REAL_ABS_LE0] >>
322 simp[float_to_real_eq, float_is_zero_to_real]
323QED
324
325Theorem round_representable_nonzero:
326 2 ≤ precision(:β) ∧ float_is_finite (f:(α,β)float) ∧ f2r f ≠ 0 ⇒
327 round m (f2r f) = f
328Proof
329 rpt strip_tac >>
330 drule_all_then (qspec_then ‘m’ strip_assume_tac) round_representable >>
331 simp[] >> gvs[float_to_real_eq, float_is_zero_to_real]
332QED
333
334Theorem float_to_real_EQ0_cases:
335 f2r f = 0 ⇔ f = POS0 ∨ f = NEG0
336Proof
337 simp[EQ_IMP_THM, DISJ_IMP_THM] >>
338 simp[GSYM float_is_zero_to_real, float_is_zero] >>
339 simp[float_plus_zero_def, float_minus_zero_def, float_component_equality] >>
340 Cases_on ‘f.Sign’ >> gvs[dimword_1]
341QED
342
343Theorem round_representable_zero:
344 2 ≤ precision(:β) ⇒ round m 0 = (POS0:(α,β)float) ∨ round m 0 = (NEG0:(α,β)float)
345Proof
346 strip_tac >>
347 drule_then (qspecl_then [‘m’, ‘POS0’] strip_assume_tac) round_representable >>
348 gvs[] >>
349 metis_tac[float_to_real_round0, float_to_real_EQ0_cases]
350QED