summaryrefslogtreecommitdiff
path: root/theories/Reals/Rsigma.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /theories/Reals/Rsigma.v
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'theories/Reals/Rsigma.v')
-rw-r--r--theories/Reals/Rsigma.v220
1 files changed, 107 insertions, 113 deletions
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index 1e69a8f5..690c420f 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rsigma.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: Rsigma.v 9245 2006-10-17 12:53:34Z notin $ i*)
Require Import Rbase.
Require Import Rfunctions.
@@ -18,123 +18,117 @@ Set Implicit Arguments.
Section Sigma.
-Variable f : nat -> R.
+ Variable f : nat -> R.
-Definition sigma (low high:nat) : R :=
- sum_f_R0 (fun k:nat => f (low + k)) (high - low).
+ Definition sigma (low high:nat) : R :=
+ sum_f_R0 (fun k:nat => f (low + k)) (high - low).
-Theorem sigma_split :
- forall low high k:nat,
- (low <= k)%nat ->
- (k < high)%nat -> sigma low high = sigma low k + sigma (S k) high.
-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).
-apply (decomp_sum (fun k:nat => f k)).
-assumption.
-apply pred_of_minus.
-inversion H; reflexivity.
-cut ((low <= k)%nat \/ low = S k).
-intro; elim H1; intro.
-replace (sigma low (S k)) with (sigma low k + f (S k)).
-rewrite Rplus_assoc;
- replace (f (S k) + sigma (S (S k)) high) with (sigma (S k) high).
-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;
- [ 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))).
-apply (decomp_sum (fun i:nat => f (S k + i))).
-apply lt_minus_O_lt; assumption.
-apply sum_eq; intros; replace (S k + S i)%nat with (S (S k) + i)%nat.
-reflexivity.
-apply INR_eq; do 2 rewrite plus_INR; do 3 rewrite S_INR; ring.
-replace (high - S (S k))%nat with (high - S k - 1)%nat.
-apply pred_of_minus.
-apply INR_eq; repeat rewrite minus_INR.
-do 4 rewrite S_INR; ring.
-apply lt_le_S; assumption.
-apply lt_le_weak; assumption.
-apply lt_le_S; apply lt_minus_O_lt; assumption.
-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))).
-apply INR_eq; rewrite plus_INR; do 2 rewrite S_INR; rewrite minus_INR.
-ring.
-assumption.
-apply minus_Sn_m; assumption.
-rewrite <- H2; unfold sigma in |- *; rewrite <- minus_n_n; simpl in |- *;
- 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))).
-apply (decomp_sum (fun k0:nat => f (low + k0))).
-apply lt_minus_O_lt.
-apply le_lt_trans with (S k); [ rewrite H2; apply le_n | assumption ].
-apply sum_eq; intros; replace (S (low + i)) with (low + S i)%nat.
-reflexivity.
-apply INR_eq; rewrite plus_INR; do 2 rewrite S_INR; rewrite plus_INR; ring.
-replace (high - S low)%nat with (high - low - 1)%nat.
-apply pred_of_minus.
-apply INR_eq; repeat rewrite minus_INR.
-do 2 rewrite S_INR; ring.
-apply lt_le_S; rewrite H2; assumption.
-rewrite H2; apply lt_le_weak; assumption.
-apply lt_le_S; apply lt_minus_O_lt; rewrite H2; assumption.
-inversion H; [ right; reflexivity | left; assumption ].
-Qed.
+ Theorem sigma_split :
+ forall low high k:nat,
+ (low <= k)%nat ->
+ (k < high)%nat -> sigma low high = sigma low k + sigma (S k) high.
+ 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).
+ apply (decomp_sum (fun k:nat => f k)).
+ assumption.
+ apply pred_of_minus.
+ inversion H; reflexivity.
+ cut ((low <= k)%nat \/ low = S k).
+ intro; elim H1; intro.
+ replace (sigma low (S k)) with (sigma low k + f (S k)).
+ rewrite Rplus_assoc;
+ replace (f (S k) + sigma (S (S k)) high) with (sigma (S k) high).
+ 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;
+ [ 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))).
+ apply (decomp_sum (fun i:nat => f (S k + i))).
+ apply lt_minus_O_lt; assumption.
+ apply sum_eq; intros; replace (S k + S i)%nat with (S (S k) + i)%nat.
+ reflexivity.
+ ring_nat.
+ 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))).
+ omega.
+ omega.
+ rewrite <- H2; unfold sigma in |- *; rewrite <- minus_n_n; simpl in |- *;
+ 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))).
+ apply (decomp_sum (fun k0:nat => f (low + k0))).
+ apply lt_minus_O_lt.
+ apply le_lt_trans with (S k); [ rewrite H2; apply le_n | assumption ].
+ apply sum_eq; intros; replace (S (low + i)) with (low + S i)%nat.
+ reflexivity.
+ ring_nat.
+ omega.
+ inversion H; [ right; reflexivity | left; assumption ].
+ Qed.
-Theorem sigma_diff :
- forall low high k:nat,
- (low <= k)%nat ->
- (k < high)%nat -> sigma low high - sigma low k = sigma (S k) high.
-intros low high k H1 H2; symmetry in |- *; rewrite (sigma_split H1 H2); ring.
-Qed.
+ Theorem sigma_diff :
+ forall low high k:nat,
+ (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.
+ Qed.
-Theorem sigma_diff_neg :
- forall low high k:nat,
- (low <= k)%nat ->
- (k < high)%nat -> sigma low k - sigma low high = - sigma (S k) high.
-intros low high k H1 H2; rewrite (sigma_split H1 H2); ring.
-Qed.
+ Theorem sigma_diff_neg :
+ forall low high k:nat,
+ (low <= k)%nat ->
+ (k < high)%nat -> sigma low k - sigma low high = - sigma (S k) high.
+ Proof.
+ intros low high k H1 H2; rewrite (sigma_split H1 H2); ring.
+ Qed.
-Theorem sigma_first :
- forall low high:nat,
- (low < high)%nat -> sigma low high = f low + sigma (S low) high.
-intros low high H1; generalize (lt_le_S low high H1); intro H2;
- generalize (lt_le_weak low high H1); intro H3;
- replace (f low) with (sigma low low).
-apply sigma_split.
-apply le_n.
-assumption.
-unfold sigma in |- *; rewrite <- minus_n_n.
-simpl in |- *.
-replace (low + 0)%nat with low; [ reflexivity | ring ].
-Qed.
+ Theorem sigma_first :
+ forall low high:nat,
+ (low < high)%nat -> sigma low high = f low + sigma (S low) high.
+ Proof.
+ intros low high H1; generalize (lt_le_S low high H1); intro H2;
+ generalize (lt_le_weak low high H1); intro H3;
+ replace (f low) with (sigma low low).
+ apply sigma_split.
+ apply le_n.
+ assumption.
+ unfold sigma in |- *; rewrite <- minus_n_n.
+ simpl in |- *.
+ replace (low + 0)%nat with low; [ reflexivity | ring ].
+ Qed.
-Theorem sigma_last :
- forall low high:nat,
- (low < high)%nat -> sigma low high = f high + sigma low (pred high).
-intros low high H1; generalize (lt_le_S low high H1); intro H2;
- 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.
-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 |- *;
- replace (high + 0)%nat with high; [ reflexivity | ring ].
-Qed.
+ Theorem sigma_last :
+ forall low high:nat,
+ (low < high)%nat -> sigma low high = f high + sigma low (pred high).
+ Proof.
+ intros low high H1; generalize (lt_le_S low high H1); intro H2;
+ 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.
+ 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 |- *;
+ replace (high + 0)%nat with high; [ reflexivity | ring ].
+ Qed.
-Theorem sigma_eq_arg : forall low:nat, sigma low low = f low.
-intro; unfold sigma in |- *; rewrite <- minus_n_n.
-simpl in |- *; replace (low + 0)%nat with low; [ 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 ].
+ Qed.
-End Sigma. \ No newline at end of file
+End Sigma.