1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / Matita is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/Z/dirichlet_product".
17 include "nat/primes.ma".
18 include "Z/sigma_p.ma".
21 definition dirichlet_product : (nat \to Z) \to (nat \to Z) \to nat \to Z \def
22 \lambda f,g.\lambda n.
24 (\lambda d.divides_b d n) (\lambda d. (f d)*(g (div n d))).
28 (* spostati in div_and_mod.ma
29 theorem mod_SO: \forall n:nat. mod n (S O) = O.
37 theorem div_SO: \forall n:nat. div n (S O) = n.
39 rewrite > (div_mod ? (S O)) in \vdash (? ? ? %)
47 theorem and_true: \forall a,b:bool.
48 andb a b =true \to a =true \land b= true.
51 [reflexivity|assumption]
53 apply not_eq_true_false.
59 theorem lt_times_plus_times: \forall a,b,n,m:nat.
60 a < n \to b < m \to a*m + b < n*m.
63 [intros.apply False_ind.apply (not_le_Sn_O ? H)
67 change with (S b+a*m1 \leq m1+m*m1).
71 [apply le_S_S_to_le.assumption
78 theorem divides_to_divides_b_true1 : \forall n,m:nat.
79 O < m \to n \divides m \to divides_b n m = true.
81 elim (le_to_or_lt_eq O n (le_O_n n))
82 [apply divides_to_divides_b_true
83 [assumption|assumption]
88 apply (not_le_Sn_O O).
93 (* spostato in primes.ma
94 theorem divides_to_div: \forall n,m.divides n m \to m/n*n = m.
96 elim (le_to_or_lt_eq O n (le_O_n n))
98 rewrite < (divides_to_mod_O ? ? H H1).
103 generalize in match H2.
111 (* spostato in div_and_mod.ma
112 theorem le_div: \forall n,m. O < n \to m/n \le m.
114 rewrite > (div_mod m n) in \vdash (? ? %)
115 [apply (trans_le ? (m/n*n))
116 [rewrite > times_n_SO in \vdash (? % ?).
118 [apply le_n|assumption]
126 \forall g: nat \to nat \to Z.
127 \forall h11,h12,h21,h22: nat \to nat \to nat.
129 \forall p11,p21:nat \to bool.
130 \forall p12,p22:nat \to nat \to bool.
131 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
132 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
133 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
134 \land h11 i j < n \land h12 i j < m) \to
135 (\forall i,j. i < n \to j < m \to p11 i = true \to p12 i j = true \to
136 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
137 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
138 \land (h21 i j) < n \land (h22 i j) < m) \to
139 sigma_p n p11 (\lambda x:nat .sigma_p m (p12 x) (\lambda y. g x y)) =
140 sigma_p n p21 (\lambda x:nat .sigma_p m (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
145 letin h := (\lambda x.(h11 (x/m) (x\mod m))*m + (h12 (x/m) (x\mod m))).
146 letin h1 := (\lambda x.(h21 (x/m) (x\mod m))*m + (h22 (x/m) (x\mod m))).
148 (sigma_p (n*m) (\lambda x:nat.p21 (x/m)\land p22 (x/m) (x\mod m))
149 (\lambda x:nat.g ((h x)/m) ((h x)\mod m))))
157 [elim (and_true ? ? H3).
158 elim (H ? ? Hcut1 Hcut2 H4 H5).
165 apply div_plus_times.
172 |apply (lt_times_n_to_lt m)
174 |apply (le_to_lt_to_lt ? x)
175 [apply (eq_plus_to_le ? ? (x \mod m)).
182 |apply not_le_to_lt.unfold.intro.
183 generalize in match H2.
184 apply (le_n_O_elim ? H4).
190 |apply (eq_sigma_p_gh ? h h1);intros
194 [elim (and_true ? ? H3).
195 elim (H ? ? Hcut1 Hcut2 H4 H5).
200 cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))/m =
202 [cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))\mod m =
209 |apply mod_plus_times.
212 |apply div_plus_times.
218 |apply (lt_times_n_to_lt m)
220 |apply (le_to_lt_to_lt ? i)
221 [apply (eq_plus_to_le ? ? (i \mod m)).
228 |apply not_le_to_lt.unfold.intro.
229 generalize in match H2.
230 apply (le_n_O_elim ? H4).
238 [elim (and_true ? ? H3).
239 elim (H ? ? Hcut1 Hcut2 H4 H5).
244 cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))/m =
246 [cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))\mod m =
255 |apply mod_plus_times.
258 |apply div_plus_times.
264 |apply (lt_times_n_to_lt m)
266 |apply (le_to_lt_to_lt ? i)
267 [apply (eq_plus_to_le ? ? (i \mod m)).
274 |apply not_le_to_lt.unfold.intro.
275 generalize in match H2.
276 apply (le_n_O_elim ? H4).
284 [elim (and_true ? ? H3).
285 elim (H ? ? Hcut1 Hcut2 H4 H5).
290 apply lt_times_plus_times
291 [assumption|assumption]
295 |apply (lt_times_n_to_lt m)
297 |apply (le_to_lt_to_lt ? i)
298 [apply (eq_plus_to_le ? ? (i \mod m)).
305 |apply not_le_to_lt.unfold.intro.
306 generalize in match H2.
307 apply (le_n_O_elim ? H4).
315 [elim (and_true ? ? H3).
316 elim (H1 ? ? Hcut1 Hcut2 H4 H5).
321 cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))/m =
323 [cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))\mod m =
330 |apply mod_plus_times.
333 |apply div_plus_times.
339 |apply (lt_times_n_to_lt m)
341 |apply (le_to_lt_to_lt ? j)
342 [apply (eq_plus_to_le ? ? (j \mod m)).
349 |apply not_le_to_lt.unfold.intro.
350 generalize in match H2.
351 apply (le_n_O_elim ? H4).
359 [elim (and_true ? ? H3).
360 elim (H1 ? ? Hcut1 Hcut2 H4 H5).
365 cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))/m =
367 [cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))\mod m =
376 |apply mod_plus_times.
379 |apply div_plus_times.
385 |apply (lt_times_n_to_lt m)
387 |apply (le_to_lt_to_lt ? j)
388 [apply (eq_plus_to_le ? ? (j \mod m)).
395 |apply not_le_to_lt.unfold.intro.
396 generalize in match H2.
397 apply (le_n_O_elim ? H4).
405 [elim (and_true ? ? H3).
406 elim (H1 ? ? Hcut1 Hcut2 H4 H5).
411 apply (lt_times_plus_times ? ? ? m)
412 [assumption|assumption]
416 |apply (lt_times_n_to_lt m)
418 |apply (le_to_lt_to_lt ? j)
419 [apply (eq_plus_to_le ? ? (j \mod m)).
426 |apply not_le_to_lt.unfold.intro.
427 generalize in match H2.
428 apply (le_n_O_elim ? H4).
437 (* dirichlet_product is associative only up to extensional equality *)
438 theorem associative_dirichlet_product:
439 \forall f,g,h:nat\to Z.\forall n:nat.O < n \to
440 dirichlet_product (dirichlet_product f g) h n
441 = dirichlet_product f (dirichlet_product g h) n.
443 unfold dirichlet_product.
444 unfold dirichlet_product.
446 (sigma_p (S n) (\lambda d:nat.divides_b d n)
448 .sigma_p (S n) (\lambda d1:nat.divides_b d1 d) (\lambda d1:nat.f d1*g (d/d1)*h (n/d)))))
453 (sigma_p (S x) (\lambda d1:nat.divides_b d1 x) (\lambda d1:nat.f d1*g (x/d1)*h (n/x))))
454 [apply Ztimes_sigma_pr
455 |(* hint solleva unification uncertain ?? *)
457 apply false_to_eq_sigma_p
460 apply not_divides_to_divides_b_false
461 [apply (lt_to_le_to_lt ? (S x))
462 [apply lt_O_S|assumption]
464 apply (lt_to_not_le ? ? H3).
466 [apply (divides_b_true_to_lt_O ? ? H H2).
474 (sigma_p (S n) (\lambda d:nat.divides_b d n)
476 .sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/d))
477 (\lambda d1:nat.f d*g d1*h ((n/d)/d1)))))
479 (sigma_p (S n) (\lambda d:nat.divides_b d n)
481 .sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/d))
482 (\lambda d1:nat.f d*g ((times d d1)/d)*h ((n/times d d1))))))
484 (\lambda d,d1.f d1*g (d/d1)*h (n/d))
485 (\lambda d,d1:nat.times d d1)
487 (\lambda d,d1:nat.d1)
488 (\lambda d,d1:nat.d/d1)
493 (\lambda d,d1:nat.divides_b d1 d)
494 (\lambda d,d1:nat.divides_b d1 (n/d))
502 [apply divides_to_divides_b_true1
504 |apply (witness ? ? ((n/i)/j)).
505 rewrite > assoc_times.
506 rewrite > sym_times in \vdash (? ? ? (? ? %)).
507 rewrite > divides_to_div
508 [rewrite > sym_times.
509 rewrite > divides_to_div
511 |apply divides_b_true_to_divides.
514 |apply divides_b_true_to_divides.
518 |apply divides_to_divides_b_true
519 [apply (divides_b_true_to_lt_O ? ? H H3)
520 |apply (witness ? ? j).
526 |rewrite < sym_times.
527 rewrite > (plus_n_O (j*i)).
528 apply div_plus_times.
529 apply (divides_b_true_to_lt_O ? ? H H3)
531 |apply (le_to_lt_to_lt ? (i*(n/i)))
535 [elim (le_to_or_lt_eq ? ? (le_O_n (n/i)))
538 apply (lt_to_not_le ? ? H).
539 rewrite < (divides_to_div i n)
542 |apply divides_b_true_to_divides.
546 |apply divides_b_true_to_divides.
550 |rewrite < sym_times.
551 rewrite > divides_to_div
553 |apply divides_b_true_to_divides.
566 [apply divides_to_divides_b_true1
568 |apply (transitive_divides ? i)
569 [apply divides_b_true_to_divides.
571 |apply divides_b_true_to_divides.
575 |apply divides_to_divides_b_true
576 [apply (divides_b_true_to_lt_O i (i/j))
577 [apply (divides_b_true_to_lt_O ? ? ? H3).
579 |apply divides_to_divides_b_true1
580 [apply (divides_b_true_to_lt_O ? ? ? H3).
582 |apply (witness ? ? j).
584 apply divides_to_div.
585 apply divides_b_true_to_divides.
589 |apply (witness ? ? (n/i)).
590 apply (inj_times_l1 j)
591 [apply (divides_b_true_to_lt_O ? ? ? H4).
592 apply (divides_b_true_to_lt_O ? ? ? H3).
594 |rewrite > divides_to_div
595 [rewrite > sym_times in \vdash (? ? ? (? % ?)).
596 rewrite > assoc_times.
597 rewrite > divides_to_div
598 [rewrite > divides_to_div
600 |apply divides_b_true_to_divides.
603 |apply divides_b_true_to_divides.
606 |apply (transitive_divides ? i)
607 [apply divides_b_true_to_divides.
609 |apply divides_b_true_to_divides.
616 |rewrite < sym_times.
617 apply divides_to_div.
618 apply divides_b_true_to_divides.
625 |apply (le_to_lt_to_lt ? i)
627 apply (divides_b_true_to_lt_O ? ? ? H4).
628 apply (divides_b_true_to_lt_O ? ? ? H3).
645 rewrite > (plus_n_O (x1*x)).
646 apply div_plus_times.
647 apply (divides_b_true_to_lt_O ? ? ? H2).
653 [apply (inj_times_l1 (x*x1))
654 [rewrite > (times_n_O O).
655 apply lt_times;assumption
656 |rewrite > divides_to_div
657 [rewrite > sym_times in \vdash (? ? ? (? ? %)).
658 rewrite < assoc_times.
659 rewrite > divides_to_div
660 [rewrite > divides_to_div
662 |apply divides_b_true_to_divides.
665 |apply divides_b_true_to_divides.
668 |elim (divides_b_true_to_divides ? ? H4).
669 apply (witness ? ? n2).
670 rewrite > assoc_times.
674 apply divides_to_div.
675 apply divides_b_true_to_divides.
679 |apply (divides_b_true_to_lt_O ? ? ? H4).
680 apply (lt_times_n_to_lt x)
683 rewrite > divides_to_div
685 |apply (divides_b_true_to_divides ? ? H2).
690 |apply (divides_b_true_to_lt_O ? ? ? H2).
701 (sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/x)) (\lambda d1:nat.f x*(g d1*h (n/x/d1)))))
704 |intros.apply assoc_Ztimes
707 (sigma_p (S (n/x)) (\lambda d1:nat.divides_b d1 (n/x)) (\lambda d1:nat.f x*(g d1*h (n/x/d1)))))
708 [apply false_to_eq_sigma_p
711 [apply (le_times_to_le x)
713 |rewrite > sym_times.
714 rewrite > divides_to_div
717 |apply divides_b_true_to_divides.
721 |apply (divides_b_true_to_lt_O ? ? ? H2).
725 apply not_divides_to_divides_b_false
726 [apply (trans_le ? ? ? ? H3).
730 apply (le_to_not_lt ? ? H3).
733 [apply (lt_times_n_to_lt x)
734 [apply (divides_b_true_to_lt_O ? ? ? H2).
737 rewrite > divides_to_div
739 |apply (divides_b_true_to_divides ? ? H2).
748 apply Ztimes_sigma_pl
756 definition is_one: nat \to Z \def
762 [ O \Rightarrow pos O
763 | (S q) \Rightarrow OZ]]
766 theorem is_one_OZ: \forall n. n \neq S O \to is_one n = OZ.
767 intro.apply (nat_case n)
769 |intro. apply (nat_case m)
770 [intro.apply False_ind.apply H.reflexivity
776 (* da spostare in times *)
777 definition Zone \def pos O.
779 theorem Ztimes_Zone_l: \forall z:Z. Ztimes Zone z = z.
780 intro.unfold Zone.simplify.
783 |rewrite < plus_n_O.reflexivity
784 |rewrite < plus_n_O.reflexivity
788 theorem Ztimes_Zone_r: \forall z:Z. Ztimes z Zone = z.
790 rewrite < sym_Ztimes.
794 theorem injective_Zplus_l: \forall x:Z.injective Z Z (\lambda y.y+x).
795 intro.simplify.intros (z y).
796 rewrite < Zplus_z_OZ.
797 rewrite < (Zplus_z_OZ y).
798 rewrite < (Zplus_Zopp x).
799 rewrite < (Zplus_Zopp x).
800 rewrite < assoc_Zplus.
801 rewrite < assoc_Zplus.
803 [assumption|reflexivity]
806 theorem injective_Zplus_r: \forall x:Z.injective Z Z (\lambda y.x+y).
807 intro.simplify.intros (z y).
808 apply (injective_Zplus_l x).
815 \forall p: nat \to bool.\forall n.sigma_p n p (\lambda m.OZ) = OZ.
818 |apply (bool_elim ? (p n1));intro
819 [rewrite > true_to_sigma_p_Sn
820 [rewrite > sym_Zplus.
821 rewrite > Zplus_z_OZ.
825 |rewrite > false_to_sigma_p_Sn
833 theorem dirichlet_product_is_one_r:
834 \forall f:nat\to Z.\forall n:nat.
835 dirichlet_product f is_one n = f n.
838 [unfold dirichlet_product.
839 rewrite > true_to_sigma_p_Sn
840 [rewrite > Ztimes_Zone_r.
841 rewrite > Zplus_z_OZ.
845 |unfold dirichlet_product.
846 rewrite > true_to_sigma_p_Sn
848 [rewrite > Ztimes_Zone_r.
849 rewrite < Zplus_z_OZ in \vdash (? ? ? %).
852 |apply (trans_eq ? ? (sigma_p (S n1)
853 (\lambda d:nat.divides_b d (S n1)) (\lambda d:nat.OZ)))
854 [apply eq_sigma_p1;intros
859 apply (lt_to_not_le ? ? H1).
860 rewrite > (times_n_SO x).
863 rewrite > (div_mod ? x) in \vdash (? % ?)
864 [rewrite > divides_to_mod_O
867 |apply (divides_b_true_to_lt_O ? ? ? H2).
869 |apply divides_b_true_to_divides.
872 |apply (divides_b_true_to_lt_O ? ? ? H2).
882 |apply divides_to_divides_b_true
891 theorem notb_notb: \forall b:bool. notb (notb b) = b.
896 theorem injective_notb: injective bool bool notb.
900 rewrite < (notb_notb y).
905 theorem divides_div: \forall d,n. divides d n \to divides (n/d) n.
907 apply (witness ? ? d).
909 apply divides_to_div.
913 theorem divides_b_div_true:
914 \forall d,n. O < n \to
915 divides_b d n = true \to divides_b (n/d) n = true.
917 apply divides_to_divides_b_true1
920 apply divides_b_true_to_divides.
925 (* spostato in primes.ma (non in div_and_mod.ma perche' serve il predicato divides)
926 theorem div_div: \forall n,d:nat. O < n \to divides d n \to
929 apply (inj_times_l1 (n/d))
930 [apply (lt_times_n_to_lt d)
931 [apply (divides_to_lt_O ? ? H H1).
932 |rewrite > divides_to_div;assumption
934 |rewrite > divides_to_div
935 [rewrite > sym_times.
936 rewrite > divides_to_div
940 |apply (witness ? ? d).
942 apply divides_to_div.
948 theorem commutative_dirichlet_product: \forall f,g:nat \to Z.\forall n. O < n \to
949 dirichlet_product f g n = dirichlet_product g f n.
951 unfold dirichlet_product.
953 (sigma_p (S n) (\lambda d:nat.divides_b d n)
954 (\lambda d:nat.g (n/d) * f (n/(n/d)))))
955 [apply eq_sigma_p1;intros
960 |apply divides_b_true_to_divides.
964 |apply (eq_sigma_p_gh ? (\lambda d.(n/d)) (\lambda d.(n/d)))
966 apply divides_b_div_true;assumption
970 |apply divides_b_true_to_divides.
976 apply (divides_b_true_to_lt_O ? ? H H2)
978 apply divides_b_div_true;assumption
982 |apply divides_b_true_to_divides.
988 apply (divides_b_true_to_lt_O ? ? H H2)
993 theorem dirichlet_product_is_one_l:
994 \forall f:nat\to Z.\forall n:nat.
995 O < n \to dirichlet_product is_one f n = f n.
997 rewrite > commutative_dirichlet_product.
998 apply dirichlet_product_is_one_r.
1002 theorem dirichlet_product_one_r:
1003 \forall f:nat\to Z.\forall n:nat. O < n \to
1004 dirichlet_product f (\lambda n.Zone) n =
1005 sigma_p (S n) (\lambda d.divides_b d n) f.
1007 unfold dirichlet_product.
1008 apply eq_sigma_p;intros
1010 |simplify in \vdash (? ? (? ? %) ?).
1015 theorem dirichlet_product_one_l:
1016 \forall f:nat\to Z.\forall n:nat. O < n \to
1017 dirichlet_product (\lambda n.Zone) f n =
1018 sigma_p (S n) (\lambda d.divides_b d n) f.
1020 rewrite > commutative_dirichlet_product
1021 [apply dirichlet_product_one_r.