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, 156 insertions, 129 deletions

diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index c613c7647..9d962e125 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -8,157 +8,184 @@
  
 (*i $Id$ i*)
 
-Require Compare.
-Require Rbase.
-Require Rfunctions.
-Require Rseries.
-Require PartSum.
-Require Binomial.
-V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Require Import Compare.
+Require Import Rbase.
+Require Import Rfunctions.
+Require Import Rseries.
+Require Import PartSum.
+Require Import Binomial.
 Open Local Scope R_scope.
 
 (* TT Ak; 1<=k<=N *)
-Fixpoint prod_f_SO [An:nat->R;N:nat] : R := Cases N of
-  O => R1
-| (S p) => ``(prod_f_SO An p)*(An (S p))``
-end.
+Fixpoint prod_f_SO (An:nat -> R) (N:nat) {struct N} : R :=
+  match N with
+  | O => 1
+  | S p => prod_f_SO An p * An (S p)
+  end.
 
 (**********)
-Lemma prod_SO_split : (An:nat->R;n,k:nat) (le k n) -> (prod_f_SO An n)==(Rmult (prod_f_SO An k) (prod_f_SO [l:nat](An (plus k l)) (minus n k))).
-Intros; Induction n.
-Cut k=O; [Intro; Rewrite H0; Simpl; Ring | Inversion H; Reflexivity].
-Cut k=(S n)\/(le k n).
-Intro; Elim H0; Intro.
-Rewrite H1; Simpl; Rewrite <- minus_n_n; Simpl; Ring.
-Replace (minus (S n) k) with (S (minus n k)).
-Simpl; Replace (plus k (S (minus n k))) with (S n).
-Rewrite Hrecn; [Ring | Assumption].
-Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Rewrite S_INR; Rewrite minus_INR; [Ring | Assumption].
-Apply INR_eq; Rewrite S_INR; Repeat Rewrite minus_INR.
-Rewrite S_INR; Ring.
-Apply le_trans with n; [Assumption | Apply le_n_Sn].
-Assumption.
-Inversion H; [Left; Reflexivity | Right; Assumption].
+Lemma prod_SO_split :
+ forall (An:nat -> R) (n k:nat),
+   (k <= n)%nat ->
+   prod_f_SO An n =
+   prod_f_SO An k * prod_f_SO (fun l:nat => An (k + l)%nat) (n - k).
+intros; induction  n as [| n Hrecn].
+cut (k = 0%nat);
+ [ intro; rewrite H0; simpl in |- *; ring | inversion H; reflexivity ].
+cut (k = S n \/ (k <= n)%nat).
+intro; elim H0; intro.
+rewrite H1; simpl in |- *; rewrite <- minus_n_n; simpl in |- *; ring.
+replace (S n - k)%nat with (S (n - k)).
+simpl in |- *; replace (k + S (n - k))%nat with (S n).
+rewrite Hrecn; [ ring | assumption ].
+apply INR_eq; rewrite S_INR; rewrite plus_INR; rewrite S_INR;
+ rewrite minus_INR; [ ring | assumption ].
+apply INR_eq; rewrite S_INR; repeat rewrite minus_INR.
+rewrite S_INR; ring.
+apply le_trans with n; [ assumption | apply le_n_Sn ].
+assumption.
+inversion H; [ left; reflexivity | right; assumption ].
 Qed.
 
 (**********)
-Lemma prod_SO_pos : (An:nat->R;N:nat) ((n:nat)(le n N)->``0<=(An n)``) -> ``0<=(prod_f_SO An N)``.
-Intros; Induction N.
-Simpl; Left; Apply Rlt_R0_R1.
-Simpl; Apply Rmult_le_pos.
-Apply HrecN; Intros; Apply H; Apply le_trans with N; [Assumption | Apply le_n_Sn].
-Apply H; Apply le_n.
+Lemma prod_SO_pos :
+ forall (An:nat -> R) (N:nat),
+   (forall n:nat, (n <= N)%nat -> 0 <= An n) -> 0 <= prod_f_SO An N.
+intros; induction  N as [| N HrecN].
+simpl in |- *; left; apply Rlt_0_1.
+simpl in |- *; apply Rmult_le_pos.
+apply HrecN; intros; apply H; apply le_trans with N;
+ [ assumption | apply le_n_Sn ].
+apply H; apply le_n.
 Qed.
 
 (**********)
