1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Import Rbase.
Require Import Rtrigo1.
Require Import Rfunctions.
Require Import Lra.
Require Import Ranalysis_reg.
Local Open Scope R_scope.
(*********************************************************)
(** * Bounds of expressions with trigonometric functions *)
(*********************************************************)
Lemma sin2_bound : forall x,
0 <= (sin x)² <= 1.
Proof.
intros x.
rewrite <- Rsqr_1.
apply Rsqr_bounds_le.
apply SIN_bound.
Qed.
Lemma cos2_bound : forall x,
0 <= (cos x)² <= 1.
Proof.
intros x.
rewrite <- Rsqr_1.
apply Rsqr_bounds_le.
apply COS_bound.
Qed.
(*********************************************************)
(** * Express trigonometric functions with each other *)
(*********************************************************)
(** ** Express sin and cos with each other *)
Lemma cos_sin : forall x, cos x >=0 ->
cos x = sqrt(1 - (sin x)²).
Proof.
intros x H.
apply Rsqr_inj.
- lra.
- apply sqrt_pos.
- rewrite Rsqr_sqrt.
apply cos2.
pose proof sin2_bound x.
lra.
Qed.
Lemma cos_sin_opp : forall x, cos x <=0 ->
cos x = - sqrt(1 - (sin x)²).
Proof.
intros x H.
rewrite <- (Ropp_involutive (cos x)).
apply Ropp_eq_compat.
apply Rsqr_inj.
- lra.
- apply sqrt_pos.
- rewrite Rsqr_sqrt.
rewrite <- Rsqr_neg.
apply cos2.
pose proof sin2_bound x.
lra.
Qed.
Lemma cos_sin_Rabs : forall x,
Rabs (cos x) = sqrt(1 - (sin x)²).
Proof.
intros x.
unfold Rabs.
destruct (Rcase_abs (cos x)).
- rewrite <- (Ropp_involutive (sqrt (1 - (sin x)²))).
apply Ropp_eq_compat.
apply cos_sin_opp; lra.
- apply cos_sin; assumption.
Qed.
Lemma sin_cos : forall x, sin x >=0 ->
sin x = sqrt(1 - (cos x)²).
Proof.
intros x H.
apply Rsqr_inj.
- lra.
- apply sqrt_pos.
- rewrite Rsqr_sqrt.
apply sin2.
pose proof cos2_bound x.
lra.
Qed.
Lemma sin_cos_opp : forall x, sin x <=0 ->
sin x = - sqrt(1 - (cos x)²).
Proof.
intros x H.
rewrite <- (Ropp_involutive (sin x)).
apply Ropp_eq_compat.
apply Rsqr_inj.
- lra.
- apply sqrt_pos.
- rewrite Rsqr_sqrt.
rewrite <- Rsqr_neg.
apply sin2.
pose proof cos2_bound x.
lra.
Qed.
Lemma sin_cos_Rabs : forall x,
Rabs (sin x) = sqrt(1 - (cos x)²).
Proof.
intros x.
unfold Rabs.
destruct (Rcase_abs (sin x)).
- rewrite <- ( Ropp_involutive (sqrt (1 - (cos x)²))).
apply Ropp_eq_compat.
apply sin_cos_opp; lra.
- apply sin_cos; assumption.
Qed.
(** ** Express tan with sin and cos *)
Lemma tan_sin : forall x, 0 <= cos x ->
tan x = sin x / sqrt (1 - (sin x)²).
Proof.
intros x H.
unfold tan.
rewrite <- (sqrt_Rsqr (cos x)) by assumption.
rewrite <- (cos2 x).
reflexivity.
Qed.
Lemma tan_sin_opp : forall x, 0 > cos x ->
tan x = - (sin x / sqrt (1 - (sin x)²)).
Proof.
intros x H.
unfold tan.
rewrite cos_sin_opp by lra.
apply Rdiv_opp_r.
Qed.
(** Note: tan_sin_Rabs wouldn't make a lot of sense, because one would need Rabs on both sides *)
Lemma tan_cos : forall x, 0 <= sin x ->
tan x = sqrt (1 - (cos x)²) / cos x.
Proof.
intros x H.
unfold tan.
rewrite <- (sqrt_Rsqr (sin x)) by assumption.
rewrite <- (sin2 x).
reflexivity.
Qed.
Lemma tan_cos_opp : forall x, 0 >= sin x ->
tan x = - sqrt (1 - (cos x)²) / cos x.
Proof.
intros x H.
unfold tan.
rewrite sin_cos_opp by lra.
reflexivity.
Qed.
(** ** Express sin and cos with tan *)
Lemma sin_tan : forall x, 0 < cos x ->
sin x = tan x / sqrt (1 + (tan x)²).
Proof.
intros.
assert(Hcosle:0<=cos x) by lra.
pose proof tan_sin x Hcosle as Htan.
pose proof (sin2 x); pose proof Rsqr_pos_lt (cos x).
rewrite Htan.
unfold Rdiv at 1 2.
rewrite Rmult_assoc, <- Rinv_mult.
rewrite <- sqrt_mult_alt by lra.
rewrite Rsqr_div', Rsqr_sqrt by lra.
field_simplify ((1 - (sin x)²) * (1 + (sin x)² / (1 - (sin x)²))).
rewrite sqrt_1.
field.
lra.
Qed.
Lemma cos_tan : forall x, 0 < cos x ->
cos x = 1 / sqrt (1 + (tan x)²).
Proof.
intros.
destruct (Rcase_abs (sin x)) as [Hsignsin|Hsignsin].
- assert(Hsinle:0>=sin x) by lra.
pose proof tan_cos_opp x Hsinle as Htan.
rewrite Htan.
rewrite Rsqr_div'.
rewrite <- Rsqr_neg.
rewrite Rsqr_sqrt.
field_simplify( 1 + (1 - (cos x)²) / (cos x)² ).
rewrite sqrt_div_alt.
rewrite sqrt_1.
field_simplify_eq.
rewrite sqrt_Rsqr.
reflexivity.
all: pose proof cos2_bound x.
all: pose proof Rsqr_pos_lt (cos x) ltac:(lra).
all: pose proof sqrt_lt_R0 (cos x)² ltac:(assumption).
all: lra.
- assert(Hsinge:0<=sin x) by lra.
pose proof tan_cos x Hsinge as Htan.
rewrite Htan.
rewrite Rsqr_div'.
rewrite Rsqr_sqrt.
field_simplify( 1 + (1 - (cos x)²) / (cos x)² ).
rewrite sqrt_div_alt.
rewrite sqrt_1.
field_simplify_eq.
rewrite sqrt_Rsqr.
reflexivity.
all: pose proof cos2_bound x.
all: pose proof Rsqr_pos_lt (cos x) ltac:(lra).
all: pose proof sqrt_lt_R0 (cos x)² ltac:(assumption).
all: lra.
Qed.
(*********************************************************)
(** * Additional shift lemmas for sin, cos, tan *)
(*********************************************************)
Lemma sin_pi_minus : forall x,
sin (PI - x) = sin x.
Proof.
intros x.
rewrite sin_minus, cos_PI, sin_PI.
ring.
Qed.
Lemma sin_pi_plus : forall x,
sin (PI + x) = - sin x.
Proof.
intros x.
rewrite sin_plus, cos_PI, sin_PI.
ring.
Qed.
Lemma cos_pi_minus : forall x,
cos (PI - x) = - cos x.
Proof.
intros x.
rewrite cos_minus, cos_PI, sin_PI.
ring.
Qed.
Lemma cos_pi_plus : forall x,
cos (PI + x) = - cos x.
Proof.
intros x.
rewrite cos_plus, cos_PI, sin_PI.
ring.
Qed.
Lemma tan_pi_minus : forall x, cos x <> 0 ->
tan (PI - x) = - tan x.
Proof.
intros x H.
unfold tan; rewrite sin_pi_minus, cos_pi_minus.
field; assumption.
Qed.
Lemma tan_pi_plus : forall x, cos x <> 0 ->
tan (PI + x) = tan x.
Proof.
intros x H.
unfold tan; rewrite sin_pi_plus, cos_pi_plus.
field; assumption.
Qed.
|
