From 096310efb4266fe89455d473f704ec6c7ed5a97c Mon Sep 17 00:00:00 2001 From: desmettr Date: Wed, 22 Jan 2003 16:30:04 +0000 Subject: Renommages dans Rtrigo_def git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3589 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Reals/Rtrigo.v | 8 ++++---- theories/Reals/Rtrigo_alt.v | 2 +- theories/Reals/Rtrigo_def.v | 19 ++++++++----------- theories/Reals/Rtrigo_reg.v | 4 ++-- 4 files changed, 15 insertions(+), 18 deletions(-) diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 631757abe..8210b35f1 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -31,7 +31,7 @@ Qed. (**********) Lemma cos_minus : (x,y:R) ``(cos (x-y))==(cos x)*(cos y)+(sin x)*(sin y)``. Intros; Unfold Rminus; Rewrite cos_plus. -Rewrite <- cos_paire; Rewrite sin_impaire; Ring. +Rewrite <- cos_sym; Rewrite sin_antisym; Ring. Qed. (**********) @@ -94,7 +94,7 @@ Qed. Lemma sin_minus : (x,y:R) ``(sin (x-y))==(sin x)*(cos y)-(cos x)*(sin y)``. Intros; Unfold Rminus; Rewrite sin_plus. -Rewrite <- cos_paire; Rewrite sin_impaire; Ring. +Rewrite <- cos_sym; Rewrite sin_antisym; Ring. Qed. (**********) @@ -151,11 +151,11 @@ Repeat Rewrite double; Intros; Repeat Rewrite double; Rewrite double in H0; Appl Qed. Lemma sin_neg : (x:R) ``(sin (-x))==-(sin x)``. -Apply sin_impaire. +Apply sin_antisym. Qed. Lemma cos_neg : (x:R) ``(cos (-x))==(cos x)``. -Intro; Symmetry; Apply cos_paire. +Intro; Symmetry; Apply cos_sym. Qed. Lemma tan_0 : ``(tan 0)==0``. diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index 74526c8ee..be9a6f872 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -284,7 +284,7 @@ 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_paire; Apply H. +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. diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 038f1efb7..554a2059e 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -38,7 +38,7 @@ Intros; Apply pow_ne_zero. Red; Intro; Rewrite H0 in H; Elim (lt_n_n ? H). Qed. -(*i Calcul de $e^0$ *) +(*i Calculus of $e^0$ *) Lemma exist_exp0 : (SigT R [l:R](exp_in R0 l)). Apply Specif.existT with R1. Unfold exp_in; Unfold infinit_sum; Intros. @@ -81,7 +81,6 @@ Unfold sinh; Rewrite Ropp_O; Rewrite exp_0. Unfold Rminus Rdiv; Rewrite Rplus_Ropp_r; Apply Rmult_Ol. Qed. -(* TG de la série entière définissant COS *) Definition cos_n [n:nat] : R := ``(pow (-1) n)/(INR (fact (mult (S (S O)) n)))``. Lemma simpl_cos_n : (n:nat) (Rdiv (cos_n (S n)) (cos_n n))==(Ropp (Rinv (INR (mult (mult (2) (S n)) (plus (mult (2) n) (1)))))). @@ -142,7 +141,6 @@ Assert H0 := (archimed ``/eps``). Elim H0; Intros; Assumption. Qed. -(* Convergence de la SE de TG cos_n *) Lemma Alembert_cos : (Un_cv [n:nat]``(Rabsolu (cos_n (S n))/(cos_n n))`` R0). Unfold Un_cv; Intros. Assert H0 := (archimed_cor1 eps H). @@ -207,11 +205,11 @@ Intro; Generalize (Alembert_C3 cos_n x cosn_no_R0 Alembert_cos). Unfold Pser cos_in; Trivial. Qed. -(* Définition du cosinus *) +(* Definition of cosinus *) (*************************) Definition cos : R -> R := [x:R](Cases (exist_cos (Rsqr x)) of (Specif.existT a b) => a end). -(* TG de la série entière définissant SIN *) + Definition sin_n [n:nat] : R := ``(pow (-1) n)/(INR (fact (plus (mult (S (S O)) n) (S O))))``. Lemma simpl_sin_n : (n:nat) (Rdiv (sin_n (S n)) (sin_n n))==(Ropp (Rinv (INR (mult (plus (mult (2) (S n)) (1)) (mult (2) (S n)))))). @@ -250,7 +248,6 @@ Apply pow_nonzero; DiscrR. Apply Rinv_neq_R0; Apply INR_fact_neq_0. Qed. -(* Convergence de la SE de TG sin_n *) Lemma Alembert_sin : (Un_cv [n:nat]``(Rabsolu (sin_n (S n))/(sin_n n))`` R0). Unfold Un_cv; Intros; Assert H0 := (archimed_cor1 eps H). Elim H0; Intros; Exists x. @@ -306,20 +303,20 @@ Unfold Pser sin_n; Trivial. Qed. (***********************) -(* Définition du sinus *) +(* Definition of sinus *) Definition sin : R -> R := [x:R](Cases (exist_sin (Rsqr x)) of (Specif.existT a b) => ``x*a`` end). (*********************************************) -(* PROPRIETES *) +(* PROPERTIES *) (*********************************************) -Lemma cos_paire : (x:R) ``(cos x)==(cos (-x))``. +Lemma cos_sym : (x:R) ``(cos x)==(cos (-x))``. Intros; Unfold cos; Replace ``(Rsqr (-x))`` with (Rsqr x). Reflexivity. Apply Rsqr_neg. Qed. -Lemma sin_impaire : (x:R)``(sin (-x))==-(sin x)``. +Lemma sin_antisym : (x:R)``(sin (-x))==-(sin x)``. Intro; Unfold sin; Replace ``(Rsqr (-x))`` with (Rsqr x); [Idtac | Apply Rsqr_neg]. Case (exist_sin (Rsqr x)); Intros; Ring. Qed. @@ -346,7 +343,7 @@ Apply Hrecn; Unfold ge; Apply le_O_n. Simpl; Ring. Defined. -(* Calcul de (cos 0) *) +(* Calculus of (cos 0) *) Lemma cos_0 : ``(cos 0)==1``. Cut (cos_in R0 (cos R0)). Cut (cos_in R0 R1). diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index 620035ceb..7694cf0a2 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -232,7 +232,7 @@ Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rsqr_pos_lt Assert H0 := (cond_pos r); Red; Intro; Rewrite H1 in H0; Elim (Rlt_antirefl ? H0). Qed. -(* (sin h)/h -> 1 quand h -> 0 *) +(* (sin h)/h -> 1 when h -> 0 *) Lemma derivable_pt_lim_sin_0 : (derivable_pt_lim sin R0 R1). Unfold derivable_pt_lim; Intros. Pose fn := [N:nat][x:R]``(pow ( -1) N)/(INR (fact (plus (mult (S (S O)) N) (S O))))*(pow x (mult (S (S O)) N))``. @@ -298,7 +298,7 @@ Apply (CVN_R_CVS ? X). Apply CVN_R_sin; Unfold fn; Reflexivity. Qed. -(* ((cos h)-1)/h -> 0 quand h -> 0 *) +(* ((cos h)-1)/h -> 0 when h -> 0 *) Lemma derivable_pt_lim_cos_0 : (derivable_pt_lim cos ``0`` ``0``). Unfold derivable_pt_lim; Intros. Assert H0 := derivable_pt_lim_sin_0. -- cgit v1.2.3