diff options
Diffstat (limited to 'theories/Reals/PartSum.v')
-rw-r--r-- | theories/Reals/PartSum.v | 65 |
1 files changed, 28 insertions, 37 deletions
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index 364d72cb..b710c75c 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.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 *) @@ -180,12 +180,9 @@ Proof. replace (S (S (pred N))) with (S N). rewrite (HrecN H1); ring. rewrite H2; simpl; reflexivity. - assert (H2 := O_or_S N). - elim H2; intros. - elim a; intros. - rewrite <- p. + destruct (O_or_S N) as [(m,<-)|<-]. simpl; reflexivity. - rewrite <- b in H1; elim (lt_irrefl _ H1). + elim (lt_irrefl _ H1). rewrite H1; simpl; reflexivity. inversion H. right; reflexivity. @@ -395,9 +392,7 @@ Proof. (sum_f_R0 (fun i:nat => Rabs (An i)) m)). assumption. apply H1; assumption. - assert (H4 := lt_eq_lt_dec n m). - elim H4; intro. - elim a; intro. + destruct (lt_eq_lt_dec n m) as [[ | -> ]|]. rewrite (tech2 An n m); [ idtac | assumption ]. rewrite (tech2 (fun i:nat => Rabs (An i)) n m); [ idtac | assumption ]. unfold R_dist. @@ -418,7 +413,6 @@ Proof. apply Rle_ge. apply cond_pos_sum. intro; apply Rabs_pos. - rewrite b. unfold R_dist. unfold Rminus; do 2 rewrite Rplus_opp_r. rewrite Rabs_R0; right; reflexivity. @@ -451,8 +445,7 @@ Lemma cv_cauchy_1 : { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l } -> Cauchy_crit_series An. Proof. - intros An X. - elim X; intros. + intros An (x,p). unfold Un_cv in p. unfold Cauchy_crit_series; unfold Cauchy_crit. intros. @@ -508,12 +501,11 @@ Lemma sum_incr : Un_cv (fun n:nat => sum_f_R0 An n) l -> (forall n:nat, 0 <= An n) -> sum_f_R0 An N <= l. Proof. - intros; case (total_order_T (sum_f_R0 An N) l); intro. - elim s; intro. - left; apply a. - right; apply b. + intros; destruct (total_order_T (sum_f_R0 An N) l) as [[Hlt|Heq]|Hgt]. + left; apply Hlt. + right; apply Heq. cut (Un_growing (fun n:nat => sum_f_R0 An n)). - intro; set (l1 := sum_f_R0 An N) in r. + intro; set (l1 := sum_f_R0 An N) in Hgt. unfold Un_cv in H; cut (0 < l1 - l). intro; elim (H _ H2); intros. set (N0 := max x N); cut (N0 >= x)%nat. @@ -522,21 +514,21 @@ Proof. intro; unfold R_dist in H5; rewrite Rabs_right in H5. cut (sum_f_R0 An N0 < l1). intro; elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H7 H6)). - apply Rplus_lt_reg_r with (- l). + apply Rplus_lt_reg_l with (- l). do 2 rewrite (Rplus_comm (- l)). apply H5. apply Rle_ge; apply Rplus_le_reg_l with l. rewrite Rplus_0_r; replace (l + (sum_f_R0 An N0 - l)) with (sum_f_R0 An N0); [ idtac | ring ]; apply Rle_trans with l1. - left; apply r. + left; apply Hgt. apply H6. unfold l1; apply Rge_le; apply (growing_prop (fun k:nat => sum_f_R0 An k)). apply H1. unfold ge, N0; apply le_max_r. unfold ge, N0; apply le_max_l. - apply Rplus_lt_reg_r with l; rewrite Rplus_0_r; - replace (l + (l1 - l)) with l1; [ apply r | ring ]. + apply Rplus_lt_reg_l with l; rewrite Rplus_0_r; + replace (l + (l1 - l)) with l1; [ apply Hgt | ring ]. unfold Un_growing; intro; simpl; pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; apply H0. @@ -549,10 +541,9 @@ Lemma sum_cv_maj : Un_cv (fun n:nat => sum_f_R0 An n) l2 -> (forall n:nat, Rabs (fn n x) <= An n) -> Rabs l1 <= l2. Proof. - intros; case (total_order_T (Rabs l1) l2); intro. - elim s; intro. - left; apply a. - right; apply b. + intros; destruct (total_order_T (Rabs l1) l2) as [[Hlt|Heq]|Hgt]. + left; apply Hlt. + right; apply Heq. cut (forall n0:nat, Rabs (SP fn n0 x) <= sum_f_R0 An n0). intro; cut (0 < (Rabs l1 - l2) / 2). intro; unfold Un_cv in H, H0. @@ -568,17 +559,17 @@ Proof. intro; assert (H11 := H2 N). elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H11 H10)). apply Rlt_trans with ((Rabs l1 + l2) / 2); assumption. - case (Rcase_abs (Rabs l1 - Rabs (SP fn N x))); intro. + destruct (Rcase_abs (Rabs l1 - Rabs (SP fn N x))) as [Hlt|Hge]. apply Rlt_trans with (Rabs l1). apply Rmult_lt_reg_l with 2. prove_sup0. unfold Rdiv; rewrite (Rmult_comm 2); rewrite Rmult_assoc; rewrite <- Rinv_l_sym. - rewrite Rmult_1_r; rewrite double; apply Rplus_lt_compat_l; apply r. + rewrite Rmult_1_r; rewrite double; apply Rplus_lt_compat_l; apply Hgt. discrR. - apply (Rminus_lt _ _ r0). - rewrite (Rabs_right _ r0) in H7. - apply Rplus_lt_reg_r with ((Rabs l1 - l2) / 2 - Rabs (SP fn N x)). + apply (Rminus_lt _ _ Hlt). + rewrite (Rabs_right _ Hge) in H7. + apply Rplus_lt_reg_l with ((Rabs l1 - l2) / 2 - Rabs (SP fn N x)). replace ((Rabs l1 - l2) / 2 - Rabs (SP fn N x) + (Rabs l1 + l2) / 2) with (Rabs l1 - Rabs (SP fn N x)). unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l; @@ -586,18 +577,18 @@ Proof. unfold Rdiv; rewrite Rmult_plus_distr_r; rewrite <- (Rmult_comm (/ 2)); rewrite Rmult_minus_distr_l; repeat rewrite (Rmult_comm (/ 2)); pattern (Rabs l1) at 1; - rewrite double_var; unfold Rdiv; ring. - case (Rcase_abs (sum_f_R0 An N - l2)); intro. + rewrite double_var; unfold Rdiv in |- *; ring. + destruct (Rcase_abs (sum_f_R0 An N - l2)) as [Hlt|Hge]. apply Rlt_trans with l2. - apply (Rminus_lt _ _ r0). + apply (Rminus_lt _ _ Hlt). apply Rmult_lt_reg_l with 2. prove_sup0. rewrite (double l2); unfold Rdiv; rewrite (Rmult_comm 2); rewrite Rmult_assoc; rewrite <- Rinv_l_sym. rewrite Rmult_1_r; rewrite (Rplus_comm (Rabs l1)); apply Rplus_lt_compat_l; - apply r. + apply Hgt. discrR. - rewrite (Rabs_right _ r0) in H6; apply Rplus_lt_reg_r with (- l2). + rewrite (Rabs_right _ Hge) in H6; apply Rplus_lt_reg_l with (- l2). replace (- l2 + (Rabs l1 + l2) / 2) with ((Rabs l1 - l2) / 2). rewrite Rplus_comm; apply H6. unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); @@ -610,9 +601,9 @@ Proof. apply H4; unfold ge, N; apply le_max_l. apply H5; unfold ge, N; apply le_max_r. unfold Rdiv; apply Rmult_lt_0_compat. - apply Rplus_lt_reg_r with l2. + apply Rplus_lt_reg_l with l2. rewrite Rplus_0_r; replace (l2 + (Rabs l1 - l2)) with (Rabs l1); - [ apply r | ring ]. + [ apply Hgt | ring ]. apply Rinv_0_lt_compat; prove_sup0. intros; induction n0 as [| n0 Hrecn0]. unfold SP; simpl; apply H1. |