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.
632 sigma_p n (\lambda b:nat. true) (\lambda a:nat.(f a) + (g a)) =
633 sigma_p n (\lambda b:nat. true) f + sigma_p n (\lambda b:nat. true) g.
638 | rewrite > true_to_sigma_p_Sn
639 [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) f)
640 [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) g)
641 [ rewrite > assoc_plus in \vdash (? ? ? %).
642 rewrite < assoc_plus in \vdash (? ? ? (? ? %)).
643 rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))).
644 rewrite > assoc_plus in \vdash (? ? ? (? ? %)).
645 rewrite < assoc_plus in \vdash (? ? ? %).
658 theorem eq_sigma_p_sigma_p_times1 : \forall n,m:nat.\forall f:nat \to nat.
659 sigma_p (n*m) (\lambda x:nat.true) f =
660 sigma_p m (\lambda x:nat.true)
661 (\lambda a.(sigma_p n (\lambda x:nat.true) (\lambda b.f (b*m + a)))).
668 | rewrite > true_to_sigma_p_Sn
674 | change in \vdash (? ? ? (? ? ? (\lambda a:?.%))) with ((f ((n1*m)+a)) +
675 (sigma_p n1 (\lambda x:nat.true) (\lambda b:nat.f (b*m +a)))).
676 rewrite > sigma_p_plus_1 in \vdash (? ? ? %).
677 rewrite > (sym_times (S n1) m).
678 rewrite < (times_n_Sm m n1).
679 rewrite > sigma_p_plus in \vdash (? ? % ?).
681 [ rewrite < (sym_times m n1).
686 rewrite < (sym_plus ? (m * n1)).
689 | rewrite > (sym_times m n1).
695 theorem eq_sigma_p_sigma_p_times2 : \forall n,m:nat.\forall f:nat \to nat.
696 sigma_p (n *m) (\lambda c:nat.true) f =
697 sigma_p n (\lambda c:nat.true)
698 (\lambda a.(sigma_p m (\lambda c:nat.true) (\lambda b:nat.f (b* n + a)))).
701 apply eq_sigma_p_sigma_p_times1.
704 theorem sigma_p_times:\forall n,m:nat.
705 \forall f,f1,f2:nat \to bool.
706 \forall g:nat \to nat \to nat.
707 \forall g1,g2: nat \to nat.
708 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g b a) < (S n)*(S m)) \to
709 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g1 (g b a)) = a) \to
710 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g2 (g b a)) = b) \to
711 (\forall a,b:nat. a < (S n) \to b < (S m) \to f (g b a) = andb (f2 b) (f1 a)) \to
712 (sigma_p ((S n) * (S m)) f (\lambda c:nat.(S O))) =
713 sigma_p (S n) f1 (\lambda c:nat.(S O)) * sigma_p (S m) f2 (\lambda c:nat.(S O)).
716 rewrite > (sigma_P_SO_to_sigma_p_true ).
717 rewrite > (S_pred ((S n)*(S m))) in \vdash (? ? (? % ? ?) ?)
718 [ rewrite < (eq_map_iter_i_sigma_p_alwaysTrue (pred ((S n)* (S m)))).
719 rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ?
720 (\lambda i.g (div i (S n)) (mod i (S n))))
721 [ rewrite > eq_map_iter_i_sigma_p_alwaysTrue.
723 [ rewrite > eq_sigma_p_sigma_p_times2.
724 apply (trans_eq ? ? (sigma_p (S n) (\lambda c:nat.true)
725 (\lambda a. sigma_p (S m) (\lambda c:nat.true)
726 (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))))))
727 [ apply eq_sigma_p;intros
729 | apply eq_sigma_p;intros
732 rewrite > (div_mod_spec_to_eq (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
733 ((x1*(S n) + x) \mod (S n)) x1 x)
734 [ rewrite > (div_mod_spec_to_eq2 (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
735 ((x1*(S n) + x) \mod (S n)) x1 x)
737 [ apply bool_to_nat_andb
741 | apply div_mod_spec_div_mod.
748 | apply div_mod_spec_div_mod.
757 | apply (trans_eq ? ?
758 (sigma_p (S n) (\lambda c:nat.true) (\lambda n.((bool_to_nat (f1 n)) *
759 (sigma_p (S m) (\lambda c:nat.true) (\lambda n.bool_to_nat (f2 n)))))))
760 [ apply eq_sigma_p;intros
762 | rewrite > distributive_times_plus_sigma_p.
763 apply eq_sigma_p;intros
765 | rewrite > sym_times.
770 rewrite > sigma_P_SO_to_sigma_p_true.
771 rewrite > sigma_P_SO_to_sigma_p_true in \vdash (? ? (? ? %) ?).
773 rewrite > distributive_times_plus_sigma_p.
774 apply eq_sigma_p;intros
776 | rewrite > distributive_times_plus_sigma_p.
778 rewrite > distributive_times_plus_sigma_p.
784 | apply lt_O_times_S_S
792 rewrite < S_pred in \vdash (? ? %)
793 [ change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
799 | apply (lt_times_to_lt_l n).
800 apply (le_to_lt_to_lt ? i)
801 [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
802 [ rewrite > sym_plus.
809 rewrite > S_pred in \vdash (? ? %)
811 rewrite > plus_n_O in \vdash (? ? %).
814 | apply lt_O_times_S_S
818 | apply lt_O_times_S_S
820 | rewrite < plus_n_O.
823 cut (i < (S n)*(S m))
824 [ cut (j < (S n)*(S m))
825 [ cut ((i \mod (S n)) < (S n))
826 [ cut ((i/(S n)) < (S m))
827 [ cut ((j \mod (S n)) < (S n))
828 [ cut ((j/(S n)) < (S m))
829 [ rewrite > (div_mod i (S n))
830 [ rewrite > (div_mod j (S n))
831 [ rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
832 rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
833 rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
834 rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
845 | apply (lt_times_to_lt_l n).
846 apply (le_to_lt_to_lt ? j)
847 [ rewrite > (div_mod j (S n)) in \vdash (? ? %)
848 [ rewrite > sym_plus.
850 | unfold lt. apply le_S_S.
853 | rewrite < sym_times.
862 | apply (lt_times_to_lt_l n).
863 apply (le_to_lt_to_lt ? i)
864 [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
865 [ rewrite > sym_plus.
871 | rewrite < sym_times.
881 rewrite > S_pred in \vdash (? ? %)
884 | apply lt_O_times_S_S
888 rewrite > S_pred in \vdash (? ? %)
891 | apply lt_O_times_S_S
897 apply (not_le_Sn_O m1 H4)
899 | apply lt_O_times_S_S
904 \forall g: nat \to nat.
905 \forall h2:nat \to nat \to nat.
906 \forall h11,h12:nat \to nat.
908 \forall p1,p21:nat \to bool.
909 \forall p22:nat \to nat \to bool.
910 (\forall x. x < k \to p1 x = true \to
911 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
912 \land h2 (h11 x) (h12 x) = x
913 \land (h11 x) < n \land (h12 x) < m) \to
914 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
915 p1 (h2 i j) = true \land
916 h11 (h2 i j) = i \land h12 (h2 i j) = j
917 \land h2 i j < k) \to
919 sigma_p n p21 (\lambda x:nat.sigma_p m (p22 x) (\lambda y. g (h2 x y))).
922 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
924 [apply symmetricIntPlus
925 |apply associative_plus
926 |intro.rewrite < plus_n_O.reflexivity
936 \forall g: nat \to nat \to nat.
937 \forall h11,h12,h21,h22: nat \to nat \to nat.
939 \forall p11,p21:nat \to bool.
940 \forall p12,p22:nat \to nat \to bool.
941 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
942 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
943 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
944 \land h11 i j < n1 \land h12 i j < m1) \to
945 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
946 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
947 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
948 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
949 sigma_p n1 p11 (\lambda x:nat .sigma_p m1 (p12 x) (\lambda y. g x y)) =
950 sigma_p n2 p21 (\lambda x:nat .sigma_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
953 unfold sigma_p in \vdash (? ? (? ? ? ? (\lambda x:?.%) ? ?) ?).
954 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
956 apply(iter_p_gen_2_eq nat O plus ? ? ? g h11 h12 h21 h22 n1 m1 n2 m2 p11 p21 p12 p22)
957 [ apply symmetricIntPlus
958 | apply associative_plus
960 rewrite < (plus_n_O).
967 theorem sigma_p_sigma_p:
968 \forall g: nat \to nat \to nat.
970 \forall p11,p21:nat \to bool.
971 \forall p12,p22:nat \to nat \to bool.
972 (\forall x,y. x < n \to y < m \to
973 (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
974 sigma_p n p11 (\lambda x:nat.sigma_p m (p12 x) (\lambda y. g x y)) =
975 sigma_p m p21 (\lambda y:nat.sigma_p n (p22 y) (\lambda x. g x y)).
977 unfold sigma_p.unfold sigma_p.
978 apply (iter_p_gen_iter_p_gen ? ? ? sym_plus assoc_plus)
979 [intros.apply sym_eq.apply plus_n_O.