Flocq_rnd_generic.v 13.7 KB
Newer Older
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
Require Import Flocq_Raux.
Require Import Flocq_defs.
Require Import Flocq_rnd_ex.

Section RND_generic.

Variable beta : radix.

Notation bpow := (epow beta).

Variable fexp : Z -> Z.

Variable valid_fexp :
 forall k : Z,
 ( (fexp k < k)%Z -> (fexp (k + 1) <= k)%Z ) /\
 ( (k <= fexp k)%Z ->
   (fexp (fexp k + 1) <= fexp k)%Z /\
   forall l : Z, (l <= fexp k)%Z -> fexp l = fexp k ).

Definition generic_format (x : R) :=
  exists f : float beta,
22
23
  x = F2R f /\ forall (H : x <> R0),
  Fexp f = fexp (projT1 (ln_beta beta _ (Rabs_pos_lt _ H))).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
24
25
26
27
28
29
30
31

Theorem generic_format_satisfies_any :
  satisfies_any generic_format.
Proof.
refine ((fun D => Satisfies_any _ _ _ (projT1 D) (projT2 D)) _).
(* symmetric set *)
exists (Float beta 0 0).
split.
32
unfold F2R. simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
33
now rewrite Rmult_0_l.
34
35
intros H.
now elim H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
36
37
38
39
intros x ((m,e),(H1,H2)).
exists (Float beta (-m) e).
split.
rewrite H1.
40
unfold F2R. simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
41
now rewrite opp_Z2R, Ropp_mult_distr_l_reverse.
42
43
44
45
46
47
48
49
50
51
52
53
intros H3.
simpl in H2.
assert (H4 := Ropp_neq_0_compat _ H3).
rewrite Ropp_involutive in H4.
rewrite (H2 H4).
clear H2.
destruct (ln_beta beta (Rabs x)) as (ex, H5).
simpl.
apply f_equal.
apply sym_eq.
apply ln_beta_unique.
now rewrite Rabs_Ropp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
(* rounding down *)
assert (Hxx : forall x, (0 > x)%R -> (0 < -x)%R).
intros.
now apply Ropp_0_gt_lt_contravar.
exists (fun x =>
  match total_order_T 0 x with
  | inleft (left Hx) =>
    let e := fexp (projT1 (ln_beta beta _ Hx)) in
    F2R (Float beta (up (x * bpow (Zopp e)) - 1) e)
  | inleft (right _) => R0
  | inright Hx =>
    let e := fexp (projT1 (ln_beta beta _ (Hxx _ Hx))) in
    F2R (Float beta (up (x * bpow (Zopp e)) - 1) e)
  end).
