diff options
Diffstat (limited to 'theories')
30 files changed, 171 insertions, 171 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index ca9bea5094..1ae9b9d5ed 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -103,7 +103,7 @@ destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as [R' H0]. intros [x HPx]. destruct (H x HPx) as [y HRxy]. exists y; exact HRxy. -pose (R'' := fun (x:A) (y:B) => exists H : P x, R' (existT P x H) y). +set (R'' := fun (x:A) (y:B) => exists H : P x, R' (existT P x H) y). exists R''; intros x HPx. destruct (H0 (existT P x HPx)) as [y [HRxy [HR'xy Huniq]]]. exists y. split. diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index a20036f0a5..d76d896585 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -45,7 +45,7 @@ Qed. Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False. Proof. intro HnotEM. -pose (R := fun A b => A /\ true = b \/ ~ A /\ false = b). +set (R := fun A b => A /\ true = b \/ ~ A /\ false = b). assert (H : exists f : Prop -> bool, (forall A:Prop, R A (f A))). apply description. intro A. @@ -75,4 +75,4 @@ destruct (f P). discriminate. assumption. Qed. -
\ No newline at end of file + diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 0ece7ac76a..aa4960a35b 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -130,7 +130,7 @@ Lemma aux : prop_extensionality -> bool_dep_induction -> true = false. Proof. intros Ext Ind. case (ext_prop_fixpoint Ext bool true); intros G Gfix. -pose (neg := fun b:bool => bool_elim bool false true b). +set (neg := fun b:bool => bool_elim bool false true b). generalize (refl_equal (G neg)). pattern (G neg) at 1 in |- *. apply Ind with (b := G neg); intro Heq. @@ -145,7 +145,7 @@ Lemma ext_prop_dep_proof_irrel_gen : prop_extensionality -> bool_dep_induction -> proof_irrelevance. Proof. intros Ext Ind A a1 a2. -pose (f := fun b:bool => bool_elim A a1 a2 b). +set (f := fun b:bool => bool_elim A a1 a2 b). rewrite (bool_elim_redl A a1 a2). change (f true = a2) in |- *. rewrite (bool_elim_redr A a1 a2). diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index e1fb12f398..03c31298f7 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -100,8 +100,8 @@ intro P. (* first we exhibit the choice functional relation R *) destruct AC as [R H]. -pose (class_of_true := fun b => b = true \/ P). -pose (class_of_false := fun b => b = false \/ P). +set (class_of_true := fun b => b = true \/ P). +set (class_of_false := fun b => b = false \/ P). (* the actual "decision": is (R class_of_true) = true or false? *) destruct (H class_of_true) as [b0 [H0 [H0' H0'']]]. diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index 7d8a939143..396029c035 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -121,8 +121,8 @@ Lemma Alembert_C2 : 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). intros. -pose (Vn := fun i:nat => (2 * Rabs (An i) + An i) / 2). -pose (Wn := fun i:nat => (2 * Rabs (An i) - An i) / 2). +set (Vn := fun i:nat => (2 * Rabs (An i) + An i) / 2). +set (Wn := fun i:nat => (2 * Rabs (An i) - An i) / 2). cut (forall n:nat, 0 < Vn n). intro; cut (forall n:nat, 0 < Wn n). intro; cut (Un_cv (fun n:nat => Rabs (Vn (S n) / Vn n)) 0). @@ -135,7 +135,7 @@ apply existT with (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. -pose (N := max x1 x2). +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). unfold R_dist in |- *; @@ -340,7 +340,7 @@ Lemma AlembertC3_step1 : (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). -intros; pose (Bn := fun i:nat => An i * x ^ i). +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). diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index e9be3fc028..9cbbd1ea5d 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -164,7 +164,7 @@ intros; cut (0 < eps / 2); [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. elim (H1 (eps / 2) H5); intros N2 H6. elim (p (eps / 2) H5); intros N1 H7. -pose (N := max (S (2 * N1)) N2). +set (N := max (S (2 * N1)) N2). exists N; intros. assert (H9 := even_odd_cor n). elim H9; intros P H10. diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index 8be8c47faf..ef632a0914 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -20,7 +20,7 @@ intros; red in |- *; intro. cut (forall n m:nat, (m <= n)%nat -> (n - m)%nat = 0%nat -> n = m). intro; assert (H2 := H1 _ _ (lt_le_weak _ _ H) H0); rewrite H2 in H; elim (lt_irrefl _ H). -pose (R := fun n m:nat => (m <= n)%nat -> (n - m)%nat = 0%nat -> n = m). +set (R := fun n m:nat => (m <= n)%nat -> (n - m)%nat = 0%nat -> n = m). cut ((forall n m:nat, R n m) -> forall n0 m:nat, (m <= n0)%nat -> (n0 - m)%nat = 0%nat -> n0 = m). @@ -34,7 +34,7 @@ unfold R in |- *; intros; apply H1; assumption. Qed. Lemma le_minusni_n : forall n i:nat, (i <= n)%nat -> (n - i <= n)%nat. -pose (R := fun m n:nat => (n <= m)%nat -> (m - n <= m)%nat). +set (R := fun m n:nat => (n <= m)%nat -> (m - n <= m)%nat). cut ((forall m n:nat, R m n) -> forall n i:nat, (i <= n)%nat -> (n - i <= n)%nat). intro; apply H. @@ -89,7 +89,7 @@ Lemma euclidian_division : y <> 0 -> exists k : Z, (exists r : R, x = IZR k * y + r /\ 0 <= r < Rabs y). intros. -pose +set (k0 := match Rcase_abs y with | left _ => (1 - up (x / - y))%Z diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v index e8173b82e4..ad5a358e8a 100644 --- a/theories/Reals/Binomial.v +++ b/theories/Reals/Binomial.v @@ -135,7 +135,7 @@ replace (y ^ 0) with 1; [ rewrite Rmult_1_r | simpl in |- *; reflexivity ]. induction n as [| n Hrecn0]. simpl in |- *; do 2 rewrite H; ring. (* N >= 1 *) -pose (N := S n). +set (N := S n). rewrite Rmult_plus_distr_l. replace (sum_f_R0 (fun i:nat => C N i * x ^ i * y ^ (N - i)) N * x) with (sum_f_R0 (fun i:nat => C N i * x ^ S i * y ^ (N - i)) N). @@ -145,8 +145,8 @@ rewrite (decomp_sum (fun i:nat => C (S N) i * x ^ i * y ^ (S N - i)) N). rewrite H; replace (x ^ 0) with 1; [ idtac | reflexivity ]. do 2 rewrite Rmult_1_l. replace (S N - 0)%nat with (S N); [ idtac | reflexivity ]. -pose (An := fun i:nat => C N i * x ^ S i * y ^ (N - i)). -pose (Bn := fun i:nat => C N (S i) * x ^ S i * y ^ (N - i)). +set (An := fun i:nat => C N i * x ^ S i * y ^ (N - i)). +set (Bn := fun i:nat => C N (S i) * x ^ S i * y ^ (N - i)). replace (pred N) with n. replace (sum_f_R0 (fun i:nat => C (S N) (S i) * x ^ S i * y ^ (S N - S i)) n) with (sum_f_R0 (fun i:nat => An i + Bn i) n). @@ -156,7 +156,7 @@ rewrite (Rplus_comm (sum_f_R0 An n)). repeat rewrite Rplus_assoc. rewrite <- tech5. fold N in |- *. -pose (Cn := fun i:nat => C N i * x ^ i * y ^ (S N - i)). +set (Cn := fun i:nat => C N i * x ^ i * y ^ (S N - i)). cut (forall i:nat, (i < N)%nat -> Cn (S i) = Bn i). intro; replace (sum_f_R0 Bn n) with (sum_f_R0 (fun i:nat => Cn (S i)) n). replace (y ^ S N) with (Cn 0%nat). diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v index 6cd5fa17fa..543e1a8520 100644 --- a/theories/Reals/Cauchy_prod.v +++ b/theories/Reals/Cauchy_prod.v @@ -115,13 +115,13 @@ replace (pred (pred (N - k)))) (pred (pred N)) + An (S N) * sum_f_R0 (fun l:nat => Bn (S l)) (pred N)). rewrite (decomp_sum Bn N H1); rewrite Rmult_plus_distr_l. -pose +set (Z := sum_f_R0 (fun k:nat => sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat) (pred (pred (N - k)))) (pred (pred N))); - pose (Z2 := sum_f_R0 (fun i:nat => Bn (S i)) (pred N)); + set (Z2 := sum_f_R0 (fun i:nat => Bn (S i)) (pred N)); ring. rewrite (sum_N_predN diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v index d29193ad7d..f2b2bcd850 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -20,8 +20,8 @@ Definition Majxy (x y:R) (n:nat) : R := Lemma Majxy_cv_R0 : forall x y:R, Un_cv (Majxy x y) 0. intros. -pose (C := Rmax 1 (Rmax (Rabs x) (Rabs y))). -pose (C0 := C ^ 4). +set (C := Rmax 1 (Rmax (Rabs x) (Rabs y))). +set (C0 := C ^ 4). cut (0 < C). intro. cut (0 < C0). @@ -69,7 +69,7 @@ Lemma reste1_maj : forall (x y:R) (N:nat), (0 < N)%nat -> Rabs (Reste1 x y N) <= Majxy x y (pred N). intros. -pose (C := Rmax 1 (Rmax (Rabs x) (Rabs y))). +set (C := Rmax 1 (Rmax (Rabs x) (Rabs y))). unfold Reste1 in |- *. apply Rle_trans with (sum_f_R0 @@ -454,7 +454,7 @@ Qed. Lemma reste2_maj : forall (x y:R) (N:nat), (0 < N)%nat -> Rabs (Reste2 x y N) <= Majxy x y N. intros. -pose (C := Rmax 1 (Rmax (Rabs x) (Rabs y))). +set (C := Rmax 1 (Rmax (Rabs x) (Rabs y))). unfold Reste2 in |- *. apply Rle_trans with (sum_f_R0 @@ -926,8 +926,8 @@ Qed. Lemma reste_cv_R0 : forall x y:R, Un_cv (Reste x y) 0. intros. unfold Reste in |- *. -pose (An := fun n:nat => Reste2 x y n). -pose (Bn := fun n:nat => Reste1 x y (S n)). +set (An := fun n:nat => Reste2 x y n). +set (Bn := fun n:nat => Reste1 x y (S n)). cut (Un_cv (fun n:nat => An n - Bn n) (0 - 0) -> Un_cv (fun N:nat => Reste2 x y N - Reste1 x y (S N)) 0). @@ -979,7 +979,7 @@ cut (0 < eps / 3); elim (H4 (eps / 3) H7); intros N1 H8. elim (H5 (eps / 3) H7); intros N2 H9. elim (H6 (eps / 3) H7); intros N3 H10. -pose (N := S (S (max (max N1 N2) N3))). +set (N := S (S (max (max N1 N2) N3))). exists N. intros. cut (n = S (pred n)). diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index 5e9d26001f..1054f73ecb 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -98,7 +98,7 @@ replace sum_f_R0 (fun l:nat => C (2 * k) (2 * l) * x ^ (2 * l) * y ^ (2 * (k - l))) k) (S n)). -pose +set (sin_nnn := fun n:nat => match n with @@ -135,7 +135,7 @@ unfold sin_nnn in |- *. rewrite <- Rmult_plus_distr_l. apply Rmult_eq_compat_l. rewrite binomial. -pose (Wn := fun i0:nat => C (2 * S i) i0 * x ^ i0 * y ^ (2 * S i - i0)). +set (Wn := fun i0:nat => C (2 * S i) i0 * x ^ i0 * y ^ (2 * S i - i0)). replace (sum_f_R0 (fun l:nat => C (2 * S i) (2 * l) * x ^ (2 * l) * y ^ (2 * (S i - l))) diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index c424b9e140..ffc3005045 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -114,7 +114,7 @@ Qed. Lemma Reste_E_maj : forall (x y:R) (N:nat), (0 < N)%nat -> Rabs (Reste_E x y N) <= maj_Reste_E x y N. -intros; pose (M := Rmax 1 (Rmax (Rabs x) (Rabs y))). +intros; set (M := Rmax 1 (Rmax (Rabs x) (Rabs y))). apply Rle_trans with (M ^ (2 * N) * sum_f_R0 @@ -742,7 +742,7 @@ Qed. (**********) Lemma exp_pos_pos : forall x:R, 0 < x -> 0 < exp x. -intros; pose (An := fun N:nat => / INR (fact N) * x ^ N). +intros; set (An := fun N:nat => / INR (fact N) * x ^ N). cut (Un_cv (fun n:nat => sum_f_R0 An n) (exp x)). intro; apply Rlt_le_trans with (sum_f_R0 An 0). unfold An in |- *; simpl in |- *; rewrite Rinv_1; rewrite Rmult_1_r; @@ -784,7 +784,7 @@ Qed. (* ((exp h)-1)/h -> 0 quand h->0 *) Lemma derivable_pt_lim_exp_0 : derivable_pt_lim exp 0 1. unfold derivable_pt_lim in |- *; intros. -pose (fn := fun (N:nat) (x:R) => x ^ N / INR (fact (S N))). +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 cv; cut (forall n:nat, continuity (fn n)). diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v index d7531e49f5..a6c2d115c5 100644 --- a/theories/Reals/MVT.v +++ b/theories/Reals/MVT.v @@ -25,7 +25,7 @@ Theorem MVT : (g b - g a) * derive_pt f c (pr1 c P) = (f b - f a) * derive_pt g c (pr2 c P)). intros; assert (H2 := Rlt_le _ _ H). -pose (h := fun y:R => (g b - g a) * f y - (f b - f a) * g y). +set (h := fun y:R => (g b - g a) * f y - (f b - f a) * g y). cut (forall c:R, a < c < b -> derivable_pt h c). intro; cut (forall c:R, a <= c <= b -> continuity_pt h c). intro; assert (H4 := continuity_ab_maj h a b H2 H3). @@ -33,7 +33,7 @@ assert (H5 := continuity_ab_min h a b H2 H3). elim H4; intros Mx H6. elim H5; intros mx H7. cut (h a = h b). -intro; pose (M := h Mx); pose (m := h mx). +intro; set (M := h Mx); set (m := h mx). cut (forall (c:R) (P:a < c < b), derive_pt h c (X c P) = diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index e2080827bf..2d55efe780 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -288,7 +288,7 @@ assert (H6 := H _ H5); elim H6; clear H6; intros; unfold derivable_pt_lim in |- *; assert (H7 : derive_pt F0 x x0 = f x). symmetry in |- *; assumption. assert (H8 := derive_pt_eq_1 F0 x (f x) x0 H7); unfold derivable_pt_lim in H8; - intros; elim (H8 _ H9); intros; pose (D := Rmin x1 (b - x)). + intros; elim (H8 _ H9); intros; set (D := Rmin x1 (b - x)). assert (H11 : 0 < D). unfold D in |- *; unfold Rmin in |- *; case (Rle_dec x1 (b - x)); intro. apply (cond_pos x1). @@ -335,7 +335,7 @@ assert (H11 := derive_pt_eq_1 F0 x (f x) x1 H9); | right _ => F1 x + (F0 b - F1 b) end) x (f x)). unfold derivable_pt_lim in |- *; unfold derivable_pt_lim in H11, H12; intros; - elim (H11 _ H13); elim (H12 _ H13); intros; pose (D := Rmin x2 x3); + elim (H11 _ H13); elim (H12 _ H13); intros; set (D := Rmin x2 x3); assert (H16 : 0 < D). unfold D in |- *; unfold Rmin in |- *; case (Rle_dec x2 x3); intro. apply (cond_pos x2). @@ -375,7 +375,7 @@ assert (H6 := H0 _ H5); elim H6; clear H6; intros; unfold derivable_pt_lim in |- *; assert (H7 : derive_pt F1 x x0 = f x). symmetry in |- *; assumption. assert (H8 := derive_pt_eq_1 F1 x (f x) x0 H7); unfold derivable_pt_lim in H8; - intros; elim (H8 _ H9); intros; pose (D := Rmin x1 (x - b)); + intros; elim (H8 _ H9); intros; set (D := Rmin x1 (x - b)); assert (H11 : 0 < D). unfold D in |- *; unfold Rmin in |- *; case (Rle_dec x1 (x - b)); intro. apply (cond_pos x1). @@ -462,7 +462,7 @@ Lemma NewtonInt_P7 : Newton_integrable f b c -> Newton_integrable f a c. unfold Newton_integrable in |- *; intros f a b c Hab Hbc X X0; elim X; clear X; intros F0 H0; elim X0; clear X0; intros F1 H1; - pose + set (g := fun x:R => match Rle_dec x b with diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v index b6375829bf..130f3b6596 100644 --- a/theories/Reals/PSeries_reg.v +++ b/theories/Reals/PSeries_reg.v @@ -110,7 +110,7 @@ elim H6; intros del1 H7. unfold continuity_pt in H5; unfold continue_in in H5; unfold limit1_in in H5; unfold limit_in in H5; simpl in H5; unfold R_dist in H5. elim (H5 _ H3); intros del2 H8. -pose (del := Rmin del1 del2). +set (del := Rmin del1 del2). exists del; intros. split. unfold del in |- *; unfold Rmin in |- *; case (Rle_dec del1 del2); intro. @@ -226,7 +226,7 @@ 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). intros; apply R_complete. -unfold SP in |- *; pose (An := fun N:nat => fn N x). +unfold SP in |- *; set (An := fun N:nat => fn N x). change (Cauchy_crit_series An) in |- *. apply cauchy_abs. unfold Cauchy_crit_series in |- *; apply CV_Cauchy. diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index c12aea9df6..6a65ade8b3 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -212,7 +212,7 @@ assumption. cut (0 < Rabs ((l1 - l2) / 2)); [ intro | apply Rabs_pos_lt ]. elim (H (Rabs ((l1 - l2) / 2)) H2); intros. elim (H0 (Rabs ((l1 - l2) / 2)) H2); intros. -pose (N := max x0 x); cut (N >= x0)%nat. +set (N := max x0 x); cut (N >= x0)%nat. cut (N >= x)%nat. intros; assert (H7 := H3 N H5); assert (H8 := H4 N H6). cut (Rabs (l1 - l2) <= R_dist (sum_f_R0 An N) l1 + R_dist (sum_f_R0 An N) l2). @@ -390,7 +390,7 @@ do 2 rewrite Rabs_Ropp. rewrite (Rabs_right (sum_f_R0 (fun i:nat => Rabs (An (S n + i)%nat)) (m - S n))) . -pose (Bn := fun i:nat => An (S n + i)%nat). +set (Bn := fun i:nat => An (S n + i)%nat). replace (fun i:nat => Rabs (An (S n + i)%nat)) with (fun i:nat => Rabs (Bn i)). apply Rabs_triang_gen. @@ -415,7 +415,7 @@ do 2 rewrite Rplus_0_r. rewrite (Rabs_right (sum_f_R0 (fun i:nat => Rabs (An (S m + i)%nat)) (n - S m))) . -pose (Bn := fun i:nat => An (S m + i)%nat). +set (Bn := fun i:nat => An (S m + i)%nat). replace (fun i:nat => Rabs (An (S m + i)%nat)) with (fun i:nat => Rabs (Bn i)). apply Rabs_triang_gen. @@ -489,11 +489,11 @@ elim s; intro. left; apply a. right; apply b. cut (Un_growing (fun n:nat => sum_f_R0 An n)). -intro; pose (l1 := sum_f_R0 An N). +intro; set (l1 := sum_f_R0 An N). fold l1 in r. unfold Un_cv in H; cut (0 < l1 - l). intro; elim (H _ H2); intros. -pose (N0 := max x N); cut (N0 >= x)%nat. +set (N0 := max x N); cut (N0 >= x)%nat. intro; assert (H5 := H3 N0 H4). cut (l1 <= sum_f_R0 An N0). intro; unfold R_dist in H5; rewrite Rabs_right in H5. @@ -534,7 +534,7 @@ intro; cut (0 < (Rabs l1 - l2) / 2). intro; unfold Un_cv in H, H0. elim (H _ H3); intros Na H4. elim (H0 _ H3); intros Nb H5. -pose (N := max Na Nb). +set (N := max Na Nb). unfold R_dist in H4, H5. cut (Rabs (sum_f_R0 An N - l2) < (Rabs l1 - l2) / 2). intro; cut (Rabs (Rabs l1 - Rabs (SP fn N x)) < (Rabs l1 - l2) / 2). diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index b7d4902254..868ca35fc5 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -931,7 +931,7 @@ reflexivity. replace (fun y:R => y ^ S n) with (fun y:R => y * y ^ n). replace (pred (S n)) with n; [ idtac | reflexivity ]. replace (fun y:R => y * y ^ n) with (id * (fun y:R => y ^ n))%F. -pose (f := fun y:R => y ^ n). +set (f := fun y:R => y ^ n). replace (INR (S n) * x ^ n) with (1 * f x + id x * (INR n * x ^ pred n)). apply derivable_pt_lim_mult. apply derivable_pt_lim_id. diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v index 53624cbb2d..5887e8ef06 100644 --- a/theories/Reals/Rcomplete.v +++ b/theories/Reals/Rcomplete.v @@ -26,8 +26,8 @@ Open Local Scope R_scope. Theorem R_complete : forall Un:nat -> R, Cauchy_crit Un -> sigT (fun l:R => Un_cv Un l). intros. -pose (Vn := sequence_minorant Un (cauchy_min Un H)). -pose (Wn := sequence_majorant Un (cauchy_maj Un H)). +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). @@ -118,7 +118,7 @@ elim (p0 (eps / 5) H3); intros N2 H5. unfold Cauchy_crit in H. unfold R_dist in H. elim (H (eps / 5) H3); intros N3 H6. -pose (N := max (max N1 N2) N3). +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 ]. apply Rle_lt_trans with diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 8b087856c6..7ebeed34b8 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -144,8 +144,8 @@ Lemma RiemannInt_P3 : intros; case (Rle_dec a b); intro. apply RiemannInt_P2 with f un wn; assumption. assert (H1 : b <= a); auto with real. -pose (vn' := fun n:nat => mkStepFun (StepFun_P6 (pre (vn n)))); - pose (wn' := fun n:nat => mkStepFun (StepFun_P6 (pre (wn n)))); +set (vn' := fun n:nat => mkStepFun (StepFun_P6 (pre (vn n)))); + set (wn' := fun n:nat => mkStepFun (StepFun_P6 (pre (wn n)))); assert (H2 : forall n:nat, @@ -221,7 +221,7 @@ unfold Un_cv in |- *; unfold R_dist in |- *; intros f; intros; unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. elim (H _ H3); clear H; intros N0 H; elim (H0 _ H3); clear H0; intros N1 H0; - elim (H1 _ H3); clear H1; intros N2 H1; pose (N := max (max N0 N1) N2); + elim (H1 _ H3); clear H1; intros N2 H1; set (N := max (max N0 N1) N2); exists N; intros; apply Rle_lt_trans with (Rabs @@ -426,7 +426,7 @@ 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). -intros; pose (I := fun n:nat => a + INR n * del < b); +intros; set (I := fun n:nat => a + INR n * del < b); assert (H0 : exists n : nat, I n). exists 0%nat; unfold I in |- *; rewrite Rmult_0_l; rewrite Rplus_0_r; assumption. @@ -487,7 +487,7 @@ Lemma Heine_cor1 : a <= x <= b -> a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps)). intro f; intros; - pose + set (E := fun l:R => 0 < l <= b - a /\ @@ -512,7 +512,7 @@ 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. apply H5. unfold is_lub in p; elim p; intros; unfold is_upper_bound in H6; - pose (D := Rabs (x0 - y)); elim (classic (exists y : R, D < y /\ E y)); + set (D := Rabs (x0 - y)); elim (classic (exists y : R, D < y /\ E y)); intro. elim H11; intros; elim H12; clear H12; intros; unfold E in H13; elim H13; intros; apply H15; assumption. @@ -743,7 +743,7 @@ apply le_lt_n_Sm; assumption. apply Rge_minus; apply Rle_ge; assumption. intros; clear H0 H1 H4 phi H5 H6 t H7; case (Req_dec t0 b); intro. left; assumption. -right; pose (I := fun j:nat => a + INR j * del <= t0); +right; set (I := fun j:nat => a + INR j * del <= t0); assert (H1 : exists n : nat, I n). exists 0%nat; unfold I in |- *; rewrite Rmult_0_l; rewrite Rplus_0_r; elim H8; intros; assumption. @@ -1070,7 +1070,7 @@ unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. elim (H _ H4); clear H; intros N0 H. elim (H2 _ H4); clear H2; intros N1 H2. -pose (N := max N0 N1); exists N; intros; unfold R_dist in |- *. +set (N := max N0 N1); exists N; intros; unfold R_dist in |- *. apply Rle_lt_trans with (Rabs (RiemannInt_SF (phi2 n) - RiemannInt_SF (phi1 n)) + Rabs (RiemannInt_SF (phi1 n) - l)). @@ -1142,7 +1142,7 @@ unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. elim (H _ H4); clear H; intros N0 H. elim (H2 _ H4); clear H2; intros N1 H2. -pose (N := max N0 N1); exists N; intros; unfold R_dist in |- *. +set (N := max N0 N1); exists N; intros; unfold R_dist in |- *. apply Rle_lt_trans with (Rabs (RiemannInt_SF (phi2 n) - RiemannInt_SF (phi1 n)) + Rabs (RiemannInt_SF (phi1 n) - l)). @@ -1242,8 +1242,8 @@ pattern l at 2 in |- *; rewrite H0; rewrite Rmult_0_l; rewrite Rplus_0_r; case (RiemannInt_exists pr1 RinvN RinvN_cv); intros; eapply UL_sequence; [ apply u0 - | pose (psi1 := fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); - pose (psi2 := fun n:nat => projT1 (phi_sequence_prop RinvN pr3 n)); + | set (psi1 := fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); + set (psi2 := fun n:nat => projT1 (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)) @@ -1277,7 +1277,7 @@ unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ prove_sup0 | apply Rabs_pos_lt; assumption ] ]. elim (u _ H5); clear u; intros N2 H6; assert (H7 := RinvN_cv); unfold Un_cv in H7; elim (H7 _ H5); clear H7 H5; intros N3 H5; - unfold R_dist in H3, H4, H5, H6; pose (N := max (max N0 N1) (max N2 N3)). + unfold R_dist in H3, H4, H5, H6; set (N := max (max N0 N1) (max N2 N3)). assert (H7 : forall n:nat, (n >= N1)%nat -> RinvN n < eps / 5). intros; replace (pos (RinvN n)) with (Rabs (RinvN n - 0)); [ unfold RinvN in |- *; apply H4; assumption @@ -1508,9 +1508,9 @@ Lemma RiemannInt_P15 : intros; unfold RiemannInt in |- *; case (RiemannInt_exists pr RinvN RinvN_cv); intros; eapply UL_sequence. apply u. -pose (phi1 := fun N:nat => phi_sequence RinvN pr N); +set (phi1 := fun N:nat => phi_sequence RinvN pr N); change (Un_cv (fun N:nat => RiemannInt_SF (phi1 N)) (c * (b - a))) in |- *; - pose (f := fct_cte c); + set (f := fct_cte c); assert (H1 : exists psi1 : nat -> StepFun a b, @@ -1522,8 +1522,8 @@ pose (phi1 := fun N:nat => phi_sequence RinvN pr N); split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr n)); intro; apply (projT2 (phi_sequence_prop RinvN pr n)). elim H1; clear H1; intros psi1 H1; - pose (phi2 := fun n:nat => mkStepFun (StepFun_P4 a b c)); - pose (psi2 := fun n:nat => mkStepFun (StepFun_P4 a b 0)); + set (phi2 := fun n:nat => mkStepFun (StepFun_P4 a b c)); + set (psi2 := fun n:nat => mkStepFun (StepFun_P4 a b 0)); apply RiemannInt_P11 with f RinvN phi2 psi2 psi1; try assumption. apply RinvN_cv. @@ -1559,7 +1559,7 @@ clear n; assert (H3 : 0 < (l1 - l2) / 2). unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ apply Rlt_Rminus; assumption | apply Rinv_0_lt_compat; prove_sup0 ]. elim (H1 _ H3); elim (H0 _ H3); clear H0 H1; unfold R_dist in |- *; intros; - pose (N := max x x0); cut (Vn N < Un N). + set (N := max x x0); cut (Vn N < Un N). intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (H N) H4)). apply Rlt_trans with ((l1 + l2) / 2). apply Rplus_lt_reg_r with (- l2); @@ -1593,8 +1593,8 @@ Lemma RiemannInt_P17 : intro f; intros; unfold RiemannInt in |- *; case (RiemannInt_exists pr1 RinvN RinvN_cv); case (RiemannInt_exists pr2 RinvN RinvN_cv); intros; - pose (phi1 := phi_sequence RinvN pr1); - pose (phi2 := fun N:nat => mkStepFun (StepFun_P32 (phi1 N))); + set (phi1 := phi_sequence RinvN pr1); + set (phi2 := fun N:nat => mkStepFun (StepFun_P32 (phi1 N))); apply Rle_cv_lim with (fun N:nat => Rabs (RiemannInt_SF (phi1 N))) (fun N:nat => RiemannInt_SF (phi2 N)). @@ -1603,7 +1603,7 @@ fold phi1 in u0; apply (continuity_seq Rabs (fun N:nat => RiemannInt_SF (phi1 N)) x0); try assumption. apply Rcontinuity_abs. -pose (phi3 := phi_sequence RinvN pr2); +set (phi3 := phi_sequence RinvN pr2); assert (H0 : exists psi3 : nat -> StepFun a b, @@ -1652,7 +1652,7 @@ intro f; intros; unfold RiemannInt in |- *; case (RiemannInt_exists pr2 RinvN RinvN_cv); intros; eapply UL_sequence. apply u0. -pose (phi1 := fun N:nat => phi_sequence RinvN pr1 N); +set (phi1 := fun N:nat => phi_sequence RinvN pr1 N); change (Un_cv (fun N:nat => RiemannInt_SF (phi1 N)) x) in |- *; assert (H1 : @@ -1665,8 +1665,8 @@ pose (phi1 := fun N:nat => phi_sequence RinvN pr1 N); split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); intro; apply (projT2 (phi_sequence_prop RinvN pr1 n)). elim H1; clear H1; intros psi1 H1; - pose (phi2 := fun N:nat => phi_sequence RinvN pr2 N). -pose + set (phi2 := fun N:nat => phi_sequence RinvN pr2 N). +set (phi2_aux := fun (N:nat) (x:R) => match Req_EM_T x a with @@ -1678,7 +1678,7 @@ pose end end). cut (forall N:nat, IsStepFun (phi2_aux N) a b). -intro; pose (phi2_m := fun N:nat => mkStepFun (X N)). +intro; set (phi2_m := fun N:nat => mkStepFun (X N)). assert (H2 : exists psi2 : nat -> StepFun a b, @@ -1850,7 +1850,7 @@ unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ apply (cond_pos eps) | apply Rinv_0_lt_compat; prove_sup0 ]. elim (X (mkposreal _ H)); clear X; intros phi1 [psi1 H1]; elim (X0 (mkposreal _ H)); clear X0; intros phi2 [psi2 H2]. -pose +set (phi3 := fun x:R => match Rle_dec a x with @@ -1861,7 +1861,7 @@ pose end | right _ => 0 end). -pose +set (psi3 := fun x:R => match Rle_dec a x with @@ -2276,7 +2276,7 @@ elim (u1 _ H0); clear u1; intros N1 H1; elim (u0 _ H0); clear u0; (RiemannInt_SF (phi_sequence RinvN pr1 n) + RiemannInt_SF (phi_sequence RinvN pr2 n))) 0). intro; elim (H3 _ H0); clear H3; intros N3 H3; - pose (N0 := max (max N1 N2) N3); exists N0; intros; + set (N0 := max (max N1 N2) N3); exists N0; intros; unfold R_dist in |- *; apply Rle_lt_trans with (Rabs @@ -2372,9 +2372,9 @@ unfold R_dist in |- *; unfold Rminus in |- *; rewrite Ropp_0; left; apply (cond_pos (RinvN n)). exists N0; intros; elim (H1 n); elim (H2 n); elim (H3 n); clear H1 H2 H3; intros; unfold R_dist in |- *; unfold Rminus in |- *; - rewrite Ropp_0; rewrite Rplus_0_r; pose (phi1 := phi_sequence RinvN pr1 n); - fold phi1 in H8; pose (phi2 := phi_sequence RinvN pr2 n); - fold phi2 in H3; pose (phi3 := phi_sequence RinvN pr3 n); + rewrite Ropp_0; rewrite Rplus_0_r; set (phi1 := phi_sequence RinvN pr1 n); + fold phi1 in H8; set (phi2 := phi_sequence RinvN pr2 n); + fold phi2 in H3; set (phi3 := phi_sequence RinvN pr3 n); fold phi2 in H1; assert (H10 : IsStepFun phi3 a b). apply StepFun_P44 with c. apply (pre phi3). @@ -2577,7 +2577,7 @@ unfold derivable_pt_lim in |- *; intros; assert (Hyp : 0 < eps / 2). unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. elim (H1 _ Hyp); unfold dist, D_x, no_cond in |- *; simpl in |- *; - unfold R_dist in |- *; intros; pose (del := Rmin x0 (Rmin (b - x) (x - a))); + unfold R_dist in |- *; intros; set (del := Rmin x0 (Rmin (b - x) (x - a))); assert (H4 : 0 < del). unfold del in |- *; unfold Rmin in |- *; case (Rle_dec (b - x) (x - a)); intro. @@ -2786,7 +2786,7 @@ intro f; intros; elim h; intro. elim H; clear H; intros; elim H; intro. elim H1; intro. apply RiemannInt_P27; split; assumption. -pose +set (f_b := fun x:R => f b * (x - b) + RiemannInt (FTC_P1 h C0 h (Rle_refl b))); rewrite H3. assert (H4 : derivable_pt_lim f_b b (f b)). @@ -2815,7 +2815,7 @@ assert (H8 : 0 < eps / 2). unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. elim (H7 _ H8); unfold D_x, no_cond, dist in |- *; simpl in |- *; - unfold R_dist in |- *; intros; pose (del := Rmin x0 (Rmin x1 (b - a))); + unfold R_dist in |- *; intros; set (del := Rmin x0 (Rmin x1 (b - a))); assert (H10 : 0 < del). unfold del in |- *; unfold Rmin in |- *; case (Rle_dec x1 (b - a)); intros. case (Rle_dec x0 x1); intro; @@ -2960,7 +2960,7 @@ unfold f_b in |- *; unfold Rminus in |- *; rewrite Rplus_opp_r; | elim n; left; assumption | elim n; right; reflexivity ]. (*****) -pose (f_a := fun x:R => f a * (x - a)); rewrite <- H2; +set (f_a := fun x:R => f a * (x - a)); rewrite <- H2; assert (H3 : derivable_pt_lim f_a a (f a)). unfold f_a in |- *; change (derivable_pt_lim (fct_cte (f a) * (id - fct_cte a)%F) a (f a)) @@ -2981,7 +2981,7 @@ unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. elim (H6 _ H7); unfold D_x, no_cond, dist in |- *; simpl in |- *; unfold R_dist in |- *; intros. -pose (del := Rmin x0 (Rmin x1 (b - a))). +set (del := Rmin x0 (Rmin x1 (b - a))). assert (H9 : 0 < del). unfold del in |- *; unfold Rmin in |- *. case (Rle_dec x1 (b - a)); intros. @@ -3116,7 +3116,7 @@ rewrite Rplus_comm; apply Rle_trans with del; (*****) assert (H1 : x = a). rewrite <- H0 in H; elim H; intros; apply Rle_antisym; assumption. -pose (f_a := fun x:R => f a * (x - a)). +set (f_a := fun x:R => f a * (x - a)). assert (H2 : derivable_pt_lim f_a a (f a)). unfold f_a in |- *; change (derivable_pt_lim (fct_cte (f a) * (id - fct_cte a)%F) a (f a)) @@ -3129,7 +3129,7 @@ apply derivable_pt_lim_minus. apply derivable_pt_lim_id. apply derivable_pt_lim_const. unfold fct_cte in |- *; ring. -pose +set (f_b := fun x:R => f b * (x - b) + RiemannInt (FTC_P1 h C0 h (Rle_refl b))). assert (H3 : derivable_pt_lim f_b b (f b)). unfold f_b in |- *; pattern (f b) at 2 in |- *; replace (f b) with (f b + 0). @@ -3151,7 +3151,7 @@ unfold fct_cte in |- *; ring. apply derivable_pt_lim_const. ring. unfold derivable_pt_lim in |- *; intros; elim (H2 _ H4); intros; - elim (H3 _ H4); intros; pose (del := Rmin x0 x1). + elim (H3 _ H4); intros; set (del := Rmin x0 x1). assert (H7 : 0 < del). unfold del in |- *; unfold Rmin in |- *; case (Rle_dec x0 x1); intro. apply (cond_pos x0). diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 19782f2bcb..f0b4793ebf 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -31,7 +31,7 @@ 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)). -intros I H H0; pose (E := fun x:R => exists i : nat, I i /\ INR i = x); +intros I H H0; set (E := fun x:R => exists i : nat, I i /\ INR i = x); assert (H1 : bound E). unfold Nbound in H0; elim H0; intros N H1; unfold bound in |- *; exists (INR N); unfold is_upper_bound in |- *; intros; @@ -534,7 +534,7 @@ rewrite <- H4; apply RList_P7; clear Hrecs3; induction lf2 as [| r5 lf2 Hreclf2]. simpl in H11; discriminate. clear Hreclf2; assert (H17 : r3 = r4). -pose (x := (r + s2) / 2); assert (H17 := H8 0%nat (lt_O_Sn _)); +set (x := (r + s2) / 2); assert (H17 := H8 0%nat (lt_O_Sn _)); assert (H18 := H13 0%nat (lt_O_Sn _)); unfold constant_D_eq, open_interval in H17, H18; simpl in H17; simpl in H18; rewrite <- (H17 x). @@ -578,7 +578,7 @@ assert (H19 : r3 = r5). assert (H19 := H7 1%nat); simpl in H19; assert (H20 := H19 (lt_n_S _ _ (lt_O_Sn _))); elim H20; intro. -pose (x := (s2 + Rmin r1 r0) / 2); assert (H22 := H8 0%nat); +set (x := (s2 + Rmin r1 r0) / 2); assert (H22 := H8 0%nat); assert (H23 := H13 1%nat); simpl in H22; simpl in H23; rewrite <- (H22 (lt_O_Sn _) x). rewrite <- (H23 (lt_n_S _ _ (lt_O_Sn _)) x). @@ -703,7 +703,7 @@ case (Req_dec r r1); intro. right; assumption. left; cut (r1 <= s2). intro; unfold adapted_couple in H2, H; decompose [and] H; decompose [and] H2; - clear H H2; pose (x := (r + r1) / 2); assert (H18 := H14 0%nat); + clear H H2; set (x := (r + r1) / 2); assert (H18 := H14 0%nat); assert (H20 := H19 0%nat); unfold constant_D_eq, open_interval in H18, H20; simpl in H18; simpl in H20; rewrite <- (H18 (lt_O_Sn _) x). rewrite <- (H20 (lt_O_Sn _) x). @@ -1148,7 +1148,7 @@ apply lt_n_Sm_le; apply lt_n_S; assumption. apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H8; elim (lt_n_O _ H8). rewrite H0; assumption. -pose +set (I := fun j:nat => pos_Rl lf j <= pos_Rl (cons_ORlist lf lg) i /\ (j < Rlength lf)%nat); @@ -1395,7 +1395,7 @@ apply lt_n_Sm_le; apply lt_n_S; assumption. apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H13 in H8; elim (lt_n_O _ H8). rewrite H0; assumption. -pose +set (I := fun j:nat => pos_Rl lg j <= pos_Rl (cons_ORlist lf lg) i /\ (j < Rlength lg)%nat); @@ -1774,7 +1774,7 @@ reflexivity. assert (H4 : pos_Rl (cons r1 l) (pred (Rlength (cons r1 l))) = b). rewrite <- H1; reflexivity. elim (IHl r1 H2 H3 H4); intros g [H5 H6]. -pose +set (g' := fun x:R => match Rle_dec r1 x with | left _ => g x diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index 30f7be1f03..20382b0857 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -146,7 +146,7 @@ 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). -intros; pose (f := fun x:R => exp x - y); cut (f 0 <= 0). +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). @@ -560,7 +560,7 @@ Lemma derivable_pt_lim_ln : forall x:R, 0 < x -> derivable_pt_lim ln x (/ x). intros; assert (H0 := Dln x H); unfold D_in in H0; unfold limit1_in in H0; unfold limit_in in H0; simpl in H0; unfold R_dist in H0; unfold derivable_pt_lim in |- *; intros; elim (H0 _ H1); - intros; elim H2; clear H2; intros; pose (alp := Rmin x0 (x / 2)); + intros; elim H2; clear H2; intros; set (alp := Rmin x0 (x / 2)); assert (H4 : 0 < alp). unfold alp in |- *; unfold Rmin in |- *; case (Rle_dec x0 (x / 2)); intro. apply H2. diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index b123f1bb75..932e407732 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -267,7 +267,7 @@ unfold cv_infty in |- *. intro. case (total_order_T 0 M); intro. elim s; intro. -pose (N := up M). +set (N := up M). cut (0 <= N)%Z. intro. elim (IZN N H0); intros N0 H1. @@ -475,8 +475,8 @@ apply dicho_up_decreasing; assumption. assumption. right; reflexivity. 2: left; assumption. -pose (Vn := fun n:nat => dicho_lb x y (fun z:R => cond_positivity (f z)) n). -pose (Wn := fun n:nat => dicho_up x y (fun z:R => cond_positivity (f z)) n). +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). cut ((forall n:nat, 0 <= f (Wn n)) -> 0 <= f x0). intros. @@ -652,7 +652,7 @@ Qed. Lemma Rsqrt_exists : forall y:R, 0 <= y -> sigT (fun z:R => 0 <= z /\ y = Rsqr z). intros. -pose (f := fun x:R => Rsqr x - y). +set (f := fun x:R => Rsqr x - y). cut (f 0 <= 0). intro. cut (continuity f). diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index 75385b4248..4c9a94031d 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -64,7 +64,7 @@ Lemma interior_P3 : forall D:R -> Prop, open_set (interior D). intro; unfold open_set, interior in |- *; unfold neighbourhood in |- *; intros; elim H; intros. exists x0; unfold included in |- *; intros. -pose (del := x0 - Rabs (x - x1)). +set (del := x0 - Rabs (x - x1)). cut (0 < del). intro; exists (mkposreal del H2); intros. cut (included (disc x1 (mkposreal del H2)) (disc x x0)). @@ -108,7 +108,7 @@ Lemma adherence_P3 : forall D:R -> Prop, closed_set (adherence D). intro; unfold closed_set, adherence in |- *; unfold open_set, complementary, point_adherent in |- *; intros; - pose + set (P := fun V:R -> Prop => neighbourhood V x -> exists y : R, intersection_domain V D y); @@ -121,7 +121,7 @@ assert (H8 := H7 V0); cut (exists delta : posreal, (forall x:R, disc x1 delta x -> V0 x)). intro; assert (H10 := H8 H9); elim H4; assumption. cut (0 < x0 - Rabs (x - x1)). -intro; pose (del := mkposreal _ H9); exists del; intros; +intro; set (del := mkposreal _ H9); exists del; intros; unfold included in H5; apply H5; unfold disc in |- *; apply Rle_lt_trans with (Rabs (x2 - x1) + Rabs (x1 - x)). replace (x2 - x) with (x2 - x1 + (x1 - x)); [ apply Rabs_triang | ring ]. @@ -198,7 +198,7 @@ assert (H4 := H _ H2); assert (H5 := H0 _ H3); unfold intersection_domain in |- *; unfold neighbourhood in H4, H5; elim H4; clear H; intros del1 H; elim H5; clear H0; intros del2 H0; cut (0 < Rmin del1 del2). -intro; pose (del := mkposreal _ H6). +intro; set (del := mkposreal _ H6). exists del; unfold included in |- *; intros; unfold included in H, H0; unfold disc in H, H0, H7. split. @@ -228,7 +228,7 @@ elim H; intros; apply H1. unfold eq_Dom in |- *; split. unfold included, interior, disc in |- *; intros; cut (0 < del - Rabs (x - x0)). -intro; pose (del2 := mkposreal _ H3). +intro; set (del2 := mkposreal _ H3). exists del2; unfold included in |- *; intros. apply Rle_lt_trans with (Rabs (x1 - x0) + Rabs (x0 - x)). replace (x1 - x) with (x1 - x0 + (x0 - x)); [ apply Rabs_triang | ring ]. @@ -333,7 +333,7 @@ Theorem Rsepare : (exists W : R -> Prop, neighbourhood V x /\ neighbourhood W y /\ ~ (exists y : R, intersection_domain V W y)). -intros x y Hsep; pose (D := Rabs (x - y)). +intros x y Hsep; set (D := Rabs (x - y)). cut (0 < D / 2). intro; exists (disc x (mkposreal _ H)). exists (disc y (mkposreal _ H)); split. @@ -431,16 +431,16 @@ Qed. (**********) Lemma compact_P1 : forall X:R -> Prop, compact X -> bounded X. -intros; unfold compact in H; pose (D := fun x:R => True); - pose (g := fun x y:R => Rabs y < x); +intros; unfold compact in H; set (D := fun x:R => True); + set (g := fun x y:R => Rabs y < x); cut (forall x:R, (exists y : _, g x y) -> True); [ intro | intro; trivial ]. -pose (f0 := mkfamily D g H0); assert (H1 := H f0); +set (f0 := mkfamily D g H0); assert (H1 := H f0); cut (covering_open_set X f0). intro; assert (H3 := H1 H2); elim H3; intros D' H4; unfold covering_finite in H4; elim H4; intros; unfold family_finite in H6; unfold domain_finite in H6; elim H6; intros l H7; - unfold bounded in |- *; pose (r := MaxRlist l). + unfold bounded in |- *; set (r := MaxRlist l). exists (- r); exists r; intros. unfold covering in H5; assert (H9 := H5 _ H8); elim H9; intros; unfold subfamily in H10; simpl in H10; elim H10; intros; @@ -496,17 +496,17 @@ unfold included in |- *; unfold adherence in |- *; assert (H1 := classic (X x)); elim H1; clear H1; intro. assumption. cut (forall y:R, X y -> 0 < Rabs (y - x) / 2). -intro; pose (D := X); - pose (g := fun y z:R => Rabs (y - z) < Rabs (y - x) / 2 /\ D y); +intro; set (D := X); + set (g := fun y z:R => Rabs (y - z) < Rabs (y - x) / 2 /\ D y); cut (forall x:R, (exists y : _, g x y) -> D x). -intro; pose (f0 := mkfamily D g H3); assert (H4 := H f0); +intro; set (f0 := mkfamily D g H3); assert (H4 := H f0); cut (covering_open_set X f0). intro; assert (H6 := H4 H5); elim H6; clear H6; intros D' H6. unfold covering_finite in H6; decompose [and] H6; unfold covering, subfamily in H7; simpl in H7; unfold family_finite, subfamily in H8; simpl in H8; unfold domain_finite in H8; elim H8; clear H8; intros l H8; - pose (alp := MinRlist (AbsList l x)); cut (0 < alp). + set (alp := MinRlist (AbsList l x)); cut (0 < alp). intro; assert (H10 := H0 (disc x (mkposreal _ H9))); cut (neighbourhood (disc x (mkposreal alp H9)) x). intro; assert (H12 := H10 H11); elim H12; clear H12; intros y H12; @@ -596,7 +596,7 @@ Qed. Lemma compact_P3 : forall a b:R, compact (fun c:R => a <= c <= b). intros; case (Rle_dec a b); intro. unfold compact in |- *; intros; - pose + set (A := fun x:R => a <= x <= b /\ @@ -617,7 +617,7 @@ intro; elim H9; clear H9; intros x H9; elim H9; clear H9; intros; case (Req_dec m b); intro. rewrite H11 in H10; rewrite H11 in H8; unfold A in H9; elim H9; clear H9; intros; elim H12; clear H12; intros Dx H12; - pose (Db := fun x:R => Dx x \/ x = y0); exists Db; + set (Db := fun x:R => Dx x \/ x = y0); exists Db; unfold covering_finite in |- *; split. unfold covering in |- *; unfold covering_finite in H12; elim H12; clear H12; intros; unfold covering in H12; case (Rle_dec x0 x); @@ -663,7 +663,7 @@ intros _ H16; assert (H17 := H16 H15); simpl in H17; unfold intersection_domain in H17; split. elim H17; intros; assumption. unfold Db in |- *; left; elim H17; intros; assumption. -pose (m' := Rmin (m + eps / 2) b); cut (A m'). +set (m' := Rmin (m + eps / 2) b); cut (A m'). intro; elim H3; intros; unfold is_upper_bound in H13; assert (H15 := H13 m' H12); cut (m < m'). intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H15 H16)). @@ -689,7 +689,7 @@ assumption. elim H11; assumption. unfold m' in |- *; apply Rmin_r. unfold A in H9; elim H9; clear H9; intros; elim H12; clear H12; intros Dx H12; - pose (Db := fun x:R => Dx x \/ x = y0); exists Db; + set (Db := fun x:R => Dx x \/ x = y0); exists Db; unfold covering_finite in |- *; split. unfold covering in |- *; unfold covering_finite in H12; elim H12; clear H12; intros; unfold covering in H12; case (Rle_dec x0 x); @@ -759,7 +759,7 @@ intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H13 H14)). pattern m at 2 in |- *; rewrite <- Rplus_0_r; unfold Rminus in |- *; apply Rplus_lt_compat_l; apply Ropp_lt_cancel; rewrite Ropp_involutive; rewrite Ropp_0; apply (cond_pos eps). -pose (P := fun n:R => A n /\ m - eps < n <= m); +set (P := fun n:R => A n /\ m - eps < n <= m); assert (H12 := not_ex_all_not _ P H9); unfold P in H12; unfold is_upper_bound in |- *; intros; assert (H14 := not_and_or _ _ (H12 x)); elim H14; @@ -785,7 +785,7 @@ unfold A in |- *; split. split; [ right; reflexivity | apply r ]. unfold covering_open_set in H; elim H; clear H; intros; unfold covering in H; cut (a <= a <= b). -intro; elim (H _ H1); intros y0 H2; pose (D' := fun x:R => x = y0); exists D'; +intro; elim (H _ H1); intros y0 H2; set (D' := fun x:R => x = y0); exists D'; unfold covering_finite in |- *; split. unfold covering in |- *; simpl in |- *; intros; cut (x = a). intro; exists y0; split. @@ -812,11 +812,11 @@ Lemma compact_P4 : forall X F:R -> Prop, compact X -> closed_set F -> included F X -> compact F. unfold compact in |- *; intros; elim (classic (exists z : R, F z)); intro Hyp_F_NE. -pose (D := ind f0); pose (g := f f0); unfold closed_set in H0. -pose (g' := fun x y:R => f0 x y \/ complementary F y /\ D x). -pose (D' := D). +set (D := ind f0); set (g := f f0); unfold closed_set in H0. +set (g' := fun x y:R => f0 x y \/ complementary F y /\ D x). +set (D' := D). cut (forall x:R, (exists y : R, g' x y) -> D' x). -intro; pose (f' := mkfamily D' g' H3); cut (covering_open_set X f'). +intro; set (f' := mkfamily D' g' H3); cut (covering_open_set X f'). intro; elim (H _ H4); intros DX H5; exists DX. unfold covering_finite in |- *; unfold covering_finite in H5; elim H5; clear H5; intros. @@ -916,10 +916,10 @@ Lemma continuity_compact : (forall x:R, continuity_pt f x) -> compact X -> compact (image_dir f X). unfold compact in |- *; intros; unfold covering_open_set in H1. elim H1; clear H1; intros. -pose (D := ind f1). -pose (g := fun x y:R => image_rec f0 (f1 x) y). +set (D := ind f1). +set (g := fun x y:R => image_rec f0 (f1 x) y). cut (forall x:R, (exists y : R, g x y) -> D x). -intro; pose (f' := mkfamily D g H3). +intro; set (f' := mkfamily D g H3). cut (covering_open_set X f'). intro; elim (H0 f' H4); intros D' H5; exists D'. unfold covering_finite in H5; elim H5; clear H5; intros; @@ -961,7 +961,7 @@ Lemma prolongement_C0 : exists g : R -> R, continuity g /\ (forall c:R, a <= c <= b -> g c = f c). intros; elim H; intro. -pose +set (h := fun x:R => match Rle_dec x a with @@ -1363,11 +1363,11 @@ Lemma compact_P6 : intersection_vide_in X g -> exists D : R -> Prop, intersection_vide_finite_in X (subfamily g D). intros X H Hyp g H0 H1. -pose (D' := ind g). -pose (f' := fun x y:R => complementary (g x) y /\ D' x). +set (D' := ind g). +set (f' := fun x y:R => complementary (g x) y /\ D' x). assert (H2 : forall x:R, (exists y : R, f' x y) -> D' x). intros; elim H2; intros; unfold f' in H3; elim H3; intros; assumption. -pose (f0 := mkfamily D' f' H2). +set (f0 := mkfamily D' f' H2). unfold compact in H; assert (H3 : covering_open_set X f0). unfold covering_open_set in |- *; split. unfold covering in |- *; intros; unfold intersection_vide_in in H1; @@ -1441,8 +1441,8 @@ intro; elim H1; intros; exists x; elim (ValAdh_un_prop un x); intros; apply (H4 H2). assert (H1 : exists z : R, X z). exists (un 0%nat); apply H0. -pose (D := fun x:R => exists n : nat, x = INR n). -pose +set (D := fun x:R => exists n : nat, x = INR n). +set (g := fun x:R => adherence (fun y:R => (exists p : nat, y = un p /\ x <= INR p) /\ D x)). @@ -1454,7 +1454,7 @@ unfold neighbourhood in |- *; exists (mkposreal _ Rlt_0_1); unfold included in |- *; trivial. elim (H3 _ H4); intros; unfold intersection_domain in H5; decompose [and] H5; assumption. -pose (f0 := mkfamily D g H2). +set (f0 := mkfamily D g H2). assert (H3 := compact_P6 X H H1 f0). elim (classic (exists l : R, ValAdh_un un l)); intro. assumption. @@ -1465,7 +1465,7 @@ elim H7; intros SF H8; unfold intersection_vide_finite_in in H8; elim H8; clear H8; intros; unfold intersection_vide_in in H8; elim (H8 0); intros _ H10; elim H10; unfold family_finite in H9; unfold domain_finite in H9; elim H9; clear H9; intros l H9; - pose (r := MaxRlist l); cut (D r). + set (r := MaxRlist l); cut (D r). intro; unfold D in H11; elim H11; intros; exists (un x); unfold intersection_family in |- *; simpl in |- *; unfold intersection_domain in |- *; intros; split. @@ -1583,7 +1583,7 @@ elim X_enc; clear X_enc; intros m X_enc; elim X_enc; clear X_enc; assert (H1 : forall t:posreal, 0 < t / 2). intro; unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ apply (cond_pos t) | apply Rinv_0_lt_compat; prove_sup0 ]. -pose +set (g := fun x y:R => X x /\ @@ -1597,7 +1597,7 @@ pose assert (H2 : forall x:R, (exists y : R, g x y) -> X x). intros; elim H2; intros; unfold g in H3; elim H3; clear H3; intros H3 _; apply H3. -pose (f' := mkfamily X g H2); unfold compact in H0; +set (f' := mkfamily X g H2); unfold compact in H0; assert (H3 : covering_open_set X f'). unfold covering_open_set in |- *; split. unfold covering in |- *; intros; exists x; simpl in |- *; unfold g in |- *; @@ -1607,7 +1607,7 @@ assert (H4 := H _ H3); unfold continuity_pt in H4; unfold continue_in in H4; unfold limit1_in in H4; unfold limit_in in H4; simpl in H4; unfold R_dist in H4; elim (H4 (eps / 2) (H1 eps)); intros; - pose + set (E := fun zeta:R => 0 < zeta <= M - m /\ @@ -1675,7 +1675,7 @@ apply H4. split. elim H5; intros; apply H8. apply H7. -pose (d := x1 / 2 - Rabs (x0 - x)); assert (H7 : 0 < d). +set (d := x1 / 2 - Rabs (x0 - x)); assert (H7 : 0 < d). unfold d in |- *; apply Rlt_Rminus; elim H5; clear H5; intros; unfold disc in H7; apply H7. exists (mkposreal _ H7); unfold included in |- *; intros; split. @@ -1716,7 +1716,7 @@ intros; (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\ included (g x) (fun z:R => Rabs (z - x) < del / 2)) H6); elim H7; clear H7; intros l' H7; elim H7; clear H7; - intros; pose (D := MinRlist l'); cut (0 < D / 2). + intros; set (D := MinRlist l'); cut (0 < D / 2). intro; exists (mkposreal _ H9); intros; assert (H13 := H4 _ H10); elim H13; clear H13; intros xi H13; assert (H14 : In xi l). unfold g in H13; decompose [and] H13; elim (H5 xi); intros; apply H14; split; @@ -1760,7 +1760,7 @@ unfold Rdiv in |- *; apply Rmult_lt_0_compat; apply H15 | apply Rinv_0_lt_compat; prove_sup0 ]. intros; elim (H5 x); intros; elim (H8 H6); intros; - pose + set (E := fun zeta:R => 0 < zeta <= M - m /\ diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 6cba456fb5..3ff1f07152 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -343,7 +343,7 @@ Definition cos_ub (a:R) : R := cos_approx a 4. Lemma sin_lb_gt_0 : forall a:R, 0 < a -> a <= PI / 2 -> 0 < sin_lb a. intros. unfold sin_lb in |- *; unfold sin_approx in |- *; unfold sin_term in |- *. -pose (Un := fun i:nat => a ^ (2 * i + 1) / INR (fact (2 * i + 1))). +set (Un := fun i:nat => a ^ (2 * i + 1) / INR (fact (2 * i + 1))). replace (sum_f_R0 (fun i:nat => (-1) ^ i * (a ^ (2 * i + 1) / INR (fact (2 * i + 1)))) 3) @@ -407,7 +407,7 @@ apply Rmult_lt_compat_l. apply lt_INR_0; apply neq_O_lt. assert (H2 := fact_neq_0 (2 * n + 1)). red in |- *; intro; elim H2; symmetry in |- *; assumption. -do 2 rewrite S_INR; rewrite plus_INR; rewrite mult_INR; pose (x := INR n); +do 2 rewrite S_INR; rewrite plus_INR; rewrite mult_INR; set (x := INR n); unfold INR in |- *. replace ((2 * x + 1 + 1 + 1) * (2 * x + 1 + 1)) with (4 * x * x + 10 * x + 6); [ idtac | ring ]. diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index c1ffc68ea9..098d4c7301 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -61,7 +61,7 @@ cut a + sum_f_R0 (fun i:nat => sin_term a (S i)) (pred (2 * n + 1)) <= sin a /\ sin a <= a + sum_f_R0 (fun i:nat => sin_term a (S i)) (pred (2 * (n + 1)))). intro; apply H1. -pose (Un := fun n:nat => a ^ (2 * S n + 1) / INR (fact (2 * S n + 1))). +set (Un := fun n:nat => a ^ (2 * S n + 1) / INR (fact (2 * S n + 1))). replace (pred (2 * n + 1)) with (2 * n)%nat. replace (pred (2 * (n + 1))) with (S (2 * n)). replace (sum_f_R0 (fun i:nat => sin_term a (S i)) (2 * n)) with @@ -256,7 +256,7 @@ cut cos a0 <= 1 + sum_f_R0 (fun i:nat => cos_term a0 (S i)) (pred (2 * (n0 + 1)))). intro; apply H2. -pose (Un := fun n:nat => a0 ^ (2 * S n) / INR (fact (2 * S n))). +set (Un := fun n:nat => a0 ^ (2 * S n) / INR (fact (2 * S n))). replace (pred (2 * n0 + 1)) with (2 * n0)%nat. replace (pred (2 * (n0 + 1))) with (S (2 * n0)). replace (sum_f_R0 (fun i:nat => cos_term a0 (S i)) (2 * n0)) with diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index ca0eb33dc6..dc20ff7dc7 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -121,7 +121,7 @@ Qed. (**********) Lemma continuity_cos : continuity cos. -pose (fn := fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N)) * x ^ (2 * N)). +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 cv; cut (forall n:nat, continuity (fn n)). @@ -299,12 +299,12 @@ Qed. (* (sin h)/h -> 1 when h -> 0 *) Lemma derivable_pt_lim_sin_0 : derivable_pt_lim sin 0 1. unfold derivable_pt_lim in |- *; intros. -pose +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 cv. -pose (r := mkposreal _ Rlt_0_1). +set (r := mkposreal _ Rlt_0_1). cut (CVN_r fn r). intro; cut (forall (n:nat) (y:R), Boule 0 r y -> continuity_pt (fn n) y). intro; cut (Boule 0 r 0). @@ -393,7 +393,7 @@ intro; unfold continuity_pt in H3; unfold continue_in in H3; cut (0 < eps / 2); [ intro | assumption ]. elim (H3 _ H4); intros del_c H5. cut (0 < Rmin del del_c). -intro; pose (delta := mkposreal _ H6). +intro; set (delta := mkposreal _ H6). exists delta; intros. rewrite Rplus_0_l; replace (cos h - cos 0) with (-2 * Rsqr (sin (h / 2))). unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r. @@ -498,7 +498,7 @@ cut (0 < eps / 2); [ apply H1 | apply Rinv_0_lt_compat; prove_sup0 ] ]. elim (H0 _ H2); intros alp1 H3. elim (H _ H2); intros alp2 H4. -pose (alp := Rmin alp1 alp2). +set (alp := Rmin alp1 alp2). cut (0 < alp). intro; exists (mkposreal _ H5); intros. replace ((sin (x + h) - sin x) / h - cos x) with diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 4f69514299..3f976cee90 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -493,7 +493,7 @@ 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. intros. -pose (P := fun k:nat => Rabs (majorant Un pr - Un k) < eps). +set (P := fun k:nat => Rabs (majorant Un pr - Un k) < eps). unfold P in |- *. cut ((exists k : nat, P k) -> @@ -561,7 +561,7 @@ 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. intros. -pose (P := fun k:nat => Rabs (minorant Un pr - Un k) < eps). +set (P := fun k:nat => Rabs (minorant Un pr - Un k) < eps). unfold P in |- *. cut ((exists k : nat, P k) -> @@ -639,7 +639,7 @@ intros; cut (0 < eps / 2); [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. elim (H (eps / 2) H2); intros. elim (H0 (eps / 2) H2); intros. -pose (N := max x x0). +set (N := max x x0). apply Rle_lt_trans with (Rabs (l1 - Un N) + Rabs (Un N - l2)). replace (l1 - l2) with (l1 - Un N + (Un N - l2)); [ apply Rabs_triang | ring ]. @@ -660,7 +660,7 @@ cut (0 < eps / 2); [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. elim (H (eps / 2) H2); intros. elim (H0 (eps / 2) H2); intros. -pose (N := max x x0). +set (N := max x x0). exists N; intros. replace (An n + Bn n - (l1 + l2)) with (An n - l1 + (Bn n - l2)); [ idtac | ring ]. @@ -799,7 +799,7 @@ unfold Un_cv in H; unfold R_dist in H; unfold Un_cv in H0; unfold R_dist in H0. elim (H (eps / (2 * Rabs l2)) H8); intros N1 H9. elim (H0 (eps / (2 * M)) H6); intros N2 H10. -pose (N := max N1 N2). +set (N := max N1 N2). exists N; intros. apply Rle_lt_trans with (Rabs (An n * Bn n - An n * l2) + Rabs (An n * l2 - l1 * l2)). @@ -997,7 +997,7 @@ right; assumption. cut (0 < Un n - l). intro; unfold Un_cv in H0; unfold R_dist in H0. elim (H0 (Un n - l) H1); intros N1 H2. -pose (N := max n N1). +set (N := max n N1). cut (Un n - l <= Un N - l). intro; cut (Un N - l < Un n - l). intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H3 H4)). @@ -1111,9 +1111,9 @@ rewrite H1; unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_R0; rewrite pow_ne_zero; [ unfold Rdiv in |- *; rewrite Rmult_0_l; rewrite Rabs_R0; assumption | red in |- *; intro; rewrite H3 in H2; elim (le_Sn_n _ H2) ]. -assert (H2 := Rabs_pos_lt x H1); pose (M := up (Rabs x)); cut (0 <= M)%Z. +assert (H2 := Rabs_pos_lt x H1); set (M := up (Rabs x)); cut (0 <= M)%Z. intro; elim (IZN M H3); intros M_nat H4. -pose (Un := fun n:nat => Rabs x ^ (M_nat + n) / INR (fact (M_nat + n))). +set (Un := fun n:nat => Rabs x ^ (M_nat + n) / INR (fact (M_nat + n))). cut (Un_cv Un 0); unfold Un_cv in |- *; unfold R_dist in |- *; intros. elim (H5 eps H0); intros N H6. exists (M_nat + N)%nat; intros; @@ -1130,7 +1130,7 @@ apply le_plus_l. assumption. apply le_plus_minus; apply le_trans with (M_nat + N)%nat; [ apply le_plus_l | assumption ]. -pose (Vn := fun n:nat => Rabs x * (Un 0%nat / INR (S n))). +set (Vn := fun n:nat => Rabs x * (Un 0%nat / INR (S n))). cut (1 <= M_nat)%nat. intro; cut (forall n:nat, 0 < Un n). intro; cut (Un_decreasing Un). @@ -1195,7 +1195,7 @@ elim s; intro. exists 0%nat; intros. apply Rlt_trans with 0; [ assumption | apply lt_INR_0; apply lt_O_Sn ]. exists 0%nat; intros; rewrite b; apply lt_INR_0; apply lt_O_Sn. -pose (M0_z := up M0). +set (M0_z := up M0). assert (H10 := archimed M0). cut (0 <= M0_z)%Z. intro; elim (IZN _ H11); intros M0_nat H12. diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index 2c035cf837..602cd871b4 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -281,7 +281,7 @@ assert (H5 := cv_infty_cv_R0 _ H4 H1); assert (H6 : 0 < eps / 2)... unfold Rdiv in |- *; apply Rmult_lt_0_compat... apply Rinv_0_lt_compat; prove_sup... elim (H _ H6); clear H; intros N1 H; - pose (C := Rabs (sum_f_R0 (fun k:nat => An k * (Bn k - l)) N1)); + set (C := Rabs (sum_f_R0 (fun k:nat => An k * (Bn k - l)) N1)); assert (H7 : exists N : nat, @@ -309,7 +309,7 @@ ring... discrR... apply Rabs_no_R0... apply Rabs_no_R0... -elim H7; clear H7; intros N2 H7; pose (N := max N1 N2); exists (S N); intros; +elim H7; clear H7; intros N2 H7; set (N := max N1 N2); exists (S N); intros; unfold R_dist in |- *; replace (sum_f_R0 (fun k:nat => An k * Bn k) n / sum_f_R0 An n - l) with (sum_f_R0 (fun k:nat => An k * (Bn k - l)) n / sum_f_R0 An n)... @@ -375,7 +375,7 @@ Lemma Cesaro_1 : forall (An:nat -> R) (l:R), Un_cv An l -> Un_cv (fun n:nat => sum_f_R0 An (pred n) / INR n) l. Proof with trivial. -intros Bn l H; pose (An := fun _:nat => 1)... +intros Bn l H; set (An := fun _:nat => 1)... assert (H0 : forall n:nat, 0 < An n)... intro; unfold An in |- *; apply Rlt_0_1... assert (H1 : forall n:nat, 0 < sum_f_R0 An n)... @@ -385,7 +385,7 @@ unfold cv_infty in |- *; intro; case (Rle_dec M 0); intro... exists 0%nat; intros; apply Rle_lt_trans with 0... assert (H2 : 0 < M)... auto with real... -clear n; pose (m := up M); elim (archimed M); intros; +clear n; set (m := up M); elim (archimed M); intros; assert (H5 : (0 <= m)%Z)... apply le_IZR; unfold m in |- *; simpl in |- *; left; apply Rlt_trans with M... elim (IZN _ H5); intros; exists x; intros; unfold An in |- *; rewrite sum_cte; diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index def3cd0a4b..a4ec84154c 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -104,7 +104,7 @@ unfold continuity_pt in |- *; unfold continue_in in |- *; unfold limit1_in in |- *; unfold limit_in in |- *; unfold dist in |- *; simpl in |- *; unfold R_dist in |- *; intros. -pose (alpha := Rmin eps 1). +set (alpha := Rmin eps 1). exists alpha; intros. split. unfold alpha in |- *; unfold Rmin in |- *; case (Rle_dec eps 1); intro. @@ -131,7 +131,7 @@ unfold continuity_pt in |- *; unfold continue_in in |- *; cut (0 < eps / sqrt x). intro; elim (H0 _ H2); intros alp_1 H3. elim H3; intros. -pose (alpha := alp_1 * x). +set (alpha := alp_1 * x). exists (Rmin alpha x); intros. split. change (0 < Rmin alpha x) in |- *; unfold Rmin in |- *; @@ -228,7 +228,7 @@ Qed. (* sqrt is derivable for all x>0 *) Lemma derivable_pt_lim_sqrt : forall x:R, 0 < x -> derivable_pt_lim sqrt x (/ (2 * sqrt x)). -intros; pose (g := fun h:R => sqrt x + sqrt (x + h)). +intros; set (g := fun h:R => sqrt x + sqrt (x + h)). cut (continuity_pt g 0). intro; cut (g 0 <> 0). intro; assert (H2 := continuity_pt_inv g 0 H0 H1). @@ -237,7 +237,7 @@ unfold derivable_pt_lim in |- *; intros; unfold continuity_pt in H2; unfold limit_in in H2; simpl in H2; unfold R_dist in H2. elim (H2 eps H3); intros alpha H4. elim H4; intros. -pose (alpha1 := Rmin alpha x). +set (alpha1 := Rmin alpha x). cut (0 < alpha1). intro; exists (mkposreal alpha1 H7); intros. replace ((sqrt (x + h) - sqrt x) / h) with (/ (sqrt x + sqrt (x + h))). diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index 1b1cf27d20..afe21b8d41 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -201,4 +201,4 @@ Proof. exact Z_lt_rec. Qed. -End Efficient_Rec.
\ No newline at end of file +End Efficient_Rec. |