]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/iteration2.ma
...
[helm.git] / helm / software / matita / library / nat / iteration2.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/primes.ma".
16 include "nat/ord.ma".
17 include "nat/generic_iter_p.ma".
18 include "nat/count.ma".(*necessary just to use bool_to_nat and bool_to_nat_andb*)
19
20 (* sigma_p on nautral numbers is a specialization of sigma_p_gen *)
21 definition sigma_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def
22 \lambda n, p, g. (iter_p_gen n p nat g O plus).
23
24 theorem symmetricIntPlus: symmetric nat plus.
25 change with (\forall a,b:nat. (plus a b) = (plus b a)).
26 intros.
27 rewrite > sym_plus.
28 reflexivity.
29 qed.
30    
31 (*the following theorems on sigma_p in N are obtained by the more general ones
32  * in sigma_p_gen.ma
33  *)
34 theorem true_to_sigma_p_Sn: 
35 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
36 p n = true \to sigma_p (S n) p g = 
37 (g n)+(sigma_p n p g).
38 intros.
39 unfold sigma_p.
40 apply true_to_iter_p_gen_Sn.
41 assumption.
42 qed.
43    
44 theorem false_to_sigma_p_Sn: 
45 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
46 p n = false \to sigma_p (S n) p g = sigma_p n p g.
47 intros.
48 unfold sigma_p.
49 apply false_to_iter_p_gen_Sn.
50 assumption.
51 qed.  
52
53 theorem eq_sigma_p: \forall p1,p2:nat \to bool.
54 \forall g1,g2: nat \to nat.\forall n.
55 (\forall x.  x < n \to p1 x = p2 x) \to
56 (\forall x.  x < n \to g1 x = g2 x) \to
57 sigma_p n p1 g1 = sigma_p n p2 g2.
58 intros.
59 unfold sigma_p.
60 apply eq_iter_p_gen;
61   assumption.
62 qed.
63
64 theorem eq_sigma_p1: \forall p1,p2:nat \to bool.
65 \forall g1,g2: nat \to nat.\forall n.
66 (\forall x.  x < n \to p1 x = p2 x) \to
67 (\forall x.  x < n \to p1 x = true \to g1 x = g2 x) \to
68 sigma_p n p1 g1 = sigma_p n p2 g2.
69 intros.
70 unfold sigma_p.
71 apply eq_iter_p_gen1;
72   assumption.
73 qed.
74
75 theorem sigma_p_false: 
76 \forall g: nat \to nat.\forall n.sigma_p n (\lambda x.false) g = O.
77 intros.
78 unfold sigma_p.
79 apply iter_p_gen_false.
80 qed.
81
82 theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool.
83 \forall g: nat \to nat.
84 sigma_p (k+n) p g 
85 = sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g.
86 intros.
87 unfold sigma_p.
88 apply (iter_p_gen_plusA nat n k p g O plus)
89 [ apply symmetricIntPlus.
90 | intros.
91   apply sym_eq.
92   apply plus_n_O
93 | apply associative_plus
94 ]
95 qed.
96
97 theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to
98 \forall p:nat \to bool.
99 \forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to
100 p i = false) \to sigma_p m p g = sigma_p n p g.
101 intros.
102 unfold sigma_p.
103 apply (false_to_eq_iter_p_gen);
104   assumption.
105 qed.
106
107 theorem or_false_to_eq_sigma_p:
108 \forall n,m:nat.\forall p:nat \to bool.
109 \forall g: nat \to nat. 
110 n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = O)
111 \to sigma_p m p g = sigma_p n p g.
112 intros.
113 unfold sigma_p.
114 apply or_false_eq_baseA_to_eq_iter_p_gen
115   [intros.reflexivity
116   |assumption
117   |assumption
118   ]
119 qed.
120
121 theorem bool_to_nat_to_eq_sigma_p:
122 \forall n:nat.\forall p1,p2:nat \to bool.
123 \forall g1,g2: nat \to nat. 
124 (\forall i:nat. 
125 bool_to_nat (p1 i)*(g1 i) = bool_to_nat (p2 i)*(g2 i)) 
126 \to sigma_p n p1 g1 = sigma_p n p2 g2.
127 intros.elim n
128   [reflexivity
129   |generalize in match (H n1).
130    apply (bool_elim ? (p1 n1));intro
131     [apply (bool_elim ? (p2 n1));intros
132       [rewrite > true_to_sigma_p_Sn
133         [rewrite > true_to_sigma_p_Sn
134           [apply eq_f2
135             [simplify in H4.
136              rewrite > plus_n_O.
137              rewrite > plus_n_O in ⊢ (? ? ? %).
138              assumption
139             |assumption
140             ]
141           |assumption
142           ]
143         |assumption
144         ]
145       |rewrite > true_to_sigma_p_Sn
146         [rewrite > false_to_sigma_p_Sn
147           [change in ⊢ (? ? ? %) with (O + sigma_p n1 p2 g2).
148            apply eq_f2
149             [simplify in H4.
150              rewrite > plus_n_O.
151              assumption
152             |assumption
153             ]
154           |assumption
155           ]
156         |assumption
157         ]
158       ]
159     |apply (bool_elim ? (p2 n1));intros
160       [rewrite > false_to_sigma_p_Sn
161         [rewrite > true_to_sigma_p_Sn
162           [change in ⊢ (? ? % ?) with (O + sigma_p n1 p1 g1).
163            apply eq_f2
164             [simplify in H4.
165              rewrite < plus_n_O in H4.
166              assumption
167             |assumption
168             ]
169           |assumption
170           ]
171         |assumption
172         ]
173       |rewrite > false_to_sigma_p_Sn
174         [rewrite > false_to_sigma_p_Sn
175           [assumption
176           |assumption
177           ]
178         |assumption
179         ]
180       ]
181     ]
182   ]
183 qed.
184             
185 theorem sigma_p2 : 
186 \forall n,m:nat.
187 \forall p1,p2:nat \to bool.
188 \forall g: nat \to nat \to nat.
189 sigma_p (n*m) 
190   (\lambda x.andb (p1 (div x m)) (p2 (mod x m))) 
191   (\lambda x.g (div x m) (mod x m)) =
192 sigma_p n p1 
193   (\lambda x.sigma_p m p2 (g x)).
194 intros.
195 unfold sigma_p.
196 apply (iter_p_gen2 n m p1 p2 nat g O plus)
197 [ apply symmetricIntPlus
198 | apply associative_plus
199 | intros.
200   apply sym_eq.
201   apply plus_n_O
202 ]
203 qed.
204
205 theorem sigma_p2' : 
206 \forall n,m:nat.
207 \forall p1:nat \to bool.
208 \forall p2:nat \to nat \to bool.
209 \forall g: nat \to nat \to nat.
210 sigma_p (n*m) 
211   (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x  m))) 
212   (\lambda x.g (div x m) (mod x m)) =
213 sigma_p n p1 
214   (\lambda x.sigma_p m (p2 x) (g x)).
215 intros.
216 unfold sigma_p.
217 apply (iter_p_gen2' n m p1 p2 nat g O plus)
218 [ apply symmetricIntPlus
219 | apply associative_plus
220 | intros.
221   apply sym_eq.
222   apply plus_n_O
223 ]
224 qed.
225
226 lemma sigma_p_gi: \forall g: nat \to nat.
227 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to 
228 sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
229 intros.
230 unfold sigma_p.
231 apply (iter_p_gen_gi)
232 [ apply symmetricIntPlus
233 | apply associative_plus
234 | intros.
235   apply sym_eq.
236   apply plus_n_O
237 | assumption
238 | assumption
239 ]
240 qed.
241
242 theorem eq_sigma_p_gh: 
243 \forall g,h,h1: nat \to nat.\forall n,n1.
244 \forall p1,p2:nat \to bool.
245 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
246 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to 
247 (\forall i. i < n \to p1 i = true \to h i < n1) \to 
248 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
249 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to 
250 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to 
251 sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 p2 g.
252 intros.
253 unfold sigma_p.
254 apply (eq_iter_p_gen_gh nat O plus ? ? ? g h h1 n n1 p1 p2)
255 [ apply symmetricIntPlus
256 | apply associative_plus
257 | intros.
258   apply sym_eq.
259   apply plus_n_O
260 | assumption
261 | assumption
262 | assumption
263 | assumption
264 | assumption
265 | assumption
266 ]
267 qed.
268
269 theorem eq_sigma_p_pred: 
270 \forall n,p,g. p O = true \to
271 sigma_p (S n) (\lambda i.p (pred i)) (\lambda i.g(pred i)) = 
272 plus (sigma_p n p g) (g O).
273 intros.
274 unfold sigma_p.
275 apply eq_iter_p_gen_pred
276   [assumption
277   |apply symmetricIntPlus
278   |apply associative_plus
279   |intros.apply sym_eq.apply plus_n_O
280   ]
281 qed.
282
283 (* monotonicity *)
284 theorem le_sigma_p: 
285 \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.
286 (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to 
287 sigma_p n p g1 \le sigma_p n p g2.
288 intros.
289 elim n in H ⊢ %
290   [apply le_n.
291   |apply (bool_elim ? (p n1));intros
292     [rewrite > true_to_sigma_p_Sn
293       [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
294         [apply le_plus
295           [apply H1[apply le_n|assumption]
296           |apply H.
297            intros.
298            apply H1[apply le_S.assumption|assumption]
299           ]
300         |assumption
301         ]
302       |assumption
303       ]
304     |rewrite > false_to_sigma_p_Sn
305       [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
306         [apply H.
307          intros.
308          apply H1[apply le_S.assumption|assumption]
309         |assumption
310         ]
311       |assumption
312       ]
313     ]
314   ]
315 qed.
316
317 (* a slightly more general result *)
318 theorem le_sigma_p1: 
319 \forall n:nat. \forall p1,p2:nat \to bool. \forall g1,g2:nat \to nat.
320 (\forall i. i < n \to 
321 bool_to_nat (p1 i)*(g1 i) \le bool_to_nat (p2 i)*g2 i) \to 
322 sigma_p n p1 g1 \le sigma_p n p2 g2.
323 intros.
324 elim n in H ⊢ %
325   [apply le_n.
326   |apply (bool_elim ? (p1 n1));intros
327     [apply (bool_elim ? (p2 n1));intros
328       [rewrite > true_to_sigma_p_Sn
329         [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
330           [apply le_plus
331             [lapply (H1 n1) as H5
332               [rewrite > H2 in H5.
333                rewrite > H3 in H5.
334                simplify in H5.
335                rewrite < plus_n_O in H5.
336                rewrite < plus_n_O in H5.
337                assumption
338               |apply le_S_S.apply le_n
339               ]
340             |apply H.intros.
341              apply H1.apply le_S.assumption
342             ]
343           |assumption
344           ]
345         |assumption
346         ]
347       |rewrite > true_to_sigma_p_Sn
348         [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
349           [change in ⊢ (? ? %) with (O + sigma_p n1 p2 g2).
350            apply le_plus
351             [lapply (H1 n1) as H5
352               [rewrite > H2 in H5.
353                rewrite > H3 in H5.
354                simplify in H5.
355                rewrite < plus_n_O in H5.
356                assumption
357               |apply le_S_S.apply le_n
358               ]
359             |apply H.intros.
360              apply H1.apply le_S.assumption
361             ]
362           |assumption
363           ]
364         |assumption
365         ]
366       ]
367     |apply (bool_elim ? (p2 n1));intros
368       [rewrite > false_to_sigma_p_Sn
369         [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
370           [change in ⊢ (? % ?) with (O + sigma_p n1 p1 g1).
371            apply le_plus
372             [lapply (H1 n1) as H5
373               [rewrite > H2 in H5.
374                rewrite > H3 in H5.
375                simplify in H5.
376                rewrite < plus_n_O in H5.
377                assumption
378               |apply le_S_S.apply le_n
379               ]
380             |apply H.intros.
381              apply H1.apply le_S.assumption
382             ]
383           |assumption
384           ]
385         |assumption
386         ]
387       |rewrite > false_to_sigma_p_Sn
388         [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
389           [apply H.intros.
390            apply H1.apply le_S.assumption
391           |assumption
392           ]
393         |assumption
394         ]
395       ]
396     ]
397   ]
398 qed.
399
400 theorem lt_sigma_p: 
401 \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.
402 (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to
403 (\exists i. i < n \and (p i = true) \and (g1 i < g2 i)) \to
404 sigma_p n p g1 < sigma_p n p g2.
405 intros 4.
406 elim n
407   [elim H1.clear H1.
408    elim H2.clear H2.
409    elim H1.clear H1.
410    apply False_ind.
411    apply (lt_to_not_le ? ? H2).
412    apply le_O_n
413   |apply (bool_elim ? (p n1));intros
414     [apply (bool_elim ? (leb (S (g1 n1)) (g2 n1)));intros
415       [rewrite > true_to_sigma_p_Sn
416         [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
417           [change with 
418            (S (g1 n1)+sigma_p n1 p g1 \le g2 n1+sigma_p n1 p g2).
419            apply le_plus
420             [apply leb_true_to_le.assumption
421             |apply le_sigma_p.intros.
422              apply H1
423               [apply lt_to_le.apply le_S_S.assumption
424               |assumption
425               ]
426             ]
427           |assumption
428           ]
429         |assumption
430         ]
431       |rewrite > true_to_sigma_p_Sn
432         [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
433           [unfold lt.
434            rewrite > plus_n_Sm.
435            apply le_plus
436             [apply H1
437               [apply le_n
438               |assumption
439               ]
440             |apply H
441               [intros.apply H1
442                 [apply lt_to_le.apply le_S_S.assumption
443                 |assumption
444                 ]
445               |elim H2.clear H2.
446                elim H5.clear H5.
447                elim H2.clear H2.
448                apply (ex_intro ? ? a).
449                split
450                 [split
451                   [elim (le_to_or_lt_eq a n1)
452                     [assumption
453                     |absurd (g1 a < g2 a)
454                       [assumption
455                       |apply leb_false_to_not_le.
456                        rewrite > H2.
457                        assumption
458                       ]
459                     |apply le_S_S_to_le.
460                      assumption
461                     ]
462                   |assumption
463                   ]
464                 |assumption
465                 ]
466               ]
467             ]
468           |assumption
469           ]
470         |assumption
471         ]
472       ]
473     |rewrite > false_to_sigma_p_Sn
474       [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
475         [apply H
476           [intros.apply H1
477             [apply lt_to_le.apply le_S_S.assumption
478             |assumption
479             ]
480           |elim H2.clear H2.
481            elim H4.clear H4.
482            elim H2.clear H2.
483            apply (ex_intro ? ? a).
484            split
485             [split
486               [elim (le_to_or_lt_eq a n1)
487                 [assumption
488                 |apply False_ind.
489                  apply not_eq_true_false.
490                  rewrite < H6.
491                  rewrite < H3.
492                  rewrite < H2. 
493                  reflexivity
494                 |apply le_S_S_to_le.
495                  assumption
496                 ]
497               |assumption
498               ]
499             |assumption
500             ]
501           ]
502         |assumption
503         ]
504       |assumption
505       ]
506     ]
507   ]
508 qed.
509           
510 theorem sigma_p_divides: 
511 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to 
512 \forall g: nat \to nat.
513 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
514 sigma_p (S n) (\lambda x.divides_b x n)
515   (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
516 intros.
517 unfold sigma_p.
518 apply (iter_p_gen_divides nat O plus n m p ? ? ? g)
519 [ assumption
520 | assumption
521 | assumption
522 | apply symmetricIntPlus
523 | apply associative_plus
524 | intros.
525   apply sym_eq.
526   apply plus_n_O
527 ]
528 qed.
529
530 theorem distributive_times_plus_sigma_p: \forall n,k:nat. \forall p:nat \to bool. \forall g:nat \to nat.
531 k*(sigma_p n p g) = sigma_p n p (\lambda i:nat.k * (g i)).
532 intros.
533 apply (distributive_times_plus_iter_p_gen nat plus O times n k p g)
534 [ apply symmetricIntPlus
535 | apply associative_plus
536 | intros.
537   apply sym_eq.
538   apply plus_n_O
539 | apply symmetric_times
540 | apply distributive_times_plus
541 | intros.
542   rewrite < (times_n_O a).
543   reflexivity
544 ]
545 qed.
546
547 (*some properties of sigma_p invoked with an "always true" predicate (in this 
548   way sigma_p just counts the elements, without doing any control) or with
549   the nat \to nat function which always returns (S O).
550   It 's not easily possible proving these theorems in a general form 
551   in generic_sigma_p.ma
552  *)
553
554 theorem sigma_p_true: \forall n:nat.
555 (sigma_p n (\lambda x.true) (\lambda x.S O)) = n.
556 intros.
557 elim n
558 [ simplify.
559   reflexivity
560 | rewrite > (true_to_sigma_p_Sn n1 (\lambda x:nat.true) (\lambda x:nat.S O))
561   [ rewrite > H.
562     simplify.
563     reflexivity
564   | reflexivity 
565   ]
566 ]
567 qed.
568
569 theorem sigma_P_SO_to_sigma_p_true: \forall n:nat. \forall g:nat \to bool.
570 sigma_p n g (\lambda n:nat. (S O)) = 
571 sigma_p n (\lambda x:nat.true) (\lambda i:nat.bool_to_nat (g i)).
572 intros.
573 elim n
574 [ simplify.
575   reflexivity
576 | cut ((g n1) = true \lor (g n1) = false)
577   [ rewrite > true_to_sigma_p_Sn in \vdash (? ? ? %)
578     [ elim Hcut
579       [ rewrite > H1.
580         rewrite > true_to_sigma_p_Sn in \vdash (? ? % ?)
581         [ simplify.
582           apply eq_f.
583           assumption
584         | assumption
585         ]
586       | rewrite > H1.
587         rewrite > false_to_sigma_p_Sn in \vdash (? ? % ?)
588         [ simplify.
589           assumption
590         | assumption
591         ]
592       ]
593     | reflexivity
594     ]
595   | elim (g n1)
596     [ left.
597       reflexivity
598     | right.
599       reflexivity
600     ]
601   ]
602 ]
603 qed.
604
605 (* I introduce an equivalence in the form map_iter_i in order to use
606  * the existing result about permutation in that part of the library.
607  *) 
608  
609 theorem eq_map_iter_i_sigma_p_alwaysTrue:  \forall n:nat.\forall g:nat \to nat. 
610 map_iter_i n g plus O = sigma_p (S n) (\lambda c:nat.true) g.
611 intros.
612 elim n
613 [ simplify.
614   rewrite < plus_n_O.
615   reflexivity
616 | rewrite > true_to_sigma_p_Sn
617   [ simplify in \vdash (? ? % ?).
618     rewrite < plus_n_O.
619     apply eq_f.
620     assumption
621   | reflexivity
622   ]
623 ]
624 qed.
625
626 theorem sigma_p_plus_1: \forall n:nat. \forall f,g:nat \to nat.
627 \forall p.
628 sigma_p n p (\lambda a:nat.(f a) + (g a)) = 
629 sigma_p n p f + sigma_p n p g.
630 intros.
631 elim n
632 [ simplify.
633   reflexivity
634 | apply (bool_elim ? (p n1)); intro;
635   [ rewrite > true_to_sigma_p_Sn
636     [ rewrite > (true_to_sigma_p_Sn n1 p f)
637       [ rewrite > (true_to_sigma_p_Sn n1 p g)
638         [ rewrite > assoc_plus in \vdash (? ? ? %).
639           rewrite < assoc_plus in \vdash (? ? ? (? ? %)).
640           rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))).
641           rewrite > assoc_plus in \vdash (? ? ? (? ? %)).
642           rewrite < assoc_plus in \vdash (? ? ? %).
643           apply eq_f.
644           assumption]]]
645    assumption
646  | rewrite > false_to_sigma_p_Sn
647     [ rewrite > (false_to_sigma_p_Sn n1 p f)
648       [ rewrite > (false_to_sigma_p_Sn n1 p g)
649         [assumption]]]
650    assumption
651 ]]
652 qed.
653
654 theorem eq_sigma_p_sigma_p_times1 : \forall n,m:nat.\forall f:nat \to nat.
655 sigma_p (n*m) (\lambda x:nat.true) f =
656 sigma_p m (\lambda x:nat.true) 
657     (\lambda a.(sigma_p n (\lambda x:nat.true) (\lambda b.f (b*m + a)))).
658 intro.
659 elim n
660 [ simplify.
661   elim m
662   [ simplify.
663     reflexivity
664   | rewrite > true_to_sigma_p_Sn
665     [ rewrite < H.
666       reflexivity
667     | reflexivity
668     ]
669   ]
670 | change in \vdash (? ? ? (? ? ? (\lambda a:?.%))) with ((f ((n1*m)+a)) + 
671   (sigma_p n1 (\lambda x:nat.true) (\lambda b:nat.f (b*m +a)))).
672   rewrite > sigma_p_plus_1 in \vdash (? ? ? %).
673   rewrite > (sym_times (S n1) m).
674   rewrite < (times_n_Sm m  n1).
675   rewrite > sigma_p_plus in \vdash (? ? % ?).
676   apply eq_f2
677   [ rewrite < (sym_times m n1).
678     apply eq_sigma_p
679     [ intros. 
680       reflexivity
681     | intros.
682       rewrite < (sym_plus ? (m * n1)).
683       reflexivity
684     ]
685   | rewrite > (sym_times m n1).
686     apply H
687   ]
688 ]
689 qed.
690
691 theorem eq_sigma_p_sigma_p_times2 : \forall n,m:nat.\forall f:nat \to nat.
692 sigma_p (n *m) (\lambda c:nat.true) f =
693 sigma_p  n (\lambda c:nat.true) 
694   (\lambda a.(sigma_p m (\lambda c:nat.true) (\lambda b:nat.f (b* n + a)))).
695 intros.
696 rewrite > sym_times.
697 apply eq_sigma_p_sigma_p_times1.
698 qed.
699
700 theorem sigma_p_times:\forall n,m:nat. 
701 \forall f,f1,f2:nat \to bool.
702 \forall g:nat \to nat \to nat. 
703 \forall g1,g2: nat \to nat.
704 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g b a) < (S n)*(S m)) \to
705 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g1 (g b a)) = a) \to
706 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g2 (g b a)) = b) \to
707 (\forall a,b:nat. a < (S n) \to b < (S m) \to f (g b a) = andb (f2 b) (f1 a)) \to
708 (sigma_p ((S n) * (S m)) f (\lambda c:nat.(S O))) = 
709 sigma_p (S n) f1 (\lambda c:nat.(S O)) * sigma_p (S m) f2 (\lambda c:nat.(S O)). 
710 intros.
711
712 rewrite > (sigma_P_SO_to_sigma_p_true ).
713 rewrite > (S_pred ((S n)*(S m))) in \vdash (? ? (? % ? ?) ?)
714 [ rewrite < (eq_map_iter_i_sigma_p_alwaysTrue (pred ((S n)* (S m)))).
715   rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ? 
716            (\lambda i.g (div i (S n)) (mod i (S n))))
717   [ rewrite > eq_map_iter_i_sigma_p_alwaysTrue.
718     rewrite < S_pred
719     [ rewrite > eq_sigma_p_sigma_p_times2.
720       apply (trans_eq ? ? (sigma_p (S n)  (\lambda c:nat.true) 
721         (\lambda a. sigma_p (S m) (\lambda c:nat.true) 
722                 (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))))))
723       [ apply eq_sigma_p;intros
724         [ reflexivity
725         | apply eq_sigma_p;intros
726           [ reflexivity
727           | 
728             rewrite > (div_mod_spec_to_eq (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n)) 
729                                                   ((x1*(S n) + x) \mod (S n)) x1 x)
730             [ rewrite > (div_mod_spec_to_eq2 (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n)) 
731                                                   ((x1*(S n) + x) \mod (S n)) x1 x)
732               [ rewrite > H3
733                 [ apply bool_to_nat_andb
734                 | assumption
735                 | assumption
736                 ]
737               | apply div_mod_spec_div_mod.
738                 apply lt_O_S
739               | constructor 1
740                 [ assumption
741                 | reflexivity
742                 ]
743               ]
744             | apply div_mod_spec_div_mod.
745               apply lt_O_S
746             | constructor 1
747               [ assumption
748               | reflexivity
749               ]
750             ]
751           ]
752         ]
753       | apply (trans_eq ? ? 
754          (sigma_p (S n) (\lambda c:nat.true) (\lambda n.((bool_to_nat (f1 n)) *
755          (sigma_p (S m) (\lambda c:nat.true) (\lambda n.bool_to_nat (f2 n)))))))
756         [ apply eq_sigma_p;intros
757           [ reflexivity
758           | rewrite > distributive_times_plus_sigma_p.
759             apply eq_sigma_p;intros
760             [ reflexivity
761             | rewrite > sym_times. 
762               reflexivity
763             ]
764           ]
765         | apply sym_eq.
766           rewrite > sigma_P_SO_to_sigma_p_true.
767           rewrite > sigma_P_SO_to_sigma_p_true in \vdash (? ? (? ? %) ?).
768           rewrite > sym_times. 
769           rewrite > distributive_times_plus_sigma_p.
770           apply eq_sigma_p;intros
771           [ reflexivity
772           | rewrite > distributive_times_plus_sigma_p.
773             rewrite < sym_times.
774             rewrite > distributive_times_plus_sigma_p.
775             apply eq_sigma_p;
776               intros; reflexivity            
777           ]
778         ]
779       ]
780     | apply lt_O_times_S_S
781     ]
782     
783   | unfold permut.
784     split
785     [ intros.
786       rewrite < plus_n_O.
787       apply le_S_S_to_le.
788       rewrite < S_pred in \vdash (? ? %)
789       [ change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
790         apply H
791         [ apply lt_mod_m_m.
792           unfold lt. 
793           apply le_S_S.
794           apply le_O_n 
795         | apply (lt_times_to_lt_l n).
796           apply (le_to_lt_to_lt ? i)
797           [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
798             [ rewrite > sym_plus.
799               apply le_plus_n
800             | unfold lt. 
801               apply le_S_S.
802               apply le_O_n
803             ]
804           | unfold lt.
805             rewrite > S_pred in \vdash (? ? %)
806             [ apply le_S_S.
807               rewrite > plus_n_O in \vdash (? ? %).
808               rewrite > sym_times. 
809               assumption
810             | apply lt_O_times_S_S
811             ]
812           ]
813         ]
814       | apply lt_O_times_S_S
815       ]
816     | rewrite < plus_n_O.
817       unfold injn.
818       intros.
819       cut (i < (S n)*(S m))
820       [ cut (j < (S n)*(S m))
821         [ cut ((i \mod (S n)) < (S n))
822           [ cut ((i/(S n)) < (S m))
823             [ cut ((j \mod (S n)) < (S n))
824               [ cut ((j/(S n)) < (S m))
825                 [ rewrite > (div_mod i (S n))
826                   [ rewrite > (div_mod j (S n))
827                     [ rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
828                       rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
829                       rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
830                       rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
831                       rewrite > H6.
832                       reflexivity
833                     | unfold lt.
834                       apply le_S_S.
835                       apply le_O_n
836                     ]
837                   | unfold lt. 
838                     apply le_S_S.
839                     apply le_O_n
840                   ]
841                 | apply (lt_times_to_lt_l n).
842                   apply (le_to_lt_to_lt ? j)
843                   [ rewrite > (div_mod j (S n)) in \vdash (? ? %)
844                     [ rewrite > sym_plus.
845                       apply le_plus_n
846                     | unfold lt. apply le_S_S.
847                       apply le_O_n
848                     ]
849                   | rewrite < sym_times. 
850                     assumption                    
851                   ]
852                 ]
853               | apply lt_mod_m_m.
854                 unfold lt. 
855                 apply le_S_S.
856                 apply le_O_n
857               ]
858             | apply (lt_times_to_lt_l n).
859               apply (le_to_lt_to_lt ? i)
860               [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
861                 [ rewrite > sym_plus.
862                   apply le_plus_n
863                 | unfold lt. 
864                   apply le_S_S.
865                   apply le_O_n
866                 ]
867               | rewrite < sym_times. 
868                 assumption
869               ]
870             ]
871           | apply lt_mod_m_m.
872             unfold lt. 
873             apply le_S_S.
874             apply le_O_n
875           ]
876         | unfold lt.
877           rewrite > S_pred in \vdash (? ? %)
878           [ apply le_S_S.
879             assumption
880           | apply lt_O_times_S_S 
881           ]
882         ]
883       | unfold lt.
884         rewrite > S_pred in \vdash (? ? %)
885         [ apply le_S_S.
886           assumption
887         | apply lt_O_times_S_S 
888         ]
889       ]
890     ]
891   | intros.
892     apply False_ind.
893     apply (not_le_Sn_O m1 H4)
894   ]
895 | apply lt_O_times_S_S
896 ]
897 qed.
898
899 theorem sigma_p_knm: 
900 \forall g: nat \to nat.
901 \forall h2:nat \to nat \to nat.
902 \forall h11,h12:nat \to nat. 
903 \forall k,n,m.
904 \forall p1,p21:nat \to bool.
905 \forall p22:nat \to nat \to bool.
906 (\forall x. x < k \to p1 x = true \to 
907 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
908 \land h2 (h11 x) (h12 x) = x 
909 \land (h11 x) < n \land (h12 x) < m) \to
910 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to 
911 p1 (h2 i j) = true \land 
912 h11 (h2 i j) = i \land h12 (h2 i j) = j
913 \land h2 i j < k) \to
914 sigma_p k p1 g=
915 sigma_p n p21 (\lambda x:nat.sigma_p m (p22 x) (\lambda y. g (h2 x y))).
916 intros.
917 unfold sigma_p.
918 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
919 apply iter_p_gen_knm
920   [apply symmetricIntPlus
921   |apply associative_plus
922   |intro.rewrite < plus_n_O.reflexivity
923   |exact h11
924   |exact h12
925   |assumption
926   |assumption
927   ]
928 qed.
929   
930   
931 theorem sigma_p2_eq: 
932 \forall g: nat \to nat \to nat.
933 \forall h11,h12,h21,h22: nat \to nat \to nat. 
934 \forall n1,m1,n2,m2.
935 \forall p11,p21:nat \to bool.
936 \forall p12,p22:nat \to nat \to bool.
937 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to 
938 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
939 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
940 \land h11 i j < n1 \land h12 i j < m1) \to
941 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to 
942 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
943 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
944 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
945 sigma_p n1 p11 (\lambda x:nat .sigma_p m1 (p12 x) (\lambda y. g x y)) =
946 sigma_p n2 p21 (\lambda x:nat .sigma_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
947 intros.
948 unfold sigma_p.
949 unfold sigma_p in \vdash (? ? (? ? ? ? (\lambda x:?.%) ? ?) ?).
950 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
951
952 apply(iter_p_gen_2_eq nat O plus ? ? ? g h11 h12 h21 h22 n1 m1 n2 m2 p11 p21 p12 p22)
953 [ apply symmetricIntPlus
954 | apply associative_plus
955 | intro.
956   rewrite < (plus_n_O).
957   reflexivity
958 | assumption
959 | assumption
960 ]
961 qed.
962
963 theorem sigma_p_sigma_p: 
964 \forall g: nat \to nat \to nat.
965 \forall n,m.
966 \forall p11,p21:nat \to bool.
967 \forall p12,p22:nat \to nat \to bool.
968 (\forall x,y. x < n \to y < m \to 
969  (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
970 sigma_p n p11 (\lambda x:nat.sigma_p m (p12 x) (\lambda y. g x y)) =
971 sigma_p m p21 (\lambda y:nat.sigma_p n (p22 y) (\lambda x. g x y)).
972 intros.
973 unfold sigma_p.unfold sigma_p.
974 apply (iter_p_gen_iter_p_gen ? ? ? sym_plus assoc_plus)
975   [intros.apply sym_eq.apply plus_n_O.
976   |assumption
977   ]
978 qed.