diff options
| author |  Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
| commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
| tree | dabcac548e299fee1da464c93b3dba98484f45b1 /theories/Reals | |
| parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) | |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'theories/Reals')
46 files changed, 1502 insertions, 1035 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index 802bfa71..7625cce6 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Alembert.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Alembert.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -25,12 +25,12 @@ Lemma Alembert_C1 : forall An:nat -> R, (forall n:nat, 0 < An n) -> Un_cv (fun n:nat => Rabs (An (S n) / An n)) 0 -> - sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l). + { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }. Proof. intros An H H0. cut - (sigT (fun l:R => is_lub (EUn (fun N:nat => sum_f_R0 An N)) l) -> - sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l)). + ({ l:R | is_lub (EUn (fun N:nat => sum_f_R0 An N)) l } -> + { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }). intro X; apply X. apply completeness. unfold Un_cv in H0; unfold bound in |- *; cut (0 < / 2); @@ -109,18 +109,18 @@ Proof. symmetry in |- *; apply tech2; assumption. exists (sum_f_R0 An 0); unfold EUn in |- *; exists 0%nat; reflexivity. intro X; elim X; intros. - apply existT with x; apply tech10; + exists x; apply tech10; [ 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 | apply p ]. -Qed. +Defined. Lemma Alembert_C2 : forall An:nat -> R, (forall n:nat, An n <> 0) -> Un_cv (fun n:nat => Rabs (An (S n) / An n)) 0 -> - sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l). + { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }. Proof. intros. set (Vn := fun i:nat => (2 * Rabs (An i) + An i) / 2). @@ -133,7 +133,7 @@ Proof. assert (H6 := Alembert_C1 Wn H2 H4). elim H5; intros. elim H6; intros. - apply existT with (x - x0); unfold Un_cv in |- *; unfold Un_cv in p; + exists (x - x0); unfold Un_cv in |- *; unfold Un_cv in p; unfold Un_cv in p0; intros; cut (0 < eps / 2). intro; elim (p (eps / 2) H8); clear p; intros. elim (p0 (eps / 2) H8); clear p0; intros. @@ -334,21 +334,21 @@ Proof. rewrite <- Rabs_Ropp; apply RRle_abs. rewrite double; pattern (Rabs (An n)) at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; apply Rabs_pos_lt; apply H. -Qed. +Defined. Lemma AlembertC3_step1 : forall (An:nat -> R) (x:R), x <> 0 -> (forall n:nat, An n <> 0) -> Un_cv (fun n:nat => Rabs (An (S n) / An n)) 0 -> - sigT (fun l:R => Pser An x l). + { l:R | Pser An x l }. Proof. intros; set (Bn := fun i:nat => An i * x ^ i). cut (forall n:nat, Bn n <> 0). intro; cut (Un_cv (fun n:nat => Rabs (Bn (S n) / Bn n)) 0). intro; assert (H4 := Alembert_C2 Bn H2 H3). elim H4; intros. - apply existT with x0; unfold Bn in p; apply tech12; assumption. + exists x0; unfold Bn in p; apply tech12; assumption. unfold Un_cv in |- *; intros; unfold Un_cv in H1; cut (0 < eps / Rabs x). intro; elim (H1 (eps / Rabs x) H4); intros. exists x0; intros; unfold R_dist in |- *; unfold Rminus in |- *; @@ -379,13 +379,13 @@ Proof. [ assumption | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ]. intro; unfold Bn in |- *; apply prod_neq_R0; [ apply H0 | apply pow_nonzero; assumption ]. -Qed. +Defined. Lemma AlembertC3_step2 : - forall (An:nat -> R) (x:R), x = 0 -> sigT (fun l:R => Pser An x l). + forall (An:nat -> R) (x:R), x = 0 -> { l:R | Pser An x l }. Proof. - intros; apply existT with (An 0%nat). - unfold Pser in |- *; unfold infinit_sum in |- *; intros; exists 0%nat; intros; + intros; exists (An 0%nat). + unfold Pser in |- *; unfold infinite_sum in |- *; intros; exists 0%nat; intros; replace (sum_f_R0 (fun n0:nat => An n0 * x ^ n0) n) with (An 0%nat). unfold R_dist in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. @@ -395,12 +395,12 @@ Proof. [ rewrite H; simpl in |- *; ring | unfold ge in |- *; apply le_O_n ]. Qed. -(** An useful criterion of convergence for power series *) +(** A useful criterion of convergence for power series *) Theorem Alembert_C3 : forall (An:nat -> R) (x:R), (forall n:nat, An n <> 0) -> Un_cv (fun n:nat => Rabs (An (S n) / An n)) 0 -> - sigT (fun l:R => Pser An x l). + { l:R | Pser An x l }. Proof. intros; case (total_order_T x 0); intro. elim s; intro. @@ -411,19 +411,19 @@ Proof. cut (x <> 0). intro; apply AlembertC3_step1; assumption. red in |- *; intro; rewrite H1 in r; elim (Rlt_irrefl _ r). -Qed. +Defined. Lemma Alembert_C4 : forall (An:nat -> R) (k:R), 0 <= k < 1 -> (forall n:nat, 0 < An n) -> Un_cv (fun n:nat => Rabs (An (S n) / An n)) k -> - sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l). + { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }. Proof. intros An k Hyp H H0. cut - (sigT (fun l:R => is_lub (EUn (fun N:nat => sum_f_R0 An N)) l) -> - sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l)). + ({ l:R | is_lub (EUn (fun N:nat => sum_f_R0 An N)) l } -> + { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }). intro X; apply X. apply completeness. assert (H1 := tech13 _ _ Hyp H0). @@ -524,7 +524,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. - apply existT with x; apply tech10; + exists x; apply tech10; [ 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 @@ -536,21 +536,19 @@ Lemma Alembert_C5 : 0 <= k < 1 -> (forall n:nat, An n <> 0) -> Un_cv (fun n:nat => Rabs (An (S n) / An n)) k -> - sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l). + { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }. Proof. intros. cut - (sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l) -> - sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l)). + ({ l:R | Un_cv (fun N:nat => sum_f_R0 An N) l } -> + { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }). intro Hyp0; apply Hyp0. apply cv_cauchy_2. apply cauchy_abs. apply cv_cauchy_1. cut - (sigT - (fun l:R => Un_cv (fun N:nat => sum_f_R0 (fun i:nat => Rabs (An i)) N) l) -> - sigT - (fun l:R => Un_cv (fun N:nat => sum_f_R0 (fun i:nat => Rabs (An i)) N) l)). + ({ l:R | Un_cv (fun N:nat => sum_f_R0 (fun i:nat => Rabs (An i)) N) l } -> + { l:R | Un_cv (fun N:nat => sum_f_R0 (fun i:nat => Rabs (An i)) N) l }). intro Hyp; apply Hyp. apply (Alembert_C4 (fun i:nat => Rabs (An i)) k). assumption. @@ -568,11 +566,11 @@ Proof. apply H0. intro X. elim X; intros. - apply existT with x. + exists x. assumption. intro X. elim X; intros. - apply existT with x. + exists x. assumption. Qed. @@ -583,14 +581,12 @@ Lemma Alembert_C6 : 0 < k -> (forall n:nat, An n <> 0) -> Un_cv (fun n:nat => Rabs (An (S n) / An n)) k -> - Rabs x < / k -> sigT (fun l:R => Pser An x l). + Rabs x < / k -> { l:R | Pser An x l }. intros. - cut - (sigT - (fun l:R => Un_cv (fun N:nat => sum_f_R0 (fun i:nat => An i * x ^ i) N) l)). + cut { l:R | Un_cv (fun N:nat => sum_f_R0 (fun i:nat => An i * x ^ i) N) l }. intro X. elim X; intros. - apply existT with x0. + exists x0. apply tech12; assumption. case (total_order_T x 0); intro. elim s; intro. @@ -655,7 +651,7 @@ Lemma Alembert_C6 : assumption. apply Rinv_0_lt_compat; apply Rabs_pos_lt. red in |- *; intro H7; rewrite H7 in a; elim (Rlt_irrefl _ a). - apply existT with (An 0%nat). + exists (An 0%nat). unfold Un_cv in |- *. intros. exists 0%nat. diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index 581c181f..5c4bbd6a 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id: AltSeries.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) + (*i $Id: AltSeries.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -153,14 +153,14 @@ Lemma CV_ALT : Un_decreasing Un -> positivity_seq Un -> Un_cv Un 0 -> - sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 (tg_alt Un) N) l). + { l:R | Un_cv (fun N:nat => sum_f_R0 (tg_alt Un) N) l }. Proof. intros. assert (H2 := CV_ALT_step0 _ H). assert (H3 := CV_ALT_step4 _ H H0). assert (X := growing_cv _ H2 H3). elim X; intros. - apply existT with x. + exists x. unfold Un_cv in |- *; unfold R_dist in |- *; unfold Un_cv in H1; unfold R_dist in H1; unfold Un_cv in p; unfold R_dist in p. intros; cut (0 < eps / 2); @@ -220,7 +220,7 @@ Theorem alternated_series : forall Un:nat -> R, Un_decreasing Un -> Un_cv Un 0 -> - sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 (tg_alt Un) N) l). + { l:R | Un_cv (fun N:nat => sum_f_R0 (tg_alt Un) N) l }. Proof. intros; apply CV_ALT. assumption. @@ -408,7 +408,7 @@ Proof. Qed. Lemma exist_PI : - sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 (tg_alt PI_tg) N) l). + { l:R | Un_cv (fun N:nat => sum_f_R0 (tg_alt PI_tg) N) l }. Proof. apply alternated_series. apply PI_tg_decreasing. @@ -416,9 +416,7 @@ Proof. Qed. (** Now, PI is defined *) -Definition PI : R := 4 * match exist_PI with - | existT a b => a - end. +Definition PI : R := 4 * (let (a,_) := exist_PI in a). (** We can get an approximation of PI with the following inequality *) Lemma PI_ineq : diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index 7dbbd605..7327c64c 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id: ArithProp.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) + (*i $Id: ArithProp.v 9454 2006-12-15 15:30:59Z bgregoir $ i*) Require Import Rbase. Require Import Rbasic_fun. diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v index 10965951..0de639e8 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -6,14 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id: Cos_plus.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) + (*i $Id: Cos_plus.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. Require Import Rtrigo_def. Require Import Cos_rel. -Require Import Max. Open Local Scope nat_scope. Open Local Scope R_scope. +Require Import Max. +Open Local Scope nat_scope. +Open Local Scope R_scope. Definition Majxy (x y:R) (n:nat) : R := Rmax 1 (Rmax (Rabs x) (Rabs y)) ^ (4 * S n) / INR (fact n). diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index d410e14a..aed481c7 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Cos_rel.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: Cos_rel.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -263,7 +263,7 @@ assert (H := exist_cos (x * x)). elim H; intros. assert (p_i := p). unfold cos_in in p. -unfold cos_n, infinit_sum in p. +unfold cos_n, infinite_sum in p. unfold R_dist in p. cut (cos x = x0). intro. @@ -295,7 +295,7 @@ assert (H := exist_cos ((x + y) * (x + y))). elim H; intros. assert (p_i := p). unfold cos_in in p. -unfold cos_n, infinit_sum in p. +unfold cos_n, infinite_sum in p. unfold R_dist in p. cut (cos (x + y) = x0). intro. @@ -344,7 +344,7 @@ assert (H0 := exist_sin (x * x)). elim H0; intros. assert (p_i := p). unfold sin_in in p. -unfold sin_n, infinit_sum in p. +unfold sin_n, infinite_sum in p. unfold R_dist in p. cut (sin x = x * x0). intro. diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index a16af05c..22a52e67 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -6,10 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: DiscrR.v 9178 2006-09-26 11:18:22Z barras $ i*) +(*i $Id: DiscrR.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import RIneq. -Require Import Omega. Open Local Scope R_scope. +Require Import Omega. +Open Local Scope R_scope. Lemma Rlt_R0_R2 : 0 < 2. change 2 with (INR 2); apply lt_INR_0; apply lt_O_Sn. diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index beb4b744..bf729526 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Exp_prop.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: Exp_prop.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -27,7 +27,7 @@ Lemma E1_cvg : forall x:R, Un_cv (E1 x) (exp x). Proof. intro; unfold exp in |- *; unfold projT1 in |- *. case (exist_exp x); intro. - unfold exp_in, Un_cv in |- *; unfold infinit_sum, E1 in |- *; trivial. + unfold exp_in, Un_cv in |- *; unfold infinite_sum, E1 in |- *; trivial. Qed. Definition Reste_E (x y:R) (N:nat) : R := @@ -734,7 +734,7 @@ Proof. apply Rinv_0_lt_compat; apply INR_fact_lt_0. apply (pow_lt _ n H). unfold exp in |- *; unfold projT1 in |- *; case (exist_exp x); intro. - unfold exp_in in |- *; unfold infinit_sum, Un_cv in |- *; trivial. + unfold exp_in in |- *; unfold infinite_sum, Un_cv in |- *; trivial. Qed. (**********) @@ -769,7 +769,7 @@ Proof. unfold derivable_pt_lim in |- *; intros. set (fn := fun (N:nat) (x:R) => x ^ N / INR (fact (S N))). cut (CVN_R fn). - intro; cut (forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)). + intro; cut (forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }). intro cv; cut (forall n:nat, continuity (fn n)). intro; cut (continuity (SFL fn cv)). intro; unfold continuity in H1. @@ -809,13 +809,12 @@ Proof. unfold Rdiv in |- *; rewrite Rinv_1; rewrite Rmult_1_r; reflexivity. apply lt_le_trans with 1%nat; [ apply lt_n_Sn | apply H9 ]. unfold SFL, exp in |- *. - unfold projT1 in |- *. - case (cv h); case (exist_exp h); intros. + case (cv h); case (exist_exp h); simpl; intros. eapply UL_sequence. apply u. unfold Un_cv in |- *; intros. unfold exp_in in e. - unfold infinit_sum in e. + unfold infinite_sum in e. cut (0 < eps0 * Rabs h). intro; elim (e _ H9); intros N0 H10. exists N0; intros. @@ -871,13 +870,12 @@ Proof. assert (H0 := Alembert_exp). unfold CVN_R in |- *. intro; unfold CVN_r in |- *. - apply existT with (fun N:nat => r ^ N / INR (fact (S N))). + exists (fun N:nat => r ^ N / INR (fact (S N))). cut - (sigT - (fun l:R => + { l:R | Un_cv (fun n:nat => - sum_f_R0 (fun k:nat => Rabs (r ^ k / INR (fact (S k)))) n) l)). + sum_f_R0 (fun k:nat => Rabs (r ^ k / INR (fact (S k)))) n) l }. intro X. elim X; intros. exists x; intros. diff --git a/theories/Reals/LegacyRfield.v b/theories/Reals/LegacyRfield.v index b33274af..3f76e77a 100644 --- a/theories/Reals/LegacyRfield.v +++ b/theories/Reals/LegacyRfield.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: LegacyRfield.v 10739 2008-04-01 14:45:20Z herbelin $ i*) Require Export Raxioms. Require Export LegacyField. diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v index 8bb9298a..f22e49e1 100644 --- a/theories/Reals/MVT.v +++ b/theories/Reals/MVT.v @@ -6,12 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: MVT.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: MVT.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. -Require Import Rtopology. Open Local Scope R_scope. +Require Import Rtopology. +Open Local Scope R_scope. (* The Mean Value Theorem *) Theorem MVT : @@ -189,7 +190,7 @@ Proof. intros; apply derivable_pt_id. intros; apply derivable_continuous_pt; apply X; assumption. intros; elim H1; intros; apply X; split; left; assumption. - intros; unfold derivable_pt in |- *; apply existT with (f' c); apply H0; + intros; unfold derivable_pt in |- *; exists (f' c); apply H0; apply H1. Qed. @@ -695,11 +696,11 @@ Proof. unfold antiderivative in |- *; intros; elim H; clear H; intros; elim H0; clear H0; intros H0 _; exists (g1 a - g2 a); intros; assert (H3 : forall x:R, a <= x <= b -> derivable_pt g1 x). - intros; unfold derivable_pt in |- *; apply existT with (f x0); elim (H x0 H3); + intros; unfold derivable_pt in |- *; exists (f x0); elim (H x0 H3); intros; eapply derive_pt_eq_1; symmetry in |- *; apply H4. assert (H4 : forall x:R, a <= x <= b -> derivable_pt g2 x). - intros; unfold derivable_pt in |- *; apply existT with (f x0); + intros; unfold derivable_pt in |- *; exists (f x0); elim (H0 x0 H4); intros; eapply derive_pt_eq_1; symmetry in |- *; apply H5. assert (H5 : forall x:R, a < x < b -> derivable_pt (g1 - g2) x). diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index 306d5ac4..47ae149e 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -6,32 +6,31 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: NewtonInt.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: NewtonInt.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. Require Import Rtrigo. -Require Import Ranalysis. Open Local Scope R_scope. +Require Import Ranalysis. +Open Local Scope R_scope. (*******************************************) (* Newton's Integral *) (*******************************************) Definition Newton_integrable (f:R -> R) (a b:R) : Type := - sigT (fun g:R -> R => antiderivative f g a b \/ antiderivative f g b a). + { g:R -> R | antiderivative f g a b \/ antiderivative f g b a }. Definition NewtonInt (f:R -> R) (a b:R) (pr:Newton_integrable f a b) : R := - let g := match pr with - | existT a b => a - end in g b - g a. + let (g,_) := pr in g b - g a. (* If f is differentiable, then f' is Newton integrable (Tautology ?) *) Lemma FTCN_step1 : forall (f:Differential) (a b:R), Newton_integrable (fun x:R => derive_pt f x (cond_diff f x)) a b. Proof. - intros f a b; unfold Newton_integrable in |- *; apply existT with (d1 f); + intros f a b; unfold Newton_integrable in |- *; exists (d1 f); unfold antiderivative in |- *; intros; case (Rle_dec a b); intro; [ left; split; [ intros; exists (cond_diff f x); reflexivity | assumption ] @@ -52,7 +51,7 @@ Qed. Lemma NewtonInt_P1 : forall (f:R -> R) (a:R), Newton_integrable f a a. Proof. intros f a; unfold Newton_integrable in |- *; - apply existT with (fct_cte (f a) * id)%F; left; + exists (fct_cte (f a) * id)%F; left; unfold antiderivative in |- *; split. intros; assert (H1 : derivable_pt (fct_cte (f a) * id) x). apply derivable_pt_mult. @@ -82,7 +81,7 @@ Lemma NewtonInt_P3 : Newton_integrable f b a. Proof. unfold Newton_integrable in |- *; intros; elim X; intros g H; - apply existT with g; tauto. + exists g; tauto. Defined. (* $\int_a^b f = -\int_b^a f$ *) @@ -94,7 +93,7 @@ Proof. unfold NewtonInt in |- *; case (NewtonInt_P3 f a b - (existT + (exist (fun g:R -> R => antiderivative f g a b \/ antiderivative f g b a) x p)). intros; elim o; intro. @@ -112,7 +111,7 @@ Proof. unfold NewtonInt in |- *; case (NewtonInt_P3 f a b - (existT + (exist (fun g:R -> R => antiderivative f g a b \/ antiderivative f g b a) x p)); intros; elim o; intro. assert (H1 := antiderivative_Ucte f x x0 b a H H0); elim H1; intros; @@ -325,7 +324,7 @@ Proof. | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end) x). - unfold derivable_pt in |- *; apply existT with (f x); apply H7. + unfold derivable_pt in |- *; exists (f x); apply H7. exists H8; symmetry in |- *; apply derive_pt_eq_0; apply H7. assert (H5 : a <= x <= b). split; [ assumption | right; assumption ]. @@ -370,7 +369,7 @@ Proof. | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end) x). - unfold derivable_pt in |- *; apply existT with (f x); apply H13. + unfold derivable_pt in |- *; exists (f x); apply H13. exists H14; symmetry in |- *; apply derive_pt_eq_0; apply H13. assert (H5 : b <= x <= c). split; [ left; assumption | assumption ]. @@ -417,7 +416,7 @@ Proof. | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end) x). - unfold derivable_pt in |- *; apply existT with (f x); apply H7. + unfold derivable_pt in |- *; exists (f x); apply H7. exists H8; symmetry in |- *; apply derive_pt_eq_0; apply H7. Qed. @@ -482,7 +481,7 @@ Proof. match Rle_dec x b with | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) - end); apply existT with g; left; unfold g in |- *; + end); exists g; left; unfold g in |- *; apply antiderivative_P2. elim H0; intro. assumption. @@ -508,7 +507,7 @@ Proof. elim s0; intro. (* a<b & b<c *) unfold Newton_integrable in |- *; - apply existT with + exists (fun x:R => match Rle_dec x b with | left _ => F0 x @@ -526,7 +525,7 @@ Proof. (* a<b & b>c *) case (total_order_T a c); intro. elim s0; intro. - unfold Newton_integrable in |- *; apply existT with F0. + unfold Newton_integrable in |- *; exists F0. left. elim H1; intro. unfold antiderivative in H; elim H; clear H; intros _ H. @@ -540,7 +539,7 @@ Proof. unfold antiderivative in H2; elim H2; clear H2; intros _ H2. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 a0)). rewrite b0; apply NewtonInt_P1. - unfold Newton_integrable in |- *; apply existT with F1. + unfold Newton_integrable in |- *; exists F1. right. elim H1; intro. unfold antiderivative in H; elim H; clear H; intros _ H. @@ -560,7 +559,7 @@ Proof. (* a>b & b<c *) case (total_order_T a c); intro. elim s0; intro. - unfold Newton_integrable in |- *; apply existT with F1. + unfold Newton_integrable in |- *; exists F1. left. elim H1; intro. (*****************) @@ -575,7 +574,7 @@ Proof. unfold antiderivative in H; elim H; clear H; intros _ H. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H a0)). rewrite b0; apply NewtonInt_P1. - unfold Newton_integrable in |- *; apply existT with F0. + unfold Newton_integrable in |- *; exists F0. right. elim H0; intro. unfold antiderivative in H; elim H; clear H; intros _ H. diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v index 64b8e0af..e122a26a 100644 --- a/theories/Reals/PSeries_reg.v +++ b/theories/Reals/PSeries_reg.v @@ -6,14 +6,15 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: PSeries_reg.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: PSeries_reg.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. Require Import Ranalysis1. Require Import Max. -Require Import Even. Open Local Scope R_scope. +Require Import Even. +Open Local Scope R_scope. Definition Boule (x:R) (r:posreal) (y:R) : Prop := Rabs (y - x) < r. @@ -28,25 +29,21 @@ Definition CVU (fn:nat -> R -> R) (f:R -> R) (x:R) (** Normal convergence *) Definition CVN_r (fn:nat -> R -> R) (r:posreal) : Type := - sigT - (fun An:nat -> R => - sigT - (fun l:R => + { An:nat -> R & + { l:R | Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (An k)) n) l /\ - (forall (n:nat) (y:R), Boule 0 r y -> Rabs (fn n y) <= An n))). + (forall (n:nat) (y:R), Boule 0 r y -> Rabs (fn n y) <= An n) } }. Definition CVN_R (fn:nat -> R -> R) : Type := forall r:posreal, CVN_r fn r. Definition SFL (fn:nat -> R -> R) - (cv:forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)) - (y:R) : R := match cv y with - | existT a b => a - end. + (cv:forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }) + (y:R) : R := let (a,_) := cv y in a. (** In a complete space, normal convergence implies uniform convergence *) Lemma CVN_CVU : forall (fn:nat -> R -> R) - (cv:forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)) + (cv:forall x:R, {l:R | Un_cv (fun N:nat => SP fn N x) l }) (r:posreal), CVN_r fn r -> CVU (fun n:nat => SP fn n) (SFL fn cv) 0 r. Proof. intros; unfold CVU in |- *; intros. @@ -193,7 +190,7 @@ Qed. (** Continuity and normal convergence *) Lemma SFL_continuity_pt : forall (fn:nat -> R -> R) - (cv:forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)) + (cv:forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }) (r:posreal), CVN_r fn r -> (forall (n:nat) (y:R), Boule 0 r y -> continuity_pt (fn n) y) -> @@ -210,7 +207,7 @@ Qed. Lemma SFL_continuity : forall (fn:nat -> R -> R) - (cv:forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)), + (cv:forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }), CVN_R fn -> (forall n:nat, continuity (fn n)) -> continuity (SFL fn cv). Proof. intros; unfold continuity in |- *; intro. @@ -229,7 +226,7 @@ Qed. (** As R is complete, normal convergence implies that (fn) is simply-uniformly convergent *) Lemma CVN_R_CVS : forall fn:nat -> R -> R, - CVN_R fn -> forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l). + CVN_R fn -> forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }. Proof. intros; apply R_complete. unfold SP in |- *; set (An := fun N:nat => fn N x). @@ -248,7 +245,7 @@ Proof. rewrite Rminus_0_r. pattern (Rabs x) at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; apply Rlt_0_1. - apply existT with l. + exists l. cut (forall n:nat, 0 <= Bn n). intro; unfold Un_cv in H3; unfold Un_cv in |- *; intros. elim (H3 _ H6); intros. diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index a8f72302..d5ae2aca 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: PartSum.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: PartSum.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -153,7 +153,7 @@ Lemma tech12 : Un_cv (fun N:nat => sum_f_R0 (fun i:nat => An i * x ^ i) N) l -> Pser An x l. Proof. - intros; unfold Pser in |- *; unfold infinit_sum in |- *; unfold Un_cv in H; + intros; unfold Pser in |- *; unfold infinite_sum in |- *; unfold Un_cv in H; assumption. Qed. @@ -218,9 +218,9 @@ Qed. (* Unicity of the limit defined by convergent series *) Lemma uniqueness_sum : forall (An:nat -> R) (l1 l2:R), - infinit_sum An l1 -> infinit_sum An l2 -> l1 = l2. + infinite_sum An l1 -> infinite_sum An l2 -> l1 = l2. Proof. - unfold infinit_sum in |- *; intros. + unfold infinite_sum in |- *; intros. case (Req_dec l1 l2); intro. assumption. cut (0 < Rabs ((l1 - l2) / 2)); [ intro | apply Rabs_pos_lt ]. @@ -450,7 +450,7 @@ Qed. (**********) Lemma cv_cauchy_1 : forall An:nat -> R, - sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l) -> + { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l } -> Cauchy_crit_series An. Proof. intros An X. @@ -481,7 +481,7 @@ Qed. Lemma cv_cauchy_2 : forall An:nat -> R, Cauchy_crit_series An -> - sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l). + { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }. Proof. intros. apply R_complete. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 7d98a844..19bdeccd 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: RIneq.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: RIneq.v 10762 2008-04-06 16:57:31Z herbelin $ i*) -(***************************************************************************) -(** Basic lemmas for the classical reals numbers *) -(***************************************************************************) +(*********************************************************) +(** * Basic lemmas for the classical real numbers *) +(*********************************************************) Require Export Raxioms. Require Import Rpow_def. @@ -24,21 +24,32 @@ Open Local Scope R_scope. Implicit Type r : R. -(**************************************************************************) -(** * Relation between orders and equality *) -(**************************************************************************) +(*********************************************************) +(** ** Relation between orders and equality *) +(*********************************************************) + +(** Reflexivity of the large order *) + +Lemma Rle_refl : forall r, r <= r. +Proof. + intro; right; reflexivity. +Qed. +Hint Immediate Rle_refl: rorders. + +Lemma Rge_refl : forall r, r <= r. +Proof. exact Rle_refl. Qed. +Hint Immediate Rge_refl: rorders. + +(** Irreflexivity of the strict order *) -(**********) Lemma Rlt_irrefl : forall r, ~ r < r. Proof. generalize Rlt_asym. intuition eauto. Qed. Hint Resolve Rlt_irrefl: real. -Lemma Rle_refl : forall r, r <= r. -Proof. - intro; right; reflexivity. -Qed. +Lemma Rgt_irrefl : forall r, ~ r > r. +Proof. exact Rlt_irrefl. Qed. Lemma Rlt_not_eq : forall r1 r2, r1 < r2 -> r1 <> r2. Proof. @@ -58,7 +69,7 @@ Proof. Qed. Hint Resolve Rlt_dichotomy_converse: real. -(** Reasoning by case on equalities and order *) +(** Reasoning by case on equality and order *) (**********) Lemma Req_dec : forall r1 r2, r1 = r2 \/ r1 <> r2. @@ -80,58 +91,104 @@ Proof. intros; generalize (total_order_T r1 r2); tauto. Qed. +(*********************************************************) +(** ** Relating [<], [>], [<=] and [>=] *) +(*********************************************************) -(*********************************************************************************) -(** * Order Lemma : relating [<], [>], [<=] and [>=] *) -(*********************************************************************************) +(*********************************************************) +(** ** Order *) +(*********************************************************) + +(** *** Relating strict and large orders *) -(**********) Lemma Rlt_le : forall r1 r2, r1 < r2 -> r1 <= r2. Proof. intros; red in |- *; tauto. Qed. Hint Resolve Rlt_le: real. +Lemma Rgt_ge : forall r1 r2, r1 > r2 -> r1 >= r2. +Proof. + intros; red; tauto. +Qed. + (**********) Lemma Rle_ge : forall r1 r2, r1 <= r2 -> r2 >= r1. Proof. destruct 1; red in |- *; auto with real. Qed. - Hint Immediate Rle_ge: real. +Hint Resolve Rle_ge: rorders. -(**********) Lemma Rge_le : forall r1 r2, r1 >= r2 -> r2 <= r1. Proof. destruct 1; red in |- *; auto with real. Qed. - Hint Resolve Rge_le: real. +Hint Immediate Rge_le: rorders. (**********) +Lemma Rlt_gt : forall r1 r2, r1 < r2 -> r2 > r1. +Proof. + trivial. +Qed. +Hint Resolve Rlt_gt: rorders. + +Lemma Rgt_lt : forall r1 r2, r1 > r2 -> r2 < r1. +Proof. + trivial. +Qed. +Hint Immediate Rgt_lt: rorders. + +(**********) + Lemma Rnot_le_lt : forall r1 r2, ~ r1 <= r2 -> r2 < r1. Proof. intros r1 r2; generalize (Rtotal_order r1 r2); unfold Rle in |- *; tauto. Qed. - Hint Immediate Rnot_le_lt: real. +Lemma Rnot_ge_gt : forall r1 r2, ~ r1 >= r2 -> r2 > r1. +Proof. intros; red; apply Rnot_le_lt. auto with real. Qed. + +Lemma Rnot_le_gt : forall r1 r2, ~ r1 <= r2 -> r1 > r2. +Proof. intros; red; apply Rnot_le_lt. auto with real. Qed. + Lemma Rnot_ge_lt : forall r1 r2, ~ r1 >= r2 -> r1 < r2. +Proof. intros; apply Rnot_le_lt. auto with real. Qed. + +Lemma Rnot_lt_le : forall r1 r2, ~ r1 < r2 -> r2 <= r1. Proof. - intros; apply Rnot_le_lt; auto with real. + intros r1 r2 H; destruct (Rtotal_order r1 r2) as [ | [ H0 | H0 ] ]. + contradiction. subst; auto with rorders. auto with real. Qed. +Lemma Rnot_gt_le : forall r1 r2, ~ r1 > r2 -> r1 <= r2. +Proof. auto using Rnot_lt_le with real. Qed. + +Lemma Rnot_gt_ge : forall r1 r2, ~ r1 > r2 -> r2 >= r1. +Proof. intros; eauto using Rnot_lt_le with rorders. Qed. + +Lemma Rnot_lt_ge : forall r1 r2, ~ r1 < r2 -> r1 >= r2. +Proof. eauto using Rnot_gt_ge with rorders. Qed. + (**********) Lemma Rlt_not_le : forall r1 r2, r2 < r1 -> ~ r1 <= r2. Proof. generalize Rlt_asym Rlt_dichotomy_converse; unfold Rle in |- *. intuition eauto 3. Qed. +Hint Immediate Rlt_not_le: real. Lemma Rgt_not_le : forall r1 r2, r1 > r2 -> ~ r1 <= r2. -Proof Rlt_not_le. +Proof. exact Rlt_not_le. Qed. -Hint Immediate Rlt_not_le: real. +Lemma Rlt_not_ge : forall r1 r2, r1 < r2 -> ~ r1 >= r2. +Proof. red; intros; eapply Rlt_not_le; eauto with real. Qed. +Hint Immediate Rlt_not_ge: real. + +Lemma Rgt_not_ge : forall r1 r2, r2 > r1 -> ~ r1 >= r2. +Proof. exact Rlt_not_ge. Qed. Lemma Rle_not_lt : forall r1 r2, r2 <= r1 -> ~ r1 < r2. Proof. @@ -139,13 +196,14 @@ Proof. unfold Rle in |- *; intuition. Qed. -(**********) -Lemma Rlt_not_ge : forall r1 r2, r1 < r2 -> ~ r1 >= r2. -Proof. - generalize Rlt_not_le. unfold Rle, Rge in |- *. intuition eauto 3. -Qed. +Lemma Rge_not_lt : forall r1 r2, r1 >= r2 -> ~ r1 < r2. +Proof. intros; apply Rle_not_lt; auto with real. Qed. -Hint Immediate Rlt_not_ge: real. +Lemma Rle_not_gt : forall r1 r2, r1 <= r2 -> ~ r1 > r2. +Proof. do 2 intro; apply Rle_not_lt. Qed. + +Lemma Rge_not_gt : forall r1 r2, r2 >= r1 -> ~ r1 > r2. +Proof. do 2 intro; apply Rge_not_lt. Qed. (**********) Lemma Req_le : forall r1 r2, r1 = r2 -> r1 <= r2. @@ -172,25 +230,51 @@ Proof. Qed. Hint Immediate Req_ge_sym: real. +(** *** Asymmetry *) + +(** Remark: [Rlt_asym] is an axiom *) + +Lemma Rgt_asym : forall r1 r2:R, r1 > r2 -> ~ r2 > r1. +Proof. do 2 intro; apply Rlt_asym. Qed. + +(** *** Antisymmetry *) + Lemma Rle_antisym : forall r1 r2, r1 <= r2 -> r2 <= r1 -> r1 = r2. Proof. intros r1 r2; generalize (Rlt_asym r1 r2); unfold Rle in |- *; intuition. Qed. Hint Resolve Rle_antisym: real. +Lemma Rge_antisym : forall r1 r2, r1 >= r2 -> r2 >= r1 -> r1 = r2. +Proof. auto with real. Qed. + (**********) Lemma Rle_le_eq : forall r1 r2, r1 <= r2 /\ r2 <= r1 <-> r1 = r2. Proof. intuition. Qed. +Lemma Rge_ge_eq : forall r1 r2, r1 >= r2 /\ r2 >= r1 <-> r1 = r2. +Proof. + intuition. +Qed. + +(** *** Compatibility with equality *) + Lemma Rlt_eq_compat : forall r1 r2 r3 r4, r1 = r2 -> r2 < r4 -> r4 = r3 -> r1 < r3. Proof. intros x x' y y'; intros; replace x with x'; replace y with y'; assumption. Qed. -(**********) +Lemma Rgt_eq_compat : + forall r1 r2 r3 r4, r1 = r2 -> r2 > r4 -> r4 = r3 -> r1 > r3. +Proof. intros; red; apply Rlt_eq_compat with (r2:=r4) (r4:=r2); auto. Qed. + +(** *** Transitivity *) + +(** Remark: [Rlt_trans] is an axiom *) + Lemma Rle_trans : forall r1 r2 r3, r1 <= r2 -> r2 <= r3 -> r1 <= r3. Proof. generalize trans_eq Rlt_trans Rlt_eq_compat. @@ -198,6 +282,12 @@ Proof. intuition eauto 2. Qed. +Lemma Rge_trans : forall r1 r2 r3, r1 >= r2 -> r2 >= r3 -> r1 >= r3. +Proof. eauto using Rle_trans with rorders. Qed. + +Lemma Rgt_trans : forall r1 r2 r3, r1 > r2 -> r2 > r3 -> r1 > r3. +Proof. eauto using Rlt_trans with rorders. Qed. + (**********) Lemma Rle_lt_trans : forall r1 r2 r3, r1 <= r2 -> r2 < r3 -> r1 < r3. Proof. @@ -206,21 +296,25 @@ Proof. intuition eauto 2. Qed. -(**********) Lemma Rlt_le_trans : forall r1 r2 r3, r1 < r2 -> r2 <= r3 -> r1 < r3. Proof. generalize Rlt_trans Rlt_eq_compat; unfold Rle in |- *; intuition eauto 2. Qed. +Lemma Rge_gt_trans : forall r1 r2 r3, r1 >= r2 -> r2 > r3 -> r1 > r3. +Proof. eauto using Rlt_le_trans with rorders. Qed. + +Lemma Rgt_ge_trans : forall r1 r2 r3, r1 > r2 -> r2 >= r3 -> r1 > r3. +Proof. eauto using Rle_lt_trans with rorders. Qed. + +(** *** (Classical) decidability *) -(** Decidability of the order *) Lemma Rlt_dec : forall r1 r2, {r1 < r2} + {~ r1 < r2}. Proof. intros; generalize (total_order_T r1 r2) (Rlt_dichotomy_converse r1 r2); intuition. Qed. -(**********) Lemma Rle_dec : forall r1 r2, {r1 <= r2} + {~ r1 <= r2}. Proof. intros r1 r2. @@ -228,28 +322,44 @@ Proof. intuition eauto 4 with real. Qed. -(**********) Lemma Rgt_dec : forall r1 r2, {r1 > r2} + {~ r1 > r2}. -Proof. - intros; unfold Rgt in |- *; intros; apply Rlt_dec. -Qed. +Proof. do 2 intro; apply Rlt_dec. Qed. -(**********) Lemma Rge_dec : forall r1 r2, {r1 >= r2} + {~ r1 >= r2}. +Proof. intros; edestruct Rle_dec; [left|right]; eauto with rorders. Qed. + +Lemma Rlt_le_dec : forall r1 r2, {r1 < r2} + {r2 <= r1}. Proof. - intros; generalize (Rle_dec r2 r1); intuition. + intros; generalize (total_order_T r1 r2); intuition. Qed. -Lemma Rlt_le_dec : forall r1 r2, {r1 < r2} + {r2 <= r1}. +Lemma Rgt_ge_dec : forall r1 r2, {r1 > r2} + {r2 >= r1}. +Proof. intros; edestruct Rlt_le_dec; [left|right]; eauto with rorders. Qed. + +Lemma Rle_lt_dec : forall r1 r2, {r1 <= r2} + {r2 < r1}. Proof. intros; generalize (total_order_T r1 r2); intuition. Qed. +Lemma Rge_gt_dec : forall r1 r2, {r1 >= r2} + {r2 > r1}. +Proof. intros; edestruct Rle_lt_dec; [left|right]; eauto with rorders. Qed. + +Lemma Rlt_or_le : forall r1 r2, r1 < r2 \/ r2 <= r1. +Proof. + intros n m; elim (Rle_lt_dec m n); auto with real. +Qed. + +Lemma Rgt_or_ge : forall r1 r2, r1 > r2 \/ r2 >= r1. +Proof. intros; edestruct Rlt_or_le; [left|right]; eauto with rorders. Qed. + Lemma Rle_or_lt : forall r1 r2, r1 <= r2 \/ r2 < r1. Proof. intros n m; elim (Rlt_le_dec m n); auto with real. Qed. +Lemma Rge_or_gt : forall r1 r2, r1 >= r2 \/ r2 > r1. +Proof. intros; edestruct Rle_or_lt; [left|right]; eauto with rorders. Qed. + Lemma Rle_lt_or_eq_dec : forall r1 r2, r1 <= r2 -> {r1 < r2} + {r1 = r2}. Proof. intros r1 r2 H; generalize (total_order_T r1 r2); intuition. @@ -262,19 +372,11 @@ Proof. intros n m p q; intros; generalize (Rlt_le_dec m q); intuition. Qed. -(****************************************************************) -(** * Field Lemmas *) -(* This part contains lemma involving the Fields operations *) -(****************************************************************) (*********************************************************) -(** ** Addition *) +(** ** Addition *) (*********************************************************) -Lemma Rplus_ne : forall r, r + 0 = r /\ 0 + r = r. -Proof. - split; ring. -Qed. -Hint Resolve Rplus_ne: real v62. +(** Remark: [Rplus_0_l] is an axiom *) Lemma Rplus_0_r : forall r, r + 0 = r. Proof. @@ -282,14 +384,22 @@ Proof. Qed. Hint Resolve Rplus_0_r: real. +Lemma Rplus_ne : forall r, r + 0 = r /\ 0 + r = r. +Proof. + split; ring. +Qed. +Hint Resolve Rplus_ne: real v62. + (**********) + +(** Remark: [Rplus_opp_r] is an axiom *) + Lemma Rplus_opp_l : forall r, - r + r = 0. Proof. intro; ring. Qed. Hint Resolve Rplus_opp_l: real. - (**********) Lemma Rplus_opp_r_uniq : forall r1 r2, r1 + r2 = 0 -> r2 = - r1. Proof. @@ -298,7 +408,6 @@ Proof. rewrite Rplus_assoc; rewrite H; ring. Qed. -(*i New i*) Hint Resolve (f_equal (A:=R)): real. Lemma Rplus_eq_compat_l : forall r r1 r2, r1 = r2 -> r + r1 = r + r2. @@ -325,9 +434,31 @@ Proof. intros r b; pattern r at 2 in |- *; replace r with (r + 0); eauto with real. Qed. -(***********************************************************) -(** ** Multiplication *) -(***********************************************************) +(***********) +Lemma Rplus_eq_0_l : + forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0. +Proof. + intros a b H [H0| H0] H1; auto with real. + absurd (0 < a + b). + rewrite H1; auto with real. + apply Rle_lt_trans with (a + 0). + rewrite Rplus_0_r in |- *; assumption. + auto using Rplus_lt_compat_l with real. + rewrite <- H0, Rplus_0_r in H1; assumption. +Qed. + +Lemma Rplus_eq_R0 : + forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0 /\ r2 = 0. +Proof. + intros a b; split. + apply Rplus_eq_0_l with b; auto with real. + apply Rplus_eq_0_l with a; auto with real. + rewrite Rplus_comm; auto with real. +Qed. + +(*********************************************************) +(** ** Multiplication *) +(*********************************************************) (**********) Lemma Rinv_r : forall r, r <> 0 -> r * / r = 1. @@ -340,13 +471,13 @@ Lemma Rinv_l_sym : forall r, r <> 0 -> 1 = / r * r. Proof. intros; field; trivial. Qed. +Hint Resolve Rinv_l_sym: real. Lemma Rinv_r_sym : forall r, r <> 0 -> 1 = r * / r. Proof. intros; field; trivial. Qed. -Hint Resolve Rinv_l_sym Rinv_r_sym: real. - +Hint Resolve Rinv_r_sym: real. (**********) Lemma Rmult_0_r : forall r, r * 0 = 0. @@ -382,7 +513,7 @@ Proof. auto with real. Qed. -(*i OLD i*)Hint Resolve Rmult_eq_compat_l: v62. +(*i Old i*)Hint Resolve Rmult_eq_compat_l: v62. (**********) Lemma Rmult_eq_reg_l : forall r r1 r2, r * r1 = r * r2 -> r <> 0 -> r1 = r2. @@ -423,7 +554,6 @@ Proof. auto with real. Qed. - (**********) Lemma Rmult_neq_0_reg : forall r1 r2, r1 * r2 <> 0 -> r1 <> 0 /\ r2 <> 0. Proof. @@ -439,6 +569,10 @@ Proof. Qed. Hint Resolve Rmult_integral_contrapositive: real. +Lemma Rmult_integral_contrapositive_currified : + forall r1 r2, r1 <> 0 -> r2 <> 0 -> r1 * r2 <> 0. +Proof. auto using Rmult_integral_contrapositive. Qed. + (**********) Lemma Rmult_plus_distr_r : forall r1 r2 r3, (r1 + r2) * r3 = r1 * r3 + r2 * r3. @@ -446,11 +580,15 @@ Proof. intros; ring. Qed. -(** ** Square function *) +(*********************************************************) +(** ** Square function *) +(*********************************************************) (***********) Definition Rsqr r : R := r * r. +Notation "r ²" := (Rsqr r) (at level 1, format "r ²") : R_scope. + (***********) Lemma Rsqr_0 : Rsqr 0 = 0. unfold Rsqr in |- *; auto with real. @@ -462,7 +600,7 @@ Lemma Rsqr_0_uniq : forall r, Rsqr r = 0 -> r = 0. Qed. (*********************************************************) -(** ** Opposite *) +(** ** Opposite *) (*********************************************************) (**********) @@ -509,8 +647,9 @@ Proof. Qed. Hint Resolve Ropp_plus_distr: real. - -(** ** Opposite and multiplication *) +(*********************************************************) +(** ** Opposite and multiplication *) +(*********************************************************) Lemma Ropp_mult_distr_l_reverse : forall r1 r2, - r1 * r2 = - (r1 * r2). Proof. @@ -530,7 +669,9 @@ Proof. intros; ring. Qed. -(** ** Substraction *) +(*********************************************************) +(** ** Substraction *) +(*********************************************************) Lemma Rminus_0_r : forall r, r - 0 = r. Proof. @@ -555,7 +696,6 @@ Lemma Ropp_minus_distr' : forall r1 r2, - (r2 - r1) = r1 - r2. Proof. intros; ring. Qed. -Hint Resolve Ropp_minus_distr': real. (**********) Lemma Rminus_diag_eq : forall r1 r2, r1 = r2 -> r1 - r2 = 0. @@ -605,7 +745,6 @@ Proof. Qed. Hint Resolve Rminus_not_eq_right: real. - (**********) Lemma Rmult_minus_distr_l : forall r1 r2 r3, r1 * (r2 - r3) = r1 * r2 - r1 * r3. @@ -613,7 +752,10 @@ Proof. intros; ring. Qed. -(** ** Inverse *) +(*********************************************************) +(** ** Inverse *) +(*********************************************************) + Lemma Rinv_1 : / 1 = 1. Proof. field. @@ -677,28 +819,28 @@ Proof. ring. Qed. -(** * Field operations and order *) +(*********************************************************) +(** ** Order and addition *) +(*********************************************************) + +(** *** Compatibility *) -(** ** Order and addition *) +(** Remark: [Rplus_lt_compat_l] is an axiom *) +Lemma Rplus_gt_compat_l : forall r r1 r2, r1 > r2 -> r + r1 > r + r2. +Proof. eauto using Rplus_lt_compat_l with rorders. Qed. +Hint Resolve Rplus_gt_compat_l: real. + +(**********) Lemma Rplus_lt_compat_r : forall r r1 r2, r1 < r2 -> r1 + r < r2 + r. Proof. intros. rewrite (Rplus_comm r1 r); rewrite (Rplus_comm r2 r); auto with real. Qed. - Hint Resolve Rplus_lt_compat_r: real. -(**********) -Lemma Rplus_lt_reg_r : forall r r1 r2, r + r1 < r + r2 -> r1 < r2. -Proof. - intros; cut (- r + r + r1 < - r + r + r2). - rewrite Rplus_opp_l. - elim (Rplus_ne r1); elim (Rplus_ne r2); intros; rewrite <- H3; rewrite <- H1; - auto with zarith real. - rewrite Rplus_assoc; rewrite Rplus_assoc; - apply (Rplus_lt_compat_l (- r) (r + r1) (r + r2) H). -Qed. +Lemma Rplus_gt_compat_r : forall r r1 r2, r1 > r2 -> r1 + r > r2 + r. +Proof. do 3 intro; apply Rplus_lt_compat_r. Qed. (**********) Lemma Rplus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2. @@ -708,6 +850,10 @@ Proof. right; rewrite <- H0; auto with zarith real. Qed. +Lemma Rplus_ge_compat_l : forall r r1 r2, r1 >= r2 -> r + r1 >= r + r2. +Proof. auto using Rplus_le_compat_l with rorders. Qed. +Hint Resolve Rplus_ge_compat_l: real. + (**********) Lemma Rplus_le_compat_r : forall r r1 r2, r1 <= r2 -> r1 + r <= r2 + r. Proof. @@ -718,23 +864,8 @@ Qed. Hint Resolve Rplus_le_compat_l Rplus_le_compat_r: real. -(**********) -Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2. -Proof. - unfold Rle in |- *; intros; elim H; intro. - left; apply (Rplus_lt_reg_r r r1 r2 H0). - right; apply (Rplus_eq_reg_l r r1 r2 H0). -Qed. - -(**********) -Lemma sum_inequa_Rle_lt : - forall a x b c y d:R, - a <= x -> x < b -> c < y -> y <= d -> a + c < x + y < b + d. -Proof. - intros; split. - apply Rlt_le_trans with (a + y); auto with real. - apply Rlt_le_trans with (b + y); auto with real. -Qed. +Lemma Rplus_ge_compat_r : forall r r1 r2, r1 >= r2 -> r1 + r >= r2 + r. +Proof. auto using Rplus_le_compat_r with rorders. Qed. (*********) Lemma Rplus_lt_compat : @@ -742,12 +873,22 @@ Lemma Rplus_lt_compat : Proof. intros; apply Rlt_trans with (r2 + r3); auto with real. Qed. +Hint Immediate Rplus_lt_compat: real. Lemma Rplus_le_compat : forall r1 r2 r3 r4, r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4. Proof. intros; apply Rle_trans with (r2 + r3); auto with real. Qed. +Hint Immediate Rplus_le_compat: real. + +Lemma Rplus_gt_compat : + forall r1 r2 r3 r4, r1 > r2 -> r3 > r4 -> r1 + r3 > r2 + r4. +Proof. auto using Rplus_lt_compat with rorders. Qed. + +Lemma Rplus_ge_compat : + forall r1 r2 r3 r4, r1 >= r2 -> r3 >= r4 -> r1 + r3 >= r2 + r4. +Proof. auto using Rplus_le_compat with rorders. Qed. (*********) Lemma Rplus_lt_le_compat : @@ -756,19 +897,133 @@ Proof. intros; apply Rlt_le_trans with (r2 + r3); auto with real. Qed. -(*********) Lemma Rplus_le_lt_compat : forall r1 r2 r3 r4, r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4. Proof. intros; apply Rle_lt_trans with (r2 + r3); auto with real. Qed. -Hint Immediate Rplus_lt_compat Rplus_le_compat Rplus_lt_le_compat - Rplus_le_lt_compat: real. +Hint Immediate Rplus_lt_le_compat Rplus_le_lt_compat: real. + +Lemma Rplus_gt_ge_compat : + forall r1 r2 r3 r4, r1 > r2 -> r3 >= r4 -> r1 + r3 > r2 + r4. +Proof. auto using Rplus_lt_le_compat with rorders. Qed. + +Lemma Rplus_ge_gt_compat : + forall r1 r2 r3 r4, r1 >= r2 -> r3 > r4 -> r1 + r3 > r2 + r4. +Proof. auto using Rplus_le_lt_compat with rorders. Qed. + +(**********) +Lemma Rplus_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 + r2. +Proof. + intros x y; intros; apply Rlt_trans with x; + [ assumption + | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l; + assumption ]. +Qed. + +Lemma Rplus_le_lt_0_compat : forall r1 r2, 0 <= r1 -> 0 < r2 -> 0 < r1 + r2. +Proof. + intros x y; intros; apply Rle_lt_trans with x; + [ assumption + | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l; + assumption ]. +Qed. + +Lemma Rplus_lt_le_0_compat : forall r1 r2, 0 < r1 -> 0 <= r2 -> 0 < r1 + r2. +Proof. + intros x y; intros; rewrite <- Rplus_comm; apply Rplus_le_lt_0_compat; + assumption. +Qed. -(** ** Order and Opposite *) +Lemma Rplus_le_le_0_compat : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2. +Proof. + intros x y; intros; apply Rle_trans with x; + [ assumption + | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; + assumption ]. +Qed. (**********) +Lemma sum_inequa_Rle_lt : + forall a x b c y d:R, + a <= x -> x < b -> c < y -> y <= d -> a + c < x + y < b + d. +Proof. + intros; split. + apply Rlt_le_trans with (a + y); auto with real. + apply Rlt_le_trans with (b + y); auto with real. +Qed. + +(** *** Cancellation *) + +Lemma Rplus_lt_reg_r : forall r r1 r2, r + r1 < r + r2 -> r1 < r2. +Proof. + intros; cut (- r + r + r1 < - r + r + r2). + rewrite Rplus_opp_l. + elim (Rplus_ne r1); elim (Rplus_ne r2); intros; rewrite <- H3; rewrite <- H1; + auto with zarith real. + rewrite Rplus_assoc; rewrite Rplus_assoc; + apply (Rplus_lt_compat_l (- r) (r + r1) (r + r2) H). +Qed. + +Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2. +Proof. + unfold Rle in |- *; intros; elim H; intro. + left; apply (Rplus_lt_reg_r r r1 r2 H0). + right; apply (Rplus_eq_reg_l r r1 r2 H0). +Qed. + +Lemma Rplus_gt_reg_l : forall r r1 r2, r + r1 > r + r2 -> r1 > r2. +Proof. + unfold Rgt in |- *; intros; apply (Rplus_lt_reg_r r r2 r1 H). +Qed. + +Lemma Rplus_ge_reg_l : forall r r1 r2, r + r1 >= r + r2 -> r1 >= r2. +Proof. + intros; apply Rle_ge; apply Rplus_le_reg_l with r; auto with real. +Qed. + +(**********) +Lemma Rplus_le_reg_pos_r : + forall r1 r2 r3, 0 <= r2 -> r1 + r2 <= r3 -> r1 <= r3. +Proof. + intros x y z; intros; apply Rle_trans with (x + y); + [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; + assumption + | assumption ]. +Qed. + +Lemma Rplus_lt_reg_pos_r : forall r1 r2 r3, 0 <= r2 -> r1 + r2 < r3 -> r1 < r3. +Proof. + intros x y z; intros; apply Rle_lt_trans with (x + y); + [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; + assumption + | assumption ]. +Qed. + +Lemma Rplus_ge_reg_neg_r : + forall r1 r2 r3, 0 >= r2 -> r1 + r2 >= r3 -> r1 >= r3. +Proof. + intros x y z; intros; apply Rge_trans with (x + y); + [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_ge_compat_l; + assumption + | assumption ]. +Qed. + +Lemma Rplus_gt_reg_neg_r : forall r1 r2 r3, 0 >= r2 -> r1 + r2 > r3 -> r1 > r3. +Proof. + intros x y z; intros; apply Rge_gt_trans with (x + y); + [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_ge_compat_l; + assumption + | assumption ]. +Qed. + +(*********************************************************) +(** ** Order and opposite *) +(*********************************************************) + +(** *** Contravariant compatibility *) + Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2. Proof. unfold Rgt in |- *; intros. @@ -781,55 +1036,44 @@ Proof. Qed. Hint Resolve Ropp_gt_lt_contravar. -(**********) Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2. Proof. unfold Rgt in |- *; auto with real. Qed. Hint Resolve Ropp_lt_gt_contravar: real. -Lemma Ropp_lt_cancel : forall r1 r2, - r2 < - r1 -> r1 < r2. -Proof. - intros x y H'. - rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y); - auto with real. -Qed. -Hint Immediate Ropp_lt_cancel: real. - +(**********) Lemma Ropp_lt_contravar : forall r1 r2, r2 < r1 -> - r1 < - r2. Proof. auto with real. Qed. Hint Resolve Ropp_lt_contravar: real. +Lemma Ropp_gt_contravar : forall r1 r2, r2 > r1 -> - r1 > - r2. +Proof. auto with real. Qed. + (**********) Lemma Ropp_le_ge_contravar : forall r1 r2, r1 <= r2 -> - r1 >= - r2. Proof. - unfold Rge in |- *; intros r1 r2 [H| H]; auto with real. + unfold Rge; intros r1 r2 [H| H]; auto with real. Qed. Hint Resolve Ropp_le_ge_contravar: real. -Lemma Ropp_le_cancel : forall r1 r2, - r2 <= - r1 -> r1 <= r2. +Lemma Ropp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2. Proof. - intros x y H. - elim H; auto with real. - intro H1; rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y); - rewrite H1; auto with real. + unfold Rle; intros r1 r2 [H| H]; auto with real. Qed. -Hint Immediate Ropp_le_cancel: real. +Hint Resolve Ropp_ge_le_contravar: real. +(**********) Lemma Ropp_le_contravar : forall r1 r2, r2 <= r1 -> - r1 <= - r2. Proof. intros r1 r2 H; elim H; auto with real. Qed. Hint Resolve Ropp_le_contravar: real. -(**********) -Lemma Ropp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2. -Proof. - unfold Rge in |- *; intros r1 r2 [H| H]; auto with real. -Qed. -Hint Resolve Ropp_ge_le_contravar: real. +Lemma Ropp_ge_contravar : forall r1 r2, r2 >= r1 -> - r1 >= - r2. +Proof. auto using Ropp_le_contravar with real. Qed. (**********) Lemma Ropp_0_lt_gt_contravar : forall r, 0 < r -> 0 > - r. @@ -838,7 +1082,6 @@ Proof. Qed. Hint Resolve Ropp_0_lt_gt_contravar: real. -(**********) Lemma Ropp_0_gt_lt_contravar : forall r, 0 > r -> 0 < - r. Proof. intros; replace 0 with (-0); auto with real. @@ -850,13 +1093,13 @@ Lemma Ropp_lt_gt_0_contravar : forall r, r > 0 -> - r < 0. Proof. intros; rewrite <- Ropp_0; auto with real. Qed. +Hint Resolve Ropp_lt_gt_0_contravar: real. -(**********) Lemma Ropp_gt_lt_0_contravar : forall r, r < 0 -> - r > 0. Proof. intros; rewrite <- Ropp_0; auto with real. Qed. -Hint Resolve Ropp_lt_gt_0_contravar Ropp_gt_lt_0_contravar: real. +Hint Resolve Ropp_gt_lt_0_contravar: real. (**********) Lemma Ropp_0_le_ge_contravar : forall r, 0 <= r -> 0 >= - r. @@ -865,40 +1108,56 @@ Proof. Qed. Hint Resolve Ropp_0_le_ge_contravar: real. -(**********) Lemma Ropp_0_ge_le_contravar : forall r, 0 >= r -> 0 <= - r. Proof. intros; replace 0 with (-0); auto with real. Qed. Hint Resolve Ropp_0_ge_le_contravar: real. -(** ** Order and multiplication *) +(** *** Cancellation *) -Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r. +Lemma Ropp_lt_cancel : forall r1 r2, - r2 < - r1 -> r1 < r2. Proof. - intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with real. + intros x y H'. + rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y); + auto with real. Qed. -Hint Resolve Rmult_lt_compat_r. +Hint Immediate Ropp_lt_cancel: real. -Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2. +Lemma Ropp_gt_cancel : forall r1 r2, - r2 > - r1 -> r1 > r2. +Proof. auto using Ropp_lt_cancel with rorders. Qed. + +Lemma Ropp_le_cancel : forall r1 r2, - r2 <= - r1 -> r1 <= r2. Proof. - intros z x y H H0. - case (Rtotal_order x y); intros Eq0; auto; elim Eq0; clear Eq0; intros Eq0. - rewrite Eq0 in H0; elimtype False; apply (Rlt_irrefl (z * y)); auto. - generalize (Rmult_lt_compat_l z y x H Eq0); intro; elimtype False; - generalize (Rlt_trans (z * x) (z * y) (z * x) H0 H1); - intro; apply (Rlt_irrefl (z * x)); auto. + intros x y H. + elim H; auto with real. + intro H1; rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y); + rewrite H1; auto with real. Qed. +Hint Immediate Ropp_le_cancel: real. +Lemma Ropp_ge_cancel : forall r1 r2, - r2 >= - r1 -> r1 >= r2. +Proof. auto using Ropp_le_cancel with rorders. Qed. -Lemma Rmult_lt_gt_compat_neg_l : - forall r r1 r2, r < 0 -> r1 < r2 -> r * r1 > r * r2. +(*********************************************************) +(** ** Order and multiplication *) +(*********************************************************) + +(** Remark: [Rmult_lt_compat_l] is an axiom *) + +(** *** Covariant compatibility *) + +Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r. Proof. - intros; replace r with (- - r); auto with real. - rewrite (Ropp_mult_distr_l_reverse (- r)); - rewrite (Ropp_mult_distr_l_reverse (- r)). - apply Ropp_lt_gt_contravar; auto with real. + intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with real. Qed. +Hint Resolve Rmult_lt_compat_r. + +Lemma Rmult_gt_compat_r : forall r r1 r2, r > 0 -> r1 > r2 -> r1 * r > r2 * r. +Proof. eauto using Rmult_lt_compat_r with rorders. Qed. + +Lemma Rmult_gt_compat_l : forall r r1 r2, r > 0 -> r1 > r2 -> r * r1 > r * r2. +Proof. eauto using Rmult_lt_compat_l with rorders. Qed. (**********) Lemma Rmult_le_compat_l : @@ -918,18 +1177,59 @@ Proof. Qed. Hint Resolve Rmult_le_compat_r: real. -Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2. +Lemma Rmult_ge_compat_l : + forall r r1 r2, r >= 0 -> r1 >= r2 -> r * r1 >= r * r2. +Proof. eauto using Rmult_le_compat_l with rorders. Qed. + +Lemma Rmult_ge_compat_r : + forall r r1 r2, r >= 0 -> r1 >= r2 -> r1 * r >= r2 * r. +Proof. eauto using Rmult_le_compat_r with rorders. Qed. + +(**********) +Lemma Rmult_le_compat : + forall r1 r2 r3 r4, + 0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4. Proof. - intros z x y H H0; case H0; auto with real. - intros H1; apply Rlt_le. - apply Rmult_lt_reg_l with (r := z); auto. - intros H1; replace x with (/ z * (z * x)); auto with real. - replace y with (/ z * (z * y)). - rewrite H1; auto with real. - rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real. - rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real. + intros x y z t H' H'0 H'1 H'2. + apply Rle_trans with (r2 := x * t); auto with real. + repeat rewrite (fun x => Rmult_comm x t). + apply Rmult_le_compat_l; auto. + apply Rle_trans with z; auto. +Qed. +Hint Resolve Rmult_le_compat: real. + +Lemma Rmult_ge_compat : + forall r1 r2 r3 r4, + 0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4. +Proof. auto with real rorders. Qed. + +Lemma Rmult_gt_0_lt_compat : + forall r1 r2 r3 r4, + r3 > 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. +Proof. + intros; apply Rlt_trans with (r2 * r3); auto with real. +Qed. + +(*********) +Lemma Rmult_le_0_lt_compat : + forall r1 r2 r3 r4, + 0 <= r1 -> 0 <= r3 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. +Proof. + intros; apply Rle_lt_trans with (r2 * r3); + [ apply Rmult_le_compat_r; [ assumption | left; assumption ] + | apply Rmult_lt_compat_l; + [ apply Rle_lt_trans with r1; assumption | assumption ] ]. Qed. +(*********) +Lemma Rmult_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 * r2. +Proof. intros; replace 0 with (0 * r2); auto with real. Qed. + +Lemma Rmult_gt_0_compat : forall r1 r2, r1 > 0 -> r2 > 0 -> r1 * r2 > 0. +Proof Rmult_lt_0_compat. + +(** *** Contravariant compatibility *) + Lemma Rmult_le_compat_neg_l : forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r2 <= r * r1. Proof. @@ -946,35 +1246,45 @@ Proof. Qed. Hint Resolve Rmult_le_ge_compat_neg_l: real. -Lemma Rmult_le_compat : - forall r1 r2 r3 r4, - 0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4. +Lemma Rmult_lt_gt_compat_neg_l : + forall r r1 r2, r < 0 -> r1 < r2 -> r * r1 > r * r2. Proof. - intros x y z t H' H'0 H'1 H'2. - apply Rle_trans with (r2 := x * t); auto with real. - repeat rewrite (fun x => Rmult_comm x t). - apply Rmult_le_compat_l; auto. - apply Rle_trans with z; auto. + intros; replace r with (- - r); auto with real. + rewrite (Ropp_mult_distr_l_reverse (- r)); + rewrite (Ropp_mult_distr_l_reverse (- r)). + apply Ropp_lt_gt_contravar; auto with real. Qed. -Hint Resolve Rmult_le_compat: real. -Lemma Rmult_gt_0_lt_compat : - forall r1 r2 r3 r4, - r3 > 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. +(** *** Cancellation *) + +Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2. Proof. - intros; apply Rlt_trans with (r2 * r3); auto with real. + intros z x y H H0. + case (Rtotal_order x y); intros Eq0; auto; elim Eq0; clear Eq0; intros Eq0. + rewrite Eq0 in H0; elimtype False; apply (Rlt_irrefl (z * y)); auto. + generalize (Rmult_lt_compat_l z y x H Eq0); intro; elimtype False; + generalize (Rlt_trans (z * x) (z * y) (z * x) H0 H1); + intro; apply (Rlt_irrefl (z * x)); auto. Qed. -(*********) -Lemma Rmult_ge_0_gt_0_lt_compat : - forall r1 r2 r3 r4, - r3 >= 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. +Lemma Rmult_gt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2. +Proof. eauto using Rmult_lt_reg_l with rorders. Qed. + +Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2. Proof. - intros; apply Rle_lt_trans with (r2 * r3); auto with real. + intros z x y H H0; case H0; auto with real. + intros H1; apply Rlt_le. + apply Rmult_lt_reg_l with (r := z); auto. + intros H1; replace x with (/ z * (z * x)); auto with real. + replace y with (/ z * (z * y)). + rewrite H1; auto with real. + rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real. + rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real. Qed. - -(** ** Order and Substractions *) +(*********************************************************) +(** ** Order and substraction *) +(*********************************************************) Lemma Rlt_minus : forall r1 r2, r1 < r2 -> r1 - r2 < 0. Proof. @@ -985,12 +1295,27 @@ Proof. Qed. Hint Resolve Rlt_minus: real. +Lemma Rgt_minus : forall r1 r2, r1 > r2 -> r1 - r2 > 0. +Proof. + intros; apply (Rplus_lt_reg_r r2). + replace (r2 + (r1 - r2)) with r1. + replace (r2 + 0) with r2; auto with real. + ring. +Qed. + (**********) Lemma Rle_minus : forall r1 r2, r1 <= r2 -> r1 - r2 <= 0. Proof. destruct 1; unfold Rle in |- *; auto with real. Qed. +Lemma Rge_minus : forall r1 r2, r1 >= r2 -> r1 - r2 >= 0. +Proof. + destruct 1. + auto using Rgt_minus, Rgt_ge. + right; auto using Rminus_diag_eq with rorders. +Qed. + (**********) Lemma Rminus_lt : forall r1 r2, r1 - r2 < 0 -> r1 < r2. Proof. @@ -999,6 +1324,14 @@ Proof. ring. Qed. +Lemma Rminus_gt : forall r1 r2, r1 - r2 > 0 -> r1 > r2. +Proof. + intros; replace r2 with (0 + r2); auto with real. + replace r1 with (r1 - r2 + r2). + apply Rplus_gt_compat_r; assumption. + ring. +Qed. + (**********) Lemma Rminus_le : forall r1 r2, r1 - r2 <= 0 -> r1 <= r2. Proof. @@ -1007,6 +1340,14 @@ Proof. ring. Qed. +Lemma Rminus_ge : forall r1 r2, r1 - r2 >= 0 -> r1 >= r2. +Proof. + intros; replace r2 with (0 + r2); auto with real. + replace r1 with (r1 - r2 + r2). + apply Rplus_ge_compat_r; assumption. + ring. +Qed. + (**********) Lemma tech_Rplus : forall r (s:R), 0 <= r -> 0 < s -> r + s <> 0. Proof. @@ -1015,8 +1356,9 @@ Proof. Qed. Hint Immediate tech_Rplus: real. - -(** ** Order and the square function *) +(*********************************************************) +(** ** Order and square function *) +(*********************************************************) Lemma Rle_0_sqr : forall r, 0 <= Rsqr r. Proof. @@ -1036,7 +1378,26 @@ Proof. Qed. Hint Resolve Rle_0_sqr Rlt_0_sqr: real. -(** ** Zero is less than one *) +(***********) +Lemma Rplus_sqr_eq_0_l : forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0. +Proof. + intros a b; intros; apply Rsqr_0_uniq; apply Rplus_eq_0_l with (Rsqr b); + auto with real. +Qed. + +Lemma Rplus_sqr_eq_0 : + forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0 /\ r2 = 0. +Proof. + intros a b; split. + apply Rplus_sqr_eq_0_l with b; auto with real. + apply Rplus_sqr_eq_0_l with a; auto with real. + rewrite Rplus_comm; auto with real. +Qed. + +(*********************************************************) +(** ** Zero is less than one *) +(*********************************************************) + Lemma Rlt_0_1 : 0 < 1. Proof. replace 1 with (Rsqr 1); auto with real. @@ -1050,7 +1411,10 @@ Proof. exact Rlt_0_1. Qed. -(** ** Order and inverse *) +(*********************************************************) +(** ** Order and inverse *) +(*********************************************************) + Lemma Rinv_0_lt_compat : forall r, 0 < r -> 0 < / r. Proof. intros; apply Rnot_le_lt; red in |- *; intros. @@ -1099,68 +1463,9 @@ Proof. Qed. Hint Resolve Rinv_1_lt_contravar: real. -(********************************************************) -(** * Greater *) -(********************************************************) - -(**********) -Lemma Rge_antisym : forall r1 r2, r1 >= r2 -> r2 >= r1 -> r1 = r2. -Proof. - intros; apply Rle_antisym; auto with real. -Qed. - -(**********) -Lemma Rnot_lt_ge : forall r1 r2, ~ r1 < r2 -> r1 >= r2. -Proof. - intros; unfold Rge in |- *; elim (Rtotal_order r1 r2); intro. - absurd (r1 < r2); trivial. - case H0; auto. -Qed. - -(**********) -Lemma Rnot_lt_le : forall r1 r2, ~ r1 < r2 -> r2 <= r1. -Proof. - intros; apply Rge_le; apply Rnot_lt_ge; assumption. -Qed. - -(**********) -Lemma Rnot_gt_le : forall r1 r2, ~ r1 > r2 -> r1 <= r2. -Proof. - intros r1 r2 H; apply Rge_le. - exact (Rnot_lt_ge r2 r1 H). -Qed. - -(**********) -Lemma Rgt_ge : forall r1 r2, r1 > r2 -> r1 >= r2. -Proof. - red in |- *; auto with real. -Qed. - - -(**********) -Lemma Rge_gt_trans : forall r1 r2 r3, r1 >= r2 -> r2 > r3 -> r1 > r3. -Proof. - unfold Rgt in |- *; intros; apply Rlt_le_trans with r2; auto with real. -Qed. - -(**********) -Lemma Rgt_ge_trans : forall r1 r2 r3, r1 > r2 -> r2 >= r3 -> r1 > r3. -Proof. - unfold Rgt in |- *; intros; apply Rle_lt_trans with r2; auto with real. -Qed. - -(**********) -Lemma Rgt_trans : forall r1 r2 r3, r1 > r2 -> r2 > r3 -> r1 > r3. -Proof. - unfold Rgt in |- *; intros; apply Rlt_trans with r2; auto with real. -Qed. - -(**********) -Lemma Rge_trans : forall r1 r2 r3, r1 >= r2 -> r2 >= r3 -> r1 >= r3. -Proof. - intros; apply Rle_ge. - apply Rle_trans with r2; auto with real. -Qed. +(*********************************************************) +(** ** Miscellaneous *) +(*********************************************************) (**********) Lemma Rle_lt_0_plus_1 : forall r, 0 <= r -> 0 < r + 1. @@ -1186,121 +1491,9 @@ Proof. pattern r1 at 2 in |- *; replace r1 with (r1 + 0); auto with real. Qed. -(***********) -Lemma Rplus_gt_compat_l : forall r r1 r2, r1 > r2 -> r + r1 > r + r2. -Proof. - unfold Rgt in |- *; auto with real. -Qed. -Hint Resolve Rplus_gt_compat_l: real. - -(***********) -Lemma Rplus_gt_reg_l : forall r r1 r2, r + r1 > r + r2 -> r1 > r2. -Proof. - unfold Rgt in |- *; intros; apply (Rplus_lt_reg_r r r2 r1 H). -Qed. - -(***********) -Lemma Rplus_ge_compat_l : forall r r1 r2, r1 >= r2 -> r + r1 >= r + r2. -Proof. - intros; apply Rle_ge; auto with real. -Qed. -Hint Resolve Rplus_ge_compat_l: real. - -(***********) -Lemma Rplus_ge_reg_l : forall r r1 r2, r + r1 >= r + r2 -> r1 >= r2. -Proof. - intros; apply Rle_ge; apply Rplus_le_reg_l with r; auto with real. -Qed. - -(***********) -Lemma Rmult_ge_compat_r : - forall r r1 r2, r >= 0 -> r1 >= r2 -> r1 * r >= r2 * r. -Proof. - intros; apply Rle_ge; apply Rmult_le_compat_r; apply Rge_le; assumption. -Qed. - -(***********) -Lemma Rgt_minus : forall r1 r2, r1 > r2 -> r1 - r2 > 0. -Proof. - intros; replace 0 with (r2 - r2); auto with real. - unfold Rgt, Rminus in |- *; auto with real. -Qed. - -(*********) -Lemma minus_Rgt : forall r1 r2, r1 - r2 > 0 -> r1 > r2. -Proof. - intros; replace r2 with (r2 + 0); auto with real. - intros; replace r1 with (r2 + (r1 - r2)); auto with real. -Qed. - -(**********) -Lemma Rge_minus : forall r1 r2, r1 >= r2 -> r1 - r2 >= 0. -Proof. - unfold Rge in |- *; intros; elim H; intro. - left; apply (Rgt_minus r1 r2 H0). - right; apply (Rminus_diag_eq r1 r2 H0). -Qed. - -(*********) -Lemma minus_Rge : forall r1 r2, r1 - r2 >= 0 -> r1 >= r2. -Proof. - intros; replace r2 with (r2 + 0); auto with real. - intros; replace r1 with (r2 + (r1 - r2)); auto with real. -Qed. - - -(*********) -Lemma Rmult_gt_0_compat : forall r1 r2, r1 > 0 -> r2 > 0 -> r1 * r2 > 0. -Proof. - unfold Rgt in |- *; intros. - replace 0 with (0 * r2); auto with real. -Qed. - -(*********) -Lemma Rmult_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 * r2. -Proof Rmult_gt_0_compat. - -(***********) -Lemma Rplus_eq_0_l : - forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0. -Proof. - intros a b [H| H] H0 H1; auto with real. - absurd (0 < a + b). - rewrite H1; auto with real. - replace 0 with (0 + 0); auto with real. -Qed. - - -Lemma Rplus_eq_R0 : - forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0 /\ r2 = 0. -Proof. - intros a b; split. - apply Rplus_eq_0_l with b; auto with real. - apply Rplus_eq_0_l with a; auto with real. - rewrite Rplus_comm; auto with real. -Qed. - - -(***********) -Lemma Rplus_sqr_eq_0_l : forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0. -Proof. - intros a b; intros; apply Rsqr_0_uniq; apply Rplus_eq_0_l with (Rsqr b); - auto with real. -Qed. - -Lemma Rplus_sqr_eq_0 : - forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0 /\ r2 = 0. -Proof. - intros a b; split. - apply Rplus_sqr_eq_0_l with b; auto with real. - apply Rplus_sqr_eq_0_l with a; auto with real. - rewrite Rplus_comm; auto with real. -Qed. - - -(**********************************************************) -(** * Injection from [N] to [R] *) -(**********************************************************) +(*********************************************************) +(** ** Injection from [N] to [R] *) +(*********************************************************) (**********) Lemma S_INR : forall n:nat, INR (S n) = INR n + 1. @@ -1323,6 +1516,7 @@ Proof. repeat rewrite S_INR. rewrite Hrecn; ring. Qed. +Hint Resolve plus_INR: real. (**********) Lemma minus_INR : forall n m:nat, (m <= n)%nat -> INR (n - m) = INR n - INR m. @@ -1332,6 +1526,7 @@ Proof. intros; repeat rewrite S_INR; simpl in |- *. rewrite H0; ring. Qed. +Hint Resolve minus_INR: real. (*********) Lemma mult_INR : forall n m:nat, INR (n * m) = INR n * INR m. @@ -1341,16 +1536,15 @@ Proof. intros; repeat rewrite S_INR; simpl in |- *. rewrite plus_INR; rewrite Hrecn; ring. Qed. - -Hint Resolve plus_INR minus_INR mult_INR: real. +Hint Resolve mult_INR: real. (*********) -Lemma lt_INR_0 : forall n:nat, (0 < n)%nat -> 0 < INR n. +Lemma lt_0_INR : forall n:nat, (0 < n)%nat -> 0 < INR n. Proof. simple induction 1; intros; auto with real. rewrite S_INR; auto with real. Qed. -Hint Resolve lt_INR_0: real. +Hint Resolve lt_0_INR: real. Lemma lt_INR : forall n m:nat, (n < m)%nat -> INR n < INR m. Proof. @@ -1360,20 +1554,20 @@ Proof. Qed. Hint Resolve lt_INR: real. -Lemma INR_lt_1 : forall n:nat, (1 < n)%nat -> 1 < INR n. +Lemma lt_1_INR : forall n:nat, (1 < n)%nat -> 1 < INR n. Proof. intros; replace 1 with (INR 1); auto with real. Qed. -Hint Resolve INR_lt_1: real. +Hint Resolve lt_1_INR: real. (**********) -Lemma INR_pos : forall p:positive, 0 < INR (nat_of_P p). +Lemma pos_INR_nat_of_P : forall p:positive, 0 < INR (nat_of_P p). Proof. - intro; apply lt_INR_0. + intro; apply lt_0_INR. simpl in |- *; auto with real. apply lt_O_nat_of_P. Qed. -Hint Resolve INR_pos: real. +Hint Resolve pos_INR_nat_of_P: real. (**********) Lemma pos_INR : forall n:nat, 0 <= INR n. @@ -1410,25 +1604,25 @@ Qed. Hint Resolve le_INR: real. (**********) -Lemma not_INR_O : forall n:nat, INR n <> 0 -> n <> 0%nat. +Lemma INR_not_0 : forall n:nat, INR n <> 0 -> n <> 0%nat. Proof. red in |- *; intros n H H1. apply H. rewrite H1; trivial. Qed. -Hint Immediate not_INR_O: real. +Hint Immediate INR_not_0: real. (**********) -Lemma not_O_INR : forall n:nat, n <> 0%nat -> INR n <> 0. +Lemma not_0_INR : forall n:nat, n <> 0%nat -> INR n <> 0. Proof. intro n; case n. intro; absurd (0%nat = 0%nat); trivial. intros; rewrite S_INR. apply Rgt_not_eq; red in |- *; auto with real. Qed. -Hint Resolve not_O_INR: real. +Hint Resolve not_0_INR: real. -Lemma not_nm_INR : forall n m:nat, n <> m -> INR n <> INR m. +Lemma not_INR : forall n m:nat, n <> m -> INR n <> INR m. Proof. intros n m H; case (le_or_lt n m); intros H1. case (le_lt_or_eq _ _ H1); intros H2. @@ -1436,17 +1630,17 @@ Proof. elimtype False; auto. apply sym_not_eq; apply Rlt_dichotomy_converse; auto with real. Qed. -Hint Resolve not_nm_INR: real. +Hint Resolve not_INR: real. Lemma INR_eq : forall n m:nat, INR n = INR m -> n = m. Proof. intros; case (le_or_lt n m); intros H1. case (le_lt_or_eq _ _ H1); intros H2; auto. cut (n <> m). - intro H3; generalize (not_nm_INR n m H3); intro H4; elimtype False; auto. + intro H3; generalize (not_INR n m H3); intro H4; elimtype False; auto. omega. symmetry in |- *; cut (m <> n). - intro H3; generalize (not_nm_INR m n H3); intro H4; elimtype False; auto. + intro H3; generalize (not_INR m n H3); intro H4; elimtype False; auto. omega. Qed. Hint Resolve INR_eq: real. @@ -1465,9 +1659,9 @@ Proof. Qed. Hint Resolve not_1_INR: real. -(**********************************************************) -(** * Injection from [Z] to [R] *) -(**********************************************************) +(*********************************************************) +(** ** Injection from [Z] to [R] *) +(*********************************************************) (**********) @@ -1541,6 +1735,12 @@ Proof. Qed. (**********) +Lemma succ_IZR : forall n:Z, IZR (Zsucc n) = IZR n + 1. +Proof. + intro; change 1 with (IZR 1); unfold Zsucc; apply plus_IZR. +Qed. + +(**********) Lemma Ropp_Ropp_IZR : forall n:Z, IZR (- n) = - IZR n. Proof. intro z; case z; simpl in |- *; auto with real. @@ -1554,7 +1754,7 @@ Proof. Qed. (**********) -Lemma lt_O_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z. +Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z. Proof. intro z; case z; simpl in |- *; intros. absurd (0 < 0); auto with real. @@ -1567,7 +1767,7 @@ Qed. Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z. Proof. intros z1 z2 H; apply Zlt_0_minus_lt. - apply lt_O_IZR. + apply lt_0_IZR. rewrite <- Z_R_minus. exact (Rgt_minus (IZR z2) (IZR z1) H). Qed. @@ -1578,7 +1778,7 @@ Proof. intro z; destruct z; simpl in |- *; intros; auto with zarith. case (Rlt_not_eq 0 (INR (nat_of_P p))); auto with real. case (Rlt_not_eq (- INR (nat_of_P p)) 0); auto with real. - apply Ropp_lt_gt_0_contravar. unfold Rgt in |- *; apply INR_pos. + apply Ropp_lt_gt_0_contravar. unfold Rgt in |- *; apply pos_INR_nat_of_P. Qed. (**********) @@ -1590,17 +1790,17 @@ Proof. Qed. (**********) -Lemma not_O_IZR : forall n:Z, n <> 0%Z -> IZR n <> 0. +Lemma not_0_IZR : forall n:Z, n <> 0%Z -> IZR n <> 0. Proof. intros z H; red in |- *; intros H0; case H. apply eq_IZR; auto. Qed. (*********) -Lemma le_O_IZR : forall n:Z, 0 <= IZR n -> (0 <= n)%Z. +Lemma le_0_IZR : forall n:Z, 0 <= IZR n -> (0 <= n)%Z. Proof. unfold Rle in |- *; intros z [H| H]. - red in |- *; intro; apply (Zlt_le_weak 0 z (lt_O_IZR z H)); assumption. + red in |- *; intro; apply (Zlt_le_weak 0 z (lt_0_IZR z H)); assumption. rewrite (eq_IZR_R0 z); auto with zarith real. Qed. @@ -1685,32 +1885,6 @@ Proof. apply H3; apply single_z_r_R1 with r; trivial. Qed. -(*****************************************************************) -(** * Definitions of new types *) -(*****************************************************************) - -Record nonnegreal : Type := mknonnegreal - {nonneg :> R; cond_nonneg : 0 <= nonneg}. - -Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}. - -Record nonposreal : Type := mknonposreal - {nonpos :> R; cond_nonpos : nonpos <= 0}. - -Record negreal : Type := mknegreal {neg :> R; cond_neg : neg < 0}. - -Record nonzeroreal : Type := mknonzeroreal - {nonzero :> R; cond_nonzero : nonzero <> 0}. - -(**********) -Lemma prod_neq_R0 : forall r1 r2, r1 <> 0 -> r2 <> 0 -> r1 * r2 <> 0. -Proof. - intros x y; intros; red in |- *; intro; generalize (Rmult_integral x y H1); - intro; elim H2; intro; - [ rewrite H3 in H; elim H | rewrite H3 in H0; elim H0 ]; - reflexivity. -Qed. - (*********) Lemma Rmult_le_pos : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2. Proof. @@ -1728,67 +1902,18 @@ Proof. intro; rewrite <- double; unfold Rdiv in |- *; rewrite <- Rmult_assoc; symmetry in |- *; apply Rinv_r_simpl_m. replace 2 with (INR 2); - [ apply not_O_INR; discriminate | unfold INR in |- *; ring ]. -Qed. - -(**********************************************************) -(** * Other rules about < and <= *) -(**********************************************************) - -Lemma Rplus_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 + r2. -Proof. - intros x y; intros; apply Rlt_trans with x; - [ assumption - | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l; - assumption ]. -Qed. - -Lemma Rplus_le_lt_0_compat : forall r1 r2, 0 <= r1 -> 0 < r2 -> 0 < r1 + r2. -Proof. - intros x y; intros; apply Rle_lt_trans with x; - [ assumption - | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l; - assumption ]. -Qed. - -Lemma Rplus_lt_le_0_compat : forall r1 r2, 0 < r1 -> 0 <= r2 -> 0 < r1 + r2. -Proof. - intros x y; intros; rewrite <- Rplus_comm; apply Rplus_le_lt_0_compat; - assumption. -Qed. - -Lemma Rplus_le_le_0_compat : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2. -Proof. - intros x y; intros; apply Rle_trans with x; - [ assumption - | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; - assumption ]. -Qed. - -Lemma plus_le_is_le : forall r1 r2 r3, 0 <= r2 -> r1 + r2 <= r3 -> r1 <= r3. -Proof. - intros x y z; intros; apply Rle_trans with (x + y); - [ pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; - assumption - | assumption ]. + [ apply not_0_INR; discriminate | unfold INR in |- *; ring ]. Qed. -Lemma plus_lt_is_lt : forall r1 r2 r3, 0 <= r2 -> r1 + r2 < r3 -> r1 < r3. -Proof. - intros x y z; intros; apply Rle_lt_trans with (x + y); - [ pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; - assumption - | assumption ]. -Qed. +(*********************************************************) +(** ** Other rules about < and <= *) +(*********************************************************) -Lemma Rmult_le_0_lt_compat : +Lemma Rmult_ge_0_gt_0_lt_compat : forall r1 r2 r3 r4, - 0 <= r1 -> 0 <= r3 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. + r3 >= 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. Proof. - intros; apply Rle_lt_trans with (r2 * r3); - [ apply Rmult_le_compat_r; [ assumption | left; assumption ] - | apply Rmult_lt_compat_l; - [ apply Rle_lt_trans with r1; assumption | assumption ] ]. + intros; apply Rle_lt_trans with (r2 * r3); auto with real. Qed. Lemma le_epsilon : @@ -1811,7 +1936,7 @@ Proof. rewrite Rmult_1_r; replace (2 * x) with (x + x). rewrite (Rplus_comm y); intro H5; apply Rplus_le_reg_l with x; assumption. ring. - replace 2 with (INR 2); [ apply not_O_INR; discriminate | reflexivity ]. + replace 2 with (INR 2); [ apply not_0_INR; discriminate | reflexivity ]. pattern y at 2 in |- *; replace y with (y / 2 + y / 2). unfold Rminus, Rdiv in |- *. repeat rewrite Rmult_plus_distr_r. @@ -1822,12 +1947,12 @@ Proof. unfold Rdiv in |- *. rewrite <- Rmult_assoc; apply Rinv_r_simpl_m. replace 2 with (INR 2). - apply not_O_INR. + apply not_0_INR. discriminate. unfold INR in |- *; reflexivity. intro; ring. cut (0%nat <> 2%nat); - [ intro H0; generalize (lt_INR_0 2 (neq_O_lt 2 H0)); unfold INR in |- *; + [ intro H0; generalize (lt_0_INR 2 (neq_O_lt 2 H0)); unfold INR in |- *; intro; assumption | discriminate ]. Qed. @@ -1839,3 +1964,37 @@ Lemma completeness_weak : Proof. intros; elim (completeness E H H0); intros; split with x; assumption. Qed. + +(*********************************************************) +(** * Definitions of new types *) +(*********************************************************) + +Record nonnegreal : Type := mknonnegreal + {nonneg :> R; cond_nonneg : 0 <= nonneg}. + +Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}. + +Record nonposreal : Type := mknonposreal + {nonpos :> R; cond_nonpos : nonpos <= 0}. + +Record negreal : Type := mknegreal {neg :> R; cond_neg : neg < 0}. + +Record nonzeroreal : Type := mknonzeroreal + {nonzero :> R; cond_nonzero : nonzero <> 0}. + +(** Compatibility *) + +Notation prod_neq_R0 := Rmult_integral_contrapositive_currified (only parsing). +Notation minus_Rgt := Rminus_gt (only parsing). +Notation minus_Rge := Rminus_ge (only parsing). +Notation plus_le_is_le := Rplus_le_reg_pos_r (only parsing). +Notation plus_lt_is_lt := Rplus_lt_reg_pos_r (only parsing). +Notation INR_lt_1 := lt_1_INR (only parsing). +Notation lt_INR_0 := lt_0_INR (only parsing). +Notation not_nm_INR := not_INR (only parsing). +Notation INR_pos := pos_INR_nat_of_P (only parsing). +Notation not_INR_O := INR_not_0 (only parsing). +Notation not_O_INR := not_0_INR (only parsing). +Notation not_O_IZR := not_0_IZR (only parsing). +Notation le_O_IZR := le_0_IZR (only parsing). +Notation lt_O_IZR := lt_0_IZR (only parsing). diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index 270ea6da..17b6c60d 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -6,10 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: R_sqr.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: R_sqr.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. -Require Import Rbasic_fun. Open Local Scope R_scope. +Require Import Rbasic_fun. +Open Local Scope R_scope. (****************************************************) (** Rsqr : some results *) diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index 736365a0..63b8940b 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -6,11 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: R_sqrt.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: R_sqrt.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. -Require Import Rsqrt_def. Open Local Scope R_scope. +Require Import Rsqrt_def. +Open Local Scope R_scope. (** * Continuous extension of Rsqrt on R *) Definition sqrt (x:R) : R := diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index d712f74b..f48ce563 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ranalysis.v 9319 2006-10-30 12:41:21Z barras $ i*) +(*i $Id: Ranalysis.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -27,7 +27,8 @@ Require Export Rgeom. Require Export RList. Require Export Sqrt_reg. Require Export Ranalysis4. -Require Export Rpower. Open Local Scope R_scope. +Require Export Rpower. +Open Local Scope R_scope. Axiom AppVar : R. diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 93a66e70..9414f7c9 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -6,12 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ranalysis1.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Ranalysis1.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. Require Export Rlimit. -Require Export Rderiv. Open Local Scope R_scope. +Require Export Rderiv. +Open Local Scope R_scope. Implicit Type f : R -> R. (****************************************************) @@ -269,10 +270,10 @@ Definition derivable_pt_lim f (x l:R) : Prop := Definition derivable_pt_abs f (x l:R) : Prop := derivable_pt_lim f x l. -Definition derivable_pt f (x:R) := sigT (derivable_pt_abs f x). +Definition derivable_pt f (x:R) := { l:R | derivable_pt_abs f x l }. Definition derivable f := forall x:R, derivable_pt f x. -Definition derive_pt f (x:R) (pr:derivable_pt f x) := projT1 pr. +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]. @@ -380,9 +381,9 @@ Lemma derive_pt_eq : derive_pt f x pr = l <-> derivable_pt_lim f x l. Proof. intros; split. - intro; assert (H1 := projT2 pr); unfold derive_pt in H; rewrite H in H1; + intro; assert (H1 := proj2_sig pr); unfold derive_pt in H; rewrite H in H1; assumption. - intro; assert (H1 := projT2 pr); unfold derivable_pt_abs in H1. + intro; assert (H1 := proj2_sig pr); unfold derivable_pt_abs in H1. assert (H2 := uniqueness_limite _ _ _ _ H H1). unfold derive_pt in |- *; unfold derivable_pt_abs in |- *. symmetry in |- *; assumption. @@ -486,7 +487,7 @@ Qed. Lemma derivable_derive : forall f (x:R) (pr:derivable_pt f x), exists l : R, derive_pt f x pr = l. Proof. - intros; exists (projT1 pr). + intros; exists (proj1_sig pr). unfold derive_pt in |- *; reflexivity. Qed. @@ -714,7 +715,7 @@ Proof. unfold derivable_pt in |- *; intros f1 f2 x X X0. elim X; intros. elim X0; intros. - apply existT with (x0 + x1). + exists (x0 + x1). apply derivable_pt_lim_plus; assumption. Qed. @@ -723,7 +724,7 @@ Lemma derivable_pt_opp : Proof. unfold derivable_pt in |- *; intros f x X. elim X; intros. - apply existT with (- x0). + exists (- x0). apply derivable_pt_lim_opp; assumption. Qed. @@ -734,7 +735,7 @@ Proof. unfold derivable_pt in |- *; intros f1 f2 x X X0. elim X; intros. elim X0; intros. - apply existT with (x0 - x1). + exists (x0 - x1). apply derivable_pt_lim_minus; assumption. Qed. @@ -745,14 +746,14 @@ Proof. unfold derivable_pt in |- *; intros f1 f2 x X X0. elim X; intros. elim X0; intros. - apply existT with (x0 * f2 x + f1 x * x1). + exists (x0 * f2 x + f1 x * x1). apply derivable_pt_lim_mult; assumption. Qed. Lemma derivable_pt_const : forall a x:R, derivable_pt (fct_cte a) x. Proof. intros; unfold derivable_pt in |- *. - apply existT with 0. + exists 0. apply derivable_pt_lim_const. Qed. @@ -761,7 +762,7 @@ Lemma derivable_pt_scal : Proof. unfold derivable_pt in |- *; intros f1 a x X. elim X; intros. - apply existT with (a * x0). + exists (a * x0). apply derivable_pt_lim_scal; assumption. Qed. @@ -774,7 +775,7 @@ Qed. Lemma derivable_pt_Rsqr : forall x:R, derivable_pt Rsqr x. Proof. - unfold derivable_pt in |- *; intro; apply existT with (2 * x). + unfold derivable_pt in |- *; intro; exists (2 * x). apply derivable_pt_lim_Rsqr. Qed. @@ -785,7 +786,7 @@ Proof. unfold derivable_pt in |- *; intros f1 f2 x X X0. elim X; intros. elim X0; intros. - apply existT with (x1 * x0). + exists (x1 * x0). apply derivable_pt_lim_comp; assumption. Qed. @@ -860,9 +861,9 @@ Proof. elim H0; clear H0; intros l2 H0. elim H1; clear H1; intros l H1. rewrite H; rewrite H0; apply derive_pt_eq_0. - assert (H3 := projT2 pr1). + assert (H3 := proj2_sig pr1). unfold derive_pt in H; rewrite H in H3. - assert (H4 := projT2 pr2). + assert (H4 := proj2_sig pr2). unfold derive_pt in H0; rewrite H0 in H4. apply derivable_pt_lim_plus; assumption. Qed. @@ -877,7 +878,7 @@ Proof. elim H; clear H; intros l1 H. elim H0; clear H0; intros l2 H0. rewrite H; apply derive_pt_eq_0. - assert (H3 := projT2 pr1). + assert (H3 := proj2_sig pr1). unfold derive_pt in H; rewrite H in H3. apply derivable_pt_lim_opp; assumption. Qed. @@ -896,9 +897,9 @@ Proof. elim H0; clear H0; intros l2 H0. elim H1; clear H1; intros l H1. rewrite H; rewrite H0; apply derive_pt_eq_0. - assert (H3 := projT2 pr1). + assert (H3 := proj2_sig pr1). unfold derive_pt in H; rewrite H in H3. - assert (H4 := projT2 pr2). + assert (H4 := proj2_sig pr2). unfold derive_pt in H0; rewrite H0 in H4. apply derivable_pt_lim_minus; assumption. Qed. @@ -917,9 +918,9 @@ Proof. elim H0; clear H0; intros l2 H0. elim H1; clear H1; intros l H1. rewrite H; rewrite H0; apply derive_pt_eq_0. - assert (H3 := projT2 pr1). + assert (H3 := proj2_sig pr1). unfold derive_pt in H; rewrite H in H3. - assert (H4 := projT2 pr2). + assert (H4 := proj2_sig pr2). unfold derive_pt in H0; rewrite H0 in H4. apply derivable_pt_lim_mult; assumption. Qed. @@ -944,7 +945,7 @@ Proof. elim H; clear H; intros l1 H. elim H0; clear H0; intros l2 H0. rewrite H; apply derive_pt_eq_0. - assert (H3 := projT2 pr). + assert (H3 := proj2_sig pr). unfold derive_pt in H; rewrite H in H3. apply derivable_pt_lim_scal; assumption. Qed. @@ -978,9 +979,9 @@ Proof. elim H0; clear H0; intros l2 H0. elim H1; clear H1; intros l H1. rewrite H; rewrite H0; apply derive_pt_eq_0. - assert (H3 := projT2 pr1). + assert (H3 := proj2_sig pr1). unfold derive_pt in H; rewrite H in H3. - assert (H4 := projT2 pr2). + assert (H4 := proj2_sig pr2). unfold derive_pt in H0; rewrite H0 in H4. apply derivable_pt_lim_comp; assumption. Qed. @@ -1046,7 +1047,7 @@ Lemma derivable_pt_pow : forall (n:nat) (x:R), derivable_pt (fun y:R => y ^ n) x. Proof. intros; unfold derivable_pt in |- *. - apply existT with (INR n * x ^ pred n). + exists (INR n * x ^ pred n). apply derivable_pt_lim_pow. Qed. diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index fb89da67..54801eb7 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -6,11 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ranalysis2.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Ranalysis2.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. -Require Import Ranalysis1. Open Local Scope R_scope. +Require Import Ranalysis1. +Open Local Scope R_scope. (**********) Lemma formule : diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v index f50aa2ad..180cf9d6 100644 --- a/theories/Reals/Ranalysis3.v +++ b/theories/Reals/Ranalysis3.v @@ -6,12 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ranalysis3.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Ranalysis3.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. -Require Import Ranalysis2. Open Local Scope R_scope. +Require Import Ranalysis2. +Open Local Scope R_scope. (** Division *) Theorem derivable_pt_lim_div : @@ -23,7 +24,7 @@ Theorem derivable_pt_lim_div : Proof. intros f1 f2 x l1 l2 H H0 H1. cut (derivable_pt f2 x); - [ intro X | unfold derivable_pt in |- *; apply existT with l2; exact H0 ]. + [ intro X | unfold derivable_pt in |- *; exists l2; exact H0 ]. assert (H2 := continuous_neq_0 _ _ (derivable_continuous_pt _ _ X) H1). elim H2; clear H2; intros eps_f2 H2. unfold div_fct in |- *. @@ -761,7 +762,7 @@ Proof. intros f1 f2 x X X0 H. elim X; intros. elim X0; intros. - apply existT with ((x0 * f2 x - x1 * f1 x) / Rsqr (f2 x)). + exists ((x0 * f2 x - x1 * f1 x) / Rsqr (f2 x)). apply derivable_pt_lim_div; assumption. Qed. @@ -789,9 +790,9 @@ Proof. elim H0; clear H0; intros l2 H0. elim H1; clear H1; intros l H1. rewrite H; rewrite H0; apply derive_pt_eq_0. - assert (H3 := projT2 pr1). + assert (H3 := proj2_sig pr1). unfold derive_pt in H; rewrite H in H3. - assert (H4 := projT2 pr2). + assert (H4 := proj2_sig pr2). unfold derive_pt in H0; rewrite H0 in H4. apply derivable_pt_lim_div; assumption. Qed. diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index 205c06b4..95f6d27e 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ranalysis4.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Ranalysis4.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -14,7 +14,8 @@ Require Import SeqSeries. Require Import Rtrigo. Require Import Ranalysis1. Require Import Ranalysis3. -Require Import Exp_prop. Open Local Scope R_scope. +Require Import Exp_prop. +Open Local Scope R_scope. (**********) Lemma derivable_pt_inv : @@ -28,7 +29,7 @@ Proof. assumption. assumption. unfold div_fct, inv_fct, fct_cte in |- *; intro X0; elim X0; intros; - unfold derivable_pt in |- *; apply existT with x0; + unfold derivable_pt in |- *; exists x0; unfold derivable_pt_abs in |- *; unfold derivable_pt_lim in |- *; unfold derivable_pt_abs in p; unfold derivable_pt_lim in p; intros; elim (p eps H0); intros; exists x1; intros; @@ -164,10 +165,10 @@ Proof. intros. case (total_order_T x 0); intro. elim s; intro. - unfold derivable_pt in |- *; apply existT with (-1). + unfold derivable_pt in |- *; exists (-1). apply (Rabs_derive_2 x a). elim H; exact b. - unfold derivable_pt in |- *; apply existT with 1. + unfold derivable_pt in |- *; exists 1. apply (Rabs_derive_1 x r). Qed. @@ -294,8 +295,8 @@ Proof. unfold derivable_pt in |- *. assert (H := derivable_pt_lim_finite_sum An x N). induction N as [| N HrecN]. - apply existT with 0; apply H. - apply existT with + exists 0; apply H. + exists (sum_f_R0 (fun k:nat => INR (S k) * An (S k) * x ^ k) (pred (S N))); apply H. Qed. @@ -352,7 +353,7 @@ Lemma derivable_pt_exp : forall x:R, derivable_pt exp x. Proof. intro. unfold derivable_pt in |- *. - apply existT with (exp x). + exists (exp x). apply derivable_pt_lim_exp. Qed. @@ -360,7 +361,7 @@ Lemma derivable_pt_cosh : forall x:R, derivable_pt cosh x. Proof. intro. unfold derivable_pt in |- *. - apply existT with (sinh x). + exists (sinh x). apply derivable_pt_lim_cosh. Qed. @@ -368,7 +369,7 @@ Lemma derivable_pt_sinh : forall x:R, derivable_pt sinh x. Proof. intro. unfold derivable_pt in |- *. - apply existT with (cosh x). + exists (cosh x). apply derivable_pt_lim_sinh. Qed. diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index aaea59f4..6667d2ec 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Raxioms.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Raxioms.v 10710 2008-03-23 09:24:09Z herbelin $ i*) (*********************************************************) (** Axiomatisation of the classical reals *) @@ -130,7 +130,7 @@ Definition IZR (z:Z) : R := Arguments Scope IZR [Z_scope]. (**********************************************************) -(** * [R] Archimedian *) +(** * [R] Archimedean *) (**********************************************************) (**********) @@ -154,4 +154,4 @@ Definition is_lub (E:R -> Prop) (m:R) := Axiom completeness : forall E:R -> Prop, - bound E -> (exists x : R, E x) -> sigT (fun m:R => is_lub E m). + bound E -> (exists x : R, E x) -> { m:R | is_lub E m }. diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 98bd607b..a5cc9f19 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rbasic_fun.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Rbasic_fun.v 10710 2008-03-23 09:24:09Z herbelin $ i*) (*********************************************************) (** Complements for the real numbers *) @@ -15,7 +15,8 @@ Require Import Rbase. Require Import R_Ifp. -Require Import Fourier. Open Local Scope R_scope. +Require Import Fourier. +Open Local Scope R_scope. Implicit Type r : R. diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v index 16e12d7f..d7fee9c5 100644 --- a/theories/Reals/Rcomplete.v +++ b/theories/Reals/Rcomplete.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rcomplete.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Rcomplete.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -24,7 +24,7 @@ Open Local Scope R_scope. (****************************************************) Theorem R_complete : - forall Un:nat -> R, Cauchy_crit Un -> sigT (fun l:R => Un_cv Un l). + forall Un:nat -> R, Cauchy_crit Un -> { l:R | Un_cv Un l } . Proof. intros. set (Vn := sequence_minorant Un (cauchy_min Un H)). @@ -37,7 +37,7 @@ Proof. elim H1; intros. cut (x = x0). intros. - apply existT with x. + exists x. rewrite <- H2 in p0. unfold Un_cv in |- *. intros. diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 330c0042..002ce8d6 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rdefinitions.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: Rdefinitions.v 10751 2008-04-04 10:23:35Z herbelin $ i*) (*********************************************************) @@ -22,6 +22,8 @@ Delimit Scope R_scope with R. (* Automatically open scope R_scope for arguments of type R *) Bind Scope R_scope with R. +Open Local Scope R_scope. + Parameter R0 : R. Parameter R1 : R. Parameter Rplus : R -> R -> R. @@ -38,33 +40,33 @@ Notation "/ x" := (Rinv x) : R_scope. Infix "<" := Rlt : R_scope. -(*i*******************************************************i*) +(***********************************************************) (**********) -Definition Rgt (r1 r2:R) : Prop := (r2 < r1)%R. +Definition Rgt (r1 r2:R) : Prop := r2 < r1. (**********) -Definition Rle (r1 r2:R) : Prop := (r1 < r2)%R \/ r1 = r2. +Definition Rle (r1 r2:R) : Prop := r1 < r2 \/ r1 = r2. (**********) Definition Rge (r1 r2:R) : Prop := Rgt r1 r2 \/ r1 = r2. (**********) -Definition Rminus (r1 r2:R) : R := (r1 + - r2)%R. +Definition Rminus (r1 r2:R) : R := r1 + - r2. (**********) -Definition Rdiv (r1 r2:R) : R := (r1 * / r2)%R. +Definition Rdiv (r1 r2:R) : R := r1 * / r2. (**********) Infix "-" := Rminus : R_scope. -Infix "/" := Rdiv : R_scope. +Infix "/" := Rdiv : R_scope. Infix "<=" := Rle : R_scope. Infix ">=" := Rge : R_scope. -Infix ">" := Rgt : R_scope. +Infix ">" := Rgt : R_scope. -Notation "x <= y <= z" := ((x <= y)%R /\ (y <= z)%R) : R_scope. -Notation "x <= y < z" := ((x <= y)%R /\ (y < z)%R) : R_scope. -Notation "x < y < z" := ((x < y)%R /\ (y < z)%R) : R_scope. -Notation "x < y <= z" := ((x < y)%R /\ (y <= z)%R) : R_scope. +Notation "x <= y <= z" := (x <= y /\ y <= z) : R_scope. +Notation "x <= y < z" := (x <= y /\ y < z) : R_scope. +Notation "x < y < z" := (x < y /\ y < z) : R_scope. +Notation "x < y <= z" := (x < y /\ y <= z) : R_scope. diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index e2fd2efe..ba42bad9 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rderiv.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Rderiv.v 10710 2008-03-23 09:24:09Z herbelin $ i*) (*********************************************************) (** Definition of the derivative,continuity *) @@ -19,7 +19,8 @@ Require Import Rlimit. Require Import Fourier. Require Import Classical_Prop. Require Import Classical_Pred_Type. -Require Import Omega. Open Local Scope R_scope. +Require Import Omega. +Open Local Scope R_scope. (*********) Definition D_x (D:R -> Prop) (y x:R) : Prop := D x /\ y <> x. diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 3d1c0375..b9aec1ea 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rfunctions.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: Rfunctions.v 10762 2008-04-06 16:57:31Z 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*) @@ -349,8 +349,7 @@ Proof. rewrite Rabs_Rinv; auto. rewrite <- Rinv_pow; auto. rewrite RPow_abs; auto. - rewrite H'0; rewrite Rabs_right; auto with real. - apply Rle_ge; auto with real. + rewrite H'0; rewrite Rabs_right; auto with real rorders. apply Rlt_pow; auto with arith. rewrite Rabs_Rinv; auto. apply Rmult_lt_reg_l with (r := Rabs r). @@ -786,11 +785,14 @@ Proof. Qed. (*******************************) -(** * Infinit Sum *) +(** * Infinite Sum *) (*******************************) (*********) -Definition infinit_sum (s:nat -> R) (l:R) : Prop := +Definition infinite_sum (s:nat -> R) (l:R) : Prop := forall eps:R, eps > 0 -> exists N : nat, (forall n:nat, (n >= N)%nat -> R_dist (sum_f_R0 s n) l < eps). + +(** Compatibility with previous versions *) +Notation infinit_sum := infinite_sum (only parsing). diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v index 8ac9c07f..c96ae5d6 100644 --- a/theories/Reals/Rgeom.v +++ b/theories/Reals/Rgeom.v @@ -6,13 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rgeom.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Rgeom.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. Require Import Rtrigo. -Require Import R_sqrt. Open Local Scope R_scope. +Require Import R_sqrt. +Open Local Scope R_scope. (** * Distance *) diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 1cba821e..8d069e2d 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: RiemannInt.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: RiemannInt.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rfunctions. Require Import SeqSeries. @@ -15,7 +15,8 @@ Require Import Rbase. Require Import RiemannInt_SF. Require Import Classical_Prop. Require Import Classical_Pred_Type. -Require Import Max. Open Local Scope R_scope. +Require Import Max. +Open Local Scope R_scope. Set Implicit Arguments. @@ -25,13 +26,11 @@ Set Implicit Arguments. Definition Riemann_integrable (f:R -> R) (a b:R) : Type := forall eps:posreal, - sigT - (fun phi:StepFun a b => - sigT - (fun psi:StepFun a b => + { phi:StepFun a b & + { psi:StepFun a b | (forall t:R, Rmin a b <= t <= Rmax a b -> Rabs (f t - phi t) <= psi t) /\ - Rabs (RiemannInt_SF psi) < eps)). + Rabs (RiemannInt_SF psi) < eps } }. Definition phi_sequence (un:nat -> posreal) (f:R -> R) (a b:R) (pr:Riemann_integrable f a b) (n:nat) := @@ -40,12 +39,11 @@ Definition phi_sequence (un:nat -> posreal) (f:R -> R) Lemma phi_sequence_prop : forall (un:nat -> posreal) (f:R -> R) (a b:R) (pr:Riemann_integrable f a b) (N:nat), - sigT - (fun psi:StepFun a b => + { psi:StepFun a b | (forall t:R, Rmin a b <= t <= Rmax a b -> Rabs (f t - phi_sequence un pr N t) <= psi t) /\ - Rabs (RiemannInt_SF psi) < un N). + Rabs (RiemannInt_SF psi) < un N }. Proof. intros; apply (projT2 (pr (un N))). Qed. @@ -55,8 +53,8 @@ Lemma RiemannInt_P1 : Riemann_integrable f a b -> Riemann_integrable f b a. Proof. unfold Riemann_integrable in |- *; intros; elim (X eps); clear X; intros; - elim p; clear p; intros; apply existT with (mkStepFun (StepFun_P6 (pre x))); - apply existT with (mkStepFun (StepFun_P6 (pre x0))); + elim p; clear p; intros; exists (mkStepFun (StepFun_P6 (pre x))); + exists (mkStepFun (StepFun_P6 (pre x0))); elim p; clear p; intros; split. intros; apply (H t); elim H1; clear H1; intros; split; [ apply Rle_trans with (Rmin b a); try assumption; right; @@ -90,7 +88,7 @@ Lemma RiemannInt_P2 : (forall n:nat, (forall t:R, Rmin a b <= t <= Rmax a b -> Rabs (f t - vn n t) <= wn n t) /\ Rabs (RiemannInt_SF (wn n)) < un n) -> - sigT (fun l:R => Un_cv (fun N:nat => RiemannInt_SF (vn N)) l). + { l:R | Un_cv (fun N:nat => RiemannInt_SF (vn N)) l }. Proof. intros; apply R_complete; unfold Un_cv in H; unfold Cauchy_crit in |- *; intros; assert (H3 : 0 < eps / 2). @@ -143,7 +141,7 @@ Lemma RiemannInt_P3 : (forall n:nat, (forall t:R, Rmin a b <= t <= Rmax a b -> Rabs (f t - vn n t) <= wn n t) /\ Rabs (RiemannInt_SF (wn n)) < un n) -> - sigT (fun l:R => Un_cv (fun N:nat => RiemannInt_SF (vn N)) l). + { l:R | Un_cv (fun N:nat => RiemannInt_SF (vn N)) l }. Proof. intros; case (Rle_dec a b); intro. apply RiemannInt_P2 with f un wn; assumption. @@ -181,7 +179,7 @@ Proof. rewrite Rabs_Ropp in H4; apply H4. apply H4. assert (H3 := RiemannInt_P2 _ _ _ _ H H1 H2); elim H3; intros; - apply existT with (- x); unfold Un_cv in |- *; unfold Un_cv in p; + exists (- x); unfold Un_cv in |- *; unfold Un_cv in p; intros; elim (p _ H4); intros; exists x0; intros; generalize (H5 _ H6); unfold R_dist, RiemannInt_SF in |- *; case (Rle_dec b a); case (Rle_dec a b); intros. @@ -205,13 +203,12 @@ Lemma RiemannInt_exists : forall (f:R -> R) (a b:R) (pr:Riemann_integrable f a b) (un:nat -> posreal), Un_cv un 0 -> - sigT - (fun l:R => Un_cv (fun N:nat => RiemannInt_SF (phi_sequence un pr N)) l). + { l:R | Un_cv (fun N:nat => RiemannInt_SF (phi_sequence un pr N)) l }. Proof. intros f; intros; apply RiemannInt_P3 with - f un (fun n:nat => projT1 (phi_sequence_prop un pr n)); - [ apply H | intro; apply (projT2 (phi_sequence_prop un pr n)) ]. + f un (fun n:nat => proj1_sig (phi_sequence_prop un pr n)); + [ apply H | intro; apply (proj2_sig (phi_sequence_prop un pr n)) ]. Qed. Lemma RiemannInt_P4 : @@ -411,9 +408,7 @@ Qed. (**********) Definition RiemannInt (f:R -> R) (a b:R) (pr:Riemann_integrable f a b) : R := - match RiemannInt_exists pr RinvN RinvN_cv with - | existT a' b' => a' - end. + let (a,_) := RiemannInt_exists pr RinvN RinvN_cv in a. Lemma RiemannInt_P5 : forall (f:R -> R) (a b:R) (pr1 pr2:Riemann_integrable f a b), @@ -433,8 +428,7 @@ Qed. Lemma maxN : forall (a b:R) (del:posreal), - a < b -> - sigT (fun n:nat => a + INR n * del < b /\ b <= a + INR (S n) * del). + a < b -> { n:nat | a + INR n * del < b /\ b <= a + INR (S n) * del }. Proof. intros; set (I := fun n:nat => a + INR n * del < b); assert (H0 : exists n : nat, I n). @@ -478,9 +472,7 @@ Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) {struct N} : Rlist := end. Definition max_N (a b:R) (del:posreal) (h:a < b) : nat := - match maxN del h with - | existT N H0 => N - end. + let (N,_) := maxN del h in N. Definition SubEqui (a b:R) (del:posreal) (h:a < b) : Rlist := SubEquiN (S (max_N del h)) a b del. @@ -490,12 +482,11 @@ Lemma Heine_cor1 : a < b -> (forall x:R, a <= x <= b -> continuity_pt f x) -> forall eps:posreal, - sigT - (fun delta:posreal => + { delta:posreal | delta <= b - a /\ (forall x y:R, a <= x <= b -> - a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps)). + a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps) }. Proof. intro f; intros; set @@ -520,7 +511,7 @@ Proof. | intros; apply H3; try assumption; apply Rlt_le_trans with (Rmin x (b - a)); [ assumption | apply Rmin_l ] ]. assert (H3 := completeness E H1 H2); elim H3; intros; cut (0 < x <= b - a). - intro; elim H4; clear H4; intros; apply existT with (mkposreal _ H4); split. + intro; elim H4; clear H4; intros; exists (mkposreal _ H4); split. apply H5. unfold is_lub in p; elim p; intros; unfold is_upper_bound in H6; set (D := Rabs (x0 - y)); elim (classic (exists y : R, D < y /\ E y)); @@ -549,22 +540,21 @@ Lemma Heine_cor2 : forall (f:R -> R) (a b:R), (forall x:R, a <= x <= b -> continuity_pt f x) -> forall eps:posreal, - sigT - (fun delta:posreal => + { delta:posreal | forall x y:R, a <= x <= b -> - a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps). + a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps }. Proof. intro f; intros; case (total_order_T a b); intro. elim s; intro. - assert (H0 := Heine_cor1 a0 H eps); elim H0; intros; apply existT with x; + assert (H0 := Heine_cor1 a0 H eps); elim H0; intros; exists x; elim p; intros; apply H2; assumption. - apply existT with (mkposreal _ Rlt_0_1); intros; assert (H3 : x = y); + exists (mkposreal _ Rlt_0_1); intros; assert (H3 : x = y); [ elim H0; elim H1; intros; rewrite b0 in H3; rewrite b0 in H5; apply Rle_antisym; apply Rle_trans with b; assumption | rewrite H3; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; apply (cond_pos eps) ]. - apply existT with (mkposreal _ Rlt_0_1); intros; elim H0; intros; + exists (mkposreal _ Rlt_0_1); intros; elim H0; intros; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (Rle_trans _ _ _ H3 H4) r)). Qed. @@ -664,15 +654,14 @@ Qed. Lemma SubEqui_P9 : forall (a b:R) (del:posreal) (f:R -> R) (h:a < b), - sigT - (fun g:StepFun a b => + { g:StepFun a b | g b = f b /\ (forall i:nat, (i < pred (Rlength (SubEqui del h)))%nat -> constant_D_eq g (co_interval (pos_Rl (SubEqui del h) i) (pos_Rl (SubEqui del h) (S i))) - (f (pos_Rl (SubEqui del h) i)))). + (f (pos_Rl (SubEqui del h) i))) }. Proof. intros; apply StepFun_P38; [ apply SubEqui_P7 | apply SubEqui_P1 | apply SubEqui_P2 ]. @@ -1003,11 +992,11 @@ Proof. do 2 rewrite (Rmult_comm 3); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ ring | discrR ] | discrR ]. - split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr2 n)); intro; + split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr2 n)); intro; rewrite Rmin_comm; rewrite RmaxSym; - apply (projT2 (phi_sequence_prop RinvN pr2 n)). - split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); intro; - apply (projT2 (phi_sequence_prop RinvN pr1 n)). + apply (proj2_sig (phi_sequence_prop RinvN pr2 n)). + split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); intro; + apply (proj2_sig (phi_sequence_prop RinvN pr1 n)). Qed. Lemma RiemannInt_P9 : @@ -1272,11 +1261,11 @@ Proof. case (RiemannInt_exists pr1 RinvN RinvN_cv); intros; eapply UL_sequence; [ apply u0 - | set (psi1 := fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); - set (psi2 := fun n:nat => projT1 (phi_sequence_prop RinvN pr3 n)); + | set (psi1 := fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); + set (psi2 := fun n:nat => proj1_sig (phi_sequence_prop RinvN pr3 n)); apply RiemannInt_P11 with f RinvN (phi_sequence RinvN pr1) psi1 psi2; [ apply RinvN_cv - | intro; apply (projT2 (phi_sequence_prop RinvN pr1 n)) + | intro; apply (proj2_sig (phi_sequence_prop RinvN pr1 n)) | intro; assert (H1 : @@ -1284,7 +1273,7 @@ Proof. Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t + l * g t - phi_sequence RinvN pr3 n t) <= psi2 n t) /\ Rabs (RiemannInt_SF (psi2 n)) < RinvN n); - [ apply (projT2 (phi_sequence_prop RinvN pr3 n)) + [ apply (proj2_sig (phi_sequence_prop RinvN pr3 n)) | elim H1; intros; split; try assumption; intros; replace (f t) with (f t + l * g t); [ apply H2; assumption | rewrite H0; ring ] ] @@ -1360,8 +1349,8 @@ Proof. Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi_sequence RinvN pr1 n t) <= psi1 n t) /\ Rabs (RiemannInt_SF (psi1 n)) < RinvN n)). - split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); intro; - apply (projT2 (phi_sequence_prop RinvN pr1 n0)). + split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); intro; + apply (proj2_sig (phi_sequence_prop RinvN pr1 n0)). assert (H8 : exists psi2 : nat -> StepFun a b, @@ -1370,8 +1359,8 @@ Proof. Rmin a b <= t /\ t <= Rmax a b -> Rabs (g t - phi_sequence RinvN pr2 n t) <= psi2 n t) /\ Rabs (RiemannInt_SF (psi2 n)) < RinvN n)). - split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr2 n)); intro; - apply (projT2 (phi_sequence_prop RinvN pr2 n0)). + split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr2 n)); intro; + apply (proj2_sig (phi_sequence_prop RinvN pr2 n0)). assert (H9 : exists psi3 : nat -> StepFun a b, @@ -1380,8 +1369,8 @@ Proof. Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t + l * g t - phi_sequence RinvN pr3 n t) <= psi3 n t) /\ Rabs (RiemannInt_SF (psi3 n)) < RinvN n)). - split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr3 n)); intro; - apply (projT2 (phi_sequence_prop RinvN pr3 n0)). + split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr3 n)); intro; + apply (proj2_sig (phi_sequence_prop RinvN pr3 n0)). elim H7; clear H7; intros psi1 H7; elim H8; clear H8; intros psi2 H8; elim H9; clear H9; intros psi3 H9; replace @@ -1552,8 +1541,8 @@ Proof. Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi_sequence RinvN pr n t) <= psi1 n t) /\ Rabs (RiemannInt_SF (psi1 n)) < RinvN n)). - split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr n)); intro; - apply (projT2 (phi_sequence_prop RinvN pr n)). + split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr n)); intro; + apply (proj2_sig (phi_sequence_prop RinvN pr n)). elim H1; clear H1; intros psi1 H1; set (phi2 := fun n:nat => mkStepFun (StepFun_P4 a b c)); set (psi2 := fun n:nat => mkStepFun (StepFun_P4 a b 0)); @@ -1647,8 +1636,8 @@ Proof. Rmin a b <= t /\ t <= Rmax a b -> Rabs (Rabs (f t) - phi3 n t) <= psi3 n t) /\ Rabs (RiemannInt_SF (psi3 n)) < RinvN n)). - split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr2 n)); intro; - apply (projT2 (phi_sequence_prop RinvN pr2 n)). + split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr2 n)); intro; + apply (proj2_sig (phi_sequence_prop RinvN pr2 n)). assert (H1 : exists psi2 : nat -> StepFun a b, @@ -1664,8 +1653,8 @@ Proof. (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi1 n t) <= psi2 n t) /\ Rabs (RiemannInt_SF (psi2 n)) < RinvN n)). - split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); intro; - apply (projT2 (phi_sequence_prop RinvN pr1 n)). + split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); intro; + apply (proj2_sig (phi_sequence_prop RinvN pr1 n)). elim H1; clear H1; intros psi2 H1; split with psi2; intros; elim (H1 n); clear H1; intros; split; try assumption. intros; unfold phi2 in |- *; simpl in |- *; @@ -1698,8 +1687,8 @@ Proof. Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi1 n t) <= psi1 n t) /\ Rabs (RiemannInt_SF (psi1 n)) < RinvN n)). - split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); intro; - apply (projT2 (phi_sequence_prop RinvN pr1 n)). + split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); intro; + apply (proj2_sig (phi_sequence_prop RinvN pr1 n)). elim H1; clear H1; intros psi1 H1; set (phi2 := fun N:nat => phi_sequence RinvN pr2 N). set @@ -1722,8 +1711,8 @@ Proof. (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (g t - phi2 n t) <= psi2 n t) /\ Rabs (RiemannInt_SF (psi2 n)) < RinvN n)). - split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr2 n)); intro; - apply (projT2 (phi_sequence_prop RinvN pr2 n)). + split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr2 n)); intro; + apply (proj2_sig (phi_sequence_prop RinvN pr2 n)). elim H2; clear H2; intros psi2 H2; apply RiemannInt_P11 with f RinvN phi2_m psi2 psi1; try assumption. @@ -2378,8 +2367,8 @@ Proof. Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi_sequence RinvN pr1 n t) <= psi1 n t) /\ Rabs (RiemannInt_SF (psi1 n)) < RinvN n)). - split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); intro; - apply (projT2 (phi_sequence_prop RinvN pr1 n)). + split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); intro; + apply (proj2_sig (phi_sequence_prop RinvN pr1 n)). assert (H2 : exists psi2 : nat -> StepFun b c, @@ -2388,8 +2377,8 @@ Proof. Rmin b c <= t /\ t <= Rmax b c -> Rabs (f t - phi_sequence RinvN pr2 n t) <= psi2 n t) /\ Rabs (RiemannInt_SF (psi2 n)) < RinvN n)). - split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr2 n)); intro; - apply (projT2 (phi_sequence_prop RinvN pr2 n)). + split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr2 n)); intro; + apply (proj2_sig (phi_sequence_prop RinvN pr2 n)). assert (H3 : exists psi3 : nat -> StepFun a c, @@ -2398,8 +2387,8 @@ Proof. Rmin a c <= t /\ t <= Rmax a c -> Rabs (f t - phi_sequence RinvN pr3 n t) <= psi3 n t) /\ Rabs (RiemannInt_SF (psi3 n)) < RinvN n)). - split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr3 n)); intro; - apply (projT2 (phi_sequence_prop RinvN pr3 n)). + split with (fun n:nat => proj1_sig (phi_sequence_prop RinvN pr3 n)); intro; + apply (proj2_sig (phi_sequence_prop RinvN pr3 n)). elim H1; clear H1; intros psi1 H1; elim H2; clear H2; intros psi2 H2; elim H3; clear H3; intros psi3 H3; assert (H := RinvN_cv); unfold Un_cv in |- *; intros; assert (H4 : 0 < eps / 3). @@ -3259,7 +3248,7 @@ Lemma RiemannInt_P30 : forall (f:R -> R) (a b:R), a <= b -> (forall x:R, a <= x <= b -> continuity_pt f x) -> - sigT (fun g:R -> R => antiderivative f g a b). + { g:R -> R | antiderivative f g a b }. Proof. intros; split with (primitive H (FTC_P1 H H0)); apply RiemannInt_P29. Qed. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 0f91d006..7a02544e 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: RiemannInt_SF.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: RiemannInt_SF.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -31,7 +31,7 @@ Qed. Lemma Nzorn : forall I:nat -> Prop, (exists n : nat, I n) -> - Nbound I -> sigT (fun n:nat => I n /\ (forall i:nat, I i -> (i <= n)%nat)). + Nbound I -> { n:nat | I n /\ (forall i:nat, I i -> (i <= n)%nat) }. Proof. intros I H H0; set (E := fun x:R => exists i : nat, I i /\ INR i = x); assert (H1 : bound E). @@ -133,10 +133,10 @@ Definition adapted_couple_opt (f:R -> R) (a b:R) (l lf:Rlist) := (forall i:nat, (i < pred (Rlength l))%nat -> pos_Rl l i <> pos_Rl l (S i)). Definition is_subdivision (f:R -> R) (a b:R) (l:Rlist) : Type := - sigT (fun l0:Rlist => adapted_couple f a b l l0). + { l0:Rlist & adapted_couple f a b l l0 }. Definition IsStepFun (f:R -> R) (a b:R) : Type := - sigT (fun l:Rlist => is_subdivision f a b l). + { l:Rlist & is_subdivision f a b l }. (** ** Class of step functions *) Record StepFun (a b:R) : Type := mkStepFun @@ -1779,13 +1779,12 @@ Lemma StepFun_P38 : ordered_Rlist l -> pos_Rl l 0 = a -> pos_Rl l (pred (Rlength l)) = b -> - sigT - (fun g:StepFun a b => + { g:StepFun a b | g b = f b /\ (forall i:nat, (i < pred (Rlength l))%nat -> constant_D_eq g (co_interval (pos_Rl l i) (pos_Rl l (S i))) - (f (pos_Rl l i)))). + (f (pos_Rl l i))) }. Proof. intros l a b f; generalize a; clear a; induction l. intros a H H0 H1; simpl in H0; simpl in H1; @@ -2206,21 +2205,10 @@ Lemma StepFun_P43 : RiemannInt_SF (mkStepFun pr1) + RiemannInt_SF (mkStepFun pr2) = RiemannInt_SF (mkStepFun pr3). Proof. - intros f; intros; - assert - (H1 : - sigT (fun l:Rlist => sigT (fun l0:Rlist => adapted_couple f a b l l0))). - apply pr1. - assert - (H2 : - sigT (fun l:Rlist => sigT (fun l0:Rlist => adapted_couple f b c l l0))). - apply pr2. - assert - (H3 : - sigT (fun l:Rlist => sigT (fun l0:Rlist => adapted_couple f a c l l0))). - apply pr3. - elim H1; clear H1; intros l1 [lf1 H1]; elim H2; clear H2; intros l2 [lf2 H2]; - elim H3; clear H3; intros l3 [lf3 H3]. + intros f; intros. + pose proof pr1 as (l1,(lf1,H1)). + pose proof pr2 as (l2,(lf2,H2)). + pose proof pr3 as (l3,(lf3,H3)). replace (RiemannInt_SF (mkStepFun pr1)) with match Rle_dec a b with | left _ => Int_SF lf1 l1 @@ -2462,7 +2450,7 @@ Proof. (forall (l1 lf1:Rlist) (a b c:R) (f:R -> R), adapted_couple f a b l1 lf1 -> a <= c <= b -> - sigT (fun l:Rlist => sigT (fun l0:Rlist => adapted_couple f a c l l0))). + { l:Rlist & { l0:Rlist & adapted_couple f a c l l0 } }). intro X; unfold IsStepFun in |- *; unfold is_subdivision in |- *; eapply X. apply H2. split; assumption. @@ -2578,7 +2566,7 @@ Proof. (forall (l1 lf1:Rlist) (a b c:R) (f:R -> R), adapted_couple f a b l1 lf1 -> a <= c <= b -> - sigT (fun l:Rlist => sigT (fun l0:Rlist => adapted_couple f c b l l0))). + { l:Rlist & { l0:Rlist & adapted_couple f c b l l0 } }). intro X; unfold IsStepFun in |- *; unfold is_subdivision in |- *; eapply X; [ apply H2 | split; assumption ]. clear f a b c H0 H H1 H2 l1 lf1; simple induction l1. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 76579ccb..1a2fa03a 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rlimit.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Rlimit.v 10710 2008-03-23 09:24:09Z herbelin $ i*) (*********************************************************) (** Definition of the limit *) @@ -16,7 +16,8 @@ Require Import Rbase. Require Import Rfunctions. Require Import Classical_Prop. -Require Import Fourier. Open Local Scope R_scope. +Require Import Fourier. +Open Local Scope R_scope. (*******************************) (** * Calculus *) @@ -560,9 +561,9 @@ Proof. | apply Rlt_le_trans with (Rmin delta1 delta2); [ assumption | apply Rmin_l ] ]. change (0 < eps * (Rsqr l / 2)) in |- *; unfold Rdiv in |- *; - repeat rewrite Rmult_assoc; repeat apply Rmult_lt_0_compat. + repeat rewrite Rmult_assoc; apply Rmult_lt_0_compat. assumption. - apply Rsqr_pos_lt; assumption. + apply Rmult_lt_0_compat. apply Rsqr_pos_lt; assumption. apply Rinv_0_lt_compat; cut (0%nat <> 2%nat); [ intro H3; generalize (lt_INR_0 2 (neq_O_lt 2 H3)); unfold INR in |- *; intro; assumption diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v new file mode 100644 index 00000000..8aadf8f5 --- /dev/null +++ b/theories/Reals/Rlogic.v @@ -0,0 +1,293 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * This module proves some logical properties of the axiomatics of Reals + +1. Decidablity of arithmetical statements from + the axiom that the order of the real numbers is decidable. + +2. Derivability of the archimedean "axiom" +*) + +(** 1- Proof of the decidablity of arithmetical statements from +excluded middle and the axiom that the order of the real numbers is +decidable. *) + +(** Assuming a decidable predicate [P n], A series is constructed whose +[n]th term is 1/2^n if [P n] holds and 0 otherwise. This sum reaches 2 +only if [P n] holds for all [n], otherwise the sum is less than 2. +Comparing the sum to 2 decides if [forall n, P n] or [~forall n, P n] *) + +(** One can iterate this lemma and use classical logic to decide any +statement in the arithmetical hierarchy. *) + +(** Contributed by Cezary Kaliszyk and Russell O'Connor *) + +Require Import ConstructiveEpsilon. +Require Import Rfunctions. +Require Import PartSum. +Require Import SeqSeries. +Require Import RiemannInt. +Require Import Fourier. + +Section Arithmetical_dec. + +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). +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). +apply Rplus_le_compat_l. + induction (n - S m)%nat; simpl in *. + apply fpos. +replace 0 with (0 + 0) by ring. +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). +intros m n f mn pos. + elim (le_lt_or_eq _ _ mn). + intro; apply ge_fun_sums_ge_lemma; assumption. +intro H; rewrite H; auto with *. +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. +intros e He. +assert (X:(Pser (fun n:nat => 1) (1/2) (/ (1 - (1/2))))%R). + apply GP_infinite. + apply Rabs_def1; fourier. +assert (He':e/2 > 0) by fourier. +destruct (X _ He') as [N HN]. +clear X. +exists N. +intros n m Hn Hm. +replace e with (e/2 + e/2)%R by field. +set (g:=(fun n0 : nat => 1 * (1 / 2) ^ n0)) in *. +assert (R_dist (sum_f_R0 g n) (sum_f_R0 g m) < e / 2 + e / 2). + apply Rle_lt_trans with (R_dist (sum_f_R0 g n) 2+R_dist 2 (sum_f_R0 g m))%R. + apply R_dist_tri. + replace (/(1 - 1/2)) with 2 in HN by field. + cut (forall n, (n >= N)%nat -> R_dist (sum_f_R0 g n) 2 < e/2)%R. + intros Z. + apply Rplus_lt_compat. + apply Z; assumption. + rewrite R_dist_sym. + apply Z; assumption. + clear - HN He. + intros n Hn. + apply HN. + auto. +eapply Rle_lt_trans;[|apply H]. +clear -ge_fun_sums_ge n. +cut (forall n m, (m <= n)%nat -> R_dist (sum_f_R0 f n) (sum_f_R0 f m) <= R_dist (sum_f_R0 g n) (sum_f_R0 g m)). + intros H. + destruct (le_lt_dec m n). + apply H; assumption. + rewrite R_dist_sym. + rewrite (R_dist_sym (sum_f_R0 g n)). + apply H; auto with *. +clear n m. +intros n m Hnm. +unfold R_dist. +cut (forall i : nat, (1 / 2) ^ i >= 0). intro RPosPow. +rewrite Rabs_pos_eq. + rewrite Rabs_pos_eq. + cut (sum_f_R0 g m - sum_f_R0 f m <= sum_f_R0 g n - sum_f_R0 f n). + intros; fourier. + do 2 rewrite <- minus_sum. + apply (ge_fun_sums_ge m n (fun i : nat => g i - f i) Hnm). + intro i. + unfold f, g. + elim (HP i); intro; ring_simplify; auto with *. + cut (sum_f_R0 g m <= sum_f_R0 g n). + intro; fourier. + apply (ge_fun_sums_ge m n g Hnm). + intro. unfold g. + ring_simplify. + apply Rge_le. + apply RPosPow. + cut (sum_f_R0 f m <= sum_f_R0 f n). + intro; fourier. + apply (ge_fun_sums_ge m n f Hnm). + intro; unfold f. + elim (HP i); intro; simpl. + apply Rge_le. + apply RPosPow. + auto with *. +intro i. +apply Rle_ge. +apply pow_le. +fourier. +Qed. + +Lemma forall_dec : {forall n, P n} + {~forall n, P n}. +Proof. +destruct (cv_cauchy_2 _ cauchy_crit_geometric_dec_fun). + cut (2 <= x <-> forall n : nat, P n). + intro H. + elim (Rle_dec 2 x); intro X. + left; tauto. + right; tauto. +assert (A:Rabs(1/2) < 1) by (apply Rabs_def1; fourier). +assert (A0:=(GP_infinite (1/2) A)). +symmetry. + split; intro. + replace 2 with (/ (1 - (1 / 2))) by field. + unfold Pser, infinite_sum in A0. + eapply Rle_cv_lim;[|unfold Un_cv; apply A0 |apply u]. + intros n. + clear -n H. + induction n; unfold f;simpl. + destruct (HP 0); auto with *. + elim n; auto. + apply Rplus_le_compat; auto. + destruct (HP (S n)); auto with *. + elim n0; auto. +intros n. +destruct (HP n); auto. +elim (RIneq.Rle_not_lt _ _ H). +assert (B:0< (1/2)^n). + apply pow_lt. + fourier. +apply Rle_lt_trans with (2-(1/2)^n);[|fourier]. +replace (/(1-1/2))%R with 2 in A0 by field. +set (g:= fun m => if (eq_nat_dec m n) then (1/2)^n else 0). +assert (Z: Un_cv (fun N : nat => sum_f_R0 g N) ((1/2)^n)). + intros e He. + exists n. + intros a Ha. + replace (sum_f_R0 g a) with ((1/2)^n). + rewrite (R_dist_eq); assumption. + symmetry. + cut (forall a : nat, ((a >= n)%nat -> sum_f_R0 g a = (1 / 2) ^ n) /\ ((a < n)%nat -> sum_f_R0 g a = 0))%R. + intros H0. + destruct (H0 a). + auto. + clear - g. + induction a. + split; + intros H; + simpl; unfold g; + destruct (eq_nat_dec 0 n); try reflexivity. + elim f; auto with *. + elimtype False; omega. + destruct IHa as [IHa0 IHa1]. + split; + intros H; + simpl; unfold g at 2; + destruct (eq_nat_dec (S a) n). + rewrite IHa1. + ring. + omega. + ring_simplify. + apply IHa0. + omega. + elimtype False; omega. + ring_simplify. + apply IHa1. + omega. +assert (C:=CV_minus _ _ _ _ A0 Z). +eapply Rle_cv_lim;[|apply u |apply C]. +clear - n0 B. +intros m. +simpl. +induction m. + simpl. + unfold f, g. + destruct (eq_nat_dec 0 n). + destruct (HP 0). + elim n0. + congruence. + clear -n. + induction n; simpl; fourier. + destruct (HP); simpl; fourier. +cut (f (S m) <= 1 * ((1 / 2) ^ (S m)) - g (S m)). + intros L. + eapply Rle_trans. + simpl. + apply Rplus_le_compat. + apply IHm. + apply L. + simpl; fourier. +unfold f, g. +destruct (eq_nat_dec (S m) n). + destruct (HP (S m)). + elim n0. + congruence. + rewrite e. + fourier. +destruct (HP (S m)). + fourier. +ring_simplify. +apply pow_le. +fourier. +Qed. + +Lemma sig_forall_dec : {n | ~P n}+{forall n, P n}. +destruct forall_dec. + right; assumption. +left. +apply constructive_indefinite_description_nat; auto. + clear - HP. + firstorder. +apply Classical_Pred_Type.not_all_ex_not. +assumption. +Qed. + +End Arithmetical_dec. + +(** 2- Derivability of the Archimedean axiom *) + +(* This is a standard proof (it has been taken from PlanetMath). It is +formulated negatively so as to avoid the need for classical +logic. Using a proof of {n | ~P n}+{forall n, P n} (the one above or a +variant of it that does not need classical axioms) , we can in +principle also derive [up] and its [specification] *) + +Theorem not_not_archimedean : + forall r : R, ~ (forall n : nat, (INR n <= r)%R). +intros r H. +set (E := fun r => exists n : nat, r = INR n). +assert (exists x : R, E x) by + (exists 0%R; simpl; red; exists 0%nat; reflexivity). +assert (bound E) by (exists r; intros x (m,H2); rewrite H2; apply H). +destruct (completeness E) as (M,(H3,H4)); try assumption. +set (M' := (M + -1)%R). +assert (H2 : ~ is_upper_bound E M'). + intro H5. + assert (M <= M')%R by (apply H4; exact H5). + apply (Rlt_not_le M M'). + unfold M' in |- *. + pattern M at 2 in |- *. + rewrite <- Rplus_0_l. + pattern (0 + M)%R in |- *. + rewrite Rplus_comm. + rewrite <- (Rplus_opp_r 1). + apply Rplus_lt_compat_l. + rewrite Rplus_comm. + apply Rlt_plus_1. + assumption. +apply H2. +intros N (n,H7). +rewrite H7. +unfold M' in |- *. +assert (H5 : (INR (S n) <= M)%R) by (apply H3; exists (S n); reflexivity). +rewrite S_INR in H5. +assert (H6 : (INR n + 1 + -1 <= M + -1)%R). + apply Rplus_le_compat_r. + assumption. +rewrite Rplus_assoc in H6. +rewrite Rplus_opp_r in H6. +rewrite (Rplus_comm (INR n) 0) in H6. +rewrite Rplus_0_l in H6. +assumption. +Qed. diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v index 5bdbb76b..90ea9726 100644 --- a/theories/Reals/Rpow_def.v +++ b/theories/Reals/Rpow_def.v @@ -1,3 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: Rpow_def.v 10923 2008-05-12 18:25:06Z herbelin $ *) + Require Import Rdefinitions. Fixpoint pow (r:R) (n:nat) {struct n} : R := diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index cb6c59d5..adf53ef9 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rpower.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Rpower.v 10710 2008-03-23 09:24:09Z herbelin $ i*) (*i Due to L.Thery i*) (************************************************************) @@ -22,7 +22,8 @@ Require Import Exp_prop. Require Import Rsqrt_def. Require Import R_sqrt. Require Import MVT. -Require Import Ranalysis4. Open Local Scope R_scope. +Require Import Ranalysis4. +Open Local Scope R_scope. Lemma P_Rmin : forall (P:R -> Prop) (x y:R), P x -> P y -> P (Rmin x y). Proof. @@ -90,7 +91,7 @@ Proof. replace (/ INR (fact n)) with (1 ^ n / INR (fact n)). apply (H2 _ H3). unfold Rdiv in |- *; rewrite pow1; rewrite Rmult_1_l; reflexivity. - unfold infinit_sum in e; unfold Un_cv, tg_alt in |- *; intros; elim (e _ H0); + unfold infinite_sum in e; unfold Un_cv, tg_alt in |- *; intros; elim (e _ H0); intros; exists x0; intros; replace (sum_f_R0 (fun i:nat => (-1) ^ i * / INR (fact i)) n) with (sum_f_R0 (fun i:nat => / INR (fact i) * (-1) ^ i) n). @@ -150,62 +151,59 @@ Proof. symmetry in |- *; apply derive_pt_eq_0; apply derivable_pt_lim_exp. Qed. -Lemma ln_exists1 : forall y:R, 0 < y -> 1 <= y -> sigT (fun z:R => y = exp z). +Lemma ln_exists1 : forall y:R, 1 <= y -> { z:R | y = exp z }. Proof. - intros; set (f := fun x:R => exp x - y); cut (f 0 <= 0). - intro; cut (continuity f). - intro; cut (0 <= f y). - intro; cut (f 0 * f y <= 0). - intro; assert (X := IVT_cor f 0 y H2 (Rlt_le _ _ H) H4); elim X; intros t H5; - apply existT with t; elim H5; intros; unfold f in H7; - apply Rminus_diag_uniq_sym; exact H7. + intros; set (f := fun x:R => exp x - y). + assert (H0 : 0 < y) by (apply Rlt_le_trans with 1; auto with real). + cut (f 0 <= 0); [intro H1|]. + cut (continuity f); [intro H2|]. + cut (0 <= f y); [intro H3|]. + cut (f 0 * f y <= 0); [intro H4|]. + pose proof (IVT_cor f 0 y H2 (Rlt_le _ _ H0) H4) as (t,(_,H7)); + exists t; unfold f in H7; apply Rminus_diag_uniq_sym; exact H7. pattern 0 at 2 in |- *; rewrite <- (Rmult_0_r (f y)); rewrite (Rmult_comm (f 0)); apply Rmult_le_compat_l; assumption. unfold f in |- *; apply Rplus_le_reg_l with y; left; apply Rlt_trans with (1 + y). rewrite <- (Rplus_comm y); apply Rplus_lt_compat_l; apply Rlt_0_1. - replace (y + (exp y - y)) with (exp y); [ apply (exp_ineq1 y H) | ring ]. + replace (y + (exp y - y)) with (exp y); [ apply (exp_ineq1 y H0) | ring ]. unfold f in |- *; change (continuity (exp - fct_cte y)) in |- *; apply continuity_minus; [ apply derivable_continuous; apply derivable_exp | apply derivable_continuous; apply derivable_const ]. unfold f in |- *; rewrite exp_0; apply Rplus_le_reg_l with y; - rewrite Rplus_0_r; replace (y + (1 - y)) with 1; [ apply H0 | ring ]. + rewrite Rplus_0_r; replace (y + (1 - y)) with 1; [ apply H | ring ]. Qed. (**********) -Lemma ln_exists : forall y:R, 0 < y -> sigT (fun z:R => y = exp z). +Lemma ln_exists : forall y:R, 0 < y -> { z:R | y = exp z }. Proof. intros; case (Rle_dec 1 y); intro. - apply (ln_exists1 _ H r). + apply (ln_exists1 _ r). assert (H0 : 1 <= / y). apply Rmult_le_reg_l with y. apply H. rewrite <- Rinv_r_sym. rewrite Rmult_1_r; left; apply (Rnot_le_lt _ _ n). red in |- *; intro; rewrite H0 in H; elim (Rlt_irrefl _ H). - assert (H1 : 0 < / y). - apply Rinv_0_lt_compat; apply H. - assert (H2 := ln_exists1 _ H1 H0); elim H2; intros; apply existT with (- x); + destruct (ln_exists1 _ H0) as (x,p); exists (- x); apply Rmult_eq_reg_l with (exp x / y). unfold Rdiv in |- *; rewrite Rmult_assoc; rewrite <- Rinv_l_sym. rewrite Rmult_1_r; rewrite <- (Rmult_comm (/ y)); rewrite Rmult_assoc; rewrite <- exp_plus; rewrite Rplus_opp_r; rewrite exp_0; rewrite Rmult_1_r; symmetry in |- *; apply p. - red in |- *; intro; rewrite H3 in H; elim (Rlt_irrefl _ H). + red in |- *; intro H3; rewrite H3 in H; elim (Rlt_irrefl _ H). unfold Rdiv in |- *; apply prod_neq_R0. - assert (H3 := exp_pos x); red in |- *; intro; rewrite H4 in H3; + assert (H3 := exp_pos x); red in |- *; intro H4; rewrite H4 in H3; elim (Rlt_irrefl _ H3). - apply Rinv_neq_0_compat; red in |- *; intro; rewrite H3 in H; + apply Rinv_neq_0_compat; red in |- *; intro H3; rewrite H3 in H; elim (Rlt_irrefl _ H). Qed. (* Definition of log R+* -> R *) Definition Rln (y:posreal) : R := - match ln_exists (pos y) (cond_pos y) with - | existT a b => a - end. + let (a,_) := ln_exists (pos y) (cond_pos y) in a. (* Extension on R *) Definition ln (x:R) : R := @@ -403,6 +401,16 @@ Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope. (** * Properties of Rpower *) (******************************************************************) +(** Note: [Rpower] is prolongated to [1] on negative real numbers and + it thus does not extend integer power. The next two lemmas, which + hold for integer power, accidentally hold on negative real numbers + as a side effect of the default value taken on negative real + numbers. Contrastingly, the lemmas that do not hold for the + integer power of a negative number are stated for [Rpower] on the + positive numbers only (even if they accidentally hold due to the + default value of [Rpower] on the negative side, as it is the case + for [Rpower_O]). *) + Theorem Rpower_plus : forall x y z:R, z ^R (x + y) = z ^R x * z ^R y. Proof. intros x y z; unfold Rpower in |- *. @@ -420,7 +428,7 @@ Qed. Theorem Rpower_O : forall x:R, 0 < x -> x ^R 0 = 1. Proof. - intros x H; unfold Rpower in |- *. + intros x _; unfold Rpower in |- *. rewrite Rmult_0_l; apply exp_0. Qed. diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index a84d5149..2113cc8f 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rprod.v 9298 2006-10-27 13:05:29Z notin $ i*) +(*i $Id: Rprod.v 10146 2007-09-27 12:28:12Z herbelin $ i*) Require Import Compare. Require Import Rbase. @@ -16,41 +16,42 @@ Require Import PartSum. Require Import Binomial. Open Local Scope R_scope. -(** TT Ak; 1<=k<=N *) -Boxed Fixpoint prod_f_SO (An:nat -> R) (N:nat) {struct N} : R := +(** TT Ak; 0<=k<=N *) +Boxed Fixpoint prod_f_R0 (f:nat -> R) (N:nat) {struct N} : R := match N with - | O => 1 - | S p => prod_f_SO An p * An (S p) + | O => f O + | S p => prod_f_R0 f p * f (S p) end. +Notation prod_f_SO := (fun An N => prod_f_R0 (fun n => An (S n)) N). + (**********) Lemma prod_SO_split : forall (An:nat -> R) (n k:nat), - (k <= n)%nat -> - prod_f_SO An n = - prod_f_SO An k * prod_f_SO (fun l:nat => An (k + l)%nat) (n - k). + (k < n)%nat -> + prod_f_R0 An n = + prod_f_R0 An k * prod_f_R0 (fun l:nat => An (k +1+l)%nat) (n - k -1). Proof. intros; induction n as [| n Hrecn]. - cut (k = 0%nat); - [ intro; rewrite H0; simpl in |- *; ring | inversion H; reflexivity ]. - cut (k = S n \/ (k <= n)%nat). - intro; elim H0; intro. - rewrite H1; simpl in |- *; rewrite <- minus_n_n; simpl in |- *; ring. - replace (S n - k)%nat with (S (n - k)). + absurd (k < 0)%nat; omega. + cut (k = n \/ (k < n)%nat);[intro; elim H0; intro|omega]. + replace (S n - k - 1)%nat with O; [rewrite H1; simpl|omega]. + replace (n+1+0)%nat with (S n); ring. + replace (S n - k-1)%nat with (S (n - k-1));[idtac|omega]. simpl in |- *; replace (k + S (n - k))%nat with (S n). + replace (k + 1 + S (n - k - 1))%nat with (S n). rewrite Hrecn; [ ring | assumption ]. omega. omega. - omega. -Qed. +Qed. (**********) Lemma prod_SO_pos : forall (An:nat -> R) (N:nat), - (forall n:nat, (n <= N)%nat -> 0 <= An n) -> 0 <= prod_f_SO An N. + (forall n:nat, (n <= N)%nat -> 0 <= An n) -> 0 <= prod_f_R0 An N. Proof. intros; induction N as [| N HrecN]. - simpl in |- *; left; apply Rlt_0_1. + simpl in |- *; apply H; trivial. simpl in |- *; apply Rmult_le_pos. apply HrecN; intros; apply H; apply le_trans with N; [ assumption | apply le_n_Sn ]. @@ -61,11 +62,11 @@ Qed. Lemma prod_SO_Rle : forall (An Bn:nat -> R) (N:nat), (forall n:nat, (n <= N)%nat -> 0 <= An n <= Bn n) -> - prod_f_SO An N <= prod_f_SO Bn N. + prod_f_R0 An N <= prod_f_R0 Bn N. Proof. intros; induction N as [| N HrecN]. - right; reflexivity. - simpl in |- *; apply Rle_trans with (prod_f_SO An N * Bn (S N)). + elim H with O; trivial. + simpl in |- *; apply Rle_trans with (prod_f_R0 An N * Bn (S N)). apply Rmult_le_compat_l. apply prod_SO_pos; intros; elim (H n (le_trans _ _ _ H0 (le_n_Sn N))); intros; assumption. @@ -79,12 +80,17 @@ Qed. (** Application to factorial *) Lemma fact_prodSO : - forall n:nat, INR (fact n) = prod_f_SO (fun k:nat => INR k) n. + forall n:nat, INR (fact n) = prod_f_R0 (fun k:nat => + (match (eq_nat_dec k 0) with + | left _ => 1%R + | right _ => INR k + end)) n. Proof. intro; induction n as [| n Hrecn]. reflexivity. - change (INR (S n * fact n) = prod_f_SO (fun k:nat => INR k) (S n)) in |- *. - rewrite mult_INR; rewrite Rmult_comm; rewrite Hrecn; reflexivity. + simpl; rewrite <- Hrecn. + case n; auto with real. + intros; repeat rewrite plus_INR;rewrite mult_INR;ring. Qed. Lemma le_n_2n : forall n:nat, (n <= 2 * n)%nat. @@ -104,40 +110,58 @@ Lemma RfactN_fact2N_factk : (k <= 2 * N)%nat -> Rsqr (INR (fact N)) <= INR (fact (2 * N - k)) * INR (fact k). Proof. + assert (forall (n:nat), 0 <= (if eq_nat_dec n 0 then 1 else INR n)). + intros; case (eq_nat_dec n 0); auto with real. + assert (forall (n:nat), (0 < n)%nat -> + (if eq_nat_dec n 0 then 1 else INR n) = INR n). + intros n; case (eq_nat_dec n 0); auto with real. + intros; absurd (0 < n)%nat; omega. intros; unfold Rsqr in |- *; repeat rewrite fact_prodSO. - cut ((k <= N)%nat \/ (N <= k)%nat). - intro; elim H0; intro. - rewrite (prod_SO_split (fun l:nat => INR l) (2 * N - k) N). + cut ((k=N)%nat \/ (k < N)%nat \/ (N < k)%nat). + intro H2; elim H2; intro H3. + rewrite H3; replace (2*N-N)%nat with N;[right; ring|omega]. + case H3; intro; clear H2 H3. + rewrite (prod_SO_split (fun l:nat => if eq_nat_dec l 0 then 1 else INR l) (2 * N - k) N). rewrite Rmult_assoc; apply Rmult_le_compat_l. - apply prod_SO_pos; intros; apply pos_INR. - replace (2 * N - k - N)%nat with (N - k)%nat. - rewrite Rmult_comm; rewrite (prod_SO_split (fun l:nat => INR l) N k). + apply prod_SO_pos; intros; auto. + replace (2 * N - k - N-1)%nat with (N - k-1)%nat. + rewrite Rmult_comm; rewrite (prod_SO_split + (fun l:nat => if eq_nat_dec l 0 then 1 else INR l) N k). apply Rmult_le_compat_l. - apply prod_SO_pos; intros; apply pos_INR. - apply prod_SO_Rle; intros; split. - apply pos_INR. - apply le_INR; apply plus_le_compat_r; assumption. + apply prod_SO_pos; intros; auto. + apply prod_SO_Rle; intros; split; auto. + rewrite H0. + rewrite H0. + apply le_INR; omega. + omega. + omega. assumption. omega. omega. - rewrite <- (Rmult_comm (prod_f_SO (fun l:nat => INR l) k)); - rewrite (prod_SO_split (fun l:nat => INR l) k N). + rewrite <- (Rmult_comm (prod_f_R0 (fun l:nat => + if eq_nat_dec l 0 then 1 else INR l) k)); + rewrite (prod_SO_split (fun l:nat => + if eq_nat_dec l 0 then 1 else INR l) k N). rewrite Rmult_assoc; apply Rmult_le_compat_l. - apply prod_SO_pos; intros; apply pos_INR. + apply prod_SO_pos; intros; auto. rewrite Rmult_comm; - rewrite (prod_SO_split (fun l:nat => INR l) N (2 * N - k)). + rewrite (prod_SO_split (fun l:nat => + if eq_nat_dec l 0 then 1 else INR l) N (2 * N - k)). apply Rmult_le_compat_l. - apply prod_SO_pos; intros; apply pos_INR. - replace (N - (2 * N - k))%nat with (k - N)%nat. - apply prod_SO_Rle; intros; split. - apply pos_INR. - apply le_INR; apply plus_le_compat_r. + apply prod_SO_pos; intros; auto. + replace (N - (2 * N - k)-1)%nat with (k - N-1)%nat. + apply prod_SO_Rle; intros; split; auto. + rewrite H0. + rewrite H0. + apply le_INR; omega. + omega. omega. omega. omega. assumption. omega. -Qed. +Qed. + (**********) Lemma INR_fact_lt_0 : forall n:nat, 0 < INR (fact n). diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 38c39bae..702aafa4 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rseries.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Rseries.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -194,14 +194,14 @@ Section Isequence. Variable An : nat -> R. (*********) - Definition Pser (x l:R) : Prop := infinit_sum (fun n:nat => An n * x ^ n) l. + Definition Pser (x l:R) : Prop := infinite_sum (fun n:nat => An n * x ^ n) l. End Isequence. Lemma GP_infinite : forall x:R, Rabs x < 1 -> Pser (fun n:nat => 1) x (/ (1 - x)). Proof. - intros; unfold Pser in |- *; unfold infinit_sum in |- *; intros; + intros; unfold Pser in |- *; unfold infinite_sum in |- *; intros; elim (Req_dec x 0). intros; exists 0%nat; intros; rewrite H1; rewrite Rminus_0_r; rewrite Rinv_1; cut (sum_f_R0 (fun n0:nat => 1 * 0 ^ n0) n = 1). diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v index cb31d3b2..7cdd4d02 100644 --- a/theories/Reals/Rsigma.v +++ b/theories/Reals/Rsigma.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rsigma.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: Rsigma.v 9454 2006-12-15 15:30:59Z bgregoir $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index 0a9f7754..0a3af6ca 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rsqrt_def.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: Rsqrt_def.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Sumbool. Require Import Rbase. @@ -192,7 +192,7 @@ Qed. Lemma dicho_lb_cv : forall (x y:R) (P:R -> bool), - x <= y -> sigT (fun l:R => Un_cv (dicho_lb x y P) l). + x <= y -> { l:R | Un_cv (dicho_lb x y P) l }. Proof. intros. apply growing_cv. @@ -202,7 +202,7 @@ Qed. Lemma dicho_up_cv : forall (x y:R) (P:R -> bool), - x <= y -> sigT (fun l:R => Un_cv (dicho_up x y P) l). + x <= y -> { l:R | Un_cv (dicho_up x y P) l }. Proof. intros. apply decreasing_cv. @@ -466,7 +466,7 @@ Qed. Lemma IVT : forall (f:R -> R) (x y:R), continuity f -> - x < y -> f x < 0 -> 0 < f y -> sigT (fun z:R => x <= z <= y /\ f z = 0). + x < y -> f x < 0 -> 0 < f y -> { z:R | x <= z <= y /\ f z = 0 }. Proof. intros. cut (x <= y). @@ -478,7 +478,7 @@ Proof. elim X0; intros. assert (H4 := cv_dicho _ _ _ _ _ H3 p0 p). rewrite H4 in p0. - apply existT with x0. + exists x0. split. split. apply Rle_trans with (dicho_lb x y (fun z:R => cond_positivity (f z)) 0). @@ -602,7 +602,7 @@ Qed. Lemma IVT_cor : forall (f:R -> R) (x y:R), continuity f -> - x <= y -> f x * f y <= 0 -> sigT (fun z:R => x <= z <= y /\ f z = 0). + x <= y -> f x * f y <= 0 -> { z:R | x <= z <= y /\ f z = 0 }. Proof. intros. case (total_order_T 0 (f x)); intro. @@ -628,7 +628,7 @@ Proof. cut (0 < (- f)%F y). intros. elim (H3 H5 H4); intros. - apply existT with x0. + exists x0. elim p; intros. split. assumption. @@ -643,7 +643,7 @@ Proof. assumption. rewrite H2 in a. elim (Rlt_irrefl _ (Rlt_trans _ _ _ r a)). - apply existT with x. + exists x. split. split; [ right; reflexivity | assumption ]. symmetry in |- *; assumption. @@ -656,7 +656,7 @@ Proof. assumption. rewrite H2 in r. elim (Rlt_irrefl _ (Rlt_trans _ _ _ r a)). - apply existT with y. + exists y. split. split; [ assumption | right; reflexivity ]. symmetry in |- *; assumption. @@ -670,7 +670,7 @@ Qed. (** We can now define the square root function as the reciprocal transformation of the square root function *) Lemma Rsqrt_exists : - forall y:R, 0 <= y -> sigT (fun z:R => 0 <= z /\ y = Rsqr z). + forall y:R, 0 <= y -> { z:R | 0 <= z /\ y = Rsqr z }. Proof. intros. set (f := fun x:R => Rsqr x - y). @@ -686,7 +686,7 @@ Proof. intro. assert (X := IVT_cor f 0 1 H1 (Rlt_le _ _ Rlt_0_1) H3). elim X; intros t H4. - apply existT with t. + exists t. elim H4; intros. split. elim H5; intros; assumption. @@ -700,7 +700,7 @@ Proof. rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus in |- *; rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; left; assumption. - apply existT with 1. + exists 1. split. left; apply Rlt_0_1. rewrite b; symmetry in |- *; apply Rsqr_1. @@ -710,7 +710,7 @@ Proof. intro. assert (X := IVT_cor f 0 y H1 H H3). elim X; intros t H4. - apply existT with t. + exists t. elim H4; intros. split. elim H5; intros; assumption. @@ -739,9 +739,7 @@ Qed. (* Definition of the square root: R+->R *) Definition Rsqrt (y:nonnegreal) : R := - match Rsqrt_exists (nonneg y) (cond_nonneg y) with - | existT a b => a - end. + let (a,_) := Rsqrt_exists (nonneg y) (cond_nonneg y) in a. (**********) Lemma Rsqrt_positivity : forall x:nonnegreal, 0 <= Rsqrt x. diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index aa47d72f..9501bc1e 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -6,15 +6,15 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rtopology.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Rtopology.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. Require Import RList. Require Import Classical_Prop. -Require Import Classical_Pred_Type. Open Local Scope R_scope. - +Require Import Classical_Pred_Type. +Open Local Scope R_scope. (** * General definitions and propositions *) diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index b744c788..0baece39 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rtrigo.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: Rtrigo.v 9454 2006-12-15 15:30:59Z bgregoir $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index 89ee1745..d82bafc6 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rtrigo_alt.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: Rtrigo_alt.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -137,7 +137,7 @@ Proof. ring. assert (X := exist_sin (Rsqr a)); elim X; intros. cut (x = sin a / a). - intro; rewrite H3 in p; unfold sin_in in p; unfold infinit_sum in p; + intro; rewrite H3 in p; unfold sin_in in p; unfold infinite_sum in p; unfold R_dist in p; unfold Un_cv in |- *; unfold R_dist in |- *; intros. cut (0 < eps / Rabs a). @@ -327,7 +327,7 @@ Proof. apply (fun m n p:nat => mult_le_compat_l p n m); apply le_n_S; assumption. assert (X := exist_cos (Rsqr a0)); elim X; intros. cut (x = cos a0). - intro; rewrite H4 in p; unfold cos_in in p; unfold infinit_sum in p; + intro; rewrite H4 in p; unfold cos_in in p; unfold infinite_sum in p; unfold R_dist in p; unfold Un_cv in |- *; unfold R_dist in |- *; intros. elim (p _ H5); intros N H6. diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index b2aeb766..e94d7448 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rtrigo_def.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Rtrigo_def.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -19,7 +19,7 @@ Open Local Scope R_scope. (** * Definition of exponential *) (********************************) Definition exp_in (x l:R) : Prop := - infinit_sum (fun i:nat => / INR (fact i) * x ^ i) l. + infinite_sum (fun i:nat => / INR (fact i) * x ^ i) l. Lemma exp_cof_no_R0 : forall n:nat, / INR (fact n) <> 0. Proof. @@ -28,7 +28,7 @@ Proof. apply INR_fact_neq_0. Qed. -Lemma exist_exp : forall x:R, sigT (fun l:R => exp_in x l). +Lemma exist_exp : forall x:R, { l:R | exp_in x l }. Proof. intro; generalize @@ -37,7 +37,7 @@ Proof. trivial. Defined. -Definition exp (x:R) : R := projT1 (exist_exp x). +Definition exp (x:R) : R := proj1_sig (exist_exp x). Lemma pow_i : forall i:nat, (0 < i)%nat -> 0 ^ i = 0. Proof. @@ -45,11 +45,10 @@ Proof. red in |- *; intro; rewrite H0 in H; elim (lt_irrefl _ H). Qed. -(*i Calculus of $e^0$ *) -Lemma exist_exp0 : sigT (fun l:R => exp_in 0 l). +Lemma exist_exp0 : { l:R | exp_in 0 l }. Proof. - apply existT with 1. - unfold exp_in in |- *; unfold infinit_sum in |- *; intros. + exists 1. + unfold exp_in in |- *; unfold infinite_sum in |- *; intros. exists 0%nat. intros; replace (sum_f_R0 (fun i:nat => / INR (fact i) * 0 ^ i) n) with 1. unfold R_dist in |- *; replace (1 - 1) with 0; @@ -63,6 +62,7 @@ Proof. unfold ge in |- *; apply le_O_n. Defined. +(* Value of [exp 0] *) Lemma exp_0 : exp 0 = 1. Proof. cut (exp_in 0 (exp 0)). @@ -70,8 +70,8 @@ Proof. unfold exp_in in |- *; intros; eapply uniqueness_sum. apply H0. apply H. - exact (projT2 exist_exp0). - exact (projT2 (exist_exp 0)). + exact (proj2_sig exist_exp0). + exact (proj2_sig (exist_exp 0)). Qed. (*****************************************) @@ -235,21 +235,17 @@ Qed. (**********) Definition cos_in (x l:R) : Prop := - infinit_sum (fun i:nat => cos_n i * x ^ i) l. + infinite_sum (fun i:nat => cos_n i * x ^ i) l. (**********) -Lemma exist_cos : forall x:R, sigT (fun l:R => cos_in x l). +Lemma exist_cos : forall x:R, { l:R | cos_in x l }. intro; generalize (Alembert_C3 cos_n x cosn_no_R0 Alembert_cos). unfold Pser, cos_in in |- *; trivial. Qed. (** Definition of cosinus *) -Definition cos (x:R) : R := - match exist_cos (Rsqr x) with - | existT a b => a - end. - +Definition cos (x:R) : R := let (a,_) := exist_cos (Rsqr x) in a. Definition sin_n (n:nat) : R := (-1) ^ n / INR (fact (2 * n + 1)). @@ -348,7 +344,7 @@ Proof. apply INR_eq; repeat rewrite S_INR; rewrite plus_INR; repeat rewrite mult_INR; rewrite plus_INR; rewrite mult_INR; repeat rewrite S_INR; replace (INR 0) with 0; [ ring | reflexivity ]. -Qed. +Defined. Lemma sin_no_R0 : forall n:nat, sin_n n <> 0. Proof. @@ -359,21 +355,18 @@ Qed. (**********) Definition sin_in (x l:R) : Prop := - infinit_sum (fun i:nat => sin_n i * x ^ i) l. + infinite_sum (fun i:nat => sin_n i * x ^ i) l. (**********) -Lemma exist_sin : forall x:R, sigT (fun l:R => sin_in x l). +Lemma exist_sin : forall x:R, { l:R | sin_in x l }. Proof. intro; generalize (Alembert_C3 sin_n x sin_no_R0 Alembert_sin). unfold Pser, sin_n in |- *; trivial. -Qed. +Defined. (***********************) (* Definition of sinus *) -Definition sin (x:R) : R := - match exist_sin (Rsqr x) with - | existT a b => x * a - end. +Definition sin (x:R) : R := let (a,_) := exist_sin (Rsqr x) in x * a. (*********************************************) (** * Properties *) @@ -399,10 +392,10 @@ Proof. intros; ring. Qed. -Lemma exist_cos0 : sigT (fun l:R => cos_in 0 l). +Lemma exist_cos0 : { l:R | cos_in 0 l }. Proof. - apply existT with 1. - unfold cos_in in |- *; unfold infinit_sum in |- *; intros; exists 0%nat. + exists 1. + unfold cos_in in |- *; unfold infinite_sum in |- *; intros; exists 0%nat. intros. unfold R_dist in |- *. induction n as [| n Hrecn]. @@ -417,7 +410,7 @@ Proof. simpl in |- *; ring. Defined. -(* Calculus of (cos 0) *) +(* Value of [cos 0] *) Lemma cos_0 : cos 0 = 1. Proof. cut (cos_in 0 (cos 0)). @@ -425,7 +418,7 @@ Proof. unfold cos_in in |- *; intros; eapply uniqueness_sum. apply H0. apply H. - exact (projT2 exist_cos0). - assert (H := projT2 (exist_cos (Rsqr 0))); unfold cos in |- *; + exact (proj2_sig exist_cos0). + assert (H := proj2_sig (exist_cos (Rsqr 0))); unfold cos in |- *; pattern 0 at 1 in |- *; replace 0 with (Rsqr 0); [ exact H | apply Rsqr_0 ]. Qed. diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v index 78ef847f..6eec0329 100644 --- a/theories/Reals/Rtrigo_fun.v +++ b/theories/Reals/Rtrigo_fun.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rtrigo_fun.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Rtrigo_fun.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -15,8 +15,7 @@ Open Local Scope R_scope. (*****************************************************************) (** To define transcendental functions *) -(** for exponential function *) -(* *) +(** and exponential function *) (*****************************************************************) (*********) diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index b105ca69..139563bf 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rtrigo_reg.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: Rtrigo_reg.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -25,16 +25,15 @@ Proof. unfold CVN_R in |- *; intros. cut ((r:R) <> 0). intro hyp_r; unfold CVN_r in |- *. - apply existT with (fun n:nat => / INR (fact (2 * n)) * r ^ (2 * n)). + exists (fun n:nat => / INR (fact (2 * n)) * r ^ (2 * n)). cut - (sigT - (fun l:R => + { l:R | Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k)) * r ^ (2 * k))) - n) l)). + n) l }. intro X; elim X; intros. - apply existT with x. + exists x. split. apply p. intros; rewrite H; unfold Rdiv in |- *; do 2 rewrite Rabs_mult. @@ -124,7 +123,7 @@ Lemma continuity_cos : continuity cos. Proof. set (fn := fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N)) * x ^ (2 * N)). cut (CVN_R fn). - intro; cut (forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)). + intro; cut (forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }). intro cv; cut (forall n:nat, continuity (fn n)). intro; cut (forall x:R, cos x = SFL fn cv x). intro; cut (continuity (SFL fn cv) -> continuity cos). @@ -144,7 +143,7 @@ Proof. case (cv x); case (exist_cos (Rsqr x)); intros. symmetry in |- *; eapply UL_sequence. apply u. - unfold cos_in in c; unfold infinit_sum in c; unfold Un_cv in |- *; intros. + unfold cos_in in c; unfold infinite_sum in c; unfold Un_cv in |- *; intros. elim (c _ H0); intros N0 H1. exists N0; intros. unfold R_dist in H1; unfold R_dist, SP in |- *. @@ -200,17 +199,16 @@ Lemma CVN_R_sin : CVN_R fn. Proof. unfold CVN_R in |- *; unfold CVN_r in |- *; intros fn H r. - apply existT with (fun n:nat => / INR (fact (2 * n + 1)) * r ^ (2 * n)). + exists (fun n:nat => / INR (fact (2 * n + 1)) * r ^ (2 * n)). cut - (sigT - (fun l:R => + { l:R | Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k + 1)) * r ^ (2 * k))) n) - l)). + l }. intro X; elim X; intros. - apply existT with x. + exists x. split. apply p. intros; rewrite H; unfold Rdiv in |- *; do 2 rewrite Rabs_mult; @@ -305,7 +303,7 @@ Proof. set (fn := fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N + 1)) * x ^ (2 * N)). cut (CVN_R fn). - intro; cut (forall x:R, sigT (fun l:R => Un_cv (fun N:nat => SP fn N x) l)). + intro; cut (forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }). intro cv. set (r := mkposreal _ Rlt_0_1). cut (CVN_r fn r). @@ -331,7 +329,7 @@ Proof. unfold Rdiv in |- *; rewrite (Rinv_r_simpl_m h x0 H6). eapply UL_sequence. apply u. - unfold sin_in in s; unfold sin_n, infinit_sum in s; + unfold sin_in in s; unfold sin_n, infinite_sum in s; unfold SP, fn, Un_cv in |- *; intros. elim (s _ H10); intros N0 H11. exists N0; intros. @@ -584,14 +582,14 @@ Qed. Lemma derivable_pt_sin : forall x:R, derivable_pt sin x. Proof. unfold derivable_pt in |- *; intro. - apply existT with (cos x). + exists (cos x). apply derivable_pt_lim_sin. Qed. Lemma derivable_pt_cos : forall x:R, derivable_pt cos x. Proof. unfold derivable_pt in |- *; intro. - apply existT with (- sin x). + exists (- sin x). apply derivable_pt_lim_cos. Qed. diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 96351618..56088a2e 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: SeqProp.v 9551 2007-01-29 15:13:35Z bgregoir $ i*) +(*i $Id: SeqProp.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -15,6 +15,10 @@ Require Import Classical. Require Import Max. Open Local Scope R_scope. +(*****************************************************************) +(** Convergence properties of sequences *) +(*****************************************************************) + Definition Un_decreasing (Un:nat -> R) : Prop := forall n:nat, Un (S n) <= Un n. Definition opp_seq (Un:nat -> R) (n:nat) : R := - Un n. @@ -23,8 +27,7 @@ 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 -> sigT (fun l:R => Un_cv Un l). + 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]]. @@ -64,11 +67,10 @@ Proof. Qed. Lemma decreasing_cv : - forall Un:nat -> R, - Un_decreasing Un -> has_lb Un -> sigT (fun l:R => Un_cv Un l). + forall Un:nat -> R, Un_decreasing Un -> has_lb Un -> { l:R | Un_cv Un l }. Proof. intros. - cut (sigT (fun l:R => Un_cv (opp_seq Un) l) -> sigT (fun l:R => Un_cv Un l)). + cut ({ l:R | Un_cv (opp_seq Un) l } -> { l:R | Un_cv Un l }). intro X. apply X. apply growing_cv. @@ -76,7 +78,7 @@ Proof. exact H0. intro X. elim X; intros. - apply existT with (- x). + exists (- x). unfold Un_cv in p. unfold R_dist in p. unfold opp_seq in p. @@ -91,8 +93,8 @@ Proof. Qed. (***********) -Lemma maj_sup : - forall Un:nat -> R, has_ub Un -> sigT (fun l:R => is_lub (EUn Un) l). +Lemma ub_to_lub : + forall Un:nat -> R, has_ub Un -> { l:R | is_lub (EUn Un) l }. Proof. intros. unfold has_ub in H. @@ -104,9 +106,8 @@ Proof. Qed. (**********) -Lemma min_inf : - forall Un:nat -> R, - has_lb Un -> sigT (fun l:R => is_lub (EUn (opp_seq Un)) l). +Lemma lb_to_glb : + forall Un:nat -> R, has_lb Un -> { l:R | is_lub (EUn (opp_seq Un)) l }. Proof. intros; unfold has_lb in H. apply completeness. @@ -116,15 +117,17 @@ Proof. reflexivity. Qed. -Definition majorant (Un:nat -> R) (pr:has_ub Un) : R := - match maj_sup Un pr with - | existT a b => a - end. +Definition lub (Un:nat -> R) (pr:has_ub Un) : R := + let (a,_) := ub_to_lub Un pr in a. -Definition minorant (Un:nat -> R) (pr:has_lb Un) : R := - match min_inf Un pr with - | existT a b => - a - end. +Definition glb (Un:nat -> R) (pr:has_lb Un) : R := + let (a,_) := lb_to_glb Un pr in - a. + +(* Compatibility with previous unappropriate terminology *) +Notation maj_sup := ub_to_lub (only parsing). +Notation min_inf := lb_to_glb (only parsing). +Notation majorant := lub (only parsing). +Notation minorant := glb (only parsing). Lemma maj_ss : forall (Un:nat -> R) (k:nat), @@ -162,26 +165,30 @@ Proof. exists (k + x1)%nat; assumption. Qed. -Definition sequence_majorant (Un:nat -> R) (pr:has_ub Un) - (i:nat) : R := majorant (fun k:nat => Un (i + k)%nat) (maj_ss Un i pr). +Definition sequence_ub (Un:nat -> R) (pr:has_ub Un) + (i:nat) : R := lub (fun k:nat => Un (i + k)%nat) (maj_ss Un i pr). + +Definition sequence_lb (Un:nat -> R) (pr:has_lb Un) + (i:nat) : R := glb (fun k:nat => Un (i + k)%nat) (min_ss Un i pr). -Definition sequence_minorant (Un:nat -> R) (pr:has_lb Un) - (i:nat) : R := minorant (fun k:nat => Un (i + k)%nat) (min_ss Un i pr). +(* Compatibility *) +Notation sequence_majorant := sequence_ub (only parsing). +Notation sequence_minorant := sequence_lb (only parsing). Lemma Wn_decreasing : - forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_majorant Un pr). + forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_ub Un pr). Proof. intros. unfold Un_decreasing in |- *. intro. - unfold sequence_majorant in |- *. - assert (H := maj_sup (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)). - assert (H0 := maj_sup (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)). + unfold sequence_ub in |- *. + assert (H := ub_to_lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)). + assert (H0 := ub_to_lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)). elim H; intros. elim H0; intros. - cut (majorant (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr) = x); + cut (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr) = x); [ intro Maj1; rewrite Maj1 | idtac ]. - cut (majorant (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr) = x0); + cut (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr) = x0); [ intro Maj2; rewrite Maj2 | idtac ]. unfold is_lub in p. unfold is_lub in p0. @@ -199,47 +206,47 @@ Proof. replace (S n) with (1 + n)%nat; [ ring | ring ]. cut (is_lub (EUn (fun k:nat => Un (n + k)%nat)) - (majorant (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr))). + (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr))). intro. unfold is_lub in p0; unfold is_lub in H1. elim p0; intros; elim H1; intros. assert (H6 := H5 x0 H2). assert - (H7 := H3 (majorant (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)) H4). + (H7 := H3 (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)) H4). apply Rle_antisym; assumption. - unfold majorant in |- *. - case (maj_sup (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)). + unfold lub in |- *. + case (ub_to_lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)). trivial. cut (is_lub (EUn (fun k:nat => Un (S n + k)%nat)) - (majorant (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr))). + (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr))). intro. unfold is_lub in p; unfold is_lub in H1. elim p; intros; elim H1; intros. assert (H6 := H5 x H2). assert (H7 := - H3 (majorant (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)) H4). + H3 (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)) H4). apply Rle_antisym; assumption. - unfold majorant in |- *. - case (maj_sup (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)). + unfold lub in |- *. + case (ub_to_lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)). trivial. Qed. Lemma Vn_growing : - forall (Un:nat -> R) (pr:has_lb Un), Un_growing (sequence_minorant Un pr). + forall (Un:nat -> R) (pr:has_lb Un), Un_growing (sequence_lb Un pr). Proof. intros. unfold Un_growing in |- *. intro. - unfold sequence_minorant in |- *. - assert (H := min_inf (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr)). - assert (H0 := min_inf (fun k:nat => Un (n + k)%nat) (min_ss Un n pr)). + unfold sequence_lb in |- *. + assert (H := lb_to_glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr)). + assert (H0 := lb_to_glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr)). elim H; intros. elim H0; intros. - cut (minorant (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr) = - x); + cut (glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr) = - x); [ intro Maj1; rewrite Maj1 | idtac ]. - cut (minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr) = - x0); + cut (glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr) = - x0); [ intro Maj2; rewrite Maj2 | idtac ]. unfold is_lub in p. unfold is_lub in p0. @@ -260,38 +267,38 @@ Proof. replace (S n) with (1 + n)%nat; [ ring | ring ]. cut (is_lub (EUn (opp_seq (fun k:nat => Un (n + k)%nat))) - (- minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr))). + (- glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr))). intro. unfold is_lub in p0; unfold is_lub in H1. elim p0; intros; elim H1; intros. assert (H6 := H5 x0 H2). assert - (H7 := H3 (- minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr)) H4). + (H7 := H3 (- glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr)) H4). rewrite <- - (Ropp_involutive (minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr))) + (Ropp_involutive (glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr))) . apply Ropp_eq_compat; apply Rle_antisym; assumption. - unfold minorant in |- *. - case (min_inf (fun k:nat => Un (n + k)%nat) (min_ss Un n pr)). + unfold glb in |- *. + case (lb_to_glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr)); simpl. intro; rewrite Ropp_involutive. trivial. cut (is_lub (EUn (opp_seq (fun k:nat => Un (S n + k)%nat))) - (- minorant (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr))). + (- glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr))). intro. unfold is_lub in p; unfold is_lub in H1. elim p; intros; elim H1; intros. assert (H6 := H5 x H2). assert (H7 := - H3 (- minorant (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr)) H4). + H3 (- glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr)) H4). rewrite <- (Ropp_involutive - (minorant (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr))) + (glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr))) . apply Ropp_eq_compat; apply Rle_antisym; assumption. - unfold minorant in |- *. - case (min_inf (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr)). + unfold glb in |- *. + case (lb_to_glb (fun k:nat => Un (S n + k)%nat) (min_ss Un (S n) pr)); simpl. intro; rewrite Ropp_involutive. trivial. Qed. @@ -299,16 +306,15 @@ Qed. (**********) Lemma Vn_Un_Wn_order : forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un) - (n:nat), sequence_minorant Un pr2 n <= Un n <= sequence_majorant Un pr1 n. + (n:nat), sequence_lb Un pr2 n <= Un n <= sequence_ub Un pr1 n. Proof. intros. split. - unfold sequence_minorant in |- *. - cut - (sigT (fun l:R => is_lub (EUn (opp_seq (fun i:nat => Un (n + i)%nat))) l)). + unfold sequence_lb in |- *. + cut { l:R | is_lub (EUn (opp_seq (fun i:nat => Un (n + i)%nat))) l }. intro X. elim X; intros. - replace (minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)) with (- x). + replace (glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)) with (- x). unfold is_lub in p. elim p; intros. unfold is_upper_bound in H. @@ -320,28 +326,28 @@ Proof. replace (n + 0)%nat with n; [ reflexivity | ring ]. cut (is_lub (EUn (opp_seq (fun k:nat => Un (n + k)%nat))) - (- minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2))). + (- glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2))). intro. unfold is_lub in p; unfold is_lub in H. elim p; intros; elim H; intros. assert (H4 := H3 x H0). assert - (H5 := H1 (- minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)) H2). + (H5 := H1 (- glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)) H2). rewrite <- - (Ropp_involutive (minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2))) + (Ropp_involutive (glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2))) . apply Ropp_eq_compat; apply Rle_antisym; assumption. - unfold minorant in |- *. - case (min_inf (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)). + unfold glb in |- *. + case (lb_to_glb (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)); simpl. intro; rewrite Ropp_involutive. trivial. - apply min_inf. + apply lb_to_glb. apply min_ss; assumption. - unfold sequence_majorant in |- *. - cut (sigT (fun l:R => is_lub (EUn (fun i:nat => Un (n + i)%nat)) l)). + unfold sequence_ub in |- *. + cut { l:R | is_lub (EUn (fun i:nat => Un (n + i)%nat)) l }. intro X. elim X; intros. - replace (majorant (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)) with x. + replace (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)) with x. unfold is_lub in p. elim p; intros. unfold is_upper_bound in H. @@ -350,24 +356,24 @@ Proof. replace (n + 0)%nat with n; [ reflexivity | ring ]. cut (is_lub (EUn (fun k:nat => Un (n + k)%nat)) - (majorant (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1))). + (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1))). intro. unfold is_lub in p; unfold is_lub in H. elim p; intros; elim H; intros. assert (H4 := H3 x H0). assert - (H5 := H1 (majorant (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)) H2). + (H5 := H1 (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)) H2). apply Rle_antisym; assumption. - unfold majorant in |- *. - case (maj_sup (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)). + unfold lub in |- *. + case (ub_to_lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)). intro; trivial. - apply maj_sup. + apply ub_to_lub. apply maj_ss; assumption. Qed. Lemma min_maj : forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un), - has_ub (sequence_minorant Un pr2). + has_ub (sequence_lb Un pr2). Proof. intros. assert (H := Vn_Un_Wn_order Un pr1 pr2). @@ -390,7 +396,7 @@ Qed. Lemma maj_min : forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un), - has_lb (sequence_majorant Un pr1). + has_lb (sequence_ub Un pr1). Proof. intros. assert (H := Vn_Un_Wn_order Un pr1 pr2). @@ -451,7 +457,7 @@ Qed. (**********) Lemma maj_cv : forall (Un:nat -> R) (pr:Cauchy_crit Un), - sigT (fun l:R => Un_cv (sequence_majorant Un (cauchy_maj Un pr)) l). + { l:R | Un_cv (sequence_ub Un (cauchy_maj Un pr)) l }. Proof. intros. apply decreasing_cv. @@ -464,7 +470,7 @@ Qed. (**********) Lemma min_cv : forall (Un:nat -> R) (pr:Cauchy_crit Un), - sigT (fun l:R => Un_cv (sequence_minorant Un (cauchy_min Un pr)) l). + { l:R | Un_cv (sequence_lb Un (cauchy_min Un pr)) l }. Proof. intros. apply growing_cv. @@ -510,40 +516,40 @@ Qed. (**********) Lemma approx_maj : forall (Un:nat -> R) (pr:has_ub Un) (eps:R), - 0 < eps -> exists k : nat, Rabs (majorant Un pr - Un k) < eps. + 0 < eps -> exists k : nat, Rabs (lub Un pr - Un k) < eps. Proof. intros. - set (P := fun k:nat => Rabs (majorant Un pr - Un k) < eps). + 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 (majorant Un pr - Un k) < eps). + 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 (majorant Un pr - Un n) >= eps). + cut (forall n:nat, Rabs (lub Un pr - Un n) >= eps). intro. - cut (is_lub (EUn Un) (majorant Un pr)). + 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 <= majorant Un pr - Un n). + cut (forall n:nat, eps <= lub Un pr - Un n). intro. - cut (forall n:nat, Un n <= majorant Un pr - eps). + cut (forall n:nat, Un n <= lub Un pr - eps). intro. - cut (forall x:R, EUn Un x -> x <= majorant Un pr - eps). + cut (forall x:R, EUn Un x -> x <= lub Un pr - eps). intro. - assert (H9 := H5 (majorant Un pr - eps) H8). + 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 (majorant Un pr - eps). + apply Rplus_le_reg_l with (lub Un pr - eps). rewrite Rplus_0_r. - replace (majorant Un pr - eps + eps) with (majorant Un pr); + replace (lub Un pr - eps + eps) with (lub Un pr); [ assumption | ring ]. intros. unfold EUn in H8. @@ -553,7 +559,7 @@ Proof. 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 + (majorant Un pr - eps)) with (majorant Un pr - Un n). + replace (eps - Un n + (lub Un pr - eps)) with (lub Un pr - Un n). assumption. ring. ring. @@ -565,11 +571,11 @@ Proof. apply Rle_ge. apply Rplus_le_reg_l with (Un n). rewrite Rplus_0_r; - replace (Un n + (majorant Un pr - Un n)) with (majorant Un pr); + replace (Un n + (lub Un pr - Un n)) with (lub Un pr); [ apply H4 | ring ]. exists n; reflexivity. - unfold majorant in |- *. - case (maj_sup Un pr). + unfold lub in |- *. + case (ub_to_lub Un pr). trivial. intro. assert (H2 := H1 n). @@ -579,40 +585,40 @@ Qed. (**********) Lemma approx_min : forall (Un:nat -> R) (pr:has_lb Un) (eps:R), - 0 < eps -> exists k : nat, Rabs (minorant Un pr - Un k) < eps. + 0 < eps -> exists k : nat, Rabs (glb Un pr - Un k) < eps. Proof. intros. - set (P := fun k:nat => Rabs (minorant Un pr - Un k) < eps). + 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 (minorant Un pr - Un k) < eps). + 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 (minorant Un pr - Un n) >= eps). + cut (forall n:nat, Rabs (glb Un pr - Un n) >= eps). intro. - cut (is_lub (EUn (opp_seq Un)) (- minorant Un pr)). + 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 - minorant Un pr). + cut (forall n:nat, eps <= Un n - glb Un pr). intro. - cut (forall n:nat, opp_seq Un n <= - minorant Un pr - eps). + cut (forall n:nat, opp_seq Un n <= - glb Un pr - eps). intro. - cut (forall x:R, EUn (opp_seq Un) x -> x <= - minorant Un pr - eps). + cut (forall x:R, EUn (opp_seq Un) x -> x <= - glb Un pr - eps). intro. - assert (H9 := H5 (- minorant Un pr - eps) H8). + 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 (- minorant Un pr - eps). + apply Rplus_le_reg_l with (- glb Un pr - eps). rewrite Rplus_0_r. - replace (- minorant Un pr - eps + eps) with (- minorant Un pr); + replace (- glb Un pr - eps + eps) with (- glb Un pr); [ assumption | ring ]. intros. unfold EUn in H8. @@ -623,7 +629,7 @@ Proof. 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 + (- minorant Un pr - eps)) with (Un n - minorant Un pr). + replace (eps + Un n + (- glb Un pr - eps)) with (Un n - glb Un pr). assumption. ring. ring. @@ -631,16 +637,16 @@ Proof. assert (H6 := H2 n). rewrite Rabs_left1 in H6. apply Rge_le. - replace (Un n - minorant Un pr) with (- (minorant Un pr - Un n)); + replace (Un n - glb Un pr) with (- (glb Un pr - Un n)); [ assumption | ring ]. - apply Rplus_le_reg_l with (- minorant Un pr). + apply Rplus_le_reg_l with (- glb Un pr). rewrite Rplus_0_r; - replace (- minorant Un pr + (minorant Un pr - Un n)) with (- Un n). + replace (- glb Un pr + (glb Un pr - Un n)) with (- Un n). apply H4. exists n; reflexivity. ring. - unfold minorant in |- *. - case (min_inf Un pr). + unfold glb in |- *. + case (lb_to_glb Un pr); simpl. intro. rewrite Ropp_involutive. trivial. @@ -711,7 +717,7 @@ Qed. (**********) Lemma CV_Cauchy : - forall Un:nat -> R, sigT (fun l:R => Un_cv Un l) -> Cauchy_crit Un. + forall Un:nat -> R, { l:R | Un_cv Un l } -> Cauchy_crit Un. Proof. intros Un X; elim X; intros. unfold Cauchy_crit in |- *; intros. @@ -734,11 +740,11 @@ Qed. (**********) Lemma maj_by_pos : forall Un:nat -> R, - sigT (fun l:R => Un_cv Un l) -> + { l:R | Un_cv Un l } -> exists l : R, 0 < l /\ (forall n:nat, Rabs (Un n) <= l). Proof. intros Un X; elim X; intros. - cut (sigT (fun l:R => Un_cv (fun k:nat => Rabs (Un k)) l)). + cut { l:R | Un_cv (fun k:nat => Rabs (Un k)) l }. intro X0. assert (H := CV_Cauchy (fun k:nat => Rabs (Un k)) X0). assert (H0 := cauchy_bound (fun k:nat => Rabs (Un k)) H). @@ -760,7 +766,7 @@ Proof. unfold is_upper_bound in H1. apply H1. exists 0%nat; reflexivity. - apply existT with (Rabs x). + exists (Rabs x). apply cv_cvabs; assumption. Qed. @@ -770,7 +776,7 @@ Lemma CV_mult : Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i * Bn i) (l1 * l2). Proof. intros. - cut (sigT (fun l:R => Un_cv An l)). + cut { l:R | Un_cv An l }. intro X. assert (H1 := maj_by_pos An X). elim H1; intros M H2. @@ -881,7 +887,7 @@ Proof. [ assumption | apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; [ prove_sup0 | assumption ] ]. - apply existT with l1; assumption. + exists l1; assumption. Qed. Lemma tech9 : diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index bc17cd43..9680b75e 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: SeqSeries.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: SeqSeries.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -33,15 +33,9 @@ Lemma sum_maj1 : Rabs (l1 - SP fn N x) <= l2 - sum_f_R0 An N. Proof. intros; - cut - (sigT - (fun l:R => - Un_cv (fun n:nat => sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n) l)). + cut { l:R | Un_cv (fun n => sum_f_R0 (fun l => fn (S N + l)%nat x) n) l }. intro X; - cut - (sigT - (fun l:R => - Un_cv (fun n:nat => sum_f_R0 (fun l:nat => An (S N + l)%nat) n) l)). + cut { l:R | Un_cv (fun n => sum_f_R0 (fun l => An (S N + l)%nat) n) l }. intro X0; elim X; intros l1N H2. elim X0; intros l2N H3. cut (l1 - SP fn N x = l1N). @@ -131,7 +125,7 @@ Proof. apply le_lt_n_Sm. apply le_plus_l. apply le_O_n. - apply existT with (l2 - sum_f_R0 An N). + exists (l2 - sum_f_R0 An N). unfold Un_cv in H0; unfold Un_cv in |- *; intros. elim (H0 eps H2); intros N0 H3. unfold R_dist in H3; exists N0; intros. @@ -167,7 +161,7 @@ Proof. apply le_lt_n_Sm. apply le_plus_l. apply le_O_n. - apply existT with (l1 - SP fn N x). + exists (l1 - SP fn N x). unfold Un_cv in H; unfold Un_cv in |- *; intros. elim (H eps H2); intros N0 H3. unfold R_dist in H3; exists N0; intros. @@ -216,8 +210,8 @@ Qed. Lemma Rseries_CV_comp : forall An Bn:nat -> R, (forall n:nat, 0 <= An n <= Bn n) -> - sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 Bn N) l) -> - sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l). + { l:R | Un_cv (fun N:nat => sum_f_R0 Bn N) l } -> + { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l }. Proof. intros An Bn H X; apply cv_cauchy_2. assert (H0 := cv_cauchy_1 _ X). diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index ff0a72e8..13be46da 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -6,12 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Sqrt_reg.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Sqrt_reg.v 10710 2008-03-23 09:24:09Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. -Require Import R_sqrt. Open Local Scope R_scope. +Require Import R_sqrt. +Open Local Scope R_scope. (**********) Lemma sqrt_var_maj : @@ -309,7 +310,7 @@ Qed. Lemma derivable_pt_sqrt : forall x:R, 0 < x -> derivable_pt sqrt x. Proof. unfold derivable_pt in |- *; intros. - apply existT with (/ (2 * sqrt x)). + exists (/ (2 * sqrt x)). apply derivable_pt_lim_sqrt; assumption. Qed. |