← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Reals/Cos_rel.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Reals/Cos_rel.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: Cos_rel.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
10
 
 
11
Require Import Rbase.
 
12
Require Import Rfunctions.
 
13
Require Import SeqSeries.
 
14
Require Import Rtrigo_def.
 
15
Open Local Scope R_scope.
 
16
 
 
17
Definition A1 (x:R) (N:nat) : R :=
 
18
  sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * x ^ (2 * k)) N. 
 
19
 
 
20
Definition B1 (x:R) (N:nat) : R :=
 
21
  sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * x ^ (2 * k + 1))
 
22
    N. 
 
23
 
 
24
Definition C1 (x y:R) (N:nat) : R :=
 
25
  sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * (x + y) ^ (2 * k)) N. 
 
26
 
 
27
Definition Reste1 (x y:R) (N:nat) : R :=
 
28
  sum_f_R0
 
29
    (fun k:nat =>
 
30
       sum_f_R0
 
31
         (fun l:nat =>
 
32
            (-1) ^ S (l + k) / INR (fact (2 * S (l + k))) *
 
33
            x ^ (2 * S (l + k)) * ((-1) ^ (N - l) / INR (fact (2 * (N - l)))) *
 
34
            y ^ (2 * (N - l))) (pred (N - k))) (pred N).
 
35
 
 
36
Definition Reste2 (x y:R) (N:nat) : R :=
 
37
  sum_f_R0
 
38
    (fun k:nat =>
 
39
       sum_f_R0
 
40
         (fun l:nat =>
 
41
            (-1) ^ S (l + k) / INR (fact (2 * S (l + k) + 1)) *
 
42
            x ^ (2 * S (l + k) + 1) *
 
43
            ((-1) ^ (N - l) / INR (fact (2 * (N - l) + 1))) *
 
44
            y ^ (2 * (N - l) + 1)) (pred (N - k))) (
 
45
    pred N).
 
46
 
 
47
Definition Reste (x y:R) (N:nat) : R := Reste2 x y N - Reste1 x y (S N).
 
48
 
 
49
(* Here is the main result that will be used to prove that (cos (x+y))=(cos x)(cos y)-(sin x)(sin y) *)
 
50
Theorem cos_plus_form :
 
51
 forall (x y:R) (n:nat),
 
52
   (0 < n)%nat ->
 
53
   A1 x (S n) * A1 y (S n) - B1 x n * B1 y n + Reste x y n = C1 x y (S n). 
 
54
intros.
 
55
unfold A1, B1 in |- *.
 
56
rewrite
 
57
 (cauchy_finite (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * x ^ (2 * k))
 
58
    (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * y ^ (2 * k)) (
 
59
    S n)).
 
60
rewrite
 
61
 (cauchy_finite
 
62
    (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * x ^ (2 * k + 1))
 
63
    (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * y ^ (2 * k + 1)) n H)
 
64
 .
 
65
unfold Reste in |- *.
 
66
replace
 
67
 (sum_f_R0
 
68
    (fun k:nat =>
 
69
       sum_f_R0
 
70
         (fun l:nat =>
 
71
            (-1) ^ S (l + k) / INR (fact (2 * S (l + k))) *
 
72
            x ^ (2 * S (l + k)) *
 
73
            ((-1) ^ (S n - l) / INR (fact (2 * (S n - l))) *
 
74
             y ^ (2 * (S n - l)))) (pred (S n - k))) (
 
75
    pred (S n))) with (Reste1 x y (S n)).
 
76
replace
 
77
 (sum_f_R0
 
78
    (fun k:nat =>
 
79
       sum_f_R0
 
80
         (fun l:nat =>
 
81
            (-1) ^ S (l + k) / INR (fact (2 * S (l + k) + 1)) *
 
82
            x ^ (2 * S (l + k) + 1) *
 
83
            ((-1) ^ (n - l) / INR (fact (2 * (n - l) + 1)) *
 
84
             y ^ (2 * (n - l) + 1))) (pred (n - k))) (
 
85
    pred n)) with (Reste2 x y n).
 
