Renommages dans Rtrigo_def

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3589 85f007b7-540e-0410-9357-904b9bb8a0f7

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.