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

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

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
Context { valid_exp : Valid_exp fexp }.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
36

37
Definition ulp x := bpow (canonic_exponent beta fexp x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
38

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

41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
Theorem ulp_opp :
  forall x, ulp (- x) = ulp x.
Proof.
intros x.
unfold ulp.
now rewrite canonic_exponent_opp.
Qed.

Theorem ulp_abs :
  forall x, ulp (Rabs x) = ulp x.
Proof.
intros x.
unfold ulp.
now rewrite canonic_exponent_abs.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
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
Theorem ulp_le_pos:
  forall x, 
    (0 < x)%R ->
    F x -> 
    (ulp x <= x)%R.
Proof.
intros x Zx Fx.
rewrite <- (Rmult_1_l (ulp x)).
pattern x at 2; rewrite Fx.
unfold F2R, ulp; simpl.
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.
apply F2R_gt_0_reg with beta (canonic_exponent beta fexp x).
now rewrite <- Fx.
Qed.

Theorem ulp_le_abs:
  forall x, 
    (x <> 0)%R ->
    F x -> 
    (ulp x <= Rabs x)%R.
Proof.
intros x Zx Fx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
83 84 85 86
rewrite <- ulp_abs.
apply ulp_le_pos.
now apply Rabs_pos_lt.
now apply generic_format_abs.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
87 88
Qed.

89 90
Theorem ulp_DN_UP :
  forall x, ~ F x ->
91
  round beta fexp rndUP x = (round beta fexp rndDN x + ulp x)%R.
92
Proof.
93
intros x Fx.
94
unfold round, Zrnd, ulp. simpl.
95 96
unfold F2R. simpl.
rewrite Zceil_floor_neq.
97
rewrite Z2R_plus. simpl.
98
ring.
99
intros H.
100
apply Fx.
101
unfold generic_format, F2R. simpl.
102 103 104
rewrite <- H.
rewrite Ztrunc_Z2R.
rewrite H.
105
now rewrite scaled_mantissa_bpow.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
106 107
Qed.

108
(** The successor of x is x + ulp x *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
109 110 111 112 113 114 115 116 117 118 119
Theorem succ_le_bpow :
  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.
unfold ulp, F2R. simpl.
pattern (bpow (canonic_exponent beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
rewrite <- Rmult_plus_distr_r.
change 1%R with (Z2R 1).
120
rewrite <- Z2R_plus.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
121 122 123 124 125 126 127 128
change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exponent beta fexp x)) <= bpow e)%R.
apply F2R_p1_le_bpow.
apply F2R_gt_0_reg with beta (canonic_exponent beta fexp x).
now rewrite <- Fx.
now rewrite <- Fx.
Qed.

Theorem ln_beta_succ :
129 130
  forall x, (0 < x)%R -> F x ->
  forall eps, (0 <= eps < ulp x)%R ->
131
  ln_beta beta (x + eps) = ln_beta beta x :> Z.
132 133 134 135 136 137 138 139 140 141 142 143 144 145 146
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.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
147
unfold ulp, F2R. simpl.
148 149 150
pattern (bpow (canonic_exponent beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
rewrite <- Rmult_plus_distr_r.
change 1%R with (Z2R 1).
151
rewrite <- Z2R_plus.
152 153 154 155 156 157 158 159 160
change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exponent beta fexp x)) <= bpow ex)%R.
apply F2R_p1_le_bpow.
apply F2R_gt_0_reg with beta (canonic_exponent beta fexp x).
now rewrite <- Fx.
now rewrite <- Fx.
now apply Rlt_le.
apply Rplus_le_le_0_compat.
now apply Rlt_le.
apply Heps.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
161 162
Qed.

163
Theorem round_DN_succ :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
164 165
  forall x, (0 < x)%R -> F x ->
  forall eps, (0 <= eps < ulp x)%R ->
166
  round beta fexp rndDN (x + eps) = x.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
