Fcore_ulp.v 59.7 KB
Newer Older
1
(**
2
3
4
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

5
Copyright (C) 2010-2013 Sylvie Boldo
6
#<br />#
7
Copyright (C) 2010-2013 Guillaume Melquiond
8
9
10
11
12
13
14
15
16
17
18
19

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.

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.
*)

BOLDO Sylvie's avatar
BOLDO Sylvie committed
20
(** * Unit in the Last Place: our definition using fexp and its properties, successor and predecessor *)
21
22
23
24
25
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_generic_fmt.
Require Import Fcore_float_prop.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
26

27
Section Fcore_ulp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
28
29
30

Variable beta : radix.

31
Notation bpow e := (bpow beta e).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
32
33
34

Variable fexp : Z -> Z.

35
36
37
(** Definition and basic properties about the minimal exponent, when it exists *)

Lemma Z_le_dec_aux: forall x y : Z, (x <= y)%Z \/ ~ (x <= y)%Z.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
38
Proof.
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
intros.
destruct (Z_le_dec x y).
now left.
now right.
Qed.


(** [negligible_exp] is either none (as in FLX) or Some n such that n <= fexp n. *)
Definition negligible_exp: option Z :=
  match (LPO_Z _ (fun z => Z_le_dec_aux z (fexp z))) with
   | inleft N => Some (proj1_sig N)
   | inright _ => None
 end.


54
55
56
57
58
59
60
61
62
63
64
65
Inductive negligible_exp_prop: option Z -> Prop :=
  | negligible_None: (forall n, (fexp n < n)%Z) -> negligible_exp_prop None
  | negligible_Some: forall n, (n <= fexp n)%Z -> negligible_exp_prop (Some n).


Lemma negligible_exp_spec: negligible_exp_prop negligible_exp.
Proof.
unfold negligible_exp; destruct LPO_Z as [(n,Hn)|Hn].
now apply negligible_Some.
apply negligible_None.
intros n; specialize (Hn n); omega.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
66
67
68
69
70
71
72
73
74

Lemma negligible_exp_spec': (negligible_exp = None /\ forall n, (fexp n < n)%Z)
           \/ exists n, (negligible_exp = Some n /\ (n <= fexp n)%Z).
Proof.
unfold negligible_exp; destruct LPO_Z as [(n,Hn)|Hn].
right; simpl; exists n; now split.
left; split; trivial.
intros n; specialize (Hn n); omega.
Qed.
75

76
Context { valid_exp : Valid_exp fexp }.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
77

78
79
80
81
82
83
84
85
86
87
Lemma fexp_negligible_exp_eq: forall n m, (n <= fexp n)%Z -> (m <= fexp m)%Z -> fexp n = fexp m.
Proof.
intros n m Hn Hm.
case (Zle_or_lt n m); intros H.
apply valid_exp; omega.
apply sym_eq, valid_exp; omega.
Qed.