-Lemma prod_SO_Rle : (An,Bn:nat->R;N:nat) ((n:nat)(le n N)->``0<=(An n)<=(Bn n)``) -> ``(prod_f_SO An N)<=(prod_f_SO Bn N)``.
-Intros; Induction N.
-Right; Reflexivity.
-Simpl; Apply Rle_trans with ``(prod_f_SO An N)*(Bn (S N))``.
-Apply Rle_monotony.
-Apply prod_SO_pos; Intros; Elim (H n (le_trans ? ? ? H0 (le_n_Sn N))); Intros; Assumption.
-Elim (H (S N) (le_n (S N))); Intros; Assumption.
-Do 2 Rewrite <- (Rmult_sym (Bn (S N))); Apply Rle_monotony.
-Elim (H (S N) (le_n (S N))); Intros.
-Apply Rle_trans with (An (S N)); Assumption.
-Apply HrecN; Intros; Elim (H n (le_trans ? ? ? H0 (le_n_Sn N))); Intros; Split; Assumption.
+Lemma prod_SO_Rle :
+ forall (An Bn:nat -> R) (N:nat),
+   (forall n:nat, (n <= N)%nat -> 0 <= An n <= Bn n) ->
+   prod_f_SO An N <= prod_f_SO Bn N.
+intros; induction  N as [| N HrecN].
+right; reflexivity.
+simpl in |- *; apply Rle_trans with (prod_f_SO An N * Bn (S N)).
+apply Rmult_le_compat_l.
+apply prod_SO_pos; intros; elim (H n (le_trans _ _ _ H0 (le_n_Sn N))); intros;
+ assumption.
+elim (H (S N) (le_n (S N))); intros; assumption.
+do 2 rewrite <- (Rmult_comm (Bn (S N))); apply Rmult_le_compat_l.
+elim (H (S N) (le_n (S N))); intros.
+apply Rle_trans with (An (S N)); assumption.
+apply HrecN; intros; elim (H n (le_trans _ _ _ H0 (le_n_Sn N))); intros;
+ split; assumption.
 Qed.
 
 (* Application to factorial *)
-Lemma fact_prodSO : (n:nat) (INR (fact n))==(prod_f_SO [k:nat](INR k) n).
-Intro; Induction n.
-Reflexivity.
-Change (INR (mult (S n) (fact n)))==(prod_f_SO ([k:nat](INR k)) (S n)).
-Rewrite mult_INR; Rewrite Rmult_sym; Rewrite Hrecn; Reflexivity.
+Lemma fact_prodSO :
+ forall n:nat, INR (fact n) = prod_f_SO (fun k:nat => INR k) n.
+intro; induction  n as [| n Hrecn].
+reflexivity.
+change (INR (S n * fact n) = prod_f_SO (fun k:nat => INR k) (S n)) in |- *.
+rewrite mult_INR; rewrite Rmult_comm; rewrite Hrecn; reflexivity.
 Qed.
 
-Lemma le_n_2n : (n:nat) (le n (mult (2) n)).
-Induction n.
-Replace (mult (2) (O)) with O; [Apply le_n | Ring].
-Intros; Replace (mult (2) (S n0)) with (S (S (mult (2) n0))).
-Apply le_n_S; Apply le_S; Assumption.
-Replace (S (S (mult (2) n0))) with (plus (mult (2) n0) (2)); [Idtac | Ring].
-Replace (S n0) with (plus n0 (1)); [Idtac | Ring].
-Ring.
+Lemma le_n_2n : forall n:nat, (n <= 2 * n)%nat.
+simple induction n.
+replace (2 * 0)%nat with 0%nat; [ apply le_n | ring ].
+intros; replace (2 * S n0)%nat with (S (S (2 * n0))).
+apply le_n_S; apply le_S; assumption.
+replace (S (S (2 * n0))) with (2 * n0 + 2)%nat; [ idtac | ring ].
+replace (S n0) with (n0 + 1)%nat; [ idtac | ring ].
+ring.
 Qed. 
 
 (* We prove that (N!)²<=(2N-k)!*k! forall k in [|O;2N|] *)
