diff options
Diffstat (limited to 'theories/Reals/Rcomplete.v')
| -rw-r--r-- | theories/Reals/Rcomplete.v | 52 |
1 files changed, 25 insertions, 27 deletions
diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v index f6d40631..8e0e0692 100644 --- a/theories/Reals/Rcomplete.v +++ b/theories/Reals/Rcomplete.v @@ -1,19 +1,17 @@ (************************************************************************) (* 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 *) (************************************************************************) -(*i $Id: Rcomplete.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rseries. Require Import SeqProp. Require Import Max. -Open Local Scope R_scope. +Local Open Scope R_scope. (****************************************************) (* R is complete : *) @@ -39,7 +37,7 @@ Proof. intros. exists x. rewrite <- H2 in p0. - unfold Un_cv in |- *. + unfold Un_cv. intros. unfold Un_cv in p; unfold Un_cv in p0. cut (0 < eps / 3). @@ -48,7 +46,7 @@ Proof. elim (p0 (eps / 3) H4); intros. exists (max x1 x2). intros. - unfold R_dist in |- *. + unfold R_dist. apply Rle_lt_trans with (Rabs (Un n - Vn n) + Rabs (Vn n - x)). replace (Un n - x) with (Un n - Vn n + (Vn n - x)); [ apply Rabs_triang | ring ]. @@ -56,14 +54,14 @@ Proof. do 2 rewrite <- (Rplus_comm (Rabs (Vn n - x))). apply Rplus_le_compat_l. repeat rewrite Rabs_right. - unfold Rminus in |- *; do 2 rewrite <- (Rplus_comm (- Vn n)); + unfold Rminus; do 2 rewrite <- (Rplus_comm (- Vn n)); apply Rplus_le_compat_l. assert (H8 := Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)). fold Vn Wn in H8. elim (H8 n); intros. assumption. apply Rle_ge. - unfold Rminus in |- *; apply Rplus_le_reg_l with (Vn n). + unfold Rminus; apply Rplus_le_reg_l with (Vn n). rewrite Rplus_0_r. replace (Vn n + (Wn n + - Vn n)) with (Wn n); [ idtac | ring ]. assert (H8 := Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)). @@ -71,7 +69,7 @@ Proof. elim (H8 n); intros. apply Rle_trans with (Un n); assumption. apply Rle_ge. - unfold Rminus in |- *; apply Rplus_le_reg_l with (Vn n). + unfold Rminus; apply Rplus_le_reg_l with (Vn n). rewrite Rplus_0_r. replace (Vn n + (Un n + - Vn n)) with (Un n); [ idtac | ring ]. assert (H8 := Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)). @@ -87,26 +85,26 @@ Proof. repeat apply Rplus_lt_compat. unfold R_dist in H5. apply H5. - unfold ge in |- *; apply le_trans with (max x1 x2). + unfold ge; apply le_trans with (max x1 x2). apply le_max_l. assumption. rewrite <- Rabs_Ropp. replace (- (x - Vn n)) with (Vn n - x); [ idtac | ring ]. unfold R_dist in H6. apply H6. - unfold ge in |- *; apply le_trans with (max x1 x2). + unfold ge; apply le_trans with (max x1 x2). apply le_max_r. assumption. unfold R_dist in H6. apply H6. - unfold ge in |- *; apply le_trans with (max x1 x2). + unfold ge; apply le_trans with (max x1 x2). apply le_max_r. assumption. right. - pattern eps at 4 in |- *; replace eps with (3 * (eps / 3)). + pattern eps at 4; replace eps with (3 * (eps / 3)). ring. - unfold Rdiv in |- *; rewrite <- Rmult_assoc; apply Rinv_r_simpl_m; discrR. - unfold Rdiv in |- *; apply Rmult_lt_0_compat; + unfold Rdiv; rewrite <- Rmult_assoc; apply Rinv_r_simpl_m; discrR. + unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. apply cond_eq. intros. @@ -132,10 +130,10 @@ Proof. repeat apply Rplus_lt_compat. rewrite <- Rabs_Ropp. replace (- (x - Wn N)) with (Wn N - x); [ apply H4 | ring ]. - unfold ge, N in |- *. + unfold ge, N. apply le_trans with (max N1 N2); apply le_max_l. - unfold Wn, Vn in |- *. - unfold sequence_majorant, sequence_minorant in |- *. + unfold Wn, Vn. + unfold sequence_majorant, sequence_minorant. assert (H7 := approx_maj (fun k:nat => Un (N + k)%nat) (maj_ss Un N (cauchy_maj Un H))). @@ -171,13 +169,13 @@ Proof. [ repeat apply Rplus_lt_compat | ring ]. assumption. apply H6. - unfold ge in |- *. + unfold ge. apply le_trans with N. - unfold N in |- *; apply le_max_r. + unfold N; apply le_max_r. apply le_plus_l. - unfold ge in |- *. + unfold ge. apply le_trans with N. - unfold N in |- *; apply le_max_r. + unfold N; apply le_max_r. apply le_plus_l. rewrite <- Rabs_Ropp. replace (- (Un (N + k1)%nat - Vn N)) with (Vn N - Un (N + k1)%nat); @@ -185,14 +183,14 @@ Proof. reflexivity. reflexivity. apply H5. - unfold ge in |- *; apply le_trans with (max N1 N2). + unfold ge; apply le_trans with (max N1 N2). apply le_max_r. - unfold N in |- *; apply le_max_l. - pattern eps at 4 in |- *; replace eps with (5 * (eps / 5)). + unfold N; apply le_max_l. + pattern eps at 4; replace eps with (5 * (eps / 5)). ring. - unfold Rdiv in |- *; rewrite <- Rmult_assoc; apply Rinv_r_simpl_m. + unfold Rdiv; rewrite <- Rmult_assoc; apply Rinv_r_simpl_m. discrR. - unfold Rdiv in |- *; apply Rmult_lt_0_compat. + unfold Rdiv; apply Rmult_lt_0_compat. assumption. apply Rinv_0_lt_compat. prove_sup0; try apply lt_O_Sn. |