Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 110 insertions, 87 deletions

diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index fd14d2c8c..592ddf68f 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -8,110 +8,133 @@
 
 (*i $Id$ i*)
 
-Require Rbase.
-Require Rfunctions.
-Require Rseries.
-Require PartSum.
-V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Require Import Rbase.
+Require Import Rfunctions.
+Require Import Rseries.
+Require Import PartSum.
 Open Local Scope R_scope.
 
 Set Implicit Arguments.
 
 Section Sigma.
 
-Variable f : nat->R.
+Variable f : nat -> R.
 
-Definition sigma [low,high:nat] : R := (sum_f_R0 [k:nat](f (plus low k)) (minus high low)).
+Definition sigma (low high:nat) : R :=
+  sum_f_R0 (fun k:nat => f (low + k)) (high - low).
 
-Theorem sigma_split : (low,high,k:nat) (le low k)->(lt k high)->``(sigma low high)==(sigma low k)+(sigma (S k) high)``.
-Intros; Induction k.
-Cut low = O.
-Intro; Rewrite H1; Unfold sigma; Rewrite <- minus_n_n; Rewrite <- minus_n_O; Simpl; Replace (minus high (S O)) with (pred high).
-Apply (decomp_sum [k:nat](f k)).
-Assumption.
-Apply pred_of_minus.
-Inversion H; Reflexivity.
-Cut (le low k)\/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; Replace (minus high (S (S k))) with (pred (minus high (S k))).
-Pattern 3 (S k); Replace (S k) with (plus (S k) O); [Idtac | Ring].
-Replace (sum_f_R0 [k0:nat](f (plus (S (S k)) k0)) (pred (minus high (S k)))) with (sum_f_R0 [k0:nat](f (plus (S k) (S k0))) (pred (minus high (S k)))).
-Apply (decomp_sum [i:nat](f (plus (S k) i))).
-Apply lt_minus_O_lt; Assumption.
-Apply sum_eq; Intros; Replace (plus (S k) (S i)) with (plus (S (S k)) i).
-Reflexivity.
-Apply INR_eq; Do 2 Rewrite plus_INR; Do 3 Rewrite S_INR; Ring.
-Replace (minus high (S (S k))) with (minus (minus high (S k)) (S O)).
-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; Replace (minus (S k) low) with (S (minus k low)).
-Pattern 1 (S k); Replace (S k) with (plus low (S (minus k low))).
-Symmetry; Apply (tech5 [i:nat](f (plus 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; Rewrite <- minus_n_n; Simpl; Replace (minus high (S low)) with (pred (minus high low)).
-Replace (sum_f_R0 [k0:nat](f (S (plus low k0))) (pred (minus high low))) with (sum_f_R0 [k0:nat](f (plus low (S k0))) (pred (minus high low))).
-Apply (decomp_sum [k0:nat](f (plus 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 (plus low i)) with (plus low (S i)).
-Reflexivity.
-Apply INR_eq; Rewrite plus_INR; Do 2 Rewrite S_INR; Rewrite plus_INR; Ring.
-Replace (minus high (S low)) with (minus (minus high low) (S O)).
-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].
+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_diff : (low,high,k:nat) (le low k) -> (lt k high )->``(sigma low high)-(sigma low k)==(sigma (S k) high)``.
-Intros low high k H1 H2; Symmetry; Rewrite -> (sigma_split H1 H2); Ring.
+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_neg : (low,high,k:nat) (le low k) -> (lt k high)-> ``(sigma low k)-(sigma low high)==-(sigma (S k) high)``.
-Intros low high k H1 H2; Rewrite -> (sigma_split H1 H2); Ring.
+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_first : (low,high:nat) (lt low high) -> ``(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; Rewrite <- minus_n_n.
-Simpl.
-Replace (plus low O) with low; [Reflexivity | Ring].
+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_last : (low,high:nat) (lt low high) -> ``(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_sym; Cut high = (S (pred high)).
-Intro; Pattern 3 high; 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 O; Apply le_lt_trans with low; [Apply le_O_n | Assumption].
-Unfold sigma; Rewrite <- minus_n_n; Simpl; Replace (plus high O) with high; [Reflexivity | Ring].
+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_eq_arg : (low:nat) (sigma low low)==(f low).
-Intro; Unfold sigma; Rewrite <- minus_n_n.
-Simpl; Replace (plus low O) with low; [Reflexivity | Ring].
+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.
 
-End Sigma.
+End Sigma.
\ No newline at end of file