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 "Z/sigma_p.ma".
20 definition dirichlet_product : (nat \to Z) \to (nat \to Z) \to nat \to Z \def
21 \lambda f,g.\lambda n.
23 (\lambda d.divides_b d n) (\lambda d. (f d)*(g (div n d))).
27 theorem mod_SO: \forall n:nat. mod n (S O) = O.
35 theorem div_SO: \forall n:nat. div n (S O) = n.
37 rewrite > (div_mod ? (S O)) in \vdash (? ? ? %)
45 theorem and_true: \forall a,b:bool.
46 andb a b =true \to a =true \land b= true.
49 [reflexivity|assumption]
51 apply not_eq_true_false.
57 theorem lt_times_plus_times: \forall a,b,n,m:nat.
58 a < n \to b < m \to a*m + b < n*m.
61 [intros.apply False_ind.apply (not_le_Sn_O ? H)
65 change with (S b+a*m1 \leq m1+m*m1).
69 [apply le_S_S_to_le.assumption
76 theorem divides_to_divides_b_true1 : \forall n,m:nat.
77 O < m \to n \divides m \to divides_b n m = true.
79 elim (le_to_or_lt_eq O n (le_O_n n))
80 [apply divides_to_divides_b_true
81 [assumption|assumption]
86 apply (not_le_Sn_O O).
92 theorem divides_to_div: \forall n,m.divides n m \to m/n*n = m.
94 elim (le_to_or_lt_eq O n (le_O_n n))
96 rewrite < (divides_to_mod_O ? ? H H1).
101 generalize in match H2.
110 theorem le_div: \forall n,m. O < n \to m/n \le m.
112 rewrite > (div_mod m n) in \vdash (? ? %)
113 [apply (trans_le ? (m/n*n))
114 [rewrite > times_n_SO in \vdash (? % ?).
116 [apply le_n|assumption]
124 \forall g: nat \to nat \to Z.
125 \forall h11,h12,h21,h22: nat \to nat \to nat.
127 \forall p11,p21:nat \to bool.
128 \forall p12,p22:nat \to nat \to bool.
129 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
130 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
131 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
132 \land h11 i j < n \land h12 i j < m) \to
133 (\forall i,j. i < n \to j < m \to p11 i = true \to p12 i j = true \to
134 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
135 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
136 \land (h21 i j) < n \land (h22 i j) < m) \to
137 sigma_p n p11 (\lambda x:nat .sigma_p m (p12 x) (\lambda y. g x y)) =
138 sigma_p n p21 (\lambda x:nat .sigma_p m (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
143 letin h := (\lambda x.(h11 (x/m) (x\mod m))*m + (h12 (x/m) (x\mod m))).
144 letin h1 := (\lambda x.(h21 (x/m) (x\mod m))*m + (h22 (x/m) (x\mod m))).
146 (sigma_p (n*m) (\lambda x:nat.p21 (x/m)\land p22 (x/m) (x\mod m))
147 (\lambda x:nat.g ((h x)/m) ((h x)\mod m))))
155 [elim (and_true ? ? H3).
156 elim (H ? ? Hcut1 Hcut2 H4 H5).
163 apply div_plus_times.
170 |apply (lt_times_n_to_lt m)
172 |apply (le_to_lt_to_lt ? x)
173 [apply (eq_plus_to_le ? ? (x \mod m)).
180 |apply not_le_to_lt.unfold.intro.
181 generalize in match H2.
182 apply (le_n_O_elim ? H4).
188 |apply (eq_sigma_p_gh ? h h1);intros
192 [elim (and_true ? ? H3).
193 elim (H ? ? Hcut1 Hcut2 H4 H5).
198 cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))/m =
200 [cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))\mod m =
207 |apply mod_plus_times.
210 |apply div_plus_times.
216 |apply (lt_times_n_to_lt m)
218 |apply (le_to_lt_to_lt ? i)
219 [apply (eq_plus_to_le ? ? (i \mod m)).
226 |apply not_le_to_lt.unfold.intro.
227 generalize in match H2.
228 apply (le_n_O_elim ? H4).
236 [elim (and_true ? ? H3).
237 elim (H ? ? Hcut1 Hcut2 H4 H5).
242 cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))/m =
244 [cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))\mod m =
253 |apply mod_plus_times.
256 |apply div_plus_times.
262 |apply (lt_times_n_to_lt m)
264 |apply (le_to_lt_to_lt ? i)
265 [apply (eq_plus_to_le ? ? (i \mod m)).
272 |apply not_le_to_lt.unfold.intro.
273 generalize in match H2.
274 apply (le_n_O_elim ? H4).
282 [elim (and_true ? ? H3).
283 elim (H ? ? Hcut1 Hcut2 H4 H5).
288 apply lt_times_plus_times
289 [assumption|assumption]
293 |apply (lt_times_n_to_lt m)
295 |apply (le_to_lt_to_lt ? i)
296 [apply (eq_plus_to_le ? ? (i \mod m)).
303 |apply not_le_to_lt.unfold.intro.
304 generalize in match H2.
305 apply (le_n_O_elim ? H4).
313 [elim (and_true ? ? H3).
314 elim (H1 ? ? Hcut1 Hcut2 H4 H5).
319 cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))/m =
321 [cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))\mod m =
328 |apply mod_plus_times.
331 |apply div_plus_times.
337 |apply (lt_times_n_to_lt m)
339 |apply (le_to_lt_to_lt ? j)
340 [apply (eq_plus_to_le ? ? (j \mod m)).
347 |apply not_le_to_lt.unfold.intro.
348 generalize in match H2.
349 apply (le_n_O_elim ? H4).
357 [elim (and_true ? ? H3).
358 elim (H1 ? ? Hcut1 Hcut2 H4 H5).
363 cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))/m =
365 [cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))\mod m =
374 |apply mod_plus_times.
377 |apply div_plus_times.
383 |apply (lt_times_n_to_lt m)
385 |apply (le_to_lt_to_lt ? j)
386 [apply (eq_plus_to_le ? ? (j \mod m)).
393 |apply not_le_to_lt.unfold.intro.
394 generalize in match H2.
395 apply (le_n_O_elim ? H4).
403 [elim (and_true ? ? H3).
404 elim (H1 ? ? Hcut1 Hcut2 H4 H5).
409 apply (lt_times_plus_times ? ? ? m)
410 [assumption|assumption]
414 |apply (lt_times_n_to_lt m)
416 |apply (le_to_lt_to_lt ? j)
417 [apply (eq_plus_to_le ? ? (j \mod m)).
424 |apply not_le_to_lt.unfold.intro.
425 generalize in match H2.
426 apply (le_n_O_elim ? H4).
435 (* dirichlet_product is associative only up to extensional equality *)
436 theorem associative_dirichlet_product:
437 \forall f,g,h:nat\to Z.\forall n:nat.O < n \to
438 dirichlet_product (dirichlet_product f g) h n
439 = dirichlet_product f (dirichlet_product g h) n.
441 unfold dirichlet_product.
442 unfold dirichlet_product.
444 (sigma_p (S n) (\lambda d:nat.divides_b d n)
446 .sigma_p (S n) (\lambda d1:nat.divides_b d1 d) (\lambda d1:nat.f d1*g (d/d1)*h (n/d)))))
451 (sigma_p (S x) (\lambda d1:nat.divides_b d1 x) (\lambda d1:nat.f d1*g (x/d1)*h (n/x))))
452 [apply Ztimes_sigma_pr
453 |(* hint solleva unification uncertain ?? *)
455 apply false_to_eq_sigma_p
458 apply not_divides_to_divides_b_false
459 [apply (lt_to_le_to_lt ? (S x))
460 [apply lt_O_S|assumption]
462 apply (lt_to_not_le ? ? H3).
464 [apply (divides_b_true_to_lt_O ? ? H H2).
472 (sigma_p (S n) (\lambda d:nat.divides_b d n)
474 .sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/d))
475 (\lambda d1:nat.f d*g d1*h ((n/d)/d1)))))
477 (sigma_p (S n) (\lambda d:nat.divides_b d n)
479 .sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/d))
480 (\lambda d1:nat.f d*g ((times d d1)/d)*h ((n/times d d1))))))
482 (\lambda d,d1.f d1*g (d/d1)*h (n/d))
483 (\lambda d,d1:nat.times d d1)
485 (\lambda d,d1:nat.d1)
486 (\lambda d,d1:nat.d/d1)
491 (\lambda d,d1:nat.divides_b d1 d)
492 (\lambda d,d1:nat.divides_b d1 (n/d))
500 [apply divides_to_divides_b_true1
502 |apply (witness ? ? ((n/i)/j)).
503 rewrite > assoc_times.
504 rewrite > sym_times in \vdash (? ? ? (? ? %)).
505 rewrite > divides_to_div
506 [rewrite > sym_times.
507 rewrite > divides_to_div
509 |apply divides_b_true_to_divides.
512 |apply divides_b_true_to_divides.
516 |apply divides_to_divides_b_true
517 [apply (divides_b_true_to_lt_O ? ? H H3)
518 |apply (witness ? ? j).
524 |rewrite < sym_times.
525 rewrite > (plus_n_O (j*i)).
526 apply div_plus_times.
527 apply (divides_b_true_to_lt_O ? ? H H3)
529 |apply (le_to_lt_to_lt ? (i*(n/i)))
533 [elim (le_to_or_lt_eq ? ? (le_O_n (n/i)))
536 apply (lt_to_not_le ? ? H).
537 rewrite < (divides_to_div i n)
540 |apply divides_b_true_to_divides.
544 |apply divides_b_true_to_divides.
548 |rewrite < sym_times.
549 rewrite > divides_to_div
551 |apply divides_b_true_to_divides.
564 [apply divides_to_divides_b_true1
566 |apply (transitive_divides ? i)
567 [apply divides_b_true_to_divides.
569 |apply divides_b_true_to_divides.
573 |apply divides_to_divides_b_true
574 [apply (divides_b_true_to_lt_O i (i/j))
575 [apply (divides_b_true_to_lt_O ? ? ? H3).
577 |apply divides_to_divides_b_true1
578 [apply (divides_b_true_to_lt_O ? ? ? H3).
580 |apply (witness ? ? j).
582 apply divides_to_div.
583 apply divides_b_true_to_divides.
587 |apply (witness ? ? (n/i)).
588 apply (inj_times_l1 j)
589 [apply (divides_b_true_to_lt_O ? ? ? H4).
590 apply (divides_b_true_to_lt_O ? ? ? H3).
592 |rewrite > divides_to_div
593 [rewrite > sym_times in \vdash (? ? ? (? % ?)).
594 rewrite > assoc_times.
595 rewrite > divides_to_div
596 [rewrite > divides_to_div
598 |apply divides_b_true_to_divides.
601 |apply divides_b_true_to_divides.
604 |apply (transitive_divides ? i)
605 [apply divides_b_true_to_divides.
607 |apply divides_b_true_to_divides.
614 |rewrite < sym_times.
615 apply divides_to_div.
616 apply divides_b_true_to_divides.
623 |apply (le_to_lt_to_lt ? i)
625 apply (divides_b_true_to_lt_O ? ? ? H4).
626 apply (divides_b_true_to_lt_O ? ? ? H3).
643 rewrite > (plus_n_O (x1*x)).
644 apply div_plus_times.
645 apply (divides_b_true_to_lt_O ? ? ? H2).
651 [apply (inj_times_l1 (x*x1))
652 [rewrite > (times_n_O O).
653 apply lt_times;assumption
654 |rewrite > divides_to_div
655 [rewrite > sym_times in \vdash (? ? ? (? ? %)).
656 rewrite < assoc_times.
657 rewrite > divides_to_div
658 [rewrite > divides_to_div
660 |apply divides_b_true_to_divides.
663 |apply divides_b_true_to_divides.
666 |elim (divides_b_true_to_divides ? ? H4).
667 apply (witness ? ? n2).
668 rewrite > assoc_times.
672 apply divides_to_div.
673 apply divides_b_true_to_divides.
677 |apply (divides_b_true_to_lt_O ? ? ? H4).
678 apply (lt_times_n_to_lt x)
681 rewrite > divides_to_div
683 |apply (divides_b_true_to_divides ? ? H2).
688 |apply (divides_b_true_to_lt_O ? ? ? H2).
699 (sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/x)) (\lambda d1:nat.f x*(g d1*h (n/x/d1)))))
702 |intros.apply assoc_Ztimes
705 (sigma_p (S (n/x)) (\lambda d1:nat.divides_b d1 (n/x)) (\lambda d1:nat.f x*(g d1*h (n/x/d1)))))
706 [apply false_to_eq_sigma_p
709 [apply (le_times_to_le x)
711 |rewrite > sym_times.
712 rewrite > divides_to_div
715 |apply divides_b_true_to_divides.
719 |apply (divides_b_true_to_lt_O ? ? ? H2).
723 apply not_divides_to_divides_b_false
724 [apply (trans_le ? ? ? ? H3).
728 apply (le_to_not_lt ? ? H3).
731 [apply (lt_times_n_to_lt x)
732 [apply (divides_b_true_to_lt_O ? ? ? H2).
735 rewrite > divides_to_div
737 |apply (divides_b_true_to_divides ? ? H2).
746 apply Ztimes_sigma_pl
754 definition is_one: nat \to Z \def
760 [ O \Rightarrow pos O
761 | (S q) \Rightarrow OZ]]
764 theorem is_one_OZ: \forall n. n \neq S O \to is_one n = OZ.
765 intro.apply (nat_case n)
767 |intro. apply (nat_case m)
768 [intro.apply False_ind.apply H.reflexivity
774 (* da spostare in times *)
775 definition Zone \def pos O.
777 theorem Ztimes_Zone_l: \forall z:Z. Ztimes Zone z = z.
778 intro.unfold Zone.simplify.
781 |rewrite < plus_n_O.reflexivity
782 |rewrite < plus_n_O.reflexivity
786 theorem Ztimes_Zone_r: \forall z:Z. Ztimes z Zone = z.
788 rewrite < sym_Ztimes.
792 theorem injective_Zplus_l: \forall x:Z.injective Z Z (\lambda y.y+x).
793 intro.simplify.intros (z y).
794 rewrite < Zplus_z_OZ.
795 rewrite < (Zplus_z_OZ y).
796 rewrite < (Zplus_Zopp x).
797 rewrite < (Zplus_Zopp x).
798 rewrite < assoc_Zplus.
799 rewrite < assoc_Zplus.
801 [assumption|reflexivity]
804 theorem injective_Zplus_r: \forall x:Z.injective Z Z (\lambda y.x+y).
805 intro.simplify.intros (z y).
806 apply (injective_Zplus_l x).
813 \forall p: nat \to bool.\forall n.sigma_p n p (\lambda m.OZ) = OZ.
816 |apply (bool_elim ? (p n1));intro
817 [rewrite > true_to_sigma_p_Sn
818 [rewrite > sym_Zplus.
819 rewrite > Zplus_z_OZ.
823 |rewrite > false_to_sigma_p_Sn
831 theorem dirichlet_product_is_one_r:
832 \forall f:nat\to Z.\forall n:nat.
833 dirichlet_product f is_one n = f n.
836 [unfold dirichlet_product.
837 rewrite > true_to_sigma_p_Sn
838 [rewrite > Ztimes_Zone_r.
839 rewrite > Zplus_z_OZ.
843 |unfold dirichlet_product.
844 rewrite > true_to_sigma_p_Sn
846 [rewrite > Ztimes_Zone_r.
847 rewrite < Zplus_z_OZ in \vdash (? ? ? %).
850 |apply (trans_eq ? ? (sigma_p (S n1)
851 (\lambda d:nat.divides_b d (S n1)) (\lambda d:nat.OZ)))
852 [apply eq_sigma_p1;intros
857 apply (lt_to_not_le ? ? H1).
858 rewrite > (times_n_SO x).
861 rewrite > (div_mod ? x) in \vdash (? % ?)
862 [rewrite > divides_to_mod_O
865 |apply (divides_b_true_to_lt_O ? ? ? H2).
867 |apply divides_b_true_to_divides.
870 |apply (divides_b_true_to_lt_O ? ? ? H2).
880 |apply divides_to_divides_b_true
889 theorem notb_notb: \forall b:bool. notb (notb b) = b.
894 theorem injective_notb: injective bool bool notb.
898 rewrite < (notb_notb y).
903 theorem divides_div: \forall d,n. divides d n \to divides (n/d) n.
905 apply (witness ? ? d).
907 apply divides_to_div.
911 theorem divides_b_div_true:
912 \forall d,n. O < n \to
913 divides_b d n = true \to divides_b (n/d) n = true.
915 apply divides_to_divides_b_true1
918 apply divides_b_true_to_divides.
923 theorem div_div: \forall n,d:nat. O < n \to divides d n \to
926 apply (inj_times_l1 (n/d))
927 [apply (lt_times_n_to_lt d)
928 [apply (divides_to_lt_O ? ? H H1).
929 |rewrite > divides_to_div;assumption
931 |rewrite > divides_to_div
932 [rewrite > sym_times.
933 rewrite > divides_to_div
937 |apply (witness ? ? d).
939 apply divides_to_div.
945 theorem commutative_dirichlet_product: \forall f,g:nat \to Z.\forall n. O < n \to
946 dirichlet_product f g n = dirichlet_product g f n.
948 unfold dirichlet_product.
950 (sigma_p (S n) (\lambda d:nat.divides_b d n)
951 (\lambda d:nat.g (n/d) * f (n/(n/d)))))
952 [apply eq_sigma_p1;intros
957 |apply divides_b_true_to_divides.
961 |apply (eq_sigma_p_gh ? (\lambda d.(n/d)) (\lambda d.(n/d)))
963 apply divides_b_div_true;assumption
967 |apply divides_b_true_to_divides.
973 apply (divides_b_true_to_lt_O ? ? H H2)
975 apply divides_b_div_true;assumption
979 |apply divides_b_true_to_divides.
985 apply (divides_b_true_to_lt_O ? ? H H2)
990 theorem dirichlet_product_is_one_l:
991 \forall f:nat\to Z.\forall n:nat.
992 O < n \to dirichlet_product is_one f n = f n.
994 rewrite > commutative_dirichlet_product.
995 apply dirichlet_product_is_one_r.
999 theorem dirichlet_product_one_r:
1000 \forall f:nat\to Z.\forall n:nat. O < n \to
1001 dirichlet_product f (\lambda n.Zone) n =
1002 sigma_p (S n) (\lambda d.divides_b d n) f.
1004 unfold dirichlet_product.
1005 apply eq_sigma_p;intros
1007 |simplify in \vdash (? ? (? ? %) ?).
1012 theorem dirichlet_product_one_l:
1013 \forall f:nat\to Z.\forall n:nat. O < n \to
1014 dirichlet_product (\lambda n.Zone) f n =
1015 sigma_p (S n) (\lambda d.divides_b d n) f.
1017 rewrite > commutative_dirichlet_product
1018 [apply dirichlet_product_one_r.