-Lemma RfactN_fact2N_factk : (N,k:nat) (le k (mult (2) N)) -> ``(Rsqr (INR (fact N)))<=(INR (fact (minus (mult (S (S O)) N) k)))*(INR (fact k))``.
-Intros; Unfold Rsqr; Repeat Rewrite fact_prodSO.
-Cut (le k N)\/(le N k).
-Intro; Elim H0; Intro.
-Rewrite (prod_SO_split [l:nat](INR l) (minus (mult (2) N) k) N).
-Rewrite Rmult_assoc; Apply Rle_monotony.
-Apply prod_SO_pos; Intros; Apply pos_INR.
-Replace (minus (minus (mult (2) N) k) N) with (minus N k).
-Rewrite Rmult_sym; Rewrite (prod_SO_split [l:nat](INR l) N k).
-Apply Rle_monotony.
-Apply prod_SO_pos; Intros; Apply pos_INR.
-Apply prod_SO_Rle; Intros; Split.
-Apply pos_INR.
-Apply le_INR; Apply le_reg_r; Assumption.
-Assumption.
-Apply INR_eq; Repeat Rewrite minus_INR.
-Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
-Apply le_trans with N; [Assumption | Apply le_n_2n].
-Apply simpl_le_plus_l with k; Rewrite <- le_plus_minus.
-Replace (mult (2) N) with (plus N N); [Idtac | Ring].
-Apply le_reg_r; Assumption.
-Assumption.
-Assumption.
-Apply simpl_le_plus_l with k; Rewrite <- le_plus_minus.
-Replace (mult (2) N) with (plus N N); [Idtac | Ring].
-Apply le_reg_r; Assumption.
-Assumption.
-Rewrite <- (Rmult_sym (prod_f_SO [l:nat](INR l) k)); Rewrite (prod_SO_split [l:nat](INR l) k N).
-Rewrite Rmult_assoc; Apply Rle_monotony.
-Apply prod_SO_pos; Intros; Apply pos_INR.
-Rewrite Rmult_sym; Rewrite (prod_SO_split [l:nat](INR l) N (minus (mult (2) N) k)).
-Apply Rle_monotony.
-Apply prod_SO_pos; Intros; Apply pos_INR.
-Replace (minus N (minus (mult (2) N) k)) with (minus k N).
-Apply prod_SO_Rle; Intros; Split.
-Apply pos_INR.
-Apply le_INR; Apply le_reg_r.
-Apply simpl_le_plus_l with k; Rewrite <- le_plus_minus.
-Replace (mult (2) N) with (plus N N); [Idtac | Ring]; Apply le_reg_r; Assumption.
-Assumption.
-Apply INR_eq; Repeat Rewrite minus_INR.
-Rewrite mult_INR; Do 2 Rewrite S_INR; Ring.
-Assumption.
-Apply simpl_le_plus_l with k; Rewrite <- le_plus_minus.
-Replace (mult (2) N) with (plus N N); [Idtac | Ring]; Apply le_reg_r; Assumption.
-Assumption.
-Assumption.
-Apply simpl_le_plus_l with k; Rewrite <- le_plus_minus.
-Replace (mult (2) N) with (plus N N); [Idtac | Ring]; Apply le_reg_r; Assumption.
-Assumption.
-Assumption.
-Elim (le_dec k N); Intro; [Left; Assumption | Right; Assumption].
+Lemma RfactN_fact2N_factk :
+ forall N k:nat,
+   (k <= 2 * N)%nat ->
+   Rsqr (INR (fact N)) <= INR (fact (2 * N - k)) * INR (fact k).
+intros; unfold Rsqr in |- *; repeat rewrite fact_prodSO.
+cut ((k <= N)%nat \/ (N <= k)%nat).
+intro; elim H0; intro.
+rewrite (prod_SO_split (fun l:nat => INR l) (2 * N - k) N).
+rewrite Rmult_assoc; apply Rmult_le_compat_l.
+apply prod_SO_pos; intros; apply pos_INR.
+replace (2 * N - k - N)%nat with (N - k)%nat.
+rewrite Rmult_comm; rewrite (prod_SO_split (fun l:nat => INR l) N k).
+apply Rmult_le_compat_l.
+apply prod_SO_pos; intros; apply pos_INR.
+apply prod_SO_Rle; intros; split.
+apply pos_INR.
+apply le_INR; apply plus_le_compat_r; assumption.
+assumption.
+apply INR_eq; repeat rewrite minus_INR.
+rewrite mult_INR; repeat rewrite S_INR; ring.
+apply le_trans with N; [ assumption | apply le_n_2n ].
+apply (fun p n m:nat => plus_le_reg_l n m p) with k; rewrite <- le_plus_minus.
+replace (2 * N)%nat with (N + N)%nat; [ idtac | ring ].
+apply plus_le_compat_r; assumption.
+assumption.
+assumption.
+apply (fun p n m:nat => plus_le_reg_l n m p) with k; rewrite <- le_plus_minus.
+replace (2 * N)%nat with (N + N)%nat; [ idtac | ring ].
+apply plus_le_compat_r; assumption.
+assumption.
+rewrite <- (Rmult_comm (prod_f_SO (fun l:nat => INR l) k));
+ rewrite (prod_SO_split (fun l:nat => INR l) k N).
+rewrite Rmult_assoc; apply Rmult_le_compat_l.
+apply prod_SO_pos; intros; apply pos_INR.
+rewrite Rmult_comm;
+ rewrite (prod_SO_split (fun l:nat => INR l) N (2 * N - k)).
+apply Rmult_le_compat_l.
+apply prod_SO_pos; intros; apply pos_INR.
+replace (N - (2 * N - k))%nat with (k - N)%nat.
+apply prod_SO_Rle; intros; split.
+apply pos_INR.
+apply le_INR; apply plus_le_compat_r.
+apply (fun p n m:nat => plus_le_reg_l n m p) with k; rewrite <- le_plus_minus.
+replace (2 * N)%nat with (N + N)%nat; [ idtac | ring ];
+ apply plus_le_compat_r; assumption.
+assumption.
+apply INR_eq; repeat rewrite minus_INR.
+rewrite mult_INR; do 2 rewrite S_INR; ring.
+assumption.
+apply (fun p n m:nat => plus_le_reg_l n m p) with k; rewrite <- le_plus_minus.
+replace (2 * N)%nat with (N + N)%nat; [ idtac | ring ];
+ apply plus_le_compat_r; assumption.
+assumption.
+assumption.
+apply (fun p n m:nat => plus_le_reg_l n m p) with k; rewrite <- le_plus_minus.
+replace (2 * N)%nat with (N + N)%nat; [ idtac | ring ];
+ apply plus_le_compat_r; assumption.
+assumption.
+assumption.
+elim (le_dec k N); intro; [ left; assumption | right; assumption ].
 Qed.
 
 (**********)