(** Definition and basic properties about the ulp *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
88
89
90
91
92
93
(** Now includes a nice ulp(0): ulp(0) is now 0 when there is no minimal
   exponent, such as in FLX, and beta^(fexp n) when there is a n such
   that n <= fexp n. For instance, the value of ulp(O) is then
   beta^emin in FIX and FLT. The main lemma to use is ulp_neq_0 that
   is equivalent to the previous "unfold ulp" provided the value is
   not zero. *)
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108

Definition ulp x := match Req_bool x 0 with
  | true   => match negligible_exp with
            | Some n => bpow (fexp n)
            | None => 0%R
            end
  | false  => bpow (canonic_exp beta fexp x)
 end.

Lemma ulp_neq_0 : forall x:R, (x <> 0)%R -> ulp x = bpow (canonic_exp beta fexp x).
Proof.
intros  x Hx.
unfold ulp; case (Req_bool_spec x); trivial.
intros H; now contradict H.
Qed.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
109

110
Notation F := (generic_format beta fexp).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
111

112
113
114
115
116
Theorem ulp_opp :
  forall x, ulp (- x) = ulp x.
Proof.
intros x.
unfold ulp.
117
118
119
120
case Req_bool_spec; intros H1.
rewrite Req_bool_true; trivial.
rewrite <- (Ropp_involutive x), H1; ring.
rewrite Req_bool_false.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
121
now rewrite canonic_exp_opp.
122
intros H2; apply H1; rewrite H2; ring.
123
124
125
126
127
128
Qed.

Theorem ulp_abs :
  forall x, ulp (Rabs x) = ulp x.
Proof.
intros x.
129
130
131
132
unfold ulp; case (Req_bool_spec x 0); intros H1.
rewrite Req_bool_true; trivial.
now rewrite H1, Rabs_R0.
rewrite Req_bool_false.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
133
now rewrite canonic_exp_abs.
134
135
136
now apply Rabs_no_R0.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
137
Theorem ulp_ge_0:
138
139
140
141
142
143
144
  forall x, (0 <= ulp x)%R.
Proof.
intros x; unfold ulp; case Req_bool_spec; intros.
case negligible_exp; intros.
apply bpow_ge_0.
apply Rle_refl.
apply bpow_ge_0.
145
146
Qed.

147

148
Theorem ulp_le_id:
149
  forall x,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
150
    (0 < x)%R ->
151
    F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
152
153
154
155
156
    (ulp x <= x)%R.
Proof.
intros x Zx Fx.
rewrite <- (Rmult_1_l (ulp x)).
pattern x at 2; rewrite Fx.
157
158
159
rewrite ulp_neq_0.
2: now apply Rgt_not_eq.
unfold F2R; simpl.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
160
161
apply Rmult_le_compat_r.
apply bpow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
162
apply (Z2R_le (Zsucc 0)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
163
apply Zlt_le_succ.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
164
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
165
166
167
168
now rewrite <- Fx.
Qed.

Theorem ulp_le_abs:
169
  forall x,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
170
    (x <> 0)%R ->
171
    F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
172
173
174
    (ulp x <= Rabs x)%R.
Proof.
intros x Zx Fx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
175
rewrite <- ulp_abs.
176
apply ulp_le_id.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
177
178
now apply Rabs_pos_lt.
now apply generic_format_abs.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
179
180
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
181
182
183

(* was ulp_DN_UP *)
Theorem round_UP_DN_ulp :
184
  forall x, ~ F x ->
185
  round beta fexp Zceil x = (round beta fexp Zfloor x + ulp x)%R.
186
Proof.
187
intros x Fx.
188
189
rewrite ulp_neq_0.
unfold round. simpl.
190
191
unfold F2R. simpl.
rewrite Zceil_floor_neq.
192
rewrite Z2R_plus. simpl.
193
ring.
194
intros H.
195
apply Fx.
196
unfold generic_format, F2R. simpl.
197
198
199
rewrite <- H.
rewrite Ztrunc_Z2R.
rewrite H.
200
now rewrite scaled_mantissa_mult_bpow.
201
202
203
204
205
206
207
208
intros V; apply Fx.
rewrite V.
apply generic_format_0.
Qed.


Theorem ulp_bpow :
  forall e, ulp (bpow e) = bpow (fexp (e + 1)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
209
Proof.
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
intros e.
rewrite ulp_neq_0.
apply f_equal.
apply canonic_exp_fexp.
rewrite Rabs_pos_eq.
split.
ring_simplify (e + 1 - 1)%Z.
apply Rle_refl.
apply bpow_lt.
apply Zlt_succ.
apply bpow_ge_0.
apply Rgt_not_eq, Rlt_gt, bpow_gt_0.
Qed.


Lemma generic_format_ulp_0:
  F (ulp 0).
Proof.
unfold ulp.
rewrite Req_bool_true; trivial.
case negligible_exp_spec.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
231
232
intros _; apply generic_format_0.
intros n H1.
233
234
235
236
237
238
239
240
241
242
apply generic_format_bpow.
now apply valid_exp.
Qed.

Lemma generic_format_bpow_ge_ulp_0:  forall e,
    (ulp 0 <= bpow e)%R -> F (bpow e).
Proof.
intros e; unfold ulp.
rewrite Req_bool_true; trivial.
case negligible_exp_spec.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
243
intros H1 _.
244
apply generic_format_bpow.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
245
246
specialize (H1 (e+1)%Z); omega.
intros n H1 H2.
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
apply generic_format_bpow.
case (Zle_or_lt (e+1) (fexp (e+1))); intros H4.
absurd (e+1 <= e)%Z.
omega.
apply Zle_trans with (1:=H4).
replace (fexp (e+1)) with (fexp n).
now apply le_bpow with beta.
now apply fexp_negligible_exp_eq.
omega.
Qed.

(** The three following properties are equivalent:
      [Exp_not_FTZ] ;  forall x, F (ulp x) ; forall x, ulp 0 <= ulp x *)

Lemma generic_format_ulp: Exp_not_FTZ fexp ->
  forall x,  F (ulp x).
Proof.
unfold Exp_not_FTZ; intros H x.
case (Req_dec x 0); intros Hx.
rewrite Hx; apply generic_format_ulp_0.
rewrite (ulp_neq_0 _ Hx).
apply generic_format_bpow; unfold canonic_exp.
apply H.
Qed.

Lemma not_FTZ_generic_format_ulp:
   (forall x,  F (ulp x)) -> Exp_not_FTZ fexp.
intros H e.
specialize (H (bpow (e-1))).
rewrite ulp_neq_0 in H.
2: apply Rgt_not_eq, bpow_gt_0.
unfold canonic_exp in H.
rewrite ln_beta_bpow in H.
apply generic_format_bpow_inv' in H...
now replace (e-1+1)%Z with e in H by ring.
Qed.


Lemma ulp_ge_ulp_0: Exp_not_FTZ fexp ->
  forall x,  (ulp 0 <= ulp x)%R.
Proof.
unfold Exp_not_FTZ; intros H x.
case (Req_dec x 0); intros Hx.
rewrite Hx; now right.
unfold ulp at 1.
rewrite Req_bool_true; trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
293
294
case negligible_exp_spec'.
intros (H1,H2); rewrite H1; apply ulp_ge_0.
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
intros (n,(H1,H2)); rewrite H1.
rewrite ulp_neq_0; trivial.
apply bpow_le; unfold canonic_exp.
generalize (ln_beta beta x); intros l.
case (Zle_or_lt l (fexp l)); intros Hl.
rewrite (fexp_negligible_exp_eq n l); trivial; apply Zle_refl.
case (Zle_or_lt (fexp n) (fexp l)); trivial; intros K.
absurd (fexp n <= fexp l)%Z.
omega.
apply Zle_trans with (2:= H _).
apply Zeq_le, sym_eq, valid_exp; trivial.
omega.
Qed.

Lemma not_FTZ_ulp_ge_ulp_0:
   (forall x,  (ulp 0 <= ulp x)%R) -> Exp_not_FTZ fexp.
Proof.
intros H e.
apply generic_format_bpow_inv' with beta.
apply generic_format_bpow_ge_ulp_0.
replace e with ((e-1)+1)%Z by ring.
rewrite <- ulp_bpow.
apply H.
Qed.



Theorem ulp_le_pos :
  forall { Hm : Monotone_exp fexp },
  forall x y: R,
  (0 <= x)%R -> (x <= y)%R ->
  (ulp x <= ulp y)%R.
Proof with auto with typeclass_instances.
intros Hm x y Hx Hxy.
destruct Hx as [Hx|Hx].
rewrite ulp_neq_0.
rewrite ulp_neq_0.
apply bpow_le.
apply Hm.
now apply ln_beta_le.
apply Rgt_not_eq, Rlt_gt.
now apply Rlt_le_trans with (1:=Hx).
now apply Rgt_not_eq.
rewrite <- Hx.
apply ulp_ge_ulp_0.
apply monotone_exp_not_FTZ...
Qed.


Theorem ulp_le :
  forall { Hm : Monotone_exp fexp },
  forall x y: R,
  (Rabs x <= Rabs y)%R ->
  (ulp x <= ulp y)%R.
Proof.
intros Hm x y Hxy.
rewrite <- ulp_abs.
rewrite <- (ulp_abs y).
apply ulp_le_pos; trivial.
apply Rabs_pos.
Qed.



(** Definition and properties of pred and succ *)

Definition pred_pos x :=
  if Req_bool x (bpow (ln_beta beta x - 1)) then
    (x - bpow (fexp (ln_beta beta x - 1)))%R
  else
    (x - ulp x)%R.

Definition succ x :=
   if (Rle_bool 0 x) then
          (x+ulp x)%R
   else
     (- pred_pos (-x))%R.

Definition pred x := (- succ (-x))%R.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
375
Theorem pred_eq_pos:
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
  forall x, (0 <= x)%R -> (pred x = pred_pos x)%R.
Proof.
intros x Hx; unfold pred, succ.
case Rle_bool_spec; intros Hx'.
assert (K:(x = 0)%R).
apply Rle_antisym; try assumption.
apply Ropp_le_cancel.
now rewrite Ropp_0.
rewrite K; unfold pred_pos.
rewrite Req_bool_false.
2: apply Rlt_not_eq, bpow_gt_0.
rewrite Ropp_0; ring.
now rewrite 2!Ropp_involutive.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
391
Theorem succ_eq_pos:
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
  forall x, (0 <= x)%R -> (succ x = x + ulp x)%R.
Proof.
intros x Hx; unfold succ.
now rewrite Rle_bool_true.
Qed.

Lemma pred_eq_opp_succ_opp: forall x, pred x = (- succ (-x))%R.
Proof.
reflexivity.
Qed.

Lemma succ_eq_opp_pred_opp: forall x, succ x = (- pred (-x))%R.
Proof.
intros x; unfold pred.
now rewrite 2!Ropp_involutive.
Qed.

Lemma succ_opp: forall x, (succ (-x) = - pred x)%R.
Proof.
intros x; rewrite succ_eq_opp_pred_opp.
now rewrite Ropp_involutive.
Qed.

Lemma pred_opp: forall x, (pred (-x) = - succ x)%R.
Proof.
intros x; rewrite pred_eq_opp_succ_opp.
now rewrite Ropp_involutive.
Qed.



423

424
425
(** pred and succ are in the format *)

426
427
428
(* cannont be x <> ulp 0, due to the counter-example 1-bit FP format fexp: e -> e-1 *)
(* was pred_ge_bpow *)
Theorem id_m_ulp_ge_bpow :
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
  forall x e,  F x ->
  x <> ulp x ->
  (bpow e < x)%R ->
  (bpow e <= x - ulp x)%R.
Proof.
intros x e Fx Hx' Hx.
(* *)
assert (1 <= Ztrunc (scaled_mantissa beta fexp x))%Z.
assert (0 <  Ztrunc (scaled_mantissa beta fexp x))%Z.
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
rewrite <- Fx.
apply Rle_lt_trans with (2:=Hx).
apply bpow_ge_0.
omega.
case (Zle_lt_or_eq _ _ H); intros Hm.
(* *)
pattern x at 1 ; rewrite Fx.
rewrite ulp_neq_0.
unfold F2R. simpl.
pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
rewrite <- Rmult_minus_distr_r.
change 1%R with (Z2R 1).
rewrite <- Z2R_minus.
change (bpow e <= F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) - 1) (canonic_exp beta fexp x)))%R.
apply bpow_le_F2R_m1; trivial.
now rewrite <- Fx.
apply Rgt_not_eq, Rlt_gt.
apply Rlt_trans with (2:=Hx), bpow_gt_0.
(* *)
contradict Hx'.
pattern x at 1; rewrite Fx.
rewrite  <- Hm.
rewrite ulp_neq_0.
unfold F2R; simpl.
now rewrite Rmult_1_l.
apply Rgt_not_eq, Rlt_gt.
apply Rlt_trans with (2:=Hx), bpow_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
466
467
Qed.

