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_sigma_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. (sigma_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_sigma_p_Sn_gen.
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_sigma_p_Sn_gen.
57 theorem eq_sigma_p: \forall p1,p2:nat \to bool.
58 \forall g1,g2: nat \to nat.\forall n.
59 (\forall x. x < n \to p1 x = p2 x) \to
60 (\forall x. x < n \to g1 x = g2 x) \to
61 sigma_p n p1 g1 = sigma_p n p2 g2.
68 theorem eq_sigma_p1: \forall p1,p2:nat \to bool.
69 \forall g1,g2: nat \to nat.\forall n.
70 (\forall x. x < n \to p1 x = p2 x) \to
71 (\forall x. x < n \to p1 x = true \to g1 x = g2 x) \to
72 sigma_p n p1 g1 = sigma_p n p2 g2.
75 apply eq_sigma_p1_gen;
79 theorem sigma_p_false:
80 \forall g: nat \to nat.\forall n.sigma_p n (\lambda x.false) g = O.
83 apply sigma_p_false_gen.
86 theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool.
87 \forall g: nat \to nat.
89 = sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g.
92 apply (sigma_p_plusA_gen nat n k p g O plus)
93 [ apply symmetricIntPlus.
97 | apply associative_plus
101 theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to
102 \forall p:nat \to bool.
103 \forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to
104 p i = false) \to sigma_p m p g = sigma_p n p g.
107 apply (false_to_eq_sigma_p_gen);
113 \forall p1,p2:nat \to bool.
114 \forall g: nat \to nat \to nat.
116 (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
117 (\lambda x.g (div x m) (mod x m)) =
119 (\lambda x.sigma_p m p2 (g x)).
122 apply (sigma_p2_gen n m p1 p2 nat g O plus)
123 [ apply symmetricIntPlus
124 | apply associative_plus
133 \forall p1:nat \to bool.
134 \forall p2:nat \to nat \to bool.
135 \forall g: nat \to nat \to nat.
137 (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x m)))
138 (\lambda x.g (div x m) (mod x m)) =
140 (\lambda x.sigma_p m (p2 x) (g x)).
143 apply (sigma_p2_gen' n m p1 p2 nat g O plus)
144 [ apply symmetricIntPlus
145 | apply associative_plus
152 lemma sigma_p_gi: \forall g: nat \to nat.
153 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
154 sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
157 apply (sigma_p_gi_gen)
158 [ apply symmetricIntPlus
159 | apply associative_plus
168 theorem eq_sigma_p_gh:
169 \forall g,h,h1: nat \to nat.\forall n,n1.
170 \forall p1,p2:nat \to bool.
171 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
172 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
173 (\forall i. i < n \to p1 i = true \to h i < n1) \to
174 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
175 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
176 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
177 sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 (\lambda x.p2 x) g.
180 apply (eq_sigma_p_gh_gen nat O plus ? ? ? g h h1 n n1 p1 p2)
181 [ apply symmetricIntPlus
182 | apply associative_plus
196 theorem sigma_p_divides:
197 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
198 \forall g: nat \to nat.
199 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
200 sigma_p (S n) (\lambda x.divides_b x n)
201 (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
204 apply (sigma_p_divides_gen nat O plus n m p ? ? ? g)
208 | apply symmetricIntPlus
209 | apply associative_plus
216 theorem distributive_times_plus_sigma_p: \forall n,k:nat. \forall p:nat \to bool. \forall g:nat \to nat.
217 k*(sigma_p n p g) = sigma_p n p (\lambda i:nat.k * (g i)).
219 apply (distributive_times_plus_sigma_p_generic nat plus O times n k p g)
220 [ apply symmetricIntPlus
221 | apply associative_plus
225 | apply symmetric_times
226 | apply distributive_times_plus
228 rewrite < (times_n_O a).
233 (*some properties of sigma_p invoked with an "always true" predicate (in this
234 way sigma_p just counts the elements, without doing any control) or with
235 the nat \to nat function which always returns (S O).
236 It 's not easily possible proving these theorems in a general form
237 in generic_sigma_p.ma
240 theorem sigma_p_true: \forall n:nat.
241 (sigma_p n (\lambda x.true) (\lambda x.S O)) = n.
246 | rewrite > (true_to_sigma_p_Sn n1 (\lambda x:nat.true) (\lambda x:nat.S O))
255 theorem sigma_P_SO_to_sigma_p_true: \forall n:nat. \forall g:nat \to bool.
256 sigma_p n g (\lambda n:nat. (S O)) =
257 sigma_p n (\lambda x:nat.true) (\lambda i:nat.bool_to_nat (g i)).
262 | cut ((g n1) = true \lor (g n1) = false)
263 [ rewrite > true_to_sigma_p_Sn in \vdash (? ? ? %)
266 rewrite > true_to_sigma_p_Sn in \vdash (? ? % ?)
273 rewrite > false_to_sigma_p_Sn in \vdash (? ? % ?)
291 (* I introduce an equivalence in the form map_iter_i in order to use
292 * the existing result about permutation in that part of the library.
295 theorem eq_map_iter_i_sigma_p_alwaysTrue: \forall n:nat.\forall g:nat \to nat.
296 map_iter_i n g plus O = sigma_p (S n) (\lambda c:nat.true) g.
302 | rewrite > true_to_sigma_p_Sn
303 [ simplify in \vdash (? ? % ?).
312 theorem sigma_p_plus_1: \forall n:nat. \forall f,g:nat \to nat.
313 sigma_p n (\lambda b:nat. true) (\lambda a:nat.(f a) + (g a)) =
314 sigma_p n (\lambda b:nat. true) f + sigma_p n (\lambda b:nat. true) g.
319 | rewrite > true_to_sigma_p_Sn
320 [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) f)
321 [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) g)
322 [ rewrite > assoc_plus in \vdash (? ? ? %).
323 rewrite < assoc_plus in \vdash (? ? ? (? ? %)).
324 rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))).
325 rewrite > assoc_plus in \vdash (? ? ? (? ? %)).
326 rewrite < assoc_plus in \vdash (? ? ? %).
339 theorem eq_sigma_p_sigma_p_times1 : \forall n,m:nat.\forall f:nat \to nat.
340 sigma_p (n*m) (\lambda x:nat.true) f =
341 sigma_p m (\lambda x:nat.true)
342 (\lambda a.(sigma_p n (\lambda x:nat.true) (\lambda b.f (b*m + a)))).
349 | rewrite > true_to_sigma_p_Sn
355 | change in \vdash (? ? ? (? ? ? (\lambda a:?.%))) with ((f ((n1*m)+a)) +
356 (sigma_p n1 (\lambda x:nat.true) (\lambda b:nat.f (b*m +a)))).
357 rewrite > sigma_p_plus_1 in \vdash (? ? ? %).
358 rewrite > (sym_times (S n1) m).
359 rewrite < (times_n_Sm m n1).
360 rewrite > sigma_p_plus in \vdash (? ? % ?).
362 [ rewrite < (sym_times m n1).
367 rewrite < (sym_plus ? (m * n1)).
370 | rewrite > (sym_times m n1).
376 theorem eq_sigma_p_sigma_p_times2 : \forall n,m:nat.\forall f:nat \to nat.
377 sigma_p (n *m) (\lambda c:nat.true) f =
378 sigma_p n (\lambda c:nat.true)
379 (\lambda a.(sigma_p m (\lambda c:nat.true) (\lambda b:nat.f (b* n + a)))).
382 apply eq_sigma_p_sigma_p_times1.
386 theorem sigma_p_times:\forall n,m:nat.
387 \forall f,f1,f2:nat \to bool.
388 \forall g:nat \to nat \to nat.
389 \forall g1,g2: nat \to nat.
390 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g b a) < (S n)*(S m)) \to
391 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g1 (g b a)) = a) \to
392 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g2 (g b a)) = b) \to
393 (\forall a,b:nat. a < (S n) \to b < (S m) \to f (g b a) = andb (f2 b) (f1 a)) \to
394 (sigma_p ((S n) * (S m)) f (\lambda c:nat.(S O))) =
395 sigma_p (S n) f1 (\lambda c:nat.(S O)) * sigma_p (S m) f2 (\lambda c:nat.(S O)).
398 rewrite > (sigma_P_SO_to_sigma_p_true ).
399 rewrite > (S_pred ((S n)*(S m))) in \vdash (? ? (? % ? ?) ?)
400 [ rewrite < (eq_map_iter_i_sigma_p_alwaysTrue (pred ((S n)* (S m)))).
401 rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ?
402 (\lambda i.g (div i (S n)) (mod i (S n))))
403 [ rewrite > eq_map_iter_i_sigma_p_alwaysTrue.
405 [ rewrite > eq_sigma_p_sigma_p_times2.
406 apply (trans_eq ? ? (sigma_p (S n) (\lambda c:nat.true)
407 (\lambda a. sigma_p (S m) (\lambda c:nat.true)
408 (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))))))
409 [ apply eq_sigma_p;intros
411 | apply eq_sigma_p;intros
414 rewrite > (div_mod_spec_to_eq (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
415 ((x1*(S n) + x) \mod (S n)) x1 x)
416 [ rewrite > (div_mod_spec_to_eq2 (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
417 ((x1*(S n) + x) \mod (S n)) x1 x)
419 [ apply bool_to_nat_andb
423 | apply div_mod_spec_div_mod.
430 | apply div_mod_spec_div_mod.
439 | apply (trans_eq ? ?
440 (sigma_p (S n) (\lambda c:nat.true) (\lambda n.((bool_to_nat (f1 n)) *
441 (sigma_p (S m) (\lambda c:nat.true) (\lambda n.bool_to_nat (f2 n)))))))
442 [ apply eq_sigma_p;intros
444 | rewrite > distributive_times_plus_sigma_p.
445 apply eq_sigma_p;intros
447 | rewrite > sym_times.
452 rewrite > sigma_P_SO_to_sigma_p_true.
453 rewrite > sigma_P_SO_to_sigma_p_true in \vdash (? ? (? ? %) ?).
455 rewrite > distributive_times_plus_sigma_p.
456 apply eq_sigma_p;intros
458 | rewrite > distributive_times_plus_sigma_p.
460 rewrite > distributive_times_plus_sigma_p.
466 | apply lt_O_times_S_S
474 rewrite < S_pred in \vdash (? ? %)
475 [ change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
481 | apply (lt_times_to_lt_l n).
482 apply (le_to_lt_to_lt ? i)
483 [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
484 [ rewrite > sym_plus.
491 rewrite > S_pred in \vdash (? ? %)
493 rewrite > plus_n_O in \vdash (? ? %).
496 | apply lt_O_times_S_S
500 | apply lt_O_times_S_S
502 | rewrite < plus_n_O.
505 cut (i < (S n)*(S m))
506 [ cut (j < (S n)*(S m))
507 [ cut ((i \mod (S n)) < (S n))
508 [ cut ((i/(S n)) < (S m))
509 [ cut ((j \mod (S n)) < (S n))
510 [ cut ((j/(S n)) < (S m))
511 [ rewrite > (div_mod i (S n))
512 [ rewrite > (div_mod j (S n))
513 [ rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
514 rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
515 rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
516 rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
527 | apply (lt_times_to_lt_l n).
528 apply (le_to_lt_to_lt ? j)
529 [ rewrite > (div_mod j (S n)) in \vdash (? ? %)
530 [ rewrite > sym_plus.
532 | unfold lt. apply le_S_S.
535 | rewrite < sym_times.
544 | apply (lt_times_to_lt_l n).
545 apply (le_to_lt_to_lt ? i)
546 [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
547 [ rewrite > sym_plus.
553 | rewrite < sym_times.
563 rewrite > S_pred in \vdash (? ? %)
566 | apply lt_O_times_S_S
570 rewrite > S_pred in \vdash (? ? %)
573 | apply lt_O_times_S_S
579 apply (not_le_Sn_O m1 H4)
581 | apply lt_O_times_S_S