-Lemma INR_fact_lt_0 : (n:nat) ``0<(INR (fact n))``.
-Intro; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Elim (fact_neq_0 n); Symmetry; Assumption.
+Lemma INR_fact_lt_0 : forall n:nat, 0 < INR (fact n).
+intro; apply lt_INR_0; apply neq_O_lt; red in |- *; intro;
+ elim (fact_neq_0 n); symmetry  in |- *; assumption.
 Qed.
 
 (* We have the following inequality : (C 2N k) <= (C 2N N) forall k in [|O;2N|] *)
-Lemma C_maj : (N,k:nat) (le k (mult (2) N)) -> ``(C (mult (S (S O)) N) k)<=(C (mult (S (S O)) N) N)``.
-Intros; Unfold C; Unfold Rdiv; Apply Rle_monotony.
-Apply pos_INR.
-Replace (minus (mult (2) N) N) with N.
-Apply Rle_monotony_contra with ``((INR (fact N))*(INR (fact N)))``.
-Apply Rmult_lt_pos; Apply INR_fact_lt_0.
-Rewrite <- Rinv_r_sym.
-Rewrite Rmult_sym; Apply Rle_monotony_contra with ``((INR (fact k))*
-   (INR (fact (minus (mult (S (S O)) N) k))))``.
-Apply Rmult_lt_pos; Apply INR_fact_lt_0.
-Rewrite Rmult_1r; Rewrite <- mult_INR; Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym.
-Rewrite Rmult_1l; Rewrite mult_INR; Rewrite (Rmult_sym (INR (fact k))); Replace ``(INR (fact N))*(INR (fact N))`` with (Rsqr (INR (fact N))).
-Apply RfactN_fact2N_factk.
-Assumption.
-Reflexivity.
-Rewrite mult_INR; Apply prod_neq_R0; Apply INR_fact_neq_0.
-Apply prod_neq_R0; Apply INR_fact_neq_0.
-Apply INR_eq; Rewrite minus_INR; [Rewrite mult_INR; Do 2 Rewrite S_INR; Ring | Apply le_n_2n].
-Qed.
+Lemma C_maj : forall N k:nat, (k <= 2 * N)%nat -> C (2 * N) k <= C (2 * N) N.
+intros; unfold C in |- *; unfold Rdiv in |- *; apply Rmult_le_compat_l.
+apply pos_INR.
+replace (2 * N - N)%nat with N.
+apply Rmult_le_reg_l with (INR (fact N) * INR (fact N)).
+apply Rmult_lt_0_compat; apply INR_fact_lt_0.
+rewrite <- Rinv_r_sym.
+rewrite Rmult_comm;
+ apply Rmult_le_reg_l with (INR (fact k) * INR (fact (2 * N - k))).
+apply Rmult_lt_0_compat; apply INR_fact_lt_0.
+rewrite Rmult_1_r; rewrite <- mult_INR; rewrite <- Rmult_assoc;
+ rewrite <- Rinv_r_sym.
+rewrite Rmult_1_l; rewrite mult_INR; rewrite (Rmult_comm (INR (fact k)));
+ replace (INR (fact N) * INR (fact N)) with (Rsqr (INR (fact N))).
+apply RfactN_fact2N_factk.
+assumption.
+reflexivity.
+rewrite mult_INR; apply prod_neq_R0; apply INR_fact_neq_0.
+apply prod_neq_R0; apply INR_fact_neq_0.
+apply INR_eq; rewrite minus_INR;
+ [ rewrite mult_INR; do 2 rewrite S_INR; ring | apply le_n_2n ].
+Qed.
\ No newline at end of file