diff options
Diffstat (limited to 'flocq/Core/Fcore_Raux.v')
| -rw-r--r-- | flocq/Core/Fcore_Raux.v | 1996 |
1 files changed, 1996 insertions, 0 deletions
diff --git a/flocq/Core/Fcore_Raux.v b/flocq/Core/Fcore_Raux.v new file mode 100644 index 0000000..748e36e --- /dev/null +++ b/flocq/Core/Fcore_Raux.v @@ -0,0 +1,1996 @@ +(** +This file is part of the Flocq formalization of floating-point +arithmetic in Coq: http://flocq.gforge.inria.fr/ + +Copyright (C) 2010-2011 Sylvie Boldo +#<br /># +Copyright (C) 2010-2011 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. +*) + +(** * Missing definitions/lemmas *) +Require Export Reals. +Require Export ZArith. +Require Export Fcore_Zaux. + +Section Rmissing. + +(** About R *) +Theorem 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. + +Theorem 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. + +Theorem Rabs_minus_le: + forall x y : R, + (0 <= y)%R -> (y <= 2*x)%R -> + (Rabs (x-y) <= x)%R. +Proof. +intros x y Hx Hy. +unfold Rabs; case (Rcase_abs (x - y)); intros H. +apply Rplus_le_reg_l with x; ring_simplify; assumption. +apply Rplus_le_reg_l with (-x)%R; ring_simplify. +auto with real. +Qed. + +Theorem Rplus_eq_reg_r : + forall r r1 r2 : R, + (r1 + r = r2 + r)%R -> (r1 = r2)%R. +Proof. +intros r r1 r2 H. +apply Rplus_eq_reg_l with r. +now rewrite 2!(Rplus_comm r). +Qed. + +Theorem 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. + +Theorem 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. + +Theorem 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. + +Theorem Rmult_eq_reg_r : + 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. + +Theorem Rmult_minus_distr_r : + forall r r1 r2 : R, + ((r1 - r2) * r = r1 * r - r2 * r)%R. +Proof. +intros r r1 r2. +rewrite <- 3!(Rmult_comm r). +apply Rmult_minus_distr_l. +Qed. + +Theorem Rmult_min_distr_r : + forall r r1 r2 : R, + (0 <= r)%R -> + (Rmin r1 r2 * r)%R = Rmin (r1 * r) (r2 * r). +Proof. +intros r r1 r2 [Hr|Hr]. +unfold Rmin. +destruct (Rle_dec r1 r2) as [H1|H1] ; + destruct (Rle_dec (r1 * r) (r2 * r)) as [H2|H2] ; + try easy. +apply (f_equal (fun x => Rmult x r)). +apply Rle_antisym. +exact H1. +apply Rmult_le_reg_r with (1 := Hr). +apply Rlt_le. +now apply Rnot_le_lt. +apply Rle_antisym. +apply Rmult_le_compat_r. +now apply Rlt_le. +apply Rlt_le. +now apply Rnot_le_lt. +exact H2. +rewrite <- Hr. +rewrite 3!Rmult_0_r. +unfold Rmin. +destruct (Rle_dec 0 0) as [H0|H0]. +easy. +elim H0. +apply Rle_refl. +Qed. + +Theorem Rmult_min_distr_l : + forall r r1 r2 : R, + (0 <= r)%R -> + (r * Rmin r1 r2)%R = Rmin (r * r1) (r * r2). +Proof. +intros r r1 r2 Hr. +rewrite 3!(Rmult_comm r). +now apply Rmult_min_distr_r. +Qed. + +Theorem exp_le : + 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. + +Theorem Rinv_lt : + forall x y, + (0 < x)%R -> (x < y)%R -> (/y < /x)%R. +Proof. +intros x y Hx Hxy. +apply Rinv_lt_contravar. +apply Rmult_lt_0_compat. +exact Hx. +now apply Rlt_trans with x. +exact Hxy. +Qed. + +Theorem Rinv_le : + forall x y, + (0 < x)%R -> (x <= y)%R -> (/y <= /x)%R. +Proof. +intros x y Hx Hxy. +apply Rle_Rinv. +exact Hx. +now apply Rlt_le_trans with x. +exact Hxy. +Qed. + +Theorem sqrt_ge_0 : + forall x : R, + (0 <= sqrt x)%R. +Proof. +intros x. +unfold sqrt. +destruct (Rcase_abs x) as [_|H]. +apply Rle_refl. +apply Rsqrt_positivity. +Qed. + +Theorem Rabs_le : + forall x y, + (-y <= x <= y)%R -> (Rabs x <= y)%R. +Proof. +intros x y (Hyx,Hxy). +unfold Rabs. +case Rcase_abs ; intros Hx. +apply Ropp_le_cancel. +now rewrite Ropp_involutive. +exact Hxy. +Qed. + +Theorem Rabs_le_inv : + forall x y, + (Rabs x <= y)%R -> (-y <= x <= y)%R. +Proof. +intros x y Hxy. +split. +apply Rle_trans with (- Rabs x)%R. +now apply Ropp_le_contravar. +apply Ropp_le_cancel. +rewrite Ropp_involutive, <- Rabs_Ropp. +apply RRle_abs. +apply Rle_trans with (2 := Hxy). +apply RRle_abs. +Qed. + +Theorem Rabs_ge : + forall x y, + (y <= -x \/ x <= y)%R -> (x <= Rabs y)%R. +Proof. +intros x y [Hyx|Hxy]. +apply Rle_trans with (-y)%R. +apply Ropp_le_cancel. +now rewrite Ropp_involutive. +rewrite <- Rabs_Ropp. +apply RRle_abs. +apply Rle_trans with (1 := Hxy). +apply RRle_abs. +Qed. + +Theorem Rabs_ge_inv : + forall x y, + (x <= Rabs y)%R -> (y <= -x \/ x <= y)%R. +Proof. +intros x y. +unfold Rabs. +case Rcase_abs ; intros Hy Hxy. +left. +apply Ropp_le_cancel. +now rewrite Ropp_involutive. +now right. +Qed. + +Theorem Rabs_lt : + forall x y, + (-y < x < y)%R -> (Rabs x < y)%R. +Proof. +intros x y (Hyx,Hxy). +now apply Rabs_def1. +Qed. + +Theorem Rabs_lt_inv : + forall x y, + (Rabs x < y)%R -> (-y < x < y)%R. +Proof. +intros x y H. +now split ; eapply Rabs_def2. +Qed. + +Theorem Rabs_gt : + forall x y, + (y < -x \/ x < y)%R -> (x < Rabs y)%R. +Proof. +intros x y [Hyx|Hxy]. +rewrite <- Rabs_Ropp. +apply Rlt_le_trans with (Ropp y). +apply Ropp_lt_cancel. +now rewrite Ropp_involutive. +apply RRle_abs. +apply Rlt_le_trans with (1 := Hxy). +apply RRle_abs. +Qed. + +Theorem Rabs_gt_inv : + forall x y, + (x < Rabs y)%R -> (y < -x \/ x < y)%R. +Proof. +intros x y. +unfold Rabs. +case Rcase_abs ; intros Hy Hxy. +left. +apply Ropp_lt_cancel. +now rewrite Ropp_involutive. +now right. +Qed. + +End Rmissing. + +Section Z2R. + +(** Z2R function (Z -> R) *) +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. + +Theorem 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. + +Theorem 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. + +Theorem Z2R_opp : + forall n, Z2R (-n) = (- Z2R n)%R. +Proof. +intros. +repeat rewrite Z2R_IZR. +apply Ropp_Ropp_IZR. +Qed. + +Theorem Z2R_plus : + forall m n, (Z2R (m + n) = Z2R m + Z2R n)%R. +Proof. +intros. +repeat rewrite Z2R_IZR. +apply plus_IZR. +Qed. + +Theorem 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. + +Theorem Z2R_minus : + forall m n, (Z2R (m - n) = Z2R m - Z2R n)%R. +Proof. +intros. +repeat rewrite Z2R_IZR. +apply minus_IZR. +Qed. + +Theorem Z2R_mult : + forall m n, (Z2R (m * n) = Z2R m * Z2R n)%R. +Proof. +intros. +repeat rewrite Z2R_IZR. +apply mult_IZR. +Qed. + +Theorem 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. + +Theorem 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. + +Theorem 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. + +Theorem 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. + +Theorem Z2R_le_lt : + 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. + +Theorem le_lt_Z2R : + 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. +now apply lt_Z2R. +Qed. + +Theorem eq_Z2R : + 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. + +Theorem neq_Z2R : + forall m n, (Z2R m <> Z2R n)%R -> (m <> n)%Z. +Proof. +intros m n H H'. +apply H. +now apply f_equal. +Qed. + +Theorem 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. + +Theorem Z2R_abs : + forall z, Z2R (Zabs z) = Rabs (Z2R z). +Proof. +intros. +repeat rewrite Z2R_IZR. +now rewrite Rabs_Zabs. +Qed. + +End Z2R. + +(** Decidable comparison on reals *) +Section Rcompare. + +Definition Rcompare x y := + match total_order_T x y with + | inleft (left _) => Lt + | inleft (right _) => Eq + | inright _ => Gt + end. + +Inductive Rcompare_prop (x y : R) : comparison -> Prop := + | Rcompare_Lt_ : (x < y)%R -> Rcompare_prop x y Lt + | Rcompare_Eq_ : x = y -> Rcompare_prop x y Eq + | Rcompare_Gt_ : (y < x)%R -> Rcompare_prop x y Gt. + +Theorem Rcompare_spec : + forall x y, Rcompare_prop x y (Rcompare x y). +Proof. +intros x y. +unfold Rcompare. +now destruct (total_order_T x y) as [[H|H]|H] ; constructor. +Qed. + +Global Opaque Rcompare. + +Theorem Rcompare_Lt : + forall x y, + (x < y)%R -> Rcompare x y = Lt. +Proof. +intros x y H. +case Rcompare_spec ; intro H'. +easy. +rewrite H' in H. +elim (Rlt_irrefl _ H). +elim (Rlt_irrefl x). +now apply Rlt_trans with y. +Qed. + +Theorem Rcompare_Lt_inv : + forall x y, + Rcompare x y = Lt -> (x < y)%R. +Proof. +intros x y. +now case Rcompare_spec. +Qed. + +Theorem Rcompare_not_Lt : + forall x y, + (y <= x)%R -> Rcompare x y <> Lt. +Proof. +intros x y H1 H2. +apply Rle_not_lt with (1 := H1). +now apply Rcompare_Lt_inv. +Qed. + +Theorem Rcompare_not_Lt_inv : + forall x y, + Rcompare x y <> Lt -> (y <= x)%R. +Proof. +intros x y H. +apply Rnot_lt_le. +contradict H. +now apply Rcompare_Lt. +Qed. + +Theorem Rcompare_Eq : + forall x y, + x = y -> Rcompare x y = Eq. +Proof. +intros x y H. +rewrite H. +now case Rcompare_spec ; intro H' ; try elim (Rlt_irrefl _ H'). +Qed. + +Theorem Rcompare_Eq_inv : + forall x y, + Rcompare x y = Eq -> x = y. +Proof. +intros x y. +now case Rcompare_spec. +Qed. + +Theorem Rcompare_Gt : + forall x y, + (y < x)%R -> Rcompare x y = Gt. +Proof. +intros x y H. +case Rcompare_spec ; intro H'. +elim (Rlt_irrefl x). +now apply Rlt_trans with y. +rewrite H' in H. +elim (Rlt_irrefl _ H). +easy. +Qed. + +Theorem Rcompare_Gt_inv : + forall x y, + Rcompare x y = Gt -> (y < x)%R. +Proof. +intros x y. +now case Rcompare_spec. +Qed. + +Theorem Rcompare_not_Gt : + forall x y, + (x <= y)%R -> Rcompare x y <> Gt. +Proof. +intros x y H1 H2. +apply Rle_not_lt with (1 := H1). +now apply Rcompare_Gt_inv. +Qed. + +Theorem Rcompare_not_Gt_inv : + forall x y, + Rcompare x y <> Gt -> (x <= y)%R. +Proof. +intros x y H. +apply Rnot_lt_le. +contradict H. +now apply Rcompare_Gt. +Qed. + +Theorem Rcompare_Z2R : + forall x y, Rcompare (Z2R x) (Z2R y) = Zcompare x y. +Proof. +intros x y. +case Rcompare_spec ; intros H ; apply sym_eq. +apply Zcompare_Lt. +now apply lt_Z2R. +apply Zcompare_Eq. +now apply eq_Z2R. +apply Zcompare_Gt. +now apply lt_Z2R. +Qed. + +Theorem Rcompare_sym : + forall x y, + Rcompare x y = CompOpp (Rcompare y x). +Proof. +intros x y. +destruct (Rcompare_spec y x) as [H|H|H]. +now apply Rcompare_Gt. +now apply Rcompare_Eq. +now apply Rcompare_Lt. +Qed. + +Theorem Rcompare_plus_r : + forall z x y, + Rcompare (x + z) (y + z) = Rcompare x y. +Proof. +intros z x y. +destruct (Rcompare_spec x y) as [H|H|H]. +apply Rcompare_Lt. +now apply Rplus_lt_compat_r. +apply Rcompare_Eq. +now rewrite H. +apply Rcompare_Gt. +now apply Rplus_lt_compat_r. +Qed. + +Theorem Rcompare_plus_l : + forall z x y, + Rcompare (z + x) (z + y) = Rcompare x y. +Proof. +intros z x y. +rewrite 2!(Rplus_comm z). +apply Rcompare_plus_r. +Qed. + +Theorem Rcompare_mult_r : + forall z x y, + (0 < z)%R -> + Rcompare (x * z) (y * z) = Rcompare x y. +Proof. +intros z x y Hz. +destruct (Rcompare_spec x y) as [H|H|H]. +apply Rcompare_Lt. +now apply Rmult_lt_compat_r. +apply Rcompare_Eq. +now rewrite H. +apply Rcompare_Gt. +now apply Rmult_lt_compat_r. +Qed. + +Theorem Rcompare_mult_l : + forall z x y, + (0 < z)%R -> + Rcompare (z * x) (z * y) = Rcompare x y. +Proof. +intros z x y. +rewrite 2!(Rmult_comm z). +apply Rcompare_mult_r. +Qed. + +Theorem Rcompare_middle : + forall x d u, + Rcompare (x - d) (u - x) = Rcompare x ((d + u) / 2). +Proof. +intros x d u. +rewrite <- (Rcompare_plus_r (- x / 2 - d / 2) x). +rewrite <- (Rcompare_mult_r (/2) (x - d)). +field_simplify (x + (- x / 2 - d / 2))%R. +now field_simplify ((d + u) / 2 + (- x / 2 - d / 2))%R. +apply Rinv_0_lt_compat. +now apply (Z2R_lt 0 2). +Qed. + +Theorem Rcompare_half_l : + forall x y, Rcompare (x / 2) y = Rcompare x (2 * y). +Proof. +intros x y. +rewrite <- (Rcompare_mult_r 2%R). +unfold Rdiv. +rewrite Rmult_assoc, Rinv_l, Rmult_1_r. +now rewrite Rmult_comm. +now apply (Z2R_neq 2 0). +now apply (Z2R_lt 0 2). +Qed. + +Theorem Rcompare_half_r : + forall x y, Rcompare x (y / 2) = Rcompare (2 * x) y. +Proof. +intros x y. +rewrite <- (Rcompare_mult_r 2%R). +unfold Rdiv. +rewrite Rmult_assoc, Rinv_l, Rmult_1_r. +now rewrite Rmult_comm. +now apply (Z2R_neq 2 0). +now apply (Z2R_lt 0 2). +Qed. + +Theorem Rcompare_sqr : + forall x y, + (0 <= x)%R -> (0 <= y)%R -> + Rcompare (x * x) (y * y) = Rcompare x y. +Proof. +intros x y Hx Hy. +destruct (Rcompare_spec x y) as [H|H|H]. +apply Rcompare_Lt. +now apply Rsqr_incrst_1. +rewrite H. +now apply Rcompare_Eq. +apply Rcompare_Gt. +now apply Rsqr_incrst_1. +Qed. + +Theorem Rmin_compare : + forall x y, + Rmin x y = match Rcompare x y with Lt => x | Eq => x | Gt => y end. +Proof. +intros x y. +unfold Rmin. +destruct (Rle_dec x y) as [[Hx|Hx]|Hx]. +now rewrite Rcompare_Lt. +now rewrite Rcompare_Eq. +rewrite Rcompare_Gt. +easy. +now apply Rnot_le_lt. +Qed. + +End Rcompare. + +Section Rle_bool. + +Definition Rle_bool x y := + match Rcompare x y with + | Gt => false + | _ => true + end. + +Inductive Rle_bool_prop (x y : R) : bool -> Prop := + | Rle_bool_true_ : (x <= y)%R -> Rle_bool_prop x y true + | Rle_bool_false_ : (y < x)%R -> Rle_bool_prop x y false. + +Theorem Rle_bool_spec : + forall x y, Rle_bool_prop x y (Rle_bool x y). +Proof. +intros x y. +unfold Rle_bool. +case Rcompare_spec ; constructor. +now apply Rlt_le. +rewrite H. +apply Rle_refl. +exact H. +Qed. + +Theorem Rle_bool_true : + forall x y, + (x <= y)%R -> Rle_bool x y = true. +Proof. +intros x y Hxy. +case Rle_bool_spec ; intros H. +apply refl_equal. +elim (Rlt_irrefl x). +now apply Rle_lt_trans with y. +Qed. + +Theorem Rle_bool_false : + forall x y, + (y < x)%R -> Rle_bool x y = false. +Proof. +intros x y Hxy. +case Rle_bool_spec ; intros H. +elim (Rlt_irrefl x). +now apply Rle_lt_trans with y. +apply refl_equal. +Qed. + +End Rle_bool. + +Section Rlt_bool. + +Definition Rlt_bool x y := + match Rcompare x y with + | Lt => true + | _ => false + end. + +Inductive Rlt_bool_prop (x y : R) : bool -> Prop := + | Rlt_bool_true_ : (x < y)%R -> Rlt_bool_prop x y true + | Rlt_bool_false_ : (y <= x)%R -> Rlt_bool_prop x y false. + +Theorem Rlt_bool_spec : + forall x y, Rlt_bool_prop x y (Rlt_bool x y). +Proof. +intros x y. +unfold Rlt_bool. +case Rcompare_spec ; constructor. +exact H. +rewrite H. +apply Rle_refl. +now apply Rlt_le. +Qed. + +Theorem negb_Rlt_bool : + forall x y, + negb (Rle_bool x y) = Rlt_bool y x. +Proof. +intros x y. +unfold Rlt_bool, Rle_bool. +rewrite Rcompare_sym. +now case Rcompare. +Qed. + +Theorem negb_Rle_bool : + forall x y, + negb (Rlt_bool x y) = Rle_bool y x. +Proof. +intros x y. +unfold Rlt_bool, Rle_bool. +rewrite Rcompare_sym. +now case Rcompare. +Qed. + +Theorem Rlt_bool_true : + forall x y, + (x < y)%R -> Rlt_bool x y = true. +Proof. +intros x y Hxy. +rewrite <- negb_Rlt_bool. +now rewrite Rle_bool_false. +Qed. + +Theorem Rlt_bool_false : + forall x y, + (y <= x)%R -> Rlt_bool x y = false. +Proof. +intros x y Hxy. +rewrite <- negb_Rlt_bool. +now rewrite Rle_bool_true. +Qed. + +End Rlt_bool. + +Section Req_bool. + +Definition Req_bool x y := + match Rcompare x y with + | Eq => true + | _ => false + end. + +Inductive Req_bool_prop (x y : R) : bool -> Prop := + | Req_bool_true_ : (x = y)%R -> Req_bool_prop x y true + | Req_bool_false_ : (x <> y)%R -> Req_bool_prop x y false. + +Theorem Req_bool_spec : + forall x y, Req_bool_prop x y (Req_bool x y). +Proof. +intros x y. +unfold Req_bool. +case Rcompare_spec ; constructor. +now apply Rlt_not_eq. +easy. +now apply Rgt_not_eq. +Qed. + +Theorem Req_bool_true : + forall x y, + (x = y)%R -> Req_bool x y = true. +Proof. +intros x y Hxy. +case Req_bool_spec ; intros H. +apply refl_equal. +contradict H. +exact Hxy. +Qed. + +Theorem Req_bool_false : + forall x y, + (x <> y)%R -> Req_bool x y = false. +Proof. +intros x y Hxy. +case Req_bool_spec ; intros H. +contradict Hxy. +exact H. +apply refl_equal. +Qed. + +End Req_bool. + +Section Floor_Ceil. + +(** Zfloor and Zceil *) +Definition Zfloor (x : R) := (up x - 1)%Z. + +Theorem Zfloor_lb : + forall x : R, + (Z2R (Zfloor x) <= x)%R. +Proof. +intros x. +unfold Zfloor. +rewrite Z2R_minus. +simpl. +rewrite Z2R_IZR. +apply Rplus_le_reg_r with (1 - x)%R. +ring_simplify. +exact (proj2 (archimed x)). +Qed. + +Theorem Zfloor_ub : + forall x : R, + (x < Z2R (Zfloor x) + 1)%R. +Proof. +intros x. +unfold Zfloor. +rewrite Z2R_minus. +unfold Rminus. +rewrite Rplus_assoc. +rewrite Rplus_opp_l, Rplus_0_r. +rewrite Z2R_IZR. +exact (proj1 (archimed x)). +Qed. + +Theorem Zfloor_lub : + 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). +unfold Zsucc. +rewrite Z2R_plus. +apply Zfloor_ub. +Qed. + +Theorem 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. + +Theorem Zfloor_Z2R : + forall n, + Zfloor (Z2R n) = n. +Proof. +intros n. +apply Zfloor_imp. +split. +apply Rle_refl. +apply Z2R_lt. +apply Zlt_succ. +Qed. + +Theorem Zfloor_le : + forall x y, (x <= y)%R -> + (Zfloor x <= Zfloor y)%Z. +Proof. +intros x y Hxy. +apply Zfloor_lub. +apply Rle_trans with (2 := Hxy). +apply Zfloor_lb. +Qed. + +Definition Zceil (x : R) := (- Zfloor (- x))%Z. + +Theorem Zceil_ub : + forall x : R, + (x <= Z2R (Zceil x))%R. +Proof. +intros x. +unfold Zceil. +rewrite Z2R_opp. +apply Ropp_le_cancel. +rewrite Ropp_involutive. +apply Zfloor_lb. +Qed. + +Theorem Zceil_glb : + 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 Z2R_opp. +now apply Ropp_le_contravar. +Qed. + +Theorem 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 Z2R_opp. +now apply Ropp_le_contravar. +rewrite <- (Zopp_involutive 1). +rewrite <- Zopp_plus_distr. +rewrite Z2R_opp. +now apply Ropp_lt_contravar. +Qed. + +Theorem Zceil_Z2R : + forall n, + Zceil (Z2R n) = n. +Proof. +intros n. +unfold Zceil. +rewrite <- Z2R_opp, Zfloor_Z2R. +apply Zopp_involutive. +Qed. + +Theorem Zceil_le : + forall x y, (x <= y)%R -> + (Zceil x <= Zceil y)%Z. +Proof. +intros x y Hxy. +apply Zceil_glb. +apply Rle_trans with (1 := Hxy). +apply Zceil_ub. +Qed. + +Theorem Zceil_floor_neq : + forall x : R, + (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 Rlt_le. +rewrite Z2R_plus. +apply Zfloor_ub. +Qed. + +Definition Ztrunc x := if Rlt_bool x 0 then Zceil x else Zfloor x. + +Theorem Ztrunc_Z2R : + forall n, + Ztrunc (Z2R n) = n. +Proof. +intros n. +unfold Ztrunc. +case Rlt_bool_spec ; intro H. +apply Zceil_Z2R. +apply Zfloor_Z2R. +Qed. + +Theorem Ztrunc_floor : + forall x, + (0 <= x)%R -> + Ztrunc x = Zfloor x. +Proof. +intros x Hx. +unfold Ztrunc. +case Rlt_bool_spec ; intro H. +elim Rlt_irrefl with x. +now apply Rlt_le_trans with R0. +apply refl_equal. +Qed. + +Theorem Ztrunc_ceil : + forall x, + (x <= 0)%R -> + Ztrunc x = Zceil x. +Proof. +intros x Hx. +unfold Ztrunc. +case Rlt_bool_spec ; intro H. +apply refl_equal. +rewrite (Rle_antisym _ _ Hx H). +fold (Z2R 0). +rewrite Zceil_Z2R. +apply Zfloor_Z2R. +Qed. + +Theorem Ztrunc_le : + forall x y, (x <= y)%R -> + (Ztrunc x <= Ztrunc y)%Z. +Proof. +intros x y Hxy. +unfold Ztrunc at 1. +case Rlt_bool_spec ; intro Hx. +unfold Ztrunc. +case Rlt_bool_spec ; intro Hy. +now apply Zceil_le. +apply Zle_trans with 0%Z. +apply Zceil_glb. +now apply Rlt_le. +now apply Zfloor_lub. +rewrite Ztrunc_floor. +now apply Zfloor_le. +now apply Rle_trans with x. +Qed. + +Theorem Ztrunc_opp : + forall x, + Ztrunc (- x) = Zopp (Ztrunc x). +Proof. +intros x. +unfold Ztrunc at 2. +case Rlt_bool_spec ; intros Hx. +rewrite Ztrunc_floor. +apply sym_eq. +apply Zopp_involutive. +rewrite <- Ropp_0. +apply Ropp_le_contravar. +now apply Rlt_le. +rewrite Ztrunc_ceil. +unfold Zceil. +now rewrite Ropp_involutive. +rewrite <- Ropp_0. +now apply Ropp_le_contravar. +Qed. + +Theorem Ztrunc_abs : + forall x, + Ztrunc (Rabs x) = Zabs (Ztrunc x). +Proof. +intros x. +rewrite Ztrunc_floor. 2: apply Rabs_pos. +unfold Ztrunc. +case Rlt_bool_spec ; intro H. +rewrite Rabs_left with (1 := H). +rewrite Zabs_non_eq. +apply sym_eq. +apply Zopp_involutive. +apply Zceil_glb. +now apply Rlt_le. +rewrite Rabs_pos_eq with (1 := H). +apply sym_eq. +apply Zabs_eq. +now apply Zfloor_lub. +Qed. + +Theorem Ztrunc_lub : + forall n x, + (Z2R n <= Rabs x)%R -> + (n <= Zabs (Ztrunc x))%Z. +Proof. +intros n x H. +rewrite <- Ztrunc_abs. +rewrite Ztrunc_floor. 2: apply Rabs_pos. +now apply Zfloor_lub. +Qed. + +Definition Zaway x := if Rlt_bool x 0 then Zfloor x else Zceil x. + +Theorem Zaway_Z2R : + forall n, + Zaway (Z2R n) = n. +Proof. +intros n. +unfold Zaway. +case Rlt_bool_spec ; intro H. +apply Zfloor_Z2R. +apply Zceil_Z2R. +Qed. + +Theorem Zaway_ceil : + forall x, + (0 <= x)%R -> + Zaway x = Zceil x. +Proof. +intros x Hx. +unfold Zaway. +case Rlt_bool_spec ; intro H. +elim Rlt_irrefl with x. +now apply Rlt_le_trans with R0. +apply refl_equal. +Qed. + +Theorem Zaway_floor : + forall x, + (x <= 0)%R -> + Zaway x = Zfloor x. +Proof. +intros x Hx. +unfold Zaway. +case Rlt_bool_spec ; intro H. +apply refl_equal. +rewrite (Rle_antisym _ _ Hx H). +fold (Z2R 0). +rewrite Zfloor_Z2R. +apply Zceil_Z2R. +Qed. + +Theorem Zaway_le : + forall x y, (x <= y)%R -> + (Zaway x <= Zaway y)%Z. +Proof. +intros x y Hxy. +unfold Zaway at 1. +case Rlt_bool_spec ; intro Hx. +unfold Zaway. +case Rlt_bool_spec ; intro Hy. +now apply Zfloor_le. +apply le_Z2R. +apply Rle_trans with 0%R. +apply Rlt_le. +apply Rle_lt_trans with (2 := Hx). +apply Zfloor_lb. +apply Rle_trans with (1 := Hy). +apply Zceil_ub. +rewrite Zaway_ceil. +now apply Zceil_le. +now apply Rle_trans with x. +Qed. + +Theorem Zaway_opp : + forall x, + Zaway (- x) = Zopp (Zaway x). +Proof. +intros x. +unfold Zaway at 2. +case Rlt_bool_spec ; intro H. +rewrite Zaway_ceil. +unfold Zceil. +now rewrite Ropp_involutive. +apply Rlt_le. +now apply Ropp_0_gt_lt_contravar. +rewrite Zaway_floor. +apply sym_eq. +apply Zopp_involutive. +rewrite <- Ropp_0. +now apply Ropp_le_contravar. +Qed. + +Theorem Zaway_abs : + forall x, + Zaway (Rabs x) = Zabs (Zaway x). +Proof. +intros x. +rewrite Zaway_ceil. 2: apply Rabs_pos. +unfold Zaway. +case Rlt_bool_spec ; intro H. +rewrite Rabs_left with (1 := H). +rewrite Zabs_non_eq. +apply (f_equal (fun v => - Zfloor v)%Z). +apply Ropp_involutive. +apply le_Z2R. +apply Rlt_le. +apply Rle_lt_trans with (2 := H). +apply Zfloor_lb. +rewrite Rabs_pos_eq with (1 := H). +apply sym_eq. +apply Zabs_eq. +apply le_Z2R. +apply Rle_trans with (1 := H). +apply Zceil_ub. +Qed. + +End Floor_Ceil. + +Section Zdiv_Rdiv. + +Theorem Zfloor_div : + forall x y, + y <> Z0 -> + Zfloor (Z2R x / Z2R y) = (x / y)%Z. +Proof. +intros x y Zy. +generalize (Z_div_mod_eq_full x y Zy). +intros Hx. +rewrite Hx at 1. +assert (Zy': Z2R y <> R0). +contradict Zy. +now apply eq_Z2R. +unfold Rdiv. +rewrite Z2R_plus, Rmult_plus_distr_r, Z2R_mult. +replace (Z2R y * Z2R (x / y) * / Z2R y)%R with (Z2R (x / y)) by now field. +apply Zfloor_imp. +rewrite Z2R_plus. +assert (0 <= Z2R (x mod y) * / Z2R y < 1)%R. +(* *) +assert (forall x' y', (0 < y')%Z -> 0 <= Z2R (x' mod y') * / Z2R y' < 1)%R. +(* . *) +clear. +intros x y Hy. +split. +apply Rmult_le_pos. +apply (Z2R_le 0). +refine (proj1 (Z_mod_lt _ _ _)). +now apply Zlt_gt. +apply Rlt_le. +apply Rinv_0_lt_compat. +now apply (Z2R_lt 0). +apply Rmult_lt_reg_r with (Z2R y). +now apply (Z2R_lt 0). +rewrite Rmult_1_l, Rmult_assoc, Rinv_l, Rmult_1_r. +apply Z2R_lt. +eapply Z_mod_lt. +now apply Zlt_gt. +apply Rgt_not_eq. +now apply (Z2R_lt 0). +(* . *) +destruct (Z_lt_le_dec y 0) as [Hy|Hy]. +rewrite <- Rmult_opp_opp. +rewrite Ropp_inv_permute with (1 := Zy'). +rewrite <- 2!Z2R_opp. +rewrite <- Zmod_opp_opp. +apply H. +clear -Hy. omega. +apply H. +clear -Zy Hy. omega. +(* *) +split. +pattern (Z2R (x / y)) at 1 ; rewrite <- Rplus_0_r. +apply Rplus_le_compat_l. +apply H. +apply Rplus_lt_compat_l. +apply H. +Qed. + +End Zdiv_Rdiv. + +Section pow. + +Variable r : radix. + +Theorem radix_pos : (0 < Z2R r)%R. +Proof. +destruct r as (v, Hr). simpl. +apply (Z2R_lt 0). +apply Zlt_le_trans with 2%Z. +easy. +now apply Zle_bool_imp_le. +Qed. + +(** Well-used function called bpow for computing the power function #β#^e *) +Definition bpow e := + match e with + | Zpos p => Z2R (Zpower_pos r p) + | Zneg p => Rinv (Z2R (Zpower_pos r p)) + | Z0 => R1 + end. + +Theorem Z2R_Zpower_pos : + 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 Z2R_mult. +apply Rmult_eq_compat_l. +exact IHn0. +Qed. + +Theorem bpow_powerRZ : + forall e, + bpow e = powerRZ (Z2R r) e. +Proof. +destruct e ; unfold bpow. +reflexivity. +now rewrite Z2R_Zpower_pos. +now rewrite Z2R_Zpower_pos. +Qed. + +Theorem bpow_ge_0 : + forall e : Z, (0 <= bpow e)%R. +Proof. +intros. +rewrite bpow_powerRZ. +apply powerRZ_le. +apply radix_pos. +Qed. + +Theorem bpow_gt_0 : + forall e : Z, (0 < bpow e)%R. +Proof. +intros. +rewrite bpow_powerRZ. +apply powerRZ_lt. +apply radix_pos. +Qed. + +Theorem bpow_plus : + forall e1 e2 : Z, (bpow (e1 + e2) = bpow e1 * bpow e2)%R. +Proof. +intros. +repeat rewrite bpow_powerRZ. +apply powerRZ_add. +apply Rgt_not_eq. +apply radix_pos. +Qed. + +Theorem bpow_1 : + bpow 1 = Z2R r. +Proof. +unfold bpow, Zpower_pos. simpl. +now rewrite Zmult_1_r. +Qed. + +Theorem bpow_plus1 : + forall e : Z, (bpow (e + 1) = Z2R r * bpow e)%R. +Proof. +intros. +rewrite <- bpow_1. +rewrite <- bpow_plus. +now rewrite Zplus_comm. +Qed. + +Theorem bpow_opp : + forall e : Z, (bpow (-e) = /bpow 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 (bpow_gt_0 (Zpos p)). +simpl; auto with real. +Qed. + +Theorem Z2R_Zpower_nat : + forall e : nat, + Z2R (Zpower_nat r e) = bpow (Z_of_nat e). +Proof. +intros [|e]. +split. +rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ. +rewrite <- Zpower_pos_nat. +now rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P. +Qed. + +Theorem Z2R_Zpower : + forall e : Z, + (0 <= e)%Z -> + Z2R (Zpower r e) = bpow e. +Proof. +intros [|e|e] H. +split. +split. +now elim H. +Qed. + +Theorem bpow_lt : + forall e1 e2 : Z, + (e1 < e2)%Z -> (bpow e1 < bpow e2)%R. +Proof. +intros e1 e2 H. +replace e2 with (e1 + (e2 - e1))%Z by ring. +rewrite <- (Rmult_1_r (bpow e1)). +rewrite bpow_plus. +apply Rmult_lt_compat_l. +apply bpow_gt_0. +assert (0 < e2 - e1)%Z by omega. +destruct (e2 - e1)%Z ; try discriminate H0. +clear. +rewrite <- Z2R_Zpower by easy. +apply (Z2R_lt 1). +now apply Zpower_gt_1. +Qed. + +Theorem lt_bpow : + forall e1 e2 : Z, + (bpow e1 < bpow e2)%R -> (e1 < e2)%Z. +Proof. +intros e1 e2 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 bpow_lt. +rewrite H0. +apply Rle_refl. +Qed. + +Theorem bpow_le : + forall e1 e2 : Z, + (e1 <= e2)%Z -> (bpow e1 <= bpow e2)%R. +Proof. +intros e1 e2 H. +apply Rnot_lt_le. +intros H'. +apply Zle_not_gt with (1 := H). +apply Zlt_gt. +now apply lt_bpow. +Qed. + +Theorem le_bpow : + forall e1 e2 : Z, + (bpow e1 <= bpow e2)%R -> (e1 <= e2)%Z. +Proof. +intros e1 e2 H. +apply Znot_gt_le. +intros H'. +apply Rle_not_lt with (1 := H). +apply bpow_lt. +now apply Zgt_lt. +Qed. + +Theorem bpow_inj : + forall e1 e2 : Z, + bpow e1 = bpow e2 -> e1 = e2. +Proof. +intros. +apply Zle_antisym. +apply le_bpow. +now apply Req_le. +apply le_bpow. +now apply Req_le. +Qed. + +Theorem bpow_exp : + forall e : Z, + bpow e = exp (Z2R e * ln (Z2R r)). +Proof. +(* positive case *) +assert (forall e, bpow (Zpos e) = exp (Z2R (Zpos e) * ln (Z2R r))). +intros e. +unfold bpow. +rewrite Zpower_pos_nat. +unfold Z2R at 2. +rewrite P2R_INR. +induction (nat_of_P e). +rewrite Rmult_0_l. +now rewrite exp_0. +rewrite Zpower_nat_S. +rewrite S_INR. +rewrite Rmult_plus_distr_r. +rewrite exp_plus. +rewrite Rmult_1_l. +rewrite exp_ln. +rewrite <- IHn. +rewrite <- Z2R_mult. +now rewrite Zmult_comm. +apply radix_pos. +(* general case *) +intros [|e|e]. +rewrite Rmult_0_l. +now rewrite exp_0. +apply H. +unfold bpow. +change (Z2R (Zpower_pos r e)) with (bpow (Zpos e)). +rewrite H. +rewrite <- exp_Ropp. +rewrite <- Ropp_mult_distr_l_reverse. +now rewrite <- Z2R_opp. +Qed. + +(** Another well-used function for having the logarithm of a real number x to the base #β# *) +Record ln_beta_prop x := { + ln_beta_val :> Z ; + _ : (x <> 0)%R -> (bpow (ln_beta_val - 1)%Z <= Rabs x < bpow ln_beta_val)%R +}. + +Definition ln_beta : + forall x : R, ln_beta_prop x. +Proof. +intros x. +set (fact := ln (Z2R r)). +(* . *) +assert (0 < fact)%R. +apply exp_lt_inv. +rewrite exp_0. +unfold fact. +rewrite exp_ln. +apply (Z2R_lt 1). +apply radix_gt_1. +apply radix_pos. +(* . *) +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. +rewrite 2!bpow_exp. +fold fact. +pattern x at 2 3 ; replace x with (exp (ln x * / fact * fact)). +split. +rewrite Z2R_minus. +apply exp_le. +apply Rmult_le_compat_r. +now apply Rlt_le. +unfold Rminus. +rewrite Z2R_plus. +rewrite Rplus_assoc. +rewrite Rplus_opp_r, Rplus_0_r. +apply Zfloor_lb. +apply exp_increasing. +apply Rmult_lt_compat_r. +exact H. +rewrite Z2R_plus. +apply Zfloor_ub. +rewrite Rmult_assoc. +rewrite Rinv_l. +rewrite Rmult_1_r. +now apply exp_ln. +now apply Rgt_not_eq. +Qed. + +Theorem bpow_lt_bpow : + forall e1 e2, + (bpow (e1 - 1) < bpow e2)%R -> + (e1 <= e2)%Z. +Proof. +intros e1 e2 He. +rewrite (Zsucc_pred e1). +apply Zlt_le_succ. +now apply lt_bpow. +Qed. + +Theorem bpow_unique : + forall x e1 e2, + (bpow (e1 - 1) <= x < bpow e1)%R -> + (bpow (e2 - 1) <= x < bpow e2)%R -> + e1 = e2. +Proof. +intros x e1 e2 (H1a,H1b) (H2a,H2b). +apply Zle_antisym ; + apply bpow_lt_bpow ; + apply Rle_lt_trans with x ; + assumption. +Qed. + +Theorem ln_beta_unique : + forall (x : R) (e : Z), + (bpow (e - 1) <= Rabs x < bpow e)%R -> + ln_beta x = e :> Z. +Proof. +intros x e1 He. +destruct (Req_dec x 0) as [Hx|Hx]. +elim Rle_not_lt with (1 := proj1 He). +rewrite Hx, Rabs_R0. +apply bpow_gt_0. +destruct (ln_beta x) as (e2, Hx2). +simpl. +apply bpow_unique with (2 := He). +now apply Hx2. +Qed. + +Theorem ln_beta_opp : + forall x, + ln_beta (-x) = ln_beta x :> Z. +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. +Qed. + +Theorem ln_beta_abs : + forall x, + ln_beta (Rabs x) = ln_beta x :> Z. +Proof. +intros x. +unfold Rabs. +case Rcase_abs ; intros _. +apply ln_beta_opp. +apply refl_equal. +Qed. + +Theorem ln_beta_unique_pos : + forall (x : R) (e : Z), + (bpow (e - 1) <= x < bpow e)%R -> + ln_beta x = e :> Z. +Proof. +intros x e1 He1. +rewrite <- ln_beta_abs. +apply ln_beta_unique. +rewrite 2!Rabs_pos_eq. +exact He1. +apply Rle_trans with (2 := proj1 He1). +apply bpow_ge_0. +apply Rabs_pos. +Qed. + +Theorem ln_beta_le_abs : + forall x y, + (x <> 0)%R -> (Rabs x <= Rabs y)%R -> + (ln_beta x <= 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 bpow_lt_bpow. +specialize (Hx H0x). +apply Rle_lt_trans with (1 := proj1 Hx). +apply Rle_lt_trans with (1 := Hxy). +apply Hy. +intros Hy'. +apply Rlt_not_le with (1 := Rabs_pos_lt _ H0x). +apply Rle_trans with (1 := Hxy). +rewrite Hy', Rabs_R0. +apply Rle_refl. +Qed. + +Theorem ln_beta_le : + forall x y, + (0 < x)%R -> (x <= y)%R -> + (ln_beta x <= ln_beta y)%Z. +Proof. +intros x y H0x Hxy. +apply ln_beta_le_abs. +now apply Rgt_not_eq. +rewrite 2!Rabs_pos_eq. +exact Hxy. +apply Rle_trans with (2 := Hxy). +now apply Rlt_le. +now apply Rlt_le. +Qed. + +Theorem ln_beta_bpow : + forall e, (ln_beta (bpow e) = e + 1 :> Z)%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. + +Theorem ln_beta_mult_bpow : + forall x e, x <> R0 -> + (ln_beta (x * bpow e) = ln_beta x + e :>Z)%Z. +Proof. +intros x e Zx. +destruct (ln_beta x) as (ex, Ex) ; simpl. +specialize (Ex Zx). +apply ln_beta_unique. +rewrite Rabs_mult. +rewrite (Rabs_pos_eq (bpow e)) by apply bpow_ge_0. +split. +replace (ex + e - 1)%Z with (ex - 1 + e)%Z by ring. +rewrite bpow_plus. +apply Rmult_le_compat_r. +apply bpow_ge_0. +apply Ex. +rewrite bpow_plus. +apply Rmult_lt_compat_r. +apply bpow_gt_0. +apply Ex. +Qed. + +Theorem ln_beta_le_bpow : + forall x e, + x <> R0 -> + (Rabs x < bpow e)%R -> + (ln_beta x <= e)%Z. +Proof. +intros x e Zx Hx. +destruct (ln_beta x) as (ex, Ex) ; simpl. +specialize (Ex Zx). +apply bpow_lt_bpow. +now apply Rle_lt_trans with (Rabs x). +Qed. + +Theorem ln_beta_gt_bpow : + forall x e, + (bpow e <= Rabs x)%R -> + (e < ln_beta x)%Z. +Proof. +intros x e Hx. +destruct (ln_beta x) as (ex, Ex) ; simpl. +apply lt_bpow. +apply Rle_lt_trans with (1 := Hx). +apply Ex. +intros Zx. +apply Rle_not_lt with (1 := Hx). +rewrite Zx, Rabs_R0. +apply bpow_gt_0. +Qed. + +Theorem bpow_ln_beta_gt : + forall x, + (Rabs x < bpow (ln_beta x))%R. +Proof. +intros x. +destruct (Req_dec x 0) as [Zx|Zx]. +rewrite Zx, Rabs_R0. +apply bpow_gt_0. +destruct (ln_beta x) as (ex, Ex) ; simpl. +now apply Ex. +Qed. + +Theorem ln_beta_le_Zpower : + forall m e, + m <> Z0 -> + (Zabs m < Zpower r e)%Z-> + (ln_beta (Z2R m) <= e)%Z. +Proof. +intros m e Zm Hm. +apply ln_beta_le_bpow. +exact (Z2R_neq m 0 Zm). +destruct (Zle_or_lt 0 e). +rewrite <- Z2R_abs, <- Z2R_Zpower with (1 := H). +now apply Z2R_lt. +elim Zm. +cut (Zabs m < 0)%Z. +now case m. +clear -Hm H. +now destruct e. +Qed. + +Theorem ln_beta_gt_Zpower : + forall m e, + m <> Z0 -> + (Zpower r e <= Zabs m)%Z -> + (e < ln_beta (Z2R m))%Z. +Proof. +intros m e Zm Hm. +apply ln_beta_gt_bpow. +rewrite <- Z2R_abs. +destruct (Zle_or_lt 0 e). +rewrite <- Z2R_Zpower with (1 := H). +now apply Z2R_le. +apply Rle_trans with (bpow 0). +apply bpow_le. +now apply Zlt_le_weak. +apply (Z2R_le 1). +clear -Zm. +zify ; omega. +Qed. + +End pow. + +Section Bool. + +Theorem eqb_sym : + forall x y, Bool.eqb x y = Bool.eqb y x. +Proof. +now intros [|] [|]. +Qed. + +Theorem eqb_false : + forall x y, x = negb y -> Bool.eqb x y = false. +Proof. +now intros [|] [|]. +Qed. + +Theorem eqb_true : + forall x y, x = y -> Bool.eqb x y = true. +Proof. +now intros [|] [|]. +Qed. + +End Bool. + +Section cond_Ropp. + +Definition cond_Ropp (b : bool) m := if b then Ropp m else m. + +Theorem Z2R_cond_Zopp : + forall b m, + Z2R (cond_Zopp b m) = cond_Ropp b (Z2R m). +Proof. +intros [|] m. +apply Z2R_opp. +apply refl_equal. +Qed. + +Theorem abs_cond_Ropp : + forall b m, + Rabs (cond_Ropp b m) = Rabs m. +Proof. +intros [|] m. +apply Rabs_Ropp. +apply refl_equal. +Qed. + +Theorem cond_Ropp_Rlt_bool : + forall m, + cond_Ropp (Rlt_bool m 0) m = Rabs m. +Proof. +intros m. +apply sym_eq. +case Rlt_bool_spec ; intros Hm. +now apply Rabs_left. +now apply Rabs_pos_eq. +Qed. + +Theorem cond_Ropp_involutive : + forall b x, + cond_Ropp b (cond_Ropp b x) = x. +Proof. +intros [|] x. +apply Ropp_involutive. +apply refl_equal. +Qed. + +Theorem cond_Ropp_even_function : + forall {A : Type} (f : R -> A), + (forall x, f (Ropp x) = f x) -> + forall b x, f (cond_Ropp b x) = f x. +Proof. +now intros A f Hf [|] x ; simpl. +Qed. + +Theorem cond_Ropp_odd_function : + forall (f : R -> R), + (forall x, f (Ropp x) = Ropp (f x)) -> + forall b x, f (cond_Ropp b x) = cond_Ropp b (f x). +Proof. +now intros f Hf [|] x ; simpl. +Qed. + +Theorem cond_Ropp_inj : + forall b x y, + cond_Ropp b x = cond_Ropp b y -> x = y. +Proof. +intros b x y H. +rewrite <- (cond_Ropp_involutive b x), H. +apply cond_Ropp_involutive. +Qed. + +Theorem cond_Ropp_mult_l : + forall b x y, + cond_Ropp b (x * y) = (cond_Ropp b x * y)%R. +Proof. +intros [|] x y. +apply sym_eq. +apply Ropp_mult_distr_l_reverse. +apply refl_equal. +Qed. + +Theorem cond_Ropp_mult_r : + forall b x y, + cond_Ropp b (x * y) = (x * cond_Ropp b y)%R. +Proof. +intros [|] x y. +apply sym_eq. +apply Ropp_mult_distr_r_reverse. +apply refl_equal. +Qed. + +Theorem cond_Ropp_plus : + forall b x y, + cond_Ropp b (x + y) = (cond_Ropp b x + cond_Ropp b y)%R. +Proof. +intros [|] x y. +apply Ropp_plus_distr. +apply refl_equal. +Qed. + +End cond_Ropp. |