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);
110 theorem or_false_to_eq_sigma_p:
111 \forall n,m:nat.\forall p:nat \to bool.
112 \forall g: nat \to nat.
113 n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = O)
114 \to sigma_p m p g = sigma_p n p g.
117 apply or_false_eq_baseA_to_eq_iter_p_gen
124 theorem bool_to_nat_to_eq_sigma_p:
125 \forall n:nat.\forall p1,p2:nat \to bool.
126 \forall g1,g2: nat \to nat.
128 bool_to_nat (p1 i)*(g1 i) = bool_to_nat (p2 i)*(g2 i))
129 \to sigma_p n p1 g1 = sigma_p n p2 g2.
132 |generalize in match (H n1).
133 apply (bool_elim ? (p1 n1));intro
134 [apply (bool_elim ? (p2 n1));intros
135 [rewrite > true_to_sigma_p_Sn
136 [rewrite > true_to_sigma_p_Sn
140 rewrite > plus_n_O in ⊢ (? ? ? %).
148 |rewrite > true_to_sigma_p_Sn
149 [rewrite > false_to_sigma_p_Sn
150 [change in ⊢ (? ? ? %) with (O + sigma_p n1 p2 g2).
162 |apply (bool_elim ? (p2 n1));intros
163 [rewrite > false_to_sigma_p_Sn
164 [rewrite > true_to_sigma_p_Sn
165 [change in ⊢ (? ? % ?) with (O + sigma_p n1 p1 g1).
168 rewrite < plus_n_O in H4.
176 |rewrite > false_to_sigma_p_Sn
177 [rewrite > false_to_sigma_p_Sn
190 \forall p1,p2:nat \to bool.
191 \forall g: nat \to nat \to nat.
193 (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
194 (\lambda x.g (div x m) (mod x m)) =
196 (\lambda x.sigma_p m p2 (g x)).
199 apply (iter_p_gen2 n m p1 p2 nat g O plus)
200 [ apply symmetricIntPlus
201 | apply associative_plus
210 \forall p1:nat \to bool.
211 \forall p2:nat \to nat \to bool.
212 \forall g: nat \to nat \to nat.
214 (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x m)))
215 (\lambda x.g (div x m) (mod x m)) =
217 (\lambda x.sigma_p m (p2 x) (g x)).
220 apply (iter_p_gen2' n m p1 p2 nat g O plus)
221 [ apply symmetricIntPlus
222 | apply associative_plus
229 lemma sigma_p_gi: \forall g: nat \to nat.
230 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
231 sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
234 apply (iter_p_gen_gi)
235 [ apply symmetricIntPlus
236 | apply associative_plus
245 theorem eq_sigma_p_gh:
246 \forall g,h,h1: nat \to nat.\forall n,n1.
247 \forall p1,p2:nat \to bool.
248 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
249 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
250 (\forall i. i < n \to p1 i = true \to h i < n1) \to
251 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
252 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
253 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
254 sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 p2 g.
257 apply (eq_iter_p_gen_gh nat O plus ? ? ? g h h1 n n1 p1 p2)
258 [ apply symmetricIntPlus
259 | apply associative_plus
272 theorem eq_sigma_p_pred:
273 \forall n,p,g. p O = true \to
274 sigma_p (S n) (\lambda i.p (pred i)) (\lambda i.g(pred i)) =
275 plus (sigma_p n p g) (g O).
278 apply eq_iter_p_gen_pred
280 |apply symmetricIntPlus
281 |apply associative_plus
282 |intros.apply sym_eq.apply plus_n_O
288 \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.
289 (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to
290 sigma_p n p g1 \le sigma_p n p g2.
292 generalize in match H.
295 |apply (bool_elim ? (p n1));intros
296 [rewrite > true_to_sigma_p_Sn
297 [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
299 [apply H2[apply le_n|assumption]
302 apply H2[apply le_S.assumption|assumption]
308 |rewrite > false_to_sigma_p_Sn
309 [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
312 apply H2[apply le_S.assumption|assumption]
321 (* a slightly more general result *)
323 \forall n:nat. \forall p1,p2:nat \to bool. \forall g1,g2:nat \to nat.
324 (\forall i. i < n \to
325 bool_to_nat (p1 i)*(g1 i) \le bool_to_nat (p2 i)*g2 i) \to
326 sigma_p n p1 g1 \le sigma_p n p2 g2.
328 generalize in match H.
331 |apply (bool_elim ? (p1 n1));intros
332 [apply (bool_elim ? (p2 n1));intros
333 [rewrite > true_to_sigma_p_Sn
334 [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
336 [lapply (H2 n1) as H5
340 rewrite < plus_n_O in H5.
341 rewrite < plus_n_O in H5.
343 |apply le_S_S.apply le_n
346 apply H2.apply le_S.assumption
352 |rewrite > true_to_sigma_p_Sn
353 [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
354 [change in ⊢ (? ? %) with (O + sigma_p n1 p2 g2).
356 [lapply (H2 n1) as H5
360 rewrite < plus_n_O in H5.
362 |apply le_S_S.apply le_n
365 apply H2.apply le_S.assumption
372 |apply (bool_elim ? (p2 n1));intros
373 [rewrite > false_to_sigma_p_Sn
374 [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
375 [change in ⊢ (? % ?) with (O + sigma_p n1 p1 g1).
377 [lapply (H2 n1) as H5
381 rewrite < plus_n_O in H5.
383 |apply le_S_S.apply le_n
386 apply H2.apply le_S.assumption
392 |rewrite > false_to_sigma_p_Sn
393 [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
395 apply H2.apply le_S.assumption
406 \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.
407 (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to
408 (\exists i. i < n \and (p i = true) \and (g1 i < g2 i)) \to
409 sigma_p n p g1 < sigma_p n p g2.
416 apply (lt_to_not_le ? ? H2).
418 |apply (bool_elim ? (p n1));intros
419 [apply (bool_elim ? (leb (S (g1 n1)) (g2 n1)));intros
420 [rewrite > true_to_sigma_p_Sn
421 [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
423 (S (g1 n1)+sigma_p n1 p g1 \le g2 n1+sigma_p n1 p g2).
425 [apply leb_true_to_le.assumption
426 |apply le_sigma_p.intros.
428 [apply lt_to_le.apply le_S_S.assumption
436 |rewrite > true_to_sigma_p_Sn
437 [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
447 [apply lt_to_le.apply le_S_S.assumption
453 apply (ex_intro ? ? a).
456 [elim (le_to_or_lt_eq a n1)
458 |absurd (g1 a < g2 a)
460 |apply leb_false_to_not_le.
478 |rewrite > false_to_sigma_p_Sn
479 [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
482 [apply lt_to_le.apply le_S_S.assumption
488 apply (ex_intro ? ? a).
491 [elim (le_to_or_lt_eq a n1)
494 apply not_eq_true_false.
515 theorem sigma_p_divides:
516 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
517 \forall g: nat \to nat.
518 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
519 sigma_p (S n) (\lambda x.divides_b x n)
520 (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
523 apply (iter_p_gen_divides nat O plus n m p ? ? ? g)
527 | apply symmetricIntPlus
528 | apply associative_plus
535 theorem distributive_times_plus_sigma_p: \forall n,k:nat. \forall p:nat \to bool. \forall g:nat \to nat.
536 k*(sigma_p n p g) = sigma_p n p (\lambda i:nat.k * (g i)).
538 apply (distributive_times_plus_iter_p_gen nat plus O times n k p g)
539 [ apply symmetricIntPlus
540 | apply associative_plus
544 | apply symmetric_times
545 | apply distributive_times_plus
547 rewrite < (times_n_O a).
552 (*some properties of sigma_p invoked with an "always true" predicate (in this
553 way sigma_p just counts the elements, without doing any control) or with
554 the nat \to nat function which always returns (S O).
555 It 's not easily possible proving these theorems in a general form
556 in generic_sigma_p.ma
559 theorem sigma_p_true: \forall n:nat.
560 (sigma_p n (\lambda x.true) (\lambda x.S O)) = n.
565 | rewrite > (true_to_sigma_p_Sn n1 (\lambda x:nat.true) (\lambda x:nat.S O))
574 theorem sigma_P_SO_to_sigma_p_true: \forall n:nat. \forall g:nat \to bool.
575 sigma_p n g (\lambda n:nat. (S O)) =
576 sigma_p n (\lambda x:nat.true) (\lambda i:nat.bool_to_nat (g i)).
581 | cut ((g n1) = true \lor (g n1) = false)
582 [ rewrite > true_to_sigma_p_Sn in \vdash (? ? ? %)
585 rewrite > true_to_sigma_p_Sn in \vdash (? ? % ?)
592 rewrite > false_to_sigma_p_Sn in \vdash (? ? % ?)
610 (* I introduce an equivalence in the form map_iter_i in order to use
611 * the existing result about permutation in that part of the library.
614 theorem eq_map_iter_i_sigma_p_alwaysTrue: \forall n:nat.\forall g:nat \to nat.
615 map_iter_i n g plus O = sigma_p (S n) (\lambda c:nat.true) g.
621 | rewrite > true_to_sigma_p_Sn
622 [ simplify in \vdash (? ? % ?).
631 theorem sigma_p_plus_1: \forall n:nat. \forall f,g:nat \to nat.
633 sigma_p n p (\lambda a:nat.(f a) + (g a)) =
634 sigma_p n p f + sigma_p n p g.
639 | apply (bool_elim ? (p n1)); intro;
640 [ rewrite > true_to_sigma_p_Sn
641 [ rewrite > (true_to_sigma_p_Sn n1 p f)
642 [ rewrite > (true_to_sigma_p_Sn n1 p g)
643 [ rewrite > assoc_plus in \vdash (? ? ? %).
644 rewrite < assoc_plus in \vdash (? ? ? (? ? %)).
645 rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))).
646 rewrite > assoc_plus in \vdash (? ? ? (? ? %)).
647 rewrite < assoc_plus in \vdash (? ? ? %).
651 | rewrite > false_to_sigma_p_Sn
652 [ rewrite > (false_to_sigma_p_Sn n1 p f)
653 [ rewrite > (false_to_sigma_p_Sn n1 p g)
659 theorem eq_sigma_p_sigma_p_times1 : \forall n,m:nat.\forall f:nat \to nat.
660 sigma_p (n*m) (\lambda x:nat.true) f =
661 sigma_p m (\lambda x:nat.true)
662 (\lambda a.(sigma_p n (\lambda x:nat.true) (\lambda b.f (b*m + a)))).
669 | rewrite > true_to_sigma_p_Sn
675 | change in \vdash (? ? ? (? ? ? (\lambda a:?.%))) with ((f ((n1*m)+a)) +
676 (sigma_p n1 (\lambda x:nat.true) (\lambda b:nat.f (b*m +a)))).
677 rewrite > sigma_p_plus_1 in \vdash (? ? ? %).
678 rewrite > (sym_times (S n1) m).
679 rewrite < (times_n_Sm m n1).
680 rewrite > sigma_p_plus in \vdash (? ? % ?).
682 [ rewrite < (sym_times m n1).
687 rewrite < (sym_plus ? (m * n1)).
690 | rewrite > (sym_times m n1).
696 theorem eq_sigma_p_sigma_p_times2 : \forall n,m:nat.\forall f:nat \to nat.
697 sigma_p (n *m) (\lambda c:nat.true) f =
698 sigma_p n (\lambda c:nat.true)
699 (\lambda a.(sigma_p m (\lambda c:nat.true) (\lambda b:nat.f (b* n + a)))).
702 apply eq_sigma_p_sigma_p_times1.
705 theorem sigma_p_times:\forall n,m:nat.
706 \forall f,f1,f2:nat \to bool.
707 \forall g:nat \to nat \to nat.
708 \forall g1,g2: nat \to nat.
709 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g b a) < (S n)*(S m)) \to
710 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g1 (g b a)) = a) \to
711 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g2 (g b a)) = b) \to
712 (\forall a,b:nat. a < (S n) \to b < (S m) \to f (g b a) = andb (f2 b) (f1 a)) \to
713 (sigma_p ((S n) * (S m)) f (\lambda c:nat.(S O))) =
714 sigma_p (S n) f1 (\lambda c:nat.(S O)) * sigma_p (S m) f2 (\lambda c:nat.(S O)).
717 rewrite > (sigma_P_SO_to_sigma_p_true ).
718 rewrite > (S_pred ((S n)*(S m))) in \vdash (? ? (? % ? ?) ?)
719 [ rewrite < (eq_map_iter_i_sigma_p_alwaysTrue (pred ((S n)* (S m)))).
720 rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ?
721 (\lambda i.g (div i (S n)) (mod i (S n))))
722 [ rewrite > eq_map_iter_i_sigma_p_alwaysTrue.
724 [ rewrite > eq_sigma_p_sigma_p_times2.
725 apply (trans_eq ? ? (sigma_p (S n) (\lambda c:nat.true)
726 (\lambda a. sigma_p (S m) (\lambda c:nat.true)
727 (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))))))
728 [ apply eq_sigma_p;intros
730 | apply eq_sigma_p;intros
733 rewrite > (div_mod_spec_to_eq (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
734 ((x1*(S n) + x) \mod (S n)) x1 x)
735 [ rewrite > (div_mod_spec_to_eq2 (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
736 ((x1*(S n) + x) \mod (S n)) x1 x)
738 [ apply bool_to_nat_andb
742 | apply div_mod_spec_div_mod.
749 | apply div_mod_spec_div_mod.
758 | apply (trans_eq ? ?
759 (sigma_p (S n) (\lambda c:nat.true) (\lambda n.((bool_to_nat (f1 n)) *
760 (sigma_p (S m) (\lambda c:nat.true) (\lambda n.bool_to_nat (f2 n)))))))
761 [ apply eq_sigma_p;intros
763 | rewrite > distributive_times_plus_sigma_p.
764 apply eq_sigma_p;intros
766 | rewrite > sym_times.
771 rewrite > sigma_P_SO_to_sigma_p_true.
772 rewrite > sigma_P_SO_to_sigma_p_true in \vdash (? ? (? ? %) ?).
774 rewrite > distributive_times_plus_sigma_p.
775 apply eq_sigma_p;intros
777 | rewrite > distributive_times_plus_sigma_p.
779 rewrite > distributive_times_plus_sigma_p.
785 | apply lt_O_times_S_S
793 rewrite < S_pred in \vdash (? ? %)
794 [ change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
800 | apply (lt_times_to_lt_l n).
801 apply (le_to_lt_to_lt ? i)
802 [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
803 [ rewrite > sym_plus.
810 rewrite > S_pred in \vdash (? ? %)
812 rewrite > plus_n_O in \vdash (? ? %).
815 | apply lt_O_times_S_S
819 | apply lt_O_times_S_S
821 | rewrite < plus_n_O.
824 cut (i < (S n)*(S m))
825 [ cut (j < (S n)*(S m))
826 [ cut ((i \mod (S n)) < (S n))
827 [ cut ((i/(S n)) < (S m))
828 [ cut ((j \mod (S n)) < (S n))
829 [ cut ((j/(S n)) < (S m))
830 [ rewrite > (div_mod i (S n))
831 [ rewrite > (div_mod j (S n))
832 [ rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
833 rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
834 rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
835 rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
846 | apply (lt_times_to_lt_l n).
847 apply (le_to_lt_to_lt ? j)
848 [ rewrite > (div_mod j (S n)) in \vdash (? ? %)
849 [ rewrite > sym_plus.
851 | unfold lt. apply le_S_S.
854 | rewrite < sym_times.
863 | apply (lt_times_to_lt_l n).
864 apply (le_to_lt_to_lt ? i)
865 [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
866 [ rewrite > sym_plus.
872 | rewrite < sym_times.
882 rewrite > S_pred in \vdash (? ? %)
885 | apply lt_O_times_S_S
889 rewrite > S_pred in \vdash (? ? %)
892 | apply lt_O_times_S_S
898 apply (not_le_Sn_O m1 H4)
900 | apply lt_O_times_S_S
905 \forall g: nat \to nat.
906 \forall h2:nat \to nat \to nat.
907 \forall h11,h12:nat \to nat.
909 \forall p1,p21:nat \to bool.
910 \forall p22:nat \to nat \to bool.
911 (\forall x. x < k \to p1 x = true \to
912 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
913 \land h2 (h11 x) (h12 x) = x
914 \land (h11 x) < n \land (h12 x) < m) \to
915 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
916 p1 (h2 i j) = true \land
917 h11 (h2 i j) = i \land h12 (h2 i j) = j
918 \land h2 i j < k) \to
920 sigma_p n p21 (\lambda x:nat.sigma_p m (p22 x) (\lambda y. g (h2 x y))).
923 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
925 [apply symmetricIntPlus
926 |apply associative_plus
927 |intro.rewrite < plus_n_O.reflexivity
937 \forall g: nat \to nat \to nat.
938 \forall h11,h12,h21,h22: nat \to nat \to nat.
940 \forall p11,p21:nat \to bool.
941 \forall p12,p22:nat \to nat \to bool.
942 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
943 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
944 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
945 \land h11 i j < n1 \land h12 i j < m1) \to
946 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
947 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
948 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
949 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
950 sigma_p n1 p11 (\lambda x:nat .sigma_p m1 (p12 x) (\lambda y. g x y)) =
951 sigma_p n2 p21 (\lambda x:nat .sigma_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
954 unfold sigma_p in \vdash (? ? (? ? ? ? (\lambda x:?.%) ? ?) ?).
955 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
957 apply(iter_p_gen_2_eq nat O plus ? ? ? g h11 h12 h21 h22 n1 m1 n2 m2 p11 p21 p12 p22)
958 [ apply symmetricIntPlus
959 | apply associative_plus
961 rewrite < (plus_n_O).
968 theorem sigma_p_sigma_p:
969 \forall g: nat \to nat \to nat.
971 \forall p11,p21:nat \to bool.
972 \forall p12,p22:nat \to nat \to bool.
973 (\forall x,y. x < n \to y < m \to
974 (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
975 sigma_p n p11 (\lambda x:nat.sigma_p m (p12 x) (\lambda y. g x y)) =
976 sigma_p m p21 (\lambda y:nat.sigma_p n (p22 y) (\lambda x. g x y)).
978 unfold sigma_p.unfold sigma_p.
979 apply (iter_p_gen_iter_p_gen ? ? ? sym_plus assoc_plus)
980 [intros.apply sym_eq.apply plus_n_O.