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/nat/iteration2".
17 include "nat/primes.ma".
19 include "nat/generic_iter_p.ma".
20 include "nat/count.ma".(*necessary just to use bool_to_nat and bool_to_nat_andb*)
23 (* sigma_p on nautral numbers is a specialization of sigma_p_gen *)
24 definition sigma_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def
25 \lambda n, p, g. (iter_p_gen n p nat g O plus).
27 theorem symmetricIntPlus: symmetric nat plus.
28 change with (\forall a,b:nat. (plus a b) = (plus b a)).
34 (*the following theorems on sigma_p in N are obtained by the more general ones
37 theorem true_to_sigma_p_Sn:
38 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
39 p n = true \to sigma_p (S n) p g =
40 (g n)+(sigma_p n p g).
43 apply true_to_iter_p_gen_Sn.
47 theorem false_to_sigma_p_Sn:
48 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
49 p n = false \to sigma_p (S n) p g = sigma_p n p g.
52 apply false_to_iter_p_gen_Sn.
56 theorem eq_sigma_p: \forall p1,p2:nat \to bool.
57 \forall g1,g2: nat \to nat.\forall n.
58 (\forall x. x < n \to p1 x = p2 x) \to
59 (\forall x. x < n \to g1 x = g2 x) \to
60 sigma_p n p1 g1 = sigma_p n p2 g2.
67 theorem eq_sigma_p1: \forall p1,p2:nat \to bool.
68 \forall g1,g2: nat \to nat.\forall n.
69 (\forall x. x < n \to p1 x = p2 x) \to
70 (\forall x. x < n \to p1 x = true \to g1 x = g2 x) \to
71 sigma_p n p1 g1 = sigma_p n p2 g2.
78 theorem sigma_p_false:
79 \forall g: nat \to nat.\forall n.sigma_p n (\lambda x.false) g = O.
82 apply iter_p_gen_false.
85 theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool.
86 \forall g: nat \to nat.
88 = sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g.
91 apply (iter_p_gen_plusA nat n k p g O plus)
92 [ apply symmetricIntPlus.
96 | apply associative_plus
100 theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to
101 \forall p:nat \to bool.
102 \forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to
103 p i = false) \to sigma_p m p g = sigma_p n p g.
106 apply (false_to_eq_iter_p_gen);
112 \forall p1,p2:nat \to bool.
113 \forall g: nat \to nat \to nat.
115 (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
116 (\lambda x.g (div x m) (mod x m)) =
118 (\lambda x.sigma_p m p2 (g x)).
121 apply (iter_p_gen2 n m p1 p2 nat g O plus)
122 [ apply symmetricIntPlus
123 | apply associative_plus
132 \forall p1:nat \to bool.
133 \forall p2:nat \to nat \to bool.
134 \forall g: nat \to nat \to nat.
136 (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x m)))
137 (\lambda x.g (div x m) (mod x m)) =
139 (\lambda x.sigma_p m (p2 x) (g x)).
142 apply (iter_p_gen2' n m p1 p2 nat g O plus)
143 [ apply symmetricIntPlus
144 | apply associative_plus
151 lemma sigma_p_gi: \forall g: nat \to nat.
152 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
153 sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
156 apply (iter_p_gen_gi)
157 [ apply symmetricIntPlus
158 | apply associative_plus
167 theorem eq_sigma_p_gh:
168 \forall g,h,h1: nat \to nat.\forall n,n1.
169 \forall p1,p2:nat \to bool.
170 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
171 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
172 (\forall i. i < n \to p1 i = true \to h i < n1) \to
173 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
174 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
175 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
176 sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 p2 g.
179 apply (eq_iter_p_gen_gh nat O plus ? ? ? g h h1 n n1 p1 p2)
180 [ apply symmetricIntPlus
181 | apply associative_plus
195 theorem sigma_p_divides:
196 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
197 \forall g: nat \to nat.
198 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
199 sigma_p (S n) (\lambda x.divides_b x n)
200 (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
203 apply (iter_p_gen_divides nat O plus n m p ? ? ? g)
207 | apply symmetricIntPlus
208 | apply associative_plus
215 theorem distributive_times_plus_sigma_p: \forall n,k:nat. \forall p:nat \to bool. \forall g:nat \to nat.
216 k*(sigma_p n p g) = sigma_p n p (\lambda i:nat.k * (g i)).
218 apply (distributive_times_plus_iter_p_gen nat plus O times n k p g)
219 [ apply symmetricIntPlus
220 | apply associative_plus
224 | apply symmetric_times
225 | apply distributive_times_plus
227 rewrite < (times_n_O a).
232 (*some properties of sigma_p invoked with an "always true" predicate (in this
233 way sigma_p just counts the elements, without doing any control) or with
234 the nat \to nat function which always returns (S O).
235 It 's not easily possible proving these theorems in a general form
236 in generic_sigma_p.ma
239 theorem sigma_p_true: \forall n:nat.
240 (sigma_p n (\lambda x.true) (\lambda x.S O)) = n.
245 | rewrite > (true_to_sigma_p_Sn n1 (\lambda x:nat.true) (\lambda x:nat.S O))
254 theorem sigma_P_SO_to_sigma_p_true: \forall n:nat. \forall g:nat \to bool.
255 sigma_p n g (\lambda n:nat. (S O)) =
256 sigma_p n (\lambda x:nat.true) (\lambda i:nat.bool_to_nat (g i)).
261 | cut ((g n1) = true \lor (g n1) = false)
262 [ rewrite > true_to_sigma_p_Sn in \vdash (? ? ? %)
265 rewrite > true_to_sigma_p_Sn in \vdash (? ? % ?)
272 rewrite > false_to_sigma_p_Sn in \vdash (? ? % ?)
290 (* I introduce an equivalence in the form map_iter_i in order to use
291 * the existing result about permutation in that part of the library.
294 theorem eq_map_iter_i_sigma_p_alwaysTrue: \forall n:nat.\forall g:nat \to nat.
295 map_iter_i n g plus O = sigma_p (S n) (\lambda c:nat.true) g.
301 | rewrite > true_to_sigma_p_Sn
302 [ simplify in \vdash (? ? % ?).
311 theorem sigma_p_plus_1: \forall n:nat. \forall f,g:nat \to nat.
312 sigma_p n (\lambda b:nat. true) (\lambda a:nat.(f a) + (g a)) =
313 sigma_p n (\lambda b:nat. true) f + sigma_p n (\lambda b:nat. true) g.
318 | rewrite > true_to_sigma_p_Sn
319 [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) f)
320 [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) g)
321 [ rewrite > assoc_plus in \vdash (? ? ? %).
322 rewrite < assoc_plus in \vdash (? ? ? (? ? %)).
323 rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))).
324 rewrite > assoc_plus in \vdash (? ? ? (? ? %)).
325 rewrite < assoc_plus in \vdash (? ? ? %).
338 theorem eq_sigma_p_sigma_p_times1 : \forall n,m:nat.\forall f:nat \to nat.
339 sigma_p (n*m) (\lambda x:nat.true) f =
340 sigma_p m (\lambda x:nat.true)
341 (\lambda a.(sigma_p n (\lambda x:nat.true) (\lambda b.f (b*m + a)))).
348 | rewrite > true_to_sigma_p_Sn
354 | change in \vdash (? ? ? (? ? ? (\lambda a:?.%))) with ((f ((n1*m)+a)) +
355 (sigma_p n1 (\lambda x:nat.true) (\lambda b:nat.f (b*m +a)))).
356 rewrite > sigma_p_plus_1 in \vdash (? ? ? %).
357 rewrite > (sym_times (S n1) m).
358 rewrite < (times_n_Sm m n1).
359 rewrite > sigma_p_plus in \vdash (? ? % ?).
361 [ rewrite < (sym_times m n1).
366 rewrite < (sym_plus ? (m * n1)).
369 | rewrite > (sym_times m n1).
375 theorem eq_sigma_p_sigma_p_times2 : \forall n,m:nat.\forall f:nat \to nat.
376 sigma_p (n *m) (\lambda c:nat.true) f =
377 sigma_p n (\lambda c:nat.true)
378 (\lambda a.(sigma_p m (\lambda c:nat.true) (\lambda b:nat.f (b* n + a)))).
381 apply eq_sigma_p_sigma_p_times1.
385 theorem sigma_p_times:\forall n,m:nat.
386 \forall f,f1,f2:nat \to bool.
387 \forall g:nat \to nat \to nat.
388 \forall g1,g2: nat \to nat.
389 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g b a) < (S n)*(S m)) \to
390 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g1 (g b a)) = a) \to
391 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g2 (g b a)) = b) \to
392 (\forall a,b:nat. a < (S n) \to b < (S m) \to f (g b a) = andb (f2 b) (f1 a)) \to
393 (sigma_p ((S n) * (S m)) f (\lambda c:nat.(S O))) =
394 sigma_p (S n) f1 (\lambda c:nat.(S O)) * sigma_p (S m) f2 (\lambda c:nat.(S O)).
397 rewrite > (sigma_P_SO_to_sigma_p_true ).
398 rewrite > (S_pred ((S n)*(S m))) in \vdash (? ? (? % ? ?) ?)
399 [ rewrite < (eq_map_iter_i_sigma_p_alwaysTrue (pred ((S n)* (S m)))).
400 rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ?
401 (\lambda i.g (div i (S n)) (mod i (S n))))
402 [ rewrite > eq_map_iter_i_sigma_p_alwaysTrue.
404 [ rewrite > eq_sigma_p_sigma_p_times2.
405 apply (trans_eq ? ? (sigma_p (S n) (\lambda c:nat.true)
406 (\lambda a. sigma_p (S m) (\lambda c:nat.true)
407 (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))))))
408 [ apply eq_sigma_p;intros
410 | apply eq_sigma_p;intros
413 rewrite > (div_mod_spec_to_eq (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
414 ((x1*(S n) + x) \mod (S n)) x1 x)
415 [ rewrite > (div_mod_spec_to_eq2 (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
416 ((x1*(S n) + x) \mod (S n)) x1 x)
418 [ apply bool_to_nat_andb
422 | apply div_mod_spec_div_mod.
429 | apply div_mod_spec_div_mod.
438 | apply (trans_eq ? ?
439 (sigma_p (S n) (\lambda c:nat.true) (\lambda n.((bool_to_nat (f1 n)) *
440 (sigma_p (S m) (\lambda c:nat.true) (\lambda n.bool_to_nat (f2 n)))))))
441 [ apply eq_sigma_p;intros
443 | rewrite > distributive_times_plus_sigma_p.
444 apply eq_sigma_p;intros
446 | rewrite > sym_times.
451 rewrite > sigma_P_SO_to_sigma_p_true.
452 rewrite > sigma_P_SO_to_sigma_p_true in \vdash (? ? (? ? %) ?).
454 rewrite > distributive_times_plus_sigma_p.
455 apply eq_sigma_p;intros
457 | rewrite > distributive_times_plus_sigma_p.
459 rewrite > distributive_times_plus_sigma_p.
465 | apply lt_O_times_S_S
473 rewrite < S_pred in \vdash (? ? %)
474 [ change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
480 | apply (lt_times_to_lt_l n).
481 apply (le_to_lt_to_lt ? i)
482 [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
483 [ rewrite > sym_plus.
490 rewrite > S_pred in \vdash (? ? %)
492 rewrite > plus_n_O in \vdash (? ? %).
495 | apply lt_O_times_S_S
499 | apply lt_O_times_S_S
501 | rewrite < plus_n_O.
504 cut (i < (S n)*(S m))
505 [ cut (j < (S n)*(S m))
506 [ cut ((i \mod (S n)) < (S n))
507 [ cut ((i/(S n)) < (S m))
508 [ cut ((j \mod (S n)) < (S n))
509 [ cut ((j/(S n)) < (S m))
510 [ rewrite > (div_mod i (S n))
511 [ rewrite > (div_mod j (S n))
512 [ rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
513 rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
514 rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
515 rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
526 | apply (lt_times_to_lt_l n).
527 apply (le_to_lt_to_lt ? j)
528 [ rewrite > (div_mod j (S n)) in \vdash (? ? %)
529 [ rewrite > sym_plus.
531 | unfold lt. apply le_S_S.
534 | rewrite < sym_times.
543 | apply (lt_times_to_lt_l n).
544 apply (le_to_lt_to_lt ? i)
545 [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
546 [ rewrite > sym_plus.
552 | rewrite < sym_times.
562 rewrite > S_pred in \vdash (? ? %)
565 | apply lt_O_times_S_S
569 rewrite > S_pred in \vdash (? ? %)
572 | apply lt_O_times_S_S
578 apply (not_le_Sn_O m1 H4)
580 | apply lt_O_times_S_S
585 \forall g: nat \to nat.
586 \forall h2:nat \to nat \to nat.
587 \forall h11,h12:nat \to nat.
589 \forall p1,p21:nat \to bool.
590 \forall p22:nat \to nat \to bool.
591 (\forall x. x < k \to p1 x = true \to
592 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
593 \land h2 (h11 x) (h12 x) = x
594 \land (h11 x) < n \land (h12 x) < m) \to
595 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
596 p1 (h2 i j) = true \land
597 h11 (h2 i j) = i \land h12 (h2 i j) = j
598 \land h2 i j < k) \to
600 sigma_p n p21 (\lambda x:nat.sigma_p m (p22 x) (\lambda y. g (h2 x y))).
603 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
605 [apply symmetricIntPlus
606 |apply associative_plus
607 |intro.rewrite < plus_n_O.reflexivity
617 \forall g: nat \to nat \to nat.
618 \forall h11,h12,h21,h22: nat \to nat \to nat.
620 \forall p11,p21:nat \to bool.
621 \forall p12,p22:nat \to nat \to bool.
622 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
623 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
624 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
625 \land h11 i j < n1 \land h12 i j < m1) \to
626 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
627 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
628 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
629 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
630 sigma_p n1 p11 (\lambda x:nat .sigma_p m1 (p12 x) (\lambda y. g x y)) =
631 sigma_p n2 p21 (\lambda x:nat .sigma_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
634 unfold sigma_p in \vdash (? ? (? ? ? ? (\lambda x:?.%) ? ?) ?).
635 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
637 apply(iter_p_gen_2_eq nat O plus ? ? ? g h11 h12 h21 h22 n1 m1 n2 m2 p11 p21 p12 p22)
638 [ apply symmetricIntPlus
639 | apply associative_plus
641 rewrite < (plus_n_O).