diff options
Diffstat (limited to 'theories7/Reals/Rtrigo_alt.v')
| -rw-r--r-- | theories7/Reals/Rtrigo_alt.v | 294 |
1 files changed, 0 insertions, 294 deletions
diff --git a/theories7/Reals/Rtrigo_alt.v b/theories7/Reals/Rtrigo_alt.v deleted file mode 100644 index db0e2fea..00000000 --- a/theories7/Reals/Rtrigo_alt.v +++ /dev/null @@ -1,294 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Rtrigo_alt.v,v 1.1.2.1 2004/07/16 19:31:36 herbelin Exp $ i*) - -Require Rbase. -Require Rfunctions. -Require SeqSeries. -Require Rtrigo_def. -V7only [ Import nat_scope. Import Z_scope. Import R_scope. ]. -Open Local Scope R_scope. - -(*****************************************************************) -(* Using series definitions of cos and sin *) -(*****************************************************************) - -Definition sin_term [a:R] : nat->R := [i:nat] ``(pow (-1) i)*(pow a (plus (mult (S (S O)) i) (S O)))/(INR (fact (plus (mult (S (S O)) i) (S O))))``. - -Definition cos_term [a:R] : nat->R := [i:nat] ``(pow (-1) i)*(pow a (mult (S (S O)) i))/(INR (fact (mult (S (S O)) i)))``. - -Definition sin_approx [a:R;n:nat] : R := (sum_f_R0 (sin_term a) n). - -Definition cos_approx [a:R;n:nat] : R := (sum_f_R0 (cos_term a) n). - -(**********) -Lemma PI_4 : ``PI<=4``. -Assert H0 := (PI_ineq O). -Elim H0; Clear H0; Intros _ H0. -Unfold tg_alt PI_tg in H0; Simpl in H0. -Rewrite Rinv_R1 in H0; Rewrite Rmult_1r in H0; Unfold Rdiv in H0. -Apply Rle_monotony_contra with ``/4``. -Apply Rlt_Rinv; Sup0. -Rewrite <- Rinv_l_sym; [Rewrite Rmult_sym; Assumption | DiscrR]. -Qed. - -(**********) -Theorem sin_bound : (a:R; n:nat) ``0 <= a``->``a <= PI``->``(sin_approx a (plus (mult (S (S O)) n) (S O))) <= (sin a)<= (sin_approx a (mult (S (S O)) (plus n (S O))))``. -Intros; Case (Req_EM a R0); Intro Hyp_a. -Rewrite Hyp_a; Rewrite sin_0; Split; Right; Unfold sin_approx; Apply sum_eq_R0 Orelse (Symmetry; Apply sum_eq_R0); Intros; Unfold sin_term; Rewrite pow_add; Simpl; Unfold Rdiv; Rewrite Rmult_Ol; Ring. -Unfold sin_approx; Cut ``0<a``. -Intro Hyp_a_pos. -Rewrite (decomp_sum (sin_term a) (plus (mult (S (S O)) n) (S O))). -Rewrite (decomp_sum (sin_term a) (mult (S (S O)) (plus n (S O)))). -Replace (sin_term a O) with a. -Cut (Rle (sum_f_R0 [i:nat](sin_term a (S i)) (pred (plus (mult (S (S O)) n) (S O)))) ``(sin a)-a``)/\(Rle ``(sin a)-a`` (sum_f_R0 [i:nat](sin_term a (S i)) (pred (mult (S (S O)) (plus n (S O)))))) -> (Rle (Rplus a (sum_f_R0 [i:nat](sin_term a (S i)) (pred (plus (mult (S (S O)) n) (S O))))) (sin a))/\(Rle (sin a) (Rplus a (sum_f_R0 [i:nat](sin_term a (S i)) (pred (mult (S (S O)) (plus n (S O))))))). -Intro; Apply H1. -Pose Un := [n:nat]``(pow a (plus (mult (S (S O)) (S n)) (S O)))/(INR (fact (plus (mult (S (S O)) (S n)) (S O))))``. -Replace (pred (plus (mult (S (S O)) n) (S O))) with (mult (S (S O)) n). -Replace (pred (mult (S (S O)) (plus n (S O)))) with (S (mult (S (S O)) n)). -Replace (sum_f_R0 [i:nat](sin_term a (S i)) (mult (S (S O)) n)) with ``-(sum_f_R0 (tg_alt Un) (mult (S (S O)) n))``. -Replace (sum_f_R0 [i:nat](sin_term a (S i)) (S (mult (S (S O)) n))) with ``-(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n)))``. -Cut ``(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n)))<=a-(sin a)<=(sum_f_R0 (tg_alt Un) (mult (S (S O)) n))``->`` -(sum_f_R0 (tg_alt Un) (mult (S (S O)) n)) <= (sin a)-a <= -(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n)))``. -Intro; Apply H2. -Apply alternated_series_ineq. -Unfold Un_decreasing Un; Intro; Cut (plus (mult (S (S O)) (S (S n0))) (S O))=(S (S (plus (mult (S (S O)) (S n0)) (S O)))). -Intro; Rewrite H3. -Replace ``(pow a (S (S (plus (mult (S (S O)) (S n0)) (S O)))))`` with ``(pow a (plus (mult (S (S O)) (S n0)) (S O)))*(a*a)``. -Unfold Rdiv; Rewrite Rmult_assoc; Apply Rle_monotony. -Left; Apply pow_lt; Assumption. -Apply Rle_monotony_contra with ``(INR (fact (S (S (plus (mult (S (S O)) (S n0)) (S O))))))``. -Rewrite <- H3; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H5 := (sym_eq ? ? ? H4); Elim (fact_neq_0 ? H5). -Rewrite <- H3; Rewrite (Rmult_sym ``(INR (fact (plus (mult (S (S O)) (S (S n0))) (S O))))``); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r; Rewrite H3; Do 2 Rewrite fact_simpl; Do 2 Rewrite mult_INR; Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r. -Do 2 Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Simpl; Replace ``((0+1+1)*((INR n0)+1)+(0+1)+1+1)*((0+1+1)*((INR n0)+1)+(0+1)+1)`` with ``4*(INR n0)*(INR n0)+18*(INR n0)+20``; [Idtac | Ring]. -Apply Rle_trans with ``20``. -Apply Rle_trans with ``16``. -Replace ``16`` with ``(Rsqr 4)``; [Idtac | SqRing]. -Replace ``a*a`` with (Rsqr a); [Idtac | Reflexivity]. -Apply Rsqr_incr_1. -Apply Rle_trans with PI; [Assumption | Apply PI_4]. -Assumption. -Left; Sup0. -Rewrite <- (Rplus_Or ``16``); Replace ``20`` with ``16+4``; [Apply Rle_compatibility; Left; Sup0 | Ring]. -Rewrite <- (Rplus_sym ``20``); Pattern 1 ``20``; Rewrite <- Rplus_Or; Apply Rle_compatibility. -Apply ge0_plus_ge0_is_ge0. -Repeat Apply Rmult_le_pos. -Left; Sup0. -Left; Sup0. -Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity]. -Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity]. -Apply Rmult_le_pos. -Left; Sup0. -Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity]. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Simpl; Ring. -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite plus_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Assert H3 := (cv_speed_pow_fact a); Unfold Un; Unfold Un_cv in H3; Unfold R_dist in H3; Unfold Un_cv; Unfold R_dist; Intros; Elim (H3 eps H4); Intros N H5. -Exists N; Intros; Apply H5. -Replace (plus (mult (2) (S n0)) (1)) with (S (mult (2) (S n0))). -Unfold ge; Apply le_trans with (mult (2) (S n0)). -Apply le_trans with (mult (2) (S N)). -Apply le_trans with (mult (2) N). -Apply le_n_2n. -Apply mult_le; Apply le_n_Sn. -Apply mult_le; Apply le_n_S; Assumption. -Apply le_n_Sn. -Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Reflexivity. -Assert X := (exist_sin (Rsqr a)); Elim X; Intros. -Cut ``x==(sin a)/a``. -Intro; Rewrite H3 in p; Unfold sin_in in p; Unfold infinit_sum in p; Unfold R_dist in p; Unfold Un_cv; Unfold R_dist; Intros. -Cut ``0<eps/(Rabsolu a)``. -Intro; Elim (p ? H5); Intros N H6. -Exists N; Intros. -Replace (sum_f_R0 (tg_alt Un) n0) with (Rmult a (Rminus R1 (sum_f_R0 [i:nat]``(sin_n i)*(pow (Rsqr a) i)`` (S n0)))). -Unfold Rminus; Rewrite Rmult_Rplus_distr; Rewrite Rmult_1r; Rewrite Ropp_distr1; Rewrite Ropp_Ropp; Repeat Rewrite Rplus_assoc; Rewrite (Rplus_sym a); Rewrite (Rplus_sym ``-a``); Repeat Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Apply Rlt_monotony_contra with ``/(Rabsolu a)``. -Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption. -Pattern 1 ``/(Rabsolu a)``; Rewrite <- (Rabsolu_Rinv a Hyp_a). -Rewrite <- Rabsolu_mult; Rewrite Rmult_Rplus_distr; Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym; [Rewrite Rmult_1l | Assumption]; Rewrite (Rmult_sym ``/a``); Rewrite (Rmult_sym ``/(Rabsolu a)``); Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr1; Rewrite Ropp_Ropp; Unfold Rminus Rdiv in H6; Apply H6; Unfold ge; Apply le_trans with n0; [Exact H7 | Apply le_n_Sn]. -Rewrite (decomp_sum [i:nat]``(sin_n i)*(pow (Rsqr a) i)`` (S n0)). -Replace (sin_n O) with R1. -Simpl; Rewrite Rmult_1r; Unfold Rminus; Rewrite Ropp_distr1; Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_r; Rewrite Rplus_Ol; Rewrite Ropp_mul3; Rewrite <- Ropp_mul1; Rewrite scal_sum; Apply sum_eq. -Intros; Unfold sin_n Un tg_alt; Replace ``(pow (-1) (S i))`` with ``-(pow (-1) i)``. -Replace ``(pow a (plus (mult (S (S O)) (S i)) (S O)))`` with ``(Rsqr a)*(pow (Rsqr a) i)*a``. -Unfold Rdiv; Ring. -Rewrite pow_add; Rewrite pow_Rsqr; Simpl; Ring. -Simpl; Ring. -Unfold sin_n; Unfold Rdiv; Simpl; Rewrite Rinv_R1; Rewrite Rmult_1r; Reflexivity. -Apply lt_O_Sn. -Unfold Rdiv; Apply Rmult_lt_pos. -Assumption. -Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption. -Unfold sin; Case (exist_sin (Rsqr a)). -Intros; Cut x==x0. -Intro; Rewrite H3; Unfold Rdiv. -Symmetry; Apply Rinv_r_simpl_m; Assumption. -Unfold sin_in in p; Unfold sin_in in s; EApply unicity_sum. -Apply p. -Apply s. -Intros; Elim H2; Intros. -Replace ``(sin a)-a`` with ``-(a-(sin a))``; [Idtac | Ring]. -Split; Apply Rle_Ropp1; Assumption. -Replace ``-(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n)))`` with ``-1*(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n)))``; [Rewrite scal_sum | Ring]. -Apply sum_eq; Intros; Unfold sin_term Un tg_alt; Replace ``(pow (-1) (S i))`` with ``-1*(pow (-1) i)``. -Unfold Rdiv; Ring. -Reflexivity. -Replace ``-(sum_f_R0 (tg_alt Un) (mult (S (S O)) n))`` with ``-1*(sum_f_R0 (tg_alt Un) (mult (S (S O)) n))``; [Rewrite scal_sum | Ring]. -Apply sum_eq; Intros. -Unfold sin_term Un tg_alt; Replace ``(pow (-1) (S i))`` with ``-1*(pow (-1) i)``. -Unfold Rdiv; Ring. -Reflexivity. -Replace (mult (2) (plus n (1))) with (S (S (mult (2) n))). -Reflexivity. -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Rewrite plus_INR; Repeat Rewrite S_INR; Ring. -Replace (plus (mult (2) n) (1)) with (S (mult (2) n)). -Reflexivity. -Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Intro; Elim H1; Intros. -Split. -Apply Rle_anti_compatibility with ``-a``. -Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Rewrite (Rplus_sym ``-a``); Apply H2. -Apply Rle_anti_compatibility with ``-a``. -Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Rewrite (Rplus_sym ``-a``); Apply H3. -Unfold sin_term; Simpl; Unfold Rdiv; Rewrite Rinv_R1; Ring. -Replace (mult (2) (plus n (1))) with (S (S (mult (2) n))). -Apply lt_O_Sn. -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Rewrite plus_INR; Repeat Rewrite S_INR; Ring. -Replace (plus (mult (2) n) (1)) with (S (mult (2) n)). -Apply lt_O_Sn. -Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Inversion H; [Assumption | Elim Hyp_a; Symmetry; Assumption]. -Qed. - -(**********) -Lemma cos_bound : (a:R; n:nat) `` -PI/2 <= a``->``a <= PI/2``->``(cos_approx a (plus (mult (S (S O)) n) (S O))) <= (cos a) <= (cos_approx a (mult (S (S O)) (plus n (S O))))``. -Cut ((a:R; n:nat) ``0 <= a``->``a <= PI/2``->``(cos_approx a (plus (mult (S (S O)) n) (S O))) <= (cos a) <= (cos_approx a (mult (S (S O)) (plus n (S O))))``) -> ((a:R; n:nat) `` -PI/2 <= a``->``a <= PI/2``->``(cos_approx a (plus (mult (S (S O)) n) (S O))) <= (cos a) <= (cos_approx a (mult (S (S O)) (plus n (S O))))``). -Intros H a n; Apply H. -Intros; Unfold cos_approx. -Rewrite (decomp_sum (cos_term a0) (plus (mult (S (S O)) n0) (S O))). -Rewrite (decomp_sum (cos_term a0) (mult (S (S O)) (plus n0 (S O)))). -Replace (cos_term a0 O) with R1. -Cut (Rle (sum_f_R0 [i:nat](cos_term a0 (S i)) (pred (plus (mult (S (S O)) n0) (S O)))) ``(cos a0)-1``)/\(Rle ``(cos a0)-1`` (sum_f_R0 [i:nat](cos_term a0 (S i)) (pred (mult (S (S O)) (plus n0 (S O)))))) -> (Rle (Rplus R1 (sum_f_R0 [i:nat](cos_term a0 (S i)) (pred (plus (mult (S (S O)) n0) (S O))))) (cos a0))/\(Rle (cos a0) (Rplus R1 (sum_f_R0 [i:nat](cos_term a0 (S i)) (pred (mult (S (S O)) (plus n0 (S O))))))). -Intro; Apply H2. -Pose Un := [n:nat]``(pow a0 (mult (S (S O)) (S n)))/(INR (fact (mult (S (S O)) (S n))))``. -Replace (pred (plus (mult (S (S O)) n0) (S O))) with (mult (S (S O)) n0). -Replace (pred (mult (S (S O)) (plus n0 (S O)))) with (S (mult (S (S O)) n0)). -Replace (sum_f_R0 [i:nat](cos_term a0 (S i)) (mult (S (S O)) n0)) with ``-(sum_f_R0 (tg_alt Un) (mult (S (S O)) n0))``. -Replace (sum_f_R0 [i:nat](cos_term a0 (S i)) (S (mult (S (S O)) n0))) with ``-(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n0)))``. -Cut ``(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n0)))<=1-(cos a0)<=(sum_f_R0 (tg_alt Un) (mult (S (S O)) n0))``->`` -(sum_f_R0 (tg_alt Un) (mult (S (S O)) n0)) <= (cos a0)-1 <= -(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n0)))``. -Intro; Apply H3. -Apply alternated_series_ineq. -Unfold Un_decreasing; Intro; Unfold Un. -Cut (mult (S (S O)) (S (S n1)))=(S (S (mult (S (S O)) (S n1)))). -Intro; Rewrite H4; Replace ``(pow a0 (S (S (mult (S (S O)) (S n1)))))`` with ``(pow a0 (mult (S (S O)) (S n1)))*(a0*a0)``. -Unfold Rdiv; Rewrite Rmult_assoc; Apply Rle_monotony. -Apply pow_le; Assumption. -Apply Rle_monotony_contra with ``(INR (fact (S (S (mult (S (S O)) (S n1))))))``. -Rewrite <- H4; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H6 := (sym_eq ? ? ? H5); Elim (fact_neq_0 ? H6). -Rewrite <- H4; Rewrite (Rmult_sym ``(INR (fact (mult (S (S O)) (S (S n1)))))``); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r; Rewrite H4; Do 2 Rewrite fact_simpl; Do 2 Rewrite mult_INR; Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r; Do 2 Rewrite S_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Simpl; Replace ``((0+1+1)*((INR n1)+1)+1+1)*((0+1+1)*((INR n1)+1)+1)`` 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 | SqRing]. -Replace ``a0*a0`` with (Rsqr a0); [Idtac | Reflexivity]. -Apply Rsqr_incr_1. -Apply Rle_trans with ``PI/2``. -Assumption. -Unfold Rdiv; Apply Rle_monotony_contra with ``2``. -Sup0. -Rewrite <- Rmult_assoc; Rewrite Rinv_r_simpl_m. -Replace ``2*2`` with ``4``; [Apply PI_4 | Ring]. -DiscrR. -Assumption. -Left; Sup0. -Pattern 1 ``4``; Rewrite <- Rplus_Or; Replace ``12`` with ``4+8``; [Apply Rle_compatibility; Left; Sup0 | Ring]. -Rewrite <- (Rplus_sym ``12``); Pattern 1 ``12``; Rewrite <- Rplus_Or; Apply Rle_compatibility. -Apply ge0_plus_ge0_is_ge0. -Repeat Apply Rmult_le_pos. -Left; Sup0. -Left; Sup0. -Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity]. -Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity]. -Apply Rmult_le_pos. -Left; Sup0. -Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity]. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Simpl; Ring. -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Assert H4 := (cv_speed_pow_fact a0); Unfold Un; Unfold Un_cv in H4; Unfold R_dist in H4; Unfold Un_cv; Unfold R_dist; Intros; Elim (H4 eps H5); Intros N H6; Exists N; Intros. -Apply H6; Unfold ge; Apply le_trans with (mult (2) (S N)). -Apply le_trans with (mult (2) N). -Apply le_n_2n. -Apply mult_le; Apply le_n_Sn. -Apply mult_le; Apply le_n_S; Assumption. -Assert X := (exist_cos (Rsqr a0)); Elim X; Intros. -Cut ``x==(cos a0)``. -Intro; Rewrite H4 in p; Unfold cos_in in p; Unfold infinit_sum in p; Unfold R_dist in p; Unfold Un_cv; Unfold R_dist; Intros. -Elim (p ? H5); Intros N H6. -Exists N; Intros. -Replace (sum_f_R0 (tg_alt Un) n1) with (Rminus R1 (sum_f_R0 [i:nat]``(cos_n i)*(pow (Rsqr a0) i)`` (S n1))). -Unfold Rminus; Rewrite Ropp_distr1; Rewrite Ropp_Ropp; Repeat Rewrite Rplus_assoc; Rewrite (Rplus_sym R1); Rewrite (Rplus_sym ``-1``); Repeat Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr1; Rewrite Ropp_Ropp; Unfold Rminus in H6; Apply H6. -Unfold ge; Apply le_trans with n1. -Exact H7. -Apply le_n_Sn. -Rewrite (decomp_sum [i:nat]``(cos_n i)*(pow (Rsqr a0) i)`` (S n1)). -Replace (cos_n O) with R1. -Simpl; Rewrite Rmult_1r; Unfold Rminus; Rewrite Ropp_distr1; Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_r; Rewrite Rplus_Ol; Replace (Ropp (sum_f_R0 [i:nat]``(cos_n (S i))*((Rsqr a0)*(pow (Rsqr a0) i))`` n1)) with (Rmult ``-1`` (sum_f_R0 [i:nat]``(cos_n (S i))*((Rsqr a0)*(pow (Rsqr a0) i))`` n1)); [Idtac | Ring]; Rewrite scal_sum; Apply sum_eq; Intros; Unfold cos_n Un tg_alt. -Replace ``(pow (-1) (S i))`` with ``-(pow (-1) i)``. -Replace ``(pow a0 (mult (S (S O)) (S i)))`` with ``(Rsqr a0)*(pow (Rsqr a0) i)``. -Unfold Rdiv; Ring. -Rewrite pow_Rsqr; Reflexivity. -Simpl; Ring. -Unfold cos_n; Unfold Rdiv; Simpl; Rewrite Rinv_R1; Rewrite Rmult_1r; Reflexivity. -Apply lt_O_Sn. -Unfold cos; Case (exist_cos (Rsqr a0)); Intros; Unfold cos_in in p; Unfold cos_in in c; EApply unicity_sum. -Apply p. -Apply c. -Intros; Elim H3; Intros; Replace ``(cos a0)-1`` with ``-(1-(cos a0))``; [Idtac | Ring]. -Split; Apply Rle_Ropp1; Assumption. -Replace ``-(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n0)))`` with ``-1*(sum_f_R0 (tg_alt Un) (S (mult (S (S O)) n0)))``; [Rewrite scal_sum | Ring]. -Apply sum_eq; Intros; Unfold cos_term Un tg_alt; Replace ``(pow (-1) (S i))`` with ``-1*(pow (-1) i)``. -Unfold Rdiv; Ring. -Reflexivity. -Replace ``-(sum_f_R0 (tg_alt Un) (mult (S (S O)) n0))`` with ``-1*(sum_f_R0 (tg_alt Un) (mult (S (S O)) n0))``; [Rewrite scal_sum | Ring]; Apply sum_eq; Intros; Unfold cos_term Un tg_alt; Replace ``(pow (-1) (S i))`` with ``-1*(pow (-1) i)``. -Unfold Rdiv; Ring. -Reflexivity. -Replace (mult (2) (plus n0 (1))) with (S (S (mult (2) n0))). -Reflexivity. -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Rewrite plus_INR; Repeat Rewrite S_INR; Ring. -Replace (plus (mult (2) n0) (1)) with (S (mult (2) n0)). -Reflexivity. -Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Intro; Elim H2; Intros; Split. -Apply Rle_anti_compatibility with ``-1``. -Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Rewrite (Rplus_sym ``-1``); Apply H3. -Apply Rle_anti_compatibility with ``-1``. -Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Rewrite (Rplus_sym ``-1``); Apply H4. -Unfold cos_term; Simpl; Unfold Rdiv; Rewrite Rinv_R1; Ring. -Replace (mult (2) (plus n0 (1))) with (S (S (mult (2) n0))). -Apply lt_O_Sn. -Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR; Rewrite plus_INR; Repeat Rewrite S_INR; Ring. -Replace (plus (mult (2) n0) (1)) with (S (mult (2) n0)). -Apply lt_O_Sn. -Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Intros; Case (total_order_T R0 a); Intro. -Elim s; Intro. -Apply H; [Left; Assumption | Assumption]. -Apply H; [Right; Assumption | Assumption]. -Cut ``0< -a``. -Intro; Cut (x:R;n:nat) (cos_approx x n)==(cos_approx ``-x`` n). -Intro; Rewrite H3; Rewrite (H3 a (mult (S (S O)) (plus n (S O)))); Rewrite cos_sym; Apply H. -Left; Assumption. -Rewrite <- (Ropp_Ropp ``PI/2``); Apply Rle_Ropp1; Unfold Rdiv; Unfold Rdiv in H0; Rewrite <- Ropp_mul1; Exact H0. -Intros; Unfold cos_approx; Apply sum_eq; Intros; Unfold cos_term; Do 2 Rewrite pow_Rsqr; Rewrite Rsqr_neg; Unfold Rdiv; Reflexivity. -Apply Rgt_RO_Ropp; Assumption. -Qed. |