From e1e0f4f7f3c549fd3d5677b67c6b13ed687e6f12 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 3 Jun 2014 17:15:40 +0200 Subject: Make standard library independent of the names generated by induction/elim over a dependent elimination principle for Prop arguments. --- theories/Reals/Alembert.v | 47 ++++++------- theories/Reals/AltSeries.v | 12 ++-- theories/Reals/Exp_prop.v | 26 ++++---- theories/Reals/NewtonInt.v | 2 +- theories/Reals/PartSum.v | 15 ++--- theories/Reals/RList.v | 18 ++--- theories/Reals/Ranalysis1.v | 11 +-- theories/Reals/Ranalysis4.v | 19 ++---- theories/Reals/Ranalysis5.v | 8 +-- theories/Reals/Rbasic_fun.v | 6 +- theories/Reals/Rcomplete.v | 43 ++++++------ theories/Reals/RiemannInt.v | 27 ++++---- theories/Reals/RiemannInt_SF.v | 41 ++++++------ theories/Reals/Rsqrt_def.v | 56 ++++++---------- theories/Reals/Rtopology.v | 6 +- theories/Reals/Rtrigo1.v | 2 +- theories/Reals/Rtrigo_fun.v | 147 ++++++++++++++++++++--------------------- theories/Reals/Rtrigo_reg.v | 2 +- theories/Reals/SeqProp.v | 35 ++++------ theories/Reals/SeqSeries.v | 60 ++++++++--------- 20 files changed, 259 insertions(+), 324 deletions(-) (limited to 'theories/Reals') diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index a92b3584b..c4416e5d8 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -35,10 +35,8 @@ Proof. [ intro | apply Rinv_0_lt_compat; prove_sup0 ]. elim (H0 (/ 2) H1); intros. exists (sum_f_R0 An x + 2 * An (S x)). - unfold is_upper_bound; intros; unfold EUn in H3; elim H3; intros. - rewrite H4; assert (H5 := lt_eq_lt_dec x1 x). - elim H5; intros. - elim a; intro. + unfold is_upper_bound; intros; unfold EUn in H3; destruct H3 as (x1,->). + destruct (lt_eq_lt_dec x1 x) as [[| -> ]|]. replace (sum_f_R0 An x) with (sum_f_R0 An x1 + sum_f_R0 (fun i:nat => An (S x1 + i)%nat) (x - S x1)). pattern (sum_f_R0 An x1) at 1; rewrite <- Rplus_0_r; @@ -47,7 +45,7 @@ Proof. apply tech1; intros; apply H. apply Rmult_lt_0_compat; [ prove_sup0 | apply H ]. symmetry ; apply tech2; assumption. - rewrite b; pattern (sum_f_R0 An x) at 1; rewrite <- Rplus_0_r; + pattern (sum_f_R0 An x) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l. left; apply Rmult_lt_0_compat; [ prove_sup0 | apply H ]. replace (sum_f_R0 An x1) with @@ -86,8 +84,8 @@ Proof. apply (tech6 (fun i:nat => An (S x + i)%nat) (/ 2)). left; apply Rinv_0_lt_compat; prove_sup0. intro; cut (forall n:nat, (n >= x)%nat -> An (S n) < / 2 * An n). - intro; replace (S x + S i)%nat with (S (S x + i)). - apply H6; unfold ge; apply tech8. + intro H4; replace (S x + S i)%nat with (S (S x + i)). + apply H4; unfold ge; apply tech8. apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; do 2 rewrite S_INR; ring. intros; unfold R_dist in H2; apply Rmult_lt_reg_l with (/ An n). apply Rinv_0_lt_compat; apply H. @@ -101,17 +99,17 @@ Proof. unfold Rdiv; reflexivity. left; unfold Rdiv; change (0 < An (S n) * / An n); apply Rmult_lt_0_compat; [ apply H | apply Rinv_0_lt_compat; apply H ]. - red; intro; assert (H8 := H n); rewrite H7 in H8; + intro H5; assert (H8 := H n); rewrite H5 in H8; elim (Rlt_irrefl _ H8). replace (S x + 0)%nat with (S x); [ reflexivity | ring ]. symmetry ; apply tech2; assumption. exists (sum_f_R0 An 0); unfold EUn; exists 0%nat; reflexivity. - intro X; elim X; intros. + intros (x,H1). exists x; apply Un_cv_crit_lub; [ unfold Un_growing; intro; rewrite tech5; pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; apply H - | apply p ]. + | apply H1 ]. Defined. Lemma Alembert_C2 : @@ -127,14 +125,12 @@ Proof. intro; cut (forall n:nat, 0 < Wn n). intro; cut (Un_cv (fun n:nat => Rabs (Vn (S n) / Vn n)) 0). intro; cut (Un_cv (fun n:nat => Rabs (Wn (S n) / Wn n)) 0). - intro; assert (H5 := Alembert_C1 Vn H1 H3). - assert (H6 := Alembert_C1 Wn H2 H4). - elim H5; intros. - elim H6; intros. + intro; pose proof (Alembert_C1 Vn H1 H3) as (x,p). + pose proof (Alembert_C1 Wn H2 H4) as (x0,p0). exists (x - x0); unfold Un_cv; 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. + intro H6; destruct (p (eps / 2) H6) as (x1,H8). clear p. + destruct (p0 (eps / 2) H6) as (x2,H9). clear p0. set (N := max x1 x2). exists N; intros; replace (sum_f_R0 An n) with (sum_f_R0 Vn n - sum_f_R0 Wn n). @@ -146,9 +142,9 @@ Proof. apply Rabs_triang. rewrite Rabs_Ropp; apply Rlt_le_trans with (eps / 2 + eps / 2). apply Rplus_lt_compat. - unfold R_dist in H9; apply H9; unfold ge; apply le_trans with N; + unfold R_dist in H8; apply H8; unfold ge; apply le_trans with N; [ unfold N; apply le_max_l | assumption ]. - unfold R_dist in H10; apply H10; unfold ge; apply le_trans with N; + unfold R_dist in H9; apply H9; unfold ge; apply le_trans with N; [ unfold N; apply le_max_r | assumption ]. right; symmetry ; apply double_var. symmetry ; apply tech11; intro; unfold Vn, Wn; @@ -344,9 +340,8 @@ 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. - exists x0; unfold Bn in p; apply tech12; assumption. + intro; destruct (Alembert_C2 Bn H2 H3) as (x0,H4). + exists x0; unfold Bn in H4; apply tech12; assumption. unfold Un_cv; 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; unfold Rminus; @@ -431,9 +426,7 @@ Proof. unfold is_upper_bound; intros; unfold EUn in H6. elim H6; intros. rewrite H7. - assert (H8 := lt_eq_lt_dec x2 x0). - elim H8; intros. - elim a; intro. + destruct (lt_eq_lt_dec x2 x0) as [[| -> ]|]. replace (sum_f_R0 An x0) with (sum_f_R0 An x2 + sum_f_R0 (fun i:nat => An (S x2 + i)%nat) (x0 - S x2)). pattern (sum_f_R0 An x2) at 1; rewrite <- Rplus_0_r. @@ -446,7 +439,7 @@ Proof. replace (x + (1 - x)) with 1; [ elim H3; intros; assumption | ring ]. apply H. symmetry ; apply tech2; assumption. - rewrite b; pattern (sum_f_R0 An x0) at 1; rewrite <- Rplus_0_r; + pattern (sum_f_R0 An x0) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l. left; apply Rmult_lt_0_compat. apply Rinv_0_lt_compat; apply Rplus_lt_reg_l with x; rewrite Rplus_0_r; @@ -520,12 +513,12 @@ Proof. replace (S x0 + 0)%nat with (S x0); [ reflexivity | ring ]. symmetry ; apply tech2; assumption. exists (sum_f_R0 An 0); unfold EUn; exists 0%nat; reflexivity. - intro X; elim X; intros. + intros (x,H1). exists x; apply Un_cv_crit_lub; [ unfold Un_growing; intro; rewrite tech5; pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; apply H - | apply p ]. + | apply H1]. Qed. Lemma Alembert_C5 : diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index cb3c762cd..73d288aee 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -156,8 +156,7 @@ Proof. intros. assert (H2 := CV_ALT_step0 _ H). assert (H3 := CV_ALT_step4 _ H H0). - assert (X := growing_cv _ H2 H3). - elim X; intros. + destruct (growing_cv _ H2 H3) as (x,p). exists x. unfold Un_cv; unfold R_dist; unfold Un_cv in H1; unfold R_dist in H1; unfold Un_cv in p; unfold R_dist in p. @@ -388,16 +387,13 @@ Proof. apply Rle_ge; apply PI_tg_pos. apply lt_le_trans with N; assumption. elim H1; intros H5 _. - assert (H6 := lt_eq_lt_dec 0 N). - elim H6; intro. - elim a; intro. + destruct (lt_eq_lt_dec 0 N) as [[| <- ]|H6]. assumption. - rewrite <- b in H4. rewrite H4 in H5. simpl in H5. cut (0 < / (2 * eps)); [ intro | apply Rinv_0_lt_compat; assumption ]. - elim (Rlt_irrefl _ (Rlt_trans _ _ _ H7 H5)). - elim (lt_n_O _ b). + elim (Rlt_irrefl _ (Rlt_trans _ _ _ H6 H5)). + elim (lt_n_O _ H6). apply le_IZR. simpl. left; apply Rlt_trans with (/ (2 * eps)). diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index 160f3d480..88c6f9c48 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -86,18 +86,17 @@ Qed. Lemma div2_not_R0 : forall N:nat, (1 < N)%nat -> (0 < div2 N)%nat. Proof. - intros; induction N as [| N HrecN]. - elim (lt_n_O _ H). - cut ((1 < N)%nat \/ N = 1%nat). - intro; elim H0; intro. - assert (H2 := even_odd_dec N). - elim H2; intro. - rewrite <- (even_div2 _ a); apply HrecN; assumption. - rewrite <- (odd_div2 _ b); apply lt_O_Sn. - rewrite H1; simpl; apply lt_O_Sn. - inversion H. - right; reflexivity. - left; apply lt_le_trans with 2%nat; [ apply lt_n_Sn | apply H1 ]. + intros; induction N as [| N HrecN]. + - elim (lt_n_O _ H). + - cut ((1 < N)%nat \/ N = 1%nat). + { intro; elim H0; intro. + + destruct (even_odd_dec N) as [Heq|Heq]. + * rewrite <- (even_div2 _ Heq); apply HrecN; assumption. + * rewrite <- (odd_div2 _ Heq); apply lt_O_Sn. + + rewrite H1; simpl; apply lt_O_Sn. } + inversion H. + right; reflexivity. + left; apply lt_le_trans with 2%nat; [ apply lt_n_Sn | apply H1 ]. Qed. Lemma Reste_E_maj : @@ -857,8 +856,7 @@ Proof. Un_cv (fun n:nat => sum_f_R0 (fun k:nat => Rabs (r ^ k / INR (fact (S k)))) n) l }. - intro X. - elim X; intros. + intros (x,p). exists x; intros. split. apply p. diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index 928422ed8..e0bb8ee2b 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -98,7 +98,7 @@ Lemma NewtonInt_P5 : Newton_integrable (fun x:R => l * f x + g x) a b. Proof. unfold Newton_integrable; intros f g l a b X X0; - elim X; intros; elim X0; intros; + elim X; intros x p; elim X0; intros x0 p0; exists (fun y:R => l * x y + x0 y). elim p; intro. elim p0; intro. diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index 10c3327f2..d559efbce 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -180,12 +180,9 @@ Proof. replace (S (S (pred N))) with (S N). rewrite (HrecN H1); ring. rewrite H2; simpl; reflexivity. - assert (H2 := O_or_S N). - elim H2; intros. - elim a; intros. - rewrite <- p. + destruct (O_or_S N) as [(m,<-)|<-]. simpl; reflexivity. - rewrite <- b in H1; elim (lt_irrefl _ H1). + elim (lt_irrefl _ H1). rewrite H1; simpl; reflexivity. inversion H. right; reflexivity. @@ -395,9 +392,7 @@ Proof. (sum_f_R0 (fun i:nat => Rabs (An i)) m)). assumption. apply H1; assumption. - assert (H4 := lt_eq_lt_dec n m). - elim H4; intro. - elim a; intro. + destruct (lt_eq_lt_dec n m) as [[ | -> ]|]. rewrite (tech2 An n m); [ idtac | assumption ]. rewrite (tech2 (fun i:nat => Rabs (An i)) n m); [ idtac | assumption ]. unfold R_dist. @@ -418,7 +413,6 @@ Proof. apply Rle_ge. apply cond_pos_sum. intro; apply Rabs_pos. - rewrite b. unfold R_dist. unfold Rminus; do 2 rewrite Rplus_opp_r. rewrite Rabs_R0; right; reflexivity. @@ -451,8 +445,7 @@ Lemma cv_cauchy_1 : { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l } -> Cauchy_crit_series An. Proof. - intros An X. - elim X; intros. + intros An (x,p). unfold Un_cv in p. unfold Cauchy_crit_series; unfold Cauchy_crit. intros. diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v index 6d42434a4..e75a4c17d 100644 --- a/theories/Reals/RList.v +++ b/theories/Reals/RList.v @@ -181,13 +181,13 @@ Proof. elim Hrecl; intros; assert (H3 := H1 H0); elim H3; intros; elim H4; intros; exists (S x0); split; [ simpl; apply lt_n_S; assumption | simpl; assumption ]. - elim H; intros; elim H0; intros; elim (zerop x0); intro. - rewrite a in H2; simpl in H2; left; assumption. - right; elim Hrecl; intros; apply H4; assert (H5 : S (pred x0) = x0). + elim H; intros; elim H0; intros; destruct (zerop x0) as [->|]. + simpl in H2; left; assumption. + right; elim Hrecl; intros H4 H5; apply H5; assert (H6 : S (pred x0) = x0). symmetry ; apply S_pred with 0%nat; assumption. exists (pred x0); split; - [ simpl in H1; apply lt_S_n; rewrite H5; assumption - | rewrite <- H5 in H2; simpl in H2; assumption ]. + [ simpl in H1; apply lt_S_n; rewrite H6; assumption + | rewrite <- H6 in H2; simpl in H2; assumption ]. Qed. Lemma Rlist_P1 : @@ -208,11 +208,11 @@ Proof. assert (H3 := Hrecl H2); elim H1; intros; elim H3; intros; exists (cons x x0); intros; elim H5; clear H5; intros; split. simpl; rewrite H5; reflexivity. - intros; elim (zerop i); intro. - rewrite a; simpl; assumption. - assert (H8 : i = S (pred i)). + intros; destruct (zerop i) as [->|]. + simpl; assumption. + assert (H9 : i = S (pred i)). apply S_pred with 0%nat; assumption. - rewrite H8; simpl; apply H6; simpl in H7; apply lt_S_n; rewrite <- H8; + rewrite H9; simpl; apply H6; simpl in H7; apply lt_S_n; rewrite <- H9; assumption. Qed. diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 0409c99e4..6afc20f5a 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -1066,15 +1066,8 @@ Lemma pr_nu : forall f (x:R) (pr1 pr2:derivable_pt f x), derive_pt f x pr1 = derive_pt f x pr2. Proof. - intros. - unfold derivable_pt in pr1. - unfold derivable_pt in pr2. - elim pr1; intros. - elim pr2; intros. - unfold derivable_pt_abs in p. - unfold derivable_pt_abs in p0. - simpl. - apply (uniqueness_limite f x x0 x1 p p0). + intros f x (x0,H0) (x1,H1). + apply (uniqueness_limite f x x0 x1 H0 H1). Qed. diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index 663f62f7a..dd8e0dd52 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -26,7 +26,7 @@ Proof. apply derivable_pt_const. assumption. assumption. - unfold div_fct, inv_fct, fct_cte; intro X0; elim X0; intros; + unfold div_fct, inv_fct, fct_cte; intros (x0,p); unfold derivable_pt; exists x0; unfold derivable_pt_abs; unfold derivable_pt_lim; unfold derivable_pt_abs in p; unfold derivable_pt_lim in p; @@ -41,11 +41,7 @@ Lemma pr_nu_var : forall (f g:R -> R) (x:R) (pr1:derivable_pt f x) (pr2:derivable_pt g x), f = g -> derive_pt f x pr1 = derive_pt g x pr2. Proof. - unfold derivable_pt, derive_pt; intros. - elim pr1; intros. - elim pr2; intros. - simpl. - rewrite H in p. + unfold derivable_pt, derive_pt; intros f g x (x0,p0) (x1,p1) ->. apply uniqueness_limite with g x; assumption. Qed. @@ -54,14 +50,11 @@ Lemma pr_nu_var2 : forall (f g:R -> R) (x:R) (pr1:derivable_pt f x) (pr2:derivable_pt g x), (forall h:R, f h = g h) -> derive_pt f x pr1 = derive_pt g x pr2. Proof. - unfold derivable_pt, derive_pt; intros. - elim pr1; intros. - elim pr2; intros. - simpl. - assert (H0 := uniqueness_step2 _ _ _ p). - assert (H1 := uniqueness_step2 _ _ _ p0). + unfold derivable_pt, derive_pt; intros f g x (x0,p0) (x1,p1) H. + assert (H0 := uniqueness_step2 _ _ _ p0). + assert (H1 := uniqueness_step2 _ _ _ p1). cut (limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) x1 0). - intro; assert (H3 := uniqueness_step1 _ _ _ _ H0 H2). + intro H2; assert (H3 := uniqueness_step1 _ _ _ _ H0 H2). assumption. unfold limit1_in; unfold limit_in; unfold dist; simpl; unfold R_dist; unfold limit1_in in H1; diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index 6f8dcdc71..f787aa630 100644 --- a/theories/Reals/Ranalysis5.v +++ b/theories/Reals/Ranalysis5.v @@ -165,8 +165,8 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption. unfold derivable_pt in Prf. unfold derivable_pt in Prg. - elim Prf; intros. - elim Prg; intros. + elim Prf; intros x0 p. + elim Prg; intros x1 p0. assert (Temp := p); rewrite H in Temp. unfold derivable_pt_abs in p. unfold derivable_pt_abs in p0. @@ -295,8 +295,8 @@ intros. (* f x y f_cont_interv x_lt_y fx_neg fy_pos.*) generalize (dicho_lb_cv x y (fun z:R => cond_positivity (f z)) H3). generalize (dicho_up_cv x y (fun z:R => cond_positivity (f z)) H3). intros X X0. - elim X; intros. - elim X0; intros. + elim X; intros x0 p. + elim X0; intros x1 p0. assert (H4 := cv_dicho _ _ _ _ _ H3 p0 p). rewrite H4 in p0. exists x0. diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index daf895fd2..c189b0333 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -276,9 +276,9 @@ Qed. (*********) Lemma Rcase_abs : forall r, {r < 0} + {r >= 0}. Proof. - intro; generalize (Rle_dec 0 r); intro X; elim X; intro; clear X. - right; apply (Rle_ge 0 r a). - left; fold (0 > r); apply (Rnot_le_lt 0 r b). + intro; generalize (Rle_dec 0 r); intro X; elim X; intro H; clear X. + right; apply (Rle_ge 0 r H). + left; fold (0 > r); apply (Rnot_le_lt 0 r H). Qed. (*********) diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v index 8e0e0692c..b9150c181 100644 --- a/theories/Reals/Rcomplete.v +++ b/theories/Reals/Rcomplete.v @@ -27,21 +27,19 @@ Proof. intros. set (Vn := sequence_minorant Un (cauchy_min Un H)). set (Wn := sequence_majorant Un (cauchy_maj Un H)). - assert (H0 := maj_cv Un H). - fold Wn in H0. - assert (H1 := min_cv Un H). - fold Vn in H1. - elim H0; intros. - elim H1; intros. + pose proof (maj_cv Un H) as (x,p). + fold Wn in p. + pose proof (min_cv Un H) as (x0,p0). + fold Vn in p0. cut (x = x0). - intros. + intros H2. exists x. rewrite <- H2 in p0. unfold Un_cv. intros. unfold Un_cv in p; unfold Un_cv in p0. cut (0 < eps / 3). - intro. + intro H4. elim (p (eps / 3) H4); intros. elim (p0 (eps / 3) H4); intros. exists (max x1 x2). @@ -83,20 +81,20 @@ Proof. [ apply Rabs_triang | ring ]. apply Rlt_le_trans with (eps / 3 + eps / 3 + eps / 3). repeat apply Rplus_lt_compat. - unfold R_dist in H5. - apply H5. + unfold R_dist in H1. + apply H1. unfold ge; apply le_trans with (max x1 x2). apply le_max_l. assumption. rewrite <- Rabs_Ropp. replace (- (x - Vn n)) with (Vn n - x); [ idtac | ring ]. - unfold R_dist in H6. - apply H6. + unfold R_dist in H3. + apply H3. unfold ge; apply le_trans with (max x1 x2). apply le_max_r. assumption. - unfold R_dist in H6. - apply H6. + unfold R_dist in H3. + apply H3. unfold ge; apply le_trans with (max x1 x2). apply le_max_r. assumption. @@ -112,11 +110,11 @@ Proof. intro. unfold Un_cv in p; unfold Un_cv in p0. unfold R_dist in p; unfold R_dist in p0. - elim (p (eps / 5) H3); intros N1 H4. - elim (p0 (eps / 5) H3); intros N2 H5. + elim (p (eps / 5) H1); intros N1 H4. + elim (p0 (eps / 5) H1); intros N2 H5. unfold Cauchy_crit in H. unfold R_dist in H. - elim (H (eps / 5) H3); intros N3 H6. + elim (H (eps / 5) H1); intros N3 H6. set (N := max (max N1 N2) N3). apply Rle_lt_trans with (Rabs (x - Wn N) + Rabs (Wn N - x0)). replace (x - x0) with (x - Wn N + (Wn N - x0)); [ apply Rabs_triang | ring ]. @@ -146,12 +144,11 @@ Proof. cut (Vn N = minorant (fun k:nat => Un (N + k)%nat) (min_ss Un N (cauchy_min Un H))). - intros. - rewrite <- H9; rewrite <- H10. - rewrite <- H9 in H8. - rewrite <- H10 in H7. - elim (H7 (eps / 5) H3); intros k2 H11. - elim (H8 (eps / 5) H3); intros k1 H12. + intros H9 H10. + rewrite <- H9 in H8 |- *. + rewrite <- H10 in H7 |- *. + elim (H7 (eps / 5) H1); intros k2 H11. + elim (H8 (eps / 5) H1); intros k1 H12. apply Rle_lt_trans with (Rabs (Wn N - Un (N + k2)%nat) + Rabs (Un (N + k2)%nat - Vn N)). replace (Wn N - Vn N) with diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 1445e7dbe..0dc3329ee 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -49,8 +49,8 @@ Lemma RiemannInt_P1 : forall (f:R -> R) (a b:R), Riemann_integrable f a b -> Riemann_integrable f b a. Proof. - unfold Riemann_integrable; intros; elim (X eps); clear X; intros; - elim p; clear p; intros; exists (mkStepFun (StepFun_P6 (pre x))); + unfold Riemann_integrable; intros; elim (X eps); clear X; intros. + elim p; clear p; intros x0 p; 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; @@ -171,7 +171,7 @@ Proof. rewrite Rabs_Ropp; apply H4. rewrite Rabs_Ropp in H4; apply H4. apply H4. - assert (H3 := RiemannInt_P2 _ _ _ _ H H1 H2); elim H3; intros; + assert (H3 := RiemannInt_P2 _ _ _ _ H H1 H2); elim H3; intros x p; exists (- x); unfold Un_cv; unfold Un_cv in p; intros; elim (p _ H4); intros; exists x0; intros; generalize (H5 _ H6); unfold R_dist, RiemannInt_SF; @@ -423,7 +423,7 @@ Proof. exists 0%nat; unfold I; rewrite Rmult_0_l; rewrite Rplus_0_r; assumption. cut (Nbound I). - intro; assert (H2 := Nzorn H0 H1); elim H2; intros; exists x; elim p; intros; + intro; assert (H2 := Nzorn H0 H1); elim H2; intros x p; exists x; elim p; intros; split. apply H3. destruct (total_order_T (a + INR (S x) * del) b) as [[Hlt|Heq]|Hgt]. @@ -497,7 +497,7 @@ Proof. | apply Rmin_r ] | 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). + assert (H3 := completeness E H1 H2); elim H3; intros x p; cut (0 < x <= b - a). 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; @@ -535,7 +535,7 @@ Lemma Heine_cor2 : a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps }. Proof. intro f; intros; destruct (total_order_T a b) as [[Hlt|Heq]|Hgt]. - assert (H0 := Heine_cor1 Hlt H eps); elim H0; intros; exists x; + assert (H0 := Heine_cor1 Hlt H eps); elim H0; intros x p; exists x; elim p; intros; apply H2; assumption. exists (mkposreal _ Rlt_0_1); intros; assert (H3 : x = y); [ elim H0; elim H1; intros; rewrite Heq in H3, H5; @@ -993,11 +993,10 @@ Qed. Lemma Req_EM_T : forall r1 r2:R, {r1 = r2} + {r1 <> r2}. Proof. - intros; elim (total_order_T r1 r2); intros; - [ elim a; intro; - [ right; red; intro; rewrite H in a0; elim (Rlt_irrefl r2 a0) - | left; assumption ] - | right; red; intro; rewrite H in b; elim (Rlt_irrefl r2 b) ]. + intros; destruct (total_order_T r1 r2) as [[H|]|H]. + - right; red; intros ->; elim (Rlt_irrefl r2 H). + - left; assumption. + - right; red; intros ->; elim (Rlt_irrefl r2 H). Qed. (* L1([a,b]) is a vectorial space *) @@ -1008,7 +1007,7 @@ Lemma RiemannInt_P10 : Riemann_integrable (fun x:R => f x + l * g x) a b. Proof. unfold Riemann_integrable; intros f g; intros; destruct (Req_EM_T l 0) as [Heq|Hneq]. - elim (X eps); intros; split with x; elim p; intros; split with x0; elim p0; + elim (X eps); intros x p; split with x; elim p; intros x0 p0; split with x0; elim p0; intros; split; try assumption; rewrite Heq; intros; rewrite Rmult_0_l; rewrite Rplus_0_r; apply H; assumption. assert (H : 0 < eps / 2). @@ -1019,9 +1018,9 @@ Proof. [ apply (cond_pos eps) | apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; [ prove_sup0 | apply Rabs_pos_lt; assumption ] ]. - elim (X (mkposreal _ H)); intros; elim (X0 (mkposreal _ H0)); intros; + elim (X (mkposreal _ H)); intros x p; elim (X0 (mkposreal _ H0)); intros x0 p0; split with (mkStepFun (StepFun_P28 l x x0)); elim p0; - elim p; intros; split with (mkStepFun (StepFun_P28 (Rabs l) x1 x2)); + elim p; intros x1 p1 x2 p2. split with (mkStepFun (StepFun_P28 (Rabs l) x1 x2)); elim p1; elim p2; clear p1 p2 p0 p X X0; intros; split. intros; simpl; apply Rle_trans with (Rabs (f t - x t) + Rabs (l * (g t - x0 t))). diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 9466ed8e6..d2c04f556 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -40,26 +40,25 @@ Proof. assert (H2 : exists x : R, E x). elim H; intros; exists (INR x); unfold E; exists x; split; [ assumption | reflexivity ]. - assert (H3 := completeness E H1 H2); elim H3; intros; unfold is_lub in p; - elim p; clear p; intros; unfold is_upper_bound in H4, H5; + destruct (completeness E H1 H2) as (x,(H4,H5)); unfold is_upper_bound in H4, H5; assert (H6 : 0 <= x). - elim H2; intros; unfold E in H6; elim H6; intros; elim H7; intros; + destruct H2 as (x0,H6). remember H6 as H7. destruct H7 as (x1,(H8,H9)). apply Rle_trans with x0; [ rewrite <- H9; change (INR 0 <= INR x1); apply le_INR; apply le_O_n | apply H4; assumption ]. assert (H7 := archimed x); elim H7; clear H7; intros; assert (H9 : x <= IZR (up x) - 1). - apply H5; intros; assert (H10 := H4 _ H9); unfold E in H9; elim H9; intros; - elim H11; intros; rewrite <- H13; apply Rplus_le_reg_l with 1; + apply H5; intros x0 H9. assert (H10 := H4 _ H9); unfold E in H9; elim H9; intros x1 (H12,<-). + apply Rplus_le_reg_l with 1; replace (1 + (IZR (up x) - 1)) with (IZR (up x)); [ idtac | ring ]; replace (1 + INR x1) with (INR (S x1)); [ idtac | rewrite S_INR; ring ]. assert (H14 : (0 <= up x)%Z). apply le_IZR; apply Rle_trans with x; [ apply H6 | left; assumption ]. - assert (H15 := IZN _ H14); elim H15; clear H15; intros; rewrite H15; - rewrite <- INR_IZR_INZ; apply le_INR; apply lt_le_S; - apply INR_lt; rewrite H13; apply Rle_lt_trans with x; + destruct (IZN _ H14) as (x2,H15). + rewrite H15, <- INR_IZR_INZ; apply le_INR; apply lt_le_S. + apply INR_lt; apply Rle_lt_trans with x; [ assumption | rewrite INR_IZR_INZ; rewrite <- H15; assumption ]. assert (H10 : x = IZR (up x) - 1). apply Rle_antisym; @@ -84,18 +83,18 @@ Proof. cut (x = INR (pred x0)). intro; rewrite H19; apply le_INR; apply lt_le_S; apply INR_lt; rewrite H18; rewrite <- H19; assumption. - rewrite H10; rewrite p; rewrite <- INR_IZR_INZ; replace 1 with (INR 1); + rewrite H10; rewrite H8; rewrite <- INR_IZR_INZ; replace 1 with (INR 1); [ idtac | reflexivity ]; rewrite <- minus_INR. replace (x0 - 1)%nat with (pred x0); [ reflexivity | case x0; [ reflexivity | intro; simpl; apply minus_n_O ] ]. - induction x0 as [| x0 Hrecx0]; - [ rewrite p in H7; rewrite <- INR_IZR_INZ in H7; simpl in H7; - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H7)) - | apply le_n_S; apply le_O_n ]. - rewrite H15 in H13; elim H12; assumption. + induction x0 as [|x0 Hrecx0]. + rewrite H8 in H3. rewrite <- INR_IZR_INZ in H3; simpl in H3. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H3)). + apply le_n_S; apply le_O_n. + rewrite H15 in H13; elim H12; assumption. split with (pred x0); unfold E in H13; elim H13; intros; elim H12; intros; - rewrite H10 in H15; rewrite p in H15; rewrite <- INR_IZR_INZ in H15; + rewrite H10 in H15; rewrite H8 in H15; rewrite <- INR_IZR_INZ in H15; assert (H16 : INR x0 = INR x1 + 1). rewrite H15; ring. rewrite <- S_INR in H16; assert (H17 := INR_eq _ _ H16); rewrite H17; @@ -1202,13 +1201,13 @@ Proof. [ apply lt_n_S; assumption | symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H22 in H21; elim (lt_n_O _ H21) ]. - elim (Rle_dec (pos_Rl lf (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro. + elim (Rle_dec (pos_Rl lf (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro a0. assert (H23 : (S x0 <= x0)%nat). apply H20; unfold I; split; assumption. elim (le_Sn_n _ H23). assert (H23 : pos_Rl (cons_ORlist lf lg) i < pos_Rl lf (S x0)). auto with real. - clear b0; apply RList_P17; try assumption. + clear a0; apply RList_P17; try assumption. apply RList_P2; assumption. elim (RList_P9 lf lg (pos_Rl lf (S x0))); intros; apply H25; left; elim (RList_P3 lf (pos_Rl lf (S x0))); intros; apply H27; @@ -1450,12 +1449,12 @@ Proof. apply lt_n_S; assumption. symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red; intro; rewrite <- H22 in H21; elim (lt_n_O _ H21). - elim (Rle_dec (pos_Rl lg (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro. + elim (Rle_dec (pos_Rl lg (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro a0. assert (H23 : (S x0 <= x0)%nat); [ apply H20; unfold I; split; assumption | elim (le_Sn_n _ H23) ]. assert (H23 : pos_Rl (cons_ORlist lf lg) i < pos_Rl lg (S x0)). auto with real. - clear b0; apply RList_P17; try assumption; + clear a0; apply RList_P17; try assumption; [ apply RList_P2; assumption | elim (RList_P9 lf lg (pos_Rl lg (S x0))); intros; apply H25; right; elim (RList_P3 lg (pos_Rl lg (S x0))); intros; @@ -2423,7 +2422,7 @@ Proof. discriminate. clear Hreclf1; assert (H1 : {c <= r1} + {r1 < c}). case (Rle_dec c r1); intro; [ left; assumption | right; auto with real ]. - elim H1; intro. + elim H1; intro a0. split with (cons r (cons c nil)); split with (cons r3 nil); unfold adapted_couple in H; decompose [and] H; clear H; assert (H6 : r = a). @@ -2534,7 +2533,7 @@ Proof. discriminate. clear Hreclf1; assert (H1 : {c <= r1} + {r1 < c}). case (Rle_dec c r1); intro; [ left; assumption | right; auto with real ]. - elim H1; intro. + elim H1; intro a0. split with (cons c (cons r1 r2)); split with (cons r3 lf1); unfold adapted_couple in H; decompose [and] H; clear H; unfold adapted_couple; repeat split. diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index f9ad64b86..2e3d7f167 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -423,18 +423,15 @@ Lemma dicho_lb_car : P x = false -> P (dicho_lb x y P n) = false. Proof. intros. - induction n as [| n Hrecn]. - simpl. - assumption. - simpl. - assert - (X := - sumbool_of_bool (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2))). - elim X; intro. - rewrite a. - unfold dicho_lb in Hrecn; assumption. - rewrite b. - assumption. + induction n as [| n Hrecn]. + - assumption. + - simpl. + destruct + (sumbool_of_bool (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2))) as [Heq|Heq]. + + rewrite Heq. + unfold dicho_lb in Hrecn; assumption. + + rewrite Heq. + assumption. Qed. Lemma dicho_up_car : @@ -442,18 +439,15 @@ Lemma dicho_up_car : P y = true -> P (dicho_up x y P n) = true. Proof. intros. - induction n as [| n Hrecn]. - simpl. - assumption. - simpl. - assert - (X := - sumbool_of_bool (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2))). - elim X; intro. - rewrite a. - unfold dicho_lb in Hrecn; assumption. - rewrite b. - assumption. + induction n as [| n Hrecn]. + - assumption. + - simpl. + destruct + (sumbool_of_bool (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2))) as [Heq|Heq]. + + rewrite Heq. + unfold dicho_lb in Hrecn; assumption. + + rewrite Heq. + assumption. Qed. (** Intermediate Value Theorem *) @@ -463,13 +457,9 @@ Lemma IVT : x < y -> f x < 0 -> 0 < f y -> { z:R | x <= z <= y /\ f z = 0 }. Proof. intros. - cut (x <= y). - intro. - generalize (dicho_lb_cv x y (fun z:R => cond_positivity (f z)) H3). - generalize (dicho_up_cv x y (fun z:R => cond_positivity (f z)) H3). - intros X X0. - elim X; intros. - elim X0; intros. + assert (x <= y) by (left; assumption). + destruct (dicho_lb_cv x y (fun z:R => cond_positivity (f z)) H3) as (x1,p0). + destruct (dicho_up_cv x y (fun z:R => cond_positivity (f z)) H3) as (x0,p). assert (H4 := cv_dicho _ _ _ _ _ H3 p0 p). rewrite H4 in p0. exists x0. @@ -486,7 +476,6 @@ Proof. apply dicho_up_decreasing; assumption. assumption. right; reflexivity. - 2: left; assumption. set (Vn := fun n:nat => dicho_lb x y (fun z:R => cond_positivity (f z)) n). set (Wn := fun n:nat => dicho_up x y (fun z:R => cond_positivity (f z)) n). cut ((forall n:nat, f (Vn n) <= 0) -> f x0 <= 0). @@ -612,9 +601,8 @@ Proof. cut ((- f)%F x < 0). cut (0 < (- f)%F y). intros. - elim (H3 H5 H4); intros. + destruct (H3 H5 H4) as (x0,[]). exists x0. - elim p; intros. split. assumption. unfold opp_fct in H7. diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index 991a52409..ac15cf21e 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -1655,9 +1655,9 @@ Proof. apply H7; split. unfold D_x, no_cond; split; [ trivial | assumption ]. apply Rlt_le_trans with (Rmin x0 (M - m)); [ apply H8 | apply Rmin_l ]. - assert (H8 := completeness _ H6 H7); elim H8; clear H8; intros; + destruct (completeness _ H6 H7) as (x1,p). cut (0 < x1 <= M - m). - intro; elim H8; clear H8; intros; exists (mkposreal _ H8); split. + intros (H8,H9); exists (mkposreal _ H8); split. intros; cut (exists alp : R, Rabs (z - x) < alp <= x1 /\ E alp). intros; elim H11; intros; elim H12; clear H12; intros; unfold E in H13; elim H13; intros; apply H15. @@ -1811,7 +1811,7 @@ Proof. apply H14; split; [ unfold D_x, no_cond; split; [ trivial | assumption ] | apply Rlt_le_trans with (Rmin x0 (M - m)); [ apply H15 | apply Rmin_l ] ]. - assert (H13 := completeness _ H11 H12); elim H13; clear H13; intros; + destruct (completeness _ H11 H12) as (x0,p). cut (0 < x0 <= M - m). intro; elim H13; clear H13; intros; exists x0; split. assumption. diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v index e42610424..1f488aa9e 100644 --- a/theories/Reals/Rtrigo1.v +++ b/theories/Reals/Rtrigo1.v @@ -39,7 +39,7 @@ Proof. (fun n:nat => sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k)) * r ^ (2 * k))) n) l }. - intro X; elim X; intros. + intros (x,p). exists x. split. apply p. diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v index b131b5107..cbba91f06 100644 --- a/theories/Reals/Rtrigo_fun.v +++ b/theories/Reals/Rtrigo_fun.v @@ -20,80 +20,79 @@ Local Open Scope R_scope. Lemma Alembert_exp : Un_cv (fun n:nat => Rabs (/ INR (fact (S n)) * / / INR (fact n))) 0. Proof. - unfold Un_cv; intros; elim (Rgt_dec eps 1); intro. - split with 0%nat; intros; rewrite (simpl_fact n); unfold R_dist; - rewrite (Rminus_0_r (Rabs (/ INR (S n)))); - rewrite (Rabs_Rabsolu (/ INR (S n))); cut (/ INR (S n) > 0). - intro; rewrite (Rabs_pos_eq (/ INR (S n))). - cut (/ eps - 1 < 0). - intro; generalize (Rlt_le_trans (/ eps - 1) 0 (INR n) H2 (pos_INR n)); - clear H2; intro; unfold Rminus in H2; - generalize (Rplus_lt_compat_l 1 (/ eps + -1) (INR n) H2); - replace (1 + (/ eps + -1)) with (/ eps); [ clear H2; intro | ring ]. - rewrite (Rplus_comm 1 (INR n)) in H2; rewrite <- (S_INR n) in H2; - generalize (Rmult_gt_0_compat (/ INR (S n)) eps H1 H); - intro; unfold Rgt in H3; - generalize (Rmult_lt_compat_l (/ INR (S n) * eps) (/ eps) (INR (S n)) H3 H2); - intro; rewrite (Rmult_assoc (/ INR (S n)) eps (/ eps)) in H4; - rewrite (Rinv_r eps (Rlt_dichotomy_converse eps 0 (or_intror (eps < 0) H))) - in H4; rewrite (let (H1, H2) := Rmult_ne (/ INR (S n)) in H1) in H4; - rewrite (Rmult_comm (/ INR (S n))) in H4; - rewrite (Rmult_assoc eps (/ INR (S n)) (INR (S n))) in H4; - rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) (not_eq_sym (O_S n)))) in H4; - rewrite (let (H1, H2) := Rmult_ne eps in H1) in H4; - assumption. - apply Rlt_minus; unfold Rgt in a; rewrite <- Rinv_1; - apply (Rinv_lt_contravar 1 eps); auto; - rewrite (let (H1, H2) := Rmult_ne eps in H2); unfold Rgt in H; - assumption. - unfold Rgt in H1; apply Rlt_le; assumption. - unfold Rgt; apply Rinv_0_lt_compat; apply lt_INR_0; apply lt_O_Sn. -(**) - cut (0 <= up (/ eps - 1))%Z. - intro; elim (IZN (up (/ eps - 1)) H0); intros; split with x; intros; - rewrite (simpl_fact n); unfold R_dist; + unfold Un_cv; intros; destruct (Rgt_dec eps 1) as [Hgt|Hnotgt]. + - split with 0%nat; intros; rewrite (simpl_fact n); unfold R_dist; rewrite (Rminus_0_r (Rabs (/ INR (S n)))); rewrite (Rabs_Rabsolu (/ INR (S n))); cut (/ INR (S n) > 0). - intro; rewrite (Rabs_pos_eq (/ INR (S n))). - cut (/ eps - 1 < INR x). - intro ; - generalize - (Rlt_le_trans (/ eps - 1) (INR x) (INR n) H4 - (le_INR x n H2)); - clear H4; intro; unfold Rminus in H4; - generalize (Rplus_lt_compat_l 1 (/ eps + -1) (INR n) H4); - replace (1 + (/ eps + -1)) with (/ eps); [ clear H4; intro | ring ]. - rewrite (Rplus_comm 1 (INR n)) in H4; rewrite <- (S_INR n) in H4; - generalize (Rmult_gt_0_compat (/ INR (S n)) eps H3 H); - intro; unfold Rgt in H5; - generalize (Rmult_lt_compat_l (/ INR (S n) * eps) (/ eps) (INR (S n)) H5 H4); - intro; rewrite (Rmult_assoc (/ INR (S n)) eps (/ eps)) in H6; - rewrite (Rinv_r eps (Rlt_dichotomy_converse eps 0 (or_intror (eps < 0) H))) - in H6; rewrite (let (H1, H2) := Rmult_ne (/ INR (S n)) in H1) in H6; - rewrite (Rmult_comm (/ INR (S n))) in H6; - rewrite (Rmult_assoc eps (/ INR (S n)) (INR (S n))) in H6; - rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) (not_eq_sym (O_S n)))) in H6; - rewrite (let (H1, H2) := Rmult_ne eps in H1) in H6; - assumption. - cut (IZR (up (/ eps - 1)) = IZR (Z.of_nat x)); - [ intro | rewrite H1; trivial ]. - elim (archimed (/ eps - 1)); intros; clear H6; unfold Rgt in H5; - rewrite H4 in H5; rewrite INR_IZR_INZ; assumption. - unfold Rgt in H1; apply Rlt_le; assumption. - unfold Rgt; apply Rinv_0_lt_compat; apply lt_INR_0; apply lt_O_Sn. - apply (le_O_IZR (up (/ eps - 1))); - apply (Rle_trans 0 (/ eps - 1) (IZR (up (/ eps - 1)))). - generalize (Rnot_gt_le eps 1 b); clear b; unfold Rle; intro; elim H0; - clear H0; intro. - left; unfold Rgt in H; - generalize (Rmult_lt_compat_l (/ eps) eps 1 (Rinv_0_lt_compat eps H) H0); - rewrite - (Rinv_l eps - (not_eq_sym (Rlt_dichotomy_converse 0 eps (or_introl (0 > eps) H)))) - ; rewrite (let (H1, H2) := Rmult_ne (/ eps) in H1); - intro; fold (/ eps - 1 > 0); apply Rgt_minus; - unfold Rgt; assumption. - right; rewrite H0; rewrite Rinv_1; symmetry; apply Rminus_diag_eq; auto. - elim (archimed (/ eps - 1)); intros; clear H1; unfold Rgt in H0; apply Rlt_le; - assumption. + intro; rewrite (Rabs_pos_eq (/ INR (S n))). + cut (/ eps - 1 < 0). + intro H2; generalize (Rlt_le_trans (/ eps - 1) 0 (INR n) H2 (pos_INR n)); + clear H2; intro; unfold Rminus in H2; + generalize (Rplus_lt_compat_l 1 (/ eps + -1) (INR n) H2); + replace (1 + (/ eps + -1)) with (/ eps); [ clear H2; intro | ring ]. + rewrite (Rplus_comm 1 (INR n)) in H2; rewrite <- (S_INR n) in H2; + generalize (Rmult_gt_0_compat (/ INR (S n)) eps H1 H); + intro; unfold Rgt in H3; + generalize (Rmult_lt_compat_l (/ INR (S n) * eps) (/ eps) (INR (S n)) H3 H2); + intro; rewrite (Rmult_assoc (/ INR (S n)) eps (/ eps)) in H4; + rewrite (Rinv_r eps (Rlt_dichotomy_converse eps 0 (or_intror (eps < 0) H))) + in H4; rewrite (let (H1, H2) := Rmult_ne (/ INR (S n)) in H1) in H4; + rewrite (Rmult_comm (/ INR (S n))) in H4; + rewrite (Rmult_assoc eps (/ INR (S n)) (INR (S n))) in H4; + rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) (not_eq_sym (O_S n)))) in H4; + rewrite (let (H1, H2) := Rmult_ne eps in H1) in H4; + assumption. + apply Rlt_minus; unfold Rgt in Hgt; rewrite <- Rinv_1; + apply (Rinv_lt_contravar 1 eps); auto; + rewrite (let (H1, H2) := Rmult_ne eps in H2); unfold Rgt in H; + assumption. + unfold Rgt in H1; apply Rlt_le; assumption. + unfold Rgt; apply Rinv_0_lt_compat; apply lt_INR_0; apply lt_O_Sn. + - cut (0 <= up (/ eps - 1))%Z. + intro; elim (IZN (up (/ eps - 1)) H0); intros; split with x; intros; + rewrite (simpl_fact n); unfold R_dist; + rewrite (Rminus_0_r (Rabs (/ INR (S n)))); + rewrite (Rabs_Rabsolu (/ INR (S n))); cut (/ INR (S n) > 0). + intro; rewrite (Rabs_pos_eq (/ INR (S n))). + cut (/ eps - 1 < INR x). + intro ; + generalize + (Rlt_le_trans (/ eps - 1) (INR x) (INR n) H4 + (le_INR x n H2)); + clear H4; intro; unfold Rminus in H4; + generalize (Rplus_lt_compat_l 1 (/ eps + -1) (INR n) H4); + replace (1 + (/ eps + -1)) with (/ eps); [ clear H4; intro | ring ]. + rewrite (Rplus_comm 1 (INR n)) in H4; rewrite <- (S_INR n) in H4; + generalize (Rmult_gt_0_compat (/ INR (S n)) eps H3 H); + intro; unfold Rgt in H5; + generalize (Rmult_lt_compat_l (/ INR (S n) * eps) (/ eps) (INR (S n)) H5 H4); + intro; rewrite (Rmult_assoc (/ INR (S n)) eps (/ eps)) in H6; + rewrite (Rinv_r eps (Rlt_dichotomy_converse eps 0 (or_intror (eps < 0) H))) + in H6; rewrite (let (H1, H2) := Rmult_ne (/ INR (S n)) in H1) in H6; + rewrite (Rmult_comm (/ INR (S n))) in H6; + rewrite (Rmult_assoc eps (/ INR (S n)) (INR (S n))) in H6; + rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) (not_eq_sym (O_S n)))) in H6; + rewrite (let (H1, H2) := Rmult_ne eps in H1) in H6; + assumption. + cut (IZR (up (/ eps - 1)) = IZR (Z.of_nat x)); + [ intro | rewrite H1; trivial ]. + elim (archimed (/ eps - 1)); intros; clear H6; unfold Rgt in H5; + rewrite H4 in H5; rewrite INR_IZR_INZ; assumption. + unfold Rgt in H1; apply Rlt_le; assumption. + unfold Rgt; apply Rinv_0_lt_compat; apply lt_INR_0; apply lt_O_Sn. + apply (le_O_IZR (up (/ eps - 1))); + apply (Rle_trans 0 (/ eps - 1) (IZR (up (/ eps - 1)))). + generalize (Rnot_gt_le eps 1 Hnotgt); clear Hnotgt; unfold Rle; intro; elim H0; + clear H0; intro. + left; unfold Rgt in H; + generalize (Rmult_lt_compat_l (/ eps) eps 1 (Rinv_0_lt_compat eps H) H0); + rewrite + (Rinv_l eps + (not_eq_sym (Rlt_dichotomy_converse 0 eps (or_introl (0 > eps) H)))) + ; rewrite (let (H1, H2) := Rmult_ne (/ eps) in H1); + intro; fold (/ eps - 1 > 0); apply Rgt_minus; + unfold Rgt; assumption. + right; rewrite H0; rewrite Rinv_1; symmetry; apply Rminus_diag_eq; auto. + elim (archimed (/ eps - 1)); intros; clear H1; unfold Rgt in H0; apply Rlt_le; + assumption. Qed. diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index aafa3357e..1394abd2a 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -59,7 +59,7 @@ Proof. sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k + 1)) * r ^ (2 * k))) n) l }. - intro X; elim X; intros. + intros (x,p). exists x. split. apply p. diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index d8f1cc6aa..1a5171c9b 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -53,8 +53,7 @@ Proof. apply growing_cv. apply decreasing_growing; assumption. exact H0. - intro X. - elim X; intros. + intros (x,p). exists (- x). unfold Un_cv in p. unfold R_dist in p. @@ -151,7 +150,7 @@ Definition sequence_lb (Un:nat -> R) (pr:has_lb Un) (* Compatibility *) Notation sequence_majorant := sequence_ub (only parsing). Notation sequence_minorant := sequence_lb (only parsing). - +Unset Standard Proposition Elimination Names. Lemma Wn_decreasing : forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_ub Un pr). Proof. @@ -159,21 +158,15 @@ Proof. unfold Un_decreasing. intro. unfold sequence_ub. - 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. + pose proof (ub_to_lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)) as (x,(H1,H2)). + pose proof (ub_to_lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)) as (x0,(H3,H4)). cut (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr) = x); [ intro Maj1; rewrite Maj1 | idtac ]. 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. - elim p; intros. apply H2. - elim p0; intros. unfold is_upper_bound. - intros. + intros x1 H5. unfold is_upper_bound in H3. apply H3. elim H5; intros. @@ -184,12 +177,10 @@ Proof. cut (is_lub (EUn (fun k:nat => Un (n + k)%nat)) (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). + intros (H5,H6). + assert (H7 := H6 x0 H3). assert - (H7 := H3 (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)) H4). + (H8 := H4 (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)) H5). apply Rle_antisym; assumption. unfold lub. case (ub_to_lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)). @@ -197,13 +188,11 @@ Proof. cut (is_lub (EUn (fun k:nat => Un (S n + k)%nat)) (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). + intros (H5,H6). + assert (H7 := H6 x H1). assert - (H7 := - H3 (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)) H4). + (H8 := + H2 (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)) H5). apply Rle_antisym; assumption. unfold lub. case (ub_to_lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)). diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index 462a94db1..fb0c171ad 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -222,39 +222,37 @@ Proof. intro; apply Rle_lt_trans with (R_dist (sum_f_R0 Bn n) (sum_f_R0 Bn m)). assumption. apply H2; assumption. - assert (H5 := lt_eq_lt_dec n m). - elim H5; intro. - elim a; intro. - rewrite (tech2 An n m); [ idtac | assumption ]. - rewrite (tech2 Bn n m); [ idtac | assumption ]. - unfold R_dist; unfold Rminus; do 2 rewrite Ropp_plus_distr; - do 2 rewrite <- Rplus_assoc; do 2 rewrite Rplus_opp_r; - do 2 rewrite Rplus_0_l; do 2 rewrite Rabs_Ropp; repeat rewrite Rabs_right. - apply sum_Rle; intros. - elim (H (S n + n0)%nat); intros. - apply H8. - apply Rle_ge; apply cond_pos_sum; intro. - elim (H (S n + n0)%nat); intros. - apply Rle_trans with (An (S n + n0)%nat); assumption. - apply Rle_ge; apply cond_pos_sum; intro. - elim (H (S n + n0)%nat); intros; assumption. - rewrite b; unfold R_dist; unfold Rminus; + destruct (lt_eq_lt_dec n m) as [[| -> ]|]. + - rewrite (tech2 An n m); [ idtac | assumption ]. + rewrite (tech2 Bn n m); [ idtac | assumption ]. + unfold R_dist; unfold Rminus; do 2 rewrite Ropp_plus_distr; + do 2 rewrite <- Rplus_assoc; do 2 rewrite Rplus_opp_r; + do 2 rewrite Rplus_0_l; do 2 rewrite Rabs_Ropp; repeat rewrite Rabs_right. + apply sum_Rle; intros. + elim (H (S n + n0)%nat); intros. + apply H8. + apply Rle_ge; apply cond_pos_sum; intro. + elim (H (S n + n0)%nat); intros. + apply Rle_trans with (An (S n + n0)%nat); assumption. + apply Rle_ge; apply cond_pos_sum; intro. + elim (H (S n + n0)%nat); intros; assumption. + - unfold R_dist; unfold Rminus; do 2 rewrite Rplus_opp_r; rewrite Rabs_R0; right; reflexivity. - rewrite (tech2 An m n); [ idtac | assumption ]. - rewrite (tech2 Bn m n); [ idtac | assumption ]. - unfold R_dist; unfold Rminus; do 2 rewrite Rplus_assoc; - rewrite (Rplus_comm (sum_f_R0 An m)); rewrite (Rplus_comm (sum_f_R0 Bn m)); - do 2 rewrite Rplus_assoc; do 2 rewrite Rplus_opp_l; - do 2 rewrite Rplus_0_r; repeat rewrite Rabs_right. - apply sum_Rle; intros. - elim (H (S m + n0)%nat); intros; apply H8. - apply Rle_ge; apply cond_pos_sum; intro. - elim (H (S m + n0)%nat); intros. - apply Rle_trans with (An (S m + n0)%nat); assumption. - apply Rle_ge. - apply cond_pos_sum; intro. - elim (H (S m + n0)%nat); intros; assumption. + - rewrite (tech2 An m n); [ idtac | assumption ]. + rewrite (tech2 Bn m n); [ idtac | assumption ]. + unfold R_dist; unfold Rminus; do 2 rewrite Rplus_assoc; + rewrite (Rplus_comm (sum_f_R0 An m)); rewrite (Rplus_comm (sum_f_R0 Bn m)); + do 2 rewrite Rplus_assoc; do 2 rewrite Rplus_opp_l; + do 2 rewrite Rplus_0_r; repeat rewrite Rabs_right. + apply sum_Rle; intros. + elim (H (S m + n0)%nat); intros; apply H8. + apply Rle_ge; apply cond_pos_sum; intro. + elim (H (S m + n0)%nat); intros. + apply Rle_trans with (An (S m + n0)%nat); assumption. + apply Rle_ge. + apply cond_pos_sum; intro. + elim (H (S m + n0)%nat); intros; assumption. Qed. (** Cesaro's theorem *) -- cgit v1.2.3