MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

Flocq_Raux.v 13.3 KB
Newer Older
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1
2
3
Require Export Reals.
Require Export ZArith.

4
5
Section Rmissing.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
6
7
8
9
10
11
12
13
14
Lemma Rle_0_minus :
  forall x y, (x <= y)%R -> (0 <= y - x)%R.
Proof.
intros.
apply Rge_le.
apply Rge_minus.
now apply Rle_ge.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
Lemma Rabs_eq_Rabs :
  forall x y : R,
  Rabs x = Rabs y -> x = y \/ x = Ropp y.
Proof.
intros x y H.
unfold Rabs in H.
destruct (Rcase_abs x) as [_|_].
assert (H' := f_equal Ropp H).
rewrite Ropp_involutive in H'.
rewrite H'.
destruct (Rcase_abs y) as [_|_].
left.
apply Ropp_involutive.
now right.
rewrite H.
now destruct (Rcase_abs y) as [_|_] ; [right|left].
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
33
34
35
36
37
38
39
40
41
Lemma Rplus_le_reg_r :
  forall r r1 r2 : R,
  (r1 + r <= r2 + r)%R -> (r1 <= r2)%R.
Proof.
intros.
apply Rplus_le_reg_l with r.
now rewrite 2!(Rplus_comm r).
Qed.

42
43
44
45
46
47
48
49
50
51
Lemma Rmult_lt_reg_r :
  forall r r1 r2 : R, (0 < r)%R ->
  (r1 * r < r2 * r)%R -> (r1 < r2)%R.
Proof.
intros.
apply Rmult_lt_reg_l with r.
exact H.
now rewrite 2!(Rmult_comm r).
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
52
53
54
55
56
57
58
59
60
61
Lemma Rmult_le_reg_r :
  forall r r1 r2 : R, (0 < r)%R ->
  (r1 * r <= r2 * r)%R -> (r1 <= r2)%R.
Proof.
intros.
apply Rmult_le_reg_l with r.
exact H.
now rewrite 2!(Rmult_comm r).
Qed.

62
63
64
65
66
67
68
69
70
71
72
Lemma exp_increasing_weak :
  forall x y : R,
  (x <= y)%R -> (exp x <= exp y)%R.
Proof.
intros x y [H|H].
apply Rlt_le.
now apply exp_increasing.
rewrite H.
apply Rle_refl.
Qed.

73
74
End Rmissing.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
75
76
77
78
79
80
81
82
83
84
85
86
87
Section Zmissing.

Lemma Zopp_le_cancel :
  forall x y : Z,
  (-y <= -x)%Z -> Zle x y.
Proof.
intros x y Hxy.
apply Zplus_le_reg_r with (-x - y)%Z.
now ring_simplify.
Qed.

End Zmissing.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
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
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
Section Z2R.

Fixpoint P2R (p : positive) :=
  match p with
  | xH => 1%R
  | xO xH => 2%R
  | xO t => (2 * P2R t)%R
  | xI xH => 3%R
  | xI t => (1 + 2 * P2R t)%R
  end.

Definition Z2R n :=
  match n with
  | Zpos p => P2R p
  | Zneg p => Ropp (P2R p)
  | Z0 => R0
  end.

Lemma P2R_INR :
  forall n, P2R n = INR (nat_of_P n).
Proof.
induction n ; simpl ; try (
  rewrite IHn ;
  rewrite <- (mult_INR 2) ;
  rewrite <- (nat_of_P_mult_morphism 2) ;
  change (2 * n)%positive with (xO n)).
(* xI *)
rewrite (Rplus_comm 1).
change (nat_of_P (xO n)) with (Pmult_nat n 2).
case n ; intros ; simpl ; try apply refl_equal.
case (Pmult_nat p 4) ; intros ; try apply refl_equal.
rewrite Rplus_0_l.
apply refl_equal.
apply Rplus_comm.
(* xO *)
case n ; intros ; apply refl_equal.
(* xH *)
apply refl_equal.
Qed.

Lemma Z2R_IZR :
  forall n, Z2R n = IZR n.
Proof.
intro.
case n ; intros ; simpl.
apply refl_equal.
apply P2R_INR.
apply Ropp_eq_compat.
apply P2R_INR.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
139
140
141
142
143
144
145
146
Lemma opp_Z2R :
  forall n, Z2R (-n) = (- Z2R n)%R.
Proof.
intros.
repeat rewrite Z2R_IZR.
apply Ropp_Ropp_IZR.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
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
Lemma plus_Z2R :
  forall m n, (Z2R (m + n) = Z2R m + Z2R n)%R.
Proof.
intros.
repeat rewrite Z2R_IZR.
apply plus_IZR.
Qed.

Lemma minus_IZR :
  forall n m : Z,
  IZR (n - m) = (IZR n - IZR m)%R.
Proof.
intros.
unfold Zminus.
rewrite plus_IZR.
rewrite Ropp_Ropp_IZR.
apply refl_equal.
Qed.

Lemma minus_Z2R :
  forall m n, (Z2R (m - n) = Z2R m - Z2R n)%R.
Proof.
intros.
repeat rewrite Z2R_IZR.
apply minus_IZR.
Qed.

Lemma mult_Z2R :
  forall m n, (Z2R (m * n) = Z2R m * Z2R n)%R.
Proof.
intros.
repeat rewrite Z2R_IZR.
apply mult_IZR.
Qed.

Lemma le_Z2R :
  forall m n, (Z2R m <= Z2R n)%R -> (m <= n)%Z.
Proof.
intros m n.
repeat rewrite Z2R_IZR.
apply le_IZR.
Qed.

Lemma Z2R_le :
  forall m n, (m <= n)%Z -> (Z2R m <= Z2R n)%R.
Proof.
intros m n.
repeat rewrite Z2R_IZR.
apply IZR_le.
Qed.

Lemma lt_Z2R :
  forall m n, (Z2R m < Z2R n)%R -> (m < n)%Z.
Proof.
intros m n.
repeat rewrite Z2R_IZR.
apply lt_IZR.
Qed.

Lemma Z2R_lt :
  forall m n, (m < n)%Z -> (Z2R m < Z2R n)%R.
Proof.
intros m n.
repeat rewrite Z2R_IZR.
apply IZR_lt.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
214
215
216
217
218
219
Lemma Z2R_lt_le:  forall e1 e2, (Z2R (e1-1) < Z2R e2)%R -> (Z2R e1 <= Z2R e2)%R.
intros.
apply Z2R_le.
assert (e1 -1 < e2)%Z; auto with zarith.
now apply lt_Z2R.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
220
221
222
223
224
225
226
227
228

Lemma Z2R_neq :
forall m n, (m <> n)%Z -> (Z2R m <> Z2R n)%R.
Proof.
intros m n.
repeat rewrite Z2R_IZR.
apply IZR_neq.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
229
230
231
232
233
234
Lemma Rabs_Z2R: forall z, Rabs (Z2R z) = Z2R (Zabs z).
intros.
repeat rewrite Z2R_IZR.
apply Rabs_Zabs. 
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
235
236
End Z2R.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
237
238
239
240
241
242
243
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
282
283
284
Section Floor_Ceil.

Definition Zfloor (x : R) := (up x - 1)%Z.

Lemma Zfloor_lb :
  forall x : R,
  (Z2R (Zfloor x) <= x)%R.
Proof.
intros x.
unfold Zfloor.
rewrite minus_Z2R.
simpl.
rewrite Z2R_IZR.
apply Rplus_le_reg_r with (1 - x)%R.
ring_simplify.
exact (proj2 (archimed x)).
Qed.

Lemma Zfloor_lub :
  forall n x,
  (Z2R n <= x)%R ->
  (n <= Zfloor x)%Z.
Proof.
intros n x Hnx.
apply Zlt_succ_le.
unfold Zfloor.
change (n < Zsucc (Zpred (up x)))%Z.
rewrite <- Zsucc_pred.
apply lt_Z2R.
apply Rle_lt_trans with (1 := Hnx).
rewrite Z2R_IZR.
exact (proj1 (archimed x)).
Qed.

Lemma Zfloor_imp :
  forall n x,
  (Z2R n <= x < Z2R (n + 1))%R ->
  Zfloor x = n.
Proof.
intros n x Hnx.
apply Zle_antisym.
apply Zlt_succ_le.
apply lt_Z2R.
apply Rle_lt_trans with (2 := proj2 Hnx).
apply Zfloor_lb.
now apply Zfloor_lub.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
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
Definition Zceil (x : R) := (- Zfloor (- x))%Z.

Lemma Zceil_ub :
  forall x : R,
  (x <= Z2R (Zceil x))%R.
Proof.
intros x.
unfold Zceil.
rewrite opp_Z2R.
apply Ropp_le_cancel.
rewrite Ropp_involutive.
apply Zfloor_lb.
Qed.

Lemma Zceil_lub :
  forall n x,
  (x <= Z2R n)%R ->
  (Zceil x <= n)%Z.
Proof.
intros n x Hnx.
unfold Zceil.
apply Zopp_le_cancel.
rewrite Zopp_involutive.
apply Zfloor_lub.
rewrite opp_Z2R.
now apply Ropp_le_contravar.
Qed.

Lemma Zceil_imp :
  forall n x,
  (Z2R (n - 1) < x <= Z2R n)%R ->
  Zceil x = n.
Proof.
intros n x Hnx.
unfold Zceil.
rewrite <- (Zopp_involutive n).
apply f_equal.
apply Zfloor_imp.
split.
rewrite opp_Z2R.
now apply Ropp_le_contravar.
rewrite <- (Zopp_involutive 1).
rewrite <- Zopp_plus_distr.
rewrite opp_Z2R.
now apply Ropp_lt_contravar.
Qed.

Lemma Zceil_floor_neq :
  forall x,
  (Z2R (Zfloor x) <> x)%R ->
  (Zceil x = Zfloor x + 1)%Z.
Proof.
intros x Hx.
apply Zceil_imp.
split.
ring_simplify (Zfloor x + 1 - 1)%Z.
apply Rnot_le_lt.
intros H.
apply Hx.
apply Rle_antisym.
apply Zfloor_lb.
exact H.
apply Rnot_lt_le.
clear Hx. intros Hx.
generalize (Zfloor_lub _ _ (Rlt_le _ _ Hx)).
omega.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
353
End Floor_Ceil.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
354
355
356

Section pow.

357
Record radix :=  { radix_val : Z ; radix_prop :  (2 <= radix_val )%Z }.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
358
359
360

Variable r: radix.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
361
Lemma radix_pos: (0 < Z2R (radix_val r))%R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
362
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
363
364
365
366
367
368
destruct r; simpl.
apply Rle_lt_trans with (Z2R 0).
right; reflexivity.
apply Z2R_lt; auto with zarith.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
Definition epow e :=
  match e with
  | Zpos p => Z2R (Zpower_pos (radix_val r) p)
  | Zneg p => Rinv (Z2R (Zpower_pos (radix_val r) p))
  | Z0 => R1
  end.

Lemma Zpower_pos_powerRZ :
  forall n m,
  Z2R (Zpower_pos n m) = powerRZ (Z2R n) (Zpos m).
Proof.
intros.
rewrite Zpower_pos_nat.
simpl.
induction (nat_of_P m).
apply refl_equal.
unfold Zpower_nat.
simpl.
rewrite mult_Z2R.
apply Rmult_eq_compat_l.
exact IHn0.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
392
Lemma epow_powerRZ :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
393
  forall e,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
394
395
396
397
398
399
400
401
  epow e = powerRZ (Z2R (radix_val r)) e.
Proof.
destruct e ; unfold epow.
reflexivity.
now rewrite Zpower_pos_powerRZ.
now rewrite Zpower_pos_powerRZ.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
402
Lemma  epow_ge_0 :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
  forall e : Z, (0 <= epow e)%R.
Proof.
intros.
rewrite epow_powerRZ.
apply powerRZ_le.
change R0 with (Z2R 0).
apply Z2R_lt.
destruct r; simpl; auto with zarith.
Qed.

Lemma epow_gt_0 :
  forall e : Z, (0 < epow e)%R.
Proof.
intros.
rewrite epow_powerRZ.
apply powerRZ_lt.
change R0 with (Z2R 0).
apply Z2R_lt.
destruct r; simpl; auto with zarith.
Qed.

Lemma epow_add :
425
  forall e1 e2 : Z, (epow (e1 + e2) = epow e1 * epow e2)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
Proof.
intros.
repeat rewrite epow_powerRZ.
apply powerRZ_add.
change R0 with (Z2R 0).
apply Z2R_neq.
destruct r; simpl; auto with zarith.
Qed.

Lemma epow_1 :
  epow 1 = Z2R (radix_val r).
Proof.
unfold epow, Zpower_pos, iter_pos.
now rewrite Zmult_1_r.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
Lemma epow_add1 :
  forall e : Z, (epow (e+1) = Z2R (radix_val r) * epow e)%R.
Proof.
intros.
rewrite <- epow_1.
rewrite <- epow_add.
now rewrite Zplus_comm.
Qed.

Lemma epow_opp :
  forall e : Z, (epow (-e) = /epow e)%R.
Proof.
intros e; destruct e.
simpl; now rewrite Rinv_1.
now replace (-Zpos p)%Z with (Zneg p) by reflexivity.
replace (-Zneg p)%Z with (Zpos p) by reflexivity.
simpl; rewrite Rinv_involutive; trivial.
generalize (epow_gt_0 (Zpos p)).
simpl; auto with real.
Qed.

463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
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
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
Lemma Z2R_Zpower :
  forall e : Z,
  (0 <= e)%Z ->
  Z2R (Zpower (radix_val r) e) = epow e.
Proof.
intros [|e|e] H.
split.
split.
now elim H.
Qed.

Lemma epow_lt_aux :
  forall e1 e2 : Z,
  (e1 < e2)%Z -> (epow e1 < epow e2)%R.
Proof.
intros e1 e2 H.
replace e2 with (e1 + (e2 - e1))%Z by ring.
rewrite <- (Rmult_1_r (epow e1)).
rewrite epow_add.
apply Rmult_lt_compat_l.
apply epow_gt_0.
assert (0 < e2 - e1)%Z by omega.
destruct (e2 - e1)%Z ; try discriminate H0.
clear.
unfold epow.
apply (Z2R_lt 1).
rewrite Zpower_pos_nat.
case_eq (nat_of_P p).
intros H.
elim (lt_irrefl 0).
pattern O at 2 ; rewrite <- H.
apply lt_O_nat_of_P.
intros n _.
assert (1 < Zpower_nat (radix_val r) 1)%Z.
unfold Zpower_nat, iter_nat.
rewrite Zmult_1_r.
generalize (radix_prop r).
omega.
induction n.
exact H.
change (S (S n)) with (1 + (S n))%nat.
rewrite Zpower_nat_is_exp.
change 1%Z with (1 * 1)%Z.
apply Zmult_lt_compat.
now split.
now split.
Qed.

Lemma epow_lt :
  forall e1 e2 : Z,
  (e1 < e2)%Z <-> (epow e1 < epow e2)%R.
Proof.
intros e1 e2.
split.
apply epow_lt_aux.
intros H.
apply Zgt_lt.
apply Znot_le_gt.
intros H'.
apply Rlt_not_le with (1 := H).
destruct (Zle_lt_or_eq _ _ H').
apply Rlt_le.
now apply epow_lt_aux.
apply Req_le.
now apply f_equal.
Qed.

Lemma epow_le :
  forall e1 e2 : Z,
  (e1 <= e2)%Z <-> (epow e1 <= epow e2)%R.
Proof.
intros e1 e2.
split.
intros H.
apply Rnot_lt_le.
intros H'.
apply Zle_not_gt with (1 := H).
apply Zlt_gt.
now apply <- epow_lt.
intros H.
apply Znot_gt_le.
intros H'.
apply Rle_not_lt with (1 := H).
apply -> epow_lt.
now apply Zgt_lt.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
549

550
551
552
553
554
555
556
557
558
559
Lemma epow_eq :
  forall e1 e2 : Z,
  e1 = e2 -> epow e1 = epow e2.
Proof.
intros.
apply Rle_antisym.
apply -> epow_le.
now apply Zeq_le.
apply -> epow_le.
apply Zeq_le.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
560
now apply sym_eq.
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
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
Qed.

Lemma epow_exp :
  forall e : Z,
  epow e = exp (Z2R e * ln (Z2R (radix_val r))).
Proof.
(* positive case *)
assert (forall e, epow (Zpos e) = exp (Z2R (Zpos e) * ln (Z2R (radix_val r)))).
intros e.
unfold epow.
rewrite Zpower_pos_nat.
unfold Z2R at 2.
rewrite P2R_INR.
induction (nat_of_P e).
rewrite Rmult_0_l.
unfold Zpower_nat, iter_nat.
now rewrite exp_0.
change (S n) with (1 + n)%nat.
rewrite plus_INR.
rewrite Zpower_nat_is_exp.
rewrite Rmult_plus_distr_r.
rewrite exp_plus.
rewrite Rmult_1_l.
rewrite exp_ln.
rewrite <- IHn.
rewrite <- mult_Z2R.
apply f_equal.
unfold Zpower_nat at 1, iter_nat.
now rewrite Zmult_1_r.
apply (Z2R_lt 0).
generalize (radix_prop r).
omega.
(* general case *)
intros [|e|e].
rewrite Rmult_0_l.
now rewrite exp_0.
apply H.
unfold epow.
change (Z2R (Zpower_pos (radix_val r) e)) with (epow (Zpos e)).
rewrite H.
rewrite <- exp_Ropp.
rewrite <- Ropp_mult_distr_l_reverse.
now rewrite <- opp_Z2R.
Qed.

Lemma ln_beta :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
607
608
  forall x : R,
  {e | (0 < x)%R -> (epow (e - 1)%Z <= x < epow e)%R}.
609
Proof.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
610
intros x.
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
set (fact := ln (Z2R (radix_val r))).
(* . *)
assert (0 < fact)%R.
apply exp_lt_inv.
rewrite exp_0.
unfold fact.
rewrite exp_ln.
apply (Z2R_lt 1).
generalize (radix_prop r).
omega.
apply (Z2R_lt 0).
generalize (radix_prop r).
omega.
(* . *)
exists (up (ln x / fact))%Z.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
626
intros Hx.
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
rewrite 2!epow_exp.
fold fact.
pattern x at 2 3 ; replace x with (exp (ln x / fact * fact)).
split.
rewrite minus_Z2R.
apply exp_increasing_weak.
apply Rmult_le_compat_r.
now apply Rlt_le.
simpl (Z2R 1).
pattern (ln x / fact)%R at 2 ; replace (ln x / fact)%R with (1 + (ln x / fact - 1))%R by ring.
replace (Z2R (up (ln x / fact)) - 1)%R with ((Z2R (up (ln x / fact)) - ln x / fact) + (ln x / fact - 1))%R by ring.
apply Rplus_le_compat_r.
rewrite Z2R_IZR.
eapply for_base_fp.
apply exp_increasing.
apply Rmult_lt_compat_r.
exact H.
rewrite Z2R_IZR.
apply Rplus_lt_reg_r with (- (ln x / fact))%R.
rewrite Rplus_opp_l.
rewrite Rplus_comm.
eapply for_base_fp.
unfold Rdiv.
rewrite Rmult_assoc.
rewrite Rinv_l.
rewrite Rmult_1_r.
now apply exp_ln.
now apply Rgt_not_eq.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
657
658
659
660
661
662
663
664
665
666
667
Lemma epow_lt_epow :
  forall e1 e2,
  (epow (e1 - 1) < epow e2)%R ->
  (e1 <= e2)%Z.
Proof.
intros e1 e2 He.
rewrite (Zsucc_pred e1).
apply Zlt_le_succ.
now apply <- epow_lt.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
668
669
670
671
672
673
674
Lemma epow_unique :
  forall x e1 e2,
  (epow (e1 - 1) <= x < epow e1)%R ->
  (epow (e2 - 1) <= x < epow e2)%R ->
  e1 = e2.
Proof.
intros x e1 e2 (H1a,H1b) (H2a,H2b).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
675
676
677
678
apply Zle_antisym ;
  apply epow_lt_epow ;
  apply Rle_lt_trans with x ;
  assumption.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
679
680
681
Qed.

Lemma ln_beta_unique :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
682
  forall (x : R) (e : Z),
Guillaume Melquiond's avatar
Guillaume Melquiond committed
683
  (epow (e - 1) <= x < epow e)%R ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
684
  projT1 (ln_beta x) = e.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
685
Proof.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
686
687
688
689
690
691
692
intros x e1 Hx1.
destruct (ln_beta x) as (e2, Hx2).
apply epow_unique with (2 := Hx1).
simpl.
apply Hx2.
apply Rlt_le_trans with (2 := proj1 Hx1).
apply epow_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
693
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
694

Guillaume Melquiond's avatar
Guillaume Melquiond committed
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
Lemma ln_beta_monotone :
  forall x y,
  (0 < x)%R -> (x <= y)%R ->
  (projT1 (ln_beta x) <= projT1 (ln_beta y))%Z.
Proof.
intros x y H0x Hxy.
destruct (ln_beta x) as (ex, Hx).
destruct (ln_beta y) as (ey, Hy).
simpl.
apply epow_lt_epow.
specialize (Hx H0x).
specialize (Hy (Rlt_le_trans _ _ _ H0x Hxy)).
apply Rle_lt_trans with (1 := proj1 Hx).
now apply Rle_lt_trans with (2 := proj2 Hy).
Qed.

711
712
713
714
715
716
717
Lemma Zpower_pos_gt_0 :
  forall b p, (0 < b)%Z ->
  (0 < Zpower_pos b p)%Z.
Proof.
intros b p Hb.
apply lt_Z2R.
rewrite Zpower_pos_powerRZ.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
718
apply powerRZ_lt.
719
now apply (Z2R_lt 0).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
720
721
Qed.

722
723
Lemma Zpower_gt_0 :
  forall b p,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
724
  (0 < b)%Z -> (0 <= p)%Z ->
725
726
727
728
  (0 < Zpower b p)%Z.
Proof.
intros b p Hb Hz.
unfold Zpower.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
729
730
destruct p.
easy.
731
now apply Zpower_pos_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
732
now elim Hz.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
733
734
Qed.

735
736
737
738
739
Lemma Zpower_gt_1 :
  forall p,
  (0 < p)%Z ->
  (1 < Zpower (radix_val r) p)%Z.
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
740
741
intros.
apply lt_Z2R.
742
743
744
rewrite Z2R_Zpower.
now apply -> (epow_lt 0).
now apply Zlt_le_weak.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
745
746
Qed.

747
End pow.