diff options
Diffstat (limited to 'theories/Reals/Rtrigo1.v')
| -rw-r--r-- | theories/Reals/Rtrigo1.v | 33 |
1 files changed, 16 insertions, 17 deletions
diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v index b940455f..9e485ec5 100644 --- a/theories/Reals/Rtrigo1.v +++ b/theories/Reals/Rtrigo1.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,7 +16,6 @@ Require Export Cos_rel. Require Export Cos_plus. Require Import ZArith_base. Require Import Zcomplements. -Require Import Classical_Prop. Require Import Fourier. Require Import Ranalysis1. Require Import Rsqrt_def. @@ -40,7 +39,7 @@ Proof. (fun n:nat => sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k)) * r ^ (2 * k))) n) l }. - intro X; elim X; intros. + intros (x,p). exists x. split. apply p. @@ -148,11 +147,11 @@ Proof. apply H4. intros; rewrite (H0 x); rewrite (H0 x1); apply H5; apply H6. intro; unfold cos, SFL in |- *. - case (cv x); case (exist_cos (Rsqr x)); intros. - symmetry in |- *; eapply UL_sequence. - apply u. - unfold cos_in in c; unfold infinite_sum in c; unfold Un_cv in |- *; intros. - elim (c _ H0); intros N0 H1. + case (cv x) as (x1,HUn); case (exist_cos (Rsqr x)) as (x0,Hcos); intros. + symmetry; eapply UL_sequence. + apply HUn. + unfold cos_in, infinite_sum in Hcos; unfold Un_cv in |- *; intros. + elim (Hcos _ H0); intros N0 H1. exists N0; intros. unfold R_dist in H1; unfold R_dist, SP in |- *. replace (sum_f_R0 (fun k:nat => fn k x) n) with @@ -586,8 +585,8 @@ Qed. Lemma SIN_bound : forall x:R, -1 <= sin x <= 1. Proof. - intro; case (Rle_dec (-1) (sin x)); intro. - case (Rle_dec (sin x) 1); intro. + intro; destruct (Rle_dec (-1) (sin x)) as [Hle|Hnle]. + destruct (Rle_dec (sin x) 1) as [Hle'|Hnle']. split; assumption. cut (1 < sin x). intro; @@ -670,11 +669,11 @@ Proof. replace (Un 0%nat + - Un 1%nat + Un 2%nat + - Un 3%nat) with (Un 0%nat - Un 1%nat + (Un 2%nat - Un 3%nat)); [ idtac | ring ]. apply Rplus_lt_0_compat. - unfold Rminus in |- *; apply Rplus_lt_reg_r with (Un 1%nat); + unfold Rminus in |- *; apply Rplus_lt_reg_l with (Un 1%nat); rewrite Rplus_0_r; rewrite (Rplus_comm (Un 1%nat)); rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; apply H1. - unfold Rminus in |- *; apply Rplus_lt_reg_r with (Un 3%nat); + unfold Rminus in |- *; apply Rplus_lt_reg_l with (Un 3%nat); rewrite Rplus_0_r; rewrite (Rplus_comm (Un 3%nat)); rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; apply H1. @@ -722,7 +721,7 @@ Proof. unfold INR in |- *. replace ((2 * x + 1 + 1 + 1) * (2 * x + 1 + 1)) with (4 * x * x + 10 * x + 6); [ idtac | ring ]. - apply Rplus_lt_reg_r with (-4); rewrite Rplus_opp_l; + apply Rplus_lt_reg_l with (-4); rewrite Rplus_opp_l; replace (-4 + (4 * x * x + 10 * x + 6)) with (4 * x * x + 10 * x + 2); [ idtac | ring ]. apply Rplus_le_lt_0_compat. @@ -1201,7 +1200,7 @@ Proof. replace (- (PI - x)) with (x - PI). replace (- (PI - y)) with (y - PI). intros; change (sin (y - PI) < sin (x - PI)) in H8; - apply Rplus_lt_reg_r with (- PI); rewrite Rplus_comm; + 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 (sin_increasing_0 (y - PI) (x - PI) H4 H5 H6 H7 H8). @@ -1273,7 +1272,7 @@ Proof. replace (-3 * (PI / 2) + 2 * PI) with (PI / 2). replace (-3 * (PI / 2) + PI) with (- (PI / 2)). clear H1 H2 H3 H4; intros H1 H2 H3 H4; - apply Rplus_lt_reg_r with (-3 * (PI / 2)); + apply Rplus_lt_reg_l with (-3 * (PI / 2)); replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)). replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)). apply (sin_increasing_0 (x - 3 * (PI / 2)) (y - 3 * (PI / 2)) H4 H3 H2 H1 H5). @@ -1352,7 +1351,7 @@ Proof. generalize (Rplus_le_compat_l PI 0 y H1); generalize (Rplus_le_compat_l PI y PI H2); rewrite Rplus_0_r. rewrite <- double. - clear H H0 H1 H2 H3; intros; apply Rplus_lt_reg_r with PI; + clear H H0 H1 H2 H3; intros; apply Rplus_lt_reg_l with PI; apply (cos_increasing_0 (PI + y) (PI + x) H0 H H2 H1 H4). Qed. @@ -1919,7 +1918,7 @@ Proof. apply (Rmult_lt_reg_r PI); [apply PI_RGT_0|rewrite Rmult_1_l]. replace (3*(PI/2)) with (PI/2 + PI) in GT by field. rewrite Rplus_comm in GT. - now apply Rplus_lt_reg_r in GT. } + now apply Rplus_lt_reg_l in GT. } omega. Qed. |