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

4 5
Section Rmissing.

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

15
Theorem Rabs_eq_Rabs :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
  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.

33
Theorem Rplus_le_reg_r :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
34 35 36 37 38 39 40 41
  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
Theorem Rmult_lt_reg_r :
43 44 45 46 47 48 49 50 51
  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.

52
Theorem Rmult_le_reg_r :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
53 54 55 56 57 58 59 60 61
  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
Theorem Rmult_eq_reg_r :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
63 64 65 66 67 68 69 70 71
  forall r r1 r2 : R, (r1 * r)%R = (r2 * r)%R ->
  r <> 0%R -> r1 = r2.
Proof.
intros r r1 r2 H1 H2.
apply Rmult_eq_reg_l with r.
now rewrite 2!(Rmult_comm r).
exact H2.
Qed.

72
Theorem exp_increasing_weak :
73 74 75 76 77 78 79 80 81 82
  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.

83 84
End Rmissing.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
85 86
Section Zmissing.

87
Theorem Zopp_le_cancel :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
88 89 90 91 92 93 94 95 96 97
  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
98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
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.

116
Theorem P2R_INR :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137
  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.

138
Theorem Z2R_IZR :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
139 140 141 142 143 144 145 146 147 148
  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.

149
Theorem opp_Z2R :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
150 151 152 153 154 155 156
  forall n, Z2R (-n) = (- Z2R n)%R.
Proof.
intros.
repeat rewrite Z2R_IZR.
apply Ropp_Ropp_IZR.
Qed.

157
Theorem plus_Z2R :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
158 159 160 161 162 163 164
  forall m n, (Z2R (m + n) = Z2R m + Z2R n)%R.
Proof.
intros.
repeat rewrite Z2R_IZR.
apply plus_IZR.
Qed.

165
Theorem minus_IZR :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
166 167 168 169 170 171 172 173 174 175
  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.

176
Theorem minus_Z2R :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
177 178 179 180 181 182 183
  forall m n, (Z2R (m - n) = Z2R m - Z2R n)%R.
Proof.
intros.
repeat rewrite Z2R_IZR.
apply minus_IZR.
Qed.

184
Theorem mult_Z2R :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
185 186 187 188 189 190 191
  forall m n, (Z2R (m * n) = Z2R m * Z2R n)%R.
Proof.
intros.
repeat rewrite Z2R_IZR.
apply mult_IZR.
Qed.

192
Theorem le_Z2R :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
193 194 195 196 197 198 199
  forall m n, (Z2R m <= Z2R n)%R -> (m <= n)%Z.
Proof.
intros m n.
repeat rewrite Z2R_IZR.
apply le_IZR.
Qed.

200
Theorem Z2R_le :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
201 202 203 204 205 206 207
  forall m n, (m <= n)%Z -> (Z2R m <= Z2R n)%R.
Proof.
intros m n.
repeat rewrite Z2R_IZR.
apply IZR_le.
Qed.

208
Theorem lt_Z2R :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
209 210 211 212 213 214 215
  forall m n, (Z2R m < Z2R n)%R -> (m < n)%Z.
Proof.
intros m n.
repeat rewrite Z2R_IZR.
apply lt_IZR.
Qed.

216
Theorem Z2R_lt :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
217 218 219 220 221 222 223
  forall m n, (m < n)%Z -> (Z2R m < Z2R n)%R.
Proof.
intros m n.
repeat rewrite Z2R_IZR.
apply IZR_lt.
Qed.

224
Theorem Z2R_le_lt :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
225 226 227 228 229 230 231 232
  forall m n p, (m <= n < p)%Z -> (Z2R m <= Z2R n < Z2R p)%R.
Proof.
intros m n p (H1, H2).
split.
now apply Z2R_le.
now apply Z2R_lt.
Qed.

233
Theorem le_lt_Z2R :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
234 235 236 237 238
  forall m n p, (Z2R m <= Z2R n < Z2R p)%R -> (m <= n < p)%Z.
Proof.
intros m n p (H1, H2).
split.
now apply le_Z2R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
239 240
now apply lt_Z2R.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
241