86
replace
 
87
 (sum_f_R0
 
88
    (fun k:nat =>
 
89
       sum_f_R0
 
90
         (fun p:nat =>
 
91
            (-1) ^ p / INR (fact (2 * p)) * x ^ (2 * p) *
 
92
            ((-1) ^ (k - p) / INR (fact (2 * (k - p))) * y ^ (2 * (k - p))))
 
93
         k) (S n)) with
 
94
 (sum_f_R0
 
95
    (fun k:nat =>
 
96
       (-1) ^ k / INR (fact (2 * k)) *
 
97
       sum_f_R0
 
98
         (fun l:nat => C (2 * k) (2 * l) * x ^ (2 * l) * y ^ (2 * (k - l))) k)
 
99
    (S n)).
 
100
pose
 
101
 (sin_nnn :=
 
102
  fun n:nat =>
 
103
    match n with
 
104
    | O => 0
 
105
    | S p =>
 
106
        (-1) ^ S p / INR (fact (2 * S p)) *
 
107
        sum_f_R0
 
108
          (fun l:nat =>
 
109
             C (2 * S p) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (p - l))) p
 
110
    end).
 
111
ring_simplify.
 
112
unfold Rminus.
 
113
replace
 
114
(* (-   old ring compat *)
 
115
 (-
 
116
  sum_f_R0
 
117
    (fun k:nat =>
 
118
       sum_f_R0
 
119
         (fun p:nat =>
 
120
            (-1) ^ p / INR (fact (2 * p + 1)) * x ^ (2 * p + 1) *
 
121
            ((-1) ^ (k - p) / INR (fact (2 * (k - p) + 1)) *
 
122
             y ^ (2 * (k - p) + 1))) k) n) with (sum_f_R0 sin_nnn (S n)).
 
123
rewrite <- sum_plus.
 
124
unfold C1 in |- *.
 
125
apply sum_eq; intros.
 
126
induction  i as [| i Hreci].
 
127
simpl in |- *.
 
128
unfold C in |- *; simpl in |- *.
 
129
field; discrR.
 
130
unfold sin_nnn in |- *.
 
131
rewrite <- Rmult_plus_distr_l.
 
132
apply Rmult_eq_compat_l.
 
133
rewrite binomial.
 
134
pose (Wn := fun i0:nat => C (2 * S i) i0 * x ^ i0 * y ^ (2 * S i - i0)).
 
135
replace
 
136
 (sum_f_R0
 
137
    (fun l:nat => C (2 * S i) (2 * l) * x ^ (2 * l) * y ^ (2 * (S i - l)))
 
138
    (S i)) with (sum_f_R0 (fun l:nat => Wn (2 * l)%nat) (S i)).
 
139
replace
 
140
 (sum_f_R0
 
141
    (fun l:nat =>
 
142
       C (2 * S i) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (i - l))) i) with
 
143
 (sum_f_R0 (fun l:nat => Wn (S (2 * l))) i).
 
144
apply sum_decomposition.
 
145
apply sum_eq; intros.
 
146
unfold Wn in |- *.
 
147
apply Rmult_eq_compat_l.
 
148
replace (2 * S i - S (2 * i0))%nat with (S (2 * (i - i0))).
 
149
reflexivity.
 
150
omega.
 
151
apply sum_eq; intros.
 
152
unfold Wn in |- *.
 
153
apply Rmult_eq_compat_l.
 
154
replace (2 * S i - 2 * i0)%nat with (2 * (S i - i0))%nat.
 
155
reflexivity.
 
156
omega.
 
157
replace
 
158
 (-
 
159
  sum_f_R0
 
160
    (fun k:nat =>
 
161
       sum_f_R0
 
162
         (fun p:nat =>
 
163
            (-1) ^ p / INR (fact (2 * p + 1)) * x ^ (2 * p + 1) *
 
164
            ((-1) ^ (k - p) / INR (fact (2 * (k - p) + 1)) *
 
165
             y ^ (2 * (k - p) + 1))) k) n) with
 
