]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/Z/dirichlet_product.ma
...
[helm.git] / helm / software / matita / library / Z / dirichlet_product.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        Matita is distributed under the terms of the          *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/primes.ma".
16 include "Z/sigma_p.ma".
17 include "Z/times.ma".
18
19 definition dirichlet_product : (nat \to Z) \to (nat \to Z) \to nat \to Z \def
20 \lambda f,g.\lambda n.
21 sigma_p (S n) 
22  (\lambda d.divides_b d n) (\lambda d. (f d)*(g (div n d))).
23
24 (* dirichlet_product is associative only up to extensional equality *)
25 theorem associative_dirichlet_product: 
26 \forall f,g,h:nat\to Z.\forall n:nat.O < n \to
27 dirichlet_product (dirichlet_product f g) h n
28  = dirichlet_product f (dirichlet_product g h) n.
29 intros.
30 unfold dirichlet_product.
31 unfold dirichlet_product.
32 apply (trans_eq ? ? 
33 (sigma_p (S n) (\lambda d:nat.divides_b d n)
34 (\lambda d:nat
35  .sigma_p (S n) (\lambda d1:nat.divides_b d1 d) (\lambda d1:nat.f d1*g (d/d1)*h (n/d)))))
36   [apply eq_sigma_p1
37     [intros.reflexivity
38     |intros.
39      apply (trans_eq ? ? 
40      (sigma_p (S x) (\lambda d1:nat.divides_b d1 x) (\lambda d1:nat.f d1*g (x/d1)*h (n/x))))
41       [apply Ztimes_sigma_pr
42       |(* hint solleva unification uncertain ?? *)
43        apply sym_eq.
44        apply false_to_eq_sigma_p
45         [assumption
46         |intros.
47          apply not_divides_to_divides_b_false
48           [apply (lt_to_le_to_lt ? (S x))
49             [apply lt_O_S|assumption]
50           |unfold Not. intro.
51            apply (lt_to_not_le ? ? H3).
52            apply divides_to_le
53             [apply (divides_b_true_to_lt_O ? ? H H2).
54             |assumption
55             ]
56           ]
57         ]
58       ]
59     ]
60   |apply (trans_eq ? ?
61    (sigma_p (S n) (\lambda d:nat.divides_b d n)
62     (\lambda d:nat
63       .sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/d))
64       (\lambda d1:nat.f d*g d1*h ((n/d)/d1)))))
65     [apply (trans_eq ? ?
66       (sigma_p (S n) (\lambda d:nat.divides_b d n)
67        (\lambda d:nat
68         .sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/d))
69         (\lambda d1:nat.f d*g ((times d d1)/d)*h ((n/times d d1))))))
70       [apply (sigma_p2_eq 
71         (\lambda d,d1.f d1*g (d/d1)*h (n/d))
72         (\lambda d,d1:nat.times d d1) 
73         (\lambda d,d1:nat.d) 
74         (\lambda d,d1:nat.d1) 
75         (\lambda d,d1:nat.d/d1)
76         (S n)
77         (S n)
78         (S n)
79         (S n)
80         ?
81         ?
82         (\lambda d,d1:nat.divides_b d1 d)
83         (\lambda d,d1:nat.divides_b d1 (n/d))
84         )
85         [intros.
86          split
87           [split
88             [split
89               [split
90                 [split
91                   [apply divides_to_divides_b_true1
92                     [assumption
93                     |apply (witness ? ? ((n/i)/j)).
94                      rewrite > assoc_times.
95                      rewrite > sym_times in \vdash (? ? ? (? ? %)).
96                      rewrite > divides_to_div
97                       [rewrite > sym_times. 
98                        rewrite > divides_to_div
99                         [reflexivity
100                         |apply divides_b_true_to_divides.
101                          assumption
102                         ]
103                       |apply divides_b_true_to_divides.
104                        assumption
105                       ]
106                     ]
107                   |apply divides_to_divides_b_true
108                     [apply (divides_b_true_to_lt_O ? ? H H3)
109                     |apply (witness ? ? j).
110                      reflexivity
111                     ]
112                   ]
113                 |reflexivity
114                 ]
115               |rewrite < sym_times.
116                rewrite > (plus_n_O (j*i)).
117                apply div_plus_times.
118                apply (divides_b_true_to_lt_O ? ? H H3)
119               ]
120             |apply (le_to_lt_to_lt ? (i*(n/i)))
121               [apply le_times
122                 [apply le_n
123                 |apply divides_to_le
124                   [elim (le_to_or_lt_eq ? ? (le_O_n (n/i)))
125                     [assumption
126                     |apply False_ind.
127                      apply (lt_to_not_le ? ? H).
128                      rewrite < (divides_to_div i n)
129                       [rewrite < H5.
130                        apply le_n
131                       |apply divides_b_true_to_divides.
132                        assumption
133                       ]
134                     ]
135                   |apply divides_b_true_to_divides.
136                    assumption
137                   ]
138                 ]
139               |rewrite < sym_times.
140                rewrite > divides_to_div
141                 [apply le_n
142                 |apply divides_b_true_to_divides.
143                  assumption
144                 ]
145               ]
146             ]
147           |assumption
148           ]
149         |intros.
150          split
151           [split
152             [split
153               [split
154                 [split
155                   [apply divides_to_divides_b_true1
156                     [assumption
157                     |apply (transitive_divides ? i)
158                       [apply divides_b_true_to_divides.
159                        assumption
160                       |apply divides_b_true_to_divides.
161                        assumption
162                       ]
163                     ]
164                   |apply divides_to_divides_b_true
165                     [apply (divides_b_true_to_lt_O i (i/j))
166                       [apply (divides_b_true_to_lt_O ? ? ? H3).
167                        assumption
168                       |apply divides_to_divides_b_true1
169                         [apply (divides_b_true_to_lt_O ? ? ? H3).
170                          assumption
171                         |apply (witness ? ? j).
172                          apply sym_eq.
173                          apply divides_to_div.
174                          apply divides_b_true_to_divides.
175                          assumption
176                         ]
177                       ]
178                     |apply (witness ? ? (n/i)).
179                      apply (inj_times_l1 j)
180                       [apply (divides_b_true_to_lt_O ? ? ? H4).
181                        apply (divides_b_true_to_lt_O ? ? ? H3).
182                        assumption
183                       |rewrite > divides_to_div
184                         [rewrite > sym_times in \vdash (? ? ? (? % ?)).
185                          rewrite > assoc_times.
186                          rewrite > divides_to_div
187                           [rewrite > divides_to_div
188                             [reflexivity
189                             |apply divides_b_true_to_divides.
190                              assumption
191                             ]
192                           |apply divides_b_true_to_divides.
193                            assumption
194                           ]
195                         |apply (transitive_divides ? i)
196                           [apply divides_b_true_to_divides.
197                            assumption
198                           |apply divides_b_true_to_divides.
199                            assumption
200                           ]
201                         ]
202                       ]
203                     ]
204                   ]
205                 |rewrite < sym_times.
206                  apply divides_to_div.
207                  apply divides_b_true_to_divides.
208                  assumption
209                 ]
210               |reflexivity
211               ]
212             |assumption
213             ]
214           |apply (le_to_lt_to_lt ? i)
215             [apply le_div.
216              apply (divides_b_true_to_lt_O ? ? ? H4).
217              apply (divides_b_true_to_lt_O ? ? ? H3).
218              assumption
219             |assumption
220             ]
221           ]
222         ]
223       |apply eq_sigma_p1
224         [intros.reflexivity
225         |intros.
226          apply eq_sigma_p1
227           [intros.reflexivity
228           |intros.
229            apply eq_f2
230             [apply eq_f2
231               [reflexivity
232               |apply eq_f.
233                rewrite > sym_times.
234                rewrite > (plus_n_O (x1*x)).
235                apply div_plus_times.
236                apply (divides_b_true_to_lt_O ? ? ? H2).
237                assumption
238               ]
239             |apply eq_f.
240              cut (O < x)
241               [cut (O < x1)
242                 [apply (inj_times_l1 (x*x1))
243                   [rewrite > (times_n_O O).
244                    apply lt_times;assumption
245                   |rewrite > divides_to_div
246                     [rewrite > sym_times in \vdash (? ? ? (? ? %)).
247                      rewrite < assoc_times.
248                      rewrite > divides_to_div
249                       [rewrite > divides_to_div
250                         [reflexivity
251                         |apply divides_b_true_to_divides.
252                          assumption
253                         ]
254                       |apply divides_b_true_to_divides.
255                        assumption
256                       ]
257                     |elim (divides_b_true_to_divides ? ? H4).
258                      apply (witness ? ? n1).
259                      rewrite > assoc_times.
260                      rewrite < H5.
261                      rewrite < sym_times.
262                      apply sym_eq.
263                      apply divides_to_div.
264                      apply divides_b_true_to_divides.
265                      assumption
266                     ]
267                   ]
268                 |apply (divides_b_true_to_lt_O ? ? ? H4).
269                  apply (lt_times_n_to_lt x)
270                   [assumption
271                   |simplify.
272                    rewrite > divides_to_div
273                     [assumption
274                     |apply (divides_b_true_to_divides ? ? H2).
275                      assumption
276                     ]
277                   ]
278                 ]
279               |apply (divides_b_true_to_lt_O ? ? ? H2).
280                assumption
281               ]
282             ]
283           ]
284         ]
285       ]
286     |apply eq_sigma_p1
287       [intros.reflexivity
288       |intros.
289        apply (trans_eq ? ? 
290        (sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/x)) (\lambda d1:nat.f x*(g d1*h (n/x/d1)))))
291         [apply eq_sigma_p
292           [intros.reflexivity
293           |intros.apply assoc_Ztimes
294           ]
295         |apply (trans_eq ? ? 
296           (sigma_p (S (n/x)) (\lambda d1:nat.divides_b d1 (n/x)) (\lambda d1:nat.f x*(g d1*h (n/x/d1)))))
297           [apply false_to_eq_sigma_p
298             [apply le_S_S.
299              cut (O < x)
300               [apply (le_times_to_le x)
301                 [assumption
302                 |rewrite > sym_times.
303                  rewrite > divides_to_div
304                   [apply le_times_n.
305                    assumption
306                   |apply divides_b_true_to_divides.
307                    assumption
308                   ]
309                 ]
310               |apply (divides_b_true_to_lt_O ? ? ? H2).
311                assumption
312               ]
313             |intros.
314              apply not_divides_to_divides_b_false
315               [apply (trans_le ? ? ? ? H3).
316                apply le_S_S.
317                apply le_O_n
318               |unfold Not.intro.
319                apply (le_to_not_lt ? ? H3).
320                apply le_S_S.
321                apply divides_to_le
322                 [apply (lt_times_n_to_lt x)
323                   [apply (divides_b_true_to_lt_O ? ? ? H2).
324                    assumption
325                   |simplify.
326                    rewrite > divides_to_div
327                     [assumption
328                     |apply (divides_b_true_to_divides ? ? H2).
329                      assumption
330                     ]
331                   ]
332                 |assumption
333                 ]
334               ]
335             ]
336           |apply sym_eq.
337            apply Ztimes_sigma_pl
338           ]
339         ]
340       ]
341     ]
342   ]
343 qed.
344
345 definition is_one: nat \to Z \def 
346 \lambda n.
347   match n with
348   [O \Rightarrow OZ
349   | (S p) \Rightarrow 
350     match p with
351     [ O \Rightarrow pos O
352     | (S q) \Rightarrow OZ]]
353 .
354
355 theorem is_one_OZ: \forall n. n \neq S O \to is_one n = OZ.
356 intro.apply (nat_case n)
357   [intro.reflexivity
358   |intro. apply (nat_case m)
359     [intro.apply False_ind.apply H.reflexivity
360     |intros.reflexivity
361     ]
362   ]
363 qed.
364
365 theorem sigma_p_OZ:
366 \forall p: nat \to bool.\forall n.sigma_p n p (\lambda m.OZ) = OZ.
367 intros.elim n
368   [reflexivity
369   |apply (bool_elim ? (p n1));intro
370     [rewrite > true_to_sigma_p_Sn
371       [rewrite > sym_Zplus. 
372        rewrite > Zplus_z_OZ. 
373        assumption
374       |assumption
375       ]
376     |rewrite > false_to_sigma_p_Sn
377       [assumption
378       |assumption
379       ]
380     ]
381   ]
382 qed.
383
384 theorem dirichlet_product_is_one_r: 
385 \forall f:nat\to Z.\forall n:nat.
386   dirichlet_product f is_one n = f n.
387 intros.
388 elim n
389   [unfold dirichlet_product.
390    rewrite > true_to_sigma_p_Sn
391     [rewrite > Ztimes_Zone_r.
392      rewrite > Zplus_z_OZ.
393      reflexivity
394     |reflexivity
395     ]
396   |unfold dirichlet_product.
397    rewrite > true_to_sigma_p_Sn
398     [rewrite > div_n_n
399       [rewrite > Ztimes_Zone_r.
400        rewrite < Zplus_z_OZ in \vdash (? ? ? %).
401        apply eq_f2
402         [reflexivity
403         |apply (trans_eq ? ? (sigma_p (S n1) 
404           (\lambda d:nat.divides_b d (S n1)) (\lambda d:nat.OZ)))
405           [apply eq_sigma_p1;intros
406             [reflexivity
407             |rewrite > is_one_OZ
408               [apply Ztimes_z_OZ
409               |unfold Not.intro.
410                apply (lt_to_not_le ? ? H1).
411                rewrite > (times_n_SO x).
412                rewrite > sym_times.
413                rewrite < H3.
414                rewrite > (div_mod ? x) in \vdash (? % ?)
415                 [rewrite > divides_to_mod_O
416                   [rewrite < plus_n_O.
417                    apply le_n
418                   |apply (divides_b_true_to_lt_O ? ? ? H2).
419                    apply lt_O_S
420                   |apply divides_b_true_to_divides.
421                    assumption
422                   ]
423                 |apply (divides_b_true_to_lt_O ? ? ? H2).
424                  apply lt_O_S
425                 ]
426               ]
427             ]
428           |apply sigma_p_OZ
429           ]
430         ]
431       |apply lt_O_S
432       ]
433     |apply divides_to_divides_b_true
434       [apply lt_O_S
435       |apply divides_n_n
436       ]
437     ]
438   ]
439 qed.           
440
441 theorem commutative_dirichlet_product: \forall f,g:nat \to Z.\forall n. O < n \to 
442 dirichlet_product f g n = dirichlet_product g f n.
443 intros.
444 unfold dirichlet_product.
445 apply (trans_eq ? ?
446   (sigma_p (S n) (\lambda d:nat.divides_b d n)
447   (\lambda d:nat.g (n/d) * f (n/(n/d)))))
448   [apply eq_sigma_p1;intros
449     [reflexivity
450     |rewrite > div_div
451       [apply sym_Ztimes.
452       |assumption
453       |apply divides_b_true_to_divides.
454        assumption
455       ]
456     ]
457   |apply (eq_sigma_p_gh ? (\lambda d.(n/d)) (\lambda d.(n/d))) 
458     [intros.
459      apply divides_b_div_true;assumption
460     |intros.
461      apply div_div
462       [assumption
463       |apply divides_b_true_to_divides.
464        assumption
465       ]
466     |intros.
467      apply le_S_S.
468      apply le_div.
469      apply (divides_b_true_to_lt_O ? ? H H2)
470     |intros.
471      apply divides_b_div_true;assumption
472     |intros.
473      apply div_div
474       [assumption
475       |apply divides_b_true_to_divides.
476        assumption
477       ]
478     |intros.
479      apply le_S_S.
480      apply le_div.
481      apply (divides_b_true_to_lt_O ? ? H H2)
482     ]
483   ]
484 qed.
485
486 theorem dirichlet_product_is_one_l: 
487 \forall f:nat\to Z.\forall n:nat.
488 O < n \to dirichlet_product is_one f n = f n.
489 intros.
490 rewrite > commutative_dirichlet_product.
491 apply dirichlet_product_is_one_r.
492 assumption.
493 qed.
494
495 theorem dirichlet_product_one_r: 
496 \forall f:nat\to Z.\forall n:nat. O < n \to 
497 dirichlet_product f (\lambda n.Zone) n = 
498 sigma_p (S n) (\lambda d.divides_b d n) f.
499 intros.
500 unfold dirichlet_product.
501 apply eq_sigma_p;intros
502   [reflexivity
503   |simplify in \vdash (? ? (? ? %) ?).
504    apply Ztimes_Zone_r
505   ]
506 qed.
507               
508 theorem dirichlet_product_one_l: 
509 \forall f:nat\to Z.\forall n:nat. O < n \to 
510 dirichlet_product (\lambda n.Zone) f n = 
511 sigma_p (S n) (\lambda d.divides_b d n) f. 
512 intros.
513 rewrite > commutative_dirichlet_product
514   [apply dirichlet_product_one_r.
515    assumption
516   |assumption
517   ]
518 qed.