summaryrefslogtreecommitdiff
path: root/theories/Reals
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:08:29 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:08:29 +0100
commit23a6061a81ffa0c214d521287b6af0a31bfa22f0 (patch)
treef1ca9ba9240b98b8695a9f1870e56602734cf97c /theories/Reals
parentde109d8c0c68f569b907e6e24271f259ba28888e (diff)
parent39efc41237ec906226a3a53d7396d51173495204 (diff)
Merge commit 'upstream/8.4_beta+dfsg' into experimental/master
Diffstat (limited to 'theories/Reals')
-rw-r--r--theories/Reals/Alembert.v8
-rw-r--r--theories/Reals/AltSeries.v4
-rw-r--r--theories/Reals/ArithProp.v4
-rw-r--r--theories/Reals/Binomial.v4
-rw-r--r--theories/Reals/Cauchy_prod.v4
-rw-r--r--theories/Reals/Cos_plus.v4
-rw-r--r--theories/Reals/Cos_rel.v4
-rw-r--r--theories/Reals/DiscrR.v4
-rw-r--r--theories/Reals/Exp_prop.v6
-rw-r--r--theories/Reals/Integration.v6
-rw-r--r--theories/Reals/LegacyRfield.v4
-rw-r--r--theories/Reals/MVT.v4
-rw-r--r--theories/Reals/NewtonInt.v4
-rw-r--r--theories/Reals/PSeries_reg.v4
-rw-r--r--theories/Reals/PartSum.v4
-rw-r--r--theories/Reals/RIneq.v46
-rw-r--r--theories/Reals/RList.v4
-rw-r--r--theories/Reals/ROrderedType.v4
-rw-r--r--theories/Reals/R_Ifp.v4
-rw-r--r--theories/Reals/R_sqr.v6
-rw-r--r--theories/Reals/R_sqrt.v4
-rw-r--r--theories/Reals/Ranalysis.v4
-rw-r--r--theories/Reals/Ranalysis1.v38
-rw-r--r--theories/Reals/Ranalysis2.v4
-rw-r--r--theories/Reals/Ranalysis3.v4
-rw-r--r--theories/Reals/Ranalysis4.v4
-rw-r--r--theories/Reals/Raxioms.v10
-rw-r--r--theories/Reals/Rbase.v4
-rw-r--r--theories/Reals/Rbasic_fun.v4
-rw-r--r--theories/Reals/Rcomplete.v4
-rw-r--r--theories/Reals/Rdefinitions.v4
-rw-r--r--theories/Reals/Rderiv.v14
-rw-r--r--theories/Reals/Reals.v6
-rw-r--r--theories/Reals/Rfunctions.v257
-rw-r--r--theories/Reals/Rgeom.v4
-rw-r--r--theories/Reals/RiemannInt.v6
-rw-r--r--theories/Reals/RiemannInt_SF.v6
-rw-r--r--theories/Reals/Rlimit.v5
-rw-r--r--theories/Reals/Rlogic.v9
-rw-r--r--theories/Reals/Rminmax.v2
-rw-r--r--theories/Reals/Rpow_def.v4
-rw-r--r--theories/Reals/Rpower.v3
-rw-r--r--theories/Reals/Rprod.v6
-rw-r--r--theories/Reals/Rseries.v207
-rw-r--r--theories/Reals/Rsigma.v4
-rw-r--r--theories/Reals/Rsqrt_def.v12
-rw-r--r--theories/Reals/Rtopology.v4
-rw-r--r--theories/Reals/Rtrigo.v11
-rw-r--r--theories/Reals/Rtrigo_alt.v4
-rw-r--r--theories/Reals/Rtrigo_calc.v8
-rw-r--r--theories/Reals/Rtrigo_def.v10
-rw-r--r--theories/Reals/Rtrigo_fun.v4
-rw-r--r--theories/Reals/Rtrigo_reg.v4
-rw-r--r--theories/Reals/SeqProp.v317
-rw-r--r--theories/Reals/SeqSeries.v4
-rw-r--r--theories/Reals/SplitAbsolu.v4
-rw-r--r--theories/Reals/SplitRmult.v4
-rw-r--r--theories/Reals/Sqrt_reg.v4
58 files changed, 503 insertions, 636 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index 092eafa3..18612a68 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Alembert.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
@@ -109,7 +107,7 @@ Proof.
symmetry in |- *; apply tech2; assumption.
exists (sum_f_R0 An 0); unfold EUn in |- *; exists 0%nat; reflexivity.
intro X; elim X; intros.
- exists x; apply tech10;
+ exists x; apply Un_cv_crit_lub;
[ unfold Un_growing in |- *; intro; rewrite tech5;
pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r;
apply Rplus_le_compat_l; left; apply H
@@ -524,7 +522,7 @@ Proof.
symmetry in |- *; apply tech2; assumption.
exists (sum_f_R0 An 0); unfold EUn in |- *; exists 0%nat; reflexivity.
intro X; elim X; intros.
- exists x; apply tech10;
+ exists x; apply Un_cv_crit_lub;
[ unfold Un_growing in |- *; intro; rewrite tech5;
pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r;
apply Rplus_le_compat_l; left; apply H
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index cab14704..07a26929 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
- (*i $Id: AltSeries.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index c378a2e2..620561dc 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
- (*i $Id: ArithProp.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rbasic_fun.
Require Import Even.
diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v
index 55c30aec..412f6442 100644
--- a/theories/Reals/Binomial.v
+++ b/theories/Reals/Binomial.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
- (*i $Id: Binomial.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import PartSum.
diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v
index 1a2e5eca..a9d5cde3 100644
--- a/theories/Reals/Cauchy_prod.v
+++ b/theories/Reals/Cauchy_prod.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
- (*i $Id: Cauchy_prod.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index 32480b0b..ec1eeddf 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
- (*i $Id: Cos_plus.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index dec5abd3..73f3c0c6 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Cos_rel.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index 2cdc121f..144de09e 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: DiscrR.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import RIneq.
Require Import Omega.
Open Local Scope R_scope.
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 75ea4755..dd97b865 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Exp_prop.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
@@ -648,7 +646,7 @@ Proof.
apply H3.
rewrite Rminus_0_r; apply Rabs_right.
apply Rle_ge.
- unfold Rdiv in |- *; repeat apply Rmult_le_pos.
+ unfold Rdiv in |- *; apply Rmult_le_pos.
apply pow_le.
apply Rle_trans with 1.
left; apply Rlt_0_1.
diff --git a/theories/Reals/Integration.v b/theories/Reals/Integration.v
index 3199a4f8..da1742ca 100644
--- a/theories/Reals/Integration.v
+++ b/theories/Reals/Integration.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Integration.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export NewtonInt.
Require Export RiemannInt_SF.
-Require Export RiemannInt. \ No newline at end of file
+Require Export RiemannInt.
diff --git a/theories/Reals/LegacyRfield.v b/theories/Reals/LegacyRfield.v
index 32b9699d..49a94021 100644
--- a/theories/Reals/LegacyRfield.v
+++ b/theories/Reals/LegacyRfield.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: LegacyRfield.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Raxioms.
Require Export LegacyField.
Import LegacyRing_theory.
diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v
index 36bbb405..29ebd46d 100644
--- a/theories/Reals/MVT.v
+++ b/theories/Reals/MVT.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: MVT.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis1.
diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v
index 79060771..a4233021 100644
--- a/theories/Reals/NewtonInt.v
+++ b/theories/Reals/NewtonInt.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: NewtonInt.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v
index e7182312..aa588e38 100644
--- a/theories/Reals/PSeries_reg.v
+++ b/theories/Reals/PSeries_reg.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: PSeries_reg.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index b2a0e574..3f90f15a 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: PartSum.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index f02db3d4..70f4ff0d 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1,14 +1,12 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: RIneq.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(*********************************************************)
(** * Basic lemmas for the classical real numbers *)
(*********************************************************)
@@ -1603,7 +1601,7 @@ Lemma pos_INR_nat_of_P : forall p:positive, 0 < INR (nat_of_P p).
Proof.
intro; apply lt_0_INR.
simpl in |- *; auto with real.
- apply lt_O_nat_of_P.
+ apply nat_of_P_pos.
Qed.
Hint Resolve pos_INR_nat_of_P: real.
@@ -1712,38 +1710,32 @@ Qed.
Lemma INR_IZR_INZ : forall n:nat, INR n = IZR (Z_of_nat n).
Proof.
simple induction n; auto with real.
- intros; simpl in |- *; rewrite nat_of_P_o_P_of_succ_nat_eq_succ;
+ intros; simpl in |- *; rewrite nat_of_P_of_succ_nat;
auto with real.
Qed.
Lemma plus_IZR_NEG_POS :
forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q).
Proof.
- intros.
- case (lt_eq_lt_dec (nat_of_P p) (nat_of_P q)).
- intros [H| H]; simpl in |- *.
- rewrite nat_of_P_lt_Lt_compare_complement_morphism; simpl in |- *; trivial.
- rewrite (nat_of_P_minus_morphism q p).
- rewrite minus_INR; auto with arith; ring.
- apply ZC2; apply nat_of_P_lt_Lt_compare_complement_morphism; trivial.
- rewrite (nat_of_P_inj p q); trivial.
- rewrite Pcompare_refl; simpl in |- *; auto with real.
- intro H; simpl in |- *.
- rewrite nat_of_P_gt_Gt_compare_complement_morphism; simpl in |- *;
- auto with arith.
- rewrite (nat_of_P_minus_morphism p q).
- rewrite minus_INR; auto with arith; ring.
- apply ZC2; apply nat_of_P_lt_Lt_compare_complement_morphism; trivial.
+ intros p q; simpl. rewrite Z.pos_sub_spec.
+ case Pcompare_spec; intros H; simpl.
+ subst. ring.
+ rewrite Pminus_minus by trivial.
+ rewrite minus_INR by (now apply lt_le_weak, Plt_lt).
+ ring.
+ rewrite Pminus_minus by trivial.
+ rewrite minus_INR by (now apply lt_le_weak, Plt_lt).
+ ring.
Qed.
(**********)
Lemma plus_IZR : forall n m:Z, IZR (n + m) = IZR n + IZR m.
Proof.
intro z; destruct z; intro t; destruct t; intros; auto with real.
- simpl in |- *; intros; rewrite nat_of_P_plus_morphism; auto with real.
+ simpl; intros; rewrite Pplus_plus; auto with real.
apply plus_IZR_NEG_POS.
rewrite Zplus_comm; rewrite Rplus_comm; apply plus_IZR_NEG_POS.
- simpl in |- *; intros; rewrite nat_of_P_plus_morphism; rewrite plus_INR;
+ simpl; intros; rewrite Pplus_plus; rewrite plus_INR;
auto with real.
Qed.
@@ -1751,14 +1743,14 @@ Qed.
Lemma mult_IZR : forall n m:Z, IZR (n * m) = IZR n * IZR m.
Proof.
intros z t; case z; case t; simpl in |- *; auto with real.
- intros t1 z1; rewrite nat_of_P_mult_morphism; auto with real.
- intros t1 z1; rewrite nat_of_P_mult_morphism; auto with real.
+ intros t1 z1; rewrite Pmult_mult; auto with real.
+ intros t1 z1; rewrite Pmult_mult; auto with real.
rewrite Rmult_comm.
rewrite Ropp_mult_distr_l_reverse; auto with real.
apply Ropp_eq_compat; rewrite mult_comm; auto with real.
- intros t1 z1; rewrite nat_of_P_mult_morphism; auto with real.
+ intros t1 z1; rewrite Pmult_mult; auto with real.
rewrite Ropp_mult_distr_l_reverse; auto with real.
- intros t1 z1; rewrite nat_of_P_mult_morphism; auto with real.
+ intros t1 z1; rewrite Pmult_mult; auto with real.
rewrite Rmult_opp_opp; auto with real.
Qed.
@@ -1766,7 +1758,7 @@ Lemma pow_IZR : forall z n, pow (IZR z) n = IZR (Zpower z (Z_of_nat n)).
Proof.
intros z [|n];simpl;trivial.
rewrite Zpower_pos_nat.
- rewrite nat_of_P_o_P_of_succ_nat_eq_succ. unfold Zpower_nat;simpl.
+ rewrite nat_of_P_of_succ_nat. unfold Zpower_nat;simpl.
rewrite mult_IZR.
induction n;simpl;trivial.
rewrite mult_IZR;ring[IHn].
diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v
index 4e4fb378..dbd2e52f 100644
--- a/theories/Reals/RList.v
+++ b/theories/Reals/RList.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: RList.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Open Local Scope R_scope.
diff --git a/theories/Reals/ROrderedType.v b/theories/Reals/ROrderedType.v
index 87dc07b8..0a8d89c7 100644
--- a/theories/Reals/ROrderedType.v
+++ b/theories/Reals/ROrderedType.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -55,7 +55,7 @@ Definition Rcompare x y :=
| inright _ => Gt
end.
-Lemma Rcompare_spec : forall x y, CompSpec eq Rlt x y (Rcompare x y).
+Lemma Rcompare_spec : forall x y, CompareSpec (x=y) (x<y) (y<x) (Rcompare x y).
Proof.
intros. unfold Rcompare.
destruct total_order_T as [[H|H]|H]; auto.
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index 8cf36c17..9e04a7da 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: R_Ifp.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(**********************************************************)
(** Complements for the reals.Integer and fractional part *)
(* *)
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index df2267d1..f23b9f17 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: R_sqr.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rbasic_fun.
Open Local Scope R_scope.
@@ -72,7 +70,7 @@ Proof.
rewrite Rinv_mult_distr.
repeat rewrite Rmult_assoc.
apply Rmult_eq_compat_l.
- pattern x at 2 in |- *; rewrite Rmult_comm.
+ rewrite Rmult_comm.
repeat rewrite Rmult_assoc.
apply Rmult_eq_compat_l.
reflexivity.
diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v
index 26980c95..2c5ede23 100644
--- a/theories/Reals/R_sqrt.v
+++ b/theories/Reals/R_sqrt.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: R_sqrt.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Rsqrt_def.
diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v
index 39c2271b..01715cf3 100644
--- a/theories/Reals/Ranalysis.v
+++ b/theories/Reals/Ranalysis.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Ranalysis.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Rtrigo.
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 673dc3c1..3075bee8 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Ranalysis1.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Export Rlimit.
@@ -30,15 +28,15 @@ Definition inv_fct f (x:R) : R := / f x.
Delimit Scope Rfun_scope with F.
-Arguments Scope plus_fct [Rfun_scope Rfun_scope R_scope].
-Arguments Scope mult_fct [Rfun_scope Rfun_scope R_scope].
-Arguments Scope minus_fct [Rfun_scope Rfun_scope R_scope].
-Arguments Scope div_fct [Rfun_scope Rfun_scope R_scope].
-Arguments Scope inv_fct [Rfun_scope R_scope].
-Arguments Scope opp_fct [Rfun_scope R_scope].
-Arguments Scope mult_real_fct [R_scope Rfun_scope R_scope].
-Arguments Scope div_real_fct [R_scope Rfun_scope R_scope].
-Arguments Scope comp [Rfun_scope Rfun_scope R_scope].
+Arguments plus_fct (f1 f2)%F x%R.
+Arguments mult_fct (f1 f2)%F x%R.
+Arguments minus_fct (f1 f2)%F x%R.
+Arguments div_fct (f1 f2)%F x%R.
+Arguments inv_fct f%F x%R.
+Arguments opp_fct f%F x%R.
+Arguments mult_real_fct a%R f%F x%R.
+Arguments div_real_fct a%R f%F x%R.
+Arguments comp (f1 f2)%F x%R.
Infix "+" := plus_fct : Rfun_scope.
Notation "- x" := (opp_fct x) : Rfun_scope.
@@ -76,8 +74,8 @@ Definition constant_D_eq f (D:R -> Prop) (c:R) : Prop :=
Definition continuity_pt f (x0:R) : Prop := continue_in f no_cond x0.
Definition continuity f : Prop := forall x:R, continuity_pt f x.
-Arguments Scope continuity_pt [Rfun_scope R_scope].
-Arguments Scope continuity [Rfun_scope].
+Arguments continuity_pt f%F x0%R.
+Arguments continuity f%F.
(**********)
Lemma continuity_pt_plus :
@@ -276,12 +274,12 @@ Definition derivable f := forall x:R, derivable_pt f x.
Definition derive_pt f (x:R) (pr:derivable_pt f x) := proj1_sig pr.
Definition derive f (pr:derivable f) (x:R) := derive_pt f x (pr x).
-Arguments Scope derivable_pt_lim [Rfun_scope R_scope].
-Arguments Scope derivable_pt_abs [Rfun_scope R_scope R_scope].
-Arguments Scope derivable_pt [Rfun_scope R_scope].
-Arguments Scope derivable [Rfun_scope].
-Arguments Scope derive_pt [Rfun_scope R_scope _].
-Arguments Scope derive [Rfun_scope _].
+Arguments derivable_pt_lim f%F x%R l.
+Arguments derivable_pt_abs f%F (x l)%R.
+Arguments derivable_pt f%F x%R.
+Arguments derivable f%F.
+Arguments derive_pt f%F x%R pr.
+Arguments derive f%F pr x.
Definition antiderivative f (g:R -> R) (a b:R) : Prop :=
(forall x:R,
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index fcff9a01..ed80ac43 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Ranalysis2.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis1.
diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v
index c7d95660..afd4a4ee 100644
--- a/theories/Reals/Ranalysis3.v
+++ b/theories/Reals/Ranalysis3.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Ranalysis3.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis1.
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v
index a7c5a387..cc658fee 100644
--- a/theories/Reals/Ranalysis4.v
+++ b/theories/Reals/Ranalysis4.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Ranalysis4.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index b6286c0d..8f01d7d0 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Raxioms.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(*********************************************************)
(** Axiomatisation of the classical reals *)
(*********************************************************)
@@ -107,13 +105,13 @@ Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real.
(**********************************************************)
(**********)
-Boxed Fixpoint INR (n:nat) : R :=
+Fixpoint INR (n:nat) : R :=
match n with
| O => 0
| S O => 1
| S n => INR n + 1
end.
-Arguments Scope INR [nat_scope].
+Arguments INR n%nat.
(**********************************************************)
@@ -127,7 +125,7 @@ Definition IZR (z:Z) : R :=
| Zpos n => INR (nat_of_P n)
| Zneg n => - INR (nat_of_P n)
end.
-Arguments Scope IZR [Z_scope].
+Arguments IZR z%Z.
(**********************************************************)
(** * [R] Archimedean *)
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index 23aae957..dbf9ad71 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rbase.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Rdefinitions.
Require Export Raxioms.
Require Export RIneq.
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 15b04807..4bc7fd10 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rbasic_fun.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(*********************************************************)
(** Complements for the real numbers *)
(* *)
diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v
index f6d40631..77cb560c 100644
--- a/theories/Reals/Rcomplete.v
+++ b/theories/Reals/Rcomplete.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rcomplete.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index d06e2d1b..83c6b82d 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -1,12 +1,10 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rdefinitions.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(*********************************************************)
(** Definitions for the axiomatization *)
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index 701914ac..105d8347 100644
--- a/theories/Reals/Rderiv.v
+++ b/theories/Reals/Rderiv.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rderiv.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(*********************************************************)
(** Definition of the derivative,continuity *)
(* *)
@@ -17,8 +15,6 @@ Require Import Rbase.
Require Import Rfunctions.
Require Import Rlimit.
Require Import Fourier.
-Require Import Classical_Prop.
-Require Import Classical_Pred_Type.
Require Import Omega.
Open Local Scope R_scope.
@@ -168,13 +164,12 @@ Proof.
rewrite eps2 in H10; assumption.
unfold Rabs in |- *; case (Rcase_abs 2); auto.
intro; cut (0 < 2).
- intro; generalize (Rlt_asym 0 2 H7); intro; exfalso; auto.
+ intro ; elim (Rlt_asym 0 2 H7 r).
fourier.
apply Rabs_no_R0.
discrR.
Qed.
-
(*********)
Lemma Dconst :
forall (D:R -> Prop) (y x0:R), D_in (fun x:R => y) (fun x:R => 0) D x0.
@@ -344,8 +339,7 @@ Proof.
rewrite (tech_pow_Rmult x1 n0) in H2; rewrite (tech_pow_Rmult x0 n0) in H2;
rewrite (Rmult_comm (INR n0) (x0 ^ (n0 - 1))) in H2;
rewrite <- (Rmult_assoc x0 (x0 ^ (n0 - 1)) (INR n0)) in H2;
- rewrite (tech_pow_Rmult x0 (n0 - 1)) in H2; elim (classic (n0 = 0%nat));
- intro cond.
+ rewrite (tech_pow_Rmult x0 (n0 - 1)) in H2; elim (Peano_dec.eq_nat_dec n0 0) ; intros cond.
rewrite cond in H2; rewrite cond; simpl in H2; simpl in |- *;
cut (1 + x0 * 1 * 0 = 1 * 1);
[ intro A; rewrite A in H2; assumption | ring ].
@@ -391,7 +385,7 @@ Proof.
intros; elim H11; clear H11; intros; elim (Rmin_Rgt x x1 (R_dist x2 x0));
intros a b; clear b; unfold Rgt in a; elim (a H12);
clear H5 a; intros; unfold D_x, Dgf in H11, H7, H10;
- clear H12; elim (classic (f x2 = f x0)); intro.
+ clear H12; elim (Req_dec (f x2) (f x0)); intro.
elim H11; clear H11; intros; elim H11; clear H11; intros;
generalize (H10 x2 (conj (conj H11 H14) H5)); intro;
rewrite (Rminus_diag_eq (f x2) (f x0) H12) in H16;
diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v
index 9929733f..a15e9949 100644
--- a/theories/Reals/Reals.v
+++ b/theories/Reals/Reals.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Reals.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(** The library REALS is divided in 6 parts :
- Rbase: basic lemmas on R
equalities and inequalities
@@ -29,4 +27,4 @@ Require Export Rfunctions.
Require Export SeqSeries.
Require Export Rtrigo.
Require Export Ranalysis.
-Require Export Integration. \ No newline at end of file
+Require Export Integration.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index a91cf8ae..c0cd7864 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rfunctions.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(*i Some properties about pow and sum have been made with John Harrison i*)
(*i Some Lemmas (about pow and powerRZ) have been done by Laurent Thery i*)
@@ -36,7 +34,7 @@ Open Local Scope R_scope.
(*********)
Lemma INR_fact_neq_0 : forall n:nat, INR (fact n) <> 0.
Proof.
- intro; red in |- *; intro; apply (not_O_INR (fact n) (fact_neq_0 n));
+ intro; red; intro; apply (not_O_INR (fact n) (fact_neq_0 n));
assumption.
Qed.
@@ -51,7 +49,7 @@ Lemma simpl_fact :
forall n:nat, / INR (fact (S n)) * / / INR (fact n) = / INR (S n).
Proof.
intro; rewrite (Rinv_involutive (INR (fact n)) (INR_fact_neq_0 n));
- unfold fact at 1 in |- *; cbv beta iota in |- *; fold fact in |- *;
+ unfold fact at 1; cbv beta iota; fold fact;
rewrite (mult_INR (S n) (fact n));
rewrite (Rinv_mult_distr (INR (S n)) (INR (fact n))).
rewrite (Rmult_assoc (/ INR (S n)) (/ INR (fact n)) (INR (fact n)));
@@ -75,20 +73,20 @@ Qed.
Lemma pow_1 : forall x:R, x ^ 1 = x.
Proof.
- simpl in |- *; auto with real.
+ simpl; auto with real.
Qed.
Lemma pow_add : forall (x:R) (n m:nat), x ^ (n + m) = x ^ n * x ^ m.
Proof.
- intros x n; elim n; simpl in |- *; auto with real.
+ intros x n; elim n; simpl; auto with real.
intros n0 H' m; rewrite H'; auto with real.
Qed.
Lemma pow_nonzero : forall (x:R) (n:nat), x <> 0 -> x ^ n <> 0.
Proof.
- intro; simple induction n; simpl in |- *.
- intro; red in |- *; intro; apply R1_neq_R0; assumption.
- intros; red in |- *; intro; elim (Rmult_integral x (x ^ n0) H1).
+ intro; simple induction n; simpl.
+ intro; red; intro; apply R1_neq_R0; assumption.
+ intros; red; intro; elim (Rmult_integral x (x ^ n0) H1).
intro; auto.
apply H; assumption.
Qed.
@@ -98,24 +96,24 @@ Hint Resolve pow_O pow_1 pow_add pow_nonzero: real.
Lemma pow_RN_plus :
forall (x:R) (n m:nat), x <> 0 -> x ^ n = x ^ (n + m) * / x ^ m.
Proof.
- intros x n; elim n; simpl in |- *; auto with real.
+ intros x n; elim n; simpl; auto with real.
intros n0 H' m H'0.
rewrite Rmult_assoc; rewrite <- H'; auto.
Qed.
Lemma pow_lt : forall (x:R) (n:nat), 0 < x -> 0 < x ^ n.
Proof.
- intros x n; elim n; simpl in |- *; auto with real.
+ intros x n; elim n; simpl; auto with real.
intros n0 H' H'0; replace 0 with (x * 0); auto with real.
Qed.
Hint Resolve pow_lt: real.
Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n.
Proof.
- intros x n; elim n; simpl in |- *; auto with real.
+ intros x n; elim n; simpl; auto with real.
intros H' H'0; exfalso; omega.
intros n0; case n0.
- simpl in |- *; rewrite Rmult_1_r; auto.
+ simpl; rewrite Rmult_1_r; auto.
intros n1 H' H'0 H'1.
replace 1 with (1 * 1); auto with real.
apply Rlt_trans with (r2 := x * 1); auto with real.
@@ -129,7 +127,7 @@ Lemma Rlt_pow : forall (x:R) (n m:nat), 1 < x -> (n < m)%nat -> x ^ n < x ^ m.
Proof.
intros x n m H' H'0; replace m with (m - n + n)%nat.
rewrite pow_add.
- pattern (x ^ n) at 1 in |- *; replace (x ^ n) with (1 * x ^ n);
+ pattern (x ^ n) at 1; replace (x ^ n) with (1 * x ^ n);
auto with real.
apply Rminus_lt.
repeat rewrite (fun y:R => Rmult_comm y (x ^ n));
@@ -149,14 +147,14 @@ Hint Resolve Rlt_pow: real.
(*********)
Lemma tech_pow_Rmult : forall (x:R) (n:nat), x * x ^ n = x ^ S n.
Proof.
- simple induction n; simpl in |- *; trivial.
+ simple induction n; simpl; trivial.
Qed.
(*********)
Lemma tech_pow_Rplus :
forall (x:R) (a n:nat), x ^ a + INR n * x ^ a = INR (S n) * x ^ a.
Proof.
- intros; pattern (x ^ a) at 1 in |- *;
+ intros; pattern (x ^ a) at 1;
rewrite <- (let (H1, H2) := Rmult_ne (x ^ a) in H1);
rewrite (Rmult_comm (INR n) (x ^ a));
rewrite <- (Rmult_plus_distr_l (x ^ a) 1 (INR n));
@@ -167,29 +165,29 @@ Qed.
Lemma poly : forall (n:nat) (x:R), 0 < x -> 1 + INR n * x <= (1 + x) ^ n.
Proof.
intros; elim n.
- simpl in |- *; cut (1 + 0 * x = 1).
- intro; rewrite H0; unfold Rle in |- *; right; reflexivity.
+ simpl; cut (1 + 0 * x = 1).
+ intro; rewrite H0; unfold Rle; right; reflexivity.
ring.
- intros; unfold pow in |- *; fold pow in |- *;
+ intros; unfold pow; fold pow;
apply
(Rle_trans (1 + INR (S n0) * x) ((1 + x) * (1 + INR n0 * x))
((1 + x) * (1 + x) ^ n0)).
cut ((1 + x) * (1 + INR n0 * x) = 1 + INR (S n0) * x + INR n0 * (x * x)).
- intro; rewrite H1; pattern (1 + INR (S n0) * x) at 1 in |- *;
+ intro; rewrite H1; pattern (1 + INR (S n0) * x) at 1;
rewrite <- (let (H1, H2) := Rplus_ne (1 + INR (S n0) * x) in H1);
apply Rplus_le_compat_l; elim n0; intros.
- simpl in |- *; rewrite Rmult_0_l; unfold Rle in |- *; right; auto.
- unfold Rle in |- *; left; generalize Rmult_gt_0_compat; unfold Rgt in |- *;
- intro; fold (Rsqr x) in |- *;
+ simpl; rewrite Rmult_0_l; unfold Rle; right; auto.
+ unfold Rle; left; generalize Rmult_gt_0_compat; unfold Rgt;
+ intro; fold (Rsqr x);
apply (H3 (INR (S n1)) (Rsqr x) (lt_INR_0 (S n1) (lt_O_Sn n1)));
fold (x > 0) in H;
apply (Rlt_0_sqr x (Rlt_dichotomy_converse x 0 (or_intror (x < 0) H))).
rewrite (S_INR n0); ring.
unfold Rle in H0; elim H0; intro.
- unfold Rle in |- *; left; apply Rmult_lt_compat_l.
+ unfold Rle; left; apply Rmult_lt_compat_l.
rewrite Rplus_comm; apply (Rle_lt_0_plus_1 x (Rlt_le 0 x H)).
assumption.
- rewrite H1; unfold Rle in |- *; right; trivial.
+ rewrite H1; unfold Rle; right; trivial.
Qed.
Lemma Power_monotonic :
@@ -197,12 +195,12 @@ Lemma Power_monotonic :
Rabs x > 1 -> (m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n).
Proof.
intros x m n H; induction n as [| n Hrecn]; intros; inversion H0.
- unfold Rle in |- *; right; reflexivity.
- unfold Rle in |- *; right; reflexivity.
+ unfold Rle; right; reflexivity.
+ unfold Rle; right; reflexivity.
apply (Rle_trans (Rabs (x ^ m)) (Rabs (x ^ n)) (Rabs (x ^ S n))).
apply Hrecn; assumption.
- simpl in |- *; rewrite Rabs_mult.
- pattern (Rabs (x ^ n)) at 1 in |- *.
+ simpl; rewrite Rabs_mult.
+ pattern (Rabs (x ^ n)) at 1.
rewrite <- Rmult_1_r.
rewrite (Rmult_comm (Rabs x) (Rabs (x ^ n))).
apply Rmult_le_compat_l.
@@ -213,7 +211,7 @@ Qed.
Lemma RPow_abs : forall (x:R) (n:nat), Rabs x ^ n = Rabs (x ^ n).
Proof.
- intro; simple induction n; simpl in |- *.
+ intro; simple induction n; simpl.
apply sym_eq; apply Rabs_pos_eq; apply Rlt_le; apply Rlt_0_1.
intros; rewrite H; apply sym_eq; apply Rabs_mult.
Qed.
@@ -233,16 +231,16 @@ Proof.
rewrite <- RPow_abs; cut (Rabs x = 1 + (Rabs x - 1)).
intro; rewrite H3;
apply (Rge_trans ((1 + (Rabs x - 1)) ^ x0) (1 + INR x0 * (Rabs x - 1)) b).
- apply Rle_ge; apply poly; fold (Rabs x - 1 > 0) in |- *; apply Rgt_minus;
+ apply Rle_ge; apply poly; fold (Rabs x - 1 > 0); apply Rgt_minus;
assumption.
apply (Rge_trans (1 + INR x0 * (Rabs x - 1)) (INR x0 * (Rabs x - 1)) b).
apply Rle_ge; apply Rlt_le; rewrite (Rplus_comm 1 (INR x0 * (Rabs x - 1)));
- pattern (INR x0 * (Rabs x - 1)) at 1 in |- *;
+ pattern (INR x0 * (Rabs x - 1)) at 1;
rewrite <- (let (H1, H2) := Rplus_ne (INR x0 * (Rabs x - 1)) in H1);
apply Rplus_lt_compat_l; apply Rlt_0_1.
cut (b = b * / (Rabs x - 1) * (Rabs x - 1)).
intros; rewrite H4; apply Rmult_ge_compat_r.
- apply Rge_minus; unfold Rge in |- *; left; assumption.
+ apply Rge_minus; unfold Rge; left; assumption.
assumption.
rewrite Rmult_assoc; rewrite Rinv_l.
ring.
@@ -254,26 +252,26 @@ Proof.
apply
(Rge_trans (INR x0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))).
rewrite INR_IZR_INZ; apply IZR_ge; omega.
- unfold Rge in |- *; left; assumption.
+ unfold Rge; left; assumption.
exists 0%nat;
apply
(Rge_trans (INR 0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))).
- rewrite INR_IZR_INZ; apply IZR_ge; simpl in |- *; omega.
- unfold Rge in |- *; left; assumption.
+ rewrite INR_IZR_INZ; apply IZR_ge; simpl; omega.
+ unfold Rge; left; assumption.
omega.
Qed.
Lemma pow_ne_zero : forall n:nat, n <> 0%nat -> 0 ^ n = 0.
Proof.
simple induction n.
- simpl in |- *; auto.
+ simpl; auto.
intros; elim H; reflexivity.
- intros; simpl in |- *; apply Rmult_0_l.
+ intros; simpl; apply Rmult_0_l.
Qed.
Lemma Rinv_pow : forall (x:R) (n:nat), x <> 0 -> / x ^ n = (/ x) ^ n.
Proof.
- intros; elim n; simpl in |- *.
+ intros; elim n; simpl.
apply Rinv_1.
intro m; intro; rewrite Rinv_mult_distr.
rewrite H0; reflexivity; assumption.
@@ -307,7 +305,7 @@ Proof.
rewrite <- Rabs_Rinv.
rewrite Rinv_pow.
apply (Rlt_le_trans (/ y) (/ y + 1) (Rabs ((/ x) ^ n))).
- pattern (/ y) at 1 in |- *.
+ pattern (/ y) at 1.
rewrite <- (let (H1, H2) := Rplus_ne (/ y) in H1).
apply Rplus_lt_compat_l.
apply Rlt_0_1.
@@ -321,17 +319,17 @@ Proof.
apply pow_nonzero.
assumption.
apply Rlt_dichotomy_converse.
- right; unfold Rgt in |- *; assumption.
+ right; unfold Rgt; assumption.
rewrite <- (Rinv_involutive 1).
rewrite Rabs_Rinv.
- unfold Rgt in |- *; apply Rinv_lt_contravar.
+ unfold Rgt; apply Rinv_lt_contravar.
apply Rmult_lt_0_compat.
apply Rabs_pos_lt.
assumption.
rewrite Rinv_1; apply Rlt_0_1.
rewrite Rinv_1; assumption.
assumption.
- red in |- *; intro; apply R1_neq_R0; assumption.
+ red; intro; apply R1_neq_R0; assumption.
Qed.
Lemma pow_R1 : forall (r:R) (n:nat), r ^ n = 1 -> Rabs r = 1 \/ n = 0%nat.
@@ -345,7 +343,7 @@ Proof.
cut (Rabs r <> 0); [ intros Eq2 | apply Rabs_no_R0 ]; auto.
absurd (Rabs (/ r) ^ 0 < Rabs (/ r) ^ S n0); auto.
replace (Rabs (/ r) ^ S n0) with 1.
- simpl in |- *; apply Rlt_irrefl; auto.
+ simpl; apply Rlt_irrefl; auto.
rewrite Rabs_Rinv; auto.
rewrite <- Rinv_pow; auto.
rewrite RPow_abs; auto.
@@ -356,16 +354,16 @@ Proof.
case (Rabs_pos r); auto.
intros H'3; case Eq2; auto.
rewrite Rmult_1_r; rewrite Rinv_r; auto with real.
- red in |- *; intro; absurd (r ^ S n0 = 1); auto.
- simpl in |- *; rewrite H; rewrite Rmult_0_l; auto with real.
+ red; intro; absurd (r ^ S n0 = 1); auto.
+ simpl; rewrite H; rewrite Rmult_0_l; auto with real.
generalize H'; case n; auto.
intros n0 H'0.
cut (r <> 0); [ intros Eq1 | auto with real ].
cut (Rabs r <> 0); [ intros Eq2 | apply Rabs_no_R0 ]; auto.
absurd (Rabs r ^ 0 < Rabs r ^ S n0); auto with real arith.
- repeat rewrite RPow_abs; rewrite H'0; simpl in |- *; auto with real.
- red in |- *; intro; absurd (r ^ S n0 = 1); auto.
- simpl in |- *; rewrite H; rewrite Rmult_0_l; auto with real.
+ repeat rewrite RPow_abs; rewrite H'0; simpl; auto with real.
+ red; intro; absurd (r ^ S n0 = 1); auto.
+ simpl; rewrite H; rewrite Rmult_0_l; auto with real.
Qed.
Lemma pow_Rsqr : forall (x:R) (n:nat), x ^ (2 * n) = Rsqr x ^ n.
@@ -375,15 +373,15 @@ Proof.
replace (2 * S n)%nat with (S (S (2 * n))).
replace (x ^ S (S (2 * n))) with (x * x * x ^ (2 * n)).
rewrite Hrecn; reflexivity.
- simpl in |- *; ring.
+ simpl; ring.
ring.
Qed.
Lemma pow_le : forall (a:R) (n:nat), 0 <= a -> 0 <= a ^ n.
Proof.
intros; induction n as [| n Hrecn].
- simpl in |- *; left; apply Rlt_0_1.
- simpl in |- *; apply Rmult_le_pos; assumption.
+ simpl; left; apply Rlt_0_1.
+ simpl; apply Rmult_le_pos; assumption.
Qed.
(**********)
@@ -392,36 +390,36 @@ Proof.
intro; induction n as [| n Hrecn].
reflexivity.
replace (2 * S n)%nat with (2 + 2 * n)%nat by ring.
- rewrite pow_add; rewrite Hrecn; simpl in |- *; ring.
+ rewrite pow_add; rewrite Hrecn; simpl; ring.
Qed.
(**********)
Lemma pow_1_odd : forall n:nat, (-1) ^ S (2 * n) = -1.
Proof.
intro; replace (S (2 * n)) with (2 * n + 1)%nat by ring.
- rewrite pow_add; rewrite pow_1_even; simpl in |- *; ring.
+ rewrite pow_add; rewrite pow_1_even; simpl; ring.
Qed.
(**********)
Lemma pow_1_abs : forall n:nat, Rabs ((-1) ^ n) = 1.
Proof.
intro; induction n as [| n Hrecn].
- simpl in |- *; apply Rabs_R1.
+ simpl; apply Rabs_R1.
replace (S n) with (n + 1)%nat; [ rewrite pow_add | ring ].
rewrite Rabs_mult.
- rewrite Hrecn; rewrite Rmult_1_l; simpl in |- *; rewrite Rmult_1_r;
+ rewrite Hrecn; rewrite Rmult_1_l; simpl; rewrite Rmult_1_r;
rewrite Rabs_Ropp; apply Rabs_R1.
Qed.
Lemma pow_mult : forall (x:R) (n1 n2:nat), x ^ (n1 * n2) = (x ^ n1) ^ n2.
Proof.
intros; induction n2 as [| n2 Hrecn2].
- simpl in |- *; replace (n1 * 0)%nat with 0%nat; [ reflexivity | ring ].
+ simpl; replace (n1 * 0)%nat with 0%nat; [ reflexivity | ring ].
replace (n1 * S n2)%nat with (n1 * n2 + n1)%nat.
replace (S n2) with (n2 + 1)%nat by ring.
do 2 rewrite pow_add.
rewrite Hrecn2.
- simpl in |- *.
+ simpl.
ring.
ring.
Qed.
@@ -431,7 +429,7 @@ Proof.
intros.
induction n as [| n Hrecn].
right; reflexivity.
- simpl in |- *.
+ simpl.
elim H; intros.
apply Rle_trans with (y * x ^ n).
do 2 rewrite <- (Rmult_comm (x ^ n)).
@@ -448,7 +446,7 @@ Proof.
intros.
induction k as [| k Hreck].
right; reflexivity.
- simpl in |- *.
+ simpl.
apply Rle_trans with (x * 1).
rewrite Rmult_1_r; assumption.
apply Rmult_le_compat_l.
@@ -463,33 +461,33 @@ Proof.
replace n with (n - m + m)%nat.
rewrite pow_add.
rewrite Rmult_comm.
- pattern (x ^ m) at 1 in |- *; rewrite <- Rmult_1_r.
+ pattern (x ^ m) at 1; rewrite <- Rmult_1_r.
apply Rmult_le_compat_l.
apply pow_le; left; apply Rlt_le_trans with 1; [ apply Rlt_0_1 | assumption ].
apply pow_R1_Rle; assumption.
rewrite plus_comm.
- symmetry in |- *; apply le_plus_minus; assumption.
+ symmetry ; apply le_plus_minus; assumption.
Qed.
Lemma pow1 : forall n:nat, 1 ^ n = 1.
Proof.
intro; induction n as [| n Hrecn].
reflexivity.
- simpl in |- *; rewrite Hrecn; rewrite Rmult_1_r; reflexivity.
+ simpl; rewrite Hrecn; rewrite Rmult_1_r; reflexivity.
Qed.
Lemma pow_Rabs : forall (x:R) (n:nat), x ^ n <= Rabs x ^ n.
Proof.
intros; induction n as [| n Hrecn].
right; reflexivity.
- simpl in |- *; case (Rcase_abs x); intro.
+ simpl; case (Rcase_abs x); intro.
apply Rle_trans with (Rabs (x * x ^ n)).
apply RRle_abs.
rewrite Rabs_mult.
apply Rmult_le_compat_l.
apply Rabs_pos.
- right; symmetry in |- *; apply RPow_abs.
- pattern (Rabs x) at 1 in |- *; rewrite (Rabs_right x r);
+ right; symmetry ; apply RPow_abs.
+ pattern (Rabs x) at 1; rewrite (Rabs_right x r);
apply Rmult_le_compat_l.
apply Rge_le; exact r.
apply Hrecn.
@@ -502,7 +500,7 @@ Proof.
apply pow_Rabs.
induction n as [| n Hrecn].
right; reflexivity.
- simpl in |- *; apply Rle_trans with (x * Rabs y ^ n).
+ simpl; apply Rle_trans with (x * Rabs y ^ n).
do 2 rewrite <- (Rmult_comm (Rabs y ^ n)).
apply Rmult_le_compat_l.
apply pow_le; apply Rabs_pos.
@@ -519,7 +517,7 @@ Qed.
(*i Due to L.Thery i*)
Ltac case_eq name :=
- generalize (refl_equal name); pattern name at -1 in |- *; case name.
+ generalize (refl_equal name); pattern name at -1; case name.
Definition powerRZ (x:R) (n:Z) :=
match n with
@@ -533,7 +531,7 @@ Infix Local "^Z" := powerRZ (at level 30, right associativity) : R_scope.
Lemma Zpower_NR0 :
forall (x:Z) (n:nat), (0 <= x)%Z -> (0 <= Zpower_nat x n)%Z.
Proof.
- induction n; unfold Zpower_nat in |- *; simpl in |- *; auto with zarith.
+ induction n; unfold Zpower_nat; simpl; auto with zarith.
Qed.
Lemma powerRZ_O : forall x:R, x ^Z 0 = 1.
@@ -543,60 +541,47 @@ Qed.
Lemma powerRZ_1 : forall x:R, x ^Z Zsucc 0 = x.
Proof.
- simpl in |- *; auto with real.
+ simpl; auto with real.
Qed.
Lemma powerRZ_NOR : forall (x:R) (z:Z), x <> 0 -> x ^Z z <> 0.
Proof.
- destruct z; simpl in |- *; auto with real.
+ destruct z; simpl; auto with real.
Qed.
Lemma powerRZ_add :
forall (x:R) (n m:Z), x <> 0 -> x ^Z (n + m) = x ^Z n * x ^Z m.
Proof.
- intro x; destruct n as [| n1| n1]; destruct m as [| m1| m1]; simpl in |- *;
+ intro x; destruct n as [| n1| n1]; destruct m as [| m1| m1]; simpl;
auto with real.
(* POS/POS *)
- rewrite nat_of_P_plus_morphism; auto with real.
+ rewrite Pplus_plus; auto with real.
(* POS/NEG *)
- case_eq ((n1 ?= m1)%positive Datatypes.Eq); simpl in |- *; auto with real.
- intros H' H'0; rewrite Pcompare_Eq_eq with (1 := H'); auto with real.
- intros H' H'0; rewrite (nat_of_P_minus_morphism m1 n1); auto with real.
- rewrite (pow_RN_plus x (nat_of_P m1 - nat_of_P n1) (nat_of_P n1));
- auto with real.
- rewrite plus_comm; rewrite le_plus_minus_r; auto with real.
- rewrite Rinv_mult_distr; auto with real.
- rewrite Rinv_involutive; auto with real.
- apply lt_le_weak.
- apply nat_of_P_lt_Lt_compare_morphism; auto.
- apply ZC2; auto.
- intros H' H'0; rewrite (nat_of_P_minus_morphism n1 m1); auto with real.
- rewrite (pow_RN_plus x (nat_of_P n1 - nat_of_P m1) (nat_of_P m1));
- auto with real.
- rewrite plus_comm; rewrite le_plus_minus_r; auto with real.
- apply lt_le_weak.
- change (nat_of_P n1 > nat_of_P m1)%nat in |- *.
- apply nat_of_P_gt_Gt_compare_morphism; auto.
+ rewrite Z.pos_sub_spec.
+ case Pcompare_spec; intros; simpl.
+ subst; auto with real.
+ rewrite Pminus_minus by trivial.
+ rewrite (pow_RN_plus x _ (nat_of_P n1)) by auto with real.
+ rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
+ rewrite Rinv_mult_distr, Rinv_involutive; auto with real.
+ rewrite Pminus_minus by trivial.
+ rewrite (pow_RN_plus x _ (nat_of_P m1)) by auto with real.
+ rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
+ reflexivity.
(* NEG/POS *)
- case_eq ((n1 ?= m1)%positive Datatypes.Eq); simpl in |- *; auto with real.
- intros H' H'0; rewrite Pcompare_Eq_eq with (1 := H'); auto with real.
- intros H' H'0; rewrite (nat_of_P_minus_morphism m1 n1); auto with real.
- rewrite (pow_RN_plus x (nat_of_P m1 - nat_of_P n1) (nat_of_P n1));
- auto with real.
- rewrite plus_comm; rewrite le_plus_minus_r; auto with real.
- apply lt_le_weak.
- apply nat_of_P_lt_Lt_compare_morphism; auto.
- apply ZC2; auto.
- intros H' H'0; rewrite (nat_of_P_minus_morphism n1 m1); auto with real.
- rewrite (pow_RN_plus x (nat_of_P n1 - nat_of_P m1) (nat_of_P m1));
- auto with real.
- rewrite plus_comm; rewrite le_plus_minus_r; auto with real.
- rewrite Rinv_mult_distr; auto with real.
- apply lt_le_weak.
- change (nat_of_P n1 > nat_of_P m1)%nat in |- *.
- apply nat_of_P_gt_Gt_compare_morphism; auto.
+ rewrite Z.pos_sub_spec.
+ case Pcompare_spec; intros; simpl.
+ subst; auto with real.
+ rewrite Pminus_minus by trivial.
+ rewrite (pow_RN_plus x _ (nat_of_P m1)) by auto with real.
+ rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
+ rewrite Rinv_mult_distr, Rinv_involutive; auto with real.
+ rewrite Pminus_minus by trivial.
+ rewrite (pow_RN_plus x _ (nat_of_P n1)) by auto with real.
+ rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt).
+ auto with real.
(* NEG/NEG *)
- rewrite nat_of_P_plus_morphism; auto with real.
+ rewrite Pplus_plus; auto with real.
intros H'; rewrite pow_add; auto with real.
apply Rinv_mult_distr; auto.
apply pow_nonzero; auto.
@@ -607,16 +592,16 @@ Hint Resolve powerRZ_O powerRZ_1 powerRZ_NOR powerRZ_add: real.
Lemma Zpower_nat_powerRZ :
forall n m:nat, IZR (Zpower_nat (Z_of_nat n) m) = INR n ^Z Z_of_nat m.
Proof.
- intros n m; elim m; simpl in |- *; auto with real.
- intros m1 H'; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; simpl in |- *.
+ intros n m; elim m; simpl; auto with real.
+ intros m1 H'; rewrite nat_of_P_of_succ_nat; simpl.
replace (Zpower_nat (Z_of_nat n) (S m1)) with
(Z_of_nat n * Zpower_nat (Z_of_nat n) m1)%Z.
rewrite mult_IZR; auto with real.
- repeat rewrite <- INR_IZR_INZ; simpl in |- *.
- rewrite H'; simpl in |- *.
- case m1; simpl in |- *; auto with real.
- intros m2; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto.
- unfold Zpower_nat in |- *; auto.
+ repeat rewrite <- INR_IZR_INZ; simpl.
+ rewrite H'; simpl.
+ case m1; simpl; auto with real.
+ intros m2; rewrite nat_of_P_of_succ_nat; auto.
+ unfold Zpower_nat; auto.
Qed.
Lemma Zpower_pos_powerRZ :
@@ -633,7 +618,7 @@ Qed.
Lemma powerRZ_lt : forall (x:R) (z:Z), 0 < x -> 0 < x ^Z z.
Proof.
- intros x z; case z; simpl in |- *; auto with real.
+ intros x z; case z; simpl; auto with real.
Qed.
Hint Resolve powerRZ_lt: real.
@@ -646,19 +631,19 @@ Hint Resolve powerRZ_le: real.
Lemma Zpower_nat_powerRZ_absolu :
forall n m:Z, (0 <= m)%Z -> IZR (Zpower_nat n (Zabs_nat m)) = IZR n ^Z m.
Proof.
- intros n m; case m; simpl in |- *; auto with zarith.
- intros p H'; elim (nat_of_P p); simpl in |- *; auto with zarith.
- intros n0 H'0; rewrite <- H'0; simpl in |- *; auto with zarith.
+ intros n m; case m; simpl; auto with zarith.
+ intros p H'; elim (nat_of_P p); simpl; auto with zarith.
+ intros n0 H'0; rewrite <- H'0; simpl; auto with zarith.
rewrite <- mult_IZR; auto.
intros p H'; absurd (0 <= Zneg p)%Z; auto with zarith.
Qed.
Lemma powerRZ_R1 : forall n:Z, 1 ^Z n = 1.
Proof.
- intros n; case n; simpl in |- *; auto.
- intros p; elim (nat_of_P p); simpl in |- *; auto; intros n0 H'; rewrite H';
+ intros n; case n; simpl; auto.
+ intros p; elim (nat_of_P p); simpl; auto; intros n0 H'; rewrite H';
ring.
- intros p; elim (nat_of_P p); simpl in |- *.
+ intros p; elim (nat_of_P p); simpl.
exact Rinv_1.
intros n1 H'; rewrite Rinv_mult_distr; try rewrite Rinv_1; try rewrite H';
auto with real.
@@ -676,7 +661,7 @@ Definition decimal_exp (r:R) (z:Z) : R := (r * 10 ^Z z).
(** * Sum of n first naturals *)
(*******************************)
(*********)
-Boxed Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) : nat :=
+Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) : nat :=
match n with
| O => f 0%nat
| S n' => (sum_nat_f_O f n' + f (S n'))%nat
@@ -710,10 +695,10 @@ Lemma GP_finite :
forall (x:R) (n:nat),
sum_f_R0 (fun n:nat => x ^ n) n * (x - 1) = x ^ (n + 1) - 1.
Proof.
- intros; induction n as [| n Hrecn]; simpl in |- *.
+ intros; induction n as [| n Hrecn]; simpl.
ring.
rewrite Rmult_plus_distr_r; rewrite Hrecn; cut ((n + 1)%nat = S n).
- intro H; rewrite H; simpl in |- *; ring.
+ intro H; rewrite H; simpl; ring.
omega.
Qed.
@@ -721,8 +706,8 @@ Lemma sum_f_R0_triangle :
forall (x:nat -> R) (n:nat),
Rabs (sum_f_R0 x n) <= sum_f_R0 (fun i:nat => Rabs (x i)) n.
Proof.
- intro; simple induction n; simpl in |- *.
- unfold Rle in |- *; right; reflexivity.
+ intro; simple induction n; simpl.
+ unfold Rle; right; reflexivity.
intro m; intro;
apply
(Rle_trans (Rabs (sum_f_R0 x m + x (S m)))
@@ -744,16 +729,16 @@ Definition R_dist (x y:R) : R := Rabs (x - y).
(*********)
Lemma R_dist_pos : forall x y:R, R_dist x y >= 0.
Proof.
- intros; unfold R_dist in |- *; unfold Rabs in |- *; case (Rcase_abs (x - y));
+ intros; unfold R_dist; unfold Rabs; case (Rcase_abs (x - y));
intro l.
- unfold Rge in |- *; left; apply (Ropp_gt_lt_0_contravar (x - y) l).
+ unfold Rge; left; apply (Ropp_gt_lt_0_contravar (x - y) l).
trivial.
Qed.
(*********)
Lemma R_dist_sym : forall x y:R, R_dist x y = R_dist y x.
Proof.
- unfold R_dist in |- *; intros; split_Rabs; try ring.
+ unfold R_dist; intros; split_Rabs; try ring.
generalize (Ropp_gt_lt_0_contravar (y - x) r); intro;
rewrite (Ropp_minus_distr y x) in H; generalize (Rlt_asym (x - y) 0 r0);
intro; unfold Rgt in H; exfalso; auto.
@@ -765,7 +750,7 @@ Qed.
(*********)
Lemma R_dist_refl : forall x y:R, R_dist x y = 0 <-> x = y.
Proof.
- unfold R_dist in |- *; intros; split_Rabs; split; intros.
+ unfold R_dist; intros; split_Rabs; split; intros.
rewrite (Ropp_minus_distr x y) in H; apply sym_eq;
apply (Rminus_diag_uniq y x H).
rewrite (Ropp_minus_distr x y); generalize (sym_eq H); intro;
@@ -776,13 +761,13 @@ Qed.
Lemma R_dist_eq : forall x:R, R_dist x x = 0.
Proof.
- unfold R_dist in |- *; intros; split_Rabs; intros; ring.
+ unfold R_dist; intros; split_Rabs; intros; ring.
Qed.
(***********)
Lemma R_dist_tri : forall x y z:R, R_dist x y <= R_dist x z + R_dist z y.
Proof.
- intros; unfold R_dist in |- *; replace (x - y) with (x - z + (z - y));
+ intros; unfold R_dist; replace (x - y) with (x - z + (z - y));
[ apply (Rabs_triang (x - z) (z - y)) | ring ].
Qed.
@@ -790,7 +775,7 @@ Qed.
Lemma R_dist_plus :
forall a b c d:R, R_dist (a + c) (b + d) <= R_dist a b + R_dist c d.
Proof.
- intros; unfold R_dist in |- *;
+ intros; unfold R_dist;
replace (a + c - (b + d)) with (a - b + (c - d)).
exact (Rabs_triang (a - b) (c - d)).
ring.
diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v
index 3ab2bc73..bda64e77 100644
--- a/theories/Reals/Rgeom.v
+++ b/theories/Reals/Rgeom.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rgeom.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 598f5f31..8acfd75b 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -1,14 +1,12 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: RiemannInt.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Ranalysis.
@@ -2242,7 +2240,7 @@ Proof.
unfold RiemannInt_SF in |- *; case (Rle_dec a b); intro.
eapply StepFun_P17.
apply StepFun_P1.
- simpl in |- *; apply StepFun_P1.
+ simpl in |- *; apply StepFun_P1.
apply Ropp_eq_compat; eapply StepFun_P17.
apply StepFun_P1.
simpl in |- *; apply StepFun_P1.
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index d0d9519c..d16e7f2c 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: RiemannInt_SF.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis.
@@ -149,7 +147,7 @@ Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist :=
| existT a b => a
end.
-Boxed Fixpoint Int_SF (l k:Rlist) : R :=
+Fixpoint Int_SF (l k:Rlist) : R :=
match l with
| nil => 0
| cons a l' =>
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index d2d935b7..5c864de3 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rlimit.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(*********************************************************)
(** Definition of the limit *)
(* *)
@@ -15,7 +13,6 @@
Require Import Rbase.
Require Import Rfunctions.
-Require Import Classical_Prop.
Require Import Fourier.
Open Local Scope R_scope.
diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v
index b7ffec2b..2237ea6e 100644
--- a/theories/Reals/Rlogic.v
+++ b/theories/Reals/Rlogic.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -41,6 +41,7 @@ Variable P : nat -> Prop.
Hypothesis HP : forall n, {P n} + {~P n}.
Let ge_fun_sums_ge_lemma : (forall (m n : nat) (f : nat -> R), (lt m n) -> (forall i : nat, 0 <= f i) -> sum_f_R0 f m <= sum_f_R0 f n).
+Proof.
intros m n f mn fpos.
replace (sum_f_R0 f m) with (sum_f_R0 f m + 0) by ring.
rewrite (tech2 f m n mn).
@@ -52,6 +53,7 @@ apply (Rplus_le_compat _ _ _ _ IHn0 (fpos (S (m + S n0)%nat))).
Qed.
Let ge_fun_sums_ge : (forall (m n : nat) (f : nat -> R), (le m n) -> (forall i : nat, 0 <= f i) -> sum_f_R0 f m <= sum_f_R0 f n).
+Proof.
intros m n f mn pos.
elim (le_lt_or_eq _ _ mn).
intro; apply ge_fun_sums_ge_lemma; assumption.
@@ -61,6 +63,7 @@ Qed.
Let f:=fun n => (if HP n then (1/2)^n else 0)%R.
Lemma cauchy_crit_geometric_dec_fun : Cauchy_crit_series f.
+Proof.
intros e He.
assert (X:(Pser (fun n:nat => 1) (1/2) (/ (1 - (1/2))))%R).
apply GP_infinite.
@@ -233,10 +236,11 @@ fourier.
Qed.
Lemma sig_forall_dec : {n | ~P n}+{forall n, P n}.
+Proof.
destruct forall_dec.
right; assumption.
left.
-apply constructive_indefinite_description_nat; auto.
+apply constructive_indefinite_ground_description_nat; auto.
clear - HP.
firstorder.
apply Classical_Pred_Type.not_all_ex_not.
@@ -255,6 +259,7 @@ principle also derive [up] and its [specification] *)
Theorem not_not_archimedean :
forall r : R, ~ (forall n : nat, (INR n <= r)%R).
+Proof.
intros r H.
set (E := fun r => exists n : nat, r = INR n).
assert (exists x : R, E x) by
diff --git a/theories/Reals/Rminmax.v b/theories/Reals/Rminmax.v
index c9faee0c..8f8207d7 100644
--- a/theories/Reals/Rminmax.v
+++ b/theories/Reals/Rminmax.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v
index 4f7a8d22..026153b7 100644
--- a/theories/Reals/Rpow_def.v
+++ b/theories/Reals/Rpow_def.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Rpow_def.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
Require Import Rdefinitions.
Fixpoint pow (r:R) (n:nat) : R :=
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index 36db12f9..593e54c6 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -1,12 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rpower.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*i Due to L.Thery i*)
(************************************************************)
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index 947dbb11..12258d6b 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rprod.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Compare.
Require Import Rbase.
Require Import Rfunctions.
@@ -17,7 +15,7 @@ Require Import Binomial.
Open Local Scope R_scope.
(** TT Ak; 0<=k<=N *)
-Boxed Fixpoint prod_f_R0 (f:nat -> R) (N:nat) : R :=
+Fixpoint prod_f_R0 (f:nat -> R) (N:nat) : R :=
match N with
| O => f O
| S p => prod_f_R0 f p * f (S p)
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index db0fddad..479d381d 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -1,16 +1,13 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rseries.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
-Require Import Classical.
Require Import Compare.
Open Local Scope R_scope.
@@ -28,7 +25,7 @@ Section sequence.
Variable Un : nat -> R.
(*********)
- Boxed Fixpoint Rmax_N (N:nat) : R :=
+ Fixpoint Rmax_N (N:nat) : R :=
match N with
| O => Un 0
| S n => Rmax (Un (S n)) (Rmax_N n)
@@ -100,47 +97,173 @@ Section sequence.
(Rle_ge (Un n1) (Un (S n1)) (H1 n1)) H3).
Qed.
+(*********)
+ Lemma Un_cv_crit_lub : Un_growing -> forall l, is_lub EUn l -> Un_cv l.
+ Proof.
+ intros Hug l H eps Heps.
+
+ cut (exists N, Un N > l - eps).
+ intros (N, H3).
+ exists N.
+ intros n H4.
+ unfold R_dist.
+ rewrite Rabs_left1, Ropp_minus_distr.
+ apply Rplus_lt_reg_r with (Un n - eps).
+ apply Rlt_le_trans with (Un N).
+ now replace (Un n - eps + (l - Un n)) with (l - eps) by ring.
+ replace (Un n - eps + eps) with (Un n) by ring.
+ apply Rge_le.
+ now apply growing_prop.
+ apply Rle_minus.
+ apply (proj1 H).
+ now exists n.
+
+ assert (Hi2pn: forall n, 0 < (/ 2)^n).
+ clear. intros n.
+ apply pow_lt.
+ apply Rinv_0_lt_compat.
+ now apply (IZR_lt 0 2).
+
+ pose (test := fun n => match Rle_lt_dec (Un n) (l - eps) with left _ => false | right _ => true end).
+ pose (sum := let fix aux n := match n with S n' => aux n' +
+ if test n' then (/ 2)^n else 0 | O => 0 end in aux).
+
+ assert (Hsum': forall m n, sum m <= sum (m + n)%nat <= sum m + (/2)^m - (/2)^(m + n)).
+ clearbody test.
+ clear -Hi2pn.
+ intros m.
+ induction n.
+ rewrite<- plus_n_O.
+ ring_simplify (sum m + (/ 2) ^ m - (/ 2) ^ m).
+ split ; apply Rle_refl.
+ rewrite <- plus_n_Sm.
+ simpl.
+ split.
+ apply Rle_trans with (sum (m + n)%nat + 0).
+ rewrite Rplus_0_r.
+ apply IHn.
+ apply Rplus_le_compat_l.
+ case (test (m + n)%nat).
+ apply Rlt_le.
+ exact (Hi2pn (S (m + n))).
+ apply Rle_refl.
+ apply Rle_trans with (sum (m + n)%nat + / 2 * (/ 2) ^ (m + n)).
+ apply Rplus_le_compat_l.
+ case (test (m + n)%nat).
+ apply Rle_refl.
+ apply Rlt_le.
+ exact (Hi2pn (S (m + n))).
+ apply Rplus_le_reg_r with (-(/ 2 * (/ 2) ^ (m + n))).
+ rewrite Rplus_assoc, Rplus_opp_r, Rplus_0_r.
+ apply Rle_trans with (1 := proj2 IHn).
+ apply Req_le.
+ field.
+
+ assert (Hsum: forall n, 0 <= sum n <= 1 - (/2)^n).
+ intros N.
+ generalize (Hsum' O N).
+ simpl.
+ now rewrite Rplus_0_l.
+
+ destruct (completeness (fun x : R => exists n : nat, x = sum n)) as (m, (Hm1, Hm2)).
+ exists 1.
+ intros x (n, H1).
+ rewrite H1.
+ apply Rle_trans with (1 := proj2 (Hsum n)).
+ apply Rlt_le.
+ apply Rplus_lt_reg_r with ((/2)^n - 1).
+ now ring_simplify.
+ exists 0. now exists O.
+
+ destruct (Rle_or_lt m 0) as [[Hm|Hm]|Hm].
+ elim Rlt_not_le with (1 := Hm).
+ apply Hm1.
+ now exists O.
+
+ assert (Hs0: forall n, sum n = 0).
+ intros n.
+ specialize (Hm1 (sum n) (ex_intro _ _ (refl_equal _))).
+ apply Rle_antisym with (2 := proj1 (Hsum n)).
+ now rewrite <- Hm.
+
+ assert (Hub: forall n, Un n <= l - eps).
+ intros n.
+ generalize (refl_equal (sum (S n))).
+ simpl sum at 1.
+ rewrite 2!Hs0, Rplus_0_l.
+ unfold test.
+ destruct Rle_lt_dec. easy.
+ intros H'.
+ elim Rgt_not_eq with (2 := H').
+ exact (Hi2pn (S n)).
+
+ clear -Heps H Hub.
+ destruct H as (_, H).
+ refine (False_ind _ (Rle_not_lt _ _ (H (l - eps) _) _)).
+ intros x (n, H1).
+ now rewrite H1.
+ apply Rplus_lt_reg_r with (eps - l).
+ now ring_simplify.
+
+ assert (Rabs (/2) < 1).
+ rewrite Rabs_pos_eq.
+ rewrite <- Rinv_1 at 3.
+ apply Rinv_lt_contravar.
+ rewrite Rmult_1_l.
+ now apply (IZR_lt 0 2).
+ now apply (IZR_lt 1 2).
+ apply Rlt_le.
+ apply Rinv_0_lt_compat.
+ now apply (IZR_lt 0 2).
+ destruct (pow_lt_1_zero (/2) H0 m Hm) as [N H4].
+ exists N.
+ apply Rnot_le_lt.
+ intros H5.
+ apply Rlt_not_le with (1 := H4 _ (le_refl _)).
+ rewrite Rabs_pos_eq. 2: now apply Rlt_le.
+ apply Hm2.
+ intros x (n, H6).
+ rewrite H6. clear x H6.
+
+ assert (Hs: sum N = 0).
+ clear H4.
+ induction N.
+ easy.
+ simpl.
+ assert (H6: Un N <= l - eps).
+ apply Rle_trans with (2 := H5).
+ apply Rge_le.
+ apply growing_prop ; try easy.
+ apply le_n_Sn.
+ rewrite (IHN H6), Rplus_0_l.
+ unfold test.
+ destruct Rle_lt_dec.
+ apply refl_equal.
+ now elim Rlt_not_le with (1 := r).
+
+ destruct (le_or_lt N n) as [Hn|Hn].
+ rewrite le_plus_minus with (1 := Hn).
+ apply Rle_trans with (1 := proj2 (Hsum' N (n - N)%nat)).
+ rewrite Hs, Rplus_0_l.
+ set (k := (N + (n - N))%nat).
+ apply Rlt_le.
+ apply Rplus_lt_reg_r with ((/2)^k - (/2)^N).
+ now ring_simplify.
+ apply Rle_trans with (sum N).
+ rewrite le_plus_minus with (1 := Hn).
+ rewrite plus_Snm_nSm.
+ exact (proj1 (Hsum' _ _)).
+ rewrite Hs.
+ now apply Rlt_le.
+ Qed.
-(** classical is needed: [not_all_not_ex] *)
(*********)
Lemma Un_cv_crit : Un_growing -> bound EUn -> exists l : R, Un_cv l.
Proof.
- unfold Un_growing, Un_cv in |- *; intros;
- generalize (completeness_weak EUn H0 EUn_noempty);
- intro; elim H1; clear H1; intros; split with x; intros;
- unfold is_lub in H1; unfold bound in H0; unfold is_upper_bound in H0, H1;
- elim H0; clear H0; intros; elim H1; clear H1; intros;
- generalize (H3 x0 H0); intro; cut (forall n:nat, Un n <= x);
- intro.
- cut (exists N : nat, x - eps < Un N).
- intro; elim H6; clear H6; intros; split with x1.
- intros; unfold R_dist in |- *; apply (Rabs_def1 (Un n - x) eps).
- unfold Rgt in H2;
- apply (Rle_lt_trans (Un n - x) 0 eps (Rle_minus (Un n) x (H5 n)) H2).
- fold Un_growing in H; generalize (growing_prop n x1 H H7); intro;
- generalize
- (Rlt_le_trans (x - eps) (Un x1) (Un n) H6 (Rge_le (Un n) (Un x1) H8));
- intro; generalize (Rplus_lt_compat_l (- x) (x - eps) (Un n) H9);
- unfold Rminus in |- *; rewrite <- (Rplus_assoc (- x) x (- eps));
- rewrite (Rplus_comm (- x) (Un n)); fold (Un n - x) in |- *;
- rewrite Rplus_opp_l; rewrite (let (H1, H2) := Rplus_ne (- eps) in H2);
- trivial.
- cut (~ (forall N:nat, x - eps >= Un N)).
- intro; apply (not_all_not_ex nat (fun N:nat => x - eps < Un N)); red in |- *;
- intro; red in H6; elim H6; clear H6; intro;
- apply (Rnot_lt_ge (x - eps) (Un N) (H7 N)).
- red in |- *; intro; cut (forall N:nat, Un N <= x - eps).
- intro; generalize (Un_bound_imp (x - eps) H7); intro;
- unfold is_upper_bound in H8; generalize (H3 (x - eps) H8);
- intro; generalize (Rle_minus x (x - eps) H9); unfold Rminus in |- *;
- rewrite Ropp_plus_distr; rewrite <- Rplus_assoc; rewrite Rplus_opp_r;
- rewrite (let (H1, H2) := Rplus_ne (- - eps) in H2);
- rewrite Ropp_involutive; intro; unfold Rgt in H2;
- generalize (Rgt_not_le eps 0 H2); intro; auto.
- intro; elim (H6 N); intro; unfold Rle in |- *.
- left; unfold Rgt in H7; assumption.
- right; auto.
- apply (H1 (Un n) (Un_in_EUn n)).
+ intros Hug Heub.
+ exists (projT1 (completeness EUn Heub EUn_noempty)).
+ destruct (completeness EUn Heub EUn_noempty) as (l, H).
+ now apply Un_cv_crit_lub.
Qed.
(*********)
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index fad19ed2..0027c274 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rsigma.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index f2095982..7c3b4699 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rsqrt_def.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Sumbool.
Require Import Rbase.
Require Import Rfunctions.
@@ -15,7 +13,7 @@ Require Import SeqSeries.
Require Import Ranalysis1.
Open Local Scope R_scope.
-Boxed Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R :=
+Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R :=
match N with
| O => x
| S n =>
@@ -56,7 +54,7 @@ Proof.
assumption.
unfold Rdiv in |- *; apply Rmult_le_reg_l with 2.
prove_sup0.
- pattern 2 at 3 in |- *; rewrite Rmult_comm.
+ rewrite Rmult_comm.
rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ idtac | discrR ].
rewrite Rmult_1_r.
rewrite double.
@@ -95,7 +93,7 @@ Proof.
case (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2)).
unfold Rdiv in |- *; apply Rmult_le_reg_l with 2.
prove_sup0.
- pattern 2 at 3 in |- *; rewrite Rmult_comm.
+ rewrite Rmult_comm.
rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ idtac | discrR ].
rewrite Rmult_1_r.
rewrite double.
@@ -120,7 +118,7 @@ Proof.
assumption.
unfold Rdiv in |- *; apply Rmult_le_reg_l with 2.
prove_sup0.
- pattern 2 at 3 in |- *; rewrite Rmult_comm.
+ rewrite Rmult_comm.
rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ rewrite Rmult_1_r | discrR ].
rewrite double; apply Rplus_le_compat.
assumption.
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index 8e9b2bb3..f1142d24 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rtopology.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis1.
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 3499ea24..e45353b5 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rtrigo.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
@@ -18,7 +16,6 @@ Require Export Cos_rel.
Require Export Cos_plus.
Require Import ZArith_base.
Require Import Zcomplements.
-Require Import Classical_Prop.
Local Open Scope nat_scope.
Local Open Scope R_scope.
@@ -372,7 +369,11 @@ Qed.
Lemma cos_sin_0_var : forall x:R, cos x <> 0 \/ sin x <> 0.
Proof.
- intro; apply not_and_or; apply cos_sin_0.
+ intros x.
+ destruct (Req_dec (cos x) 0). 2: now left.
+ right. intros H'.
+ apply (cos_sin_0 x).
+ now split.
Qed.
(*****************************************************************)
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index de984415..3ab7d598 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rtrigo_alt.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v
index e5263f9c..587c2424 100644
--- a/theories/Reals/Rtrigo_calc.v
+++ b/theories/Reals/Rtrigo_calc.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rtrigo_calc.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
@@ -56,7 +54,7 @@ Proof with trivial.
unfold Rdiv in |- *; repeat rewrite Rmult_assoc...
rewrite <- Rinv_l_sym...
rewrite (Rmult_comm (/ 3)); repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym...
- pattern PI at 2 in |- *; rewrite (Rmult_comm PI); repeat rewrite Rmult_1_r;
+ rewrite (Rmult_comm PI); repeat rewrite Rmult_1_r;
repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym...
ring...
Qed.
@@ -73,7 +71,7 @@ Proof with trivial.
unfold Rdiv in |- *; repeat rewrite Rmult_assoc...
rewrite <- Rinv_l_sym...
rewrite (Rmult_comm (/ 3)); repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym...
- pattern PI at 2 in |- *; rewrite (Rmult_comm PI); repeat rewrite Rmult_1_r;
+ rewrite (Rmult_comm PI); repeat rewrite Rmult_1_r;
repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym...
ring...
Qed.
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v
index 417cf13c..c6493135 100644
--- a/theories/Reals/Rtrigo_def.v
+++ b/theories/Reals/Rtrigo_def.v
@@ -1,18 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rtrigo_def.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-Require Import Rbase.
-Require Import Rfunctions.
-Require Import SeqSeries.
-Require Import Rtrigo_fun.
-Require Import Max.
+Require Import Rbase Rfunctions SeqSeries Rtrigo_fun Max.
Open Local Scope R_scope.
(********************************)
diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v
index 2ed86abe..b7720141 100644
--- a/theories/Reals/Rtrigo_fun.v
+++ b/theories/Reals/Rtrigo_fun.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rtrigo_fun.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index 59afec88..100e0818 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rtrigo_reg.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 7a1319ea..75c57401 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -1,17 +1,14 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: SeqProp.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
-Require Import Classical.
Require Import Max.
Open Local Scope R_scope.
@@ -29,31 +26,10 @@ Definition has_lb (Un:nat -> R) : Prop := bound (EUn (opp_seq Un)).
Lemma growing_cv :
forall Un:nat -> R, Un_growing Un -> has_ub Un -> { l:R | Un_cv Un l }.
Proof.
- unfold Un_growing, Un_cv in |- *; intros;
- destruct (completeness (EUn Un) H0 (EUn_noempty Un)) as [x [H2 H3]].
- exists x; intros eps H1.
- unfold is_upper_bound in H2, H3.
- assert (H5 : forall n:nat, Un n <= x).
- intro n; apply (H2 (Un n) (Un_in_EUn Un n)).
- cut (exists N : nat, x - eps < Un N).
- intro H6; destruct H6 as [N H6]; exists N.
- intros n H7; unfold R_dist in |- *; apply (Rabs_def1 (Un n - x) eps).
- unfold Rgt in H1.
- apply (Rle_lt_trans (Un n - x) 0 eps (Rle_minus (Un n) x (H5 n)) H1).
- fold Un_growing in H; generalize (growing_prop Un n N H H7); intro H8.
- generalize
- (Rlt_le_trans (x - eps) (Un N) (Un n) H6 (Rge_le (Un n) (Un N) H8));
- intro H9; generalize (Rplus_lt_compat_l (- x) (x - eps) (Un n) H9);
- unfold Rminus in |- *; rewrite <- (Rplus_assoc (- x) x (- eps));
- rewrite (Rplus_comm (- x) (Un n)); fold (Un n - x) in |- *;
- rewrite Rplus_opp_l; rewrite (let (H1, H2) := Rplus_ne (- eps) in H2);
- trivial.
- cut (~ (forall N:nat, Un N <= x - eps)).
- intro H6; apply (not_all_not_ex nat (fun N:nat => x - eps < Un N)).
- intro H7; apply H6; intro N; apply Rnot_lt_le; apply H7.
- intro H7; generalize (Un_bound_imp Un (x - eps) H7); intro H8;
- unfold is_upper_bound in H8; generalize (H3 (x - eps) H8);
- apply Rlt_not_le; apply tech_Rgt_minus; exact H1.
+ intros Un Hug Heub.
+ exists (projT1 (completeness (EUn Un) Heub (EUn_noempty Un))).
+ destruct (completeness _ Heub (EUn_noempty Un)) as (l, H).
+ now apply Un_cv_crit_lub.
Qed.
Lemma decreasing_growing :
@@ -518,68 +494,77 @@ Lemma approx_maj :
forall (Un:nat -> R) (pr:has_ub Un) (eps:R),
0 < eps -> exists k : nat, Rabs (lub Un pr - Un k) < eps.
Proof.
- intros.
- set (P := fun k:nat => Rabs (lub Un pr - Un k) < eps).
- unfold P in |- *.
- cut
- ((exists k : nat, P k) ->
- exists k : nat, Rabs (lub Un pr - Un k) < eps).
- intros.
- apply H0.
- apply not_all_not_ex.
- red in |- *; intro.
- 2: unfold P in |- *; trivial.
- unfold P in H1.
- cut (forall n:nat, Rabs (lub Un pr - Un n) >= eps).
- intro.
- cut (is_lub (EUn Un) (lub Un pr)).
- intro.
- unfold is_lub in H3.
- unfold is_upper_bound in H3.
- elim H3; intros.
- cut (forall n:nat, eps <= lub Un pr - Un n).
- intro.
- cut (forall n:nat, Un n <= lub Un pr - eps).
- intro.
- cut (forall x:R, EUn Un x -> x <= lub Un pr - eps).
- intro.
- assert (H9 := H5 (lub Un pr - eps) H8).
- cut (eps <= 0).
- intro.
- elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H H10)).
- apply Rplus_le_reg_l with (lub Un pr - eps).
- rewrite Rplus_0_r.
- replace (lub Un pr - eps + eps) with (lub Un pr);
- [ assumption | ring ].
- intros.
- unfold EUn in H8.
- elim H8; intros.
- rewrite H9; apply H7.
- intro.
- assert (H7 := H6 n).
- apply Rplus_le_reg_l with (eps - Un n).
- replace (eps - Un n + Un n) with eps.
- replace (eps - Un n + (lub Un pr - eps)) with (lub Un pr - Un n).
- assumption.
- ring.
- ring.
- intro.
- assert (H6 := H2 n).
- rewrite Rabs_right in H6.
- apply Rge_le.
- assumption.
- apply Rle_ge.
- apply Rplus_le_reg_l with (Un n).
- rewrite Rplus_0_r;
- replace (Un n + (lub Un pr - Un n)) with (lub Un pr);
- [ apply H4 | ring ].
- exists n; reflexivity.
- unfold lub in |- *.
- case (ub_to_lub Un pr).
- trivial.
- intro.
- assert (H2 := H1 n).
- apply not_Rlt; assumption.
+ intros Un pr.
+ pose (Vn := fix aux n := match n with S n' => if Rle_lt_dec (aux n') (Un n) then Un n else aux n' | O => Un O end).
+ pose (In := fix aux n := match n with S n' => if Rle_lt_dec (Vn n) (Un n) then n else aux n' | O => O end).
+
+ assert (VUI: forall n, Vn n = Un (In n)).
+ induction n.
+ easy.
+ simpl.
+ destruct (Rle_lt_dec (Vn n) (Un (S n))) as [H1|H1].
+ destruct (Rle_lt_dec (Un (S n)) (Un (S n))) as [H2|H2].
+ easy.
+ elim (Rlt_irrefl _ H2).
+ destruct (Rle_lt_dec (Vn n) (Un (S n))) as [H2|H2].
+ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 H1)).
+ exact IHn.
+
+ assert (HubV : has_ub Vn).
+ destruct pr as (ub, Hub).
+ exists ub.
+ intros x (n, Hn).
+ rewrite Hn, VUI.
+ apply Hub.
+ now exists (In n).
+
+ assert (HgrV : Un_growing Vn).
+ intros n.
+ induction n.
+ simpl.
+ destruct (Rle_lt_dec (Un O) (Un 1%nat)) as [H|_].
+ exact H.
+ apply Rle_refl.
+ simpl.
+ destruct (Rle_lt_dec (Vn n) (Un (S n))) as [H1|H1].
+ destruct (Rle_lt_dec (Un (S n)) (Un (S (S n)))) as [H2|H2].
+ exact H2.
+ apply Rle_refl.
+ destruct (Rle_lt_dec (Vn n) (Un (S (S n)))) as [H2|H2].
+ exact H2.
+ apply Rle_refl.
+
+ destruct (ub_to_lub Vn HubV) as (l, Hl).
+ unfold lub.
+ destruct (ub_to_lub Un pr) as (l', Hl').
+ replace l' with l.
+ intros eps Heps.
+ destruct (Un_cv_crit_lub Vn HgrV l Hl eps Heps) as (n, Hn).
+ exists (In n).
+ rewrite <- VUI.
+ rewrite Rabs_minus_sym.
+ apply Hn.
+ apply le_refl.
+
+ apply Rle_antisym.
+ apply Hl.
+ intros n (k, Hk).
+ rewrite Hk, VUI.
+ apply Hl'.
+ now exists (In k).
+ apply Hl'.
+ intros n (k, Hk).
+ rewrite Hk.
+ apply Rle_trans with (Vn k).
+ clear.
+ induction k.
+ apply Rle_refl.
+ simpl.
+ destruct (Rle_lt_dec (Vn k) (Un (S k))) as [H|H].
+ apply Rle_refl.
+ now apply Rlt_le.
+ apply Hl.
+ now exists k.
Qed.
(**********)
@@ -587,72 +572,23 @@ Lemma approx_min :
forall (Un:nat -> R) (pr:has_lb Un) (eps:R),
0 < eps -> exists k : nat, Rabs (glb Un pr - Un k) < eps.
Proof.
- intros.
- set (P := fun k:nat => Rabs (glb Un pr - Un k) < eps).
- unfold P in |- *.
- cut
- ((exists k : nat, P k) ->
- exists k : nat, Rabs (glb Un pr - Un k) < eps).
- intros.
- apply H0.
- apply not_all_not_ex.
- red in |- *; intro.
- 2: unfold P in |- *; trivial.
- unfold P in H1.
- cut (forall n:nat, Rabs (glb Un pr - Un n) >= eps).
- intro.
- cut (is_lub (EUn (opp_seq Un)) (- glb Un pr)).
- intro.
- unfold is_lub in H3.
- unfold is_upper_bound in H3.
- elim H3; intros.
- cut (forall n:nat, eps <= Un n - glb Un pr).
- intro.
- cut (forall n:nat, opp_seq Un n <= - glb Un pr - eps).
- intro.
- cut (forall x:R, EUn (opp_seq Un) x -> x <= - glb Un pr - eps).
- intro.
- assert (H9 := H5 (- glb Un pr - eps) H8).
- cut (eps <= 0).
- intro.
- elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H H10)).
- apply Rplus_le_reg_l with (- glb Un pr - eps).
- rewrite Rplus_0_r.
- replace (- glb Un pr - eps + eps) with (- glb Un pr);
- [ assumption | ring ].
- intros.
- unfold EUn in H8.
- elim H8; intros.
- rewrite H9; apply H7.
- intro.
- assert (H7 := H6 n).
- unfold opp_seq in |- *.
- apply Rplus_le_reg_l with (eps + Un n).
- replace (eps + Un n + - Un n) with eps.
- replace (eps + Un n + (- glb Un pr - eps)) with (Un n - glb Un pr).
- assumption.
- ring.
- ring.
- intro.
- assert (H6 := H2 n).
- rewrite Rabs_left1 in H6.
- apply Rge_le.
- replace (Un n - glb Un pr) with (- (glb Un pr - Un n));
- [ assumption | ring ].
- apply Rplus_le_reg_l with (- glb Un pr).
- rewrite Rplus_0_r;
- replace (- glb Un pr + (glb Un pr - Un n)) with (- Un n).
- apply H4.
- exists n; reflexivity.
- ring.
- unfold glb in |- *.
- case (lb_to_glb Un pr); simpl.
- intro.
- rewrite Ropp_involutive.
- trivial.
- intro.
- assert (H2 := H1 n).
- apply not_Rlt; assumption.
+ intros Un pr.
+ unfold glb.
+ destruct lb_to_glb as (lb, Hlb).
+ intros eps Heps.
+ destruct (approx_maj _ pr eps Heps) as (n, Hn).
+ exists n.
+ unfold Rminus.
+ rewrite <- Ropp_plus_distr, Rabs_Ropp.
+ replace lb with (lub (opp_seq Un) pr).
+ now rewrite <- (Ropp_involutive (Un n)).
+ unfold lub.
+ destruct ub_to_lub as (ub, Hub).
+ apply Rle_antisym.
+ apply Hub.
+ apply Hlb.
+ apply Hlb.
+ apply Hub.
Qed.
(** Unicity of limit for convergent sequences *)
@@ -910,73 +846,6 @@ Proof.
left; assumption.
Qed.
-Lemma tech10 :
- forall (Un:nat -> R) (x:R), Un_growing Un -> is_lub (EUn Un) x -> Un_cv Un x.
-Proof.
- intros; cut (bound (EUn Un)).
- intro; assert (H2 := Un_cv_crit _ H H1).
- elim H2; intros.
- case (total_order_T x x0); intro.
- elim s; intro.
- cut (forall n:nat, Un n <= x).
- intro; unfold Un_cv in H3; cut (0 < x0 - x).
- intro; elim (H3 (x0 - x) H5); intros.
- cut (x1 >= x1)%nat.
- intro; assert (H8 := H6 x1 H7).
- unfold R_dist in H8; rewrite Rabs_left1 in H8.
- rewrite Ropp_minus_distr in H8; unfold Rminus in H8.
- assert (H9 := Rplus_lt_reg_r x0 _ _ H8).
- assert (H10 := Ropp_lt_cancel _ _ H9).
- assert (H11 := H4 x1).
- elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H10 H11)).
- apply Rle_minus; apply Rle_trans with x.
- apply H4.
- left; assumption.
- unfold ge in |- *; apply le_n.
- apply Rgt_minus; assumption.
- intro; unfold is_lub in H0; unfold is_upper_bound in H0; elim H0; intros.
- apply H4; unfold EUn in |- *; exists n; reflexivity.
- rewrite b; assumption.
- cut (forall n:nat, Un n <= x0).
- intro; unfold is_lub in H0; unfold is_upper_bound in H0; elim H0; intros.
- cut (forall y:R, EUn Un y -> y <= x0).
- intro; assert (H8 := H6 _ H7).
- elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H8 r)).
- unfold EUn in |- *; intros; elim H7; intros.
- rewrite H8; apply H4.
- intro; case (Rle_dec (Un n) x0); intro.
- assumption.
- cut (forall n0:nat, (n <= n0)%nat -> x0 < Un n0).
- intro; unfold Un_cv in H3; cut (0 < Un n - x0).
- intro; elim (H3 (Un n - x0) H5); intros.
- cut (max n x1 >= x1)%nat.
- intro; assert (H8 := H6 (max n x1) H7).
- unfold R_dist in H8.
- rewrite Rabs_right in H8.
- unfold Rminus in H8; do 2 rewrite <- (Rplus_comm (- x0)) in H8.
- assert (H9 := Rplus_lt_reg_r _ _ _ H8).
- cut (Un n <= Un (max n x1)).
- intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H10 H9)).
- apply tech9; [ assumption | apply le_max_l ].
- apply Rge_trans with (Un n - x0).
- unfold Rminus in |- *; apply Rle_ge; do 2 rewrite <- (Rplus_comm (- x0));
- apply Rplus_le_compat_l.
- apply tech9; [ assumption | apply le_max_l ].
- left; assumption.
- unfold ge in |- *; apply le_max_r.
- apply Rplus_lt_reg_r with x0.
- rewrite Rplus_0_r; unfold Rminus in |- *; rewrite (Rplus_comm x0);
- rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r;
- apply H4; apply le_n.
- intros; apply Rlt_le_trans with (Un n).
- case (Rlt_le_dec x0 (Un n)); intro.
- assumption.
- elim n0; assumption.
- apply tech9; assumption.
- unfold bound in |- *; exists x; unfold is_lub in H0; elim H0; intros;
- assumption.
-Qed.
-
Lemma tech13 :
forall (An:nat -> R) (k:R),
0 <= k < 1 ->
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v
index 4725fe57..0d876be5 100644
--- a/theories/Reals/SeqSeries.v
+++ b/theories/Reals/SeqSeries.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: SeqSeries.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Max.
diff --git a/theories/Reals/SplitAbsolu.v b/theories/Reals/SplitAbsolu.v
index 67af68d1..819606c4 100644
--- a/theories/Reals/SplitAbsolu.v
+++ b/theories/Reals/SplitAbsolu.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: SplitAbsolu.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbasic_fun.
Ltac split_case_Rabs :=
diff --git a/theories/Reals/SplitRmult.v b/theories/Reals/SplitRmult.v
index 85a2cdd0..e554913c 100644
--- a/theories/Reals/SplitRmult.v
+++ b/theories/Reals/SplitRmult.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: SplitRmult.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(*i Lemma mult_non_zero :(r1,r2:R)``r1<>0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*)
diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v
index 79f39892..d00ed178 100644
--- a/theories/Reals/Sqrt_reg.v
+++ b/theories/Reals/Sqrt_reg.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Sqrt_reg.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis1.