diff options
Diffstat (limited to 'theories/Reals')
43 files changed, 46 insertions, 46 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index e86a4d003..36131beb0 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -14,7 +14,7 @@ Require Rseries. Require SeqProp. Require PartSum. Require Max. -Import R_scope. +V7only [Import R_scope.]. (***************************************************) (* Various versions of the criterion of D'Alembert *) diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index 5c7f02d4d..7047bb03d 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -14,7 +14,7 @@ Require Rseries. Require SeqProp. Require PartSum. Require Max. -Import R_scope. +V7only [Import R_scope.]. (**********) Definition tg_alt [Un:nat->R] : nat->R := [i:nat]``(pow (-1) i)*(Un i)``. diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index 18e833e69..62d160934 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -12,7 +12,7 @@ Require Rbase. Require Rbasic_fun. Require Even. Require Div2. -Import R_scope. +V7only [Import R_scope.]. Lemma minus_neq_O : (n,i:nat) (lt i n) -> ~(minus n i)=O. Intros; Red; Intro. diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v index c97f98474..03b6b46fc 100644 --- a/theories/Reals/Binomial.v +++ b/theories/Reals/Binomial.v @@ -11,7 +11,7 @@ Require Rbase. Require Rfunctions. Require PartSum. -Import R_scope. +V7only [Import R_scope.]. Definition C [n,p:nat] : R := ``(INR (fact n))/((INR (fact p))*(INR (fact (minus n p))))``. diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v index c6926ec18..5cd8bf672 100644 --- a/theories/Reals/Cauchy_prod.v +++ b/theories/Reals/Cauchy_prod.v @@ -12,7 +12,7 @@ Require Rbase. Require Rfunctions. Require Rseries. Require PartSum. -Import R_scope. +V7only [Import R_scope.]. (**********) Lemma sum_N_predN : (An:nat->R;N:nat) (lt O N) -> (sum_f_R0 An N)==``(sum_f_R0 An (pred N)) + (An N)``. diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v index e366adb38..ae650225f 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -14,8 +14,8 @@ Require SeqSeries. Require Rtrigo_def. Require Cos_rel. Require Max. -Import nat_scope. -Import R_scope. +V7only [Import nat_scope.]. +V7only [Import R_scope.]. Definition Majxy [x,y:R] : nat->R := [n:nat](Rdiv (pow (Rmax R1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (4) (S n))) (INR (fact n))). diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index fb41d9927..b773057ed 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -12,7 +12,7 @@ Require Rbase. Require Rfunctions. Require SeqSeries. Require Rtrigo_def. -Import R_scope. +V7only [Import R_scope.]. Definition A1 [x:R] : nat->R := [N:nat](sum_f_R0 [k:nat]``(pow (-1) k)/(INR (fact (mult (S (S O)) k)))*(pow x (mult (S (S O)) k))`` N). diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index 791954d06..62bf0265d 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -10,7 +10,7 @@ Require RIneq. Require Omega. -Import R_scope. +V7only [Import R_scope.]. Lemma Rlt_R0_R2 : ``0<2``. Replace ``2`` with (INR (2)); [Apply lt_INR_0; Apply lt_O_Sn | Reflexivity]. diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index 8a16bfdf1..ca5de937b 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -17,7 +17,7 @@ Require PSeries_reg. Require Div2. Require Even. Require Max. -Import R_scope. +V7only [Import R_scope.]. Definition E1 [x:R] : nat->R := [N:nat](sum_f_R0 [k:nat]``/(INR (fact k))*(pow x k)`` N). diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v index 3e2ff2bb7..7de5c64c0 100644 --- a/theories/Reals/MVT.v +++ b/theories/Reals/MVT.v @@ -12,7 +12,7 @@ Require Rbase. Require Rfunctions. Require Ranalysis1. Require Rtopology. -Import R_scope. +V7only [Import R_scope.]. (* The Mean Value Theorem *) Theorem MVT : (f,g:R->R;a,b:R;pr1:(c:R)``a<c<b``->(derivable_pt f c);pr2:(c:R)``a<c<b``->(derivable_pt g c)) ``a<b`` -> ((c:R)``a<=c<=b``->(continuity_pt f c)) -> ((c:R)``a<=c<=b``->(continuity_pt g c)) -> (EXT c : R | (EXT P : ``a<c<b`` | ``((g b)-(g a))*(derive_pt f c (pr1 c P))==((f b)-(f a))*(derive_pt g c (pr2 c P))``)). diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index 8f7a4fa11..7c7cb59ea 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -13,7 +13,7 @@ Require Rfunctions. Require SeqSeries. Require Rtrigo. Require Ranalysis. -Import R_scope. +V7only [Import R_scope.]. (*******************************************) (* Newton's Integral *) diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v index 92549a55e..8a4aa1fc5 100644 --- a/theories/Reals/PSeries_reg.v +++ b/theories/Reals/PSeries_reg.v @@ -14,7 +14,7 @@ Require SeqSeries. Require Ranalysis1. Require Max. Require Even. -Import R_scope. +V7only [Import R_scope.]. Definition Boule [x:R;r:posreal] : R -> Prop := [y:R]``(Rabsolu (y-x))<r``. diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index 0b3da1ea7..66d3496d3 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -13,7 +13,7 @@ Require Rfunctions. Require Rseries. Require Rcomplete. Require Max. -Import R_scope. +V7only [Import R_scope.]. Lemma tech1 : (An:nat->R;N:nat) ((n:nat)``(le n N)``->``0<(An n)``) -> ``0 < (sum_f_R0 An N)``. Intros; Induction N. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index a09ec9174..0f57c281d 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -16,9 +16,9 @@ Require Export Raxioms. Require Export ZArithRing. Require Omega. Require Export Field. -Import nat_scope. -Import Z_scope. -Import R_scope. +V7only [Import nat_scope.]. +V7only [Import Z_scope.]. +V7only [Import R_scope.]. Implicit Variable Type r:R. diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v index ce022d7c1..edfb48728 100644 --- a/theories/Reals/RList.v +++ b/theories/Reals/RList.v @@ -10,7 +10,7 @@ Require Rbase. Require Rfunctions. -Import R_scope. +V7only [Import R_scope.]. Inductive Rlist : Type := | nil : Rlist diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index 9e8b81d3e..2fa84607f 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -10,7 +10,7 @@ Require Rbase. Require Rbasic_fun. -Import R_scope. +V7only [Import R_scope.]. (****************************************************) (* Rsqr : some results *) diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index 01f0662a9..0fd419288 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -11,7 +11,7 @@ Require Rbase. Require Rfunctions. Require Rsqrt_def. -Import R_scope. +V7only [Import R_scope.]. (* Here is a continuous extension of Rsqrt on R *) Definition sqrt : R->R := [x:R](Cases (case_Rabsolu x) of diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index 40d484dcd..d467261c7 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -28,7 +28,7 @@ Require Export RList. Require Export Sqrt_reg. Require Export Ranalysis4. Require Export Rpower. -Import R_scope. +V7only [Import R_scope.]. Axiom AppVar : R. diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index e2bc87ffe..05cfabcba 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -11,7 +11,7 @@ Require Rbase. Require Rfunctions. Require Ranalysis1. -Import R_scope. +V7only [Import R_scope.]. (**********) Lemma formule : (x,h,l1,l2:R;f1,f2:R->R) ``h<>0`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ``((f1 (x+h))/(f2 (x+h))-(f1 x)/(f2 x))/h-(l1*(f2 x)-l2*(f1 x))/(Rsqr (f2 x))`` == ``/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1) + l1/((f2 x)*(f2 (x+h)))*((f2 x)-(f2 (x+h))) - (f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))-(f2 x))/h-l2) + (l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))*((f2 (x+h))-(f2 x))``. diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v index 0ccda909d..35f28aa64 100644 --- a/theories/Reals/Ranalysis3.v +++ b/theories/Reals/Ranalysis3.v @@ -12,7 +12,7 @@ Require Rbase. Require Rfunctions. Require Ranalysis1. Require Ranalysis2. -Import R_scope. +V7only [Import R_scope.]. (* Division *) Theorem derivable_pt_lim_div : (f1,f2:R->R;x,l1,l2:R) (derivable_pt_lim f1 x l1) -> (derivable_pt_lim f2 x l2) -> ~``(f2 x)==0``-> (derivable_pt_lim (div_fct f1 f2) x ``(l1*(f2 x)-l2*(f1 x))/(Rsqr (f2 x))``). diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index 5dc3991e2..23c52c330 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -15,7 +15,7 @@ Require Rtrigo. Require Ranalysis1. Require Ranalysis3. Require Exp_prop. -Import R_scope. +V7only [Import R_scope.]. (**********) Lemma derivable_pt_inv : (f:R->R;x:R) ``(f x)<>0`` -> (derivable_pt f x) -> (derivable_pt (inv_fct f) x). diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 455511633..6775958fc 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -15,7 +15,7 @@ Require Export ZArith_base. Require Export Rsyntax. Require Export TypeSyntax. -Import R_scope. +V7only [Import R_scope.]. (*********************************************************) (* Field axioms *) diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 57de5d5b9..0c173c951 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -16,7 +16,7 @@ Require Rbase. Require R_Ifp. Require Fourier. -Import R_scope. +V7only [Import R_scope.]. Implicit Variable Type r:R. diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v index 151f2b263..e62db41e5 100644 --- a/theories/Reals/Rcomplete.v +++ b/theories/Reals/Rcomplete.v @@ -13,7 +13,7 @@ Require Rfunctions. Require Rseries. Require SeqProp. Require Max. -Import R_scope. +V7only [Import R_scope.]. (****************************************************) (* R is complete : *) diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index b5c0c6b1c..392c299a0 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -20,7 +20,7 @@ Require Fourier. Require Classical_Prop. Require Classical_Pred_Type. Require Omega. -Import R_scope. +V7only [Import R_scope.]. (*********) Definition D_x:(R->Prop)->R->R->Prop:=[D:R->Prop][y:R][x:R] diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index e4cfa330a..1131f1167 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -25,7 +25,7 @@ Require Export SplitRmult. Require Export ArithProp. Require Omega. Require Zpower. -Import R_scope. +V7only [Import R_scope.]. (*******************************) (** Factorial *) diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v index b36b9ad35..831b32b9e 100644 --- a/theories/Reals/Rgeom.v +++ b/theories/Reals/Rgeom.v @@ -13,7 +13,7 @@ Require Rfunctions. Require SeqSeries. Require Rtrigo. Require R_sqrt. -Import R_scope. +V7only [Import R_scope.]. Definition dist_euc [x0,y0,x1,y1:R] : R := ``(sqrt ((Rsqr (x0-x1))+(Rsqr (y0-y1))))``. diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 7966d9c88..55869a110 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -16,7 +16,7 @@ Require RiemannInt_SF. Require Classical_Prop. Require Classical_Pred_Type. Require Max. -Import R_scope. +V7only [Import R_scope.]. Implicit Arguments On. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 8c1329e4e..46157e3c9 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -12,7 +12,7 @@ Require Rbase. Require Rfunctions. Require Ranalysis. Require Classical_Prop. -Import R_scope. +V7only [Import R_scope.]. Implicit Arguments On. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index c9ad0032d..7f2baa8ef 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -17,7 +17,7 @@ Require Rbase. Require Rfunctions. Require Classical_Prop. Require Fourier. -Import R_scope. +V7only [Import R_scope.]. (*******************************) (* Calculus *) diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index 096ab1eaa..e76236a89 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -23,7 +23,7 @@ Require Rsqrt_def. Require R_sqrt. Require MVT. Require Ranalysis4. -Import R_scope. +V7only [Import R_scope.]. Lemma P_Rmin: (P : R -> Prop) (x, y : R) (P x) -> (P y) -> (P (Rmin x y)). Intros P x y H1 H2; Unfold Rmin; Case (total_order_Rle x y); Intro; Assumption. diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index 7089ac26c..24eba0cef 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -14,7 +14,7 @@ Require Rfunctions. Require Rseries. Require PartSum. Require Binomial. -Import R_scope. +V7only [Import R_scope.]. (* TT Ak; 1<=k<=N *) Fixpoint prod_f_SO [An:nat->R;N:nat] : R := Cases N of diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v index 21cf09264..4769c0cd2 100644 --- a/theories/Reals/Rsigma.v +++ b/theories/Reals/Rsigma.v @@ -12,7 +12,7 @@ Require Rbase. Require Rfunctions. Require Rseries. Require PartSum. -Import R_scope. +V7only [Import R_scope.]. Set Implicit Arguments. diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index 6496c9982..8267692a6 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -13,7 +13,7 @@ Require Rbase. Require Rfunctions. Require SeqSeries. Require Ranalysis1. -Import R_scope. +V7only [Import R_scope.]. Fixpoint Dichotomy_lb [x,y:R;P:R->bool;N:nat] : R := Cases N of diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index 4624850e9..5dc510c66 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -14,7 +14,7 @@ Require Ranalysis1. Require RList. Require Classical_Prop. Require Classical_Pred_Type. -Import R_scope. +V7only [Import R_scope.]. Definition included [D1,D2:R->Prop] : Prop := (x:R)(D1 x)->(D2 x). Definition disc [x:R;delta:posreal] : R->Prop := [y:R]``(Rabsolu (y-x))<delta``. diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index f265b4a77..28a9fccb8 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -19,7 +19,7 @@ Require Export Cos_plus. Require ZArith_base. Require Zcomplements. Require Classical_Prop. -Import R_scope. +V7only [Import R_scope.]. (** sin_PI2 is the only remaining axiom **) Axiom sin_PI2 : ``(sin (PI/2))==1``. diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index d147d68ac..1f8b0ad07 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -12,7 +12,7 @@ Require Rbase. Require Rfunctions. Require SeqSeries. Require Rtrigo_def. -Import R_scope. +V7only [Import R_scope.]. (*****************************************************************) (* Using series definitions of cos and sin *) diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index cfa65824b..925d7be95 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -13,7 +13,7 @@ Require Rfunctions. Require SeqSeries. Require Rtrigo. Require R_sqrt. -Import R_scope. +V7only [Import R_scope.]. Lemma tan_PI : ``(tan PI)==0``. Unfold tan; Rewrite sin_PI; Rewrite cos_PI; Unfold Rdiv; Apply Rmult_Ol. diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index cf2ba3dd2..8ede5a7a1 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -13,7 +13,7 @@ Require Rfunctions. Require SeqSeries. Require Rtrigo_fun. Require Max. -Import R_scope. +V7only [Import R_scope.]. (*****************************) (* Definition of exponential *) diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index aa1c2b9d7..6ec18e56a 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -14,7 +14,7 @@ Require SeqSeries. Require Rtrigo. Require Ranalysis1. Require PSeries_reg. -Import R_scope. +V7only [Import R_scope.]. Lemma CVN_R_cos : (fn:nat->R->R) (fn == [N:nat][x:R]``(pow (-1) N)/(INR (fact (mult (S (S O)) N)))*(pow x (mult (S (S O)) N))``) -> (CVN_R fn). Unfold CVN_R; Intros. diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index e64d9cc4f..3f1a84f9d 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -13,7 +13,7 @@ Require Rfunctions. Require Rseries. Require Classical. Require Max. -Import R_scope. +V7only [Import R_scope.]. Definition Un_decreasing [Un:nat->R] : Prop := (n:nat) (Rle (Un (S n)) (Un n)). Definition opp_seq [Un:nat->R] : nat->R := [n:nat]``-(Un n)``. diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index 14d438077..f3cc24ae9 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -21,7 +21,7 @@ Require Export Rsigma. Require Export Rprod. Require Export Cauchy_prod. Require Export Alembert. -Import R_scope. +V7only [Import R_scope.]. (**********) Lemma sum_maj1 : (fn:nat->R->R;An:nat->R;x,l1,l2:R;N:nat) (Un_cv [n:nat](SP fn n x) l1) -> (Un_cv [n:nat](sum_f_R0 An n) l2) -> ((n:nat)``(Rabsolu (fn n x))<=(An n)``) -> ``(Rabsolu (l1-(SP fn N x)))<=l2-(sum_f_R0 An N)``. diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index ccda09a0b..7d282e592 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -12,7 +12,7 @@ Require Rbase. Require Rfunctions. Require Ranalysis1. Require R_sqrt. -Import R_scope. +V7only [Import R_scope.]. (**********) Lemma sqrt_var_maj : (h:R) ``(Rabsolu h) <= 1`` -> ``(Rabsolu ((sqrt (1+h))-1))<=(Rabsolu h)``. |