Réorganisation de la librairie des réels

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

1 files changed, 6 insertions, 231 deletions

diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index 5cdfd96ce..1cf745281 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -8,11 +8,9 @@
  
 (*i $Id$ i*)
 
-Require DiscrR.
-Require Rbase.
-Require Rseries.
-Require Binome.
-Require Rcomplet.
+Require RealsB.
+Require Rfunctions.
+Require SeqSeries.
 Require Rtrigo_def.
 
 (*****************************************************************)
@@ -38,223 +36,6 @@ Apply Rlt_Rinv; Sup0.
 Rewrite <- Rinv_l_sym; [Rewrite Rmult_sym; Assumption | DiscrR].
 Qed.
 
-(* Un -> +oo *)
-Definition cv_infty [Un:nat->R] : Prop := (M:R)(EXT N:nat | (n:nat) (le N n) -> ``M<(Un n)``).
-
-(* Un -> +oo => /Un -> O *)
-Lemma cv_infty_cv_R0 : (Un:nat->R) ((n:nat)``(Un n)<>0``) -> (cv_infty Un) -> (Un_cv [n:nat]``/(Un n)`` R0).
-Unfold cv_infty Un_cv; Unfold R_dist; Intros.
-Elim (H0 ``/eps``); Intros N0 H2.
-Exists N0; Intros.
-Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite (Rabsolu_Rinv ? (H n)).
-Apply Rlt_monotony_contra with (Rabsolu (Un n)).
-Apply Rabsolu_pos_lt; Apply H.
-Rewrite <- Rinv_r_sym.
-Apply Rlt_monotony_contra with ``/eps``.
-Apply Rlt_Rinv; Assumption.
-Rewrite Rmult_1r; Rewrite (Rmult_sym ``/eps``); Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym.
-Rewrite Rmult_1r; Apply Rlt_le_trans with (Un n).
-Apply H2; Assumption.
-Apply Rle_Rabsolu.
-Red; Intro; Rewrite H4 in H1; Elim (Rlt_antirefl ? H1).
-Apply Rabsolu_no_R0; Apply H.
-Qed.
-
-(**********)
-Lemma sum_eq_R0 : (An:nat->R;N:nat) ((n:nat)(le n N)->``(An n)==0``) -> (sum_f_R0 An N)==R0.
-Intros; Induction N.
-Simpl; Apply H; Apply le_n.
-Rewrite tech5; Rewrite HrecN; [Rewrite Rplus_Ol; Apply H; Apply le_n | Intros; Apply H; Apply le_trans with N; [Assumption | Apply le_n_Sn]].
-Qed.
-
-(**********)
-Lemma decreasing_prop : (Un:nat->R;m,n:nat) (Un_decreasing Un) -> (le m n) -> ``(Un n)<=(Un m)``.
-Unfold Un_decreasing; Intros.
-Induction n.
-Induction m.
-Right; Reflexivity.
-Elim (le_Sn_O ? H0).
-Cut (le m n)\/m=(S n).
-Intro; Elim H1; Intro.
-Apply Rle_trans with (Un n).
-Apply H.
-Apply Hrecn; Assumption.
-Rewrite H2; Right; Reflexivity.
-Inversion H0; [Right; Reflexivity | Left; Assumption].
-Qed.
-
-(* |x|^n/n! -> 0 *)
-Lemma cv_speed_pow_fact : (x:R) (Un_cv [n:nat]``(pow x n)/(INR (fact n))`` R0).
-Intro; Cut (Un_cv [n:nat]``(pow (Rabsolu x) n)/(INR (fact n))`` R0) -> (Un_cv [n:nat]``(pow x n)/(INR (fact n))`` ``0``).
-Intro; Apply H.
-Unfold Un_cv; Unfold R_dist; Intros; Case (Req_EM x R0); Intro.
-Exists (S O); Intros.
-Rewrite H1; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_R0; Rewrite pow_ne_zero; [Unfold Rdiv; Rewrite Rmult_Ol; Rewrite Rabsolu_R0; Assumption | Red; Intro; Rewrite H3 in H2; Elim (le_Sn_n ? H2)].
-Assert H2 := (Rabsolu_pos_lt x H1); Pose M := (up (Rabsolu x)); Cut `0<=M`.
-Intro; Elim (IZN M H3); Intros M_nat H4.
-Pose Un := [n:nat]``(pow (Rabsolu x) (plus M_nat n))/(INR (fact (plus M_nat n)))``.
-Cut (Un_cv Un R0); Unfold Un_cv; Unfold R_dist; Intros.
-Elim (H5 eps H0); Intros N H6.
-Exists (plus M_nat N); Intros; Cut (EX p:nat | (ge p N)/\n=(plus M_nat p)).
-Intro; Elim H8; Intros p H9.
-Elim H9; Intros; Rewrite H11; Unfold Un in H6; Apply H6; Assumption.
-Exists (minus n M_nat).
-Split.
-Unfold ge; Apply simpl_le_plus_l with M_nat; Rewrite <- le_plus_minus.
-Assumption.
-Apply le_trans with (plus M_nat N).
-Apply le_plus_l.
-Assumption.
-Apply le_plus_minus; Apply le_trans with (plus M_nat N); [Apply le_plus_l | Assumption].
-Pose Vn := [n:nat]``(Rabsolu x)*(Un O)/(INR (S n))``.
-Cut (le (1) M_nat).
-Intro; Cut (n:nat)``0<(Un n)``.
-Intro; Cut (Un_decreasing Un).
-Intro; Cut (n:nat)``(Un (S n))<=(Vn n)``.
-Intro; Cut (Un_cv Vn R0).
-Unfold Un_cv; Unfold R_dist; Intros.
-Elim (H10 eps0 H5); Intros N1 H11.
-Exists (S N1); Intros.
-Cut (n:nat)``0<(Vn n)``.
-Intro; Apply Rle_lt_trans with ``(Rabsolu ((Vn (pred n))-0))``.
-Repeat Rewrite Rabsolu_right.
-Unfold Rminus; Rewrite Ropp_O; Do 2 Rewrite Rplus_Or; Replace n with (S (pred n)).
-Apply H9.
-Inversion H12; Simpl; Reflexivity.
-Apply Rle_sym1; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Left; Apply H13.
-Apply Rle_sym1; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Left; Apply H7.
-Apply H11; Unfold ge; Apply le_S_n; Replace (S (pred n)) with n; [Unfold ge in H12; Exact H12 | Inversion H12; Simpl; Reflexivity].
-Intro; Apply Rlt_le_trans with (Un (S n0)); [Apply H7 | Apply H9].
-Cut (cv_infty [n:nat](INR (S n))).
-Intro; Cut (Un_cv [n:nat]``/(INR (S n))`` R0).
-Unfold Un_cv R_dist; Intros; Unfold Vn.
-Cut ``0<eps1/((Rabsolu x)*(Un O))``.
-Intro; Elim (H11 ? H13); Intros N H14.
-Exists N; Intros; Replace ``(Rabsolu x)*(Un O)/(INR (S n))-0`` with ``((Rabsolu x)*(Un O))*(/(INR (S n))-0)``; [Idtac | Unfold Rdiv; Ring].
-Rewrite Rabsolu_mult; Apply Rlt_monotony_contra with ``/(Rabsolu ((Rabsolu x)*(Un O)))``.
-Apply Rlt_Rinv; Apply Rabsolu_pos_lt.
-Apply prod_neq_R0.
-Apply Rabsolu_no_R0; Assumption.
-Assert H16 := (H7 O); Red; Intro; Rewrite H17 in H16; Elim (Rlt_antirefl ? H16).
-Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1l.
-Replace ``/(Rabsolu ((Rabsolu x)*(Un O)))*eps1`` with ``eps1/((Rabsolu x)*(Un O))``.
-Apply H14; Assumption.
-Unfold Rdiv; Rewrite (Rabsolu_right ``(Rabsolu x)*(Un O)``).
-Apply Rmult_sym.
-Apply Rle_sym1; Apply Rmult_le_pos.
-Apply Rabsolu_pos.
-Left; Apply H7.
-Apply Rabsolu_no_R0.
-Apply prod_neq_R0; [Apply Rabsolu_no_R0; Assumption | Assert H16 := (H7 O); Red; Intro; Rewrite H17 in H16; Elim (Rlt_antirefl ? H16)].
-Unfold Rdiv; Apply Rmult_lt_pos.
-Assumption.
-Apply Rlt_Rinv; Apply Rmult_lt_pos.
-Apply Rabsolu_pos_lt; Assumption.
-Apply H7.
-Apply (cv_infty_cv_R0 [n:nat]``(INR (S n))``).
-Intro; Apply not_O_INR; Discriminate.
-Assumption.
-Unfold cv_infty; Intro; Case (total_order_T M0 R0); Intro.
-Elim s; Intro.
-Exists O; Intros.
-Apply Rlt_trans with R0; [Assumption | Apply lt_INR_0; Apply lt_O_Sn].
-Exists O; Intros; Rewrite b; Apply lt_INR_0; Apply lt_O_Sn.
-Pose M0_z := (up M0).
-Assert H10 := (archimed M0).
-Cut `0<=M0_z`.
-Intro; Elim (IZN ? H11); Intros M0_nat H12.
-Exists M0_nat; Intros.
-Apply Rlt_le_trans with (IZR M0_z).
-Elim H10; Intros; Assumption.
-Rewrite H12; Rewrite <- INR_IZR_INZ; Apply le_INR.
-Apply le_trans with n; [Assumption | Apply le_n_Sn].
-Apply le_IZR; Left; Simpl; Unfold M0_z; Apply Rlt_trans with M0; [Assumption | Elim H10; Intros; Assumption].
-Intro; Apply Rle_trans with ``(Rabsolu x)*(Un n)*/(INR (S n))``.
-Unfold Un; Replace (plus M_nat (S n)) with (plus (plus M_nat n) (1)).
-Rewrite pow_add; Replace (pow (Rabsolu x) (S O)) with (Rabsolu x); [Idtac | Simpl; Ring].
-Unfold Rdiv; Rewrite <- (Rmult_sym (Rabsolu x)); Repeat Rewrite Rmult_assoc; Repeat Apply Rle_monotony.
-Apply Rabsolu_pos.
-Left; Apply pow_lt; Assumption.
-Replace (plus (plus M_nat n) (S O)) with (S (plus M_nat n)).
-Rewrite fact_simpl; Rewrite mult_sym; Rewrite mult_INR; Rewrite Rinv_Rmult.
-Apply Rle_monotony.
-Left; Apply Rlt_Rinv; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H10 := (sym_eq ? ? ? H9); Elim (fact_neq_0 ? H10).
-Left; Apply Rinv_lt.
-Apply Rmult_lt_pos; Apply lt_INR_0; Apply lt_O_Sn.
-Apply lt_INR; Apply lt_n_S.
-Pattern 1 n; Replace n with (plus O n); [Idtac | Reflexivity].
-Apply lt_reg_r.
-Apply lt_le_trans with (S O); [Apply lt_O_Sn | Assumption].
-Apply INR_fact_neq_0.
-Apply not_O_INR; Discriminate.
-Apply INR_eq; Rewrite S_INR; Do 3 Rewrite plus_INR; Reflexivity.
-Apply INR_eq; Do 3 Rewrite plus_INR; Do 2 Rewrite S_INR; Ring.
-Unfold Vn; Rewrite Rmult_assoc; Unfold Rdiv; Rewrite (Rmult_sym (Un O)); Rewrite (Rmult_sym (Un n)).
-Repeat Apply Rle_monotony.
-Apply Rabsolu_pos.
-Left; Apply Rlt_Rinv; Apply lt_INR_0; Apply lt_O_Sn.
-Apply decreasing_prop; [Assumption | Apply le_O_n].
-Unfold Un_decreasing; Intro; Unfold Un.
-Replace (plus M_nat (S n)) with (plus (plus M_nat n) (1)).
-Rewrite pow_add; Unfold Rdiv; Rewrite Rmult_assoc; Apply Rle_monotony.
-Left; Apply pow_lt; Assumption.
-Replace (pow (Rabsolu x) (S O)) with (Rabsolu x); [Idtac | Simpl; Ring].
-Replace (plus (plus M_nat n) (S O)) with (S (plus M_nat n)).
-Apply Rle_monotony_contra with (INR (fact (S (plus M_nat n)))).
-Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H9 := (sym_eq ? ? ? H8); Elim (fact_neq_0 ? H9).
-Rewrite (Rmult_sym (Rabsolu x)); Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym.
-Rewrite Rmult_1l.
-Rewrite fact_simpl; Rewrite mult_INR; Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym.
-Rewrite Rmult_1r; Apply Rle_trans with (INR M_nat).
-Left; Rewrite INR_IZR_INZ.
-Rewrite <- H4; Assert H8 := (archimed (Rabsolu x)); Elim H8; Intros; Assumption.
-Apply le_INR; Apply le_trans with (S M_nat); [Apply le_n_Sn | Apply le_n_S; Apply le_plus_l].
-Apply INR_fact_neq_0.
-Apply INR_fact_neq_0.
-Apply INR_eq; Rewrite S_INR; Do 3 Rewrite plus_INR; Reflexivity.
-Apply INR_eq; Do 3 Rewrite plus_INR; Do 2 Rewrite S_INR; Ring.
-Intro; Unfold Un; Unfold Rdiv; Apply Rmult_lt_pos.
-Apply pow_lt; Assumption.
-Apply Rlt_Rinv; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H8 := (sym_eq ? ? ? H7); Elim (fact_neq_0 ? H8).
-Clear Un Vn; Apply INR_le; Simpl.
-Induction M_nat.
-Assert H6 := (archimed (Rabsolu x)); Fold M in H6; Elim H6; Intros. 
-Rewrite H4 in H7; Rewrite <- INR_IZR_INZ in H7.
-Simpl in H7; Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H2 H7)).
-Replace R1 with (INR (S O)); [Apply le_INR | Reflexivity]; Apply le_n_S; Apply le_O_n.
-Apply le_IZR; Simpl; Left; Apply Rlt_trans with (Rabsolu x).
-Assumption.
-Elim (archimed (Rabsolu x)); Intros; Assumption.
-Unfold Un_cv; Unfold R_dist; Intros; Elim (H eps H0); Intros.
-Exists x0; Intros; Apply Rle_lt_trans with ``(Rabsolu ((pow (Rabsolu x) n)/(INR (fact n))-0))``.
-Unfold Rminus; Rewrite Ropp_O; Do 2 Rewrite Rplus_Or; Rewrite (Rabsolu_right ``(pow (Rabsolu x) n)/(INR (fact n))``).
-Unfold Rdiv; Rewrite Rabsolu_mult; Rewrite (Rabsolu_right ``/(INR (fact n))``).
-Rewrite Pow_Rabsolu; Right; Reflexivity.
-Apply Rle_sym1; Left; Apply Rlt_Rinv; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H4 := (sym_eq ? ? ? H3); Elim (fact_neq_0 ? H4).
-Apply Rle_sym1; Unfold Rdiv; Apply Rmult_le_pos.
-Case (Req_EM x R0); Intro.
-Rewrite H3; Rewrite Rabsolu_R0.
-Induction n; [Simpl; Left; Apply Rlt_R0_R1 | Simpl; Rewrite Rmult_Ol; Right; Reflexivity].
-Left; Apply pow_lt; Apply Rabsolu_pos_lt; Assumption.
-Left; Apply Rlt_Rinv; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H4 := (sym_eq ? ? ? H3); Elim (fact_neq_0 ? H4).
-Apply H1; Assumption.
-Qed.
-
-Lemma pow_Rsqr : (x:R;n:nat) (pow x (mult (2) n))==(pow (Rsqr x) n).
-Intros; Induction n.
-Reflexivity.
-Replace (mult (2) (S n)) with (S (S (mult (2) n))).
-Replace (pow x (S (S (mult (2) n)))) with ``x*x*(pow x (mult (S (S O)) n))``.
-Rewrite Hrecn; Reflexivity.
-Simpl; Ring.
-Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring.
-Qed.
-
-Lemma Ropp_mul3 : (r1,r2:R) ``r1*(-r2) == -(r1*r2)``.
-Intros; Rewrite <- Ropp_mul1; Ring.
-Qed.
-
 (**********)
 (* Un encadrement de sin par ses sommes partielles sur [0;PI] *)
 Theorem sin_bound : (a:R; n:nat) ``0 <= a``->``a <= PI``->``(sin_approx a (plus (mult (S (S O)) n) (S O))) <= (sin a)<= (sin_approx a (mult (S (S O)) (plus n (S O))))``.