167 168 169
Proof.
intros x Zx Fx eps Heps.
pattern x at 2 ; rewrite Fx.
170
unfold round.
171
unfold scaled_mantissa, Zrnd. simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
172 173 174
unfold canonic_exponent at 1 2.
rewrite ln_beta_succ ; trivial.
apply (f_equal (fun m => F2R (Float beta m _))).
175 176 177 178 179 180 181 182 183 184 185 186 187
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_exponent beta fexp x))%R.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
now apply Rplus_lt_compat_l.
rewrite Rmult_plus_distr_r.
188
rewrite Z2R_plus.
189 190 191 192
apply Rplus_le_compat.
pattern x at 1 3 ; rewrite Fx.
unfold F2R. simpl.
rewrite Rmult_assoc.
193
rewrite <- bpow_plus.
194 195 196 197 198
rewrite Zplus_opp_r.
rewrite Rmult_1_r.
rewrite Zfloor_Z2R.
apply Rle_refl.
unfold ulp.
199
rewrite <- bpow_plus.
200 201 202 203 204 205 206
rewrite Zplus_opp_r.
apply Rle_refl.
apply Rmult_le_pos.
now apply Rlt_le.
apply bpow_ge_0.
Qed.

207 208 209 210 211 212 213 214 215 216
Theorem generic_format_succ :
  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'.
destruct (succ_le_bpow x ex) ; try easy.
217
unfold generic_format, scaled_mantissa, canonic_exponent.
218 219
rewrite ln_beta_unique with beta (x + ulp x)%R ex.
pattern x at 1 3 ; rewrite Fx.
220 221 222
unfold ulp, scaled_mantissa.
rewrite canonic_exponent_fexp with (1 := Ex).
unfold F2R. simpl.
223 224
rewrite Rmult_plus_distr_r.
rewrite Rmult_assoc.
225
rewrite <- bpow_plus, Zplus_opp_r, Rmult_1_r.
226
change (bpow 0) with (Z2R 1).
227
rewrite <- Z2R_plus.
228
rewrite Ztrunc_Z2R.
229
rewrite Z2R_plus.
230 231 232 233 234 235 236 237 238 239 240 241 242 243
rewrite Rmult_plus_distr_r.
now rewrite Rmult_1_l.
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.
apply bpow_ge_0.
exact H.
apply Rplus_le_le_0_compat.
now apply Rlt_le.
apply bpow_ge_0.
rewrite H.
apply generic_format_bpow.
244
apply valid_exp.
245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260
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.
rewrite canonic_exponent_fexp with (1 := Ex).
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.
261 262 263
now apply Rlt_le.
Qed.

264
Theorem round_UP_succ :
265 266
  forall x, (0 < x)%R -> F x ->
  forall eps, (0 < eps <= ulp x)%R ->
267
  round beta fexp rndUP (x + eps) = (x + ulp x)%R.
268 269 270 271 272 273
Proof.
intros x Zx Fx eps (Heps1,[Heps2|Heps2]).
assert (Heps: (0 <= eps < ulp x)%R).
split.
now apply Rlt_le.
exact Heps2.
274
assert (Hd := round_DN_succ x Zx Fx eps Heps).
275 276 277 278 279
rewrite ulp_DN_UP.
rewrite Hd.
unfold ulp, canonic_exponent.
now rewrite ln_beta_succ.
intros Fs.
280
rewrite round_generic in Hd.
281 282 283 284 285
apply Rgt_not_eq with (2 := Hd).
pattern x at 2 ; rewrite <- Rplus_0_r.
now apply Rplus_lt_compat_l.
exact Fs.
rewrite Heps2.
286
apply round_generic.
287 288 289
now apply generic_format_succ.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
290 291 292 293 294
Theorem succ_lt_le:
  forall x y,
  F x -> F y ->
  (0 < x < y)%R ->
  (x + ulp x <= y)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
295
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
296 297 298 299 300 301 302 303
intros x y Hx Hy H.
case (Rle_or_lt (ulp x) (y-x)); intros H1.
apply Rplus_le_reg_r with (-x)%R.
now ring_simplify (x+ulp x + -x)%R.
replace y with (x+(y-x))%R by ring.
absurd (x < y)%R.
2: apply H.
apply Rle_not_lt; apply Req_le.
304
rewrite <- round_DN_succ with (eps:=(y-x)%R); try easy.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
305
ring_simplify (x+(y-x))%R.
306
apply sym_eq; now apply round_generic.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
307 308 309 310
split; trivial.
apply Rlt_le; now apply Rlt_Rminus.
Qed.

