GenFloat.v 10.5 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10 11
(********************************************************************)

12 13
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
14
Require Import BuiltIn.
15 16 17 18 19 20 21 22 23
Require Import ZArith.
Require Import Rbase.
Require Import Rbasic_fun.
Require int.Int.
Require real.Real.
Require real.Abs.
Require real.FromInt.
Require floating_point.Rounding.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
24 25
Require Import Flocq.Core.Core.
Require Import Flocq.IEEE754.Binary.
26 27 28 29 30 31 32 33 34
Require Import int.Abs.

Section GenFloat.
Global Coercion B2R_coercion prec emax := @B2R prec emax.

Variable prec emax : Z.
Hypothesis Hprec : Zlt_bool 0 prec = true.
Hypothesis Hemax : Zlt_bool prec emax = true.
Let emin := (3 - emax - prec)%Z.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
35 36
Notation fexp := (FLT_exp emin prec).

37 38 39
Lemma Hprec': (0 < prec)%Z. revert Hprec. now case Zlt_bool_spec. Qed.
Lemma Hemax': (prec < emax)%Z. revert Hemax. now case Zlt_bool_spec. Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
40
Instance Hprec'' : Prec_gt_0 prec := Hprec'.
41 42 43 44 45 46 47 48

Record t : Set := mk_fp {
  binary : binary_float prec emax;
  value := (binary : R);
  exact : R;
  model : R
}.

49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67
Lemma t_inv :
  forall x xe xm y ye ym,
  (x = y -> xe = ye -> xm = ym -> False) ->
  (mk_fp x xe xm <> mk_fp y ye ym).