@@ -384,12 +165,6 @@ Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite
 Inversion H; [Assumption | Elim Hyp_a; Symmetry; Assumption].
 Qed.
 
-Lemma pow_le : (a:R;n:nat) ``0<=a`` -> ``0<=(pow a n)``.
-Intros; Induction n.
-Simpl; Left; Apply Rlt_R0_R1.
-Simpl; Apply Rmult_le_pos; Assumption.
-Qed.
-
 (**********)
 (* Un encadrement de cos par ses sommes partielles sur [-PI/2;PI/2] *)
 (* La preuve utilise bien sur la parite de cos et des sommes partielles *)
@@ -428,12 +203,12 @@ Apply Rsqr_incr_1.
 Apply Rle_trans with ``PI/2``.
 Assumption.
 Unfold Rdiv; Apply Rle_monotony_contra with ``2``.
-Apply Rgt_2_0.
+Sup0.
 Rewrite <- Rmult_assoc; Rewrite Rinv_r_simpl_m.
 Replace ``2*2`` with ``4``; [Apply PI_4 | Ring].
 DiscrR.
 Assumption.
-Left; Apply Rgt_2_0.
+Left; Sup0.
 Pattern 1 ``4``; Rewrite <- Rplus_Or; Replace ``12`` with ``4+8``; [Apply Rle_compatibility; Left; Sup0 | Ring].
 Rewrite <- (Rplus_sym ``12``); Pattern 1 ``12``; Rewrite <- Rplus_Or; Apply Rle_compatibility.
 Apply ge0_plus_ge0_is_ge0.
@@ -515,4 +290,4 @@ Left; Assumption.
 Rewrite <- (Ropp_Ropp ``PI/2``); Apply Rle_Ropp1; Unfold Rdiv; Unfold Rdiv in H0; Rewrite <- Ropp_mul1; Exact H0.
 Intros; Unfold cos_approx; Apply sum_eq; Intros; Unfold cos_term; Do 2 Rewrite pow_Rsqr; Rewrite Rsqr_neg; Unfold Rdiv; Reflexivity.
 Apply Rgt_RO_Ropp; Assumption.
-Qed.
+Qed.
\ No newline at end of file