diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-23 09:24:09 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-23 09:24:09 +0000 |
| commit | 98936ab93169591d6e1fc8321cb921397cfd67af (patch) | |
| tree | a634eb31f15ddcf3d51fbd2adb1093d4e61ef158 /theories | |
| parent | 881dc3ffdd2b7dd874da57402b8f3f413f8d3d05 (diff) | |
Une passe sur les réels:
- Renommage de Rlt_not_le de Fourier_util en Rlt_not_le_frac_opp pour
éviter la confusion avec le Rlt_not_le de RIneq.
- Quelques variantes de lemmes en plus dans RIneq.
- Déplacement des énoncés de sigT dans sig (y compris la complétude)
et utilisation de la notation { l:R | }.
- Suppression hypothèse inutile de ln_exists1.
- Ajout notation ² pour Rsqr.
Au passage:
- Déplacement de dec_inh_nat_subset_has_unique_least_element
de ChoiceFacts vers Wf_nat.
- Correction de l'espace en trop dans les notations de Specif.v liées à "&".
- MAJ fichier CHANGES
Note: il reste un axiome dans Ranalysis (raison technique: Ltac ne
sait pas manipuler un terme ouvert) et dans Rtrigo.v ("sin PI/2 = 1"
non prouvé).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10710 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
42 files changed, 528 insertions, 517 deletions
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 6e8f154c7..5e7ee4153 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -212,3 +212,48 @@ Lemma well_founded_inv_rel_inv_lt_rel : forall (A:Set) (F:A -> nat -> Prop), well_founded (inv_lt_rel A F). intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial. Qed. + +(** A constructive proof that any non empty decidable subset of + natural numbers has a least element *) + +Set Implicit Arguments. + +Require Import Le. +Require Import Compare_dec. +Require Import Decidable. + +Definition has_unique_least_element (A:Type) (R:A->A->Prop) (P:A->Prop) := + exists! x, P x /\ forall x', P x' -> R x x'. + +Lemma dec_inh_nat_subset_has_unique_least_element : + forall P:nat->Prop, (forall n, P n \/ ~ P n) -> + (exists n, P n) -> has_unique_least_element le P. +Proof. + intros P Pdec (n0,HPn0). + assert + (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'') + \/(forall n', P n' -> n<=n')). + induction n. + right. + intros n' Hn'. + apply le_O_n. + destruct IHn. + left; destruct H as (n', (Hlt', HPn')). + exists n'; split. + apply lt_S; assumption. + assumption. + destruct (Pdec n). + left; exists n; split. + apply lt_n_Sn. + split; assumption. + right. + intros n' Hltn'. + destruct (le_lt_eq_dec n n') as [Hltn|Heqn]. + apply H; assumption. + assumption. + destruct H0. + rewrite Heqn; assumption. + destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0]; + repeat split; + assumption || intros n' (HPn',Hminn'); apply le_antisym; auto. +Qed. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 9495cb707..4f642a73e 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -46,12 +46,12 @@ Arguments Scope sigT [type_scope type_scope]. Arguments Scope sigT2 [type_scope type_scope type_scope]. Notation "{ x | P }" := (sig (fun x => P)) : type_scope. -Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope. +Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope. Notation "{ x : A | P }" := (sig (fun x:A => P)) : type_scope. -Notation "{ x : A | P & Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) : +Notation "{ x : A | P & Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) : type_scope. -Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. -Notation "{ x : A & P & Q }" := (sigT2 (fun x:A => P) (fun x:A => Q)) : +Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. +Notation "{ x : A & P & Q }" := (sigT2 (fun x:A => P) (fun x:A => Q)) : type_scope. Add Printing Let sig. @@ -107,6 +107,13 @@ Section Projections. End Projections. +(** [sigT] of a predicate is equivalent to [sig] *) + +Lemma sig_of_sigT : forall (A:Type) (P:A->Prop), sigT P -> sig P. +Proof. destruct 1 as (x,H); exists x; trivial. Defined. + +Lemma sigT_of_sig : forall (A:Type) (P:A->Prop), sig P -> sigT P. +Proof. destruct 1 as (x,H); exists x; trivial. Defined. (** [sumbool] is a boolean type equipped with the justification of their value *) diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 20fc0ec80..20ffe7b5a 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -546,45 +546,7 @@ Qed. *) Require Import Wf_nat. -Require Import Compare_dec. Require Import Decidable. -Require Import Arith. - -Definition has_unique_least_element (A:Type) (R:A->A->Prop) (P:A->Prop) := - exists! x, P x /\ forall x', P x' -> R x x'. - -Lemma dec_inh_nat_subset_has_unique_least_element : - forall P:nat->Prop, (forall n, P n \/ ~ P n) -> - (exists n, P n) -> has_unique_least_element le P. -Proof. - intros P Pdec (n0,HPn0). - assert - (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'') - \/(forall n', P n' -> n<=n')). - induction n. - right. - intros n' Hn'. - apply le_O_n. - destruct IHn. - left; destruct H as (n', (Hlt', HPn')). - exists n'; split. - apply lt_S; assumption. - assumption. - destruct (Pdec n). - left; exists n; split. - apply lt_n_Sn. - split; assumption. - right. - intros n' Hltn'. - destruct (le_lt_eq_dec n n') as [Hltn|Heqn]. - apply H; assumption. - assumption. - destruct H0. - rewrite Heqn; assumption. - destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0]; - repeat split; - assumption || intros n' (HPn',Hminn'); apply le_antisym; auto. -Qed. Definition FunctionalChoice_on_rel (A B:Type) (R:A->B->Prop) := (forall x:A, exists y : B, R x y) -> diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index 98d352767..4511657a0 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -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 51ed8a4c0..952853a86 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -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/Cos_plus.v b/theories/Reals/Cos_plus.v index 1ef4f1ec4..a0675827b 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -13,7 +13,9 @@ 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 eff4a6c3d..56423f337 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -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 519593381..603010c91 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -9,7 +9,8 @@ (*i $Id$ 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 a79b74d7b..177035c4e 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -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/MVT.v b/theories/Reals/MVT.v index 5d36e3ce8..ca4c38954 100644 --- a/theories/Reals/MVT.v +++ b/theories/Reals/MVT.v @@ -11,7 +11,8 @@ 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 45e45be03..43ddfaf4a 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -12,26 +12,25 @@ 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 73e0f3802..623ae6311 100644 --- a/theories/Reals/PSeries_reg.v +++ b/theories/Reals/PSeries_reg.v @@ -13,7 +13,8 @@ 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 6692fd8c7..40972fbcf 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -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 5d1327528..8b3847340 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -109,6 +109,14 @@ Qed. Hint Resolve Rge_le: real. (**********) +Lemma Rlt_gt : forall r1 r2, r1 < r2 -> r2 > r1. +Proof. trivial. Qed. + +(**********) +Lemma Rgt_lt : forall r1 r2, r1 > r2 -> r2 < r1. +Proof. trivial. Qed. + +(**********) Lemma Rnot_le_lt : forall r1 r2, ~ r1 <= r2 -> r2 < r1. Proof. intros r1 r2; generalize (Rtotal_order r1 r2); unfold Rle in |- *; tauto. @@ -220,7 +228,6 @@ Proof. intuition. Qed. -(**********) Lemma Rle_dec : forall r1 r2, {r1 <= r2} + {~ r1 <= r2}. Proof. intros r1 r2. @@ -228,13 +235,11 @@ 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. -(**********) Lemma Rge_dec : forall r1 r2, {r1 >= r2} + {~ r1 >= r2}. Proof. intros; generalize (Rle_dec r2 r1); intuition. @@ -245,6 +250,16 @@ Proof. intros; generalize (total_order_T r1 r2); intuition. Qed. +Lemma Rle_lt_dec : forall r1 r2, {r1 <= r2} + {r2 < r1}. +Proof. + intros; generalize (total_order_T r1 r2); intuition. +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 Rle_or_lt : forall r1 r2, r1 <= r2 \/ r2 < r1. Proof. intros n m; elim (Rlt_le_dec m n); auto with real. @@ -451,6 +466,8 @@ Qed. (***********) 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. @@ -1541,6 +1558,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. diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index 0dd1a59da..31a9b0b59 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -9,7 +9,8 @@ (*i $Id$ 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 2d8ce1496..627f04102 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -10,7 +10,8 @@ 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 44be747da..371c1af74 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -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 c423c4cb1..de43711c3 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -11,7 +11,8 @@ 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 a22db6502..d9937e225 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -10,7 +10,8 @@ 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 7f8066f57..cb48a26b8 100644 --- a/theories/Reals/Ranalysis3.v +++ b/theories/Reals/Ranalysis3.v @@ -11,7 +11,8 @@ 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 2434c454e..adda4e5a5 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -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 0f5f04fff..eddcb561a 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -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 0d2e016a4..9856b5452 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -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 851fa2336..27d5c49ef 100644 --- a/theories/Reals/Rcomplete.v +++ b/theories/Reals/Rcomplete.v @@ -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/Rderiv.v b/theories/Reals/Rderiv.v index 7e8002b9b..398d840d9 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -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 54bc50e0a..c7226fc6b 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -786,11 +786,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 54e394bd3..9e83150fc 100644 --- a/theories/Reals/Rgeom.v +++ b/theories/Reals/Rgeom.v @@ -12,7 +12,8 @@ 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 29c4688a8..79e4fd2a1 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -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 427800d30..14f1ea6af 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -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 f792b84d1..287fda493 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -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 *) diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v index e10c3ab40..b8c85458c 100644 --- a/theories/Reals/Rlogic.v +++ b/theories/Reals/Rlogic.v @@ -6,10 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** This module proves the decidablity of arithmetical statements from -the axiom that the order of the real numbers is decidable. *) +(** * This module proves 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 who's +(** 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] *) @@ -20,7 +21,10 @@ statement in the arithmetical hierarchy. *) (** Contributed by Cezary Kaliszyk and Russell O'Connor *) Require Import ConstructiveEpsilon. -Require Import Reals. +Require Import Rfunctions. +Require Import PartSum. +Require Import SeqSeries. +Require Import RiemannInt. Require Import Fourier. Section Arithmetical_dec. @@ -130,7 +134,7 @@ assert (A0:=(GP_infinite (1/2) A)). symmetry. split; intro. replace 2 with (/ (1 - (1 / 2))) by field. - unfold Pser, infinit_sum in A0. + unfold Pser, infinite_sum in A0. eapply Rle_cv_lim;[|unfold Un_cv; apply A0 |apply u]. intros n. clear -n H. diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index f254019c7..6dfb2d604 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -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 := diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 438660425..5436b4daa 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -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/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index 14359574f..b228f8985 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -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 f4e1d668e..c36542d2b 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -13,8 +13,8 @@ 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_alt.v b/theories/Reals/Rtrigo_alt.v index d6ab9a4ce..36ed0c1a0 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -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 50ed4b4e5..7f62f538b 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -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 e263ad616..173fe4960 100644 --- a/theories/Reals/Rtrigo_fun.v +++ b/theories/Reals/Rtrigo_fun.v @@ -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 9b5111ff9..dc65dd2e9 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -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 092df1feb..a84a1cc97 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -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 cef07ba5d..e41addadb 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -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 3841ced19..42860180f 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -11,7 +11,8 @@ 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. |