2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "arithmetics/nat.ma".
14 let rec bigop' (n:nat) (filter: nat → bool) (A:Type[0]) (f: nat → A)
15 (nil: A) (op: A → A → A) ≝
20 [true ⇒ op (f k) (bigop' k filter A f nil op)
21 |false ⇒ bigop' k filter A f nil op]
24 record range (A:Type[0]): Type[0] ≝
25 {h:nat→A; upto:nat; filter:nat→bool}.
27 definition same_upto: nat → ∀A.relation (range A) ≝
30 ((filter A I i) = (filter A J i) ∧
31 ((filter A I i) = true → (h A I i) = (h A J i))).
33 definition same: ∀A.relation (range A) ≝
34 λA.λI,J. (upto A I = upto A J) ∧ same_upto (upto A I) A I J.
36 definition pad: ∀A.nat→range A→range A ≝
37 λA.λk.λI.mk_range A (h A I) k
38 (λi.if_then_else ? (leb (upto A I) i) false (filter A I i)).
40 definition same1: ∀A.relation (range A) ≝
42 let maxIJ ≝ (max (upto A I) (upto A J)) in
43 same_upto maxIJ A (pad A maxIJ I) (pad A maxIJ J).
46 definition same: ∀A.relation (range A) ≝
48 ∀i. i < max (upto A I) (upto A J) →
49 ((filter A I i) = (filter A J i) ∧
50 ((filter A I i) = true → (h A I i) = (h A J i))). *)
52 definition bigop: ∀A,B:Type[0].(range A)→B→(B→B→B)→(A→B)→B ≝
54 bigop' (upto A I) (filter A I) B (λx.f(h A I x)) nil op.
56 theorem same_bigop: ∀A,B.∀I,J:range A. ∀nil.∀op.∀f.
57 same A I J → bigop A B I nil op f = bigop A B J nil op f.
58 #A #B #I #J #nil #op #f * #equp normalize <equp #same
59 @(le_gen ? (upto A I)) #i (elim i) // #i #Hind #lti
60 (lapply (same i lti)) * #eqfilter
61 (lapply (Hind (transitive_le … (le_n_Sn i) (lti)))) #eqbigop
62 normalize <eqfilter (cases (filter A I i)) normalize //
63 #H (lapply (H (refl ??))) // qed.
65 theorem pad_bigog: ∀A,B.∀I:range A. ∀nil.∀op.∀f.∀k.
66 upto A I ≤ k → bigop A B I nil op f = bigop A B (pad A k I) nil op f.
67 #A #B #I #nil #op #f #k #lek (elim lek)
68 [@same_bigop % // #i #lti % // normalize
69 >(not_le_to_leb_false …) // @lt_to_not_le //
70 |#n #leup #Hind normalize <Hind >(le_to_leb_true … leup) normalize //
73 theorem iter_p_gen_false: \forall A:Type. \forall g: nat \to A. \forall baseA:A.
74 \forall plusA: A \to A \to A. \forall n.
75 iter_p_gen n (\lambda x.false) A g baseA plusA = baseA.
84 theorem iter_p_gen_plusA: \forall A:Type. \forall n,k:nat.\forall p:nat \to bool.
85 \forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
86 (symmetric A plusA) \to (\forall a:A. (plusA a baseA) = a) \to (associative A plusA)
88 iter_p_gen (k + n) p A g baseA plusA
89 = (plusA (iter_p_gen k (\lambda x.p (x+n)) A (\lambda x.g (x+n)) baseA plusA)
90 (iter_p_gen n p A g baseA plusA)).
95 rewrite > H in \vdash (? ? ? %).
98 | apply (bool_elim ? (p (n1+n)))
100 rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
101 rewrite > (true_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4).
102 rewrite > (H2 (g (n1 + n)) ? ?).
106 rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
107 rewrite > (false_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4).
113 theorem false_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool.
114 \forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
115 n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false)
116 \to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA.
136 (* a therem slightly more general than the previous one *)
137 theorem or_false_eq_baseA_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool.
138 \forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
139 (\forall a. plusA baseA a = a) \to
140 n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = baseA)
141 \to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA.
145 |apply (bool_elim ? (p n1));intro
148 apply not_eq_true_false.
152 |rewrite > true_to_iter_p_gen_Sn
158 |apply le_S.assumption
165 |rewrite > false_to_iter_p_gen_Sn
169 |apply le_S.assumption
177 theorem iter_p_gen2 :
179 \forall p1,p2:nat \to bool.
181 \forall g: nat \to nat \to A.
183 \forall plusA: A \to A \to A.
184 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a)
187 (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
189 (\lambda x.g (div x m) (mod x m))
193 (\lambda x.iter_p_gen m p2 A (g x) baseA plusA)
199 | apply (bool_elim ? (p1 n1))
201 rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
202 simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
203 rewrite > iter_p_gen_plusA
206 [ apply eq_iter_p_gen
209 rewrite > (div_plus_times ? ? ? H5).
210 rewrite > (mod_plus_times ? ? ? H5).
216 rewrite > (div_plus_times ? ? ? H5).
217 rewrite > (mod_plus_times ? ? ? H5).
227 rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
228 simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
229 rewrite > iter_p_gen_plusA
231 apply (trans_eq ? ? (plusA baseA
232 (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m p2 A (g x) baseA plusA) baseA plusA )))
234 [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
235 [ apply iter_p_gen_false
238 rewrite > (div_plus_times ? ? ? H5).
239 rewrite > (mod_plus_times ? ? ? H5).
242 | intros.reflexivity.
258 theorem iter_p_gen2':
260 \forall p1: nat \to bool.
261 \forall p2: nat \to nat \to bool.
263 \forall g: nat \to nat \to A.
265 \forall plusA: A \to A \to A.
266 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a)
269 (\lambda x.andb (p1 (div x m)) (p2 (div x m)(mod x m)))
271 (\lambda x.g (div x m) (mod x m))
275 (\lambda x.iter_p_gen m (p2 x) A (g x) baseA plusA)
281 | apply (bool_elim ? (p1 n1))
283 rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
284 simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
285 rewrite > iter_p_gen_plusA
288 [ apply eq_iter_p_gen
291 rewrite > (div_plus_times ? ? ? H5).
292 rewrite > (mod_plus_times ? ? ? H5).
298 rewrite > (div_plus_times ? ? ? H5).
299 rewrite > (mod_plus_times ? ? ? H5).
309 rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
310 simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
311 rewrite > iter_p_gen_plusA
313 apply (trans_eq ? ? (plusA baseA
314 (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m (p2 x) A (g x) baseA plusA) baseA plusA )))
316 [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
317 [ apply iter_p_gen_false
320 rewrite > (div_plus_times ? ? ? H5).
321 rewrite > (mod_plus_times ? ? ? H5).
324 | intros.reflexivity.
342 \forall g: nat \to A.
344 \forall plusA: A \to A \to A.
346 \forall p:nat \to bool.
347 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a)
350 i < n \to p i = true \to
351 (iter_p_gen n p A g baseA plusA) =
352 (plusA (g i) (iter_p_gen n (\lambda x:nat. andb (p x) (notb (eqb x i))) A g baseA plusA)).
356 apply (not_le_Sn_O i).
358 | apply (bool_elim ? (p n1));intro
359 [ elim (le_to_or_lt_eq i n1)
360 [ rewrite > true_to_iter_p_gen_Sn
361 [ rewrite > true_to_iter_p_gen_Sn
362 [ rewrite < (H2 (g i) ? ?).
363 rewrite > (H1 (g i) (g n1)).
364 rewrite > (H2 (g n1) ? ?).
375 | rewrite > H6.simplify.
376 change with (notb (eqb n1 i) = notb false).
378 apply not_eq_to_eqb_false.
380 apply (lt_to_not_eq ? ? H7).
381 apply sym_eq.assumption
385 | rewrite > true_to_iter_p_gen_Sn
389 | rewrite > false_to_iter_p_gen_Sn
390 [ apply eq_iter_p_gen
394 change with (notb false = notb (eqb x n1)).
397 apply not_eq_to_eqb_false.
398 apply (lt_to_not_eq ? ? H8)
405 rewrite > (eq_to_eqb_true ? ? (refl_eq ? n1)).
411 | apply le_S_S_to_le.
414 | rewrite > false_to_iter_p_gen_Sn
415 [ elim (le_to_or_lt_eq i n1)
416 [ rewrite > false_to_iter_p_gen_Sn
424 | rewrite > H6.reflexivity
427 apply not_eq_true_false.
431 | apply le_S_S_to_le.
440 (* invariance under permutation; single sum *)
441 theorem eq_iter_p_gen_gh:
444 \forall plusA: A \to A \to A.
445 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a) \to
446 \forall g: nat \to A.
447 \forall h,h1: nat \to nat.
449 \forall p1,p2:nat \to bool.
450 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
451 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
452 (\forall i. i < n \to p1 i = true \to h i < n1) \to
453 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
454 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
455 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
457 iter_p_gen n p1 A (\lambda x.g(h x)) baseA plusA =
458 iter_p_gen n1 p2 A g baseA plusA.
461 [ generalize in match H8.
464 | apply (bool_elim ? (p2 n2));intro
466 apply (not_le_Sn_O (h1 n2)).
471 | rewrite > false_to_iter_p_gen_Sn
483 | apply (bool_elim ? (p1 n1));intro
484 [ rewrite > true_to_iter_p_gen_Sn
485 [ rewrite > (iter_p_gen_gi A g baseA plusA n2 (h n1))
492 change with ((\not eqb (h i) (h n1))= \not false).
494 apply not_eq_to_eqb_false.
497 apply (lt_to_not_eq ? ? H11).
509 | apply le_S.assumption
520 [ apply le_S.assumption
526 | generalize in match H12.
535 | generalize in match H12.
542 elim (le_to_or_lt_eq (h1 j) n1)
544 | generalize in match H12.
552 | apply andb_true_true; [2: apply H12]
554 | apply eqb_false_to_not_eq.
555 generalize in match H14.
557 [ apply sym_eq.assumption
563 apply not_eq_true_false.
564 apply sym_eq.assumption
566 | apply le_S_S_to_le.
569 | generalize in match H12.
592 | rewrite > false_to_iter_p_gen_Sn
595 apply H4[apply le_S.assumption|assumption]
597 apply H5[apply le_S.assumption|assumption]
599 apply H6[apply le_S.assumption|assumption]
601 apply H7[assumption|assumption]
603 apply H8[assumption|assumption]
605 elim (le_to_or_lt_eq (h1 j) n1)
607 | absurd (j = (h n1))
615 apply not_eq_true_false.
624 | apply le_S_S_to_le.
637 theorem eq_iter_p_gen_pred:
640 \forall plusA: A \to A \to A.
643 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a) \to
644 iter_p_gen (S n) (\lambda i.p (pred i)) A (\lambda i.g(pred i)) baseA plusA =
645 plusA (iter_p_gen n p A g baseA plusA) (g O).
648 [rewrite > true_to_iter_p_gen_Sn
652 |apply (bool_elim ? (p n1));intro
653 [rewrite > true_to_iter_p_gen_Sn
654 [rewrite > true_to_iter_p_gen_Sn in ⊢ (? ? ? %)
655 [rewrite > H2 in ⊢ (? ? ? %).
656 apply eq_f.assumption
661 |rewrite > false_to_iter_p_gen_Sn
662 [rewrite > false_to_iter_p_gen_Sn in ⊢ (? ? ? %);assumption
669 definition p_ord_times \def
672 [pair q r \Rightarrow r*m+q].
674 theorem eq_p_ord_times: \forall p,m,x.
675 p_ord_times p m x = (ord_rem x p)*m+(ord x p).
676 intros.unfold p_ord_times. unfold ord_rem.
682 theorem div_p_ord_times:
683 \forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
684 intros.rewrite > eq_p_ord_times.
685 apply div_plus_times.
689 theorem mod_p_ord_times:
690 \forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
691 intros.rewrite > eq_p_ord_times.
692 apply mod_plus_times.
696 lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
698 elim (le_to_or_lt_eq O ? (le_O_n m))
702 rewrite < times_n_O in H.
703 apply (not_le_Sn_O ? H)
707 theorem iter_p_gen_knm:
710 \forall plusA: A \to A \to A.
711 (symmetric A plusA) \to
712 (associative A plusA) \to
713 (\forall a:A.(plusA a baseA) = a)\to
714 \forall g: nat \to A.
715 \forall h2:nat \to nat \to nat.
716 \forall h11,h12:nat \to nat.
718 \forall p1,p21:nat \to bool.
719 \forall p22:nat \to nat \to bool.
720 (\forall x. x < k \to p1 x = true \to
721 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
722 \land h2 (h11 x) (h12 x) = x
723 \land (h11 x) < n \land (h12 x) < m) \to
724 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
725 p1 (h2 i j) = true \land
726 h11 (h2 i j) = i \land h12 (h2 i j) = j
727 \land h2 i j < k) \to
728 iter_p_gen k p1 A g baseA plusA =
729 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.
731 rewrite < (iter_p_gen2' n m p21 p22 ? ? ? ? H H1 H2).
733 apply (eq_iter_p_gen_gh A baseA plusA H H1 H2 g ? (\lambda x.(h11 x)*m+(h12 x)))
735 elim (H4 (i/m) (i \mod m));clear H4
739 |apply (lt_times_to_lt_div ? ? ? H5)
741 apply (lt_times_to_lt_O ? ? ? H5)
742 |apply (andb_true_true ? ? H6)
743 |apply (andb_true_true_r ? ? H6)
746 elim (H4 (i/m) (i \mod m));clear H4
753 apply (lt_times_to_lt_O ? ? ? H5)
754 |apply (lt_times_to_lt_div ? ? ? H5)
756 apply (lt_times_to_lt_O ? ? ? H5)
757 |apply (andb_true_true ? ? H6)
758 |apply (andb_true_true_r ? ? H6)
761 elim (H4 (i/m) (i \mod m));clear H4
765 |apply (lt_times_to_lt_div ? ? ? H5)
767 apply (lt_times_to_lt_O ? ? ? H5)
768 |apply (andb_true_true ? ? H6)
769 |apply (andb_true_true_r ? ? H6)
776 rewrite > div_plus_times
777 [rewrite > mod_plus_times
790 rewrite > div_plus_times
791 [rewrite > mod_plus_times
802 apply (lt_to_le_to_lt ? ((h11 j)*m+m))
803 [apply monotonic_lt_plus_r.
806 change with ((S (h11 j)*m) \le n*m).
807 apply monotonic_le_times_l.
813 theorem iter_p_gen_divides:
816 \forall plusA: A \to A \to A.
817 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
818 \forall g: nat \to A.
819 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a)
823 iter_p_gen (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) A g baseA plusA =
824 iter_p_gen (S n) (\lambda x.divides_b x n) A
825 (\lambda x.iter_p_gen (S m) (\lambda y.true) A (\lambda y.g (x*(exp p y))) baseA plusA) baseA plusA.
828 [rewrite < (iter_p_gen2 ? ? ? ? ? ? ? ? H3 H4 H5).
830 (iter_p_gen (S n*S m) (\lambda x:nat.divides_b (x/S m) n) A
831 (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m))) baseA plusA) )
833 apply (eq_iter_p_gen_gh ? ? ? ? ? ? g ? (p_ord_times p (S m)))
838 lapply (divides_b_true_to_lt_O ? ? H H7).
839 apply divides_to_divides_b_true
840 [rewrite > (times_n_O O).
843 |apply lt_O_exp.assumption
846 [apply divides_b_true_to_divides.assumption
847 |apply (witness ? ? (p \sup (m-i \mod (S m)))).
848 rewrite < exp_plus_times.
851 apply plus_minus_m_m.
852 autobatch by le_S_S_to_le, lt_mod_m_m, lt_O_S;
856 lapply (divides_b_true_to_lt_O ? ? H H7).
858 rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
859 [change with ((i/S m)*S m+i \mod S m=i).
866 apply (trans_divides ? (i/ S m))
868 apply divides_b_true_to_divides;assumption]
875 change with ((i/S m) < S n).
876 apply (lt_times_to_lt_l m).
877 apply (le_to_lt_to_lt ? i);[2:assumption]
878 autobatch by eq_plus_to_le, div_mod, lt_O_S.
888 [rewrite > div_p_ord_times
889 [apply divides_to_divides_b_true
892 |apply (divides_b_true_to_lt_O ? ? ? H7).
893 rewrite > (times_n_O O).
895 [assumption|apply lt_O_exp.assumption]
897 |cut (n = ord_rem (n*(exp p m)) p)
899 apply divides_to_divides_ord_rem
900 [apply (divides_b_true_to_lt_O ? ? ? H7).
901 rewrite > (times_n_O O).
903 [assumption|apply lt_O_exp.assumption]
904 |rewrite > (times_n_O O).
906 [assumption|apply lt_O_exp.assumption]
908 |apply divides_b_true_to_divides.
912 rewrite > (p_ord_exp1 p ? m n)
922 |cut (m = ord (n*(exp p m)) p)
925 apply divides_to_le_ord
926 [apply (divides_b_true_to_lt_O ? ? ? H7).
927 rewrite > (times_n_O O).
929 [assumption|apply lt_O_exp.assumption]
930 |rewrite > (times_n_O O).
932 [assumption|apply lt_O_exp.assumption]
934 |apply divides_b_true_to_divides.
938 rewrite > (p_ord_exp1 p ? m n)
948 [rewrite > div_p_ord_times
949 [rewrite > mod_p_ord_times
950 [rewrite > sym_times.
954 |apply (divides_b_true_to_lt_O ? ? ? H7).
955 rewrite > (times_n_O O).
957 [assumption|apply lt_O_exp.assumption]
959 |cut (m = ord (n*(exp p m)) p)
962 apply divides_to_le_ord
963 [apply (divides_b_true_to_lt_O ? ? ? H7).
964 rewrite > (times_n_O O).
966 [assumption|apply lt_O_exp.assumption]
967 |rewrite > (times_n_O O).
969 [assumption|apply lt_O_exp.assumption]
971 |apply divides_b_true_to_divides.
975 rewrite > (p_ord_exp1 p ? m n)
985 |cut (m = ord (n*(exp p m)) p)
988 apply divides_to_le_ord
989 [apply (divides_b_true_to_lt_O ? ? ? H7).
990 rewrite > (times_n_O O).
992 [assumption|apply lt_O_exp.assumption]
993 |rewrite > (times_n_O O).
995 [assumption|apply lt_O_exp.assumption]
997 |apply divides_b_true_to_divides.
1001 rewrite > (p_ord_exp1 p ? m n)
1010 rewrite > eq_p_ord_times.
1012 apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
1015 cut (m = ord (n*(p \sup m)) p)
1017 apply divides_to_le_ord
1018 [apply (divides_b_true_to_lt_O ? ? ? H7).
1019 rewrite > (times_n_O O).
1021 [assumption|apply lt_O_exp.assumption]
1022 |rewrite > (times_n_O O).
1024 [assumption|apply lt_O_exp.assumption]
1026 |apply divides_b_true_to_divides.
1030 rewrite > sym_times.
1031 rewrite > (p_ord_exp1 p ? m n)
1038 |change with (S (ord_rem j p)*S m \le S n*S m).
1041 cut (n = ord_rem (n*(p \sup m)) p)
1046 |rewrite > (times_n_O O).
1048 [assumption|apply lt_O_exp.assumption]
1050 |apply divides_to_divides_ord_rem
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.
1064 rewrite > sym_times.
1065 rewrite > (p_ord_exp1 p ? m n)
1074 |apply eq_iter_p_gen
1077 elim (divides_b (x/S m) n);reflexivity
1081 |elim H1.apply lt_to_le.assumption
1085 (*distributive property for iter_p_gen*)
1086 theorem distributive_times_plus_iter_p_gen: \forall A:Type.
1087 \forall plusA: A \to A \to A. \forall basePlusA: A.
1088 \forall timesA: A \to A \to A.
1089 \forall n:nat. \forall k:A. \forall p:nat \to bool. \forall g:nat \to A.
1090 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a basePlusA) = a) \to
1091 (symmetric A timesA) \to (distributive A timesA plusA) \to
1092 (\forall a:A. (timesA a basePlusA) = basePlusA)
1096 ((timesA k (iter_p_gen n p A g basePlusA plusA)) =
1097 (iter_p_gen n p A (\lambda i:nat.(timesA k (g i))) basePlusA plusA)).
1102 | cut( (p n1) = true \lor (p n1) = false)
1104 [ rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
1105 rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
1107 rewrite > (H3 k (g n1)).
1110 | rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
1111 rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
1124 (* old version - proved without theorem iter_p_gen_knm
1125 theorem iter_p_gen_2_eq:
1128 \forall plusA: A \to A \to A.
1129 (symmetric A plusA) \to
1130 (associative A plusA) \to
1131 (\forall a:A.(plusA a baseA) = a)\to
1132 \forall g: nat \to nat \to A.
1133 \forall h11,h12,h21,h22: nat \to nat \to nat.
1134 \forall n1,m1,n2,m2.
1135 \forall p11,p21:nat \to bool.
1136 \forall p12,p22:nat \to nat \to bool.
1137 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
1138 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
1139 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
1140 \land h11 i j < n1 \land h12 i j < m1) \to
1141 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
1142 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
1143 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
1144 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
1146 (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA)
1149 (\lambda x:nat .iter_p_gen m2 (p22 x) A (\lambda y. g (h11 x y) (h12 x y)) baseA plusA )
1152 rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
1153 rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
1155 letin h := (\lambda x.(h11 (x/m2) (x\mod m2))*m1 + (h12 (x/m2) (x\mod m2))).
1156 letin h1 := (\lambda x.(h21 (x/m1) (x\mod m1))*m2 + (h22 (x/m1) (x\mod m1))).
1158 (iter_p_gen (n2*m2) (\lambda x:nat.p21 (x/m2)\land p22 (x/m2) (x\mod m2)) A
1159 (\lambda x:nat.g ((h x)/m1) ((h x)\mod m1)) baseA plusA ))
1161 apply eq_iter_p_gen1
1166 [cut (x \mod m2 < m2)
1167 [elim (and_true ? ? H6).
1168 elim (H3 ? ? Hcut1 Hcut2 H7 H8).
1175 apply div_plus_times.
1178 apply mod_plus_times.
1184 |apply (lt_times_n_to_lt m2)
1186 |apply (le_to_lt_to_lt ? x)
1187 [apply (eq_plus_to_le ? ? (x \mod m2)).
1194 |apply not_le_to_lt.unfold.intro.
1195 generalize in match H5.
1196 apply (le_n_O_elim ? H7).
1197 rewrite < times_n_O.
1202 |apply (eq_iter_p_gen_gh ? ? ? H H1 H2 ? h h1);intros
1205 [cut (i \mod m2 < m2)
1206 [elim (and_true ? ? H6).
1207 elim (H3 ? ? Hcut1 Hcut2 H7 H8).
1212 cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 =
1213 h11 (i/m2) (i\mod m2))
1214 [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
1215 h12 (i/m2) (i\mod m2))
1221 |apply mod_plus_times.
1224 |apply div_plus_times.
1230 |apply (lt_times_n_to_lt m2)
1232 |apply (le_to_lt_to_lt ? i)
1233 [apply (eq_plus_to_le ? ? (i \mod m2)).
1240 |apply not_le_to_lt.unfold.intro.
1241 generalize in match H5.
1242 apply (le_n_O_elim ? H7).
1243 rewrite < times_n_O.
1249 [cut (i \mod m2 < m2)
1250 [elim (and_true ? ? H6).
1251 elim (H3 ? ? Hcut1 Hcut2 H7 H8).
1256 cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 =
1257 h11 (i/m2) (i\mod m2))
1258 [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
1259 h12 (i/m2) (i\mod m2))
1267 |apply mod_plus_times.
1270 |apply div_plus_times.
1276 |apply (lt_times_n_to_lt m2)
1278 |apply (le_to_lt_to_lt ? i)
1279 [apply (eq_plus_to_le ? ? (i \mod m2)).
1286 |apply not_le_to_lt.unfold.intro.
1287 generalize in match H5.
1288 apply (le_n_O_elim ? H7).
1289 rewrite < times_n_O.
1295 [cut (i \mod m2 < m2)
1296 [elim (and_true ? ? H6).
1297 elim (H3 ? ? Hcut1 Hcut2 H7 H8).
1302 apply lt_times_plus_times
1303 [assumption|assumption]
1307 |apply (lt_times_n_to_lt m2)
1309 |apply (le_to_lt_to_lt ? i)
1310 [apply (eq_plus_to_le ? ? (i \mod m2)).
1317 |apply not_le_to_lt.unfold.intro.
1318 generalize in match H5.
1319 apply (le_n_O_elim ? H7).
1320 rewrite < times_n_O.
1326 [cut (j \mod m1 < m1)
1327 [elim (and_true ? ? H6).
1328 elim (H4 ? ? Hcut1 Hcut2 H7 H8).
1333 cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 =
1334 h21 (j/m1) (j\mod m1))
1335 [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
1336 h22 (j/m1) (j\mod m1))
1342 |apply mod_plus_times.
1345 |apply div_plus_times.
1351 |apply (lt_times_n_to_lt m1)
1353 |apply (le_to_lt_to_lt ? j)
1354 [apply (eq_plus_to_le ? ? (j \mod m1)).
1361 |apply not_le_to_lt.unfold.intro.
1362 generalize in match H5.
1363 apply (le_n_O_elim ? H7).
1364 rewrite < times_n_O.
1370 [cut (j \mod m1 < m1)
1371 [elim (and_true ? ? H6).
1372 elim (H4 ? ? Hcut1 Hcut2 H7 H8).
1377 cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 =
1378 h21 (j/m1) (j\mod m1))
1379 [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
1380 h22 (j/m1) (j\mod m1))
1388 |apply mod_plus_times.
1391 |apply div_plus_times.
1397 |apply (lt_times_n_to_lt m1)
1399 |apply (le_to_lt_to_lt ? j)
1400 [apply (eq_plus_to_le ? ? (j \mod m1)).
1407 |apply not_le_to_lt.unfold.intro.
1408 generalize in match H5.
1409 apply (le_n_O_elim ? H7).
1410 rewrite < times_n_O.
1416 [cut (j \mod m1 < m1)
1417 [elim (and_true ? ? H6).
1418 elim (H4 ? ? Hcut1 Hcut2 H7 H8).
1423 apply (lt_times_plus_times ? ? ? m2)
1424 [assumption|assumption]
1428 |apply (lt_times_n_to_lt m1)
1430 |apply (le_to_lt_to_lt ? j)
1431 [apply (eq_plus_to_le ? ? (j \mod m1)).
1438 |apply not_le_to_lt.unfold.intro.
1439 generalize in match H5.
1440 apply (le_n_O_elim ? H7).
1441 rewrite < times_n_O.
1450 theorem iter_p_gen_2_eq:
1453 \forall plusA: A \to A \to A.
1454 (symmetric A plusA) \to
1455 (associative A plusA) \to
1456 (\forall a:A.(plusA a baseA) = a)\to
1457 \forall g: nat \to nat \to A.
1458 \forall h11,h12,h21,h22: nat \to nat \to nat.
1459 \forall n1,m1,n2,m2.
1460 \forall p11,p21:nat \to bool.
1461 \forall p12,p22:nat \to nat \to bool.
1462 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
1463 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
1464 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
1465 \land h11 i j < n1 \land h12 i j < m1) \to
1466 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
1467 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
1468 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
1469 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
1471 (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA)
1474 (\lambda x:nat .iter_p_gen m2 (p22 x) A (\lambda y. g (h11 x y) (h12 x y)) baseA plusA )
1478 rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
1479 letin ha:= (\lambda x,y.(((h11 x y)*m1) + (h12 x y))).
1480 letin ha12:= (\lambda x.(h21 (x/m1) (x \mod m1))).
1481 letin ha22:= (\lambda x.(h22 (x/m1) (x \mod m1))).
1484 (iter_p_gen n2 p21 A (\lambda x:nat. iter_p_gen m2 (p22 x) A
1485 (\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))
1487 apply (iter_p_gen_knm A baseA plusA H H1 H2 (\lambda e. (g (e/m1) (e \mod m1))) ha ha12 ha22);intros
1488 [ elim (and_true ? ? H6).
1491 [ cut((x \mod m1) < m1)
1492 [ elim (H4 ? ? Hcut1 Hcut2 H7 H8).
1520 | apply (lt_times_n_to_lt m1)
1522 | apply (le_to_lt_to_lt ? x)
1523 [ apply (eq_plus_to_le ? ? (x \mod m1)).
1530 | apply not_le_to_lt.unfold.intro.
1531 generalize in match H5.
1532 apply (le_n_O_elim ? H9).
1533 rewrite < times_n_O.
1537 | elim (H3 ? ? H5 H6 H7 H8).
1542 cut(((h11 i j)*m1 + (h12 i j))/m1 = (h11 i j))
1543 [ cut(((h11 i j)*m1 + (h12 i j)) \mod m1 = (h12 i j))
1547 [ apply true_to_true_to_andb_true
1568 [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
1572 | rewrite > sym_plus.
1573 rewrite > (sym_times (h11 i j) m1).
1574 rewrite > times_n_Sm.
1575 rewrite > sym_times.
1579 | apply not_le_to_lt.unfold.intro.
1580 generalize in match H12.
1581 apply (le_n_O_elim ? H11).
1585 | apply not_le_to_lt.unfold.intro.
1586 generalize in match H10.
1587 apply (le_n_O_elim ? H11).
1592 | rewrite > (mod_plus_times m1 (h11 i j) (h12 i j)).
1596 | rewrite > (div_plus_times m1 (h11 i j) (h12 i j)).
1601 | apply (eq_iter_p_gen1)
1602 [ intros. reflexivity
1604 apply (eq_iter_p_gen1)
1605 [ intros. reflexivity
1607 rewrite > (div_plus_times)
1608 [ rewrite > (mod_plus_times)
1610 | elim (H3 x x1 H5 H7 H6 H8).
1613 | elim (H3 x x1 H5 H7 H6 H8).
1621 theorem iter_p_gen_iter_p_gen:
1624 \forall plusA: A \to A \to A.
1625 (symmetric A plusA) \to
1626 (associative A plusA) \to
1627 (\forall a:A.(plusA a baseA) = a)\to
1628 \forall g: nat \to nat \to A.
1630 \forall p11,p21:nat \to bool.
1631 \forall p12,p22:nat \to nat \to bool.
1632 (\forall x,y. x < n \to y < m \to
1633 (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
1635 (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA)
1638 (\lambda y:nat.iter_p_gen n (p22 y) A (\lambda x. g x y) baseA plusA )
1641 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)
1642 n m m n p11 p21 p12 p22)
1648 [apply (andb_true_true ? (p12 j i)).
1650 [rewrite > H6.rewrite > H7.reflexivity
1654 |apply (andb_true_true_r (p11 j)).
1656 [rewrite > H6.rewrite > H7.reflexivity
1674 [apply (andb_true_true ? (p22 j i)).
1676 [rewrite > H6.rewrite > H7.reflexivity
1680 |apply (andb_true_true_r (p21 j)).
1682 [rewrite > H6.rewrite > H7.reflexivity