diff options
Diffstat (limited to 'theories/Reals/AltSeries.v')
| -rw-r--r-- | theories/Reals/AltSeries.v | 122 |
1 files changed, 61 insertions, 61 deletions
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index 07a26929..69f29781 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <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 *) @@ -12,7 +12,7 @@ Require Import Rseries. Require Import SeqProp. Require Import PartSum. Require Import Max. -Open Local Scope R_scope. +Local Open Scope R_scope. (**********) (** * Formalization of alternated series *) @@ -24,13 +24,13 @@ Lemma CV_ALT_step0 : Un_decreasing Un -> Un_growing (fun N:nat => sum_f_R0 (tg_alt Un) (S (2 * N))). Proof. - intros; unfold Un_growing in |- *; intro. + intros; unfold Un_growing; intro. cut ((2 * S n)%nat = S (S (2 * n))). intro; rewrite H0. do 4 rewrite tech5; repeat rewrite Rplus_assoc; apply Rplus_le_compat_l. - pattern (tg_alt Un (S (2 * n))) at 1 in |- *; rewrite <- Rplus_0_r. + pattern (tg_alt Un (S (2 * n))) at 1; rewrite <- Rplus_0_r. apply Rplus_le_compat_l. - unfold tg_alt in |- *; rewrite <- H0; rewrite pow_1_odd; rewrite pow_1_even; + unfold tg_alt; rewrite <- H0; rewrite pow_1_odd; rewrite pow_1_even; rewrite Rmult_1_l. apply Rplus_le_reg_l with (Un (S (2 * S n))). rewrite Rplus_0_r; @@ -46,12 +46,12 @@ Lemma CV_ALT_step1 : Un_decreasing Un -> Un_decreasing (fun N:nat => sum_f_R0 (tg_alt Un) (2 * N)). Proof. - intros; unfold Un_decreasing in |- *; intro. + intros; unfold Un_decreasing; intro. cut ((2 * S n)%nat = S (S (2 * n))). intro; rewrite H0; do 2 rewrite tech5; repeat rewrite Rplus_assoc. - pattern (sum_f_R0 (tg_alt Un) (2 * n)) at 2 in |- *; rewrite <- Rplus_0_r. + pattern (sum_f_R0 (tg_alt Un) (2 * n)) at 2; rewrite <- Rplus_0_r. apply Rplus_le_compat_l. - unfold tg_alt in |- *; rewrite <- H0; rewrite pow_1_odd; rewrite pow_1_even; + unfold tg_alt; rewrite <- H0; rewrite pow_1_odd; rewrite pow_1_even; rewrite Rmult_1_l. apply Rplus_le_reg_l with (Un (S (2 * n))). rewrite Rplus_0_r; @@ -70,7 +70,7 @@ Lemma CV_ALT_step2 : sum_f_R0 (fun i:nat => tg_alt Un (S i)) (S (2 * N)) <= 0. Proof. intros; induction N as [| N HrecN]. - simpl in |- *; unfold tg_alt in |- *; simpl in |- *; rewrite Rmult_1_r. + simpl; unfold tg_alt; simpl; rewrite Rmult_1_r. replace (-1 * -1 * Un 2%nat) with (Un 2%nat); [ idtac | ring ]. apply Rplus_le_reg_l with (Un 1%nat); rewrite Rplus_0_r. replace (Un 1%nat + (-1 * Un 1%nat + Un 2%nat)) with (Un 2%nat); @@ -78,10 +78,10 @@ Proof. cut (S (2 * S N) = S (S (S (2 * N)))). intro; rewrite H1; do 2 rewrite tech5. apply Rle_trans with (sum_f_R0 (fun i:nat => tg_alt Un (S i)) (S (2 * N))). - pattern (sum_f_R0 (fun i:nat => tg_alt Un (S i)) (S (2 * N))) at 2 in |- *; + pattern (sum_f_R0 (fun i:nat => tg_alt Un (S i)) (S (2 * N))) at 2; rewrite <- Rplus_0_r. rewrite Rplus_assoc; apply Rplus_le_compat_l. - unfold tg_alt in |- *; rewrite <- H1. + unfold tg_alt; rewrite <- H1. rewrite pow_1_odd. cut (S (S (2 * S N)) = (2 * S (S N))%nat). intro; rewrite H2; rewrite pow_1_even; rewrite Rmult_1_l; rewrite <- H2. @@ -102,7 +102,7 @@ Lemma CV_ALT_step3 : positivity_seq Un -> sum_f_R0 (fun i:nat => tg_alt Un (S i)) N <= 0. Proof. intros; induction N as [| N HrecN]. - simpl in |- *; unfold tg_alt in |- *; simpl in |- *; rewrite Rmult_1_r. + simpl; unfold tg_alt; simpl; rewrite Rmult_1_r. apply Rplus_le_reg_l with (Un 1%nat). rewrite Rplus_0_r; replace (Un 1%nat + -1 * Un 1%nat) with 0; [ apply H0 | ring ]. @@ -112,10 +112,10 @@ Proof. rewrite H3; apply CV_ALT_step2; assumption. rewrite H3; rewrite tech5. apply Rle_trans with (sum_f_R0 (fun i:nat => tg_alt Un (S i)) (S (2 * x))). - pattern (sum_f_R0 (fun i:nat => tg_alt Un (S i)) (S (2 * x))) at 2 in |- *; + pattern (sum_f_R0 (fun i:nat => tg_alt Un (S i)) (S (2 * x))) at 2; rewrite <- Rplus_0_r. apply Rplus_le_compat_l. - unfold tg_alt in |- *; simpl in |- *. + unfold tg_alt; simpl. replace (x + (x + 0))%nat with (2 * x)%nat; [ idtac | ring ]. rewrite pow_1_even. replace (-1 * (-1 * (-1 * 1)) * Un (S (S (S (2 * x))))) with @@ -133,15 +133,15 @@ Lemma CV_ALT_step4 : positivity_seq Un -> has_ub (fun N:nat => sum_f_R0 (tg_alt Un) (S (2 * N))). Proof. - intros; unfold has_ub in |- *; unfold bound in |- *. + intros; unfold has_ub; unfold bound. exists (Un 0%nat). - unfold is_upper_bound in |- *; intros; elim H1; intros. + unfold is_upper_bound; intros; elim H1; intros. rewrite H2; rewrite decomp_sum. replace (tg_alt Un 0) with (Un 0%nat). - pattern (Un 0%nat) at 2 in |- *; rewrite <- Rplus_0_r. + pattern (Un 0%nat) at 2; rewrite <- Rplus_0_r. apply Rplus_le_compat_l. apply CV_ALT_step3; assumption. - unfold tg_alt in |- *; simpl in |- *; ring. + unfold tg_alt; simpl; ring. apply lt_O_Sn. Qed. @@ -159,11 +159,11 @@ Proof. assert (X := growing_cv _ H2 H3). elim X; intros. exists x. - unfold Un_cv in |- *; unfold R_dist in |- *; unfold Un_cv in H1; + unfold Un_cv; unfold R_dist; unfold Un_cv in H1; unfold R_dist in H1; unfold Un_cv in p; unfold R_dist in p. intros; cut (0 < eps / 2); [ intro - | unfold Rdiv in |- *; apply Rmult_lt_0_compat; + | unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. elim (H1 (eps / 2) H5); intros N2 H6. elim (p (eps / 2) H5); intros N1 H7. @@ -180,32 +180,32 @@ Proof. apply Rabs_triang. rewrite (double_var eps); apply Rplus_lt_compat. rewrite H12; apply H7; assumption. - rewrite Rabs_Ropp; unfold tg_alt in |- *; rewrite Rabs_mult; + rewrite Rabs_Ropp; unfold tg_alt; rewrite Rabs_mult; rewrite pow_1_abs; rewrite Rmult_1_l; unfold Rminus in H6; rewrite Ropp_0 in H6; rewrite <- (Rplus_0_r (Un (S n))); apply H6. - unfold ge in |- *; apply le_trans with n. - apply le_trans with N; [ unfold N in |- *; apply le_max_r | assumption ]. + unfold ge; apply le_trans with n. + apply le_trans with N; [ unfold N; apply le_max_r | assumption ]. apply le_n_Sn. rewrite tech5; ring. rewrite H12; apply Rlt_trans with (eps / 2). apply H7; assumption. - unfold Rdiv in |- *; apply Rmult_lt_reg_l with 2. + unfold Rdiv; apply Rmult_lt_reg_l with 2. prove_sup0. rewrite (Rmult_comm 2); rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ rewrite Rmult_1_r | discrR ]. rewrite double. - pattern eps at 1 in |- *; rewrite <- (Rplus_0_r eps); apply Rplus_lt_compat_l; + pattern eps at 1; rewrite <- (Rplus_0_r eps); apply Rplus_lt_compat_l; assumption. elim H10; intro; apply le_double. rewrite <- H11; apply le_trans with N. - unfold N in |- *; apply le_trans with (S (2 * N1)); + unfold N; apply le_trans with (S (2 * N1)); [ apply le_n_Sn | apply le_max_l ]. assumption. apply lt_n_Sm_le. rewrite <- H11. apply lt_le_trans with N. - unfold N in |- *; apply lt_le_trans with (S (2 * N1)). + unfold N; apply lt_le_trans with (S (2 * N1)). apply lt_n_Sn. apply le_max_l. assumption. @@ -222,7 +222,7 @@ Theorem alternated_series : Proof. intros; apply CV_ALT. assumption. - unfold positivity_seq in |- *; apply decreasing_ineq; assumption. + unfold positivity_seq; apply decreasing_ineq; assumption. assumption. Qed. @@ -243,31 +243,31 @@ Proof. apply (decreasing_ineq (fun N:nat => sum_f_R0 (tg_alt Un) (2 * N))). apply CV_ALT_step1; assumption. assumption. - unfold Un_cv in |- *; unfold R_dist in |- *; unfold Un_cv in H1; + unfold Un_cv; unfold R_dist; unfold Un_cv in H1; unfold R_dist in H1; intros. elim (H1 eps H2); intros. exists x; intros. apply H3. - unfold ge in |- *; apply le_trans with (2 * n)%nat. + unfold ge; apply le_trans with (2 * n)%nat. apply le_trans with n. assumption. assert (H5 := mult_O_le n 2). elim H5; intro. cut (0%nat <> 2%nat); - [ intro; elim H7; symmetry in |- *; assumption | discriminate ]. + [ intro; elim H7; symmetry ; assumption | discriminate ]. assumption. apply le_n_Sn. - unfold Un_cv in |- *; unfold R_dist in |- *; unfold Un_cv in H1; + unfold Un_cv; unfold R_dist; unfold Un_cv in H1; unfold R_dist in H1; intros. elim (H1 eps H2); intros. exists x; intros. apply H3. - unfold ge in |- *; apply le_trans with n. + unfold ge; apply le_trans with n. assumption. assert (H5 := mult_O_le n 2). elim H5; intro. cut (0%nat <> 2%nat); - [ intro; elim H7; symmetry in |- *; assumption | discriminate ]. + [ intro; elim H7; symmetry ; assumption | discriminate ]. assumption. Qed. @@ -279,13 +279,13 @@ Definition PI_tg (n:nat) := / INR (2 * n + 1). Lemma PI_tg_pos : forall n:nat, 0 <= PI_tg n. Proof. - intro; unfold PI_tg in |- *; left; apply Rinv_0_lt_compat; apply lt_INR_0; + intro; unfold PI_tg; left; apply Rinv_0_lt_compat; apply lt_INR_0; replace (2 * n + 1)%nat with (S (2 * n)); [ apply lt_O_Sn | ring ]. Qed. Lemma PI_tg_decreasing : Un_decreasing PI_tg. Proof. - unfold PI_tg, Un_decreasing in |- *; intro. + unfold PI_tg, Un_decreasing; intro. apply Rmult_le_reg_l with (INR (2 * n + 1)). apply lt_INR_0. replace (2 * n + 1)%nat with (S (2 * n)); [ apply lt_O_Sn | ring ]. @@ -306,7 +306,7 @@ Qed. Lemma PI_tg_cv : Un_cv PI_tg 0. Proof. - unfold Un_cv in |- *; unfold R_dist in |- *; intros. + unfold Un_cv; unfold R_dist; intros. cut (0 < 2 * eps); [ intro | apply Rmult_lt_0_compat; [ prove_sup0 | assumption ] ]. assert (H1 := archimed (/ (2 * eps))). @@ -316,9 +316,9 @@ Proof. cut (0 < N)%nat. intro; exists N; intros. cut (0 < n)%nat. - intro; unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r; + intro; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_right. - unfold PI_tg in |- *; apply Rlt_trans with (/ INR (2 * n)). + unfold PI_tg; apply Rlt_trans with (/ INR (2 * n)). apply Rmult_lt_reg_l with (INR (2 * n)). apply lt_INR_0. replace (2 * n)%nat with (n + n)%nat; [ idtac | ring ]. @@ -337,27 +337,27 @@ Proof. [ discriminate | ring ]. replace n with (S (pred n)). apply not_O_INR; discriminate. - symmetry in |- *; apply S_pred with 0%nat. + symmetry ; apply S_pred with 0%nat. assumption. apply Rle_lt_trans with (/ INR (2 * N)). apply Rmult_le_reg_l with (INR (2 * N)). rewrite mult_INR; apply Rmult_lt_0_compat; - [ simpl in |- *; prove_sup0 | apply lt_INR_0; assumption ]. + [ simpl; prove_sup0 | apply lt_INR_0; assumption ]. rewrite <- Rinv_r_sym. apply Rmult_le_reg_l with (INR (2 * n)). rewrite mult_INR; apply Rmult_lt_0_compat; - [ simpl in |- *; prove_sup0 | apply lt_INR_0; assumption ]. + [ simpl; prove_sup0 | apply lt_INR_0; assumption ]. rewrite (Rmult_comm (INR (2 * n))); rewrite Rmult_assoc; rewrite <- Rinv_l_sym. do 2 rewrite Rmult_1_r; apply le_INR. apply (fun m n p:nat => mult_le_compat_l p n m); assumption. replace n with (S (pred n)). apply not_O_INR; discriminate. - symmetry in |- *; apply S_pred with 0%nat. + symmetry ; apply S_pred with 0%nat. assumption. replace N with (S (pred N)). apply not_O_INR; discriminate. - symmetry in |- *; apply S_pred with 0%nat. + symmetry ; apply S_pred with 0%nat. assumption. rewrite mult_INR. rewrite Rinv_mult_distr. @@ -374,17 +374,17 @@ Proof. replace (/ (2 * eps) * (INR N * (2 * eps))) with (INR N * (2 * eps * / (2 * eps))); [ idtac | ring ]. rewrite <- Rinv_r_sym. - rewrite Rmult_1_r; replace (INR N) with (IZR (Z_of_nat N)). + rewrite Rmult_1_r; replace (INR N) with (IZR (Z.of_nat N)). rewrite <- H4. elim H1; intros; assumption. - symmetry in |- *; apply INR_IZR_INZ. + symmetry ; apply INR_IZR_INZ. apply prod_neq_R0; - [ discrR | red in |- *; intro; rewrite H8 in H; elim (Rlt_irrefl _ H) ]. + [ discrR | red; intro; rewrite H8 in H; elim (Rlt_irrefl _ H) ]. apply not_O_INR. - red in |- *; intro; rewrite H8 in H5; elim (lt_irrefl _ H5). + red; intro; rewrite H8 in H5; elim (lt_irrefl _ H5). replace (INR 2) with 2; [ discrR | reflexivity ]. apply not_O_INR. - red in |- *; intro; rewrite H8 in H5; elim (lt_irrefl _ H5). + red; intro; rewrite H8 in H5; elim (lt_irrefl _ H5). apply Rle_ge; apply PI_tg_pos. apply lt_le_trans with N; assumption. elim H1; intros H5 _. @@ -399,7 +399,7 @@ Proof. elim (Rlt_irrefl _ (Rlt_trans _ _ _ H7 H5)). elim (lt_n_O _ b). apply le_IZR. - simpl in |- *. + simpl. left; apply Rlt_trans with (/ (2 * eps)). apply Rinv_0_lt_compat; assumption. elim H1; intros; assumption. @@ -414,41 +414,41 @@ Proof. Qed. (** Now, PI is defined *) -Definition PI : R := 4 * (let (a,_) := exist_PI in a). +Definition Alt_PI : R := 4 * (let (a,_) := exist_PI in a). (** We can get an approximation of PI with the following inequality *) -Lemma PI_ineq : +Lemma Alt_PI_ineq : forall N:nat, - sum_f_R0 (tg_alt PI_tg) (S (2 * N)) <= PI / 4 <= + sum_f_R0 (tg_alt PI_tg) (S (2 * N)) <= Alt_PI / 4 <= sum_f_R0 (tg_alt PI_tg) (2 * N). Proof. intro; apply alternated_series_ineq. apply PI_tg_decreasing. apply PI_tg_cv. - unfold PI in |- *; case exist_PI; intro. + unfold Alt_PI; case exist_PI; intro. replace (4 * x / 4) with x. trivial. - unfold Rdiv in |- *; rewrite (Rmult_comm 4); rewrite Rmult_assoc; + unfold Rdiv; rewrite (Rmult_comm 4); rewrite Rmult_assoc; rewrite <- Rinv_r_sym; [ rewrite Rmult_1_r; reflexivity | discrR ]. Qed. -Lemma PI_RGT_0 : 0 < PI. +Lemma Alt_PI_RGT_0 : 0 < Alt_PI. Proof. - assert (H := PI_ineq 0). + assert (H := Alt_PI_ineq 0). apply Rmult_lt_reg_l with (/ 4). apply Rinv_0_lt_compat; prove_sup0. rewrite Rmult_0_r; rewrite Rmult_comm. elim H; clear H; intros H _. unfold Rdiv in H; apply Rlt_le_trans with (sum_f_R0 (tg_alt PI_tg) (S (2 * 0))). - simpl in |- *; unfold tg_alt in |- *; simpl in |- *; rewrite Rmult_1_l; + simpl; unfold tg_alt; simpl; rewrite Rmult_1_l; rewrite Rmult_1_r; apply Rplus_lt_reg_r with (PI_tg 1). rewrite Rplus_0_r; replace (PI_tg 1 + (PI_tg 0 + -1 * PI_tg 1)) with (PI_tg 0); - [ unfold PI_tg in |- * | ring ]. - simpl in |- *; apply Rinv_lt_contravar. + [ unfold PI_tg | ring ]. + simpl; apply Rinv_lt_contravar. rewrite Rmult_1_l; replace (2 + 1) with 3; [ prove_sup0 | ring ]. - rewrite Rplus_comm; pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; + rewrite Rplus_comm; pattern 1 at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; prove_sup0. assumption. Qed. |