From 13aedc7b3ecd257ee83123d43ad06bd1e494635f Mon Sep 17 00:00:00 2001 From: desmettr Date: Fri, 5 Jul 2002 15:41:41 +0000 Subject: sin_plus prouve (a partir de cos_plus) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2843 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Reals/Rtrigo.v | 100 +++++++++++++++++++++++++++++++++--------------- 1 file changed, 69 insertions(+), 31 deletions(-) (limited to 'theories/Reals/Rtrigo.v') diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 5c5c76567..44a020d57 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -21,6 +21,11 @@ Require Binome. Require Export Rtrigo_def. Require Export Rtrigo_alt. +(* The two remaining axioms *) +Axiom cos_plus : (x,y:R) ``(cos (x+y))==(cos x)*(cos y)-(sin x)*(sin y)``. + +Axiom sin_PI2 : ``(sin (PI/2))==1``. + (* Here, we have the euclidian division *) (* This lemma is used in the proof of sin_eq_0 : (sin x)=0<->x=kPI *) Lemma euclidian_division : (x,y:R) ``y<>0`` -> (EXT k:Z | (EXT r : R | ``x==(IZR k)*y+r``/\``0<=r<(Rabsolu y)``)). @@ -74,11 +79,75 @@ Lemma PI_neq0 : ~``PI==0``. Red; Intro; Assert H0 := PI_RGT_0; Rewrite H in H0; Elim (Rlt_antirefl ? H0). 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. +Qed. + (**********) Lemma sin2_cos2 : (x:R) ``(Rsqr (sin x)) + (Rsqr (cos x))==1``. Intro; Unfold Rsqr; Rewrite Rplus_sym; Rewrite <- (cos_minus x x); Unfold Rminus; Rewrite Rplus_Ropp_r; Apply cos_0. Qed. +Lemma cos2 : (x:R) ``(Rsqr (cos x))==1-(Rsqr (sin x))``. +Intro x; Generalize (sin2_cos2 x); Intro H1; Rewrite <- H1; Unfold Rminus; Rewrite <- (Rplus_sym (Rsqr (cos x))); Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r; Symmetry; Apply Rplus_Or. +Qed. + +(**********) +Lemma cos_PI2 : ``(cos (PI/2))==0``. +Apply Rsqr_eq_0; Rewrite cos2; Rewrite sin_PI2; Rewrite Rsqr_1; Unfold Rminus; Apply Rplus_Ropp_r. +Qed. + +(**********) +Lemma cos_PI : ``(cos PI)==-1``. +Replace ``PI`` with ``PI/2+PI/2``. +Rewrite cos_plus. +Rewrite sin_PI2; Rewrite cos_PI2. +Ring. +Symmetry; Apply double_var. +Qed. + +Lemma sin_PI : ``(sin PI)==0``. +Assert H := (sin2_cos2 PI). +Rewrite cos_PI in H. +Rewrite <- Rsqr_neg in H. +Rewrite Rsqr_1 in H. +Cut (Rsqr (sin PI))==R0. +Intro; Apply (Rsqr_eq_0 ? H0). +Apply r_Rplus_plus with R1. +Rewrite Rplus_Or; Rewrite Rplus_sym; Exact H. +Qed. + +(**********) +Lemma neg_cos : (x:R) ``(cos (x+PI))==-(cos x)``. +Intro x; Rewrite -> cos_plus; Rewrite -> sin_PI; Rewrite -> cos_PI; Ring. +Qed. + +(**********) +Lemma sin_cos : (x:R) ``(sin x)==-(cos (PI/2+x))``. +Intro x; Rewrite -> cos_plus; Rewrite -> sin_PI2; Rewrite -> cos_PI2; Ring. +Qed. + +(**********) +Lemma sin_plus : (x,y:R) ``(sin (x+y))==(sin x)*(cos y)+(cos x)*(sin y)``. +Intros. +Rewrite (sin_cos ``x+y``). +Replace ``PI/2+(x+y)`` with ``(PI/2+x)+y``; [Rewrite cos_plus | Ring]. +Rewrite (sin_cos ``PI/2+x``). +Replace ``PI/2+(PI/2+x)`` with ``x+PI``. +Rewrite neg_cos. +Replace (cos ``PI/2+x``) with ``-(sin x)``. +Ring. +Rewrite sin_cos; Rewrite Ropp_Ropp; Reflexivity. +Pattern 1 PI; Rewrite (double_var PI); Ring. +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. +Qed. + (**********) Definition tan [x:R] : R := ``(sin x)/(cos x)``. @@ -105,10 +174,6 @@ Qed. (* Some properties of cos, sin and tan *) (*******************************************************) -Lemma cos2 : (x:R) ``(Rsqr (cos x))==1-(Rsqr (sin x))``. -Intro x; Generalize (sin2_cos2 x); Intro H1; Rewrite <- H1; Unfold Rminus; Rewrite <- (Rplus_sym (Rsqr (cos x))); Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r; Symmetry; Apply Rplus_Or. -Qed. - Lemma sin2 : (x:R) ``(Rsqr (sin x))==1-(Rsqr (cos x))``. Intro x; Generalize (cos2 x); Intro H1; Rewrite -> H1. Unfold Rminus; Rewrite Ropp_distr1; Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_r; Rewrite Rplus_Ol; Symmetry; Apply Ropp_Ropp. @@ -163,25 +228,6 @@ Assumption. Rewrite tan_neg; Unfold Rminus; Rewrite <- Ropp_mul1; Rewrite Ropp_mul2; Assumption. Qed. -Lemma cos_PI2 : ``(cos (PI/2))==0``. -Apply Rsqr_eq_0; Rewrite cos2; Rewrite sin_PI2; Rewrite Rsqr_1; Unfold Rminus; Apply Rplus_Ropp_r. -Qed. - -Lemma sin_PI : ``(sin PI)==0``. -Replace ``PI`` with ``2*(PI/2)``. -Rewrite -> sin_2a; Rewrite -> sin_PI2; Rewrite -> cos_PI2; Ring. -Unfold Rdiv. -Repeat Rewrite <- Rmult_assoc; Apply Rinv_r_simpl_m. -Apply aze. -Qed. - -Lemma cos_PI : ``(cos PI)==(-1)``. -Replace ``PI`` with ``2*(PI/2)``. -Rewrite -> cos_2a; Rewrite -> sin_PI2; Rewrite -> cos_PI2. -Ring. -Unfold Rdiv; Rewrite <- Rmult_assoc; Apply Rinv_r_simpl_m; Apply aze. -Qed. - Lemma tan_PI : ``(tan PI)==0``. Unfold tan; Rewrite -> sin_PI; Rewrite -> cos_PI. Unfold Rdiv; Apply Rmult_Ol. @@ -213,10 +259,6 @@ Lemma tan_2PI : ``(tan (2*PI))==0``. Unfold tan; Rewrite sin_2PI; Unfold Rdiv; Apply Rmult_Ol. Qed. -Lemma neg_cos : (x:R) ``(cos (x+PI))==-(cos x)``. -Intro x; Rewrite -> cos_plus; Rewrite -> sin_PI; Rewrite -> cos_PI; Ring. -Qed. - Lemma neg_sin : (x:R) ``(sin (x+PI))==-(sin x)``. Intro x; Rewrite -> sin_plus; Rewrite -> sin_PI; Rewrite -> cos_PI; Ring. Qed. @@ -249,10 +291,6 @@ Lemma cos_sin : (x:R) ``(cos x)==(sin (PI/2+x))``. Intro x; Rewrite -> sin_plus; Rewrite -> sin_PI2; Rewrite -> cos_PI2; Ring. Qed. -Lemma sin_cos : (x:R) ``(sin x)==-(cos (PI/2+x))``. -Intro x; Rewrite -> cos_plus; Rewrite -> sin_PI2; Rewrite -> cos_PI2; Ring. -Qed. - Lemma PI2_RGT_0 : ``0