242
Theorem eq_Z2R :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
243 244 245 246 247 248 249
  forall m n, (Z2R m = Z2R n)%R -> (m = n)%Z.
Proof.
intros m n H.
apply eq_IZR.
now rewrite <- 2!Z2R_IZR.
Qed.

250
Theorem neq_Z2R :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
251 252 253 254 255 256 257
  forall m n, (Z2R m <> Z2R n)%R -> (m <> n)%Z.
Proof.
intros m n H H'.
apply H.
now apply f_equal.
Qed.

258
Theorem Z2R_neq :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
259
  forall m n, (m <> n)%Z -> (Z2R m <> Z2R n)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
260 261 262 263 264 265
Proof.
intros m n.
repeat rewrite Z2R_IZR.
apply IZR_neq.
Qed.

266 267
Theorem abs_Z2R :
  forall z, Z2R (Zabs z) = Rabs (Z2R z).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
268
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
269 270
intros.
repeat rewrite Z2R_IZR.
271
now rewrite Rabs_Zabs.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
272 273
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
274 275
End Z2R.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
276 277 278 279
Section Floor_Ceil.

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

280
Theorem Zfloor_lb :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
281 282 283 284 285 286 287 288 289 290 291 292 293
  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.

294
Theorem Zfloor_ub :
295 296 297 298 299 300 301 302 303 304 305 306 307
  forall x : R,
  (x < Z2R (Zfloor x) + 1)%R.
Proof.
intros x.
unfold Zfloor.
rewrite minus_Z2R.
unfold Rminus.
rewrite Rplus_assoc.
rewrite Rplus_opp_l, Rplus_0_r.
rewrite Z2R_IZR.
exact (proj1 (archimed x)).
Qed.

308
Theorem Zfloor_lub :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
309 310 311 312 313 314 315 316
  forall n x,
  (Z2R n <= x)%R ->
  (n <= Zfloor x)%Z.
Proof.
intros n x Hnx.
apply Zlt_succ_le.
apply lt_Z2R.
apply Rle_lt_trans with (1 := Hnx).
317 318 319
unfold Zsucc.
rewrite plus_Z2R.
apply Zfloor_ub.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
320 321
Qed.

322
Theorem Zfloor_imp :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
323 324 325 326 327 328 329 330 331 332 333 334 335
  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.

336 337 338 339 340 341 342 343 344 345 346 347
Theorem Zfloor_Z :
  forall n,
  Zfloor (Z2R n) = n.
Proof.
intros n.
apply Zfloor_imp.
split.
apply Rle_refl.
apply Z2R_lt.
apply Zlt_succ.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
348 349
Definition Zceil (x : R) := (- Zfloor (- x))%Z.

350
Theorem Zceil_ub :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
351 352 353 354 355 356 357 358 359 360 361
  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.

362
Theorem Zceil_lub :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
363 364 365 366 367 368 369 370 371 372 373 374 375
  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.

376
Theorem Zceil_imp :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394
  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.

395 396 397 398 399 400 401 402 403 404
Theorem Zceil_Z :
  forall n,
  Zceil (Z2R n) = n.
Proof.
intros n.
unfold Zceil.
rewrite <- opp_Z2R, Zfloor_Z.
apply Zopp_involutive.
Qed.

405
Theorem Zceil_floor_neq :
406
  forall x : R,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
