diff options
Diffstat (limited to 'theories/Reals/Rsigma.v')
| -rw-r--r-- | theories/Reals/Rsigma.v | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v index 0027c274..76b44d96 100644 --- a/theories/Reals/Rsigma.v +++ b/theories/Reals/Rsigma.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 *) @@ -10,7 +10,7 @@ Require Import Rbase. Require Import Rfunctions. Require Import Rseries. Require Import PartSum. -Open Local Scope R_scope. +Local Open Scope R_scope. Set Implicit Arguments. @@ -28,8 +28,8 @@ Section Sigma. Proof. intros; induction k as [| k Hreck]. cut (low = 0%nat). - intro; rewrite H1; unfold sigma in |- *; rewrite <- minus_n_n; - rewrite <- minus_n_O; simpl in |- *; replace (high - 1)%nat with (pred high). + intro; rewrite H1; unfold sigma; rewrite <- minus_n_n; + rewrite <- minus_n_O; simpl; replace (high - 1)%nat with (pred high). apply (decomp_sum (fun k:nat => f k)). assumption. apply pred_of_minus. @@ -42,8 +42,8 @@ Section Sigma. apply Hreck. assumption. apply lt_trans with (S k); [ apply lt_n_Sn | assumption ]. - unfold sigma in |- *; replace (high - S (S k))%nat with (pred (high - S k)). - pattern (S k) at 3 in |- *; replace (S k) with (S k + 0)%nat; + unfold sigma; replace (high - S (S k))%nat with (pred (high - S k)). + pattern (S k) at 3; replace (S k) with (S k + 0)%nat; [ idtac | ring ]. replace (sum_f_R0 (fun k0:nat => f (S (S k) + k0)) (pred (high - S k))) with (sum_f_R0 (fun k0:nat => f (S k + S k0)) (pred (high - S k))). @@ -55,12 +55,12 @@ Section Sigma. replace (high - S (S k))%nat with (high - S k - 1)%nat. apply pred_of_minus. omega. - unfold sigma in |- *; replace (S k - low)%nat with (S (k - low)). - pattern (S k) at 1 in |- *; replace (S k) with (low + S (k - low))%nat. - symmetry in |- *; apply (tech5 (fun i:nat => f (low + i))). + unfold sigma; replace (S k - low)%nat with (S (k - low)). + pattern (S k) at 1; replace (S k) with (low + S (k - low))%nat. + symmetry ; apply (tech5 (fun i:nat => f (low + i))). omega. omega. - rewrite <- H2; unfold sigma in |- *; rewrite <- minus_n_n; simpl in |- *; + rewrite <- H2; unfold sigma; rewrite <- minus_n_n; simpl; replace (high - S low)%nat with (pred (high - low)). replace (sum_f_R0 (fun k0:nat => f (S (low + k0))) (pred (high - low))) with (sum_f_R0 (fun k0:nat => f (low + S k0)) (pred (high - low))). @@ -79,7 +79,7 @@ Section Sigma. (low <= k)%nat -> (k < high)%nat -> sigma low high - sigma low k = sigma (S k) high. Proof. - intros low high k H1 H2; symmetry in |- *; rewrite (sigma_split H1 H2); ring. + intros low high k H1 H2; symmetry ; rewrite (sigma_split H1 H2); ring. Qed. Theorem sigma_diff_neg : @@ -100,8 +100,8 @@ Section Sigma. apply sigma_split. apply le_n. assumption. - unfold sigma in |- *; rewrite <- minus_n_n. - simpl in |- *. + unfold sigma; rewrite <- minus_n_n. + simpl. replace (low + 0)%nat with low; [ reflexivity | ring ]. Qed. @@ -113,20 +113,20 @@ Section Sigma. generalize (lt_le_weak low high H1); intro H3; replace (f high) with (sigma high high). rewrite Rplus_comm; cut (high = S (pred high)). - intro; pattern high at 3 in |- *; rewrite H. + intro; pattern high at 3; rewrite H. apply sigma_split. apply le_S_n; rewrite <- H; apply lt_le_S; assumption. apply lt_pred_n_n; apply le_lt_trans with low; [ apply le_O_n | assumption ]. apply S_pred with 0%nat; apply le_lt_trans with low; [ apply le_O_n | assumption ]. - unfold sigma in |- *; rewrite <- minus_n_n; simpl in |- *; + unfold sigma; rewrite <- minus_n_n; simpl; replace (high + 0)%nat with high; [ reflexivity | ring ]. Qed. Theorem sigma_eq_arg : forall low:nat, sigma low low = f low. Proof. - intro; unfold sigma in |- *; rewrite <- minus_n_n. - simpl in |- *; replace (low + 0)%nat with low; [ reflexivity | ring ]. + intro; unfold sigma; rewrite <- minus_n_n. + simpl; replace (low + 0)%nat with low; [ reflexivity | ring ]. Qed. End Sigma. |