diff options
Diffstat (limited to 'theories/Reals/Rlogic.v')
| -rw-r--r-- | theories/Reals/Rlogic.v | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v index b7ffec2b..0b892a76 100644 --- a/theories/Reals/Rlogic.v +++ b/theories/Reals/Rlogic.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -41,6 +41,7 @@ Variable P : nat -> Prop. Hypothesis HP : forall n, {P n} + {~P n}. Let ge_fun_sums_ge_lemma : (forall (m n : nat) (f : nat -> R), (lt m n) -> (forall i : nat, 0 <= f i) -> sum_f_R0 f m <= sum_f_R0 f n). +Proof. intros m n f mn fpos. replace (sum_f_R0 f m) with (sum_f_R0 f m + 0) by ring. rewrite (tech2 f m n mn). @@ -52,6 +53,7 @@ apply (Rplus_le_compat _ _ _ _ IHn0 (fpos (S (m + S n0)%nat))). Qed. Let ge_fun_sums_ge : (forall (m n : nat) (f : nat -> R), (le m n) -> (forall i : nat, 0 <= f i) -> sum_f_R0 f m <= sum_f_R0 f n). +Proof. intros m n f mn pos. elim (le_lt_or_eq _ _ mn). intro; apply ge_fun_sums_ge_lemma; assumption. @@ -61,6 +63,7 @@ Qed. Let f:=fun n => (if HP n then (1/2)^n else 0)%R. Lemma cauchy_crit_geometric_dec_fun : Cauchy_crit_series f. +Proof. intros e He. assert (X:(Pser (fun n:nat => 1) (1/2) (/ (1 - (1/2))))%R). apply GP_infinite. @@ -233,10 +236,11 @@ fourier. Qed. Lemma sig_forall_dec : {n | ~P n}+{forall n, P n}. +Proof. destruct forall_dec. right; assumption. left. -apply constructive_indefinite_description_nat; auto. +apply constructive_indefinite_ground_description_nat; auto. clear - HP. firstorder. apply Classical_Pred_Type.not_all_ex_not. @@ -255,6 +259,7 @@ principle also derive [up] and its [specification] *) Theorem not_not_archimedean : forall r : R, ~ (forall n : nat, (INR n <= r)%R). +Proof. intros r H. set (E := fun r => exists n : nat, r = INR n). assert (exists x : R, E x) by @@ -266,10 +271,10 @@ assert (H2 : ~ is_upper_bound E M'). intro H5. assert (M <= M')%R by (apply H4; exact H5). apply (Rlt_not_le M M'). - unfold M' in |- *. - pattern M at 2 in |- *. + unfold M'. + pattern M at 2. rewrite <- Rplus_0_l. - pattern (0 + M)%R in |- *. + pattern (0 + M)%R. rewrite Rplus_comm. rewrite <- (Rplus_opp_r 1). apply Rplus_lt_compat_l. @@ -279,7 +284,7 @@ assert (H2 : ~ is_upper_bound E M'). apply H2. intros N (n,H7). rewrite H7. -unfold M' in |- *. +unfold M'. assert (H5 : (INR (S n) <= M)%R) by (apply H3; exists (S n); reflexivity). rewrite S_INR in H5. assert (H6 : (INR n + 1 + -1 <= M + -1)%R). |