intros x.
destruct (total_order_T 0 x) as [[Hx|Hx]|Hx].
(* positive *)
clear Hxx.
destruct (ln_beta beta x Hx) as (ex, (Hx1, Hx2)).
simpl.
destruct (Z_lt_le_dec (fexp ex) ex) as [He1|He1].
(* - positive big enough *)
assert (Hbl : (bpow (ex - 1)%Z <= F2R (Float beta (up (x * bpow (- fexp ex)%Z) - 1) (fexp ex)))%R).
(* - . bounded left *)
clear Hx2.
unfold F2R.
simpl.
replace (ex - 1)%Z with ((ex - 1 - fexp ex) + fexp ex)%Z by ring.
rewrite epow_add.
apply Rmult_le_compat_r.
apply epow_ge_0.
assert (bpow (ex - 1 - fexp ex)%Z < Z2R (up (x * bpow (- fexp ex)%Z)))%R.
rewrite Z2R_IZR.
apply Rle_lt_trans with (2 := proj1 (archimed _)).
unfold Zminus.
rewrite epow_add.
apply Rmult_le_compat_r.
apply epow_ge_0.
exact Hx1.
case_eq (ex - 1 - fexp ex)%Z.
intros He2.
change (bpow 0%Z) with (Z2R 1).
apply Z2R_le.
change 1%Z at 1 with (1 + 1 - 1)%Z.
apply Zplus_le_compat_r.
apply (Zlt_le_succ 1).
apply lt_Z2R.
now rewrite He2 in H.
intros ep He2.
simpl.
apply Z2R_le.
replace (Zpower_pos (radix_val beta) ep) with (Zpower_pos (radix_val beta) ep + 1 - 1)%Z by ring.
apply Zplus_le_compat_r.
apply Zlt_le_succ.
apply lt_Z2R.
change (bpow (Zpos ep) < Z2R (up (x * bpow (- fexp ex)%Z)))%R.
now rewrite <- He2.
clear H Hx1.
intros.
assert (ex - 1 - fexp ex < 0)%Z.
now rewrite H.
apply False_ind.
omega.
split.
(* - . rounded *)
119
eexists ; split ; [ reflexivity | idtac ].
Guillaume Melquiond's avatar
Guillaume Melquiond committed
120
121
122
123
124
125
126
127
128
129
130
131
intros He9.
simpl.
apply f_equal.
apply sym_eq.
apply ln_beta_unique.
clear He9.
rewrite Rabs_right.
split.
exact Hbl.
(* - . . bounded right *)
clear Hbl.
apply Rle_lt_trans with (2 := Hx2).
132
unfold F2R. simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
pattern x at 2 ; replace x with ((x * bpow (- fexp ex)%Z) * bpow (fexp ex))%R.
generalize (x * bpow (- fexp ex)%Z)%R.
clear.
intros x.
apply Rmult_le_compat_r.
apply epow_ge_0.
rewrite minus_Z2R.
rewrite Z2R_IZR.
simpl.
apply Rplus_le_reg_l with (- x + 1)%R.
ring_simplify.
rewrite Rplus_comm.
exact (proj2 (archimed x)).
rewrite Rmult_assoc.
rewrite <- epow_add.
rewrite Zplus_opp_l.
apply Rmult_1_r.
(* - . . *)
apply Rle_ge.
apply Rle_trans with (2 := Hbl).
apply epow_ge_0.
split.
(* - . smaller *)
156
unfold F2R. simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
generalize (fexp ex).
clear.
intros e.
pattern x at 2 ; rewrite <- Rmult_1_r.
change R1 with (bpow Z0).
rewrite <- (Zplus_opp_l e).
rewrite epow_add, <- Rmult_assoc.
apply Rmult_le_compat_r.
apply epow_ge_0.
rewrite minus_Z2R.
rewrite Z2R_IZR.
simpl.
apply Rplus_le_reg_l with (1 - x * bpow (-e)%Z)%R.
ring_simplify.
rewrite Rplus_comm.
rewrite Ropp_mult_distr_l_reverse.
exact (proj2 (archimed _)).
(* - . biggest *)
intros g ((gm, ge), (Hg1, Hg2)) Hgx.
destruct (Rle_or_lt g R0) as [Hg3|Hg3].
apply Rle_trans with (2 := Hbl).
apply Rle_trans with (1 := Hg3).
apply epow_ge_0.
180
specialize (Hg2 (Rgt_not_eq _ _ Hg3)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
181
182
183
184
185
186
187
apply Rnot_lt_le.
intros Hrg.
assert (bpow (ex - 1)%Z <= g < bpow ex)%R.
split.
apply Rle_trans with (1 := Hbl).
now apply Rlt_le.
now apply Rle_lt_trans with (1 := Hgx).
188
rewrite <- (Rabs_pos_eq g (Rlt_le _ _ Hg3)) in H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
rewrite ln_beta_unique with (1 := H) in Hg2.
simpl in Hg2.
apply Rlt_not_le with (1 := Hrg).
rewrite Hg1, Hg2.
unfold F2R. simpl.
apply Rmult_le_compat_r.
apply epow_ge_0.
apply Z2R_le.
cut (gm < up (x * bpow (- fexp ex)%Z))%Z.
omega.
apply lt_IZR.
apply Rle_lt_trans with (2 := proj1 (archimed _)).
apply Rmult_le_reg_r with (bpow (fexp ex)).
apply epow_gt_0.
rewrite <- Hg2 at 1.
rewrite <- Z2R_IZR.
rewrite Rmult_assoc.
rewrite <- epow_add.
rewrite Zplus_opp_l.
rewrite Rmult_1_r.
unfold F2R in Hg1.
simpl in Hg1.
now rewrite <- Hg1.
(* - positive too small *)
cutrewrite (up (x * bpow (- fexp ex)%Z) = 1%Z).
(* - . rounded *)
unfold F2R. simpl.
rewrite Rmult_0_l.
split.
exists (Float beta Z0 (fexp ex)).
split.
unfold F2R. simpl.
now rewrite Rmult_0_l.
222
223
intros H.
now elim H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
224
225
226
227
228
229
split.
now apply Rlt_le.
(* - . biggest *)
intros g ((gm, ge), (Hg1, Hg2)) Hgx.
apply Rnot_lt_le.
intros Hg3.
230
specialize (Hg2 (Rgt_not_eq _ _ Hg3)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
231
destruct (ln_beta beta g Hg3) as (ge', Hg4).
232
233
234
generalize Hg4. intros Hg5.
rewrite <- (Rabs_pos_eq g (Rlt_le _ _ Hg3)) in Hg5.
rewrite ln_beta_unique with (1 := Hg5) in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
235
236
237
apply (Rlt_not_le _ _ (Rle_lt_trans _ _ _ Hgx Hx2)).
apply Rle_trans with (bpow ge).
apply -> epow_le.
238
simpl in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
239
240
241
242
rewrite Hg2.
rewrite (proj2 (proj2 (valid_fexp ex) He1) ge').
exact He1.
apply Zle_trans with (2 := He1).
243
cut (ge' - 1 < ex)%Z. omega.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
244
245
246
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
apply <- epow_lt.
apply Rle_lt_trans with (2 := Hx2).
apply Rle_trans with (2 := Hgx).
exact (proj1 Hg4).
rewrite Hg1.
unfold F2R. simpl.
pattern (bpow ge) at 1 ; rewrite <- Rmult_1_l.
apply Rmult_le_compat_r.
apply epow_ge_0.
apply (Z2R_le 1).
apply (Zlt_le_succ 0).
apply lt_Z2R.
apply Rmult_lt_reg_r with (bpow ge).
apply epow_gt_0.
rewrite Rmult_0_l.
unfold F2R in Hg1. simpl in Hg1.
now rewrite <- Hg1.
(* - . . *)
apply sym_eq.
rewrite <- (Zplus_0_l 1).
apply up_tech.
apply Rlt_le.
apply Rmult_lt_0_compat.
exact Hx.
apply epow_gt_0.
change (IZR (0 + 1)) with (bpow Z0).
rewrite <- (Zplus_opp_r (fexp ex)).
rewrite epow_add.
apply Rmult_lt_compat_r.
apply epow_gt_0.
apply Rlt_le_trans with (1 := Hx2).
now apply -> epow_le.
(* zero *)
split.
exists (Float beta 0 0).
split.
unfold F2R.
now rewrite Rmult_0_l.
282
283
intros H.
now elim H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
284
285
286
287
288
289
290
291
292
293
294
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
rewrite <- Hx.
split.
apply Rle_refl.
intros g _ H.
exact H.
(* negative *)
destruct (ln_beta beta (- x) (Hxx x Hx)) as (ex, (Hx1, Hx2)).
simpl.
clear Hxx.
assert (Hbr : (F2R (Float beta (up (x * bpow (- fexp ex)%Z) - 1) (fexp ex)) <= x)%R).
(* - bounded right *)
unfold F2R. simpl.
pattern x at 2 ; rewrite <- Rmult_1_r.
change R1 with (bpow Z0).
rewrite <- (Zplus_opp_l (fexp ex)).
rewrite epow_add.
rewrite <- Rmult_assoc.
generalize (x * bpow (- fexp ex)%Z)%R.
clear.
intros x.
apply Rmult_le_compat_r.
apply epow_ge_0.
rewrite minus_Z2R.
simpl.
rewrite Z2R_IZR.
apply Rplus_le_reg_l with (-x + 1)%R.
ring_simplify.
rewrite Rplus_comm.
exact (proj2 (archimed x)).
destruct (Z_lt_le_dec (fexp ex) ex) as [He1|He1].
(* - negative big enough *)
assert (Hbl : (- bpow ex <= F2R (Float beta (up (x * bpow (- fexp ex)%Z) - 1) (fexp ex)))%R).
(* - . bounded left *)
unfold F2R. simpl.
pattern ex at 1 ; replace ex with (ex - fexp ex + fexp ex)%Z by ring.
rewrite epow_add.
rewrite <- Ropp_mult_distr_l_reverse.
apply Rmult_le_compat_r.
apply epow_ge_0.
cut (0 < ex - fexp ex)%Z. 2: omega.
case_eq (ex - fexp ex)%Z ; try (intros ; discriminate H0).
intros ep Hp _.
simpl.
rewrite <- opp_Z2R.
apply Z2R_le.
cut (- Zpower_pos (radix_val beta) ep < up (x * bpow (- fexp ex)%Z))%Z.
omega.
apply lt_Z2R.
apply Rle_lt_trans with (x * bpow (- fexp ex)%Z)%R.
rewrite opp_Z2R.
change (- bpow (Zpos ep) <= x * bpow (- fexp ex)%Z)%R.
rewrite <- Hp.
apply Rmult_le_reg_r with (bpow (fexp ex)).
apply epow_gt_0.
rewrite Rmult_assoc.
rewrite <- epow_add.
rewrite Zplus_opp_l.
rewrite Rmult_1_r.
rewrite Ropp_mult_distr_l_reverse.
rewrite <- epow_add.
replace (ex - fexp ex + fexp ex)%Z with ex by ring.
rewrite <- (Ropp_involutive x).
apply Ropp_le_contravar.
now apply Rlt_le.
rewrite Z2R_IZR.
exact (proj1 (archimed _)).
split.
(* - . rounded *)
destruct (Rle_lt_or_eq_dec _ _ Hbl) as [Hbl2|Hbl2].
(* - . . not a radix power *)
eexists ; split ; [ reflexivity | idtac ].
intros Hr.
simpl.
apply f_equal.
apply sym_eq.
apply ln_beta_unique.
360
rewrite Rabs_left.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
361
split.
362
363
apply Ropp_le_cancel.
rewrite Ropp_involutive.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
364
apply Rle_trans with (1 := Hbr).
365
366
367
368
apply Ropp_le_cancel.
now rewrite Ropp_involutive.
apply Ropp_lt_cancel.
now rewrite Ropp_involutive.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
apply Rle_lt_trans with (1 := Hbr).
exact Hx.
(* - . . a radix power *)
rewrite <- Hbl2.
generalize (proj1 (valid_fexp _) He1).
clear.
intros He2.
exists (Float beta (- Zpower (radix_val beta) (ex - fexp (ex + 1))) (fexp (ex + 1))).
unfold F2R. simpl.
split.
clear -He2.
pattern ex at 1 ; replace ex with (ex - fexp (ex + 1) + fexp (ex + 1))%Z by ring.
rewrite epow_add.
rewrite <- Ropp_mult_distr_l_reverse.
rewrite opp_Z2R.
apply (f_equal (fun x => (- x * _)%R)).
cut (0 <= ex - fexp (ex + 1))%Z. 2: omega.
case (ex - fexp (ex + 1))%Z ; trivial.
intros ep H.
now elim H.
389
intros H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
390
391
392
apply f_equal.
apply sym_eq.
apply ln_beta_unique.
393
394
rewrite Rabs_Ropp.
rewrite Rabs_right.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
split.
apply -> epow_le.
omega.
apply -> epow_lt.
apply Zlt_succ.
apply Rle_ge.
apply epow_ge_0.
split.
exact Hbr.
(* - . biggest *)
intros g ((gm, ge), (Hg1, Hg2)) Hgx.
apply Rnot_lt_le.
intros Hg3.
assert (Hg4 : (g < 0)%R).
now apply Rle_lt_trans with (1 := Hgx).
410
411
specialize (Hg2 (Rlt_not_eq _ _ Hg4)).
destruct (ln_beta beta (Rabs g) (Rabs_pos_lt g (Rlt_not_eq g 0 Hg4))) as (ge', Hge).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
412
413
414
415
416
417
418
419
420
simpl in Hg2.
apply Rlt_not_le with (1 := Hg3).
rewrite Hg1.
unfold F2R. simpl.
rewrite Hg2.
assert (Hge' : ge' = ex).
apply epow_unique with (1 := Hge).
split.
apply Rle_trans with (1 := Hx1).
421
rewrite Rabs_left with (1 := Hg4).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
422
423
now apply Ropp_le_contravar.
apply Ropp_lt_cancel.
424
425
426
rewrite Rabs_left with (1 := Hg4).
rewrite Ropp_involutive.
now apply Rle_lt_trans with (1 := Hbl).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
427
428
429
430
rewrite Hge'.
apply Rmult_le_compat_r.
apply epow_ge_0.
apply Z2R_le.
431
cut (gm < up (x * bpow (- fexp ex)%Z))%Z. omega.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
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
apply lt_IZR.
apply Rle_lt_trans with (2 := proj1 (archimed _)).
rewrite <- Z2R_IZR.
apply Rmult_le_reg_r with (bpow (fexp ex)).
apply epow_gt_0.
rewrite Rmult_assoc.
rewrite <- epow_add.
rewrite Zplus_opp_l.
rewrite Rmult_1_r.
rewrite <- Hge'.
rewrite <- Hg2.
unfold F2R in Hg1. simpl in Hg1.
now rewrite <- Hg1.
(* - negative too small *)
cutrewrite (up (x * bpow (- fexp ex)%Z) = 0%Z).
unfold F2R. simpl.
rewrite Ropp_mult_distr_l_reverse.
rewrite Rmult_1_l.
(* - . rounded *)
split.
destruct (proj2 (valid_fexp _) He1) as (He2, _).
exists (Float beta (- Zpower (radix_val beta) (fexp ex - fexp (fexp ex + 1))) (fexp (fexp ex + 1))).
unfold F2R. simpl.
split.
rewrite opp_Z2R.
pattern (fexp ex) at 1 ; replace (fexp ex) with (fexp ex - fexp (fexp ex + 1) + fexp (fexp ex + 1))%Z by ring.
rewrite epow_add.
rewrite Ropp_mult_distr_l_reverse.
apply (f_equal (fun x => (- (x * _))%R)).
cut (0 <= fexp ex - fexp (fexp ex + 1))%Z. 2: omega.
clear.
case (fexp ex - fexp (fexp ex + 1))%Z ; trivial.
intros ep Hp.
now elim Hp.
466
intros H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
467
468
469
apply f_equal.
apply sym_eq.
apply ln_beta_unique.
470
471
rewrite Rabs_left.
rewrite Ropp_involutive.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
472
473
474
475
476
split.
replace (fexp ex + 1 - 1)%Z with (fexp ex) by ring.
apply Rle_refl.
apply -> epow_lt.
apply Zlt_succ.
477
478
479
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
apply epow_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
480
481
split.
(* - . smaller *)
482
483
apply Ropp_le_cancel.
rewrite Ropp_involutive.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
484
485
486
487
488
489
490
491
492
apply Rlt_le.
apply Rlt_le_trans with (1 := Hx2).
now apply -> epow_le.
(* - . biggest *)
intros g ((gm, ge), (Hg1, Hg2)) Hgx.
apply Rnot_lt_le.
intros Hg3.
assert (Hg4 : (g < 0)%R).
now apply Rle_lt_trans with (1 := Hgx).
493
494
specialize (Hg2 (Rlt_not_eq _ _ Hg4)).
destruct (ln_beta beta (Rabs g) (Rabs_pos_lt g (Rlt_not_eq g 0 Hg4))) as (ge', Hge).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
495
simpl in Hg2.
496
rewrite (Rabs_left _ Hg4) in Hge.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
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
523
524
assert (Hge' : (ge' <= fexp ex)%Z).
cut (ge' - 1 < fexp ex)%Z. omega.
apply <- epow_lt.
apply Rle_lt_trans with (1 := proj1 Hge).
apply Ropp_lt_cancel.
now rewrite Ropp_involutive.
rewrite (proj2 (proj2 (valid_fexp _) He1) _ Hge') in Hg2.
rewrite <- Hg2 in Hge'.
apply Rlt_not_le with (1 := proj2 Hge).
rewrite Hg1.
unfold F2R. simpl.
rewrite <- Ropp_mult_distr_l_reverse.
replace ge with (ge - ge' + ge')%Z by ring.
rewrite epow_add.
rewrite <- Rmult_assoc.
pattern (bpow ge') at 1 ; rewrite <- Rmult_1_l.
apply Rmult_le_compat_r.
apply epow_ge_0.
rewrite <- opp_Z2R.
assert (1 <= -gm)%Z.
apply (Zlt_le_succ 0).
apply lt_Z2R.
apply Rmult_lt_reg_r with (bpow ge).
apply epow_gt_0.
rewrite Rmult_0_l.
rewrite opp_Z2R.
rewrite Ropp_mult_distr_l_reverse.
unfold F2R in Hg1. simpl in Hg1.
525
526
527
rewrite <- Hg1.
rewrite <- Ropp_0.
now apply Ropp_lt_contravar.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
apply Rle_trans with (1 * bpow (ge - ge')%Z)%R.
rewrite Rmult_1_l.
cut (0 <= ge - ge')%Z. 2: omega.
clear.
case (ge - ge')%Z.
intros _.
apply Rle_refl.
intros ep _.
simpl.
apply (Z2R_le 1).
apply (Zlt_le_succ 0).
apply Zpower_pos_lt.
now apply Zlt_le_trans with (2 := radix_prop beta).
intros ep Hp. now elim Hp.
apply Rmult_le_compat_r.
apply epow_ge_0.
now apply (Z2R_le 1).
(* - . . *)
apply sym_eq.
apply (up_tech _ (-1)).
apply Ropp_le_cancel.
simpl.
rewrite Ropp_involutive.
change R1 with (bpow Z0).
rewrite <- (Zplus_opp_r (fexp ex)).
rewrite epow_add.
rewrite <- Ropp_mult_distr_l_reverse.
apply Rmult_le_compat_r.
apply epow_ge_0.
apply Rlt_le.
apply Rlt_le_trans with (1 := Hx2).
now apply -> epow_le.
simpl.
rewrite <- (Rmult_0_l (bpow (- fexp ex)%Z)).
apply Rmult_lt_compat_r.
apply epow_gt_0.
exact Hx.
Qed.

End RND_generic.