diff options
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/AltSeries.v | 58 | ||||
| -rw-r--r-- | theories/Reals/Cos_plus.v | 8 | ||||
| -rw-r--r-- | theories/Reals/Exp_prop.v | 2 | ||||
| -rw-r--r-- | theories/Reals/RIneq.v | 47 | ||||
| -rw-r--r-- | theories/Reals/R_Ifp.v | 35 | ||||
| -rw-r--r-- | theories/Reals/Ranalysis2.v | 5 | ||||
| -rw-r--r-- | theories/Reals/RiemannInt_SF.v | 9 | ||||
| -rw-r--r-- | theories/Reals/Rlimit.v | 35 | ||||
| -rw-r--r-- | theories/Reals/Rpower.v | 2 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo1.v | 294 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo_alt.v | 63 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo_def.v | 34 | ||||
| -rw-r--r-- | theories/Reals/SeqProp.v | 2 |
13 files changed, 172 insertions, 422 deletions
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index c3ab8edc5..17ffc0fe3 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -339,51 +339,24 @@ Proof. symmetry ; apply S_pred with 0%nat. assumption. apply Rle_lt_trans with (/ INR (2 * N)). - apply Rmult_le_reg_l with (INR (2 * N)). + apply Rinv_le_contravar. rewrite mult_INR; apply Rmult_lt_0_compat; [ simpl; prove_sup0 | apply lt_INR_0; assumption ]. - rewrite <- Rinv_r_sym. - apply Rmult_le_reg_l with (INR (2 * n)). - rewrite mult_INR; apply Rmult_lt_0_compat; - [ simpl; prove_sup0 | apply lt_INR_0; assumption ]. - rewrite (Rmult_comm (INR (2 * n))); rewrite Rmult_assoc; - rewrite <- Rinv_l_sym. - do 2 rewrite Rmult_1_r; apply le_INR. - apply (fun m n p:nat => mult_le_compat_l p n m); assumption. - replace n with (S (pred n)). - apply not_O_INR; discriminate. - symmetry ; apply S_pred with 0%nat. - assumption. - replace N with (S (pred N)). - apply not_O_INR; discriminate. - symmetry ; apply S_pred with 0%nat. - assumption. + apply le_INR. + now apply mult_le_compat_l. rewrite mult_INR. - rewrite Rinv_mult_distr. - replace (INR 2) with 2; [ idtac | reflexivity ]. - apply Rmult_lt_reg_l with 2. - prove_sup0. - rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ idtac | discrR ]. - rewrite Rmult_1_l; apply Rmult_lt_reg_l with (INR N). - apply lt_INR_0; assumption. - rewrite <- Rinv_r_sym. - apply Rmult_lt_reg_l with (/ (2 * eps)). - apply Rinv_0_lt_compat; assumption. - rewrite Rmult_1_r; - replace (/ (2 * eps) * (INR N * (2 * eps))) with - (INR N * (2 * eps * / (2 * eps))); [ idtac | ring ]. - rewrite <- Rinv_r_sym. - rewrite Rmult_1_r; replace (INR N) with (IZR (Z.of_nat N)). - rewrite <- H4. - elim H1; intros; assumption. - symmetry ; apply INR_IZR_INZ. - apply prod_neq_R0; - [ discrR | red; intro; rewrite H8 in H; elim (Rlt_irrefl _ H) ]. - apply not_O_INR. - red; intro; rewrite H8 in H5; elim (lt_irrefl _ H5). - replace (INR 2) with 2; [ discrR | reflexivity ]. - apply not_O_INR. - red; intro; rewrite H8 in H5; elim (lt_irrefl _ H5). + apply Rmult_lt_reg_l with (INR N / eps). + apply Rdiv_lt_0_compat with (2 := H). + now apply (lt_INR 0). + replace (_ */ _) with (/(2 * eps)). + replace (_ / _ * _) with (INR N). + rewrite INR_IZR_INZ. + now rewrite <- H4. + field. + now apply Rgt_not_eq. + simpl (INR 2); field; split. + now apply Rgt_not_eq, (lt_INR 0). + now apply Rgt_not_eq. apply Rle_ge; apply PI_tg_pos. apply lt_le_trans with N; assumption. elim H1; intros H5 _. @@ -395,7 +368,6 @@ Proof. elim (Rlt_irrefl _ (Rlt_trans _ _ _ H6 H5)). elim (lt_n_O _ H6). apply le_IZR. - simpl. left; apply Rlt_trans with (/ (2 * eps)). apply Rinv_0_lt_compat; assumption. elim H1; intros; assumption. diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v index b14d807d2..eb4a3b804 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -289,11 +289,9 @@ Proof. apply INR_fact_lt_0. rewrite <- Rinv_r_sym. rewrite Rmult_1_r. - replace 1 with (INR 1). - apply le_INR. + apply (le_INR 1). apply lt_le_S. apply INR_lt; apply INR_fact_lt_0. - reflexivity. apply INR_fact_neq_0. apply Rmult_le_reg_l with (INR (fact (S (N + n)))). apply INR_fact_lt_0. @@ -576,11 +574,9 @@ Proof. apply INR_fact_lt_0. rewrite <- Rinv_r_sym. rewrite Rmult_1_r. - replace 1 with (INR 1). - apply le_INR. + apply (le_INR 1). apply lt_le_S. apply INR_lt; apply INR_fact_lt_0. - reflexivity. apply INR_fact_neq_0. apply Rmult_le_reg_l with (INR (fact (S (S (N + n))))). apply INR_fact_lt_0. diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index e9de24898..76f4e1449 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -532,7 +532,7 @@ Proof. apply Rmult_le_reg_l with (INR (fact (div2 (pred n)))). apply INR_fact_lt_0. rewrite Rmult_1_r; rewrite <- Rinv_r_sym. - replace 1 with (INR 1); [ apply le_INR | reflexivity ]. + apply (le_INR 1). apply lt_le_S. apply INR_lt. apply INR_fact_lt_0. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 8bebb5237..7e1cc3e03 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1629,7 +1629,7 @@ Hint Resolve lt_INR: real. Lemma lt_1_INR : forall n:nat, (1 < n)%nat -> 1 < INR n. Proof. - intros; replace 1 with (INR 1); auto with real. + apply lt_INR. Qed. Hint Resolve lt_1_INR: real. @@ -1653,17 +1653,16 @@ Hint Resolve pos_INR: real. Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat. Proof. - double induction n m; intros. - simpl; exfalso; apply (Rlt_irrefl 0); auto. - auto with arith. - generalize (pos_INR (S n0)); intro; cut (INR 0 = 0); - [ intro H2; rewrite H2 in H0; idtac | simpl; trivial ]. - generalize (Rle_lt_trans 0 (INR (S n0)) 0 H1 H0); intro; exfalso; - apply (Rlt_irrefl 0); auto. - do 2 rewrite S_INR in H1; cut (INR n1 < INR n0). - intro H2; generalize (H0 n0 H2); intro; auto with arith. - apply (Rplus_lt_reg_l 1 (INR n1) (INR n0)). - rewrite Rplus_comm; rewrite (Rplus_comm 1 (INR n0)); trivial. + intros n m. revert n. + induction m ; intros n H. + - elim (Rlt_irrefl 0). + apply Rle_lt_trans with (2 := H). + apply pos_INR. + - destruct n as [|n]. + apply Nat.lt_0_succ. + apply lt_n_S, IHm. + rewrite 2!S_INR in H. + apply Rplus_lt_reg_r with (1 := H). Qed. Hint Resolve INR_lt: real. @@ -1707,14 +1706,10 @@ Hint Resolve not_INR: real. Lemma INR_eq : forall n m:nat, INR n = INR m -> n = m. Proof. - intros; case (le_or_lt n m); intros H1. - case (le_lt_or_eq _ _ H1); intros H2; auto. - cut (n <> m). - intro H3; generalize (not_INR n m H3); intro H4; exfalso; auto. - omega. - symmetry ; cut (m <> n). - intro H3; generalize (not_INR m n H3); intro H4; exfalso; auto. - omega. + intros n m HR. + destruct (dec_eq_nat n m) as [H|H]. + exact H. + now apply not_INR in H. Qed. Hint Resolve INR_eq: real. @@ -1728,7 +1723,8 @@ Hint Resolve INR_le: real. Lemma not_1_INR : forall n:nat, n <> 1%nat -> INR n <> 1. Proof. - replace 1 with (INR 1); auto with real. + intros n. + apply not_INR. Qed. Hint Resolve not_1_INR: real. @@ -1905,8 +1901,8 @@ Qed. (**********) Lemma le_IZR_R1 : forall n:Z, IZR n <= 1 -> (n <= 1)%Z. Proof. - pattern 1 at 1; replace 1 with (IZR 1); intros; auto. - apply le_IZR; trivial. + intros n. + apply le_IZR. Qed. (**********) @@ -1935,7 +1931,7 @@ Proof. intros z [H1 H2]. apply Z.le_antisymm. apply Z.lt_succ_r; apply lt_IZR; trivial. - replace 0%Z with (Z.succ (-1)); trivial. + change 0%Z with (Z.succ (-1)). apply Z.le_succ_l; apply lt_IZR; trivial. Qed. @@ -2012,8 +2008,7 @@ Lemma double_var : forall r1, r1 = r1 / 2 + r1 / 2. Proof. intro; rewrite <- double; unfold Rdiv; rewrite <- Rmult_assoc; symmetry ; apply Rinv_r_simpl_m. - replace 2 with (INR 2); - [ apply not_0_INR; discriminate | unfold INR; ring ]. + now apply not_0_IZR. Qed. Lemma R_rm : ring_morph diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index e9b1762af..46583d374 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -42,28 +42,23 @@ Qed. Lemma up_tech : forall (r:R) (z:Z), IZR z <= r -> r < IZR (z + 1) -> (z + 1)%Z = up r. Proof. - intros; generalize (Rplus_le_compat_l 1 (IZR z) r H); intro; clear H; - rewrite (Rplus_comm 1 (IZR z)) in H1; rewrite (Rplus_comm 1 r) in H1; - cut (1 = IZR 1); auto with zarith real. - intro; generalize H1; pattern 1 at 1; rewrite H; intro; clear H H1; - rewrite <- (plus_IZR z 1) in H2; apply (tech_up r (z + 1)); - auto with zarith real. + intros. + apply tech_up with (1 := H0). + rewrite plus_IZR. + now apply Rplus_le_compat_r. Qed. (**********) Lemma fp_R0 : frac_part 0 = 0. Proof. - unfold frac_part; unfold Int_part; elim (archimed 0); intros; - unfold Rminus; elim (Rplus_ne (- IZR (up 0 - 1))); - intros a b; rewrite b; clear a b; rewrite <- Z_R_minus; - cut (up 0 = 1%Z). - intro; rewrite H1; - rewrite (Rminus_diag_eq (IZR 1) (IZR 1) (eq_refl (IZR 1))); - apply Ropp_0. - elim (archimed 0); intros; clear H2; unfold Rgt in H1; - rewrite (Rminus_0_r (IZR (up 0))) in H0; generalize (lt_O_IZR (up 0) H1); - intro; clear H1; generalize (le_IZR_R1 (up 0) H0); - intro; clear H H0; omega. + unfold frac_part, Int_part. + replace (up 0) with 1%Z. + now rewrite <- minus_IZR. + destruct (archimed 0) as [H1 H2]. + apply lt_IZR in H1. + rewrite <- minus_IZR in H2. + apply le_IZR in H2. + omega. Qed. (**********) @@ -229,8 +224,7 @@ Proof. rewrite (Rplus_opp_r (IZR (Int_part r1) - IZR (Int_part r2))) in H; elim (Rplus_ne (r1 - r2)); intros a b; rewrite b in H; clear a b; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0; - rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H; - cut (1 = IZR 1); auto with zarith real. + rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H. rewrite <- (plus_IZR (Int_part r1 - Int_part r2) 1) in H; generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2) H0 H); intros; clear H H0; unfold Int_part at 1; @@ -497,8 +491,7 @@ Proof. in H0; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H0; elim (Rplus_ne (IZR (Int_part r1) + IZR (Int_part r2))); intros a b; rewrite a in H0; clear a b; elim (Rplus_ne (r1 + r2)); - intros a b; rewrite b in H0; clear a b; cut (1 = IZR 1); - auto with zarith real. + intros a b; rewrite b in H0; clear a b. rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0; rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H1; rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H1; diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 27cb356a0..b749da0d2 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -423,10 +423,7 @@ Proof. intro; rewrite H11 in H10; assert (H12 := Rmult_lt_compat_l 2 _ _ Hyp H10); rewrite Rmult_1_r in H12; rewrite <- Rinv_r_sym in H12; [ idtac | discrR ]. - cut (IZR 1 < IZR 2). - unfold IZR; unfold INR, Pos.to_nat; simpl; intro; - elim (Rlt_irrefl 1 (Rlt_trans _ _ _ H13 H12)). - apply IZR_lt; omega. + now apply lt_IZR in H12. unfold Rabs; case (Rcase_abs (/ 2)) as [Hlt|Hge]. assert (Hyp : 0 < 2). prove_sup0. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 7885d697f..af7cbb940 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -83,11 +83,10 @@ Proof. cut (x = INR (pred x0)). intro H19; rewrite H19; apply le_INR; apply lt_le_S; apply INR_lt; rewrite H18; rewrite <- H19; assumption. - 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 ] ]. + rewrite H10; rewrite H8; rewrite <- INR_IZR_INZ; + rewrite <- (minus_INR _ 1). + apply f_equal; + case x0; [ reflexivity | intro; apply sym_eq, minus_n_O ]. 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)). diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index f07140752..843aa2752 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -29,59 +29,28 @@ Qed. Lemma eps2 : forall eps:R, eps * / 2 + eps * / 2 = eps. Proof. intro esp. - assert (H := double_var esp). - unfold Rdiv in H. - symmetry ; exact H. + apply eq_sym, double_var. Qed. (*********) Lemma eps4 : forall eps:R, eps * / (2 + 2) + eps * / (2 + 2) = eps * / 2. Proof. intro eps. - replace (2 + 2) with 4. - pattern eps at 3; rewrite double_var. - rewrite (Rmult_plus_distr_r (eps / 2) (eps / 2) (/ 2)). - unfold Rdiv. - repeat rewrite Rmult_assoc. - rewrite <- Rinv_mult_distr. - reflexivity. - discrR. - discrR. - ring. + field. Qed. (*********) Lemma Rlt_eps2_eps : forall eps:R, eps > 0 -> eps * / 2 < eps. Proof. intros. - pattern eps at 2; rewrite <- Rmult_1_r. - repeat rewrite (Rmult_comm eps). - apply Rmult_lt_compat_r. - exact H. - apply Rmult_lt_reg_l with 2. fourier. - rewrite Rmult_1_r; rewrite <- Rinv_r_sym. - fourier. - discrR. Qed. (*********) Lemma Rlt_eps4_eps : forall eps:R, eps > 0 -> eps * / (2 + 2) < eps. Proof. intros. - replace (2 + 2) with 4. - pattern eps at 2; rewrite <- Rmult_1_r. - repeat rewrite (Rmult_comm eps). - apply Rmult_lt_compat_r. - exact H. - apply Rmult_lt_reg_l with 4. - replace 4 with 4. - apply Rmult_lt_0_compat; fourier. - ring. - rewrite Rmult_1_r; rewrite <- Rinv_r_sym. fourier. - discrR. - ring. Qed. (*********) diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index f62ed2a6c..b8040bb4f 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -456,7 +456,7 @@ Proof. unfold Rpower; auto. rewrite Rpower_mult. rewrite Rinv_l. - replace 1 with (INR 1); auto. + change 1 with (INR 1). repeat rewrite Rpower_pow; simpl. pattern x at 1; rewrite <- (sqrt_sqrt x (Rlt_le _ _ H)). ring. diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v index 17b9677ef..5a999eebe 100644 --- a/theories/Reals/Rtrigo1.v +++ b/theories/Reals/Rtrigo1.v @@ -694,16 +694,15 @@ Proof. rewrite <- Rinv_l_sym. do 2 rewrite Rmult_1_r; apply Rle_lt_trans with (INR (fact (2 * n + 1)) * 4). apply Rmult_le_compat_l. - replace 0 with (INR 0); [ idtac | reflexivity ]; apply le_INR; apply le_O_n. - simpl in |- *; rewrite Rmult_1_r; replace 4 with (Rsqr 2); - [ idtac | ring_Rsqr ]; replace (a * a) with (Rsqr a); - [ idtac | reflexivity ]; apply Rsqr_incr_1. + apply pos_INR. + simpl in |- *; rewrite Rmult_1_r; change 4 with (Rsqr 2); + apply Rsqr_incr_1. apply Rle_trans with (PI / 2); [ assumption | unfold Rdiv in |- *; apply Rmult_le_reg_l with 2; [ prove_sup0 | rewrite <- Rmult_assoc; rewrite Rinv_r_simpl_m; - [ replace 4 with 4; [ apply PI_4 | ring ] | discrR ] ] ]. + [ apply PI_4 | discrR ] ] ]. left; assumption. left; prove_sup0. rewrite H1; replace (2 * n + 1 + 2)%nat with (S (S (2 * n + 1))). @@ -725,9 +724,8 @@ Proof. cut (0 <= x). intro; apply Rplus_le_le_0_compat; repeat apply Rmult_le_pos; assumption || left; prove_sup. - unfold x in |- *; replace 0 with (INR 0); - [ apply le_INR; apply le_O_n | reflexivity ]. - prove_sup0. + apply pos_INR. + now apply IZR_lt. ring. apply INR_fact_neq_0. apply INR_fact_neq_0. @@ -735,39 +733,33 @@ Proof. Qed. Lemma SIN : forall a:R, 0 <= a -> a <= PI -> sin_lb a <= sin a <= sin_ub a. +Proof. intros; unfold sin_lb, sin_ub in |- *; apply (sin_bound a 1 H H0). Qed. Lemma COS : forall a:R, - PI / 2 <= a -> a <= PI / 2 -> cos_lb a <= cos a <= cos_ub a. +Proof. intros; unfold cos_lb, cos_ub in |- *; apply (cos_bound a 1 H H0). Qed. (**********) Lemma _PI2_RLT_0 : - (PI / 2) < 0. Proof. - rewrite <- Ropp_0; apply Ropp_lt_contravar; apply PI2_RGT_0. + assert (H := PI_RGT_0). + fourier. Qed. Lemma PI4_RLT_PI2 : PI / 4 < PI / 2. Proof. - unfold Rdiv in |- *; apply Rmult_lt_compat_l. - apply PI_RGT_0. - apply Rinv_lt_contravar. - apply Rmult_lt_0_compat; prove_sup0. - pattern 2 at 1 in |- *; rewrite <- Rplus_0_r. - replace 4 with (2 + 2); [ apply Rplus_lt_compat_l; prove_sup0 | ring ]. + assert (H := PI_RGT_0). + fourier. Qed. Lemma PI2_Rlt_PI : PI / 2 < PI. Proof. - unfold Rdiv in |- *; pattern PI at 2 in |- *; rewrite <- Rmult_1_r. - apply Rmult_lt_compat_l. - apply PI_RGT_0. - rewrite <- Rinv_1; apply Rinv_lt_contravar. - rewrite Rmult_1_l; prove_sup0. - pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; - apply Rlt_0_1. + assert (H := PI_RGT_0). + fourier. Qed. (***************************************************) @@ -784,12 +776,10 @@ Proof. rewrite H3; rewrite sin_PI2; apply Rlt_0_1. rewrite <- sin_PI_x; generalize (Ropp_gt_lt_contravar x (PI / 2) H3); intro H4; generalize (Rplus_lt_compat_l PI (- x) (- (PI / 2)) H4). - replace (PI + - x) with (PI - x). replace (PI + - (PI / 2)) with (PI / 2). intro H5; generalize (Ropp_lt_gt_contravar x PI H0); intro H6; change (- PI < - x) in H6; generalize (Rplus_lt_compat_l PI (- PI) (- x) H6). rewrite Rplus_opp_r. - replace (PI + - x) with (PI - x). intro H7; elim (SIN (PI - x) (Rlt_le 0 (PI - x) H7) @@ -797,9 +787,7 @@ Proof. intros H8 _; generalize (sin_lb_gt_0 (PI - x) H7 (Rlt_le (PI - x) (PI / 2) H5)); intro H9; apply (Rlt_le_trans 0 (sin_lb (PI - x)) (sin (PI - x)) H9 H8). - reflexivity. - pattern PI at 2 in |- *; rewrite double_var; ring. - reflexivity. + field. Qed. Theorem cos_gt_0 : forall x:R, - (PI / 2) < x -> x < PI / 2 -> 0 < cos x. @@ -852,16 +840,12 @@ Proof. rewrite <- (Ropp_involutive (cos x)); apply Ropp_le_ge_contravar; rewrite <- neg_cos; replace (x + PI) with (x - PI + 2 * INR 1 * PI). rewrite cos_period; apply cos_ge_0. - replace (- (PI / 2)) with (- PI + PI / 2). + replace (- (PI / 2)) with (- PI + PI / 2) by field. unfold Rminus in |- *; rewrite (Rplus_comm x); apply Rplus_le_compat_l; assumption. - pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr; - ring. unfold Rminus in |- *; rewrite Rplus_comm; - replace (PI / 2) with (- PI + 3 * (PI / 2)). + replace (PI / 2) with (- PI + 3 * (PI / 2)) by field. apply Rplus_le_compat_l; assumption. - pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr; - ring. unfold INR in |- *; ring. Qed. @@ -902,16 +886,12 @@ Proof. apply Ropp_lt_gt_contravar; rewrite <- neg_cos; replace (x + PI) with (x - PI + 2 * INR 1 * PI). rewrite cos_period; apply cos_gt_0. - replace (- (PI / 2)) with (- PI + PI / 2). + replace (- (PI / 2)) with (- PI + PI / 2) by field. unfold Rminus in |- *; rewrite (Rplus_comm x); apply Rplus_lt_compat_l; assumption. - pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr; - ring. unfold Rminus in |- *; rewrite Rplus_comm; - replace (PI / 2) with (- PI + 3 * (PI / 2)). + replace (PI / 2) with (- PI + 3 * (PI / 2)) by field. apply Rplus_lt_compat_l; assumption. - pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr; - ring. unfold INR in |- *; ring. Qed. @@ -948,7 +928,7 @@ Lemma cos_ge_0_3PI2 : forall x:R, 3 * (PI / 2) <= x -> x <= 2 * PI -> 0 <= cos x. Proof. intros; rewrite <- cos_neg; rewrite <- (cos_period (- x) 1); - unfold INR in |- *; replace (- x + 2 * 1 * PI) with (2 * PI - x). + unfold INR in |- *; replace (- x + 2 * 1 * PI) with (2 * PI - x) by ring. generalize (Ropp_le_ge_contravar x (2 * PI) H0); intro H1; generalize (Rge_le (- x) (- (2 * PI)) H1); clear H1; intro H1; generalize (Rplus_le_compat_l (2 * PI) (- (2 * PI)) (- x) H1). @@ -957,36 +937,30 @@ Proof. generalize (Rge_le (- (3 * (PI / 2))) (- x) H3); clear H3; intro H3; generalize (Rplus_le_compat_l (2 * PI) (- x) (- (3 * (PI / 2))) H3). - replace (2 * PI + - (3 * (PI / 2))) with (PI / 2). + replace (2 * PI + - (3 * (PI / 2))) with (PI / 2) by field. intro H4; apply (cos_ge_0 (2 * PI - x) (Rlt_le (- (PI / 2)) (2 * PI - x) (Rlt_le_trans (- (PI / 2)) 0 (2 * PI - x) _PI2_RLT_0 H2)) H4). - rewrite double; pattern PI at 2 3 in |- *; rewrite double_var; ring. - ring. Qed. Lemma form1 : forall p q:R, cos p + cos q = 2 * cos ((p - q) / 2) * cos ((p + q) / 2). Proof. intros p q; pattern p at 1 in |- *; - replace p with ((p - q) / 2 + (p + q) / 2). - rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2). + replace p with ((p - q) / 2 + (p + q) / 2) by field. + rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2) by field. rewrite cos_plus; rewrite cos_minus; ring. - pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. - pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. Qed. Lemma form2 : forall p q:R, cos p - cos q = -2 * sin ((p - q) / 2) * sin ((p + q) / 2). Proof. intros p q; pattern p at 1 in |- *; - replace p with ((p - q) / 2 + (p + q) / 2). - rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2). + replace p with ((p - q) / 2 + (p + q) / 2) by field. + rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2) by field. rewrite cos_plus; rewrite cos_minus; ring. - pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. - pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. Qed. Lemma form3 : @@ -1004,11 +978,9 @@ Lemma form4 : forall p q:R, sin p - sin q = 2 * cos ((p + q) / 2) * sin ((p - q) / 2). Proof. intros p q; pattern p at 1 in |- *; - replace p with ((p - q) / 2 + (p + q) / 2). - pattern q at 3 in |- *; replace q with ((p + q) / 2 - (p - q) / 2). + replace p with ((p - q) / 2 + (p + q) / 2) by field. + pattern q at 3 in |- *; replace q with ((p + q) / 2 - (p - q) / 2) by field. rewrite sin_plus; rewrite sin_minus; ring. - pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. - pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. Qed. @@ -1064,13 +1036,13 @@ Proof. repeat rewrite (Rmult_comm (/ 2)). clear H4; intro H4; generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) y H H1); - replace (- (PI / 2) + - (PI / 2)) with (- PI). + replace (- (PI / 2) + - (PI / 2)) with (- PI) by field. intro H5; generalize (Rmult_le_compat_l (/ 2) (- PI) (x + y) (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H5). - replace (/ 2 * (x + y)) with ((x + y) / 2). - replace (/ 2 * - PI) with (- (PI / 2)). + replace (/ 2 * (x + y)) with ((x + y) / 2) by apply Rmult_comm. + replace (/ 2 * - PI) with (- (PI / 2)) by field. clear H5; intro H5; elim H4; intro H40. elim H5; intro H50. generalize (cos_gt_0 ((x + y) / 2) H50 H40); intro H6; @@ -1092,13 +1064,6 @@ Proof. rewrite H40 in H3; assert (H50 := cos_PI2); unfold Rdiv in H50; rewrite H50 in H3; rewrite Rmult_0_r in H3; rewrite Rmult_0_l in H3; elim (Rlt_irrefl 0 H3). - unfold Rdiv in |- *. - rewrite <- Ropp_mult_distr_l_reverse. - apply Rmult_comm. - unfold Rdiv in |- *; apply Rmult_comm. - pattern PI at 1 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - reflexivity. Qed. Lemma sin_increasing_1 : @@ -1108,43 +1073,42 @@ Lemma sin_increasing_1 : Proof. intros; generalize (Rplus_lt_compat_l x x y H3); intro H4; generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) x H H); - replace (- (PI / 2) + - (PI / 2)) with (- PI). + replace (- (PI / 2) + - (PI / 2)) with (- PI) by field. assert (Hyp : 0 < 2). prove_sup0. intro H5; generalize (Rle_lt_trans (- PI) (x + x) (x + y) H5 H4); intro H6; generalize (Rmult_lt_compat_l (/ 2) (- PI) (x + y) (Rinv_0_lt_compat 2 Hyp) H6); - replace (/ 2 * - PI) with (- (PI / 2)). - replace (/ 2 * (x + y)) with ((x + y) / 2). + replace (/ 2 * - PI) with (- (PI / 2)) by field. + replace (/ 2 * (x + y)) with ((x + y) / 2) by apply Rmult_comm. clear H4 H5 H6; intro H4; generalize (Rplus_lt_compat_l y x y H3); intro H5; rewrite Rplus_comm in H5; generalize (Rplus_le_compat y (PI / 2) y (PI / 2) H2 H2). rewrite <- double_var. intro H6; generalize (Rlt_le_trans (x + y) (y + y) PI H5 H6); intro H7; generalize (Rmult_lt_compat_l (/ 2) (x + y) PI (Rinv_0_lt_compat 2 Hyp) H7); - replace (/ 2 * PI) with (PI / 2). - replace (/ 2 * (x + y)) with ((x + y) / 2). + replace (/ 2 * PI) with (PI / 2) by apply Rmult_comm. + replace (/ 2 * (x + y)) with ((x + y) / 2) by apply Rmult_comm. clear H5 H6 H7; intro H5; generalize (Ropp_le_ge_contravar (- (PI / 2)) y H1); rewrite Ropp_involutive; clear H1; intro H1; generalize (Rge_le (PI / 2) (- y) H1); clear H1; intro H1; generalize (Ropp_le_ge_contravar y (PI / 2) H2); clear H2; intro H2; generalize (Rge_le (- y) (- (PI / 2)) H2); clear H2; intro H2; generalize (Rplus_lt_compat_l (- y) x y H3); - replace (- y + x) with (x - y). + replace (- y + x) with (x - y) by apply Rplus_comm. rewrite Rplus_opp_l. intro H6; generalize (Rmult_lt_compat_l (/ 2) (x - y) 0 (Rinv_0_lt_compat 2 Hyp) H6); - rewrite Rmult_0_r; replace (/ 2 * (x - y)) with ((x - y) / 2). + rewrite Rmult_0_r; replace (/ 2 * (x - y)) with ((x - y) / 2) by apply Rmult_comm. clear H6; intro H6; generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) (- y) H H2); - replace (- (PI / 2) + - (PI / 2)) with (- PI). - replace (x + - y) with (x - y). + replace (- (PI / 2) + - (PI / 2)) with (- PI) by field. intro H7; generalize (Rmult_le_compat_l (/ 2) (- PI) (x - y) (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H7); - replace (/ 2 * - PI) with (- (PI / 2)). - replace (/ 2 * (x - y)) with ((x - y) / 2). + replace (/ 2 * - PI) with (- (PI / 2)) by field. + replace (/ 2 * (x - y)) with ((x - y) / 2) by apply Rmult_comm. clear H7; intro H7; clear H H0 H1 H2; apply Rminus_lt; rewrite form4; generalize (cos_gt_0 ((x + y) / 2) H4 H5); intro H8; generalize (Rmult_lt_0_compat 2 (cos ((x + y) / 2)) Hyp H8); @@ -1159,23 +1123,6 @@ Proof. 2 * cos ((x + y) / 2)) H10 H8); intro H11; rewrite Rmult_0_r in H11; rewrite Rmult_comm; assumption. apply Ropp_lt_gt_contravar; apply PI2_Rlt_PI. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse; apply Rmult_comm. - reflexivity. - pattern PI at 1 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - reflexivity. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rminus in |- *; apply Rplus_comm. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rdiv in |- *. - rewrite <- Ropp_mult_distr_l_reverse. - apply Rmult_comm. - pattern PI at 1 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - reflexivity. Qed. Lemma sin_decreasing_0 : @@ -1190,33 +1137,16 @@ Proof. generalize (Rplus_le_compat_l (- PI) (PI / 2) x H0); generalize (Rplus_le_compat_l (- PI) y (3 * (PI / 2)) H1); generalize (Rplus_le_compat_l (- PI) (PI / 2) y H2); - replace (- PI + x) with (x - PI). - replace (- PI + PI / 2) with (- (PI / 2)). - replace (- PI + y) with (y - PI). - replace (- PI + 3 * (PI / 2)) with (PI / 2). - replace (- (PI - x)) with (x - PI). - replace (- (PI - y)) with (y - PI). + replace (- PI + x) with (x - PI) by apply Rplus_comm. + replace (- PI + PI / 2) with (- (PI / 2)) by field. + replace (- PI + y) with (y - PI) by apply Rplus_comm. + replace (- PI + 3 * (PI / 2)) with (PI / 2) by field. + replace (- (PI - x)) with (x - PI) by ring. + replace (- (PI - y)) with (y - PI) by ring. intros; change (sin (y - PI) < sin (x - PI)) in H8; - apply Rplus_lt_reg_l with (- PI); rewrite Rplus_comm; - replace (y + - PI) with (y - PI). - rewrite Rplus_comm; replace (x + - PI) with (x - PI). + apply Rplus_lt_reg_l with (- PI); rewrite Rplus_comm. + rewrite (Rplus_comm _ x). apply (sin_increasing_0 (y - PI) (x - PI) H4 H5 H6 H7 H8). - reflexivity. - reflexivity. - unfold Rminus in |- *; rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - apply Rplus_comm. - unfold Rminus in |- *; rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - apply Rplus_comm. - pattern PI at 2 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - ring. - unfold Rminus in |- *; apply Rplus_comm. - pattern PI at 2 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - ring. - unfold Rminus in |- *; apply Rplus_comm. Qed. Lemma sin_decreasing_1 : @@ -1230,24 +1160,14 @@ Proof. generalize (Rplus_le_compat_l (- PI) y (3 * (PI / 2)) H1); generalize (Rplus_le_compat_l (- PI) (PI / 2) y H2); generalize (Rplus_lt_compat_l (- PI) x y H3); - replace (- PI + PI / 2) with (- (PI / 2)). - replace (- PI + y) with (y - PI). - replace (- PI + 3 * (PI / 2)) with (PI / 2). - replace (- PI + x) with (x - PI). + replace (- PI + PI / 2) with (- (PI / 2)) by field. + replace (- PI + y) with (y - PI) by apply Rplus_comm. + replace (- PI + 3 * (PI / 2)) with (PI / 2) by field. + replace (- PI + x) with (x - PI) by apply Rplus_comm. intros; apply Ropp_lt_cancel; repeat rewrite <- sin_neg; - replace (- (PI - x)) with (x - PI). - replace (- (PI - y)) with (y - PI). + replace (- (PI - x)) with (x - PI) by ring. + replace (- (PI - y)) with (y - PI) by ring. apply (sin_increasing_1 (x - PI) (y - PI) H7 H8 H5 H6 H4). - unfold Rminus in |- *; rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - apply Rplus_comm. - unfold Rminus in |- *; rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - apply Rplus_comm. - unfold Rminus in |- *; apply Rplus_comm. - pattern PI at 2 in |- *; rewrite double_var; ring. - unfold Rminus in |- *; apply Rplus_comm. - pattern PI at 2 in |- *; rewrite double_var; ring. Qed. Lemma cos_increasing_0 : @@ -1287,31 +1207,16 @@ Proof. generalize (Rplus_lt_compat_l (-3 * (PI / 2)) x y H5); rewrite <- (cos_neg x); rewrite <- (cos_neg y); rewrite <- (cos_period (- x) 1); rewrite <- (cos_period (- y) 1); - unfold INR in |- *; replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)). - replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)). - replace (-3 * (PI / 2) + PI) with (- (PI / 2)). - replace (-3 * (PI / 2) + 2 * PI) with (PI / 2). + unfold INR in |- *; replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)) by ring. + replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)) by ring. + replace (-3 * (PI / 2) + PI) with (- (PI / 2)) by field. + replace (-3 * (PI / 2) + 2 * PI) with (PI / 2) by field. clear H1 H2 H3 H4 H5; intros H1 H2 H3 H4 H5; - replace (- x + 2 * 1 * PI) with (PI / 2 - (x - 3 * (PI / 2))). - replace (- y + 2 * 1 * PI) with (PI / 2 - (y - 3 * (PI / 2))). + replace (- x + 2 * 1 * PI) with (PI / 2 - (x - 3 * (PI / 2))) by field. + replace (- y + 2 * 1 * PI) with (PI / 2 - (y - 3 * (PI / 2))) by field. repeat rewrite cos_shift; apply (sin_increasing_1 (x - 3 * (PI / 2)) (y - 3 * (PI / 2)) H5 H4 H3 H2 H1). - rewrite Rmult_1_r. - rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var. - ring. - rewrite Rmult_1_r. - rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var. - ring. - rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var. - ring. - pattern PI at 3 in |- *; rewrite double_var; ring. - unfold Rminus in |- *. - rewrite <- Ropp_mult_distr_l_reverse. - apply Rplus_comm. - unfold Rminus in |- *. - rewrite <- Ropp_mult_distr_l_reverse. - apply Rplus_comm. Qed. Lemma cos_decreasing_0 : @@ -1350,31 +1255,8 @@ Lemma tan_diff : cos x <> 0 -> cos y <> 0 -> tan x - tan y = sin (x - y) / (cos x * cos y). Proof. intros; unfold tan in |- *; rewrite sin_minus. - unfold Rdiv in |- *. - unfold Rminus in |- *. - rewrite Rmult_plus_distr_r. - rewrite Rinv_mult_distr. - repeat rewrite (Rmult_comm (sin x)). - repeat rewrite Rmult_assoc. - rewrite (Rmult_comm (cos y)). - repeat rewrite Rmult_assoc. - rewrite <- Rinv_l_sym. - rewrite Rmult_1_r. - rewrite (Rmult_comm (sin x)). - apply Rplus_eq_compat_l. - rewrite <- Ropp_mult_distr_l_reverse. - rewrite <- Ropp_mult_distr_r_reverse. - rewrite (Rmult_comm (/ cos x)). - repeat rewrite Rmult_assoc. - rewrite (Rmult_comm (cos x)). - repeat rewrite Rmult_assoc. - rewrite <- Rinv_l_sym. - rewrite Rmult_1_r. - reflexivity. - assumption. - assumption. - assumption. - assumption. + field. + now split. Qed. Lemma tan_increasing_0 : @@ -1411,10 +1293,9 @@ Proof. intro H11; generalize (Rge_le (- y) (- (PI / 4)) H11); clear H11; intro H11; generalize (Rplus_le_compat (- (PI / 4)) x (- (PI / 4)) (- y) H H11); - generalize (Rplus_le_compat x (PI / 4) (- y) (PI / 4) H0 H10); - replace (x + - y) with (x - y). - replace (PI / 4 + PI / 4) with (PI / 2). - replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)). + generalize (Rplus_le_compat x (PI / 4) (- y) (PI / 4) H0 H10). + replace (PI / 4 + PI / 4) with (PI / 2) by field. + replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)) by field. intros; case (Rtotal_order 0 (x - y)); intro H14. generalize (sin_gt_0 (x - y) H14 (Rle_lt_trans (x - y) (PI / 2) PI H12 PI2_Rlt_PI)); @@ -1422,28 +1303,6 @@ Proof. elim H14; intro H15. rewrite <- H15 in H9; rewrite sin_0 in H9; elim (Rlt_irrefl 0 H9). apply Rminus_lt; assumption. - pattern PI at 1 in |- *; rewrite double_var. - unfold Rdiv in |- *. - rewrite Rmult_plus_distr_r. - repeat rewrite Rmult_assoc. - rewrite <- Rinv_mult_distr. - rewrite Ropp_plus_distr. - replace 4 with 4. - reflexivity. - ring. - discrR. - discrR. - pattern PI at 1 in |- *; rewrite double_var. - unfold Rdiv in |- *. - rewrite Rmult_plus_distr_r. - repeat rewrite Rmult_assoc. - rewrite <- Rinv_mult_distr. - replace 4 with 4. - reflexivity. - ring. - discrR. - discrR. - reflexivity. case (Rcase_abs (sin (x - y))); intro H9. assumption. generalize (Rge_le (sin (x - y)) 0 H9); clear H9; intro H9; @@ -1457,8 +1316,7 @@ Proof. (Rlt_le 0 (/ (cos x * cos y)) H12)); intro H13; elim (Rlt_irrefl 0 (Rle_lt_trans 0 (sin (x - y) * / (cos x * cos y)) 0 H13 H3)). - rewrite Rinv_mult_distr. - reflexivity. + apply Rinv_mult_distr. assumption. assumption. Qed. @@ -1496,9 +1354,8 @@ Proof. clear H10 H11; intro H8; generalize (Ropp_le_ge_contravar y (PI / 4) H2); intro H11; generalize (Rge_le (- y) (- (PI / 4)) H11); clear H11; intro H11; - generalize (Rplus_le_compat (- (PI / 4)) x (- (PI / 4)) (- y) H H11); - replace (x + - y) with (x - y). - replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)). + generalize (Rplus_le_compat (- (PI / 4)) x (- (PI / 4)) (- y) H H11). + replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)) by field. clear H11; intro H9; generalize (Rlt_minus x y H3); clear H3; intro H3; clear H H0 H1 H2 H4 H5 HP1 HP2; generalize PI2_Rlt_PI; intro H1; generalize (Ropp_lt_gt_contravar (PI / 2) PI H1); @@ -1509,18 +1366,6 @@ Proof. generalize (Rmult_lt_gt_compat_neg_l (sin (x - y)) 0 (/ (cos x * cos y)) H2 H8); rewrite Rmult_0_r; intro H4; assumption. - pattern PI at 1 in |- *; rewrite double_var. - unfold Rdiv in |- *. - rewrite Rmult_plus_distr_r. - repeat rewrite Rmult_assoc. - rewrite <- Rinv_mult_distr. - replace 4 with 4. - rewrite Ropp_plus_distr. - reflexivity. - ring. - discrR. - discrR. - reflexivity. apply Rinv_mult_distr; assumption. Qed. @@ -1762,8 +1607,7 @@ Proof. rewrite Rplus_0_r. rewrite Ropp_Ropp_IZR. rewrite Rplus_opp_r. - left; replace 0 with (IZR 0); [ apply IZR_lt | reflexivity ]. - assumption. + now apply Rlt_le, IZR_lt. rewrite <- sin_neg. rewrite Ropp_mult_distr_l_reverse. rewrite Ropp_involutive. diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index 092bc30d0..55cb74e35 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -99,24 +99,22 @@ Proof. apply Rle_trans with 20. apply Rle_trans with 16. replace 16 with (Rsqr 4); [ idtac | ring_Rsqr ]. - replace (a * a) with (Rsqr a); [ idtac | reflexivity ]. apply Rsqr_incr_1. assumption. assumption. - left; prove_sup0. - rewrite <- (Rplus_0_r 16); replace 20 with (16 + 4); - [ apply Rplus_le_compat_l; left; prove_sup0 | ring ]. - rewrite <- (Rplus_comm 20); pattern 20 at 1; rewrite <- Rplus_0_r; - apply Rplus_le_compat_l. + now apply IZR_le. + now apply IZR_le. + rewrite <- (Rplus_0_l 20) at 1; + apply Rplus_le_compat_r. apply Rplus_le_le_0_compat. - repeat apply Rmult_le_pos. - left; prove_sup0. - left; prove_sup0. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. apply Rmult_le_pos. - left; prove_sup0. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. + apply Rmult_le_pos. + now apply IZR_le. + apply pos_INR. + apply pos_INR. + apply Rmult_le_pos. + now apply IZR_le. + apply pos_INR. apply INR_fact_neq_0. apply INR_fact_neq_0. simpl; ring. @@ -182,16 +180,14 @@ Proof. replace (- sum_f_R0 (tg_alt Un) (S (2 * n))) with (-1 * sum_f_R0 (tg_alt Un) (S (2 * n))); [ rewrite scal_sum | ring ]. apply sum_eq; intros; unfold sin_term, Un, tg_alt; - replace ((-1) ^ S i) with (-1 * (-1) ^ i). + change ((-1) ^ S i) with (-1 * (-1) ^ i). unfold Rdiv; ring. - reflexivity. replace (- sum_f_R0 (tg_alt Un) (2 * n)) with (-1 * sum_f_R0 (tg_alt Un) (2 * n)); [ rewrite scal_sum | ring ]. apply sum_eq; intros. unfold sin_term, Un, tg_alt; - replace ((-1) ^ S i) with (-1 * (-1) ^ i). + change ((-1) ^ S i) with (-1 * (-1) ^ i). unfold Rdiv; ring. - reflexivity. replace (2 * (n + 1))%nat with (S (S (2 * n))). reflexivity. ring. @@ -279,26 +275,23 @@ Proof. with (4 * INR n1 * INR n1 + 14 * INR n1 + 12); [ idtac | ring ]. apply Rle_trans with 12. apply Rle_trans with 4. - replace 4 with (Rsqr 2); [ idtac | ring_Rsqr ]. - replace (a0 * a0) with (Rsqr a0); [ idtac | reflexivity ]. + change 4 with (Rsqr 2). apply Rsqr_incr_1. assumption. - discrR. assumption. - left; prove_sup0. - pattern 4 at 1; rewrite <- Rplus_0_r; replace 12 with (4 + 8); - [ apply Rplus_le_compat_l; left; prove_sup0 | ring ]. - rewrite <- (Rplus_comm 12); pattern 12 at 1; rewrite <- Rplus_0_r; - apply Rplus_le_compat_l. + now apply IZR_le. + now apply IZR_le. + rewrite <- (Rplus_0_l 12) at 1; + apply Rplus_le_compat_r. apply Rplus_le_le_0_compat. - repeat apply Rmult_le_pos. - left; prove_sup0. - left; prove_sup0. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. apply Rmult_le_pos. - left; prove_sup0. - replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ]. + apply Rmult_le_pos. + now apply IZR_le. + apply pos_INR. + apply pos_INR. + apply Rmult_le_pos. + now apply IZR_le. + apply pos_INR. apply INR_fact_neq_0. apply INR_fact_neq_0. simpl; ring. @@ -351,15 +344,13 @@ Proof. replace (- sum_f_R0 (tg_alt Un) (S (2 * n0))) with (-1 * sum_f_R0 (tg_alt Un) (S (2 * n0))); [ rewrite scal_sum | ring ]. apply sum_eq; intros; unfold cos_term, Un, tg_alt; - replace ((-1) ^ S i) with (-1 * (-1) ^ i). + change ((-1) ^ S i) with (-1 * (-1) ^ i). unfold Rdiv; ring. - reflexivity. replace (- sum_f_R0 (tg_alt Un) (2 * n0)) with (-1 * sum_f_R0 (tg_alt Un) (2 * n0)); [ rewrite scal_sum | ring ]; apply sum_eq; intros; unfold cos_term, Un, tg_alt; - replace ((-1) ^ S i) with (-1 * (-1) ^ i). + change ((-1) ^ S i) with (-1 * (-1) ^ i). unfold Rdiv; ring. - reflexivity. replace (2 * (n0 + 1))%nat with (S (S (2 * n0))). reflexivity. ring. diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 0d2a9a8ba..b46df202e 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -157,7 +157,7 @@ Proof. apply Rinv_0_lt_compat; assumption. rewrite H3 in H0; assumption. apply lt_le_trans with 1%nat; [ apply lt_O_Sn | apply le_max_r ]. - apply le_IZR; replace (IZR 0) with 0; [ idtac | reflexivity ]; left; + apply le_IZR; left; apply Rlt_trans with (/ eps); [ apply Rinv_0_lt_compat; assumption | assumption ]. assert (H0 := archimed (/ eps)). @@ -194,30 +194,27 @@ Proof. elim H1; intros; assumption. apply lt_le_trans with (S n). unfold ge in H2; apply le_lt_n_Sm; assumption. - replace (2 * n + 1)%nat with (S (2 * n)); [ idtac | ring ]. + replace (2 * n + 1)%nat with (S (2 * n)) by ring. apply le_n_S; apply le_n_2n. apply Rmult_lt_reg_l with (INR (2 * S n)). apply lt_INR_0; replace (2 * S n)%nat with (S (S (2 * n))). apply lt_O_Sn. - replace (S n) with (n + 1)%nat; [ idtac | ring ]. + replace (S n) with (n + 1)%nat by ring. ring. rewrite <- Rinv_r_sym. - rewrite Rmult_1_r; replace 1 with (INR 1); [ apply lt_INR | reflexivity ]. + rewrite Rmult_1_r. + apply (lt_INR 1). replace (2 * S n)%nat with (S (S (2 * n))). apply lt_n_S; apply lt_O_Sn. - replace (S n) with (n + 1)%nat; [ ring | ring ]. + ring. apply not_O_INR; discriminate. apply not_O_INR; discriminate. replace (2 * n + 1)%nat with (S (2 * n)); [ apply not_O_INR; discriminate | ring ]. apply Rle_ge; left; apply Rinv_0_lt_compat. apply lt_INR_0. - replace (2 * S n * (2 * n + 1))%nat with (S (S (4 * (n * n) + 6 * n))). + replace (2 * S n * (2 * n + 1))%nat with (2 + (4 * (n * n) + 6 * n))%nat by ring. apply lt_O_Sn. - apply INR_eq. - repeat rewrite S_INR; rewrite plus_INR; repeat rewrite mult_INR; - rewrite plus_INR; rewrite mult_INR; repeat rewrite S_INR; - replace (INR 0) with 0; [ ring | reflexivity ]. Qed. Lemma cosn_no_R0 : forall n:nat, cos_n n <> 0. @@ -318,28 +315,25 @@ Proof. elim H1; intros; assumption. apply lt_le_trans with (S n). unfold ge in H2; apply le_lt_n_Sm; assumption. - replace (2 * S n + 1)%nat with (S (2 * S n)); [ idtac | ring ]. + replace (2 * S n + 1)%nat with (S (2 * S n)) by ring. apply le_S; apply le_n_2n. apply Rmult_lt_reg_l with (INR (2 * S n)). apply lt_INR_0; replace (2 * S n)%nat with (S (S (2 * n))); - [ apply lt_O_Sn | replace (S n) with (n + 1)%nat; [ idtac | ring ]; ring ]. + [ apply lt_O_Sn | ring ]. rewrite <- Rinv_r_sym. - rewrite Rmult_1_r; replace 1 with (INR 1); [ apply lt_INR | reflexivity ]. + rewrite Rmult_1_r. + apply (lt_INR 1). replace (2 * S n)%nat with (S (S (2 * n))). apply lt_n_S; apply lt_O_Sn. - replace (S n) with (n + 1)%nat; [ ring | ring ]. + ring. apply not_O_INR; discriminate. apply not_O_INR; discriminate. apply not_O_INR; discriminate. - left; change (0 < / INR ((2 * S n + 1) * (2 * S n))); - apply Rinv_0_lt_compat. + left; apply Rinv_0_lt_compat. apply lt_INR_0. replace ((2 * S n + 1) * (2 * S n))%nat with - (S (S (S (S (S (S (4 * (n * n) + 10 * n))))))). + (6 + (4 * (n * n) + 10 * n))%nat by ring. apply lt_O_Sn. - apply INR_eq; repeat rewrite S_INR; rewrite plus_INR; repeat rewrite mult_INR; - rewrite plus_INR; rewrite mult_INR; repeat rewrite S_INR; - replace (INR 0) with 0; [ ring | reflexivity ]. Qed. Lemma sin_no_R0 : forall n:nat, sin_n n <> 0. diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 5a2a07c42..3697999f7 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -1167,7 +1167,7 @@ Proof. assert (H6 := archimed (Rabs x)); fold M in H6; elim H6; intros. rewrite H4 in H7; rewrite <- INR_IZR_INZ in H7. simpl in H7; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H2 H7)). - replace 1 with (INR 1); [ apply le_INR | reflexivity ]; apply le_n_S; + apply (le_INR 1); apply le_n_S; apply le_O_n. apply le_IZR; simpl; left; apply Rlt_trans with (Rabs x). assumption. |