166
 (-1 *
 
167
  sum_f_R0
 
168
    (fun k:nat =>
 
169
       sum_f_R0
 
170
         (fun p:nat =>
 
171
            (-1) ^ p / INR (fact (2 * p + 1)) * x ^ (2 * p + 1) *
 
172
            ((-1) ^ (k - p) / INR (fact (2 * (k - p) + 1)) *
 
173
             y ^ (2 * (k - p) + 1))) k) n);[idtac|ring].
 
174
rewrite scal_sum.
 
175
rewrite decomp_sum.
 
176
replace (sin_nnn 0%nat) with 0.
 
177
rewrite Rplus_0_l.
 
178
change (pred (S n)) with n.
 
179
   (* replace (pred (S n)) with n; [ idtac | reflexivity ]. *)
 
180
apply sum_eq; intros.
 
181
rewrite Rmult_comm.
 
182
unfold sin_nnn in |- *.
 
183
rewrite scal_sum.
 
184
rewrite scal_sum.
 
185
apply sum_eq; intros.
 
186
unfold Rdiv in |- *.
 
187
(*repeat rewrite Rmult_assoc.*)
 
188
(* rewrite (Rmult_comm (/ INR (fact (2 * S i)))). *)
 
189
repeat rewrite <- Rmult_assoc.
 
190
rewrite <- (Rmult_comm (/ INR (fact (2 * S i)))).
 
191
repeat rewrite <- Rmult_assoc.
 
192
replace (/ INR (fact (2 * S i)) * C (2 * S i) (S (2 * i0))) with
 
193
 (/ INR (fact (2 * i0 + 1)) * / INR (fact (2 * (i - i0) + 1))).
 
194
replace (S (2 * i0)) with (2 * i0 + 1)%nat; [ idtac | ring ].
 
195
replace (S (2 * (i - i0))) with (2 * (i - i0) + 1)%nat; [ idtac | ring ].
 
196
replace ((-1) ^ S i) with (-1 * (-1) ^ i0 * (-1) ^ (i - i0)).
 
197
ring.
 
198
simpl in |- *.
 
199
pattern i at 2 in |- *; replace i with (i0 + (i - i0))%nat.
 
200
rewrite pow_add.
 
201
ring.
 
202
symmetry  in |- *; apply le_plus_minus; assumption.
 
203
unfold C in |- *.
 
204
unfold Rdiv in |- *; repeat rewrite <- Rmult_assoc.
 
205
rewrite <- Rinv_l_sym.
 
206
rewrite Rmult_1_l.
 
207
rewrite Rinv_mult_distr.
 
208
replace (S (2 * i0)) with (2 * i0 + 1)%nat;
 
209
 [ apply Rmult_eq_compat_l | ring ].
 
210
replace (2 * S i - (2 * i0 + 1))%nat with (2 * (i - i0) + 1)%nat.
 
211
reflexivity.
 
212
omega.
 
213
apply INR_fact_neq_0.
 
214
apply INR_fact_neq_0.
 
215
apply INR_fact_neq_0.
 
216
reflexivity.
 
217
apply lt_O_Sn.
 
218
(* ring. *)
 
219
apply sum_eq; intros.
 
220
rewrite scal_sum.
 
221
apply sum_eq; intros.
 
222
unfold Rdiv in |- *.
 
223
repeat rewrite <- Rmult_assoc.
 
224
rewrite <- (Rmult_comm (/ INR (fact (2 * i)))).
 
225
repeat rewrite <- Rmult_assoc.
 
226
replace (/ INR (fact (2 * i)) * C (2 * i) (2 * i0)) with
 
227
 (/ INR (fact (2 * i0)) * / INR (fact (2 * (i - i0)))).
 
228
replace ((-1) ^ i) with ((-1) ^ i0 * (-1) ^ (i - i0)).
 
229
ring.
 
