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 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/Z/sigma_p.ma".
18 include "nat/primes.ma".
21 let rec sigma_p n p (g:nat \to Z) \def
26 [true \Rightarrow (g k)+(sigma_p k p g)
27 |false \Rightarrow sigma_p k p g]
30 theorem true_to_sigma_p_Sn:
31 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to Z.
32 p n = true \to sigma_p (S n) p g =
33 (g n)+(sigma_p n p g).
35 rewrite > H.reflexivity.
38 theorem false_to_sigma_p_Sn:
39 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to Z.
40 p n = false \to sigma_p (S n) p g = sigma_p n p g.
42 rewrite > H.reflexivity.
45 theorem eq_sigma_p: \forall p1,p2:nat \to bool.
46 \forall g1,g2: nat \to Z.\forall n.
47 (\forall x. x < n \to p1 x = p2 x) \to
48 (\forall x. x < n \to g1 x = g2 x) \to
49 sigma_p n p1 g1 = sigma_p n p2 g2.
52 |apply (bool_elim ? (p1 n1))
54 rewrite > (true_to_sigma_p_Sn ? ? ? H3).
55 rewrite > true_to_sigma_p_Sn
59 [intros.apply H1.apply le_S.assumption
60 |intros.apply H2.apply le_S.assumption
63 |rewrite < H3.apply sym_eq.apply H1.apply le_n
66 rewrite > (false_to_sigma_p_Sn ? ? ? H3).
67 rewrite > false_to_sigma_p_Sn
69 [intros.apply H1.apply le_S.assumption
70 |intros.apply H2.apply le_S.assumption
72 |rewrite < H3.apply sym_eq.apply H1.apply le_n
78 theorem eq_sigma_p1: \forall p1,p2:nat \to bool.
79 \forall g1,g2: nat \to Z.\forall n.
80 (\forall x. x < n \to p1 x = p2 x) \to
81 (\forall x. x < n \to p1 x = true \to g1 x = g2 x) \to
82 sigma_p n p1 g1 = sigma_p n p2 g2.
86 |apply (bool_elim ? (p1 n1))
88 rewrite > (true_to_sigma_p_Sn ? ? ? H3).
89 rewrite > true_to_sigma_p_Sn
92 [apply le_n|assumption]
94 [intros.apply H1.apply le_S.assumption
96 [apply le_S.assumption|assumption]
99 |rewrite < H3.apply sym_eq.apply H1.apply le_n
102 rewrite > (false_to_sigma_p_Sn ? ? ? H3).
103 rewrite > false_to_sigma_p_Sn
105 [intros.apply H1.apply le_S.assumption
107 [apply le_S.assumption|assumption]
109 |rewrite < H3.apply sym_eq.apply H1.apply le_n
115 theorem sigma_p_false:
116 \forall g: nat \to Z.\forall n.sigma_p n (\lambda x.false) g = O.
118 elim n[reflexivity|simplify.assumption]
121 theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool.
122 \forall g: nat \to Z.
124 = sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g.
128 |apply (bool_elim ? (p (n1+n)))
130 simplify in \vdash (? ? (? % ? ?) ?).
131 rewrite > (true_to_sigma_p_Sn ? ? ? H1).
132 rewrite > (true_to_sigma_p_Sn n1 (\lambda x.p (x+n)) ? H1).
133 rewrite > assoc_Zplus.
134 rewrite < H.reflexivity
136 simplify in \vdash (? ? (? % ? ?) ?).
137 rewrite > (false_to_sigma_p_Sn ? ? ? H1).
138 rewrite > (false_to_sigma_p_Sn n1 (\lambda x.p (x+n)) ? H1).
144 theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to
145 \forall p:nat \to bool.
146 \forall g: nat \to Z. (\forall i:nat. n \le i \to i < m \to
147 p i = false) \to sigma_p m p g = sigma_p n p g.
156 apply H3[apply H4|apply le_S.assumption]
165 \forall p1,p2:nat \to bool.
166 \forall g: nat \to nat \to Z.
168 (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
169 (\lambda x.g (div x m) (mod x m)) =
171 (\lambda x.sigma_p m p2 (g x)).
174 [simplify.reflexivity
175 |apply (bool_elim ? (p1 n1))
177 rewrite > (true_to_sigma_p_Sn ? ? ? H1).
178 simplify in \vdash (? ? (? % ? ?) ?);
179 rewrite > sigma_p_plus.
185 rewrite > (div_plus_times ? ? ? H2).
186 rewrite > (mod_plus_times ? ? ? H2).
191 rewrite > (div_plus_times ? ? ? H2).
192 rewrite > (mod_plus_times ? ? ? H2).
194 simplify.reflexivity.
199 rewrite > (false_to_sigma_p_Sn ? ? ? H1).
200 simplify in \vdash (? ? (? % ? ?) ?);
201 rewrite > sigma_p_plus.
203 apply (trans_eq ? ? (O+(sigma_p n1 p1 (\lambda x:nat.sigma_p m p2 (g x)))))
205 [rewrite > (eq_sigma_p ? (\lambda x.false) ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
209 rewrite > (div_plus_times ? ? ? H2).
210 rewrite > (mod_plus_times ? ? ? H2).
223 lemma sigma_p_gi: \forall g: nat \to Z.
224 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
225 sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
229 apply (not_le_Sn_O i).
231 |apply (bool_elim ? (p n1));intro
232 [elim (le_to_or_lt_eq i n1)
233 [rewrite > true_to_sigma_p_Sn
234 [rewrite > true_to_sigma_p_Sn
235 [rewrite < assoc_Zplus.
236 rewrite < sym_Zplus in \vdash (? ? ? (? % ?)).
237 rewrite > assoc_Zplus.
240 |apply H[assumption|assumption]
242 |rewrite > H3.simplify.
243 change with (notb (eqb n1 i) = notb false).
245 apply not_eq_to_eqb_false.
247 apply (lt_to_not_eq ? ? H4).
248 apply sym_eq.assumption
252 |rewrite > true_to_sigma_p_Sn
256 |rewrite > false_to_sigma_p_Sn
261 change with (notb false = notb (eqb x n1)).
264 apply not_eq_to_eqb_false.
265 apply (lt_to_not_eq ? ? H5)
271 rewrite > (eq_to_eqb_true ? ? (refl_eq ? n1)).
277 |apply le_S_S_to_le.assumption
279 |rewrite > false_to_sigma_p_Sn
280 [elim (le_to_or_lt_eq i n1)
281 [rewrite > false_to_sigma_p_Sn
282 [apply H[assumption|assumption]
283 |rewrite > H3.reflexivity
286 apply not_eq_true_false.
290 |apply le_S_S_to_le.assumption
298 theorem eq_sigma_p_gh:
299 \forall g: nat \to Z.
300 \forall h,h1: nat \to nat.\forall n,n1.
301 \forall p1,p2:nat \to bool.
302 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
303 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
304 (\forall i. i < n \to p1 i = true \to h i < n1) \to
305 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
306 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
307 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
308 sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 (\lambda x.p2 x) g.
311 [generalize in match H5.
314 |apply (bool_elim ? (p2 n2));intro
316 apply (not_le_Sn_O (h1 n2)).
318 [apply le_n|assumption]
319 |rewrite > false_to_sigma_p_Sn
322 apply H7[apply le_S.apply H9|assumption]
327 |apply (bool_elim ? (p1 n1));intro
328 [rewrite > true_to_sigma_p_Sn
329 [rewrite > (sigma_p_gi g n2 (h n1))
336 change with ((\not eqb (h i) (h n1))= \not false).
338 apply not_eq_to_eqb_false.
340 apply (lt_to_not_eq ? ? H8).
343 [apply eq_f.assumption|apply le_n|assumption]
344 |apply le_S.assumption
347 |apply le_S.assumption
351 apply H2[apply le_S.assumption|assumption]
353 apply H3[apply le_S.assumption|assumption]
357 |generalize in match H9.
359 [reflexivity|assumption]
364 |generalize in match H9.
366 [reflexivity|assumption]
369 elim (le_to_or_lt_eq (h1 j) n1)
371 |generalize in match H9.
377 [reflexivity|assumption|auto]
378 |apply eqb_false_to_not_eq.
379 generalize in match H11.
381 [apply sym_eq.assumption|reflexivity]
385 apply not_eq_true_false.
386 apply sym_eq.assumption
391 |generalize in match H9.
393 [reflexivity|assumption]
398 |apply H3[apply le_n|assumption]
399 |apply H1[apply le_n|assumption]
403 |rewrite > false_to_sigma_p_Sn
405 [intros.apply H1[apply le_S.assumption|assumption]
406 |intros.apply H2[apply le_S.assumption|assumption]
407 |intros.apply H3[apply le_S.assumption|assumption]
408 |intros.apply H4[assumption|assumption]
409 |intros.apply H5[assumption|assumption]
411 elim (le_to_or_lt_eq (h1 j) n1)
416 [reflexivity|assumption|assumption]
418 apply not_eq_true_false.
422 [reflexivity|assumption|assumption]
425 apply H6[assumption|assumption]
434 definition p_ord_times \def
437 [pair q r \Rightarrow r*m+q].
439 theorem eq_p_ord_times: \forall p,m,x.
440 p_ord_times p m x = (ord_rem x p)*m+(ord x p).
441 intros.unfold p_ord_times. unfold ord_rem.
447 theorem div_p_ord_times:
448 \forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
449 intros.rewrite > eq_p_ord_times.
450 apply div_plus_times.
454 theorem mod_p_ord_times:
455 \forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
456 intros.rewrite > eq_p_ord_times.
457 apply mod_plus_times.
461 theorem times_O_to_O: \forall n,m:nat.n*m = O \to n = O \lor m= O.
462 apply nat_elim2;intros
467 apply (not_eq_O_S ? (sym_eq ? ? ? H1))
471 theorem prime_to_lt_O: \forall p. prime p \to O < p.
472 intros.elim H.apply lt_to_le.assumption.
475 theorem divides_exp_to_lt_ord:\forall n,m,j,p. O < n \to prime p \to
476 p \ndivides n \to j \divides n*(exp p m) \to ord j p < S m.
478 cut (m = ord (n*(exp p m)) p)
481 apply divides_to_le_ord
482 [elim (le_to_or_lt_eq ? ? (le_O_n j))
485 apply (lt_to_not_eq ? ? H).
487 rewrite < H4 in H5.simplify in H5.
488 elim (times_O_to_O ? ? H5)
489 [apply sym_eq.assumption
491 apply (not_le_Sn_n O).
492 rewrite < H6 in \vdash (? ? %).
494 elim H1.apply lt_to_le.assumption
497 |rewrite > (times_n_O O).
499 [assumption|apply lt_O_exp.apply (prime_to_lt_O ? H1)]
504 rewrite > (p_ord_exp1 p ? m n)
506 |apply (prime_to_lt_O ? H1)
513 theorem divides_exp_to_divides_ord_rem:\forall n,m,j,p. O < n \to prime p \to
514 p \ndivides n \to j \divides n*(exp p m) \to ord_rem j p \divides n.
517 [cut (n = ord_rem (n*(exp p m)) p)
519 apply divides_to_divides_ord_rem
521 |rewrite > (times_n_O O).
523 [assumption|apply lt_O_exp.apply (prime_to_lt_O ? H1)]
528 rewrite > (p_ord_exp1 p ? m n)
530 |apply (prime_to_lt_O ? H1)
535 |elim (le_to_or_lt_eq ? ? (le_O_n j))
538 apply (lt_to_not_eq ? ? H).
540 rewrite < H4 in H5.simplify in H5.
541 elim (times_O_to_O ? ? H5)
542 [apply sym_eq.assumption
544 apply (not_le_Sn_n O).
545 rewrite < H6 in \vdash (? ? %).
547 elim H1.apply lt_to_le.assumption
553 theorem sigma_p_divides_b:
554 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
555 \forall g: nat \to Z.
556 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
557 sigma_p (S n) (\lambda x.divides_b x n)
558 (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
563 (sigma_p (S n*S m) (\lambda x:nat.divides_b (x/S m) n)
564 (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m)))))
566 apply (eq_sigma_p_gh g ? (p_ord_times p (S m)))
568 lapply (divides_b_true_to_lt_O ? ? H H4).
569 apply divides_to_divides_b_true
570 [rewrite > (times_n_O O).
573 |apply lt_O_exp.assumption
576 [apply divides_b_true_to_divides.assumption
577 |apply (witness ? ? (p \sup (m-i \mod (S m)))).
578 rewrite < exp_plus_times.
581 apply plus_minus_m_m.
586 lapply (divides_b_true_to_lt_O ? ? H H4).
588 rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
589 [change with ((i/S m)*S m+i \mod S m=i).
596 apply (trans_divides ? (i/ S m))
598 apply divides_b_true_to_divides;assumption]
605 change with ((i/S m) < S n).
606 apply (lt_times_to_lt_l m).
607 apply (le_to_lt_to_lt ? i)
618 [rewrite > div_p_ord_times
619 [apply divides_to_divides_b_true
622 |apply (divides_b_true_to_lt_O ? ? ? H4).
623 rewrite > (times_n_O O).
625 [assumption|apply lt_O_exp.assumption]
627 |apply (divides_exp_to_divides_ord_rem ? m ? ? H H1 H2).
628 apply divides_b_true_to_divides.
633 |apply (divides_exp_to_lt_ord ? ? ? ? H H1 H2).
634 apply (divides_b_true_to_divides ? ? H4).
635 apply (divides_b_true_to_lt_O ? ? H4)
639 [rewrite > div_p_ord_times
640 [rewrite > mod_p_ord_times
641 [rewrite > sym_times.
645 |apply (divides_b_true_to_lt_O ? ? ? H4).
646 rewrite > (times_n_O O).
648 [assumption|apply lt_O_exp.assumption]
650 |apply (divides_exp_to_lt_ord ? ? ? ? H H1 H2).
651 apply (divides_b_true_to_divides ? ? H4).
652 apply (divides_b_true_to_lt_O ? ? H4)
656 |apply (divides_exp_to_lt_ord ? ? ? ? H H1 H2).
657 apply (divides_b_true_to_divides ? ? H4).
658 apply (divides_b_true_to_lt_O ? ? H4).
661 rewrite > eq_p_ord_times.
663 apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
666 cut (m = ord (n*(p \sup m)) p)
668 apply divides_to_le_ord
669 [apply (divides_b_true_to_lt_O ? ? ? H4).
670 rewrite > (times_n_O O).
672 [assumption|apply lt_O_exp.assumption]
673 |rewrite > (times_n_O O).
675 [assumption|apply lt_O_exp.assumption]
677 |apply divides_b_true_to_divides.
682 rewrite > (p_ord_exp1 p ? m n)
689 |change with (S (ord_rem j p)*S m \le S n*S m).
694 |apply (divides_exp_to_divides_ord_rem ? m ? ? H H1 H2).
695 apply divides_b_true_to_divides.
702 elim (divides_b (x/S m) n);reflexivity
706 |elim H1.apply lt_to_le.assumption