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, 80 insertions, 89 deletions

diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v
index 33c3f6a5f..6470dd581 100644
--- a/theories/Reals/Rtrigo_fun.v
+++ b/theories/Reals/Rtrigo_fun.v
@@ -8,10 +8,9 @@
 
 (*i $Id$ i*)
 
-Require Rbase.
-Require Rfunctions.
-Require SeqSeries.
-V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Require Import Rbase.
+Require Import Rfunctions.
+Require Import SeqSeries.
 Open Local Scope R_scope.
 
 (*****************************************************************)
@@ -24,95 +23,87 @@ Open Local Scope R_scope.
 (*****************************************************************)
 
 (*********)
-Lemma Alembert_exp:(Un_cv
-   [n:nat](Rabsolu (Rmult (Rinv (INR (fact (S n)))) 
-         (Rinv (Rinv (INR (fact n)))))) R0).
-Unfold Un_cv;Intros;Elim (total_order_Rgt eps R1);Intro.
-Split with O;Intros;Rewrite (simpl_fact n);Unfold R_dist;
- Rewrite (minus_R0 (Rabsolu (Rinv (INR (S n)))));
- Rewrite (Rabsolu_Rabsolu (Rinv (INR (S n))));
- Cut (Rgt (Rinv (INR (S n))) R0).
-Intro; Rewrite (Rabsolu_pos_eq (Rinv (INR (S n)))).
-Cut (Rlt (Rminus (Rinv eps) R1) R0).
-Intro;Generalize (Rlt_le_trans (Rminus (Rinv eps) R1) R0 (INR n) H2 
-   (pos_INR n));Clear H2;Intro;
- Unfold Rminus in H2;Generalize (Rlt_compatibility R1 
-       (Rplus (Rinv eps) (Ropp R1)) (INR n) H2);
- Replace (Rplus R1 (Rplus (Rinv eps) (Ropp R1))) with (Rinv eps);
- [Clear H2;Intro|Ring].
-Rewrite (Rplus_sym R1 (INR n)) in H2;Rewrite <-(S_INR n) in H2;
- Generalize (Rmult_gt (Rinv (INR (S n))) eps H1 H);Intro;
- Unfold Rgt in H3;
- Generalize (Rlt_monotony (Rmult (Rinv (INR (S n))) eps) (Rinv eps)
-     (INR (S n)) H3 H2);Intro;
- Rewrite (Rmult_assoc (Rinv (INR (S n))) eps (Rinv eps)) in H4;
- Rewrite (Rinv_r eps (imp_not_Req eps R0 
-      (or_intror (Rlt eps R0) (Rgt eps R0) H))) 
-  in H4;Rewrite (let (H1,H2)=(Rmult_ne (Rinv (INR (S n)))) in H1) 
-  in H4;Rewrite (Rmult_sym (Rinv (INR (S n)))) in H4;
- Rewrite (Rmult_assoc eps (Rinv (INR (S n))) (INR (S n))) in H4;
- Rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) 
-      (sym_not_equal nat O (S n) (O_S n)))) in H4;
- Rewrite (let (H1,H2)=(Rmult_ne eps) in H1) in H4;Assumption.
-Apply Rlt_minus;Unfold Rgt in a;Rewrite <- Rinv_R1;
- Apply (Rinv_lt R1 eps);Auto;
- Rewrite (let (H1,H2)=(Rmult_ne eps) in H2);Unfold Rgt in H;Assumption.
-Unfold Rgt in H1;Apply Rlt_le;Assumption.
-Unfold Rgt;Apply Rlt_Rinv; Apply lt_INR_0;Apply lt_O_Sn.
+Lemma Alembert_exp :
+ Un_cv (fun n:nat => Rabs (/ INR (fact (S n)) * / / INR (fact n))) 0.
+unfold Un_cv in |- *; intros; elim (Rgt_dec eps 1); intro.
+split with 0%nat; intros; rewrite (simpl_fact n); unfold R_dist in |- *;
+ rewrite (Rminus_0_r (Rabs (/ INR (S n))));
+ rewrite (Rabs_Rabsolu (/ INR (S n))); cut (/ INR (S n) > 0).
+intro; rewrite (Rabs_pos_eq (/ INR (S n))).
+cut (/ eps - 1 < 0).
+intro; generalize (Rlt_le_trans (/ eps - 1) 0 (INR n) H2 (pos_INR n));
+ clear H2; intro; unfold Rminus in H2;
+ generalize (Rplus_lt_compat_l 1 (/ eps + -1) (INR n) H2);
+ replace (1 + (/ eps + -1)) with (/ eps); [ clear H2; intro | ring ].
+rewrite (Rplus_comm 1 (INR n)) in H2; rewrite <- (S_INR n) in H2;
+ generalize (Rmult_gt_0_compat (/ INR (S n)) eps H1 H); 
+ intro; unfold Rgt in H3;
+ generalize (Rmult_lt_compat_l (/ INR (S n) * eps) (/ eps) (INR (S n)) H3 H2);
+ intro; rewrite (Rmult_assoc (/ INR (S n)) eps (/ eps)) in H4;
+ rewrite (Rinv_r eps (Rlt_dichotomy_converse eps 0 (or_intror (eps < 0) H)))
+   in H4; rewrite (let (H1, H2) := Rmult_ne (/ INR (S n)) in H1) in H4;
+ rewrite (Rmult_comm (/ INR (S n))) in H4;
+ rewrite (Rmult_assoc eps (/ INR (S n)) (INR (S n))) in H4;
+ rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) (sym_not_equal (O_S n)))) in H4;
+ rewrite (let (H1, H2) := Rmult_ne eps in H1) in H4; 
+ assumption.
+apply Rlt_minus; unfold Rgt in a; rewrite <- Rinv_1;
+ apply (Rinv_lt_contravar 1 eps); auto;
+ rewrite (let (H1, H2) := Rmult_ne eps in H2); unfold Rgt in H; 
+ assumption.
+unfold Rgt in H1; apply Rlt_le; assumption.
+unfold Rgt in |- *; apply Rinv_0_lt_compat; apply lt_INR_0; apply lt_O_Sn.
 (**)