311
(** Error of a rounding, expressed in number of ulps *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
312
Theorem ulp_error :
313
  forall Zrnd x,
314
  (Rabs (round beta fexp Zrnd x - x) < ulp x)%R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
315
Proof.
316
intros Zrnd x.
317
destruct (generic_format_EM beta fexp x) as [Hx|Hx].
318
(* x = rnd x *)
319
rewrite round_generic with (1 := Hx).
320 321 322
unfold Rminus.
rewrite Rplus_opp_r, Rabs_R0.
apply bpow_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
323
(* x <> rnd x *)
324
destruct (round_DN_or_UP beta fexp Zrnd x) as [H|H] ; rewrite H ; clear H.
325 326 327
(* . *)
rewrite Rabs_left1.
rewrite Ropp_minus_distr.
328
apply Rplus_lt_reg_r with (round beta fexp rndDN x).
329 330
rewrite <- ulp_DN_UP with (1 := Hx).
ring_simplify.
331
assert (Hu: (x <= round beta fexp rndUP x)%R).
332
apply (round_UP_pt beta fexp x).
333 334 335 336
destruct Hu as [Hu|Hu].
exact Hu.
elim Hx.
rewrite Hu.
337
now apply generic_format_round.
338
apply Rle_minus.
339
apply (round_DN_pt beta fexp x).
340
(* . *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
341
rewrite Rabs_pos_eq.
342
rewrite ulp_DN_UP with (1 := Hx).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
343
apply Rplus_lt_reg_r with (x - ulp x)%R.
344
ring_simplify.
345
assert (Hd: (round beta fexp rndDN x <= x)%R).
346
apply (round_DN_pt beta fexp x).
347 348 349 350
destruct Hd as [Hd|Hd].
exact Hd.
elim Hx.
rewrite <- Hd.
351
now apply generic_format_round.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
352
apply Rle_0_minus.
353
apply (round_UP_pt beta fexp x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
354 355
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
356 357
Theorem ulp_half_error :
  forall choice x,
358
  (Rabs (round beta fexp (rndN choice) x - x) <= /2 * ulp x)%R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
359
Proof.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
360
intros choice x.
361
destruct (generic_format_EM beta fexp x) as [Hx|Hx].
Guillaume Melquiond's avatar
Guillaume Melquiond committed
362
(* x = rnd x *)
363
rewrite round_generic.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
364
unfold Rminus.
365
rewrite Rplus_opp_r, Rabs_R0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
366 367 368 369
apply Rmult_le_pos.
apply Rlt_le.
apply Rinv_0_lt_compat.
now apply (Z2R_lt 0 2).
370
apply bpow_ge_0.
371 372
exact Hx.
(* x <> rnd x *)
373
set (d := round beta fexp rndDN x).
374
destruct (generic_N_pt beta fexp choice x) as (Hr1, Hr2).
375 376 377 378
destruct (Rle_or_lt (x - d) (d + ulp x - x)) as [H|H].
(* . rnd(x) = rndd(x) *)
apply Rle_trans with (Rabs (d - x)).
apply Hr2.
379
apply (round_DN_pt beta fexp x).
380 381 382 383 384 385 386 387 388
rewrite Rabs_left1.
rewrite Ropp_minus_distr.
apply Rmult_le_reg_r with 2%R.
now apply (Z2R_lt 0 2).
apply Rplus_le_reg_r with (d - x)%R.
ring_simplify.
apply Rle_trans with (1 := H).
right. field.
apply Rle_minus.
389
apply (round_DN_pt beta fexp x).
390
(* . rnd(x) = rndu(x) *)
391
assert (Hu: (d + ulp x)%R = round beta fexp rndUP x).
392 393 394 395 396
unfold d.
now rewrite <- ulp_DN_UP.
apply Rle_trans with (Rabs (d + ulp x - x)).
apply Hr2.
rewrite Hu.
397
apply (round_UP_pt beta fexp x).
398 399 400 401 402 403 404 405 406 407
rewrite Rabs_pos_eq.
apply Rmult_le_reg_r with 2%R.
now apply (Z2R_lt 0 2).
apply Rplus_le_reg_r with (- (d + ulp x - x))%R.
ring_simplify.
apply Rlt_le.
apply Rlt_le_trans with (1 := H).
right. field.
apply Rle_0_minus.
rewrite Hu.
408
apply (round_UP_pt beta fexp x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
409 410
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
411
Theorem ulp_monotone :
412
  forall { Hm : Monotone_exp fexp },
Guillaume Melquiond's avatar
Guillaume Melquiond committed
413 414 415 416 417
  forall x y: R,
  (0 < x)%R -> (x <= y)%R ->
  (ulp x <= ulp y)%R.
Proof.
intros Hm x y Hx Hxy.
418
apply bpow_le.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
419 420 421 422
apply Hm.
now apply ln_beta_monotone.
Qed.

423
Theorem ulp_bpow :
424 425 426
  forall e, ulp (bpow e) = bpow (fexp (e + 1)).
intros e.
unfold ulp.
427 428
apply f_equal.
apply canonic_exponent_fexp.
429 430
rewrite Rabs_pos_eq.
split.
431 432
ring_simplify (e + 1 - 1)%Z.
apply Rle_refl.
433
apply bpow_lt.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
434
apply Zlt_succ.
435
apply bpow_ge_0.
436 437
Qed.

438
Theorem ulp_DN_pt_eq :
439
  forall x,
440 441
  (0 < round beta fexp rndDN x)%R ->
  ulp (round beta fexp rndDN x) = ulp x.
442
Proof.
443
intros x Hd.
444
unfold ulp.
445
now rewrite canonic_exponent_DN with (2 := Hd).
446 447
Qed.

448
Theorem ulp_error_f :
449
  forall { Hm : Monotone_exp fexp },
450
  forall Zrnd x,
451 452
  (round beta fexp Zrnd x <> 0)%R ->
  (Rabs (round beta fexp Zrnd x - x) < ulp (round beta fexp Zrnd x))%R.
453
Proof.
454
intros Hm Zrnd x Hfx.
455
case (round_DN_or_UP beta fexp Zrnd x); intros Hx.
456
(* *)
457
case (Rle_or_lt 0 (round beta fexp rndDN x)).
458 459 460 461 462 463 464
intros H; destruct H.
rewrite Hx at 2.
rewrite ulp_DN_pt_eq; trivial.
apply ulp_error.
rewrite Hx in Hfx; contradict Hfx; auto with real.
intros H.
apply Rlt_le_trans with (1:=ulp_error _ _).
465
rewrite <- (ulp_opp x), <- (ulp_opp (round beta fexp Zrnd x)).
466 467 468 469 470
apply ulp_monotone; trivial.
apply Ropp_0_gt_lt_contravar; apply Rlt_gt.
case (Rle_or_lt 0 x); trivial.
intros H1; contradict H.
apply Rle_not_lt.
471
apply round_monotone_l; trivial.
472 473
apply generic_format_0.
apply Ropp_le_contravar; rewrite Hx.
474
apply (round_DN_pt beta fexp x).
475
(* *)
476
rewrite Hx; case (Rle_or_lt 0 (round beta fexp rndUP x)).
477 478 479 480 481 482
intros H; destruct H.
apply Rlt_le_trans with (1:=ulp_error _ _).
apply ulp_monotone; trivial.
case (Rle_or_lt x 0); trivial.
intros H1; contradict H.
apply Rle_not_lt.
483
apply round_monotone_r; trivial.
484
apply generic_format_0.
485
apply (round_UP_pt beta fexp x).
486 487
rewrite Hx in Hfx; contradict Hfx; auto with real.
intros H.
488 489
rewrite <- (ulp_opp (round beta fexp rndUP x)).
rewrite <- round_DN_opp.
490
rewrite ulp_DN_pt_eq; trivial.
491
replace (round beta fexp rndUP x - x)%R with (-((round beta fexp rndDN (-x) - (-x))))%R.
492 493
rewrite Rabs_Ropp.
apply ulp_error.
494 495
rewrite round_DN_opp; ring.
rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption.
496 497 498
Qed.

Theorem ulp_half_error_f : 
499
  forall { Hm : Monotone_exp fexp },
500
  forall choice x,
501 502
  (round beta fexp (rndN choice) x <> 0)%R ->
  (Rabs (round beta fexp (rndN choice) x - x) <= /2 * ulp (round beta fexp (rndN choice) x))%R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
503
Proof.
504
intros Hm choice x Hfx.
505
case (round_DN_or_UP beta fexp (rndN choice) x); intros Hx.
506
(* *)
507
case (Rle_or_lt 0 (round beta fexp rndDN x)).
508 509 510 511 512 513 514 515 516
intros H; destruct H.
rewrite Hx at 2.
rewrite ulp_DN_pt_eq; trivial.
apply ulp_half_error.
rewrite Hx in Hfx; contradict Hfx; auto with real.
intros H.
apply Rle_trans with (1:=ulp_half_error _ _).
apply Rmult_le_compat_l.
auto with real.
517
rewrite <- (ulp_opp x), <- (ulp_opp (round beta fexp (rndN choice) x)).
518 519 520 521 522
apply ulp_monotone; trivial.
apply Ropp_0_gt_lt_contravar; apply Rlt_gt.
case (Rle_or_lt 0 x); trivial.
intros H1; contradict H.
apply Rle_not_lt.
523
apply round_monotone_l; trivial.
524 525
apply generic_format_0.
apply Ropp_le_contravar; rewrite Hx.
526
apply (round_DN_pt beta fexp x).
527
(* *)
528
case (Rle_or_lt 0 (round beta fexp rndUP x)).
529 530 531 532 533 534 535 536
intros H; destruct H.
apply Rle_trans with (1:=ulp_half_error _ _).
apply Rmult_le_compat_l.
auto with real.
apply ulp_monotone; trivial.
case (Rle_or_lt x 0); trivial.
intros H1; contradict H.
apply Rle_not_lt.
537
apply round_monotone_r; trivial.
538
apply generic_format_0.
539
rewrite Hx; apply (round_UP_pt beta fexp x).
540 541
rewrite Hx in Hfx; contradict Hfx; auto with real.
intros H.
542 543
rewrite Hx at 2; rewrite <- (ulp_opp (round beta fexp rndUP x)).
rewrite <- round_DN_opp.
544
rewrite ulp_DN_pt_eq; trivial.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
545
pattern x at 1 2; rewrite <- Ropp_involutive.
546
rewrite round_N_opp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
547 548
unfold Rminus.
rewrite <- Ropp_plus_distr, Rabs_Ropp.
549
apply ulp_half_error.
550
rewrite round_DN_opp; apply Ropp_0_gt_lt_contravar; apply Rlt_gt; assumption.
551 552
Qed.

553
(** Predecessor *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
554
Definition pred x :=
555 556 557 558
  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.
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
559

BOLDO Sylvie's avatar
BOLDO Sylvie committed
560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581
Theorem pred_ge_bpow :
  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_exponent 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.
unfold ulp, F2R. simpl.
pattern (bpow (canonic_exponent beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
rewrite <- Rmult_minus_distr_r.
change 1%R with (Z2R 1).
582
rewrite <- Z2R_minus.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
583 584 585 586 587 588 589 590 591 592 593
change (bpow e <= F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) - 1) (canonic_exponent beta fexp x)))%R.
apply bpow_le_F2R_m1; trivial.
now rewrite <- Fx.
(* *)
contradict Hx'.
pattern x at 1; rewrite Fx.
rewrite  <- Hm.
unfold ulp, F2R; simpl.
now rewrite Rmult_1_l.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
594
Theorem format_pred_1:
BOLDO Sylvie's avatar
BOLDO Sylvie committed
595
  forall x, (0 < x)%R -> F x -> 
596
  x <> bpow (ln_beta beta x - 1) ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
597
  F (x - ulp x).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
598
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
599 600 601 602 603 604 605 606 607
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.
608
unfold generic_format, scaled_mantissa, canonic_exponent.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
609 610 611 612 613 614 615
rewrite ln_beta_unique with beta (x - ulp x)%R ex.
pattern x at 1 3 ; rewrite Fx.
unfold ulp, scaled_mantissa.
rewrite canonic_exponent_fexp with (1 := Ex).
unfold F2R. simpl.
rewrite Rmult_minus_distr_r.
rewrite Rmult_assoc.
616
rewrite <- bpow_plus, Zplus_opp_r, Rmult_1_r.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
617
change (bpow 0) with (Z2R 1).
618
rewrite <- Z2R_minus.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
619
rewrite Ztrunc_Z2R.
620
rewrite Z2R_minus.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
621 622 623 624 625 626 627
rewrite Rmult_minus_distr_r.
now rewrite Rmult_1_l.
rewrite Rabs_pos_eq.
split.
apply pred_ge_bpow; trivial.
unfold ulp; intro H.
assert (ex-1 < canonic_exponent beta fexp x  < ex)%Z.
628
split ; apply (lt_bpow beta) ; rewrite <- H ; easy.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652
clear -H0. omega.
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.
apply bpow_ge_0.
apply Rle_0_minus.
pattern x at 2; rewrite Fx.
unfold ulp, F2R; simpl.
pattern (bpow (canonic_exponent 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.
apply F2R_gt_0_reg with beta (canonic_exponent beta fexp x).
rewrite <- Fx.
apply Rle_lt_trans with (2:=proj1 Ex').
apply bpow_ge_0.
omega.
Qed.

653
Theorem format_pred_2 :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
654
  forall x, (0 < x)%R -> F x -> 
655
  let e := ln_beta_val beta x (ln_beta beta x) in
BOLDO Sylvie's avatar
BOLDO Sylvie committed
656
  x =  bpow (e - 1) ->
657
  F (x - bpow (fexp (e - 1))).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
658
Proof.
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
659 660
intros x Zx Fx e Hx.
pose (f:=(x - bpow (fexp (e - 1)))%R).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
661
fold f.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
662 663 664
assert (He:(fexp (e-1) <= e-1)%Z). 
apply generic_format_bpow_inv with beta; trivial.
rewrite <- Hx; assumption.
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
665
case (Zle_lt_or_eq _ _ He); clear He; intros He.
666
assert (f = F2R (Float beta (Zpower beta (e-1-(fexp (e-1))) -1) (fexp (e-1))))%R.
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
667 668
unfold f; rewrite Hx.
unfold F2R; simpl.
669
rewrite Z2R_minus, Z2R_Zpower.
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
670
rewrite Rmult_minus_distr_r, Rmult_1_l.
671
rewrite <- bpow_plus.
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
672 673 674 675 676 677 678 679 680 681 682 683 684
now replace (e - 1 - fexp (e - 1) + fexp (e - 1))%Z with (e-1)%Z by ring.
omega.
rewrite H.
apply generic_format_canonic_exponent.
apply Zeq_le.
apply canonic_exponent_fexp.
rewrite <- H.
unfold f; rewrite Hx.
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.
685
apply Rplus_le_compat ; apply bpow_le ; omega.
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
686 687 688 689 690
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.
691
replace (bpow 1) with (Z2R beta).
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
692 693 694 695 696 697
apply Z2R_le.
apply <- Zle_is_le_bool.
now destruct beta.
simpl.
unfold Zpower_pos; simpl.
now rewrite Zmult_1_r.
698
rewrite <- bpow_plus.
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
699 700 701 702 703 704 705 706
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.
707
apply bpow_le.
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
708 709 710 711 712 713 714
omega.
replace f with 0%R.
apply generic_format_0.
unfold f.
rewrite Hx, He.
ring.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
715

716
Theorem format_pred :
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
717
  forall x, (0 < x)%R -> F x -> 
BOLDO Sylvie's avatar
BOLDO Sylvie committed
718
  F (pred x).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
719
Proof.
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
720
intros x Zx Fx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
721 722 723 724
unfold pred.
case Req_bool_spec; intros H.
now apply format_pred_2.
now apply format_pred_1.
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
725
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
726

727
Theorem pred_ulp_1 :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
728
  forall x, (0 < x)%R -> F x -> 
729
  x <> bpow (ln_beta beta x - 1) ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
730
  ((x - ulp x) + ulp (x-ulp x) = x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
731
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750
intros x Zx Fx Hx.
replace (ulp (x - ulp x)) with (ulp x).
ring.
unfold ulp at 1 2; apply f_equal.
unfold canonic_exponent; apply f_equal.
destruct (ln_beta beta x) as (ex, Hex).
simpl in *.
assert (x <> 0)%R by auto with real.
specialize (Hex H).
apply sym_eq.
apply ln_beta_unique.
rewrite Rabs_right.
rewrite Rabs_right in Hex.
2: apply Rle_ge; apply Rlt_le; easy.
split.
destruct Hex as ([H1|H1],H2).
apply pred_ge_bpow; trivial.
unfold ulp; intros H3.
assert (ex-1 < canonic_exponent beta fexp x  < ex)%Z.
751
split ; apply (lt_bpow beta) ; rewrite <- H3 ; easy.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773
omega.
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.
pattern x at 2; rewrite Fx.
unfold ulp, F2R; simpl.
pattern (bpow (canonic_exponent beta fexp x)) at 1; rewrite <- Rmult_1_l.
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.
apply F2R_gt_0_reg with beta (canonic_exponent beta fexp x).
now rewrite <- Fx.
Qed.

774
Theorem pred_ulp_2 :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
775
  forall x, (0 < x)%R -> F x -> 
776
  let e := ln_beta_val beta x (ln_beta beta x) in
BOLDO Sylvie's avatar
BOLDO Sylvie committed
777 778 779
  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
780
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
781 782 783
intros x Zx Fx e Hxe Zp.
replace (ulp (x - bpow (fexp (e - 1)))) with (bpow (fexp (e - 1))).
ring.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
784 785 786
assert (He:(fexp (e-1) <= e-1)%Z). 
apply generic_format_bpow_inv with beta; trivial.
rewrite <- Hxe; assumption.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
787 788 789 790 791 792 793 794 795 796 797
case (Zle_lt_or_eq _ _ He); clear He; intros He.
(* *)
unfold ulp; apply f_equal.
unfold canonic_exponent; apply f_equal.
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.
798
apply Rplus_le_compat; apply bpow_le; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
799 800 801 802 803
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.
804
replace (bpow 1) with (Z2R beta).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
805 806 807 808 809 810
apply Z2R_le.
apply <- Zle_is_le_bool.
now destruct beta.
simpl.
unfold Zpower_pos; simpl.
now rewrite Zmult_1_r.
811
rewrite <- bpow_plus.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
812 813 814 815 816 817 818 819 820
replace (1+(e-2))%Z with (e-1)%Z by ring.
now right.
rewrite <- Rplus_0_r, Hxe.
apply Rplus_lt_compat_l.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
apply bpow_gt_0.
apply Rle_ge; apply Rle_0_minus.
rewrite Hxe.
821
apply bpow_le.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
822 823 824 825 826 827
omega.
(* *)
contradict Zp.
rewrite Hxe, He; ring.
Qed.

828
Theorem pred_ulp :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
829
  forall x, (0 < x)%R -> F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
830 831
  (pred x <> 0)%R ->
  (pred x + ulp (pred x) = x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
832
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
833
intros x Zx Fx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
834 835 836 837
unfold pred.
case Req_bool_spec; intros H Zp.
now apply pred_ulp_2.
now apply pred_ulp_1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
838
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
839

840
Theorem pred_lt :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
841
  forall x, 
842
  (pred x < x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
843
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
844
intros.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
845 846 847
unfold pred.
case Req_bool_spec; intros H.
(* *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
848 849 850 851 852
rewrite <- Rplus_0_r.
apply Rplus_lt_compat_l.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
apply bpow_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
853
(* *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
854 855 856 857 858 859
rewrite <- Rplus_0_r.
apply Rplus_lt_compat_l.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
apply bpow_gt_0.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
860

861
Theorem pred_ge_0 :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
862
  forall x, 
863
  (0 < x)%R -> F x -> (0 <= pred x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
864 865 866 867 868 869
intros x Zx Fx.
unfold pred.
case Req_bool_spec; intros H.
(* *)
apply Rle_0_minus.
rewrite H.
870
apply bpow_le.
871
destruct (ln_beta beta x) as (ex,Ex) ; simpl.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
872
rewrite ln_beta_bpow.
873
ring_simplify (ex - 1 + 1 - 1)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
874 875 876 877 878 879 880
apply generic_format_bpow_inv with beta; trivial.
simpl in H.
rewrite <- H; assumption.
apply Rle_0_minus.
now apply ulp_le_pos.
Qed.

881
Theorem round_UP_pred :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
882 883
  forall x, (0 < pred x)%R -> F x ->
  forall eps, (0 < eps <= ulp (pred x) )%R ->
884
  round beta fexp rndUP (pred x + eps) = x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
885 886
Proof.
intros x Hx Fx eps Heps.
887
rewrite round_UP_succ; trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
888
apply pred_ulp; trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
889
apply Rlt_trans with (1:=Hx).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
890
apply pred_lt.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
891
now apply Rgt_not_eq.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
892
apply format_pred; trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
893
apply Rlt_trans with (1:=Hx).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
894
apply pred_lt.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
895
Qed.
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
896

897
Theorem round_DN_pred :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
898
  forall x, (0 < pred x)%R -> F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
899
  forall eps, (0 < eps <= ulp (pred x))%R ->
900
  round beta fexp rndDN (x - eps) = pred x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
901
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
902 903 904 905
intros x Hpx Fx eps Heps.
assert (Hx:(0 < x)%R).
apply Rlt_trans with (1:=Hpx).
apply pred_lt.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
906
replace (x-eps)%R with (pred x + (ulp (pred x)-eps))%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
907 908 909
2: pattern x at 3; rewrite <- (pred_ulp x); trivial.
2: ring.
2: now apply Rgt_not_eq.
910
rewrite round_DN_succ; trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
911 912 913 914 915 916 917 918 919 920
now apply format_pred.
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
921

BOLDO Sylvie's avatar
BOLDO Sylvie committed
922
Theorem le_pred_lt:
BOLDO Sylvie's avatar
BOLDO Sylvie committed
923 924 925
  forall x y,
  F x -> F y ->
  (0 < x < y)%R ->
926
  (x <= pred y)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
927 928
Proof.
intros x y Hx Hy H. 
929 930 931
assert (Zy:(0 < y)%R).
apply Rlt_trans with (1:=proj1 H).
apply H.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
932
(* *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
933 934
assert (Zp: (0 < pred y)%R).
assert (Zp:(0 <= pred y)%R).
935
apply pred_ge_0 ; trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
936 937 938
destruct Zp; trivial.
generalize H0.
unfold pred.
939
destruct (ln_beta beta y) as (ey,Hey); simpl.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
940 941 942
case Req_bool_spec; intros Hy2.
(* . *)
intros Hy3.
943
assert (ey-1 = fexp (ey -1))%Z.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
944
apply bpow_inj with beta.
945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962
rewrite <- Hy2, <- Rplus_0_l, Hy3.
ring.
assert (Zx: (x <> 0)%R).
now apply Rgt_not_eq.
destruct (ln_beta beta x) as (ex,Hex).
specialize (Hex Zx).
assert (ex <= ey)%Z.
apply bpow_lt_bpow with beta.
apply Rle_lt_trans with (1:=proj1 Hex).
apply Rlt_trans with (Rabs y).
rewrite 2!Rabs_right.
apply H.
now apply Rgt_ge.
now apply Rgt_ge.
apply Hey.
now apply Rgt_not_eq.
case (Zle_lt_or_eq _ _ H2); intros Hexy.
assert (fexp ex = fexp (ey-1))%Z.
963
apply valid_exp.
964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998
omega.
rewrite <- H1.
omega.
absurd (0 < Ztrunc (scaled_mantissa beta fexp x) < 1)%Z.
omega.
split.
apply F2R_gt_0_reg with beta (canonic_exponent beta fexp x).
now rewrite <- Hx.
apply lt_Z2R.
apply Rmult_lt_reg_r with (bpow (canonic_exponent beta fexp x)).
apply bpow_gt_0.
replace (Z2R (Ztrunc (scaled_mantissa beta fexp x)) *
 bpow (canonic_exponent beta fexp x))%R with x.
rewrite Rmult_1_l.
unfold canonic_exponent.
rewrite ln_beta_unique with beta x ex.
rewrite H3,<-H1, <- Hy2.
apply H.
exact Hex.
absurd (y <= x)%R.
now apply Rlt_not_le.
rewrite Rabs_right in Hex