230
pattern i at 2 in |- *; replace i with (i0 + (i - i0))%nat.
 
231
rewrite pow_add.
 
232
ring.
 
233
symmetry  in |- *; apply le_plus_minus; assumption.
 
234
unfold C in |- *.
 
235
unfold Rdiv in |- *; repeat rewrite <- Rmult_assoc.
 
236
rewrite <- Rinv_l_sym.
 
237
rewrite Rmult_1_l.
 
238
rewrite Rinv_mult_distr.
 
239
replace (2 * i - 2 * i0)%nat with (2 * (i - i0))%nat.
 
240
reflexivity.
 
241
omega.
 
242
apply INR_fact_neq_0.
 
243
apply INR_fact_neq_0.
 
244
apply INR_fact_neq_0.
 
245
unfold Reste2 in |- *; apply sum_eq; intros.
 
246
apply sum_eq; intros.
 
247
unfold Rdiv in |- *; ring. 
 
248
unfold Reste1 in |- *; apply sum_eq; intros.
 
249
apply sum_eq; intros.
 
250
unfold Rdiv in |- *; ring.
 
251
apply lt_O_Sn.
 
252
Qed.
 
253
 
 
254
Lemma pow_sqr : forall (x:R) (i:nat), x ^ (2 * i) = (x * x) ^ i. 
 
255
intros. 
 
256
assert (H := pow_Rsqr x i).
 
257
unfold Rsqr in H; exact H.
 
258
Qed. 
 
259
 
 
260
Lemma A1_cvg : forall x:R, Un_cv (A1 x) (cos x). 
 
261
intro. 
 
262
assert (H := exist_cos (x * x)). 
 
263
elim H; intros. 
 
264
assert (p_i := p). 
 
265
unfold cos_in in p. 
 
266
unfold cos_n, infinite_sum in p. 
 
267
unfold R_dist in p. 
 
268
cut (cos x = x0). 
 
269
intro. 
 
270
rewrite H0. 
 
271
unfold Un_cv in |- *; unfold R_dist in |- *; intros. 
 
272
elim (p eps H1); intros. 
 
273
exists x1; intros. 
 
274
unfold A1 in |- *. 
 
275
replace
 
276
 (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * x ^ (2 * k)) n) with
 
277
 (sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i)) * (x * x) ^ i) n). 
 
278
apply H2; assumption. 
 
279
apply sum_eq. 
 
280
intros. 
 
281
replace ((x * x) ^ i) with (x ^ (2 * i)). 
 
282
reflexivity. 
 
283
apply pow_sqr. 
 
284
unfold cos in |- *. 
 
285
case (exist_cos (Rsqr x)). 
 
286
unfold Rsqr in |- *; intros. 
 
287
unfold cos_in in p_i. 
 
288
unfold cos_in in c. 
 
289
apply uniqueness_sum with (fun i:nat => cos_n i * (x * x) ^ i); assumption. 
 
290
Qed. 
 
291
 
 
292
Lemma C1_cvg : forall x y:R, Un_cv (C1 x y) (cos (x + y)). 
 
293
intros. 
 
294
assert (H := exist_cos ((x + y) * (x + y))). 
 
295
elim H; intros. 
 
296
assert (p_i := p). 
 
297
unfold cos_in in p. 
 
298
unfold cos_n, infinite_sum in p. 
 
299
unfold R_dist in p. 
 
300
cut (cos (x + y) = x0). 
 
301
intro. 
 
302
rewrite H0. 
 
303
unfold Un_cv in |- *; unfold R_dist in |- *; intros. 
 
304
elim (p eps H1); intros. 
 
305
exists x1; intros. 
 
306
unfold C1 in |- *. 
 
307
replace
 
308
 (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * (x + y) ^ (2 * k)) n)
 
309
 with
 
310
 (sum_f_R0
 
311
    (fun i:nat => (-1) ^ i / INR (fact (2 * i)) * ((x + y) * (x + y)) ^ i) n). 
 
