1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/generic_iter_p".
17 include "nat/primes.ma".
20 (*a generic definition of summatory indexed over natural numbers:
21 * n:N is the advanced end in the range of the sommatory
22 * p: N -> bool is a predicate. if (p i) = true, then (g i) is summed, else it isn't
23 * A is the type of the elements of the sum.
24 * g:nat -> A, is the function which associates the nth element of the sum to the nth natural numbers
25 * baseA (of type A) is the neutral element of A for plusA operation
26 * plusA: A -> A -> A is the sum over elements in A.
29 let rec iter_p_gen (n:nat) (p: nat \to bool) (A:Type) (g: nat \to A)
30 (baseA: A) (plusA: A \to A \to A) \def
35 [true \Rightarrow (plusA (g k) (iter_p_gen k p A g baseA plusA))
36 |false \Rightarrow iter_p_gen k p A g baseA plusA]
39 theorem true_to_iter_p_gen_Sn:
40 \forall n:nat. \forall p:nat \to bool. \forall A:Type. \forall g:nat \to A.
41 \forall baseA:A. \forall plusA: A \to A \to A.
42 p n = true \to iter_p_gen (S n) p A g baseA plusA =
43 (plusA (g n) (iter_p_gen n p A g baseA plusA)).
52 theorem false_to_iter_p_gen_Sn:
53 \forall n:nat. \forall p:nat \to bool. \forall A:Type. \forall g:nat \to A.
54 \forall baseA:A. \forall plusA: A \to A \to A.
55 p n = false \to iter_p_gen (S n) p A g baseA plusA = iter_p_gen n p A g baseA plusA.
63 theorem eq_iter_p_gen: \forall p1,p2:nat \to bool. \forall A:Type.
64 \forall g1,g2: nat \to A. \forall baseA: A.
65 \forall plusA: A \to A \to A. \forall n:nat.
66 (\forall x. x < n \to p1 x = p2 x) \to
67 (\forall x. x < n \to g1 x = g2 x) \to
68 iter_p_gen n p1 A g1 baseA plusA = iter_p_gen n p2 A g2 baseA plusA.
72 | apply (bool_elim ? (p1 n1))
74 rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
75 rewrite > true_to_iter_p_gen_Sn
77 [ apply H2.apply le_n.
79 [ intros.apply H1.apply le_S.assumption
80 | intros.apply H2.apply le_S.assumption
83 | rewrite < H3.apply sym_eq.apply H1.apply le_n
86 rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
87 rewrite > false_to_iter_p_gen_Sn
89 [ intros.apply H1.apply le_S.assumption
90 | intros.apply H2.apply le_S.assumption
92 | rewrite < H3.apply sym_eq.apply H1.apply le_n
98 theorem eq_iter_p_gen1: \forall p1,p2:nat \to bool. \forall A:Type.
99 \forall g1,g2: nat \to A. \forall baseA: A.
100 \forall plusA: A \to A \to A.\forall n:nat.
101 (\forall x. x < n \to p1 x = p2 x) \to
102 (\forall x. x < n \to p1 x = true \to g1 x = g2 x) \to
103 iter_p_gen n p1 A g1 baseA plusA = iter_p_gen n p2 A g2 baseA plusA.
107 | apply (bool_elim ? (p1 n1))
109 rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
110 rewrite > true_to_iter_p_gen_Sn
117 [ intros.apply H1.apply le_S.assumption
119 [ apply le_S.assumption
125 apply sym_eq.apply H1.apply le_n
128 rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
129 rewrite > false_to_iter_p_gen_Sn
131 [ intros.apply H1.apply le_S.assumption
133 [ apply le_S.assumption
137 | rewrite < H3.apply sym_eq.
144 theorem iter_p_gen_false: \forall A:Type. \forall g: nat \to A. \forall baseA:A.
145 \forall plusA: A \to A \to A. \forall n.
146 iter_p_gen n (\lambda x.false) A g baseA plusA = baseA.
155 theorem iter_p_gen_plusA: \forall A:Type. \forall n,k:nat.\forall p:nat \to bool.
156 \forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
157 (symmetric A plusA) \to (\forall a:A. (plusA a baseA) = a) \to (associative A plusA)
159 iter_p_gen (k + n) p A g baseA plusA
160 = (plusA (iter_p_gen k (\lambda x.p (x+n)) A (\lambda x.g (x+n)) baseA plusA)
161 (iter_p_gen n p A g baseA plusA)).
165 [ rewrite < (plus_n_O n).
167 rewrite > H in \vdash (? ? ? %).
170 | apply (bool_elim ? (p (n1+n)))
172 rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
173 rewrite > (true_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4).
174 rewrite > (H2 (g (n1 + n)) ? ?).
178 rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
179 rewrite > (false_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4).
185 theorem false_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool.
186 \forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
187 n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false)
188 \to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA.
208 (* a therem slightly more general than the previous one *)
209 theorem or_false_eq_baseA_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool.
210 \forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
211 (\forall a. plusA baseA a = a) \to
212 n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = baseA)
213 \to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA.
217 |apply (bool_elim ? (p n1));intro
220 apply not_eq_true_false.
224 |rewrite > true_to_iter_p_gen_Sn
230 |apply le_S.assumption
237 |rewrite > false_to_iter_p_gen_Sn
241 |apply le_S.assumption
249 theorem iter_p_gen2 :
251 \forall p1,p2:nat \to bool.
253 \forall g: nat \to nat \to A.
255 \forall plusA: A \to A \to A.
256 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a)
259 (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
261 (\lambda x.g (div x m) (mod x m))
265 (\lambda x.iter_p_gen m p2 A (g x) baseA plusA)
271 | apply (bool_elim ? (p1 n1))
273 rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
274 simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
275 rewrite > iter_p_gen_plusA
278 [ apply eq_iter_p_gen
281 rewrite > (div_plus_times ? ? ? H5).
282 rewrite > (mod_plus_times ? ? ? H5).
288 rewrite > (div_plus_times ? ? ? H5).
289 rewrite > (mod_plus_times ? ? ? H5).
291 simplify.reflexivity.
300 rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
301 simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
302 rewrite > iter_p_gen_plusA
304 apply (trans_eq ? ? (plusA baseA
305 (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m p2 A (g x) baseA plusA) baseA plusA )))
307 [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
308 [ apply iter_p_gen_false
311 rewrite > (div_plus_times ? ? ? H5).
312 rewrite > (mod_plus_times ? ? ? H5).
315 | intros.reflexivity.
331 theorem iter_p_gen2':
333 \forall p1: nat \to bool.
334 \forall p2: nat \to nat \to bool.
336 \forall g: nat \to nat \to A.
338 \forall plusA: A \to A \to A.
339 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a)
342 (\lambda x.andb (p1 (div x m)) (p2 (div x m)(mod x m)))
344 (\lambda x.g (div x m) (mod x m))
348 (\lambda x.iter_p_gen m (p2 x) A (g x) baseA plusA)
354 | apply (bool_elim ? (p1 n1))
356 rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
357 simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
358 rewrite > iter_p_gen_plusA
361 [ apply eq_iter_p_gen
364 rewrite > (div_plus_times ? ? ? H5).
365 rewrite > (mod_plus_times ? ? ? H5).
371 rewrite > (div_plus_times ? ? ? H5).
372 rewrite > (mod_plus_times ? ? ? H5).
374 simplify.reflexivity.
383 rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
384 simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
385 rewrite > iter_p_gen_plusA
387 apply (trans_eq ? ? (plusA baseA
388 (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m (p2 x) A (g x) baseA plusA) baseA plusA )))
390 [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
391 [ apply iter_p_gen_false
394 rewrite > (div_plus_times ? ? ? H5).
395 rewrite > (mod_plus_times ? ? ? H5).
398 | intros.reflexivity.
416 \forall g: nat \to A.
418 \forall plusA: A \to A \to A.
420 \forall p:nat \to bool.
421 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a)
424 i < n \to p i = true \to
425 (iter_p_gen n p A g baseA plusA) =
426 (plusA (g i) (iter_p_gen n (\lambda x:nat. andb (p x) (notb (eqb x i))) A g baseA plusA)).
430 apply (not_le_Sn_O i).
432 | apply (bool_elim ? (p n1));intro
433 [ elim (le_to_or_lt_eq i n1)
434 [ rewrite > true_to_iter_p_gen_Sn
435 [ rewrite > true_to_iter_p_gen_Sn
436 [ rewrite < (H2 (g i) ? ?).
437 rewrite > (H1 (g i) (g n1)).
438 rewrite > (H2 (g n1) ? ?).
449 | rewrite > H6.simplify.
450 change with (notb (eqb n1 i) = notb false).
452 apply not_eq_to_eqb_false.
454 apply (lt_to_not_eq ? ? H7).
455 apply sym_eq.assumption
459 | rewrite > true_to_iter_p_gen_Sn
463 | rewrite > false_to_iter_p_gen_Sn
464 [ apply eq_iter_p_gen
468 change with (notb false = notb (eqb x n1)).
471 apply not_eq_to_eqb_false.
472 apply (lt_to_not_eq ? ? H8)
479 rewrite > (eq_to_eqb_true ? ? (refl_eq ? n1)).
485 | apply le_S_S_to_le.
488 | rewrite > false_to_iter_p_gen_Sn
489 [ elim (le_to_or_lt_eq i n1)
490 [ rewrite > false_to_iter_p_gen_Sn
498 | rewrite > H6.reflexivity
501 apply not_eq_true_false.
505 | apply le_S_S_to_le.
514 (* invariance under permutation; single sum *)
515 theorem eq_iter_p_gen_gh:
518 \forall plusA: A \to A \to A.
519 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a) \to
520 \forall g: nat \to A.
521 \forall h,h1: nat \to nat.
523 \forall p1,p2:nat \to bool.
524 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
525 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
526 (\forall i. i < n \to p1 i = true \to h i < n1) \to
527 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
528 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
529 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
531 iter_p_gen n p1 A (\lambda x.g(h x)) baseA plusA =
532 iter_p_gen n1 p2 A g baseA plusA.
535 [ generalize in match H8.
538 | apply (bool_elim ? (p2 n2));intro
540 apply (not_le_Sn_O (h1 n2)).
545 | rewrite > false_to_iter_p_gen_Sn
557 | apply (bool_elim ? (p1 n1));intro
558 [ rewrite > true_to_iter_p_gen_Sn
559 [ rewrite > (iter_p_gen_gi A g baseA plusA n2 (h n1))
566 change with ((\not eqb (h i) (h n1))= \not false).
568 apply not_eq_to_eqb_false.
571 apply (lt_to_not_eq ? ? H11).
583 | apply le_S.assumption
594 [ apply le_S.assumption
600 | generalize in match H12.
609 | generalize in match H12.
616 elim (le_to_or_lt_eq (h1 j) n1)
618 | generalize in match H12.
628 | apply eqb_false_to_not_eq.
629 generalize in match H14.
631 [ apply sym_eq.assumption
637 apply not_eq_true_false.
638 apply sym_eq.assumption
640 | apply le_S_S_to_le.
643 | generalize in match H12.
666 | rewrite > false_to_iter_p_gen_Sn
669 apply H4[apply le_S.assumption|assumption]
671 apply H5[apply le_S.assumption|assumption]
673 apply H6[apply le_S.assumption|assumption]
675 apply H7[assumption|assumption]
677 apply H8[assumption|assumption]
679 elim (le_to_or_lt_eq (h1 j) n1)
681 | absurd (j = (h n1))
689 apply not_eq_true_false.
698 | apply le_S_S_to_le.
714 definition p_ord_times \def
717 [pair q r \Rightarrow r*m+q].
719 theorem eq_p_ord_times: \forall p,m,x.
720 p_ord_times p m x = (ord_rem x p)*m+(ord x p).
721 intros.unfold p_ord_times. unfold ord_rem.
727 theorem div_p_ord_times:
728 \forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
729 intros.rewrite > eq_p_ord_times.
730 apply div_plus_times.
734 theorem mod_p_ord_times:
735 \forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
736 intros.rewrite > eq_p_ord_times.
737 apply mod_plus_times.
741 lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
743 elim (le_to_or_lt_eq O ? (le_O_n m))
747 rewrite < times_n_O in H.
748 apply (not_le_Sn_O ? H)
752 (* lemmino da postare *)
753 theorem lt_times_to_lt_div: \forall i,n,m. i < n*m \to i/m < n.
756 [apply (lt_times_n_to_lt m)
758 |apply (le_to_lt_to_lt ? i)
759 [rewrite > (div_mod i m) in \vdash (? ? %).
765 |apply (lt_times_to_lt_O ? ? ? H)
769 theorem iter_p_gen_knm:
772 \forall plusA: A \to A \to A.
773 (symmetric A plusA) \to
774 (associative A plusA) \to
775 (\forall a:A.(plusA a baseA) = a)\to
776 \forall g: nat \to A.
777 \forall h2:nat \to nat \to nat.
778 \forall h11,h12:nat \to nat.
780 \forall p1,p21:nat \to bool.
781 \forall p22:nat \to nat \to bool.
782 (\forall x. x < k \to p1 x = true \to
783 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
784 \land h2 (h11 x) (h12 x) = x
785 \land (h11 x) < n \land (h12 x) < m) \to
786 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
787 p1 (h2 i j) = true \land
788 h11 (h2 i j) = i \land h12 (h2 i j) = j
789 \land h2 i j < k) \to
790 iter_p_gen k p1 A g baseA plusA =
791 iter_p_gen n p21 A (\lambda x:nat.iter_p_gen m (p22 x) A (\lambda y. g (h2 x y)) baseA plusA) baseA plusA.
793 rewrite < (iter_p_gen2' n m p21 p22 ? ? ? ? H H1 H2).
795 apply (eq_iter_p_gen_gh A baseA plusA H H1 H2 g ? (\lambda x.(h11 x)*m+(h12 x)))
797 elim (H4 (i/m) (i \mod m));clear H4
801 |apply (lt_times_to_lt_div ? ? ? H5)
803 apply (lt_times_to_lt_O ? ? ? H5)
804 |apply (andb_true_true ? ? H6)
805 |apply (andb_true_true_r ? ? H6)
808 elim (H4 (i/m) (i \mod m));clear H4
815 apply (lt_times_to_lt_O ? ? ? H5)
816 |apply (lt_times_to_lt_div ? ? ? H5)
818 apply (lt_times_to_lt_O ? ? ? H5)
819 |apply (andb_true_true ? ? H6)
820 |apply (andb_true_true_r ? ? H6)
823 elim (H4 (i/m) (i \mod m));clear H4
827 |apply (lt_times_to_lt_div ? ? ? H5)
829 apply (lt_times_to_lt_O ? ? ? H5)
830 |apply (andb_true_true ? ? H6)
831 |apply (andb_true_true_r ? ? H6)
838 rewrite > div_plus_times
839 [rewrite > mod_plus_times
852 rewrite > div_plus_times
853 [rewrite > mod_plus_times
864 apply (lt_to_le_to_lt ? ((h11 j)*m+m))
865 [apply monotonic_lt_plus_r.
868 change with ((S (h11 j)*m) \le n*m).
869 apply monotonic_le_times_l.
875 theorem iter_p_gen_divides:
878 \forall plusA: A \to A \to A.
879 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
880 \forall g: nat \to A.
881 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a)
885 iter_p_gen (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) A g baseA plusA =
886 iter_p_gen (S n) (\lambda x.divides_b x n) A
887 (\lambda x.iter_p_gen (S m) (\lambda y.true) A (\lambda y.g (x*(exp p y))) baseA plusA) baseA plusA.
890 [rewrite < (iter_p_gen2 ? ? ? ? ? ? ? ? H3 H4 H5).
892 (iter_p_gen (S n*S m) (\lambda x:nat.divides_b (x/S m) n) A
893 (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m))) baseA plusA) )
895 apply (eq_iter_p_gen_gh ? ? ? ? ? ? g ? (p_ord_times p (S m)))
900 lapply (divides_b_true_to_lt_O ? ? H H7).
901 apply divides_to_divides_b_true
902 [rewrite > (times_n_O O).
905 |apply lt_O_exp.assumption
908 [apply divides_b_true_to_divides.assumption
909 |apply (witness ? ? (p \sup (m-i \mod (S m)))).
910 rewrite < exp_plus_times.
913 apply plus_minus_m_m.
918 lapply (divides_b_true_to_lt_O ? ? H H7).
920 rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
921 [change with ((i/S m)*S m+i \mod S m=i).
928 apply (trans_divides ? (i/ S m))
930 apply divides_b_true_to_divides;assumption]
937 change with ((i/S m) < S n).
938 apply (lt_times_to_lt_l m).
939 apply (le_to_lt_to_lt ? i)
940 [autobatch|assumption]
950 [rewrite > div_p_ord_times
951 [apply divides_to_divides_b_true
954 |apply (divides_b_true_to_lt_O ? ? ? H7).
955 rewrite > (times_n_O O).
957 [assumption|apply lt_O_exp.assumption]
959 |cut (n = ord_rem (n*(exp p m)) p)
961 apply divides_to_divides_ord_rem
962 [apply (divides_b_true_to_lt_O ? ? ? H7).
963 rewrite > (times_n_O O).
965 [assumption|apply lt_O_exp.assumption]
966 |rewrite > (times_n_O O).
968 [assumption|apply lt_O_exp.assumption]
970 |apply divides_b_true_to_divides.
974 rewrite > (p_ord_exp1 p ? m n)
984 |cut (m = ord (n*(exp p m)) p)
987 apply divides_to_le_ord
988 [apply (divides_b_true_to_lt_O ? ? ? H7).
989 rewrite > (times_n_O O).
991 [assumption|apply lt_O_exp.assumption]
992 |rewrite > (times_n_O O).
994 [assumption|apply lt_O_exp.assumption]
996 |apply divides_b_true_to_divides.
1000 rewrite > (p_ord_exp1 p ? m n)
1010 [rewrite > div_p_ord_times
1011 [rewrite > mod_p_ord_times
1012 [rewrite > sym_times.
1016 |apply (divides_b_true_to_lt_O ? ? ? H7).
1017 rewrite > (times_n_O O).
1019 [assumption|apply lt_O_exp.assumption]
1021 |cut (m = ord (n*(exp p m)) p)
1024 apply divides_to_le_ord
1025 [apply (divides_b_true_to_lt_O ? ? ? H7).
1026 rewrite > (times_n_O O).
1028 [assumption|apply lt_O_exp.assumption]
1029 |rewrite > (times_n_O O).
1031 [assumption|apply lt_O_exp.assumption]
1033 |apply divides_b_true_to_divides.
1037 rewrite > (p_ord_exp1 p ? m n)
1047 |cut (m = ord (n*(exp p m)) p)
1050 apply divides_to_le_ord
1051 [apply (divides_b_true_to_lt_O ? ? ? H7).
1052 rewrite > (times_n_O O).
1054 [assumption|apply lt_O_exp.assumption]
1055 |rewrite > (times_n_O O).
1057 [assumption|apply lt_O_exp.assumption]
1059 |apply divides_b_true_to_divides.
1063 rewrite > (p_ord_exp1 p ? m n)
1072 rewrite > eq_p_ord_times.
1074 apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
1077 cut (m = ord (n*(p \sup m)) p)
1079 apply divides_to_le_ord
1080 [apply (divides_b_true_to_lt_O ? ? ? H7).
1081 rewrite > (times_n_O O).
1083 [assumption|apply lt_O_exp.assumption]
1084 |rewrite > (times_n_O O).
1086 [assumption|apply lt_O_exp.assumption]
1088 |apply divides_b_true_to_divides.
1092 rewrite > sym_times.
1093 rewrite > (p_ord_exp1 p ? m n)
1100 |change with (S (ord_rem j p)*S m \le S n*S m).
1103 cut (n = ord_rem (n*(p \sup m)) p)
1108 |rewrite > (times_n_O O).
1110 [assumption|apply lt_O_exp.assumption]
1112 |apply divides_to_divides_ord_rem
1113 [apply (divides_b_true_to_lt_O ? ? ? H7).
1114 rewrite > (times_n_O O).
1116 [assumption|apply lt_O_exp.assumption]
1117 |rewrite > (times_n_O O).
1119 [assumption|apply lt_O_exp.assumption]
1121 |apply divides_b_true_to_divides.
1126 rewrite > sym_times.
1127 rewrite > (p_ord_exp1 p ? m n)
1136 |apply eq_iter_p_gen
1139 elim (divides_b (x/S m) n);reflexivity
1143 |elim H1.apply lt_to_le.assumption
1147 (*distributive property for iter_p_gen*)
1148 theorem distributive_times_plus_iter_p_gen: \forall A:Type.
1149 \forall plusA: A \to A \to A. \forall basePlusA: A.
1150 \forall timesA: A \to A \to A.
1151 \forall n:nat. \forall k:A. \forall p:nat \to bool. \forall g:nat \to A.
1152 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a basePlusA) = a) \to
1153 (symmetric A timesA) \to (distributive A timesA plusA) \to
1154 (\forall a:A. (timesA a basePlusA) = basePlusA)
1158 ((timesA k (iter_p_gen n p A g basePlusA plusA)) =
1159 (iter_p_gen n p A (\lambda i:nat.(timesA k (g i))) basePlusA plusA)).
1164 | cut( (p n1) = true \lor (p n1) = false)
1166 [ rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
1167 rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
1169 rewrite > (H3 k (g n1)).
1172 | rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
1173 rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
1186 (* old version - proved without theorem iter_p_gen_knm
1187 theorem iter_p_gen_2_eq:
1190 \forall plusA: A \to A \to A.
1191 (symmetric A plusA) \to
1192 (associative A plusA) \to
1193 (\forall a:A.(plusA a baseA) = a)\to
1194 \forall g: nat \to nat \to A.
1195 \forall h11,h12,h21,h22: nat \to nat \to nat.
1196 \forall n1,m1,n2,m2.
1197 \forall p11,p21:nat \to bool.
1198 \forall p12,p22:nat \to nat \to bool.
1199 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
1200 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
1201 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
1202 \land h11 i j < n1 \land h12 i j < m1) \to
1203 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
1204 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
1205 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
1206 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
1208 (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA)
1211 (\lambda x:nat .iter_p_gen m2 (p22 x) A (\lambda y. g (h11 x y) (h12 x y)) baseA plusA )
1214 rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
1215 rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
1217 letin h := (\lambda x.(h11 (x/m2) (x\mod m2))*m1 + (h12 (x/m2) (x\mod m2))).
1218 letin h1 := (\lambda x.(h21 (x/m1) (x\mod m1))*m2 + (h22 (x/m1) (x\mod m1))).
1220 (iter_p_gen (n2*m2) (\lambda x:nat.p21 (x/m2)\land p22 (x/m2) (x\mod m2)) A
1221 (\lambda x:nat.g ((h x)/m1) ((h x)\mod m1)) baseA plusA ))
1223 apply eq_iter_p_gen1
1228 [cut (x \mod m2 < m2)
1229 [elim (and_true ? ? H6).
1230 elim (H3 ? ? Hcut1 Hcut2 H7 H8).
1237 apply div_plus_times.
1240 apply mod_plus_times.
1246 |apply (lt_times_n_to_lt m2)
1248 |apply (le_to_lt_to_lt ? x)
1249 [apply (eq_plus_to_le ? ? (x \mod m2)).
1256 |apply not_le_to_lt.unfold.intro.
1257 generalize in match H5.
1258 apply (le_n_O_elim ? H7).
1259 rewrite < times_n_O.
1264 |apply (eq_iter_p_gen_gh ? ? ? H H1 H2 ? h h1);intros
1267 [cut (i \mod m2 < m2)
1268 [elim (and_true ? ? H6).
1269 elim (H3 ? ? Hcut1 Hcut2 H7 H8).
1274 cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 =
1275 h11 (i/m2) (i\mod m2))
1276 [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
1277 h12 (i/m2) (i\mod m2))
1283 |apply mod_plus_times.
1286 |apply div_plus_times.
1292 |apply (lt_times_n_to_lt m2)
1294 |apply (le_to_lt_to_lt ? i)
1295 [apply (eq_plus_to_le ? ? (i \mod m2)).
1302 |apply not_le_to_lt.unfold.intro.
1303 generalize in match H5.
1304 apply (le_n_O_elim ? H7).
1305 rewrite < times_n_O.
1311 [cut (i \mod m2 < m2)
1312 [elim (and_true ? ? H6).
1313 elim (H3 ? ? Hcut1 Hcut2 H7 H8).
1318 cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 =
1319 h11 (i/m2) (i\mod m2))
1320 [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
1321 h12 (i/m2) (i\mod m2))
1329 |apply mod_plus_times.
1332 |apply div_plus_times.
1338 |apply (lt_times_n_to_lt m2)
1340 |apply (le_to_lt_to_lt ? i)
1341 [apply (eq_plus_to_le ? ? (i \mod m2)).
1348 |apply not_le_to_lt.unfold.intro.
1349 generalize in match H5.
1350 apply (le_n_O_elim ? H7).
1351 rewrite < times_n_O.
1357 [cut (i \mod m2 < m2)
1358 [elim (and_true ? ? H6).
1359 elim (H3 ? ? Hcut1 Hcut2 H7 H8).
1364 apply lt_times_plus_times
1365 [assumption|assumption]
1369 |apply (lt_times_n_to_lt m2)
1371 |apply (le_to_lt_to_lt ? i)
1372 [apply (eq_plus_to_le ? ? (i \mod m2)).
1379 |apply not_le_to_lt.unfold.intro.
1380 generalize in match H5.
1381 apply (le_n_O_elim ? H7).
1382 rewrite < times_n_O.
1388 [cut (j \mod m1 < m1)
1389 [elim (and_true ? ? H6).
1390 elim (H4 ? ? Hcut1 Hcut2 H7 H8).
1395 cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 =
1396 h21 (j/m1) (j\mod m1))
1397 [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
1398 h22 (j/m1) (j\mod m1))
1404 |apply mod_plus_times.
1407 |apply div_plus_times.
1413 |apply (lt_times_n_to_lt m1)
1415 |apply (le_to_lt_to_lt ? j)
1416 [apply (eq_plus_to_le ? ? (j \mod m1)).
1423 |apply not_le_to_lt.unfold.intro.
1424 generalize in match H5.
1425 apply (le_n_O_elim ? H7).
1426 rewrite < times_n_O.
1432 [cut (j \mod m1 < m1)
1433 [elim (and_true ? ? H6).
1434 elim (H4 ? ? Hcut1 Hcut2 H7 H8).
1439 cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 =
1440 h21 (j/m1) (j\mod m1))
1441 [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
1442 h22 (j/m1) (j\mod m1))
1450 |apply mod_plus_times.
1453 |apply div_plus_times.
1459 |apply (lt_times_n_to_lt m1)
1461 |apply (le_to_lt_to_lt ? j)
1462 [apply (eq_plus_to_le ? ? (j \mod m1)).
1469 |apply not_le_to_lt.unfold.intro.
1470 generalize in match H5.
1471 apply (le_n_O_elim ? H7).
1472 rewrite < times_n_O.
1478 [cut (j \mod m1 < m1)
1479 [elim (and_true ? ? H6).
1480 elim (H4 ? ? Hcut1 Hcut2 H7 H8).
1485 apply (lt_times_plus_times ? ? ? m2)
1486 [assumption|assumption]
1490 |apply (lt_times_n_to_lt m1)
1492 |apply (le_to_lt_to_lt ? j)
1493 [apply (eq_plus_to_le ? ? (j \mod m1)).
1500 |apply not_le_to_lt.unfold.intro.
1501 generalize in match H5.
1502 apply (le_n_O_elim ? H7).
1503 rewrite < times_n_O.
1512 theorem iter_p_gen_2_eq:
1515 \forall plusA: A \to A \to A.
1516 (symmetric A plusA) \to
1517 (associative A plusA) \to
1518 (\forall a:A.(plusA a baseA) = a)\to
1519 \forall g: nat \to nat \to A.
1520 \forall h11,h12,h21,h22: nat \to nat \to nat.
1521 \forall n1,m1,n2,m2.
1522 \forall p11,p21:nat \to bool.
1523 \forall p12,p22:nat \to nat \to bool.
1524 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
1525 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
1526 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
1527 \land h11 i j < n1 \land h12 i j < m1) \to
1528 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
1529 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
1530 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
1531 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
1533 (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA)
1536 (\lambda x:nat .iter_p_gen m2 (p22 x) A (\lambda y. g (h11 x y) (h12 x y)) baseA plusA )
1540 rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
1541 letin ha:= (\lambda x,y.(((h11 x y)*m1) + (h12 x y))).
1542 letin ha12:= (\lambda x.(h21 (x/m1) (x \mod m1))).
1543 letin ha22:= (\lambda x.(h22 (x/m1) (x \mod m1))).
1546 (iter_p_gen n2 p21 A (\lambda x:nat. iter_p_gen m2 (p22 x) A
1547 (\lambda y:nat.(g (((h11 x y)*m1+(h12 x y))/m1) (((h11 x y)*m1+(h12 x y))\mod m1))) baseA plusA ) baseA plusA))
1549 apply (iter_p_gen_knm A baseA plusA H H1 H2 (\lambda e. (g (e/m1) (e \mod m1))) ha ha12 ha22);intros
1550 [ elim (and_true ? ? H6).
1553 [ cut((x \mod m1) < m1)
1554 [ elim (H4 ? ? Hcut1 Hcut2 H7 H8).
1579 | apply (lt_times_n_to_lt m1)
1581 | apply (le_to_lt_to_lt ? x)
1582 [ apply (eq_plus_to_le ? ? (x \mod m1)).
1589 | apply not_le_to_lt.unfold.intro.
1590 generalize in match H5.
1591 apply (le_n_O_elim ? H9).
1592 rewrite < times_n_O.
1596 | elim (H3 ? ? H5 H6 H7 H8).
1601 cut(((h11 i j)*m1 + (h12 i j))/m1 = (h11 i j))
1602 [ cut(((h11 i j)*m1 + (h12 i j)) \mod m1 = (h12 i j))
1606 [ apply true_to_true_to_andb_true
1623 [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
1624 [ apply (lt_plus_r).
1626 | rewrite > sym_plus.
1627 rewrite > (sym_times (h11 i j) m1).
1628 rewrite > times_n_Sm.
1629 rewrite > sym_times.
1633 | apply not_le_to_lt.unfold.intro.
1634 generalize in match H12.
1635 apply (le_n_O_elim ? H11).
1639 | apply not_le_to_lt.unfold.intro.
1640 generalize in match H10.
1641 apply (le_n_O_elim ? H11).
1646 | rewrite > (mod_plus_times m1 (h11 i j) (h12 i j)).
1650 | rewrite > (div_plus_times m1 (h11 i j) (h12 i j)).
1655 | apply (eq_iter_p_gen1)
1656 [ intros. reflexivity
1658 apply (eq_iter_p_gen1)
1659 [ intros. reflexivity
1661 rewrite > (div_plus_times)
1662 [ rewrite > (mod_plus_times)
1664 | elim (H3 x x1 H5 H7 H6 H8).
1667 | elim (H3 x x1 H5 H7 H6 H8).
1675 theorem iter_p_gen_iter_p_gen:
1678 \forall plusA: A \to A \to A.
1679 (symmetric A plusA) \to
1680 (associative A plusA) \to
1681 (\forall a:A.(plusA a baseA) = a)\to
1682 \forall g: nat \to nat \to A.
1684 \forall p11,p21:nat \to bool.
1685 \forall p12,p22:nat \to nat \to bool.
1686 (\forall x,y. x < n \to y < m \to
1687 (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
1689 (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA)
1692 (\lambda y:nat.iter_p_gen n (p22 y) A (\lambda x. g x y) baseA plusA )
1695 apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y) (\lambda x,y.x) (\lambda x,y.y) (\lambda x,y.x)
1696 n m m n p11 p21 p12 p22)
1702 [apply (andb_true_true ? (p12 j i)).
1704 [rewrite > H6.rewrite > H7.reflexivity
1708 |apply (andb_true_true_r (p11 j)).
1710 [rewrite > H6.rewrite > H7.reflexivity
1728 [apply (andb_true_true ? (p22 j i)).
1730 [rewrite > H6.rewrite > H7.reflexivity
1734 |apply (andb_true_true_r (p21 j)).
1736 [rewrite > H6.rewrite > H7.reflexivity