Module Fcore_Raux
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.
Theorem Rabs_eq_Rabs :
forall x y :
R,
Rabs x =
Rabs y ->
x =
y \/
x =
Ropp y.
Proof.
Theorem Rabs_minus_le:
forall x y :
R,
(0 <=
y)%
R -> (
y <= 2*
x)%
R ->
(
Rabs (
x-
y) <=
x)%
R.
Proof.
Theorem Rplus_eq_reg_r :
forall r r1 r2 :
R,
(
r1 +
r =
r2 +
r)%
R -> (
r1 =
r2)%
R.
Proof.
Theorem Rplus_lt_reg_l :
forall r r1 r2 :
R,
(
r +
r1 <
r +
r2)%
R -> (
r1 <
r2)%
R.
Proof.
Theorem Rplus_lt_reg_r :
forall r r1 r2 :
R,
(
r1 +
r <
r2 +
r)%
R -> (
r1 <
r2)%
R.
Proof.
Theorem Rplus_le_reg_r :
forall r r1 r2 :
R,
(
r1 +
r <=
r2 +
r)%
R -> (
r1 <=
r2)%
R.
Proof.
Theorem Rmult_lt_reg_r :
forall r r1 r2 :
R, (0 <
r)%
R ->
(
r1 *
r <
r2 *
r)%
R -> (
r1 <
r2)%
R.
Proof.
Theorem Rmult_le_reg_r :
forall r r1 r2 :
R, (0 <
r)%
R ->
(
r1 *
r <=
r2 *
r)%
R -> (
r1 <=
r2)%
R.
Proof.
Theorem Rmult_lt_compat :
forall r1 r2 r3 r4,
(0 <=
r1)%
R -> (0 <=
r3)%
R -> (
r1 <
r2)%
R -> (
r3 <
r4)%
R ->
(
r1 *
r3 <
r2 *
r4)%
R.
Proof.
Theorem Rmult_eq_reg_r :
forall r r1 r2 :
R, (
r1 *
r)%
R = (
r2 *
r)%
R ->
r <> 0%
R ->
r1 =
r2.
Proof.
Theorem Rmult_minus_distr_r :
forall r r1 r2 :
R,
((
r1 -
r2) *
r =
r1 *
r -
r2 *
r)%
R.
Proof.
Lemma Rmult_neq_reg_r:
forall r1 r2 r3:
R, (
r2 *
r1 <>
r3 *
r1)%
R ->
r2 <>
r3.
intros r1 r2 r3 H1 H2.
apply H1;
rewrite H2;
ring.
Qed.
Lemma Rmult_neq_compat_r: forall r1 r2 r3:R, (r1 <> 0)%R -> (r2 <> r3)%R
-> (r2 *r1 <> r3*r1)%R.
intros r1 r2 r3 H H1 H2.
now apply H1, Rmult_eq_reg_r with r1.
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.
Theorem Rmult_min_distr_l :
forall r r1 r2 : R,
(0 <= r)%R ->
(r * Rmin r1 r2)%R = Rmin (r * r1) (r * r2).
Proof.
Lemma Rmin_opp: forall x y, (Rmin (-x) (-y) = - Rmax x y)%R.
Proof.
Lemma Rmax_opp: forall x y, (Rmax (-x) (-y) = - Rmin x y)%R.
Proof.
Theorem exp_le :
forall x y : R,
(x <= y)%R -> (exp x <= exp y)%R.
Proof.
Theorem Rinv_lt :
forall x y,
(0 < x)%R -> (x < y)%R -> (/y < /x)%R.
Proof.
Theorem Rinv_le :
forall x y,
(0 < x)%R -> (x <= y)%R -> (/y <= /x)%R.
Proof.
Theorem sqrt_ge_0 :
forall x : R,
(0 <= sqrt x)%R.
Proof.
Lemma sqrt_neg : forall x, (x <= 0)%R -> (sqrt x = 0)%R.
Proof.
Theorem Rabs_le :
forall x y,
(-y <= x <= y)%R -> (Rabs x <= y)%R.
Proof.
Theorem Rabs_le_inv :
forall x y,
(Rabs x <= y)%R -> (-y <= x <= y)%R.
Proof.
Theorem Rabs_ge :
forall x y,
(y <= -x \/ x <= y)%R -> (x <= Rabs y)%R.
Proof.
Theorem Rabs_ge_inv :
forall x y,
(x <= Rabs y)%R -> (y <= -x \/ x <= y)%R.
Proof.
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.
Theorem Rabs_gt_inv :
forall x y,
(x < Rabs y)%R -> (y < -x \/ x < y)%R.
Proof.
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 => 0%R
end.
Theorem P2R_INR :
forall n, P2R n = INR (nat_of_P n).
Proof.
Theorem Z2R_IZR :
forall n, Z2R n = IZR n.
Proof.
Theorem Z2R_opp :
forall n, Z2R (-n) = (- Z2R n)%R.
Proof.
Theorem Z2R_plus :
forall m n, (Z2R (m + n) = Z2R m + Z2R n)%R.
Proof.
Theorem minus_IZR :
forall n m : Z,
IZR (n - m) = (IZR n - IZR m)%R.
Proof.
Theorem Z2R_minus :
forall m n, (Z2R (m - n) = Z2R m - Z2R n)%R.
Proof.
Theorem Z2R_mult :
forall m n, (Z2R (m * n) = Z2R m * Z2R n)%R.
Proof.
Theorem le_Z2R :
forall m n, (Z2R m <= Z2R n)%R -> (m <= n)%Z.
Proof.
Theorem Z2R_le :
forall m n, (m <= n)%Z -> (Z2R m <= Z2R n)%R.
Proof.
Theorem lt_Z2R :
forall m n, (Z2R m < Z2R n)%R -> (m < n)%Z.
Proof.
Theorem Z2R_lt :
forall m n, (m < n)%Z -> (Z2R m < Z2R n)%R.
Proof.
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.
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.
Theorem Z2R_abs :
forall z, Z2R (Zabs z) = Rabs (Z2R z).
Proof.
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.
Global Opaque Rcompare.
Theorem Rcompare_Lt :
forall x y,
(x < y)%R -> Rcompare x y = Lt.
Proof.
Theorem Rcompare_Lt_inv :
forall x y,
Rcompare x y = Lt -> (x < y)%R.
Proof.
Theorem Rcompare_not_Lt :
forall x y,
(y <= x)%R -> Rcompare x y <> Lt.
Proof.
Theorem Rcompare_not_Lt_inv :
forall x y,
Rcompare x y <> Lt -> (y <= x)%R.
Proof.
Theorem Rcompare_Eq :
forall x y,
x = y -> Rcompare x y = Eq.
Proof.
Theorem Rcompare_Eq_inv :
forall x y,
Rcompare x y = Eq -> x = y.
Proof.
Theorem Rcompare_Gt :
forall x y,
(y < x)%R -> Rcompare x y = Gt.
Proof.
Theorem Rcompare_Gt_inv :
forall x y,
Rcompare x y = Gt -> (y < x)%R.
Proof.
Theorem Rcompare_not_Gt :
forall x y,
(x <= y)%R -> Rcompare x y <> Gt.
Proof.
Theorem Rcompare_not_Gt_inv :
forall x y,
Rcompare x y <> Gt -> (x <= y)%R.
Proof.
Theorem Rcompare_Z2R :
forall x y, Rcompare (Z2R x) (Z2R y) = Zcompare x y.
Proof.
Theorem Rcompare_sym :
forall x y,
Rcompare x y = CompOpp (Rcompare y x).
Proof.
Theorem Rcompare_plus_r :
forall z x y,
Rcompare (x + z) (y + z) = Rcompare x y.
Proof.
Theorem Rcompare_plus_l :
forall z x y,
Rcompare (z + x) (z + y) = Rcompare x y.
Proof.
Theorem Rcompare_mult_r :
forall z x y,
(0 < z)%R ->
Rcompare (x * z) (y * z) = Rcompare x y.
Proof.
Theorem Rcompare_mult_l :
forall z x y,
(0 < z)%R ->
Rcompare (z * x) (z * y) = Rcompare x y.
Proof.
Theorem Rcompare_middle :
forall x d u,
Rcompare (x - d) (u - x) = Rcompare x ((d + u) / 2).
Proof.
Theorem Rcompare_half_l :
forall x y, Rcompare (x / 2) y = Rcompare x (2 * y).
Proof.
Theorem Rcompare_half_r :
forall x y, Rcompare x (y / 2) = Rcompare (2 * x) y.
Proof.
Theorem Rcompare_sqr :
forall x y,
(0 <= x)%R -> (0 <= y)%R ->
Rcompare (x * x) (y * y) = Rcompare x y.
Proof.
Theorem Rmin_compare :
forall x y,
Rmin x y = match Rcompare x y with Lt => x | Eq => x | Gt => y end.
Proof.
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.
Theorem Rle_bool_true :
forall x y,
(x <= y)%R -> Rle_bool x y = true.
Proof.
Theorem Rle_bool_false :
forall x y,
(y < x)%R -> Rle_bool x y = false.
Proof.
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.
Theorem negb_Rlt_bool :
forall x y,
negb (Rle_bool x y) = Rlt_bool y x.
Proof.
Theorem negb_Rle_bool :
forall x y,
negb (Rlt_bool x y) = Rle_bool y x.
Proof.
Theorem Rlt_bool_true :
forall x y,
(x < y)%R -> Rlt_bool x y = true.
Proof.
Theorem Rlt_bool_false :
forall x y,
(y <= x)%R -> Rlt_bool x y = false.
Proof.
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.
Theorem Req_bool_true :
forall x y,
(x = y)%R -> Req_bool x y = true.
Proof.
Theorem Req_bool_false :
forall x y,
(x <> y)%R -> Req_bool x y = false.
Proof.
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.
Theorem Zfloor_ub :
forall x : R,
(x < Z2R (Zfloor x) + 1)%R.
Proof.
Theorem Zfloor_lub :
forall n x,
(Z2R n <= x)%R ->
(n <= Zfloor x)%Z.
Proof.
Theorem Zfloor_imp :
forall n x,
(Z2R n <= x < Z2R (n + 1))%R ->
Zfloor x = n.
Proof.
Theorem Zfloor_Z2R :
forall n,
Zfloor (Z2R n) = n.
Proof.
Theorem Zfloor_le :
forall x y, (x <= y)%R ->
(Zfloor x <= Zfloor y)%Z.
Proof.
Definition Zceil (x : R) := (- Zfloor (- x))%Z.
Theorem Zceil_ub :
forall x : R,
(x <= Z2R (Zceil x))%R.
Proof.
Theorem Zceil_glb :
forall n x,
(x <= Z2R n)%R ->
(Zceil x <= n)%Z.
Proof.
Theorem Zceil_imp :
forall n x,
(Z2R (n - 1) < x <= Z2R n)%R ->
Zceil x = n.
Proof.
Theorem Zceil_Z2R :
forall n,
Zceil (Z2R n) = n.
Proof.
Theorem Zceil_le :
forall x y, (x <= y)%R ->
(Zceil x <= Zceil y)%Z.
Proof.
Theorem Zceil_floor_neq :
forall x : R,
(Z2R (Zfloor x) <> x)%R ->
(Zceil x = Zfloor x + 1)%Z.
Proof.
Definition Ztrunc x := if Rlt_bool x 0 then Zceil x else Zfloor x.
Theorem Ztrunc_Z2R :
forall n,
Ztrunc (Z2R n) = n.
Proof.
Theorem Ztrunc_floor :
forall x,
(0 <= x)%R ->
Ztrunc x = Zfloor x.
Proof.
Theorem Ztrunc_ceil :
forall x,
(x <= 0)%R ->
Ztrunc x = Zceil x.
Proof.
Theorem Ztrunc_le :
forall x y, (x <= y)%R ->
(Ztrunc x <= Ztrunc y)%Z.
Proof.
Theorem Ztrunc_opp :
forall x,
Ztrunc (- x) = Zopp (Ztrunc x).
Proof.
Theorem Ztrunc_abs :
forall x,
Ztrunc (Rabs x) = Zabs (Ztrunc x).
Proof.
Theorem Ztrunc_lub :
forall n x,
(Z2R n <= Rabs x)%R ->
(n <= Zabs (Ztrunc x))%Z.
Proof.
Definition Zaway x := if Rlt_bool x 0 then Zfloor x else Zceil x.
Theorem Zaway_Z2R :
forall n,
Zaway (Z2R n) = n.
Proof.
Theorem Zaway_ceil :
forall x,
(0 <= x)%R ->
Zaway x = Zceil x.
Proof.
Theorem Zaway_floor :
forall x,
(x <= 0)%R ->
Zaway x = Zfloor x.
Proof.
Theorem Zaway_le :
forall x y, (x <= y)%R ->
(Zaway x <= Zaway y)%Z.
Proof.
Theorem Zaway_opp :
forall x,
Zaway (- x) = Zopp (Zaway x).
Proof.
Theorem Zaway_abs :
forall x,
Zaway (Rabs x) = Zabs (Zaway x).
Proof.
End Floor_Ceil.
Section Zdiv_Rdiv.
Theorem Zfloor_div :
forall x y,
y <> Z0 ->
Zfloor (Z2R x / Z2R y) = (x / y)%Z.
Proof.
End Zdiv_Rdiv.
Section pow.
Variable r : radix.
Theorem radix_pos : (0 < Z2R r)%R.
Proof.
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 => 1%R
end.
Theorem Z2R_Zpower_pos :
forall n m,
Z2R (Zpower_pos n m) = powerRZ (Z2R n) (Zpos m).
Proof.
Theorem bpow_powerRZ :
forall e,
bpow e = powerRZ (Z2R r) e.
Proof.
Theorem bpow_ge_0 :
forall e : Z, (0 <= bpow e)%R.
Proof.
Theorem bpow_gt_0 :
forall e : Z, (0 < bpow e)%R.
Proof.
Theorem bpow_plus :
forall e1 e2 : Z, (bpow (e1 + e2) = bpow e1 * bpow e2)%R.
Proof.
Theorem bpow_1 :
bpow 1 = Z2R r.
Proof.
Theorem bpow_plus1 :
forall e : Z, (bpow (e + 1) = Z2R r * bpow e)%R.
Proof.
Theorem bpow_opp :
forall e : Z, (bpow (-e) = /bpow e)%R.
Proof.
Theorem Z2R_Zpower_nat :
forall e : nat,
Z2R (Zpower_nat r e) = bpow (Z_of_nat e).
Proof.
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.
Theorem lt_bpow :
forall e1 e2 : Z,
(bpow e1 < bpow e2)%R -> (e1 < e2)%Z.
Proof.
Theorem bpow_le :
forall e1 e2 : Z,
(e1 <= e2)%Z -> (bpow e1 <= bpow e2)%R.
Proof.
Theorem le_bpow :
forall e1 e2 : Z,
(bpow e1 <= bpow e2)%R -> (e1 <= e2)%Z.
Proof.
Theorem bpow_inj :
forall e1 e2 : Z,
bpow e1 = bpow e2 -> e1 = e2.
Proof.
Theorem bpow_exp :
forall e : Z,
bpow e = exp (Z2R e * ln (Z2R r)).
Proof.
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.
Theorem bpow_lt_bpow :
forall e1 e2,
(bpow (e1 - 1) < bpow e2)%R ->
(e1 <= e2)%Z.
Proof.
Theorem bpow_unique :
forall x e1 e2,
(bpow (e1 - 1) <= x < bpow e1)%R ->
(bpow (e2 - 1) <= x < bpow e2)%R ->
e1 = e2.
Proof.
Theorem ln_beta_unique :
forall (x : R) (e : Z),
(bpow (e - 1) <= Rabs x < bpow e)%R ->
ln_beta x = e :> Z.
Proof.
Theorem ln_beta_opp :
forall x,
ln_beta (-x) = ln_beta x :> Z.
Proof.
Theorem ln_beta_abs :
forall x,
ln_beta (Rabs x) = ln_beta x :> Z.
Proof.
Theorem ln_beta_unique_pos :
forall (x : R) (e : Z),
(bpow (e - 1) <= x < bpow e)%R ->
ln_beta x = e :> Z.
Proof.
Theorem ln_beta_le_abs :
forall x y,
(x <> 0)%R -> (Rabs x <= Rabs y)%R ->
(ln_beta x <= ln_beta y)%Z.
Proof.
Theorem ln_beta_le :
forall x y,
(0 < x)%R -> (x <= y)%R ->
(ln_beta x <= ln_beta y)%Z.
Proof.
Lemma ln_beta_lt_pos :
forall x y,
(0 < x)%R -> (0 < y)%R ->
(ln_beta x < ln_beta y)%Z -> (x < y)%R.
Proof.
Theorem ln_beta_bpow :
forall e, (ln_beta (bpow e) = e + 1 :> Z)%Z.
Proof.
Theorem ln_beta_mult_bpow :
forall x e, x <> 0%R ->
(ln_beta (x * bpow e) = ln_beta x + e :>Z)%Z.
Proof.
Theorem ln_beta_le_bpow :
forall x e,
x <> 0%R ->
(Rabs x < bpow e)%R ->
(ln_beta x <= e)%Z.
Proof.
Theorem ln_beta_gt_bpow :
forall x e,
(bpow e <= Rabs x)%R ->
(e < ln_beta x)%Z.
Proof.
Theorem ln_beta_ge_bpow :
forall x e,
(bpow (e - 1) <= Rabs x)%R ->
(e <= ln_beta x)%Z.
Proof.
Theorem bpow_ln_beta_gt :
forall x,
(Rabs x < bpow (ln_beta x))%R.
Proof.
Theorem bpow_ln_beta_le :
forall x, (x <> 0)%R ->
(bpow (ln_beta x-1) <= Rabs x)%R.
Proof.
intros x Hx.
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.
Theorem ln_beta_gt_Zpower :
forall m e,
m <> Z0 ->
(Zpower r e <= Zabs m)%Z ->
(e < ln_beta (Z2R m))%Z.
Proof.
Lemma ln_beta_mult :
forall x y,
(x <> 0)%R -> (y <> 0)%R ->
(ln_beta x + ln_beta y - 1 <= ln_beta (x * y) <= ln_beta x + ln_beta y)%Z.
Proof.
Lemma ln_beta_plus :
forall x y,
(0 < y)%R -> (y <= x)%R ->
(ln_beta x <= ln_beta (x + y) <= ln_beta x + 1)%Z.
Proof.
Lemma ln_beta_minus :
forall x y,
(0 < y)%R -> (y < x)%R ->
(ln_beta (x - y) <= ln_beta x)%Z.
Proof.
Lemma ln_beta_minus_lb :
forall x y,
(0 < x)%R -> (0 < y)%R ->
(ln_beta y <= ln_beta x - 2)%Z ->
(ln_beta x - 1 <= ln_beta (x - y))%Z.
Proof.
Lemma ln_beta_div :
forall x y : R,
(0 < x)%R -> (0 < y)%R ->
(ln_beta x - ln_beta y <= ln_beta (x / y) <= ln_beta x - ln_beta y + 1)%Z.
Proof.
Lemma ln_beta_sqrt :
forall x,
(0 < x)%R ->
(2 * ln_beta (sqrt x) - 1 <= ln_beta x <= 2 * ln_beta (sqrt x))%Z.
Proof.
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.
Theorem abs_cond_Ropp :
forall b m,
Rabs (cond_Ropp b m) = Rabs m.
Proof.
Theorem cond_Ropp_Rlt_bool :
forall m,
cond_Ropp (Rlt_bool m 0) m = Rabs m.
Proof.
Theorem cond_Ropp_involutive :
forall b x,
cond_Ropp b (cond_Ropp b x) = x.
Proof.
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.
Theorem cond_Ropp_mult_l :
forall b x y,
cond_Ropp b (x * y) = (cond_Ropp b x * y)%R.
Proof.
Theorem cond_Ropp_mult_r :
forall b x y,
cond_Ropp b (x * y) = (x * cond_Ropp b y)%R.
Proof.
Theorem cond_Ropp_plus :
forall b x y,
cond_Ropp b (x + y) = (cond_Ropp b x + cond_Ropp b y)%R.
Proof.
End cond_Ropp.
LPO taken from Coquelicot
Theorem LPO_min :
forall P : nat -> Prop, (forall n, P n \/ ~ P n) ->
{n : nat | P n /\ forall i, (i < n)%nat -> ~ P i} + {forall n, ~ P n}.
Proof.
assert (
Hi:
forall n, (0 <
INR n + 1)%
R).
intros N.
rewrite <-
S_INR.
apply lt_0_INR.
apply lt_0_Sn.
intros P HP.
set (
E y :=
exists n, (
P n /\
y = / (
INR n + 1))%
R \/ (~
P n /\
y = 0)%
R).
assert (
HE:
forall n,
P n ->
E (/ (
INR n + 1))%
R).
intros n Pn.
exists n.
left.
now split.
assert (
BE:
is_upper_bound E 1).
intros x [
y [[
_ ->]|[
_ ->]]].
rewrite <-
Rinv_1 at 2.
apply Rinv_le.
exact Rlt_0_1.
rewrite <-
S_INR.
apply (
le_INR 1),
le_n_S,
le_0_n.
exact Rle_0_1.
destruct (
completeness E)
as [
l [
ub lub]].
now exists 1%
R.
destruct (
HP O)
as [
H0|
H0].
exists 1%
R.
exists O.
left.
apply (
conj H0).
rewrite Rplus_0_l.
apply sym_eq,
Rinv_1.
exists 0%
R.
exists O.
right.
now split.
destruct (
Rle_lt_dec l 0)
as [
Hl|
Hl].
right.
intros n Pn.
apply Rle_not_lt with (1 :=
Hl).
apply Rlt_le_trans with (/ (
INR n + 1))%
R.
now apply Rinv_0_lt_compat.
apply ub.
now apply HE.
left.
set (
N :=
Zabs_nat (
up (/
l) - 2)).
exists N.
assert (
HN: (
INR N + 1 =
IZR (
up (/
l)) - 1)%
R).
unfold N.
rewrite INR_IZR_INZ.
rewrite inj_Zabs_nat.
replace (
IZR (
up (/
l)) - 1)%
R with (
IZR (
up (/
l) - 2) + 1)%
R.
apply (
f_equal (
fun v =>
IZR v + 1)%
R).
apply Zabs_eq.
apply Zle_minus_le_0.
apply (
Zlt_le_succ 1).
apply lt_IZR.
apply Rle_lt_trans with (/
l)%
R.
apply Rmult_le_reg_r with (1 :=
Hl).
rewrite Rmult_1_l,
Rinv_l by now apply Rgt_not_eq.
apply lub.
exact BE.
apply archimed.
rewrite minus_IZR.
simpl.
ring.
assert (
H:
forall i, (
i <
N)%
nat -> ~
P i).
intros i HiN Pi.
unfold is_upper_bound in ub.
refine (
Rle_not_lt _ _ (
ub (/ (
INR i + 1))%
R _)
_).
now apply HE.
rewrite <- (
Rinv_involutive l)
by now apply Rgt_not_eq.
apply Rinv_1_lt_contravar.
rewrite <-
S_INR.
apply (
le_INR 1).
apply le_n_S.
apply le_0_n.
apply Rlt_le_trans with (
INR N + 1)%
R.
apply Rplus_lt_compat_r.
now apply lt_INR.
rewrite HN.
apply Rplus_le_reg_r with (-/
l + 1)%
R.
ring_simplify.
apply archimed.
destruct (
HP N)
as [
PN|
PN].
now split.
elimtype False.
refine (
Rle_not_lt _ _ (
lub (/ (
INR (
S N) + 1))%
R _)
_).
intros x [
y [[
Py ->]|[
_ ->]]].
destruct (
eq_nat_dec y N)
as [
HyN|
HyN].
elim PN.
now rewrite <-
HyN.
apply Rinv_le.
apply Hi.
apply Rplus_le_compat_r.
apply Rnot_lt_le.
intros Hy.
refine (
H _ _ Py).
apply INR_lt in Hy.
clear -
Hy HyN.
omega.
now apply Rlt_le,
Rinv_0_lt_compat.
rewrite S_INR,
HN.
ring_simplify (
IZR (
up (/
l)) - 1 + 1)%
R.
rewrite <- (
Rinv_involutive l)
at 2
by now apply Rgt_not_eq.
apply Rinv_1_lt_contravar.
rewrite <-
Rinv_1.
apply Rinv_le.
exact Hl.
now apply lub.
apply archimed.
Qed.
Theorem LPO :
forall P : nat -> Prop, (forall n, P n \/ ~ P n) ->
{n : nat | P n} + {forall n, ~ P n}.
Proof.
intros P HP.
destruct (
LPO_min P HP)
as [[
n [
Pn _]]|
Pn].
left.
now exists n.
now right.
Qed.
Lemma LPO_Z : forall P : Z -> Prop, (forall n, P n \/ ~P n) ->
{n : Z| P n} + {forall n, ~ P n}.
Proof.
A little tactic to simplify terms of the form bpow a * bpow b.
Ltac bpow_simplify :=
repeat
match goal with
| |- context [(bpow _ _ * bpow _ _)] =>
rewrite <- bpow_plus
| |- context [(?X1 * bpow _ _ * bpow _ _)] =>
rewrite (Rmult_assoc X1); rewrite <- bpow_plus
| |- context [(?X1 * (?X2 * bpow _ _) * bpow _ _)] =>
rewrite <- (Rmult_assoc X1 X2); rewrite (Rmult_assoc (X1 * X2));
rewrite <- bpow_plus
end;
repeat
match goal with
| |- context [(bpow _ ?X)] =>
progress ring_simplify X
end;
change (bpow _ 0) with 1;
repeat
match goal with
| |- context [(_ * 1)] =>
rewrite Rmult_1_r
end.