407 408 409 410 411 412 413 414 415 416 417 418 419
  (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.
420 421 422
apply Rlt_le.
rewrite plus_Z2R.
apply Zfloor_ub.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
423 424
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
425
End Floor_Ceil.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
426 427 428

Section pow.

429
Record radix :=  { radix_val : Z ; radix_prop :  (2 <= radix_val )%Z }.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
430 431 432

Variable r: radix.

433
Theorem radix_pos: (0 < Z2R (radix_val r))%R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
434
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
435 436 437 438 439 440
destruct r; simpl.
apply Rle_lt_trans with (Z2R 0).
right; reflexivity.
apply Z2R_lt; auto with zarith.
Qed.

441
Definition bpow e :=
BOLDO Sylvie's avatar
BOLDO Sylvie committed
442 443 444 445 446 447
  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.

448
Theorem Zpower_pos_powerRZ :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
449 450 451 452 453 454 455 456 457 458 459 460 461 462 463
  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.

464
Theorem bpow_powerRZ :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
465
  forall e,
466
  bpow e = powerRZ (Z2R (radix_val r)) e.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
467
Proof.
468
destruct e ; unfold bpow.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
469 470 471 472 473
reflexivity.
now rewrite Zpower_pos_powerRZ.
now rewrite Zpower_pos_powerRZ.
Qed.

474 475
Theorem  bpow_ge_0 :
  forall e : Z, (0 <= bpow e)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
476 477
Proof.
intros.
478
rewrite bpow_powerRZ.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
479 480 481 482 483 484
apply powerRZ_le.
change R0 with (Z2R 0).
apply Z2R_lt.
destruct r; simpl; auto with zarith.
Qed.

485 486
Theorem bpow_gt_0 :
  forall e : Z, (0 < bpow e)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
487 488
Proof.
intros.
489
rewrite bpow_powerRZ.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
490 491 492 493 494 495
apply powerRZ_lt.
change R0 with (Z2R 0).
apply Z2R_lt.
destruct r; simpl; auto with zarith.
Qed.

496 497
Theorem bpow_add :
  forall e1 e2 : Z, (bpow (e1 + e2) = bpow e1 * bpow e2)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
498 499
Proof.
intros.
500
repeat rewrite bpow_powerRZ.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
501 502 503 504 505 506
apply powerRZ_add.
change R0 with (Z2R 0).
apply Z2R_neq.
destruct r; simpl; auto with zarith.
Qed.

507 508
Theorem bpow_1 :
  bpow 1 = Z2R (radix_val r).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
509
Proof.
510
unfold bpow, Zpower_pos, iter_pos.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
511 512 513
now rewrite Zmult_1_r.
Qed.

514 515
Theorem bpow_add1 :
  forall e : Z, (bpow (e+1) = Z2R (radix_val r) * bpow e)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
516 517
Proof.
intros.
518 519
rewrite <- bpow_1.
rewrite <- bpow_add.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
520 521 522
now rewrite Zplus_comm.
Qed.

523 524
Theorem bpow_opp :
  forall e : Z, (bpow (-e) = /bpow e)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
525 526 527 528 529 530
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.
531
generalize (bpow_gt_0 (Zpos p)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
532 533 534
simpl; auto with real.
Qed.

535
Theorem Z2R_Zpower :
536 537
  forall e : Z,
  (0 <= e)%Z ->
538
  Z2R (Zpower (radix_val r) e) = bpow e.
539 540 541 542 543 544 545
Proof.
intros [|e|e] H.
split.
split.
now elim H.
Qed.

546
Theorem bpow_lt_aux :
547
  forall e1 e2 : Z,
548
  (e1 < e2)%Z -> (bpow e1 < bpow e2)%R.
549 550 551
Proof.
intros e1 e2 H.
replace e2 with (e1 + (e2 - e1))%Z by ring.
552 553
rewrite <- (Rmult_1_r (bpow e1)).
rewrite bpow_add.
554
apply Rmult_lt_compat_l.
555
apply bpow_gt_0.
556 557 558
assert (0 < e2 - e1)%Z by omega.
destruct (e2 - e1)%Z ; try discriminate H0.
clear.
559
unfold bpow.
560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582
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.

583
Theorem bpow_lt :
584
  forall e1 e2 : Z,
585
  (e1 < e2)%Z <-> (bpow e1 < bpow e2)%R.
586 587 588
Proof.
intros e1 e2.
split.
589
apply bpow_lt_aux.
590 591 592 593 594 595 596
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.
597
now apply bpow_lt_aux.
598 599 600 601
apply Req_le.
now apply f_equal.
Qed.

602
Theorem bpow_le :
603
  forall e1 e2 : Z,
604
  (e1 <= e2)%Z <-> (bpow e1 <= bpow e2)%R.
605 606 607 608 609 610 611 612
Proof.
intros e1 e2.
split.
intros H.
apply Rnot_lt_le.
intros H'.
apply Zle_not_gt with (1 := H).
apply Zlt_gt.
613
now apply <- bpow_lt.
614 615 616 617
intros H.
apply Znot_gt_le.
intros H'.
apply Rle_not_lt with (1 := H).
618
apply -> bpow_lt.
619 620
now apply Zgt_lt.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
621

622
Theorem bpow_eq :
623
  forall e1 e2 : Z,
624
  bpow e1 = bpow e2 -> e1 = e2.
625 626
Proof.
intros.
627 628 629 630 631
apply Zle_antisym.
apply <- bpow_le.
now apply Req_le.
apply <- bpow_le.
now apply Req_le.
632 633
Qed.

634
Theorem bpow_exp :
635
  forall e : Z,
636
  bpow e = exp (Z2R e * ln (Z2R (radix_val r))).
637 638
Proof.
(* positive case *)
639
assert (forall e, bpow (Zpos e) = exp (Z2R (Zpos e) * ln (Z2R (radix_val r)))).
640
intros e.
641
unfold bpow.
642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668
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.
669 670
unfold bpow.
change (Z2R (Zpower_pos (radix_val r) e)) with (bpow (Zpos e)).
671 672 673 674 675 676
rewrite H.
rewrite <- exp_Ropp.
rewrite <- Ropp_mult_distr_l_reverse.
now rewrite <- opp_Z2R.
Qed.

677
Theorem ln_beta :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
678
  forall x : R,
679
  {e | (x <> 0)%R -> (bpow (e - 1)%Z <= Rabs x < bpow e)%R}.
680
Proof.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
681
intros x.
682 683 684 685 686 687 688 689
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).
690
now apply Zlt_le_trans with (2 := radix_prop r).
691
apply (Z2R_lt 0).
692
now apply Zlt_le_trans with (2 := radix_prop r).
693
(* . *)
694 695 696 697 698
exists (Zfloor (ln (Rabs x) / fact) + 1)%Z.
intros Hx'.
generalize (Rabs_pos_lt _ Hx'). clear Hx'.
generalize (Rabs x). clear x.
intros x Hx.
699
rewrite 2!bpow_exp.
700
fold fact.
701
pattern x at 2 3 ; replace x with (exp (ln x * / fact * fact)).
702 703 704 705 706
split.
rewrite minus_Z2R.
apply exp_increasing_weak.
apply Rmult_le_compat_r.
now apply Rlt_le.
707 708 709 710 711
unfold Rminus.
rewrite plus_Z2R.
rewrite Rplus_assoc.
rewrite Rplus_opp_r, Rplus_0_r.
apply Zfloor_lb.
712 713 714
apply exp_increasing.
apply Rmult_lt_compat_r.
exact H.
715 716
rewrite plus_Z2R.
apply Zfloor_ub.
717 718 719 720 721 722 723
rewrite Rmult_assoc.
rewrite Rinv_l.
rewrite Rmult_1_r.
now apply exp_ln.
now apply Rgt_not_eq.
Qed.

724
Theorem bpow_lt_bpow :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
725
  forall e1 e2,
726
  (bpow (e1 - 1) < bpow e2)%R ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
727 728 729 730 731
  (e1 <= e2)%Z.
Proof.
intros e1 e2 He.
rewrite (Zsucc_pred e1).
apply Zlt_le_succ.
732
now apply <- bpow_lt.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
733 734
Qed.

735
Theorem bpow_unique :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
736
  forall x e1 e2,
737 738
  (bpow (e1 - 1) <= x < bpow e1)%R ->
  (bpow (e2 - 1) <= x < bpow e2)%R ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
739 740 741
  e1 = e2.
Proof.
intros x e1 e2 (H1a,H1b) (H2a,H2b).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
742
apply Zle_antisym ;
743
  apply bpow_lt_bpow ;
Guillaume Melquiond's avatar
Guillaume Melquiond committed
744 745
  apply Rle_lt_trans with x ;
  assumption.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
746 747
Qed.

748
Theorem ln_beta_unique :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
749
  forall (x : R) (e : Z),
750
  (bpow (e - 1) <= Rabs x < bpow e)%R ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
751
  projT1 (ln_beta x) = e.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
752
Proof.
753 754 755 756
intros x e1 He.
destruct (Req_dec x 0) as [Hx|Hx].
elim Rle_not_lt with (1 := proj1 He).
rewrite Hx, Rabs_R0.
757
apply bpow_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
758 759
destruct (ln_beta x) as (e2, Hx2).
simpl.
760
apply bpow_unique with (2 := He).
761 762 763
now apply Hx2.
Qed.

764
Theorem ln_beta_opp :
765 766 767 768 769 770 771 772 773 774 775
  forall x,
  projT1 (ln_beta (-x)) = projT1 (ln_beta x).
Proof.
intros x.
destruct (Req_dec x 0) as [Hx|Hx].
now rewrite Hx, Ropp_0.
destruct (ln_beta x) as (e, He).
simpl.
specialize (He Hx).
apply ln_beta_unique.
now rewrite Rabs_Ropp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
776
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
777

778
Theorem ln_beta_monotone :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
779 780 781 782 783 784 785 786
  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.
787
apply bpow_lt_bpow.
788 789
specialize (Hx (Rgt_not_eq _ _ H0x)).
specialize (Hy (Rgt_not_eq _ _ (Rlt_le_trans _ _ _ H0x Hxy))).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
790
apply Rle_lt_trans with (1 := proj1 Hx).
791 792 793 794 795 796
apply Rle_lt_trans with (2 := proj2 Hy).
rewrite 2!Rabs_pos_eq.
exact Hxy.
apply Rle_trans with (2 := Hxy).
now apply Rlt_le.
now apply Rlt_le.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
797 798
Qed.

799 800 801 802 803 804 805 806 807 808 809 810 811 812 813
Theorem ln_beta_bpow :
  forall e, projT1 (ln_beta (bpow e)) = (e + 1)%Z.
Proof.
intros e.
apply ln_beta_unique.
rewrite Rabs_right.
replace (e + 1 - 1)%Z with e by ring.
split.
apply Rle_refl.
apply -> bpow_lt.
apply Zlt_succ.
apply Rle_ge.
apply bpow_ge_0.
Qed.

814
Theorem Zpower_pos_gt_0 :
815 816 817 818 819 820
  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
821
apply powerRZ_lt.
822
now apply (Z2R_lt 0).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
823 824
Qed.

825
Theorem Zpower_gt_0 :
826
  forall b p,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
827
  (0 < b)%Z -> (0 <= p)%Z ->
828 829 830 831
  (0 < Zpower b p)%Z.
Proof.
intros b p Hb Hz.
unfold Zpower.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
832 833
destruct p.
easy.
834
now apply Zpower_pos_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
835
now elim Hz.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
836 837
Qed.

838
Theorem Zpower_gt_1 :
839 840 841 842
  forall p,
  (0 < p)%Z ->
  (1 < Zpower (radix_val r) p)%Z.
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
843 844
intros.
apply lt_Z2R.
845
rewrite Z2R_Zpower.
846
now apply -> (bpow_lt 0).
847
now apply Zlt_le_weak.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
848 849
Qed.

850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887
Theorem Zpower_Zpower_nat :
  forall b e, (0 <= e)%Z ->
  Zpower b e = Zpower_nat b (Zabs_nat e).
Proof.
intros b [|e|e] He.
apply refl_equal.
apply Zpower_pos_nat.
elim He.
apply refl_equal.
Qed.

Theorem Zodd_Zpower :
  forall b e, (0 <= e)%Z -> Zodd b ->
  Zodd (Zpower b e).
Proof.
intros b e He Hb.
rewrite Zpower_Zpower_nat.
induction (Zabs_nat e).
exact I.
unfold Zpower_nat. simpl.
now apply Zodd_mult_Zodd.
exact He.
Qed.

Theorem Zeven_Zpower :
  forall b e, (0 < e)%Z -> Zeven b ->
  Zeven (Zpower b e).
Proof.
intros b e He Hb.
replace e with (e - 1 + 1)%Z by ring.
rewrite Zpower_exp.
apply Zeven_mult_Zeven_r.
unfold Zpower, Zpower_pos, iter_pos.
now rewrite Zmult_1_r.
omega.
discriminate.
Qed.

888
End pow.