468
469
(* was succ_le_bpow *)
Theorem id_p_ulp_le_bpow :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
470
471
472
473
474
475
  forall x e, (0 < x)%R -> F x ->
  (x < bpow e)%R ->
  (x + ulp x <= bpow e)%R.
Proof.
intros x e Zx Fx Hx.
pattern x at 1 ; rewrite Fx.
476
477
rewrite ulp_neq_0.
unfold F2R. simpl.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
478
pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
479
480
rewrite <- Rmult_plus_distr_r.
change 1%R with (Z2R 1).
481
rewrite <- Z2R_plus.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
482
change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exp beta fexp x)) <= bpow e)%R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
483
apply F2R_p1_le_bpow.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
484
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
485
486
now rewrite <- Fx.
now rewrite <- Fx.
487
now apply Rgt_not_eq.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
488
489
Qed.

490
491


BOLDO Sylvie's avatar
BOLDO Sylvie committed
492
Lemma generic_format_pred_aux1:
493
  forall x, (0 < x)%R -> F x ->
494
495
  x <> bpow (ln_beta beta x - 1) ->
  F (x - ulp x).
496
Proof.
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
intros x Zx Fx Hx.
destruct (ln_beta beta x) as (ex, Ex).
simpl in Hx.
specialize (Ex (Rgt_not_eq _ _ Zx)).
assert (Ex' : (bpow (ex - 1) < x < bpow ex)%R).
rewrite Rabs_pos_eq in Ex.
destruct Ex as (H,H'); destruct H; split; trivial.
contradict Hx; easy.
now apply Rlt_le.
unfold generic_format, scaled_mantissa, canonic_exp.
rewrite ln_beta_unique with beta (x - ulp x)%R ex.
pattern x at 1 3 ; rewrite Fx.
rewrite ulp_neq_0.
unfold scaled_mantissa.
rewrite canonic_exp_fexp with (1 := Ex).
unfold F2R. simpl.
rewrite Rmult_minus_distr_r.
rewrite Rmult_assoc.
rewrite <- bpow_plus, Zplus_opp_r, Rmult_1_r.
change (bpow 0) with (Z2R 1).
rewrite <- Z2R_minus.
rewrite Ztrunc_Z2R.
rewrite Z2R_minus.
rewrite Rmult_minus_distr_r.
now rewrite Rmult_1_l.
now apply Rgt_not_eq.
523
524
rewrite Rabs_pos_eq.
split.
525
apply id_m_ulp_ge_bpow; trivial.
526
527
528
529
530
531
532
533
534
535
536
537
rewrite ulp_neq_0.
intro H.
assert (ex-1 < canonic_exp beta fexp x  < ex)%Z.
split ; apply (lt_bpow beta) ; rewrite <- H ; easy.
clear -H0. omega.
now apply Rgt_not_eq.
apply Ex'.
apply Rle_lt_trans with (2 := proj2 Ex').
pattern x at 3 ; rewrite <- Rplus_0_r.
apply Rplus_le_compat_l.
rewrite <-Ropp_0.
apply Ropp_le_contravar.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
538
apply ulp_ge_0.
539
540
541
542
543
544
545
546
547
548
apply Rle_0_minus.
pattern x at 2; rewrite Fx.
rewrite ulp_neq_0.
unfold F2R; simpl.
pattern (bpow (canonic_exp beta fexp x)) at 1; rewrite <- Rmult_1_l.
apply Rmult_le_compat_r.
apply bpow_ge_0.
replace 1%R with (Z2R 1) by reflexivity.
apply Z2R_le.
assert (0 <  Ztrunc (scaled_mantissa beta fexp x))%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
549
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
550
551
552
553
554
rewrite <- Fx.
apply Rle_lt_trans with (2:=proj1 Ex').
apply bpow_ge_0.
omega.
now apply Rgt_not_eq.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
555
556
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
557
Lemma generic_format_pred_aux2 :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
558
  forall x, (0 < x)%R -> F x ->
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
  let e := ln_beta_val beta x (ln_beta beta x) in
  x =  bpow (e - 1) ->
  F (x - bpow (fexp (e - 1))).
Proof.
intros x Zx Fx e Hx.
pose (f:=(x - bpow (fexp (e - 1)))%R).
fold f.
assert (He:(fexp (e-1) <= e-1)%Z).
apply generic_format_bpow_inv with beta; trivial.
rewrite <- Hx; assumption.
case (Zle_lt_or_eq _ _ He); clear He; intros He.
assert (f = F2R (Float beta (Zpower beta (e-1-(fexp (e-1))) -1) (fexp (e-1))))%R.
unfold f; rewrite Hx.
unfold F2R; simpl.
rewrite Z2R_minus, Z2R_Zpower.
rewrite Rmult_minus_distr_r, Rmult_1_l.
rewrite <- bpow_plus.
now replace (e - 1 - fexp (e - 1) + fexp (e - 1))%Z with (e-1)%Z by ring.
omega.
rewrite H.
apply generic_format_F2R.
intros _.
apply Zeq_le.
apply canonic_exp_fexp.
rewrite <- H.
unfold f; rewrite Hx.
rewrite Rabs_right.
586
split.
587
588
589
590
591
592
apply Rplus_le_reg_l with (bpow (fexp (e-1))).
ring_simplify.
apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R.
apply Rplus_le_compat ; apply bpow_le ; omega.
apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac].
apply Rle_trans with (bpow 1*bpow (e - 2))%R.
593
594
apply Rmult_le_compat_r.
apply bpow_ge_0.
595
596
597
598
599
600
601
602
replace 2%R with (Z2R 2) by reflexivity.
replace (bpow 1) with (Z2R beta).
apply Z2R_le.
apply <- Zle_is_le_bool.
now destruct beta.
simpl.
unfold Zpower_pos; simpl.
now rewrite Zmult_1_r.
603
rewrite <- bpow_plus.
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
replace (1+(e-2))%Z with (e-1)%Z by ring.
now right.
rewrite <- Rplus_0_r.
apply Rplus_lt_compat_l.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
apply bpow_gt_0.
apply Rle_ge; apply Rle_0_minus.
apply bpow_le.
omega.
replace f with 0%R.
apply generic_format_0.
unfold f.
rewrite Hx, He.
ring.
619
620
Qed.

621

BOLDO Sylvie's avatar
BOLDO Sylvie committed
622
Theorem generic_format_succ_aux1 :
623
624
625
626
627
628
629
630
  forall x, (0 < x)%R -> F x ->
  F (x + ulp x).
Proof.
intros x Zx Fx.
destruct (ln_beta beta x) as (ex, Ex).
specialize (Ex (Rgt_not_eq _ _ Zx)).
assert (Ex' := Ex).
rewrite Rabs_pos_eq in Ex'.
631
destruct (id_p_ulp_le_bpow x ex) ; try easy.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
632
unfold generic_format, scaled_mantissa, canonic_exp.
633
634
rewrite ln_beta_unique with beta (x + ulp x)%R ex.
pattern x at 1 3 ; rewrite Fx.
635
636
rewrite ulp_neq_0.
unfold scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
637
rewrite canonic_exp_fexp with (1 := Ex).
638
unfold F2R. simpl.
639
640
rewrite Rmult_plus_distr_r.
rewrite Rmult_assoc.
641
rewrite <- bpow_plus, Zplus_opp_r, Rmult_1_r.
642
change (bpow 0) with (Z2R 1).
643
rewrite <- Z2R_plus.
644
rewrite Ztrunc_Z2R.
645
rewrite Z2R_plus.
646
647
rewrite Rmult_plus_distr_r.
now rewrite Rmult_1_l.
648
now apply Rgt_not_eq.
649
650
651
652
653
rewrite Rabs_pos_eq.
split.
apply Rle_trans with (1 := proj1 Ex').
pattern x at 1 ; rewrite <- Rplus_0_r.
apply Rplus_le_compat_l.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
654
apply ulp_ge_0.
655
656
657
exact H.
apply Rplus_le_le_0_compat.
now apply Rlt_le.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
658
apply ulp_ge_0.
659
660
rewrite H.
apply generic_format_bpow.
661
apply valid_exp.
662
663
664
665
666
667
668
destruct (Zle_or_lt ex (fexp ex)) ; trivial.
elim Rlt_not_le with (1 := Zx).
rewrite Fx.
replace (Ztrunc (scaled_mantissa beta fexp x)) with Z0.
rewrite F2R_0.
apply Rle_refl.
unfold scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
669
rewrite canonic_exp_fexp with (1 := Ex).
670
671
672
673
674
675
676
677
destruct (mantissa_small_pos beta fexp x ex) ; trivial.
rewrite Ztrunc_floor.
apply sym_eq.
apply Zfloor_imp.
split.
now apply Rlt_le.
exact H2.
now apply Rlt_le.
678
679
680
now apply Rlt_le.
Qed.

681
682
683
Theorem generic_format_pred_pos :
  forall x, F x -> (0 < x)%R ->
  F (pred_pos x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
684
Proof.
685
686
intros x Fx Zx.
unfold pred_pos; case Req_bool_spec; intros H.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
687
688
now apply generic_format_pred_aux2.
now apply generic_format_pred_aux1.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
689
690
Qed.

691

692
693
694
Theorem generic_format_succ :
  forall x, F x ->
  F (succ x).
695
Proof.
696
697
698
intros x Fx.
unfold succ; case Rle_bool_spec; intros Zx.
destruct Zx as [Zx|Zx].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
699
now apply generic_format_succ_aux1.
700
701
702
703
704
705
rewrite <- Zx, Rplus_0_l.
apply generic_format_ulp_0.
apply generic_format_opp.
apply generic_format_pred_pos.
now apply generic_format_opp.
now apply Ropp_0_gt_lt_contravar.
706
707
Qed.

708
709
710
711
712
713
714
715
716
Theorem generic_format_pred :
  forall x, F x ->
  F (pred x).
Proof.
intros x Fx.
unfold pred.
apply generic_format_opp.
apply generic_format_succ.
now apply generic_format_opp.
717
718
Qed.

BOLDO Sylvie's avatar
Fpred    
BOLDO Sylvie committed
719

720
721
722
723
724
725
726
727
728

Theorem pred_pos_lt_id :
  forall x, (x <> 0)%R ->
  (pred_pos x < x)%R.
Proof.
intros x Zx.
unfold pred_pos.
case Req_bool_spec; intros H.
(* *)
BOLDO Sylvie's avatar
Fpred    
BOLDO Sylvie committed
729
730
731
732
733
rewrite <- Rplus_0_r.
apply Rplus_lt_compat_l.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
apply bpow_gt_0.
734
735
736
737
738
739
740
(* *)
rewrite <- Rplus_0_r.
apply Rplus_lt_compat_l.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
rewrite ulp_neq_0; trivial.
apply bpow_gt_0.
BOLDO Sylvie's avatar
Fpred    
BOLDO Sylvie committed
741
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
742

BOLDO Sylvie's avatar
BOLDO Sylvie committed
743
Theorem succ_gt_id :
744
745
  forall x, (x <> 0)%R ->
  (x < succ x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
746
Proof.
747
748
749
750
751
752
753
754
755
756
intros x Zx; unfold succ.
case Rle_bool_spec; intros Hx.
pattern x at 1; rewrite <- (Rplus_0_r x).
apply Rplus_lt_compat_l.
rewrite ulp_neq_0; trivial.
apply bpow_gt_0.
pattern x at 1; rewrite <- (Ropp_involutive x).
apply Ropp_lt_contravar.
apply pred_pos_lt_id.
now auto with real.
BOLDO Sylvie's avatar
Fpred    
BOLDO Sylvie committed
757
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
758

759
760
761
762
763
764
765
766

Theorem pred_lt_id :
  forall x,  (x <> 0)%R ->
  (pred x < x)%R.
Proof.
intros x Zx; unfold pred.
pattern x at 2; rewrite <- (Ropp_involutive x).
apply Ropp_lt_contravar.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
767
apply succ_gt_id.
768
769
770
now auto with real.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
771
Theorem succ_ge_id :
772
773
774
775
776
  forall x, (x <= succ x)%R.
Proof.
intros x; case (Req_dec x 0).
intros V; rewrite V.
unfold succ; rewrite Rle_bool_true;[idtac|now right].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
777
rewrite Rplus_0_l; apply ulp_ge_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
778
intros; left; now apply succ_gt_id.
779
780
781
782
783
784
785
786
787
Qed.


Theorem pred_le_id :
  forall x,  (pred x <= x)%R.
Proof.
intros x; unfold pred.
pattern x at 2; rewrite <- (Ropp_involutive x).
apply Ropp_le_contravar.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
788
apply succ_ge_id.
789
790
791
792
793
794
Qed.


Theorem pred_pos_ge_0 :
  forall x,
  (0 < x)%R -> F x -> (0 <= pred_pos x)%R.
795
Proof.
796
797
798
799
800
801
802
803
intros x Zx Fx.
unfold pred_pos.
case Req_bool_spec; intros H.
(* *)
apply Rle_0_minus.
rewrite H.
apply bpow_le.
destruct (ln_beta beta x) as (ex,Ex) ; simpl.
804
rewrite ln_beta_bpow.
805
806
807
808
ring_simplify (ex - 1 + 1 - 1)%Z.
apply generic_format_bpow_inv with beta; trivial.
simpl in H.
rewrite <- H; assumption.
809
apply Rle_0_minus.
810
now apply ulp_le_id.
811
812
Qed.

813
814
815
Theorem pred_ge_0 :
  forall x,
  (0 < x)%R -> F x -> (0 <= pred x)%R.
816
Proof.
817
intros x Zx Fx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
818
rewrite pred_eq_pos.
819
820
now apply pred_pos_ge_0.
now left.
821
822
Qed.

823

BOLDO Sylvie's avatar
BOLDO Sylvie committed
824
Lemma pred_pos_plus_ulp_aux1 :
825
  forall x, (0 < x)%R -> F x ->
826
  x <> bpow (ln_beta beta x - 1) ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
827
  ((x - ulp x) + ulp (x-ulp x) = x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
828
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
829
830
831
intros x Zx Fx Hx.
replace (ulp (x - ulp x)) with (ulp x).
ring.
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
assert (H:(x <> 0)%R) by auto with real.
assert (H':(x <> bpow (canonic_exp beta fexp x))%R).
unfold canonic_exp; intros M.
case_eq (ln_beta beta x); intros ex Hex T.
assert (Lex:(ln_beta_val beta x (ln_beta beta x) = ex)%Z).
rewrite T; reflexivity.
rewrite Lex in *.
clear T; simpl in *; specialize (Hex H).
rewrite Rabs_right in Hex.
2: apply Rle_ge; apply Rlt_le; easy.
assert (ex-1 < fexp ex  < ex)%Z.
split ; apply (lt_bpow beta); rewrite <- M;[idtac|easy].
destruct (proj1 Hex);[trivial|idtac].
contradict Hx; auto with real.
omega.
rewrite 2!ulp_neq_0; try auto with real.
apply f_equal.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
849
unfold canonic_exp; apply f_equal.
850
851
852
853
case_eq (ln_beta beta x); intros ex Hex T.
assert (Lex:(ln_beta_val beta x (ln_beta beta x) = ex)%Z).
rewrite T; reflexivity.
rewrite Lex in *; simpl in *; clear T.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
854
specialize (Hex H).
855
apply sym_eq, ln_beta_unique.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
856
857
858
859
860
rewrite Rabs_right.
rewrite Rabs_right in Hex.
2: apply Rle_ge; apply Rlt_le; easy.
split.
destruct Hex as ([H1|H1],H2).
861
apply Rle_trans with (x-ulp x)%R.
862
apply id_m_ulp_ge_bpow; trivial.
863
864
865
rewrite ulp_neq_0; trivial.
rewrite ulp_neq_0; trivial.
right; unfold canonic_exp; now rewrite Lex.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
866
867
868
869
870
871
872
873
874
contradict Hx; auto with real.
apply Rle_lt_trans with (2:=proj2 Hex).
rewrite <- Rplus_0_r.
apply Rplus_le_compat_l.
rewrite <- Ropp_0.
apply Ropp_le_contravar.
apply bpow_ge_0.
apply Rle_ge.
apply Rle_0_minus.
875
876
877
878
rewrite Fx.
unfold F2R, canonic_exp; simpl.
rewrite Lex.
pattern (bpow (fexp ex)) at 1; rewrite <- Rmult_1_l.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
879
880
881
882
883
apply Rmult_le_compat_r.
apply bpow_ge_0.
replace 1%R with (Z2R (Zsucc 0)) by reflexivity.
apply Z2R_le.
apply Zlt_le_succ.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
884
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
885
886
887
now rewrite <- Fx.
Qed.

888

BOLDO Sylvie's avatar
BOLDO Sylvie committed
889
Lemma pred_pos_plus_ulp_aux2 :
890
  forall x, (0 < x)%R -> F x ->
891
  let e := ln_beta_val beta x (ln_beta beta x) in
BOLDO Sylvie's avatar
BOLDO Sylvie committed
892
893
894
  x =  bpow (e - 1) ->
  (x - bpow (fexp (e-1)) <> 0)%R ->
  ((x - bpow (fexp (e-1))) + ulp (x - bpow (fexp (e-1))) = x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
895
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
896
897
898
intros x Zx Fx e Hxe Zp.
replace (ulp (x - bpow (fexp (e - 1)))) with (bpow (fexp (e - 1))).
ring.
899
assert (He:(fexp (e-1) <= e-1)%Z).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
900
901
apply generic_format_bpow_inv with beta; trivial.
rewrite <- Hxe; assumption.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
902
903
case (Zle_lt_or_eq _ _ He); clear He; intros He.
(* *)
904
905
rewrite ulp_neq_0; trivial.
apply f_equal.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
906
unfold canonic_exp; apply f_equal.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
907
908
909
910
911
912
913
apply sym_eq.
apply ln_beta_unique.
rewrite Rabs_right.
split.
apply Rplus_le_reg_l with (bpow (fexp (e-1))).
ring_simplify.
apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R.
914
apply Rplus_le_compat; apply bpow_le; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
915
916
917
918
919
apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac].
apply Rle_trans with (bpow 1*bpow (e - 2))%R.
apply Rmult_le_compat_r.
apply bpow_ge_0.
replace 2%R with (Z2R 2) by reflexivity.
920
replace (bpow 1) with (Z2R beta).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
921
922
923
924
925
926
apply Z2R_le.
apply <- Zle_is_le_bool.
now destruct beta.
simpl.
unfold Zpower_pos; simpl.
now rewrite Zmult_1_r.
927
rewrite <- bpow_plus.
928
929
930
replace (1+(e-2))%Z with (e-1)%Z by ring.
now right.
rewrite <- Rplus_0_r, Hxe.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
931
932
933
934
apply Rplus_lt_compat_l.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
apply bpow_gt_0.
935
936
937
938
939
940
941
apply Rle_ge; apply Rle_0_minus.
rewrite Hxe.
apply bpow_le.
omega.
(* *)
contradict Zp.
rewrite Hxe, He; ring.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
942
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
943

BOLDO Sylvie's avatar
BOLDO Sylvie committed
944
Lemma pred_pos_plus_ulp_aux3 :
945
946
947
948
949
950
951
952
953
954
955
956
957
958
  forall x, (0 < x)%R -> F x ->
  let e := ln_beta_val beta x (ln_beta beta x) in
  x =  bpow (e - 1) ->
  (x - bpow (fexp (e-1)) = 0)%R ->
  (ulp 0 = x)%R.
Proof.
intros x Hx Fx e H1 H2.
assert (H3:(x = bpow (fexp (e - 1)))).
now apply Rminus_diag_uniq.
assert (H4: (fexp (e-1) = e-1)%Z).
apply bpow_inj with beta.
now rewrite <- H1.
unfold ulp; rewrite Req_bool_true; trivial.
case negligible_exp_spec.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
959
intros K.
960
961
specialize (K (e-1)%Z).
contradict K; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
962
intros n Hn.
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
rewrite H3; apply f_equal.
case (Zle_or_lt n (e-1)); intros H6.
apply valid_exp; omega.
apply sym_eq, valid_exp; omega.
Qed.




(** The following one is false for x = 0 in FTZ *)

Theorem pred_pos_plus_ulp :
  forall x, (0 < x)%R -> F x ->
  (pred_pos x + ulp (pred_pos x) = x)%R.
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
978
intros x Zx Fx.
979
unfold pred_pos.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
980
case Req_bool_spec; intros H.
981
982
case (Req_EM_T (x - bpow (fexp (ln_beta_val beta x (ln_beta beta x) -1))) 0); intros H1.
rewrite H1, Rplus_0_l.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
983
984
985
now apply pred_pos_plus_ulp_aux3.
now apply pred_pos_plus_ulp_aux2.
now apply pred_pos_plus_ulp_aux1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
986
987
Qed.

988
989
990



991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
(** Rounding x + small epsilon *)

Theorem ln_beta_plus_eps:
  forall x, (0 < x)%R -> F x ->
  forall eps, (0 <= eps < ulp x)%R ->
  ln_beta beta (x + eps) = ln_beta beta x :> Z.
Proof.
intros x Zx Fx eps Heps.
destruct (ln_beta beta x) as (ex, He).
simpl.
specialize (He (Rgt_not_eq _ _ Zx)).
apply ln_beta_unique.
rewrite Rabs_pos_eq.
rewrite Rabs_pos_eq in He.
split.
apply Rle_trans with (1 := proj1 He).
pattern x at 1 ; rewrite <- Rplus_0_r.
now apply Rplus_le_compat_l.
apply Rlt_le_trans with (x + ulp x)%R.
now apply Rplus_lt_compat_l.
pattern x at 1 ; rewrite Fx.
rewrite ulp_neq_0.
unfold F2R. simpl.
pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
rewrite <- Rmult_plus_distr_r.
change 1%R with (Z2R 1).
rewrite <- Z2R_plus.
change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exp beta fexp x)) <= bpow ex)%R.
apply F2R_p1_le_bpow.
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
now rewrite <- Fx.
now rewrite <- Fx.
now apply Rgt_not_eq.
now apply Rlt_le.
apply Rplus_le_le_0_compat.
now apply Rlt_le.
apply Heps.
Qed.

Theorem round_DN_plus_eps_pos:
  forall x, (0 <= x)%R -> F x ->
  forall eps, (0 <= eps < ulp x)%R ->
  round beta fexp Zfloor (x + eps) = x.
Proof.
intros x Zx Fx eps Heps.
destruct Zx as [Zx|Zx].
(* . 0 < x *)
pattern x at 2 ; rewrite Fx.
unfold round.
unfold scaled_mantissa. simpl.
unfold canonic_exp at 1 2.
rewrite ln_beta_plus_eps ; trivial.
apply (f_equal (fun m => F2R (Float beta m _))).
rewrite Ztrunc_floor.
apply Zfloor_imp.
split.
apply (Rle_trans _ _ _ (Zfloor_lb _)).
apply Rmult_le_compat_r.
apply bpow_ge_0.
pattern x at 1 ; rewrite <- Rplus_0_r.
now apply Rplus_le_compat_l.
apply Rlt_le_trans with ((x + ulp x) * bpow (- canonic_exp beta fexp x))%R.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
now apply Rplus_lt_compat_l.
rewrite Rmult_plus_distr_r.
rewrite Z2R_plus.
apply Rplus_le_compat.
pattern x at 1 3 ; rewrite Fx.
unfold F2R. simpl.
rewrite Rmult_assoc.
rewrite <- bpow_plus.
rewrite Zplus_opp_r.
rewrite Rmult_1_r.
rewrite Zfloor_Z2R.
apply Rle_refl.
rewrite ulp_neq_0.
2: now apply Rgt_not_eq.
rewrite <- bpow_plus.
rewrite Zplus_opp_r.
apply Rle_refl.
apply Rmult_le_pos.
now apply Rlt_le.
apply bpow_ge_0.
(* . x=0 *)
rewrite <- Zx, Rplus_0_l; rewrite <- Zx in Heps.
case (proj1 Heps); intros P.
unfold round, scaled_mantissa, canonic_exp.
revert Heps; unfold ulp.
rewrite Req_bool_true; trivial.
case negligible_exp_spec.
intros _ (H1,H2).
absurd (0 < 0)%R; auto with real.
now apply Rle_lt_trans with (1:=H1).
intros n Hn H.
assert (fexp (ln_beta beta eps) = fexp n).
apply valid_exp; try assumption.
assert(ln_beta beta eps-1 < fexp n)%Z;[idtac|omega].
apply lt_bpow with beta.
apply Rle_lt_trans with (2:=proj2 H).
destruct (ln_beta beta eps) as (e,He).
simpl; rewrite Rabs_pos_eq in He.
now apply He, Rgt_not_eq.
now left.
replace (Zfloor (eps * bpow (- fexp (ln_beta beta eps)))) with 0%Z.
unfold F2R; simpl; ring.
apply sym_eq, Zfloor_imp.
split.
apply Rmult_le_pos.
now left.
apply bpow_ge_0.
apply Rmult_lt_reg_r with (bpow (fexp n)).
apply bpow_gt_0.
rewrite Rmult_assoc, <- bpow_plus.
rewrite H0; ring_simplify (-fexp n + fexp n)%Z.
simpl; rewrite Rmult_1_l, Rmult_1_r.
apply H.
rewrite <- P, round_0; trivial.
apply valid_rnd_DN.
Qed.


Theorem round_UP_plus_eps_pos :
  forall x, (0 <= x)%R -> F x ->
  forall eps, (0 < eps <= ulp x)%R ->
  round beta fexp Zceil (x + eps) = (x + ulp x)%R.
Proof with auto with typeclass_instances.
intros x Zx Fx eps.
case Zx; intros Zx1.
(* . 0 < x *)
intros (Heps1,[Heps2|Heps2]).
assert (Heps: (0 <= eps < ulp x)%R).
split.
now apply Rlt_le.
exact Heps2.
assert (Hd := round_DN_plus_eps_pos x Zx Fx eps Heps).
rewrite round_UP_DN_ulp.
rewrite Hd.
rewrite 2!ulp_neq_0.
unfold canonic_exp.
now rewrite ln_beta_plus_eps.
now apply Rgt_not_eq.
now apply Rgt_not_eq, Rplus_lt_0_compat.
intros Fs.
rewrite round_generic in Hd...
apply Rgt_not_eq with (2 := Hd).
pattern x at 2 ; rewrite <- Rplus_0_r.
now apply Rplus_lt_compat_l.
rewrite Heps2.
apply round_generic...
now apply generic_format_succ_aux1.
(* . x=0 *)
rewrite <- Zx1, 2!Rplus_0_l.
intros Heps.
case (proj2 Heps).
unfold round, scaled_mantissa, canonic_exp.
unfold ulp.
rewrite Req_bool_true; trivial.
case negligible_exp_spec.
intros H2.
intros J; absurd (0 < 0)%R; auto with real.
apply Rlt_trans with eps; try assumption; apply Heps.
intros n Hn H.
assert (fexp (ln_beta beta eps) = fexp n).
apply valid_exp; try assumption.
assert(ln_beta beta eps-1 < fexp n)%Z;[idtac|omega].
apply lt_bpow with beta.
apply Rle_lt_trans with (2:=H).
destruct (ln_beta beta eps) as (e,He).
simpl; rewrite Rabs_pos_eq in He.
now apply He, Rgt_not_eq.
now left.
replace (Zceil (eps * bpow (- fexp (ln_beta beta eps)))) with 1%Z.
unfold F2R; simpl; rewrite H0; ring.
apply sym_eq, Zceil_imp.
split.
simpl; apply Rmult_lt_0_compat.
apply Heps.
apply bpow_gt_0.
apply Rmult_le_reg_r with (bpow (fexp n)).
apply bpow_gt_0.
rewrite Rmult_assoc, <- bpow_plus.
rewrite H0; ring_simplify (-fexp n + fexp n)%Z.
simpl; rewrite Rmult_1_l, Rmult_1_r.
now left.
intros P; rewrite P.
apply round_generic...
apply generic_format_ulp_0.
Qed.


Theorem round_UP_pred_plus_eps_pos :
1183
  forall x, (0 < x)%R -> F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1184
  forall eps, (0 < eps <= ulp (pred x) )%R ->
1185
  round beta fexp Zceil (pred x + eps) = x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1186
1187
Proof.
intros x Hx Fx eps Heps.
1188
rewrite round_UP_plus_eps_pos; trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1189
rewrite pred_eq_pos.
1190
1191
1192
apply pred_pos_plus_ulp; trivial.
now left.
now apply pred_ge_0.
1193
apply generic_format_pred; trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1194
Qed.
BOLDO Sylvie's avatar
Fpred    
BOLDO Sylvie committed
1195

1196
1197
Theorem round_DN_minus_eps_pos :
  forall x,  (0 < x)%R -> F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1198
  forall eps, (0 < eps <= ulp (pred x))%R ->
1199
  round beta fexp Zfloor (x - eps) = pred x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1200
Proof.
1201
intros x Hpx Fx eps.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1202
rewrite pred_eq_pos;[intros Heps|now left].
1203
1204
replace (x-eps)%R with (pred_pos x + (ulp (pred_pos x)-eps))%R.
2: pattern x at 3; rewrite <- (pred_pos_plus_ulp x); trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1205
2: ring.
1206
rewrite round_DN_plus_eps_pos; trivial.
1207
1208
now apply pred_pos_ge_0.
now apply generic_format_pred_pos.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1209
1210
1211
1212
1213
1214
1215
1216
1217
split.
apply Rle_0_minus.
now apply Heps.
rewrite <- Rplus_0_r.
apply Rplus_lt_compat_l.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
now apply Heps.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1218

BOLDO Sylvie's avatar
BOLDO Sylvie committed
1219

1220
1221
Theorem round_DN_plus_eps:
  forall x, F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1222
1223
  forall eps, (0 <= eps < if (Rle_bool 0 x) then (ulp x)
                                     else (ulp (pred (-x))))%R ->
1224
1225
1226
1227
1228
1229
  round beta fexp Zfloor (x + eps) = x.
Proof.
intros x Fx eps Heps.
case (Rle_or_lt 0 x); intros Zx.
apply round_DN_plus_eps_pos; try assumption.
split; try apply Heps.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1230
1231
rewrite Rle_bool_true in Heps; trivial.
now apply Heps.
1232
(* *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1233
rewrite Rle_bool_false in Heps; trivial.
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
rewrite <- (Ropp_involutive (x+eps)).
pattern x at 2; rewrite <- (Ropp_involutive x).
rewrite round_DN_opp.
apply f_equal.
replace (-(x+eps))%R with (pred (-x) + (ulp (pred (-x)) - eps))%R.
rewrite round_UP_pred_plus_eps_pos; try reflexivity.
now apply Ropp_0_gt_lt_contravar.
now apply generic_format_opp.
split.
apply Rplus_lt_reg_l with eps; ring_simplify.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1244
apply Heps.
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
apply Rplus_le_reg_l with (eps-ulp (pred (- x)))%R; ring_simplify.
apply Heps.
unfold pred.
rewrite Ropp_involutive.
unfold succ; rewrite Rle_bool_false; try assumption.
rewrite Ropp_involutive; unfold Rminus.
rewrite <- Rplus_assoc, pred_pos_plus_ulp.
ring.
now apply Ropp_0_gt_lt_contravar.
now apply generic_format_opp.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
1257

1258
1259
Theorem round_UP_plus_eps :
  forall x, F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1260
1261
  forall eps, (0 < eps <= if (Rle_bool 0 x) then (ulp x)
                                     else (ulp (pred (-x))))%R ->
1262
1263
1264
1265
1266
  round beta fexp Zceil (x + eps) = (succ x)%R.
Proof with auto with typeclass_instances.
intros x Fx eps Heps.
case (Rle_or_lt 0 x); intros Zx.
rewrite succ_eq_pos; try assumption.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1267
1268
rewrite Rle_bool_true in Heps; trivial.
apply round_UP_plus_eps_pos; assumption.
1269
(* *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1270
rewrite Rle_bool_false in Heps; trivial.
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
rewrite <- (Ropp_involutive (x+eps)).
rewrite <- (Ropp_involutive (succ x)).
rewrite round_UP_opp.
apply f_equal.
replace (-(x+eps))%R with (-succ x + (-eps + ulp (pred (-x))))%R.
apply round_DN_plus_eps_pos.
rewrite <- pred_opp.
apply pred_ge_0.
now apply Ropp_0_gt_lt_contravar.
now apply generic_format_opp.
now apply generic_format_opp, generic_format_succ.
split.
apply Rplus_le_reg_l with eps; ring_simplify.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1284
apply Heps.
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
unfold pred; rewrite Ropp_involutive.
apply Rplus_lt_reg_l with (eps-ulp (- succ x))%R; ring_simplify.
apply Heps.
unfold succ; rewrite Rle_bool_false; try assumption.
apply trans_eq with (-x +-eps)%R;[idtac|ring].
pattern (-x)%R at 3; rewrite <- (pred_pos_plus_ulp (-x)).
rewrite pred_eq_pos.
ring.
left; now apply Ropp_0_gt_lt_contravar.
now apply Ropp_0_gt_lt_contravar.
now apply generic_format_opp.
Qed.


1299
Lemma le_pred_pos_lt :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1300
1301
  forall x y,
  F x -> F y ->
1302
1303
  (0 <= x < y)%R ->
  (x <= pred_pos y)%R.
1304
Proof with auto with typeclass_instances.
1305
1306
intros x y Fx Fy H.
case (proj1 H); intros V.
1307
assert (Zy:(0 < y)%R).
1308
apply Rle_lt_trans with (1:=proj1 H).
1309
apply H.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1310
(* *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1311
1312
assert (Zp: (0 < pred y)%R).
assert (Zp:(0 <= pred y)%R).
1313
apply pred_ge_0 ; trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1314
1315
destruct Zp; trivial.
generalize H0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1316
rewrite pred_eq_pos;[idtac|now left].
1317
unfold pred_pos.
1318
destruct (ln_beta beta y) as (ey,Hey); simpl.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1319
1320
1321
case Req_bool_spec; intros Hy2.
(* . *)
intros Hy3.
1322
assert (ey-1 = fexp (ey -1))%Z.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1323
apply bpow_inj with beta.
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
rewrite <- Hy2, <- Rplus_0_l, Hy3.
ring.
assert (