summaryrefslogtreecommitdiff
path: root/theories/Reals/SeqProp.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/SeqProp.v')
-rw-r--r--theories/Reals/SeqProp.v64
1 files changed, 26 insertions, 38 deletions
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index fb2eacee..9a6fb945 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -10,6 +10,7 @@ Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
Require Import Max.
+Require Import Omega.
Local Open Scope R_scope.
(*****************************************************************)
@@ -27,7 +28,7 @@ Lemma growing_cv :
forall Un:nat -> R, Un_growing Un -> has_ub Un -> { l:R | Un_cv Un l }.
Proof.
intros Un Hug Heub.
- exists (projT1 (completeness (EUn Un) Heub (EUn_noempty Un))).
+ exists (proj1_sig (completeness (EUn Un) Heub (EUn_noempty Un))).
destruct (completeness _ Heub (EUn_noempty Un)) as (l, H).
now apply Un_cv_crit_lub.
Qed.
@@ -52,8 +53,7 @@ Proof.
apply growing_cv.
apply decreasing_growing; assumption.
exact H0.
- intro X.
- elim X; intros.
+ intros (x,p).
exists (- x).
unfold Un_cv in p.
unfold R_dist in p.
@@ -150,7 +150,7 @@ Definition sequence_lb (Un:nat -> R) (pr:has_lb Un)
(* Compatibility *)
Notation sequence_majorant := sequence_ub (only parsing).
Notation sequence_minorant := sequence_lb (only parsing).
-
+Unset Standard Proposition Elimination Names.
Lemma Wn_decreasing :
forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_ub Un pr).
Proof.
@@ -158,21 +158,15 @@ Proof.
unfold Un_decreasing.
intro.
unfold sequence_ub.
- assert (H := ub_to_lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)).
- assert (H0 := ub_to_lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)).
- elim H; intros.
- elim H0; intros.
+ pose proof (ub_to_lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)) as (x,(H1,H2)).
+ pose proof (ub_to_lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)) as (x0,(H3,H4)).
cut (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr) = x);
[ intro Maj1; rewrite Maj1 | idtac ].
cut (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr) = x0);
[ intro Maj2; rewrite Maj2 | idtac ].
- unfold is_lub in p.
- unfold is_lub in p0.
- elim p; intros.
apply H2.
- elim p0; intros.
unfold is_upper_bound.
- intros.
+ intros x1 H5.
unfold is_upper_bound in H3.
apply H3.
elim H5; intros.
@@ -183,12 +177,10 @@ Proof.
cut
(is_lub (EUn (fun k:nat => Un (n + k)%nat))
(lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr))).
- intro.
- unfold is_lub in p0; unfold is_lub in H1.
- elim p0; intros; elim H1; intros.
- assert (H6 := H5 x0 H2).
+ intros (H5,H6).
+ assert (H7 := H6 x0 H3).
assert
- (H7 := H3 (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)) H4).
+ (H8 := H4 (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)) H5).
apply Rle_antisym; assumption.
unfold lub.
case (ub_to_lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)).
@@ -196,13 +188,11 @@ Proof.
cut
(is_lub (EUn (fun k:nat => Un (S n + k)%nat))
(lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr))).
- intro.
- unfold is_lub in p; unfold is_lub in H1.
- elim p; intros; elim H1; intros.
- assert (H6 := H5 x H2).
+ intros (H5,H6).
+ assert (H7 := H6 x H1).
assert
- (H7 :=
- H3 (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)) H4).
+ (H8 :=
+ H2 (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)) H5).
apply Rle_antisym; assumption.
unfold lub.
case (ub_to_lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)).
@@ -460,8 +450,7 @@ Lemma cond_eq :
forall x y:R, (forall eps:R, 0 < eps -> Rabs (x - y) < eps) -> x = y.
Proof.
intros.
- case (total_order_T x y); intro.
- elim s; intro.
+ destruct (total_order_T x y) as [[Hlt|Heq]|Hgt].
cut (0 < y - x).
intro.
assert (H1 := H (y - x) H0).
@@ -470,7 +459,7 @@ Proof.
rewrite Rabs_right in H1.
elim (Rlt_irrefl _ H1).
left; assumption.
- apply Rplus_lt_reg_r with x.
+ apply Rplus_lt_reg_l with x.
rewrite Rplus_0_r; replace (x + (y - x)) with y; [ assumption | ring ].
assumption.
cut (0 < x - y).
@@ -479,7 +468,7 @@ Proof.
rewrite Rabs_right in H1.
elim (Rlt_irrefl _ H1).
left; assumption.
- apply Rplus_lt_reg_r with y.
+ apply Rplus_lt_reg_l with y.
rewrite Rplus_0_r; replace (y + (x - y)) with x; [ assumption | ring ].
Qed.
@@ -860,7 +849,7 @@ Proof.
split.
pattern k at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l.
unfold Rdiv; apply Rmult_lt_0_compat.
- apply Rplus_lt_reg_r with k; rewrite Rplus_0_r; replace (k + (1 - k)) with 1;
+ apply Rplus_lt_reg_l with k; rewrite Rplus_0_r; replace (k + (1 - k)) with 1;
[ elim H; intros; assumption | ring ].
apply Rinv_0_lt_compat; prove_sup0.
apply Rmult_lt_reg_l with 2.
@@ -881,12 +870,12 @@ Proof.
apply Rle_lt_trans with (Rabs (Rabs (An (S n) / An n) - k) + Rabs k).
apply Rabs_triang.
rewrite (Rabs_right k).
- apply Rplus_lt_reg_r with (- k); rewrite <- (Rplus_comm k);
+ apply Rplus_lt_reg_l with (- k); rewrite <- (Rplus_comm k);
repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_l;
repeat rewrite Rplus_0_l; apply H4.
apply Rle_ge; elim H; intros; assumption.
unfold Rdiv; apply Rmult_lt_0_compat.
- apply Rplus_lt_reg_r with k; rewrite Rplus_0_r; elim H; intros;
+ apply Rplus_lt_reg_l with k; rewrite Rplus_0_r; elim H; intros;
replace (k + (1 - k)) with 1; [ assumption | ring ].
apply Rinv_0_lt_compat; prove_sup0.
Qed.
@@ -896,8 +885,7 @@ Lemma growing_ineq :
forall (Un:nat -> R) (l:R),
Un_growing Un -> Un_cv Un l -> forall n:nat, Un n <= l.
Proof.
- intros; case (total_order_T (Un n) l); intro.
- elim s; intro.
+ intros; destruct (total_order_T (Un n) l) as [[Hlt|Heq]|Hgt].
left; assumption.
right; assumption.
cut (0 < Un n - l).
@@ -916,7 +904,7 @@ Proof.
apply tech9.
assumption.
unfold N; apply le_max_l.
- apply Rplus_lt_reg_r with l.
+ apply Rplus_lt_reg_l with l.
rewrite Rplus_0_r.
replace (l + (Un n - l)) with (Un n); [ assumption | ring ].
Qed.
@@ -1102,11 +1090,11 @@ Proof.
apply (cv_infty_cv_R0 (fun n:nat => INR (S n))).
intro; apply not_O_INR; discriminate.
assumption.
- unfold cv_infty; intro; case (total_order_T M0 0); intro.
- elim s; intro.
+ unfold cv_infty; intro;
+ destruct (total_order_T M0 0) as [[Hlt|Heq]|Hgt].
exists 0%nat; intros.
apply Rlt_trans with 0; [ assumption | apply lt_INR_0; apply lt_O_Sn ].
- exists 0%nat; intros; rewrite b; apply lt_INR_0; apply lt_O_Sn.
+ exists 0%nat; intros; rewrite Heq; apply lt_INR_0; apply lt_O_Sn.
set (M0_z := up M0).
assert (H10 := archimed M0).
cut (0 <= M0_z)%Z.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 03:05:23 +0000