Proof.
intros x xe xm y ye ym H H'.
apply H.
exact (f_equal binary H').
exact (f_equal exact H').
exact (f_equal model H').
Qed.

Lemma t_WhyType : WhyType t.
Proof with
match goal with
| _ => try ( right ; apply t_inv ; easy )
end.
split.
split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
68
apply B754_zero.
69 70 71 72 73 74 75 76
exact false.
exact R0.
exact R0.
intros x y.
destruct x as (x,xv,xe,xm).
destruct y as (y,yv,ye,ym).
destruct (Req_EM_T xe ye) as [He|He]...
destruct (Req_EM_T xm ym) as [Hm|Hm]...
77 78 79 80 81 82 83 84 85 86 87 88 89
rewrite He, Hm.
destruct x as [xs|xs|xs xm'|xs xm' xe' xH] ;
  destruct y as [ys|ys|ys ym'|ys ym' ye' yH]...
clear.
destruct (Bool.bool_dec xs ys) as [->|Hs].
now left.
right.
apply t_inv.
intros H _ _.
now injection H.
clear.
destruct (Bool.bool_dec xs ys) as [->|Hs].
now left.
90 91
right.
apply t_inv.
92
intros H _ _.
93
now injection H.
94 95
clear.
destruct (Bool.bool_dec xs ys) as [->|Hs].
Guillaume Melquiond's avatar
Guillaume Melquiond committed
96
destruct (Pos.eq_dec xm' ym') as [Hm'|Hm'].
97 98
left.
apply f_equal3 ; try easy.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
99 100
revert e; rewrite Hm'; intros e.
now rewrite (eqbool_irrelevance _ e0 e).
101 102
right.
apply t_inv.
103 104 105 106 107 108 109
intros H _ _.
injection H.
contradict Hm'.
now rewrite Hm'.
right.
apply t_inv.
intros H _ _.
110 111 112 113 114 115 116 117 118 119 120 121
now injection H.
destruct (Req_EM_T xv yv) as [Hv|Hv].
left.
apply f_equal3 ; try easy.
now apply B2R_inj.
right.
apply t_inv.
intros H _ _.
apply Hv.
now apply f_equal.
Qed.

122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
Record t_strict: Set := mk_fp_strict {
  datum :> t;
  finite : is_finite prec emax (binary datum) = true
}.

Import Rounding.
Definition rnd_of_mode (m:mode) :=
  match m with
  |  NearestTiesToEven => mode_NE
  |  ToZero            => mode_ZR
  |  Up                => mode_UP
  |  Down              => mode_DN
  |  NearestTiesToAway => mode_NA
  end.

Definition r_to_fp rnd x : binary_float prec emax :=
  let r := round radix2 fexp (round_mode rnd) x in
  let m := Ztrunc (scaled_mantissa radix2 fexp r) in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
140
  let e := cexp radix2 fexp r in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
141
  binary_normalize prec emax Hprec' Hemax' rnd m e false.
142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160

Lemma is_finite_FF2B :
  forall f H,
  is_finite prec emax (FF2B prec emax f H) =
    match f with
    | F754_finite _ _ _ => true
    | F754_zero _ => true
    | _ => false
    end.
Proof.
now intros [| | |].
Qed.

Theorem r_to_fp_correct :
  forall rnd x,
  let r := round radix2 fexp (round_mode rnd) x in
  (Rabs r < bpow radix2 emax)%R ->
  is_finite prec emax (r_to_fp rnd x) = true /\
  r_to_fp rnd x = r :>R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
161
Proof with auto with typeclass_instances.
162 163
intros rnd x r Bx.
unfold r_to_fp. fold r.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
164
generalize (binary_normalize_correct prec emax Hprec' Hemax' rnd (Ztrunc (scaled_mantissa radix2 fexp r)) (cexp radix2 fexp r) false).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
165 166 167 168
unfold r.
elim generic_format_round...
fold emin r.
rewrite round_generic...
169
rewrite Rlt_bool_true with (1 := Bx).
170
now split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
171
apply generic_format_round...
172 173 174 175 176 177 178
Qed.

Theorem r_to_fp_format :
  forall rnd x,
  FLT_format radix2 emin prec x ->
  (Rabs x < bpow radix2 emax)%R ->
  r_to_fp rnd x = x :>R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
179
Proof with auto with typeclass_instances.
180 181
intros rnd x Fx Bx.
assert (Gx: generic_format radix2 fexp x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
182
apply generic_format_FLT.
183
apply Fx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
184
pattern x at 2 ; rewrite <- round_generic with (rnd := round_mode rnd) (2 := Gx)...
185
refine (proj2 (r_to_fp_correct _ _ _)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
186
rewrite round_generic...
187 188 189 190 191
Qed.

Definition r_to_fp_aux (m:mode) (r r1 r2:R) :=
  mk_fp (r_to_fp (rnd_of_mode m) r) r1 r2.

192 193 194 195
(* Why3 goal *)
Definition round: floating_point.Rounding.mode -> R -> R.
exact (fun m => round radix2 fexp (round_mode (rnd_of_mode m))).
Defined.
196

197
(* Why3 assumption *)
198 199
Definition round_error(x:t): R := (Rabs ((value x) - (exact x))%R).

200
(* Why3 assumption *)
201 202
Definition total_error(x:t): R := (Rabs ((value x) - (model x))%R).

203 204 205 206
(* Why3 goal *)
Definition max: R.
exact (F2R (Float radix2 (Zpower 2 prec - 1) (emax - prec))).
Defined.
207

208
(* Why3 assumption *)
209 210 211
Definition no_overflow(m:floating_point.Rounding.mode) (x:R): Prop :=
  ((Rabs (round m x)) <= max)%R.

212
(* Why3 goal *)
213 214
Lemma Bounded_real_no_overflow : forall (m:floating_point.Rounding.mode)
  (x:R), ((Rabs x) <= max)%R -> (no_overflow m x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
215
Proof with auto with typeclass_instances.
216 217 218
intros m x Hx.
apply Rabs_le.
assert (generic_format radix2 fexp max).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
219 220
apply generic_format_F2R.
intros H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
221 222 223
unfold cexp.
rewrite mag_F2R with (1 := H).
rewrite (mag_unique _ _ prec).
224
ring_simplify (prec + (emax - prec))%Z.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
225
unfold FLT_exp.
226 227 228
rewrite Zmax_l.
apply Zle_refl.
unfold emin.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
229
generalize Hprec' Hemax' ; clear ; omega.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
230
rewrite <- abs_IZR, Zabs_eq, <- 2!IZR_Zpower.
231
split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
232
apply IZR_le.
233 234 235
apply Zlt_succ_le.
change (2 ^ prec - 1)%Z with (Zpred (2^prec))%Z.
rewrite <- Zsucc_pred.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
236
apply lt_IZR.
237
change 2%Z with (radix_val radix2).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
238
rewrite 2!IZR_Zpower.
239 240 241 242 243
apply bpow_lt.
apply Zlt_pred.
apply Zlt_le_weak.
exact Hprec'.
generalize Hprec' ; clear ; omega.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
244
apply IZR_lt.
245 246 247 248 249 250 251 252 253 254 255 256 257
apply Zlt_pred.
apply Zlt_le_weak.
exact Hprec'.
generalize Hprec' ; clear ; omega.
apply Zlt_succ_le.
change (2 ^ prec - 1)%Z with (Zpred (2^prec))%Z.
rewrite <- Zsucc_pred.
change 2%Z with (radix_val radix2).
apply Zpower_gt_0.
apply Zlt_le_weak.
exact Hprec'.
generalize (Rabs_le_inv _ _ Hx).
split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
258
apply round_ge_generic...
259
now apply generic_format_opp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
260 261 262
apply H0.
apply round_le_generic...
apply H0.
263 264
Qed.

265
(* Why3 goal *)
266 267
Lemma Round_monotonic : forall (m:floating_point.Rounding.mode) (x:R) (y:R),
  (x <= y)%R -> ((round m x) <= (round m y))%R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
268
Proof with auto with typeclass_instances.
269
intros m x y Hxy.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
270
apply round_le with (3 := Hxy)...
271 272
Qed.

273
(* Why3 goal *)
274 275 276
Lemma Round_idempotent : forall (m1:floating_point.Rounding.mode)
  (m2:floating_point.Rounding.mode) (x:R), ((round m1 (round m2
  x)) = (round m2 x)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
277
Proof with auto with typeclass_instances.
278
intros m1 m2 x.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
279 280
apply round_generic...
apply generic_format_round...
281 282
Qed.

283
(* Why3 goal *)
284 285
Lemma Round_value : forall (m:floating_point.Rounding.mode) (x:t), ((round m
  (value x)) = (value x)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
286
Proof with auto with typeclass_instances.
287
intros m x.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
288
apply round_generic...
289 290 291
apply generic_format_B2R.
Qed.

292
(* Why3 goal *)
293
Lemma Bounded_value : forall (x:t), ((Rabs (value x)) <= max)%R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
294
Proof with auto with typeclass_instances.
295 296
intros x.
replace max with (pred radix2 fexp (bpow radix2 emax)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
297
apply pred_ge_gt...
298 299 300
apply generic_format_abs.
apply generic_format_B2R.
apply generic_format_bpow.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
301
unfold FLT_exp, emin.
302
zify ; generalize Hprec' Hemax' ; omega.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
303
apply abs_B2R_lt_emax.
304 305
rewrite pred_eq_pos.
unfold pred_pos.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
306
rewrite mag_bpow.
307
ring_simplify (emax+1-1)%Z.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
308 309
rewrite Req_bool_true by easy.
unfold FLT_exp, emin.
310 311 312 313 314
rewrite Zmax_l.
unfold max, F2R; simpl.
pattern emax at 1; replace emax with (prec+(emax-prec))%Z by ring.
rewrite bpow_plus.
change 2%Z with (radix_val radix2).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
315
rewrite minus_IZR, IZR_Zpower.
316 317 318
simpl; ring.
apply Zlt_le_weak.
exact Hprec'.
319
generalize Hprec' Hemax' ; omega.
320
apply bpow_ge_0.
321 322
Qed.

323 324 325 326
(* Why3 goal *)
Definition max_representable_integer: Z.
exact (Zpower 2 prec).
Defined.
327

328
(* Why3 goal *)
329 330 331
Lemma Exact_rounding_for_integers : forall (m:floating_point.Rounding.mode)
  (i:Z), (((-max_representable_integer)%Z <= i)%Z /\
  (i <= max_representable_integer)%Z) -> ((round m (IZR i)) = (IZR i)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
332
Proof with auto with typeclass_instances.
333
intros m z Hz.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
334
apply round_generic...
335 336 337
assert (Zabs z <= max_representable_integer)%Z.
apply Abs_le with (1:=Hz).
destruct (Zle_lt_or_eq _ _ H) as [Bz|Bz] ; clear H Hz.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
338
apply generic_format_FLT.
339
exists (Float radix2 z 0).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
340
unfold F2R ; simpl.
341
now rewrite Rmult_1_r.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
342 343
easy.
simpl; unfold emin; generalize Hprec' Hemax'; omega.
344 345
unfold max_representable_integer in Bz.
change 2%Z with (radix_val radix2) in Bz.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
346
apply generic_format_abs_inv.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
347
rewrite <- abs_IZR, Bz, IZR_Zpower.
348
apply generic_format_bpow.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
349
unfold FLT_exp, emin.
350
clear Bz; generalize Hprec' Hemax'; zify.
351 352 353 354 355
omega.
apply Zlt_le_weak.
apply Hprec'.
Qed.

356
(* Why3 goal *)
357 358
Lemma Round_down_le : forall (x:R), ((round floating_point.Rounding.Down
  x) <= x)%R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
359
Proof with auto with typeclass_instances.
360
intros x.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
361
apply round_DN_pt...
362 363
Qed.

364
(* Why3 goal *)
365 366
Lemma Round_up_ge : forall (x:R), (x <= (round floating_point.Rounding.Up
  x))%R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
367
Proof with auto with typeclass_instances.
368
intros x.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
369
apply round_UP_pt...
370 371
Qed.

372
(* Why3 goal *)
373 374
Lemma Round_down_neg : forall (x:R), ((round floating_point.Rounding.Down
  (-x)%R) = (-(round floating_point.Rounding.Up x))%R).
375
Proof.
376 377 378 379
intros x.
apply round_opp.
Qed.

380
(* Why3 goal *)
381 382
Lemma Round_up_neg : forall (x:R), ((round floating_point.Rounding.Up
  (-x)%R) = (-(round floating_point.Rounding.Down x))%R).
383
Proof.
384 385 386 387 388 389
intros x.
pattern x at 2 ; rewrite <- Ropp_involutive.
rewrite Round_down_neg.
now rewrite Ropp_involutive.
Qed.

390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408
(* Why3 goal *)
Definition round_logic: floating_point.Rounding.mode -> R -> t.
exact (fun m r => r_to_fp_aux m r r r).
Defined.

(* Why3 goal *)
Lemma Round_logic_def : forall (m:floating_point.Rounding.mode) (x:R),
  (no_overflow m x) -> ((value (round_logic m x)) = (round m x)).
Proof.
intros m x h1.
unfold value, round_logic.
simpl.
apply r_to_fp_correct.
apply Rle_lt_trans with (1 := h1).
replace emax with (prec + (emax - prec))%Z by ring.
rewrite bpow_plus.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
409 410
rewrite <- IZR_Zpower.
apply IZR_lt.
411 412 413 414 415
apply Zlt_pred.
apply Zlt_le_weak.
exact Hprec'.
Qed.

416
End GenFloat.