diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
| commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
| tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /theories/Reals | |
| parent | 300293c119981054c95182a90c829058530a6b6f (diff) | |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'theories/Reals')
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. |