-Cut `0<=(up (Rminus (Rinv eps) R1))`.
-Intro;Elim (IZN (up (Rminus (Rinv eps) R1)) H0);Intros;
- Split with x;Intros;Rewrite (simpl_fact n);Unfold R_dist;
- Rewrite (minus_R0 (Rabsolu (Rinv (INR (S n)))));
- Rewrite (Rabsolu_Rabsolu (Rinv (INR (S n))));
- Cut (Rgt (Rinv (INR (S n))) R0).
-Intro; Rewrite (Rabsolu_pos_eq (Rinv (INR (S n)))).
-Cut (Rlt (Rminus (Rinv eps) R1) (INR x)).
-Intro;Generalize (Rlt_le_trans (Rminus (Rinv eps) R1) (INR x) (INR n) 
-      H4 (le_INR x n ([n,m:nat; H:(ge m n)]H x n H2)));  
- Clear H4;Intro;Unfold Rminus in H4;Generalize (Rlt_compatibility R1 
-       (Rplus (Rinv eps) (Ropp R1)) (INR n) H4);
- Replace (Rplus R1 (Rplus (Rinv eps) (Ropp R1))) with (Rinv eps);
- [Clear H4;Intro|Ring].
-Rewrite (Rplus_sym R1 (INR n)) in H4;Rewrite <-(S_INR n) in H4;
- Generalize (Rmult_gt (Rinv (INR (S n))) eps H3 H);Intro;
- Unfold Rgt in H5;
- Generalize (Rlt_monotony (Rmult (Rinv (INR (S n))) eps) (Rinv eps)
-     (INR (S n)) H5 H4);Intro;
- Rewrite (Rmult_assoc (Rinv (INR (S n))) eps (Rinv eps)) in H6;
- Rewrite (Rinv_r eps (imp_not_Req eps R0 
-      (or_intror (Rlt eps R0) (Rgt eps R0) H))) 
-  in H6;Rewrite (let (H1,H2)=(Rmult_ne (Rinv (INR (S n)))) in H1) 
-  in H6;Rewrite (Rmult_sym (Rinv (INR (S n)))) in H6;
- Rewrite (Rmult_assoc eps (Rinv (INR (S n))) (INR (S n))) in H6;
- Rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) 
-      (sym_not_equal nat O (S n) (O_S n)))) in H6;
- Rewrite (let (H1,H2)=(Rmult_ne eps) in H1) in H6;Assumption.
-Cut (IZR (up (Rminus (Rinv eps) R1)))==(IZR (INZ x));
- [Intro|Rewrite H1;Trivial].
-Elim (archimed (Rminus (Rinv eps) R1));Intros;Clear H6;
- Unfold Rgt in H5;Rewrite H4 in H5;Rewrite INR_IZR_INZ;Assumption.
-Unfold Rgt in H1;Apply Rlt_le;Assumption.
-Unfold Rgt;Apply Rlt_Rinv; Apply lt_INR_0;Apply lt_O_Sn.
-Apply (le_O_IZR (up (Rminus (Rinv eps) R1))); 
- Apply (Rle_trans R0 (Rminus (Rinv eps) R1) 
-  (IZR (up (Rminus (Rinv eps) R1)))).
-Generalize (Rgt_not_le eps R1 b);Clear b;Unfold Rle;Intro;Elim H0;
- Clear H0;Intro.
-Left;Unfold Rgt in H;
- Generalize (Rlt_monotony (Rinv eps) eps R1 (Rlt_Rinv eps H) H0);
- Rewrite (Rinv_l eps (sym_not_eqT R R0 eps
-    (imp_not_Req R0 eps (or_introl (Rlt R0 eps) (Rgt R0 eps) H))));
- Rewrite (let (H1,H2)=(Rmult_ne (Rinv eps)) in H1);Intro;
- Fold (Rgt (Rminus (Rinv eps) R1) R0);Apply Rgt_minus;Unfold Rgt;
- Assumption.
-Right;Rewrite H0;Rewrite Rinv_R1;Apply sym_eqT;Apply eq_Rminus;Auto.
-Elim (archimed (Rminus (Rinv eps) R1));Intros;Clear H1;
- Unfold Rgt in H0;Apply Rlt_le;Assumption.
+cut (0 <= up (/ eps - 1))%Z.
+intro; elim (IZN (up (/ eps - 1)) H0); intros; split with x; intros;
+ rewrite (simpl_fact n); unfold R_dist in |- *;
+ rewrite (Rminus_0_r (Rabs (/ INR (S n))));
+ rewrite (Rabs_Rabsolu (/ INR (S n))); cut (/ INR (S n) > 0).
+intro; rewrite (Rabs_pos_eq (/ INR (S n))).
+cut (/ eps - 1 < INR x).
+intro;
+ generalize
+  (Rlt_le_trans (/ eps - 1) (INR x) (INR n) H4
+     (le_INR x n ((fun (n m:nat) (H:(m >= n)%nat) => H) x n H2))); 
+ clear H4; intro; unfold Rminus in H4;
+ generalize (Rplus_lt_compat_l 1 (/ eps + -1) (INR n) H4);
+ replace (1 + (/ eps + -1)) with (/ eps); [ clear H4; intro | ring ].
+rewrite (Rplus_comm 1 (INR n)) in H4; rewrite <- (S_INR n) in H4;
+ generalize (Rmult_gt_0_compat (/ INR (S n)) eps H3 H); 
+ intro; unfold Rgt in H5;
+ generalize (Rmult_lt_compat_l (/ INR (S n) * eps) (/ eps) (INR (S n)) H5 H4);
+ intro; rewrite (Rmult_assoc (/ INR (S n)) eps (/ eps)) in H6;
+ rewrite (Rinv_r eps (Rlt_dichotomy_converse eps 0 (or_intror (eps < 0) H)))
+   in H6; rewrite (let (H1, H2) := Rmult_ne (/ INR (S n)) in H1) in H6;
+ rewrite (Rmult_comm (/ INR (S n))) in H6;
+ rewrite (Rmult_assoc eps (/ INR (S n)) (INR (S n))) in H6;
+ rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) (sym_not_equal (O_S n)))) in H6;
+ rewrite (let (H1, H2) := Rmult_ne eps in H1) in H6; 
+ assumption.
+cut (IZR (up (/ eps - 1)) = IZR (Z_of_nat x));
+ [ intro | rewrite H1; trivial ].
+elim (archimed (/ eps - 1)); intros; clear H6; unfold Rgt in H5;
+ rewrite H4 in H5; rewrite INR_IZR_INZ; assumption.
+unfold Rgt in H1; apply Rlt_le; assumption.
+unfold Rgt in |- *; apply Rinv_0_lt_compat; apply lt_INR_0; apply lt_O_Sn.
+apply (le_O_IZR (up (/ eps - 1)));
+ apply (Rle_trans 0 (/ eps - 1) (IZR (up (/ eps - 1)))).
+generalize (Rnot_gt_le eps 1 b); clear b; unfold Rle in |- *; intro; elim H0;
+ clear H0; intro.
+left; unfold Rgt in H;
+ generalize (Rmult_lt_compat_l (/ eps) eps 1 (Rinv_0_lt_compat eps H) H0);
+ rewrite
+  (Rinv_l eps
+     (sym_not_eq (Rlt_dichotomy_converse 0 eps (or_introl (0 > eps) H))))
+  ; rewrite (let (H1, H2) := Rmult_ne (/ eps) in H1); 
+ intro; fold (/ eps - 1 > 0) in |- *; apply Rgt_minus; 
+ unfold Rgt in |- *; assumption.
+right; rewrite H0; rewrite Rinv_1; apply sym_eq; apply Rminus_diag_eq; auto.
+elim (archimed (/ eps - 1)); intros; clear H1; unfold Rgt in H0; apply Rlt_le;
+ assumption.
 Qed.
 
 
 
 
 
-