312
apply H2; assumption. 
 
313
apply sum_eq. 
 
314
intros. 
 
315
replace (((x + y) * (x + y)) ^ i) with ((x + y) ^ (2 * i)). 
 
316
reflexivity. 
 
317
apply pow_sqr. 
 
318
unfold cos in |- *. 
 
319
case (exist_cos (Rsqr (x + y))). 
 
320
unfold Rsqr in |- *; intros. 
 
321
unfold cos_in in p_i. 
 
322
unfold cos_in in c. 
 
323
apply uniqueness_sum with (fun i:nat => cos_n i * ((x + y) * (x + y)) ^ i);
 
324
 assumption. 
 
325
Qed. 
 
326
 
 
327
Lemma B1_cvg : forall x:R, Un_cv (B1 x) (sin x). 
 
328
intro. 
 
329
case (Req_dec x 0); intro. 
 
330
rewrite H. 
 
331
rewrite sin_0. 
 
332
unfold B1 in |- *. 
 
333
unfold Un_cv in |- *; unfold R_dist in |- *; intros; exists 0%nat; intros. 
 
334
replace
 
335
 (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * 0 ^ (2 * k + 1))
 
336
    n) with 0. 
 
337
unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. 
 
338
induction  n as [| n Hrecn]. 
 
339
simpl in |- *; ring. 
 
340
rewrite tech5; rewrite <- Hrecn. 
 
341
simpl in |- *; ring. 
 
342
unfold ge in |- *; apply le_O_n. 
 
343
assert (H0 := exist_sin (x * x)). 
 
344
elim H0; intros. 
 
345
assert (p_i := p). 
 
346
unfold sin_in in p. 
 
347
unfold sin_n, infinite_sum in p. 
 
348
unfold R_dist in p. 
 
349
cut (sin x = x * x0). 
 
350
intro. 
 
351
rewrite H1. 
 
352
unfold Un_cv in |- *; unfold R_dist in |- *; intros. 
 
353
cut (0 < eps / Rabs x);
 
354
 [ intro
 
355
 | unfold Rdiv in |- *; apply Rmult_lt_0_compat;
 
356
    [ assumption | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ] ]. 
 
357
elim (p (eps / Rabs x) H3); intros. 
 
358
exists x1; intros. 
 
359
unfold B1 in |- *. 
 
360
replace
 
361
 (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k + 1)) * x ^ (2 * k + 1))
 
362
    n) with
 
363
 (x *
 
364
  sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i + 1)) * (x * x) ^ i) n). 
 
365
replace
 
366
 (x *
 
367
  sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i + 1)) * (x * x) ^ i) n -
 
368
  x * x0) with
 
369
 (x *
 
370
  (sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i + 1)) * (x * x) ^ i) n -
 
371
   x0)); [ idtac | ring ]. 
 
372
rewrite Rabs_mult. 
 
373
apply Rmult_lt_reg_l with (/ Rabs x). 
 
374
apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. 
 
375
rewrite <- Rmult_assoc. 
 
376
rewrite <- Rinv_l_sym. 
 
377
rewrite Rmult_1_l; rewrite <- (Rmult_comm eps); unfold Rdiv in H4; apply H4;
 
378
 assumption. 
 
379
apply Rabs_no_R0; assumption. 
 
380
rewrite scal_sum. 
 
381
apply sum_eq. 
 
382
intros. 
 
383
rewrite pow_add. 
 
384
rewrite pow_sqr. 
 
385
simpl in |- *. 
 
386
ring. 
 
387
unfold sin in |- *. 
 
388
case (exist_sin (Rsqr x)). 
 
389
unfold Rsqr in |- *; intros. 
 
390
unfold sin_in in p_i. 
 
391
unfold sin_in in s. 
 
392
assert
 
393
 (H1 := uniqueness_sum (fun i:nat => sin_n i * (x * x) ^ i) x0 x1 p_i s). 
 
394
rewrite H1; reflexivity. 
 
395
Qed.