]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/generic_iter_p.ma
...
[helm.git] / helm / software / matita / library / nat / generic_iter_p.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/div_and_mod_diseq.ma".
16 include "nat/primes.ma".
17 include "nat/ord.ma".
18
19 (*a generic definition of summatory indexed over natural numbers:
20  * n:N is the advanced end in the range of the sommatory 
21  * p: N -> bool is a predicate. if (p i) = true, then (g i) is summed, else it isn't 
22  * A is the type of the elements of the sum.
23  * g:nat -> A, is the function which associates the nth element of the sum to the nth natural numbers 
24  * baseA (of type A) is the neutral element of A for plusA operation
25  * plusA: A -> A -> A is the sum over elements in A. 
26  *)
27  
28 let rec iter_p_gen (n:nat) (p: nat \to bool) (A:Type) (g: nat \to A) 
29    (baseA: A) (plusA: A \to A \to A)  \def
30   match n with
31    [ O \Rightarrow baseA
32    | (S k) \Rightarrow 
33       match p k with
34       [true \Rightarrow (plusA (g k) (iter_p_gen k p A g baseA plusA))
35       |false \Rightarrow iter_p_gen k p A g baseA plusA]
36    ].
37    
38 theorem true_to_iter_p_gen_Sn: 
39 \forall n:nat. \forall p:nat \to bool. \forall A:Type. \forall g:nat \to A.
40 \forall baseA:A. \forall plusA: A \to A \to A.
41 p n = true \to iter_p_gen (S n) p A g baseA plusA = 
42 (plusA (g n) (iter_p_gen n p A g baseA plusA)).
43 intros.
44 simplify.
45 rewrite > H.
46 reflexivity.
47 qed.
48
49 theorem false_to_iter_p_gen_Sn: 
50 \forall n:nat. \forall p:nat \to bool. \forall A:Type. \forall g:nat \to A.
51 \forall baseA:A. \forall plusA: A \to A \to A.
52 p n = false \to iter_p_gen (S n) p A g baseA plusA = iter_p_gen n p A g baseA plusA.
53 intros.
54 simplify.
55 rewrite > H.
56 reflexivity.
57 qed.
58
59 theorem eq_iter_p_gen: \forall p1,p2:nat \to bool. \forall A:Type.
60 \forall g1,g2: nat \to A. \forall baseA: A. 
61 \forall plusA: A \to A \to A. \forall n:nat.
62 (\forall x.  x < n \to p1 x = p2 x) \to
63 (\forall x.  x < n \to g1 x = g2 x) \to
64 iter_p_gen n p1 A g1 baseA plusA = iter_p_gen n p2 A g2 baseA plusA.
65 intros 8.
66 elim n
67 [ reflexivity
68 | apply (bool_elim ? (p1 n1))
69   [ intro.
70     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
71     rewrite > true_to_iter_p_gen_Sn     
72     [ apply eq_f2
73       [ apply H2.apply le_n.
74       | apply H
75         [ intros.apply H1.apply le_S.assumption
76         | intros.apply H2.apply le_S.assumption
77         ]
78       ]
79     | rewrite < H3.apply sym_eq.apply H1.apply le_n
80     ]
81   | intro.
82     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
83     rewrite > false_to_iter_p_gen_Sn
84     [ apply H
85       [ intros.apply H1.apply le_S.assumption
86       | intros.apply H2.apply le_S.assumption
87       ]
88     | rewrite < H3.apply sym_eq.apply H1.apply le_n
89     ]
90   ]
91 ]
92 qed.
93
94 theorem eq_iter_p_gen1: \forall p1,p2:nat \to bool. \forall A:Type.
95 \forall g1,g2: nat \to A. \forall baseA: A. 
96 \forall plusA: A \to A \to A.\forall n:nat.
97 (\forall x.  x < n \to p1 x = p2 x) \to
98 (\forall x.  x < n \to p1 x = true \to g1 x = g2 x) \to
99 iter_p_gen n p1 A g1 baseA plusA = iter_p_gen n p2 A g2 baseA plusA.
100 intros 8.
101 elim n
102 [ reflexivity
103 | apply (bool_elim ? (p1 n1))
104   [ intro.
105     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
106     rewrite > true_to_iter_p_gen_Sn
107     [ apply eq_f2
108       [ apply H2
109         [ apply le_n
110         | assumption
111         ]
112       | apply H
113         [ intros.apply H1.apply le_S.assumption
114         | intros.apply H2
115           [ apply le_S.assumption
116           | assumption
117           ]
118         ]
119       ]
120     | rewrite < H3.
121       apply sym_eq.apply H1.apply le_n
122     ]
123   | intro.
124     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
125     rewrite > false_to_iter_p_gen_Sn
126     [ apply H
127       [ intros.apply H1.apply le_S.assumption
128       | intros.apply H2
129         [ apply le_S.assumption
130         | assumption
131         ]
132       ]
133     | rewrite < H3.apply sym_eq.
134       apply H1.apply le_n
135     ]
136   ]
137 ]
138 qed.
139
140 theorem iter_p_gen_false: \forall A:Type. \forall g: nat \to A. \forall baseA:A.
141 \forall plusA: A \to A \to A. \forall n.
142 iter_p_gen n (\lambda x.false) A g baseA plusA = baseA.
143 intros.
144 elim n
145 [ reflexivity
146 | simplify.
147   assumption
148 ]
149 qed.
150
151 theorem iter_p_gen_plusA: \forall A:Type. \forall n,k:nat.\forall p:nat \to bool.
152 \forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
153 (symmetric A plusA) \to (\forall a:A. (plusA a baseA) = a) \to (associative A plusA)
154 \to
155 iter_p_gen (k + n) p A g baseA plusA 
156 = (plusA (iter_p_gen k (\lambda x.p (x+n)) A (\lambda x.g (x+n)) baseA plusA)
157          (iter_p_gen n p A g baseA plusA)).
158 intros.
159
160 elim k
161 [ simplify.
162   rewrite > H in \vdash (? ? ? %).
163   rewrite > (H1 ?).
164   reflexivity
165 | apply (bool_elim ? (p (n1+n)))
166   [ intro.     
167     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
168     rewrite > (true_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4).
169     rewrite > (H2 (g (n1 + n)) ? ?).
170     rewrite < H3.
171     reflexivity
172   | intro.
173     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
174     rewrite > (false_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4).
175     assumption
176   ]
177 ]
178 qed.
179
180 theorem false_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool.
181 \forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A. 
182 n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false)
183 \to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA.
184 intros 8.
185 elim H
186 [ reflexivity
187 | simplify.
188   rewrite > H3
189   [ simplify.
190     apply H2.
191     intros.
192     apply H3
193     [ apply H4
194     | apply le_S.
195       assumption
196     ]
197   | assumption
198   |apply le_n
199   ]
200 ]
201 qed.
202
203 (* a therem slightly more general than the previous one *)
204 theorem or_false_eq_baseA_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool.
205 \forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
206 (\forall a. plusA baseA a = a) \to
207 n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = baseA)
208 \to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA.
209 intros 9.
210 elim H1
211 [reflexivity
212 |apply (bool_elim ? (p n1));intro
213   [elim (H4 n1)
214     [apply False_ind.
215      apply not_eq_true_false.
216      rewrite < H5.
217      rewrite < H6.
218      reflexivity
219     |rewrite > true_to_iter_p_gen_Sn
220       [rewrite > H6.
221        rewrite > H.
222        apply H3.intros.
223        apply H4
224         [assumption
225         |apply le_S.assumption
226         ]
227       |assumption
228       ]
229     |assumption
230     |apply le_n
231     ]
232   |rewrite > false_to_iter_p_gen_Sn
233     [apply H3.intros.
234      apply H4
235       [assumption
236       |apply le_S.assumption
237       ]
238     |assumption
239     ]
240   ]
241 ]
242 qed.
243     
244 theorem iter_p_gen2 : 
245 \forall n,m:nat.
246 \forall p1,p2:nat \to bool.
247 \forall A:Type.
248 \forall g: nat \to nat \to A.
249 \forall baseA: A.
250 \forall plusA: A \to A \to A.
251 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
252 \to
253 iter_p_gen (n*m) 
254   (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
255   A 
256   (\lambda x.g (div x m) (mod x m)) 
257   baseA
258   plusA  =
259 iter_p_gen n p1 A
260   (\lambda x.iter_p_gen m p2 A (g x) baseA plusA)
261   baseA plusA.
262 intros.
263 elim n
264 [ simplify.
265   reflexivity
266 | apply (bool_elim ? (p1 n1))
267   [ intro.
268     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
269     simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
270     rewrite > iter_p_gen_plusA
271     [ rewrite < H3.
272       apply eq_f2
273       [ apply eq_iter_p_gen
274         [ intros.
275           rewrite > sym_plus.
276           rewrite > (div_plus_times ? ? ? H5).
277           rewrite > (mod_plus_times ? ? ? H5).
278           rewrite > H4.
279           simplify.
280           reflexivity
281         | intros.
282           rewrite > sym_plus.
283           rewrite > (div_plus_times ? ? ? H5).
284           rewrite > (mod_plus_times ? ? ? H5).
285           reflexivity.   
286         ]
287       | reflexivity
288       ]
289     | assumption
290     | assumption
291     | assumption
292     ]
293   | intro.
294     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
295     simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
296     rewrite > iter_p_gen_plusA
297     [ rewrite > H3.
298       apply (trans_eq ? ? (plusA baseA
299            (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m p2 A (g x) baseA plusA) baseA plusA )))
300       [ apply eq_f2
301         [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
302           [ apply iter_p_gen_false
303           | intros.
304             rewrite > sym_plus.
305             rewrite > (div_plus_times ? ? ? H5).
306             rewrite > (mod_plus_times ? ? ? H5).
307             rewrite > H4.
308             simplify.reflexivity
309           | intros.reflexivity.
310           ]
311         | reflexivity
312         ]
313       | rewrite < H.
314         rewrite > H2.
315         reflexivity.  
316       ]
317     | assumption
318     | assumption
319     | assumption
320     ]
321   ]
322 ]
323 qed.
324
325 theorem iter_p_gen2': 
326 \forall n,m:nat.
327 \forall p1: nat \to bool.
328 \forall p2: nat \to nat \to bool.
329 \forall A:Type.
330 \forall g: nat \to nat \to A.
331 \forall baseA: A.
332 \forall plusA: A \to A \to A.
333 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
334 \to
335 iter_p_gen (n*m) 
336   (\lambda x.andb (p1 (div x m)) (p2 (div x m)(mod x m)))
337   A 
338   (\lambda x.g (div x m) (mod x m)) 
339   baseA
340   plusA  =
341 iter_p_gen n p1 A
342   (\lambda x.iter_p_gen m (p2 x) A (g x) baseA plusA)
343   baseA plusA.
344 intros.
345 elim n
346 [ simplify.
347   reflexivity
348 | apply (bool_elim ? (p1 n1))
349   [ intro.
350     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
351     simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
352     rewrite > iter_p_gen_plusA
353     [ rewrite < H3.
354       apply eq_f2
355       [ apply eq_iter_p_gen
356         [ intros.
357           rewrite > sym_plus.
358           rewrite > (div_plus_times ? ? ? H5).
359           rewrite > (mod_plus_times ? ? ? H5).
360           rewrite > H4.
361           simplify.
362           reflexivity
363         | intros.
364           rewrite > sym_plus.
365           rewrite > (div_plus_times ? ? ? H5).
366           rewrite > (mod_plus_times ? ? ? H5).
367           reflexivity.   
368         ]
369       | reflexivity
370       ]
371     | assumption
372     | assumption
373     | assumption
374     ]
375   | intro.
376     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
377     simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
378     rewrite > iter_p_gen_plusA
379     [ rewrite > H3.
380       apply (trans_eq ? ? (plusA baseA
381            (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m (p2 x) A (g x) baseA plusA) baseA plusA )))
382       [ apply eq_f2
383         [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
384           [ apply iter_p_gen_false
385           | intros.
386             rewrite > sym_plus.
387             rewrite > (div_plus_times ? ? ? H5).
388             rewrite > (mod_plus_times ? ? ? H5).
389             rewrite > H4.
390             simplify.reflexivity
391           | intros.reflexivity.
392           ]
393         | reflexivity
394         ]
395       | rewrite < H.
396         rewrite > H2.
397         reflexivity.  
398       ]
399     | assumption
400     | assumption
401     | assumption
402     ]
403   ]
404 ]
405 qed.
406
407 lemma iter_p_gen_gi: 
408 \forall A:Type.
409 \forall g: nat \to A.
410 \forall baseA:A.
411 \forall plusA: A \to A \to A.
412 \forall n,i:nat.
413 \forall p:nat \to bool.
414 (symmetric A plusA) \to  (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a) 
415   \to 
416   
417 i < n \to p i = true \to
418 (iter_p_gen n p A g baseA plusA) = 
419 (plusA (g i) (iter_p_gen n (\lambda x:nat. andb (p x) (notb (eqb x i))) A g baseA plusA)).
420 intros 5.
421 elim n
422 [ apply False_ind.
423   apply (not_le_Sn_O i).
424   assumption
425 | apply (bool_elim ? (p n1));intro
426   [ elim (le_to_or_lt_eq i n1)
427     [ rewrite > true_to_iter_p_gen_Sn
428       [ rewrite > true_to_iter_p_gen_Sn
429         [ rewrite < (H2 (g i) ? ?).
430           rewrite > (H1 (g i) (g n1)).
431           rewrite > (H2 (g n1) ? ?).
432           apply eq_f2
433           [ reflexivity
434           | apply H
435             [ assumption
436             | assumption
437             | assumption 
438             | assumption
439             | assumption
440             ]
441           ]
442         | rewrite > H6.simplify.
443           change with (notb (eqb n1 i) = notb false).
444           apply eq_f.
445           apply not_eq_to_eqb_false.
446           unfold Not.intro.
447           apply (lt_to_not_eq ? ? H7).
448           apply sym_eq.assumption
449         ]
450       | assumption
451       ]
452     | rewrite > true_to_iter_p_gen_Sn
453       [ rewrite > H7.
454         apply eq_f2
455         [ reflexivity
456         | rewrite > false_to_iter_p_gen_Sn
457           [ apply eq_iter_p_gen
458             [ intros.
459               elim (p x)
460               [ simplify.
461                 change with (notb false = notb (eqb x n1)).
462                 apply eq_f.
463                 apply sym_eq. 
464                 apply not_eq_to_eqb_false.
465                 apply (lt_to_not_eq ? ? H8)
466               | reflexivity
467               ]
468             | intros.
469               reflexivity
470             ]
471           | rewrite > H6.
472             rewrite > (eq_to_eqb_true ? ? (refl_eq ? n1)).
473             reflexivity
474           ]
475         ]
476       | assumption
477       ]
478     | apply le_S_S_to_le.
479       assumption
480     ]
481   | rewrite > false_to_iter_p_gen_Sn
482     [ elim (le_to_or_lt_eq i n1)
483       [ rewrite > false_to_iter_p_gen_Sn
484         [ apply H
485           [ assumption
486           | assumption
487           | assumption
488           | assumption
489           | assumption
490           ]
491         | rewrite > H6.reflexivity
492         ]
493       | apply False_ind. 
494         apply not_eq_true_false.
495         rewrite < H5.
496         rewrite > H7.
497         assumption
498       | apply le_S_S_to_le.
499         assumption
500       ]
501     | assumption
502     ]
503   ] 
504
505 qed.
506
507 (* invariance under permutation; single sum *)
508 theorem eq_iter_p_gen_gh: 
509 \forall A:Type.
510 \forall baseA: A.
511 \forall plusA: A \to A \to A.
512 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a) \to
513 \forall g: nat \to A.
514 \forall h,h1: nat \to nat.
515 \forall n,n1:nat.
516 \forall p1,p2:nat \to bool.
517 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
518 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to 
519 (\forall i. i < n \to p1 i = true \to h i < n1) \to 
520 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
521 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to 
522 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to 
523
524 iter_p_gen n p1 A (\lambda x.g(h x)) baseA plusA = 
525 iter_p_gen n1 p2 A g baseA plusA.
526 intros 10.
527 elim n
528 [ generalize in match H8.
529   elim n1
530   [ reflexivity
531   | apply (bool_elim ? (p2 n2));intro
532     [ apply False_ind.
533       apply (not_le_Sn_O (h1 n2)).
534       apply H10
535       [ apply le_n
536       | assumption
537       ]
538     | rewrite > false_to_iter_p_gen_Sn
539       [ apply H9.
540         intros.  
541         apply H10
542         [ apply le_S.
543           apply H12
544         | assumption
545         ]
546       | assumption
547       ]
548     ]
549   ]
550 | apply (bool_elim ? (p1 n1));intro
551   [ rewrite > true_to_iter_p_gen_Sn
552     [ rewrite > (iter_p_gen_gi A g baseA plusA n2 (h n1))
553       [ apply eq_f2
554         [ reflexivity
555         | apply H3
556           [ intros.
557             rewrite > H4
558             [ simplify.
559               change with ((\not eqb (h i) (h n1))= \not false).
560               apply eq_f.
561               apply not_eq_to_eqb_false.
562               unfold Not.
563               intro.
564               apply (lt_to_not_eq ? ? H11).
565               rewrite < H5
566               [ rewrite < (H5 n1)
567                 [ apply eq_f.
568                   assumption
569                 | apply le_n
570                 | assumption
571                 ]
572               | apply le_S.
573                 assumption
574               | assumption
575               ]
576             | apply le_S.assumption
577             | assumption
578             ]
579           | intros.
580             apply H5
581             [ apply le_S.
582               assumption
583             | assumption
584             ]
585           | intros.
586             apply H6
587             [ apply le_S.assumption
588             | assumption
589             ]
590           | intros.
591             apply H7
592             [ assumption
593             | generalize in match H12.
594               elim (p2 j)
595               [ reflexivity
596               | assumption
597               ]
598             ]
599           | intros.
600             apply H8
601             [ assumption
602             | generalize in match H12.
603               elim (p2 j)
604               [ reflexivity
605               | assumption
606               ]
607             ]
608           | intros.
609             elim (le_to_or_lt_eq (h1 j) n1)
610             [ assumption
611             | generalize in match H12.
612               elim (p2 j)
613               [ simplify in H13.
614                 absurd (j = (h n1))
615                 [ rewrite < H13.
616                   rewrite > H8
617                   [ reflexivity
618                   | assumption
619                   | autobatch
620                   ]
621                 | apply eqb_false_to_not_eq.
622                   generalize in match H14.
623                   elim (eqb j (h n1))
624                   [ apply sym_eq.assumption
625                   | reflexivity
626                   ]
627                 ]
628               | simplify in H14.
629                 apply False_ind.
630                 apply not_eq_true_false.
631                 apply sym_eq.assumption
632               ]
633             | apply le_S_S_to_le.
634               apply H9
635               [ assumption
636               | generalize in match H12.
637                 elim (p2 j)
638                 [ reflexivity
639                 | assumption
640                 ]
641               ]
642             ]
643           ]
644         ]
645       | assumption  
646       | assumption
647       | assumption  
648       | apply H6
649         [ apply le_n
650         | assumption
651         ]
652       | apply H4
653         [ apply le_n
654         | assumption
655         ]
656       ]
657     | assumption
658     ]
659   | rewrite > false_to_iter_p_gen_Sn
660     [ apply H3
661       [ intros.
662         apply H4[apply le_S.assumption|assumption]
663       | intros.
664         apply H5[apply le_S.assumption|assumption]
665       | intros.
666         apply H6[apply le_S.assumption|assumption]
667       | intros.
668         apply H7[assumption|assumption]
669       | intros.
670         apply H8[assumption|assumption]
671       | intros.
672         elim (le_to_or_lt_eq (h1 j) n1)
673         [ assumption
674         | absurd (j = (h n1))
675           [ rewrite < H13.
676             rewrite > H8
677             [ reflexivity
678             | assumption
679             | assumption
680             ]
681           | unfold Not.intro.
682             apply not_eq_true_false.
683             rewrite < H10.
684             rewrite < H13.
685             rewrite > H7
686             [ reflexivity
687             | assumption
688             | assumption
689             ]
690           ]
691         | apply le_S_S_to_le.
692           apply H9
693           [ assumption
694           | assumption
695           ]
696         ]
697       ]
698     | assumption
699     ]
700   ]
701 ]
702 qed.
703
704 theorem eq_iter_p_gen_pred: 
705 \forall A:Type.
706 \forall baseA: A.
707 \forall plusA: A \to A \to A.
708 \forall n,p,g.
709 p O = true \to
710 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a) \to
711 iter_p_gen (S n) (\lambda i.p (pred i)) A (\lambda i.g(pred i)) baseA plusA = 
712 plusA (iter_p_gen n p A g baseA plusA) (g O).
713 intros.
714 elim n
715   [rewrite > true_to_iter_p_gen_Sn
716     [simplify.apply H1
717     |assumption
718     ]
719   |apply (bool_elim ? (p n1));intro
720     [rewrite > true_to_iter_p_gen_Sn
721       [rewrite > true_to_iter_p_gen_Sn in âŠ¢ (? ? ? %)
722         [rewrite > H2 in âŠ¢ (? ? ? %).
723          apply eq_f.assumption
724         |assumption
725         ]
726       |assumption
727       ]
728     |rewrite > false_to_iter_p_gen_Sn
729       [rewrite > false_to_iter_p_gen_Sn in âŠ¢ (? ? ? %);assumption
730       |assumption
731       ]
732     ]
733   ]
734 qed.
735     
736 definition p_ord_times \def
737 \lambda p,m,x.
738   match p_ord x p with
739   [pair q r \Rightarrow r*m+q].
740   
741 theorem  eq_p_ord_times: \forall p,m,x.
742 p_ord_times p m x = (ord_rem x p)*m+(ord x p).
743 intros.unfold p_ord_times. unfold ord_rem.
744 unfold ord.
745 elim (p_ord x p).
746 reflexivity.
747 qed.
748
749 theorem div_p_ord_times: 
750 \forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
751 intros.rewrite > eq_p_ord_times.
752 apply div_plus_times.
753 assumption.
754 qed.
755
756 theorem mod_p_ord_times: 
757 \forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
758 intros.rewrite > eq_p_ord_times.
759 apply mod_plus_times.
760 assumption.
761 qed.
762
763 lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
764 intros.
765 elim (le_to_or_lt_eq O ? (le_O_n m))
766   [assumption
767   |apply False_ind.
768    rewrite < H1 in H.
769    rewrite < times_n_O in H.
770    apply (not_le_Sn_O ? H)
771   ]
772 qed.
773
774 theorem iter_p_gen_knm:
775 \forall A:Type.
776 \forall baseA: A.
777 \forall plusA: A \to A \to A. 
778 (symmetric A plusA) \to 
779 (associative A plusA) \to 
780 (\forall a:A.(plusA a  baseA) = a)\to
781 \forall g: nat \to A.
782 \forall h2:nat \to nat \to nat.
783 \forall h11,h12:nat \to nat. 
784 \forall k,n,m.
785 \forall p1,p21:nat \to bool.
786 \forall p22:nat \to nat \to bool.
787 (\forall x. x < k \to p1 x = true \to 
788 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
789 \land h2 (h11 x) (h12 x) = x 
790 \land (h11 x) < n \land (h12 x) < m) \to
791 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to 
792 p1 (h2 i j) = true \land 
793 h11 (h2 i j) = i \land h12 (h2 i j) = j
794 \land h2 i j < k) \to
795 iter_p_gen k p1 A g baseA plusA =
796 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.
797 intros.
798 rewrite < (iter_p_gen2' n m p21 p22 ? ? ? ? H H1 H2).
799 apply sym_eq.
800 apply (eq_iter_p_gen_gh A baseA plusA H H1 H2 g ? (\lambda x.(h11 x)*m+(h12 x)))
801  [intros.
802   elim (H4 (i/m) (i \mod m));clear H4
803    [elim H7.clear H7.
804     elim H4.clear H4.
805     assumption
806    |apply (lt_times_to_lt_div ? ? ? H5)
807    |apply lt_mod_m_m.
808     apply (lt_times_to_lt_O ? ? ? H5)
809    |apply (andb_true_true ? ? H6)
810    |apply (andb_true_true_r ? ? H6)
811    ]
812  |intros.
813   elim (H4 (i/m) (i \mod m));clear H4
814    [elim H7.clear H7.
815     elim H4.clear H4.
816     rewrite > H10.
817     rewrite > H9.
818     apply sym_eq.
819     apply div_mod.
820     apply (lt_times_to_lt_O ? ? ? H5)
821    |apply (lt_times_to_lt_div ? ? ? H5)
822    |apply lt_mod_m_m.
823     apply (lt_times_to_lt_O ? ? ? H5)  
824    |apply (andb_true_true ? ? H6)
825    |apply (andb_true_true_r ? ? H6)
826    ]
827  |intros.
828   elim (H4 (i/m) (i \mod m));clear H4
829    [elim H7.clear H7.
830     elim H4.clear H4.
831     assumption
832    |apply (lt_times_to_lt_div ? ? ? H5)
833    |apply lt_mod_m_m.
834     apply (lt_times_to_lt_O ? ? ? H5)
835    |apply (andb_true_true ? ? H6)
836    |apply (andb_true_true_r ? ? H6)
837    ]
838  |intros.
839   elim (H3 j H5 H6).
840   elim H7.clear H7.
841   elim H9.clear H9.
842   elim H7.clear H7.
843   rewrite > div_plus_times
844    [rewrite > mod_plus_times
845      [rewrite > H9.
846       rewrite > H12.
847       reflexivity.
848      |assumption
849      ]
850    |assumption
851    ]
852  |intros.
853   elim (H3 j H5 H6).
854   elim H7.clear H7.
855   elim H9.clear H9.
856   elim H7.clear H7. 
857   rewrite > div_plus_times
858    [rewrite > mod_plus_times
859      [assumption
860      |assumption
861      ]
862    |assumption
863    ]
864  |intros.
865   elim (H3 j H5 H6).
866   elim H7.clear H7.
867   elim H9.clear H9.
868   elim H7.clear H7. 
869   apply (lt_to_le_to_lt ? ((h11 j)*m+m))
870    [apply monotonic_lt_plus_r.
871     assumption
872    |rewrite > sym_plus.
873     change with ((S (h11 j)*m) \le n*m).
874     apply monotonic_le_times_l.
875     assumption
876    ]
877  ]
878 qed.
879
880 theorem iter_p_gen_divides:
881 \forall A:Type.
882 \forall baseA: A.
883 \forall plusA: A \to A \to A. 
884 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to 
885 \forall g: nat \to A.
886 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
887
888 \to
889
890 iter_p_gen (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) A g baseA plusA =
891 iter_p_gen (S n) (\lambda x.divides_b x n) A
892   (\lambda x.iter_p_gen (S m) (\lambda y.true) A (\lambda y.g (x*(exp p y))) baseA plusA) baseA plusA.
893 intros.
894 cut (O < p)
895   [rewrite < (iter_p_gen2 ? ? ? ? ? ? ? ? H3 H4 H5).
896    apply (trans_eq ? ? 
897     (iter_p_gen (S n*S m) (\lambda x:nat.divides_b (x/S m) n) A
898        (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m)))  baseA plusA) )
899     [apply sym_eq.
900      apply (eq_iter_p_gen_gh ? ? ? ? ? ? g ? (p_ord_times p (S m)))
901       [ assumption
902       | assumption
903       | assumption
904       |intros.
905        lapply (divides_b_true_to_lt_O ? ? H H7).
906        apply divides_to_divides_b_true
907         [rewrite > (times_n_O O).
908          apply lt_times
909           [assumption
910           |apply lt_O_exp.assumption
911           ]
912         |apply divides_times
913           [apply divides_b_true_to_divides.assumption
914           |apply (witness ? ? (p \sup (m-i \mod (S m)))).
915            rewrite < exp_plus_times.
916            apply eq_f.
917            rewrite > sym_plus.
918            apply plus_minus_m_m.
919            autobatch
920           ]
921         ]
922       |intros.
923        lapply (divides_b_true_to_lt_O ? ? H H7).
924        unfold p_ord_times.
925        rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
926         [change with ((i/S m)*S m+i \mod S m=i).
927          apply sym_eq.
928          apply div_mod.
929          apply lt_O_S
930         |assumption
931         |unfold Not.intro.
932          apply H2.
933          apply (trans_divides ? (i/ S m))
934           [assumption|
935            apply divides_b_true_to_divides;assumption]
936         |apply sym_times.
937         ]
938       |intros.
939        apply le_S_S.
940        apply le_times
941         [apply le_S_S_to_le.
942          change with ((i/S m) < S n).
943          apply (lt_times_to_lt_l m).
944          apply (le_to_lt_to_lt ? i)
945           [autobatch|assumption]
946         |apply le_exp
947           [assumption
948           |apply le_S_S_to_le.
949            apply lt_mod_m_m.
950            apply lt_O_S
951           ]
952         ]
953       |intros.
954        cut (ord j p < S m)
955         [rewrite > div_p_ord_times
956           [apply divides_to_divides_b_true
957             [apply lt_O_ord_rem
958              [elim H1.assumption
959              |apply (divides_b_true_to_lt_O ? ? ? H7).
960                rewrite > (times_n_O O).
961                apply lt_times
962                [assumption|apply lt_O_exp.assumption]
963              ]
964            |cut (n = ord_rem (n*(exp p m)) p)
965               [rewrite > Hcut2.
966                apply divides_to_divides_ord_rem
967                 [apply (divides_b_true_to_lt_O ? ? ? H7).
968                  rewrite > (times_n_O O).
969                  apply lt_times
970                  [assumption|apply lt_O_exp.assumption]
971                  |rewrite > (times_n_O O).
972                    apply lt_times
973                   [assumption|apply lt_O_exp.assumption]
974                |assumption
975                |apply divides_b_true_to_divides.
976                 assumption
977                ]
978               |unfold ord_rem.
979               rewrite > (p_ord_exp1 p ? m n)
980                 [reflexivity
981                |assumption
982                 |assumption
983                |apply sym_times
984                ]
985              ]
986             ]
987           |assumption
988           ]
989         |cut (m = ord (n*(exp p m)) p)
990           [apply le_S_S.
991            rewrite > Hcut1.
992            apply divides_to_le_ord
993             [apply (divides_b_true_to_lt_O ? ? ? H7).
994              rewrite > (times_n_O O).
995              apply lt_times
996               [assumption|apply lt_O_exp.assumption]
997             |rewrite > (times_n_O O).
998              apply lt_times
999               [assumption|apply lt_O_exp.assumption]
1000             |assumption
1001             |apply divides_b_true_to_divides.
1002              assumption
1003             ]
1004           |unfold ord.
1005            rewrite > (p_ord_exp1 p ? m n)
1006             [reflexivity
1007             |assumption
1008             |assumption
1009             |apply sym_times
1010             ]
1011           ]
1012         ]
1013       |intros.
1014        cut (ord j p < S m)
1015         [rewrite > div_p_ord_times
1016           [rewrite > mod_p_ord_times
1017             [rewrite > sym_times.
1018              apply sym_eq.
1019              apply exp_ord
1020               [elim H1.assumption
1021               |apply (divides_b_true_to_lt_O ? ? ? H7).
1022                rewrite > (times_n_O O).
1023                apply lt_times
1024                 [assumption|apply lt_O_exp.assumption]
1025               ]
1026            |cut (m = ord (n*(exp p m)) p)
1027              [apply le_S_S.
1028               rewrite > Hcut2.
1029               apply divides_to_le_ord
1030                [apply (divides_b_true_to_lt_O ? ? ? H7).
1031                 rewrite > (times_n_O O).
1032                 apply lt_times
1033                  [assumption|apply lt_O_exp.assumption]
1034                |rewrite > (times_n_O O).
1035                 apply lt_times
1036                  [assumption|apply lt_O_exp.assumption]
1037                |assumption
1038                |apply divides_b_true_to_divides.
1039                 assumption
1040                ]
1041              |unfold ord.
1042               rewrite > (p_ord_exp1 p ? m n)
1043                 [reflexivity
1044                 |assumption
1045                 |assumption
1046                 |apply sym_times
1047                 ]
1048               ]
1049             ]
1050           |assumption
1051           ]
1052         |cut (m = ord (n*(exp p m)) p)
1053           [apply le_S_S.
1054            rewrite > Hcut1.
1055            apply divides_to_le_ord
1056             [apply (divides_b_true_to_lt_O ? ? ? H7).
1057              rewrite > (times_n_O O).
1058              apply lt_times
1059               [assumption|apply lt_O_exp.assumption]
1060             |rewrite > (times_n_O O).
1061              apply lt_times
1062               [assumption|apply lt_O_exp.assumption]
1063             |assumption
1064             |apply divides_b_true_to_divides.
1065              assumption
1066             ]
1067           |unfold ord.
1068            rewrite > (p_ord_exp1 p ? m n)
1069             [reflexivity
1070             |assumption
1071             |assumption
1072             |apply sym_times
1073             ]
1074           ]
1075         ]
1076       |intros.
1077        rewrite > eq_p_ord_times.
1078        rewrite > sym_plus.
1079        apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
1080         [apply lt_plus_l.
1081          apply le_S_S.
1082          cut (m = ord (n*(p \sup m)) p)
1083           [rewrite > Hcut1.
1084            apply divides_to_le_ord
1085             [apply (divides_b_true_to_lt_O ? ? ? H7).
1086              rewrite > (times_n_O O).
1087              apply lt_times
1088               [assumption|apply lt_O_exp.assumption]
1089             |rewrite > (times_n_O O).
1090              apply lt_times
1091               [assumption|apply lt_O_exp.assumption]
1092             |assumption
1093             |apply divides_b_true_to_divides.
1094              assumption
1095             ]
1096           |unfold ord.
1097            rewrite > sym_times.
1098            rewrite > (p_ord_exp1 p ? m n)
1099             [reflexivity
1100             |assumption
1101             |assumption
1102             |reflexivity
1103             ]
1104           ]
1105         |change with (S (ord_rem j p)*S m \le S n*S m).
1106          apply le_times_l.
1107          apply le_S_S.
1108          cut (n = ord_rem (n*(p \sup m)) p)
1109           [rewrite > Hcut1.
1110            apply divides_to_le
1111             [apply lt_O_ord_rem
1112               [elim H1.assumption
1113               |rewrite > (times_n_O O).
1114                apply lt_times
1115                 [assumption|apply lt_O_exp.assumption]
1116               ]
1117             |apply divides_to_divides_ord_rem
1118               [apply (divides_b_true_to_lt_O ? ? ? H7).
1119                rewrite > (times_n_O O).
1120                apply lt_times
1121                 [assumption|apply lt_O_exp.assumption]
1122               |rewrite > (times_n_O O).
1123                apply lt_times
1124                 [assumption|apply lt_O_exp.assumption]
1125               |assumption
1126               |apply divides_b_true_to_divides.
1127                assumption
1128               ]
1129             ]
1130         |unfold ord_rem.
1131          rewrite > sym_times.
1132          rewrite > (p_ord_exp1 p ? m n)
1133           [reflexivity
1134           |assumption
1135           |assumption
1136           |reflexivity
1137           ]
1138         ]
1139       ]
1140     ]
1141   |apply eq_iter_p_gen
1142   
1143     [intros.
1144      elim (divides_b (x/S m) n);reflexivity
1145     |intros.reflexivity
1146     ]
1147   ]
1148 |elim H1.apply lt_to_le.assumption
1149 ]
1150 qed.
1151     
1152 (*distributive property for iter_p_gen*)
1153 theorem distributive_times_plus_iter_p_gen: \forall A:Type.
1154 \forall plusA: A \to A \to A. \forall basePlusA: A.
1155 \forall timesA: A \to A \to A. 
1156 \forall n:nat. \forall k:A. \forall p:nat \to bool. \forall g:nat \to A.
1157 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  basePlusA) = a) \to
1158 (symmetric A timesA) \to (distributive A timesA plusA) \to
1159 (\forall a:A. (timesA a basePlusA) = basePlusA)
1160  
1161   \to
1162
1163 ((timesA k (iter_p_gen n p A g basePlusA plusA)) = 
1164  (iter_p_gen n p A (\lambda i:nat.(timesA k (g i))) basePlusA plusA)).
1165 intros.
1166 elim n
1167 [ simplify.
1168   apply H5
1169 | cut( (p n1) = true \lor (p n1) = false)
1170   [ elim Hcut
1171     [ rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
1172       rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
1173       rewrite > (H4).
1174       rewrite > (H3 k (g n1)).
1175       apply eq_f.
1176       assumption
1177     | rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
1178       rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
1179       assumption
1180     ]
1181   | elim ((p n1))
1182     [ left.
1183       reflexivity
1184     | right.
1185       reflexivity
1186     ]
1187   ]
1188 ]
1189 qed.
1190
1191 (* old version - proved without theorem iter_p_gen_knm
1192 theorem iter_p_gen_2_eq: 
1193 \forall A:Type.
1194 \forall baseA: A.
1195 \forall plusA: A \to A \to A. 
1196 (symmetric A plusA) \to 
1197 (associative A plusA) \to 
1198 (\forall a:A.(plusA a  baseA) = a)\to
1199 \forall g: nat \to nat \to A.
1200 \forall h11,h12,h21,h22: nat \to nat \to nat. 
1201 \forall n1,m1,n2,m2.
1202 \forall p11,p21:nat \to bool.
1203 \forall p12,p22:nat \to nat \to bool.
1204 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to 
1205 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
1206 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
1207 \land h11 i j < n1 \land h12 i j < m1) \to
1208 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to 
1209 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
1210 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
1211 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
1212 iter_p_gen n1 p11 A 
1213      (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA) 
1214      baseA plusA =
1215 iter_p_gen n2 p21 A 
1216     (\lambda x:nat .iter_p_gen m2 (p22 x) A  (\lambda y. g (h11 x y) (h12 x y)) baseA plusA )
1217     baseA plusA.
1218 intros.
1219 rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
1220 rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
1221 apply sym_eq.
1222 letin h := (\lambda x.(h11 (x/m2) (x\mod m2))*m1 + (h12 (x/m2) (x\mod m2))).
1223 letin h1 := (\lambda x.(h21 (x/m1) (x\mod m1))*m2 + (h22 (x/m1) (x\mod m1))).
1224 apply (trans_eq ? ? 
1225   (iter_p_gen (n2*m2) (\lambda x:nat.p21 (x/m2)\land p22 (x/m2) (x\mod m2)) A
1226   (\lambda x:nat.g ((h x)/m1) ((h x)\mod m1)) baseA plusA ))
1227   [clear h.clear h1.
1228    apply eq_iter_p_gen1
1229     [intros.reflexivity
1230     |intros.
1231      cut (O < m2)
1232       [cut (x/m2 < n2)
1233         [cut (x \mod m2 < m2)
1234           [elim (and_true ? ? H6).
1235            elim (H3 ? ? Hcut1 Hcut2 H7 H8).
1236            elim H9.clear H9.
1237            elim H11.clear H11.
1238            elim H9.clear H9.
1239            elim H11.clear H11.
1240            apply eq_f2
1241             [apply sym_eq.
1242              apply div_plus_times.
1243              assumption
1244             | apply sym_eq.
1245               apply mod_plus_times.
1246               assumption
1247             ]
1248           |apply lt_mod_m_m.
1249            assumption
1250           ]
1251         |apply (lt_times_n_to_lt m2)
1252           [assumption
1253           |apply (le_to_lt_to_lt ? x)
1254             [apply (eq_plus_to_le ? ? (x \mod m2)).
1255              apply div_mod.
1256              assumption
1257             |assumption
1258             ]
1259           ]
1260         ]
1261       |apply not_le_to_lt.unfold.intro.
1262        generalize in match H5.
1263        apply (le_n_O_elim ? H7).
1264        rewrite < times_n_O.
1265        apply le_to_not_lt.
1266        apply le_O_n  
1267       ]      
1268     ]
1269   |apply (eq_iter_p_gen_gh ? ? ? H H1 H2 ? h h1);intros
1270     [cut (O < m2)
1271       [cut (i/m2 < n2)
1272         [cut (i \mod m2 < m2)
1273           [elim (and_true ? ? H6).
1274            elim (H3 ? ? Hcut1 Hcut2 H7 H8).
1275            elim H9.clear H9.
1276            elim H11.clear H11.
1277            elim H9.clear H9.
1278            elim H11.clear H11.
1279            cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 = 
1280                  h11 (i/m2) (i\mod m2))
1281             [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
1282                   h12 (i/m2) (i\mod m2))
1283               [rewrite > Hcut3.
1284                rewrite > Hcut4.
1285                rewrite > H9.
1286                rewrite > H15.
1287                reflexivity
1288               |apply mod_plus_times. 
1289                assumption
1290               ]
1291             |apply div_plus_times.
1292              assumption
1293             ]
1294           |apply lt_mod_m_m.
1295            assumption
1296           ]
1297         |apply (lt_times_n_to_lt m2)
1298           [assumption
1299           |apply (le_to_lt_to_lt ? i)
1300             [apply (eq_plus_to_le ? ? (i \mod m2)).
1301              apply div_mod.
1302              assumption
1303             |assumption
1304             ]
1305           ]
1306         ]
1307       |apply not_le_to_lt.unfold.intro.
1308        generalize in match H5.
1309        apply (le_n_O_elim ? H7).
1310        rewrite < times_n_O.
1311        apply le_to_not_lt.
1312        apply le_O_n  
1313       ]      
1314     |cut (O < m2)
1315       [cut (i/m2 < n2)
1316         [cut (i \mod m2 < m2)
1317           [elim (and_true ? ? H6).
1318            elim (H3 ? ? Hcut1 Hcut2 H7 H8).
1319            elim H9.clear H9.
1320            elim H11.clear H11.
1321            elim H9.clear H9.
1322            elim H11.clear H11.
1323            cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 = 
1324                  h11 (i/m2) (i\mod m2))
1325             [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
1326                   h12 (i/m2) (i\mod m2))
1327               [rewrite > Hcut3.
1328                rewrite > Hcut4.
1329                rewrite > H13.
1330                rewrite > H14.
1331                apply sym_eq.
1332                apply div_mod.
1333                assumption
1334               |apply mod_plus_times. 
1335                assumption
1336               ]
1337             |apply div_plus_times.
1338              assumption
1339             ]
1340           |apply lt_mod_m_m.
1341            assumption
1342           ]
1343         |apply (lt_times_n_to_lt m2)
1344           [assumption
1345           |apply (le_to_lt_to_lt ? i)
1346             [apply (eq_plus_to_le ? ? (i \mod m2)).
1347              apply div_mod.
1348              assumption
1349             |assumption
1350             ]
1351           ]
1352         ]
1353       |apply not_le_to_lt.unfold.intro.
1354        generalize in match H5.
1355        apply (le_n_O_elim ? H7).
1356        rewrite < times_n_O.
1357        apply le_to_not_lt.
1358        apply le_O_n  
1359       ]      
1360     |cut (O < m2)
1361       [cut (i/m2 < n2)
1362         [cut (i \mod m2 < m2)
1363           [elim (and_true ? ? H6).
1364            elim (H3 ? ? Hcut1 Hcut2 H7 H8).
1365            elim H9.clear H9.
1366            elim H11.clear H11.
1367            elim H9.clear H9.
1368            elim H11.clear H11.
1369            apply lt_times_plus_times
1370             [assumption|assumption]
1371           |apply lt_mod_m_m.
1372            assumption
1373           ]
1374         |apply (lt_times_n_to_lt m2)
1375           [assumption
1376           |apply (le_to_lt_to_lt ? i)
1377             [apply (eq_plus_to_le ? ? (i \mod m2)).
1378              apply div_mod.
1379              assumption
1380             |assumption
1381             ]
1382           ]
1383         ]
1384       |apply not_le_to_lt.unfold.intro.
1385        generalize in match H5.
1386        apply (le_n_O_elim ? H7).
1387        rewrite < times_n_O.
1388        apply le_to_not_lt.
1389        apply le_O_n  
1390       ]
1391     |cut (O < m1)
1392       [cut (j/m1 < n1)
1393         [cut (j \mod m1 < m1)
1394           [elim (and_true ? ? H6).
1395            elim (H4 ? ? Hcut1 Hcut2 H7 H8).
1396            elim H9.clear H9.
1397            elim H11.clear H11.
1398            elim H9.clear H9.
1399            elim H11.clear H11.
1400            cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 = 
1401                  h21 (j/m1) (j\mod m1))
1402             [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
1403                   h22 (j/m1) (j\mod m1))
1404               [rewrite > Hcut3.
1405                rewrite > Hcut4.
1406                rewrite > H9.
1407                rewrite > H15.
1408                reflexivity
1409               |apply mod_plus_times. 
1410                assumption
1411               ]
1412             |apply div_plus_times.
1413              assumption
1414             ]
1415           |apply lt_mod_m_m.
1416            assumption
1417           ] 
1418         |apply (lt_times_n_to_lt m1)
1419           [assumption
1420           |apply (le_to_lt_to_lt ? j)
1421             [apply (eq_plus_to_le ? ? (j \mod m1)).
1422              apply div_mod.
1423              assumption
1424             |assumption
1425             ]
1426           ]
1427         ]
1428       |apply not_le_to_lt.unfold.intro.
1429        generalize in match H5.
1430        apply (le_n_O_elim ? H7).
1431        rewrite < times_n_O.
1432        apply le_to_not_lt.
1433        apply le_O_n  
1434       ] 
1435     |cut (O < m1)
1436       [cut (j/m1 < n1)
1437         [cut (j \mod m1 < m1)
1438           [elim (and_true ? ? H6).
1439            elim (H4 ? ? Hcut1 Hcut2 H7 H8).
1440            elim H9.clear H9.
1441            elim H11.clear H11.
1442            elim H9.clear H9.
1443            elim H11.clear H11.
1444            cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 = 
1445                  h21 (j/m1) (j\mod m1))
1446             [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
1447                   h22 (j/m1) (j\mod m1))
1448               [rewrite > Hcut3.
1449                rewrite > Hcut4.               
1450                rewrite > H13.
1451                rewrite > H14.
1452                apply sym_eq.
1453                apply div_mod.
1454                assumption
1455               |apply mod_plus_times. 
1456                assumption
1457               ]
1458             |apply div_plus_times.
1459              assumption
1460             ]
1461           |apply lt_mod_m_m.
1462            assumption
1463           ] 
1464         |apply (lt_times_n_to_lt m1)
1465           [assumption
1466           |apply (le_to_lt_to_lt ? j)
1467             [apply (eq_plus_to_le ? ? (j \mod m1)).
1468              apply div_mod.
1469              assumption
1470             |assumption
1471             ]
1472           ]
1473         ]
1474       |apply not_le_to_lt.unfold.intro.
1475        generalize in match H5.
1476        apply (le_n_O_elim ? H7).
1477        rewrite < times_n_O.
1478        apply le_to_not_lt.
1479        apply le_O_n  
1480       ] 
1481     |cut (O < m1)
1482       [cut (j/m1 < n1)
1483         [cut (j \mod m1 < m1)
1484           [elim (and_true ? ? H6).
1485            elim (H4 ? ? Hcut1 Hcut2 H7 H8).
1486            elim H9.clear H9.
1487            elim H11.clear H11.
1488            elim H9.clear H9.
1489            elim H11.clear H11.
1490            apply (lt_times_plus_times ? ? ? m2)
1491             [assumption|assumption]
1492           |apply lt_mod_m_m.
1493            assumption
1494           ] 
1495         |apply (lt_times_n_to_lt m1)
1496           [assumption
1497           |apply (le_to_lt_to_lt ? j)
1498             [apply (eq_plus_to_le ? ? (j \mod m1)).
1499              apply div_mod.
1500              assumption
1501             |assumption
1502             ]
1503           ]
1504         ]
1505       |apply not_le_to_lt.unfold.intro.
1506        generalize in match H5.
1507        apply (le_n_O_elim ? H7).
1508        rewrite < times_n_O.
1509        apply le_to_not_lt.
1510        apply le_O_n  
1511       ]
1512     ]
1513   ]
1514 qed.*)
1515
1516
1517 theorem iter_p_gen_2_eq: 
1518 \forall A:Type.
1519 \forall baseA: A.
1520 \forall plusA: A \to A \to A. 
1521 (symmetric A plusA) \to 
1522 (associative A plusA) \to 
1523 (\forall a:A.(plusA a  baseA) = a)\to
1524 \forall g: nat \to nat \to A.
1525 \forall h11,h12,h21,h22: nat \to nat \to nat. 
1526 \forall n1,m1,n2,m2.
1527 \forall p11,p21:nat \to bool.
1528 \forall p12,p22:nat \to nat \to bool.
1529 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to 
1530 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
1531 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
1532 \land h11 i j < n1 \land h12 i j < m1) \to
1533 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to 
1534 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
1535 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
1536 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
1537 iter_p_gen n1 p11 A 
1538      (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA) 
1539      baseA plusA =
1540 iter_p_gen n2 p21 A 
1541     (\lambda x:nat .iter_p_gen m2 (p22 x) A  (\lambda y. g (h11 x y) (h12 x y)) baseA plusA )
1542     baseA plusA.
1543
1544 intros.
1545 rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
1546 letin ha:= (\lambda x,y.(((h11 x y)*m1) + (h12 x y))).
1547 letin ha12:= (\lambda x.(h21 (x/m1) (x \mod m1))).
1548 letin ha22:= (\lambda x.(h22 (x/m1) (x \mod m1))).
1549
1550 apply (trans_eq ? ? 
1551 (iter_p_gen n2 p21 A (\lambda x:nat. iter_p_gen m2 (p22 x) A
1552  (\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))
1553 [
1554   apply (iter_p_gen_knm A baseA plusA H H1 H2 (\lambda e. (g (e/m1) (e \mod m1))) ha ha12 ha22);intros
1555   [ elim (and_true ? ? H6).
1556     cut(O \lt m1)
1557     [ cut(x/m1 < n1)
1558       [ cut((x \mod m1) < m1)
1559         [ elim (H4 ? ? Hcut1 Hcut2 H7 H8).
1560           elim H9.clear H9.
1561           elim H11.clear H11.
1562           elim H9.clear H9.
1563           elim H11.clear H11.
1564           split
1565           [ split
1566             [ split
1567               [ split
1568                 [ assumption
1569                 | assumption
1570                 ]
1571               | unfold ha.
1572                 unfold ha12.
1573                 unfold ha22.
1574                 rewrite > H14.
1575                 rewrite > H13.
1576                 apply sym_eq.
1577                 apply div_mod.
1578                 assumption
1579               ]
1580             | assumption
1581             ]
1582           | assumption
1583           ]
1584         | apply lt_mod_m_m.
1585           assumption
1586         ]
1587       | apply (lt_times_n_to_lt m1)
1588         [ assumption
1589         | apply (le_to_lt_to_lt ? x)
1590           [ apply (eq_plus_to_le ? ? (x \mod m1)).
1591             apply div_mod.
1592             assumption
1593           | assumption
1594         ]
1595       ]  
1596     ]
1597     | apply not_le_to_lt.unfold.intro.
1598       generalize in match H5.
1599       apply (le_n_O_elim ? H9).
1600       rewrite < times_n_O.
1601       apply le_to_not_lt.
1602       apply le_O_n.              
1603     ]
1604   | elim (H3 ? ? H5 H6 H7 H8).
1605     elim H9.clear H9.
1606     elim H11.clear H11.
1607     elim H9.clear H9.
1608     elim H11.clear H11.
1609     cut(((h11 i j)*m1 + (h12 i j))/m1 = (h11 i j))
1610     [ cut(((h11 i j)*m1 + (h12 i j)) \mod m1 = (h12 i j))
1611       [ split
1612         [ split
1613           [ split
1614             [ apply true_to_true_to_andb_true
1615               [ rewrite > Hcut.
1616                 assumption
1617               | rewrite > Hcut1.
1618                 rewrite > Hcut.
1619                 assumption
1620               ] 
1621             | unfold ha.
1622               unfold ha12.
1623               rewrite > Hcut1.
1624               rewrite > Hcut.
1625               assumption
1626             ]
1627           | unfold ha.
1628             unfold ha22.
1629             rewrite > Hcut1.
1630             rewrite > Hcut.
1631             assumption            
1632           ]
1633         | cut(O \lt m1)
1634           [ cut(O \lt n1)      
1635             [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
1636               [ unfold ha.
1637                 apply (lt_plus_r).
1638                 assumption
1639               | rewrite > sym_plus.
1640                 rewrite > (sym_times (h11 i j) m1).
1641                 rewrite > times_n_Sm.
1642                 rewrite > sym_times.
1643                 apply (le_times_l).
1644                 assumption  
1645               ]
1646             | apply not_le_to_lt.unfold.intro.
1647               generalize in match H12.
1648               apply (le_n_O_elim ? H11).       
1649               apply le_to_not_lt.
1650               apply le_O_n
1651             ]
1652           | apply not_le_to_lt.unfold.intro.
1653             generalize in match H10.
1654             apply (le_n_O_elim ? H11).       
1655             apply le_to_not_lt.
1656             apply le_O_n
1657           ]  
1658         ]
1659       | rewrite > (mod_plus_times m1 (h11 i j) (h12 i j)).
1660         reflexivity.
1661         assumption
1662       ]     
1663     | rewrite > (div_plus_times m1 (h11 i j) (h12 i j)).
1664       reflexivity.
1665       assumption
1666     ]
1667   ]
1668 | apply (eq_iter_p_gen1)
1669   [ intros. reflexivity 
1670   | intros.
1671     apply (eq_iter_p_gen1)
1672     [ intros. reflexivity
1673     | intros.
1674       rewrite > (div_plus_times)
1675       [ rewrite > (mod_plus_times)
1676         [ reflexivity
1677         | elim (H3 x x1 H5 H7 H6 H8).
1678           assumption
1679         ]
1680       | elim (H3 x x1 H5 H7 H6 H8).       
1681         assumption
1682       ]
1683     ]
1684   ]
1685 ]
1686 qed.
1687
1688 theorem iter_p_gen_iter_p_gen: 
1689 \forall A:Type.
1690 \forall baseA: A.
1691 \forall plusA: A \to A \to A. 
1692 (symmetric A plusA) \to 
1693 (associative A plusA) \to 
1694 (\forall a:A.(plusA a  baseA) = a)\to
1695 \forall g: nat \to nat \to A.
1696 \forall n,m.
1697 \forall p11,p21:nat \to bool.
1698 \forall p12,p22:nat \to nat \to bool.
1699 (\forall x,y. x < n \to y < m \to 
1700  (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
1701 iter_p_gen n p11 A 
1702   (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA) 
1703   baseA plusA =
1704 iter_p_gen m p21 A 
1705   (\lambda y:nat.iter_p_gen n (p22 y) A  (\lambda x. g x y) baseA plusA )
1706   baseA plusA.
1707 intros.
1708 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)
1709        n m m n p11 p21 p12 p22)
1710   [intros.split
1711     [split
1712       [split
1713         [split
1714           [split
1715             [apply (andb_true_true ? (p12 j i)).
1716              rewrite > H3
1717               [rewrite > H6.rewrite > H7.reflexivity
1718               |assumption
1719               |assumption
1720               ]
1721             |apply (andb_true_true_r (p11 j)).
1722              rewrite > H3
1723               [rewrite > H6.rewrite > H7.reflexivity
1724               |assumption
1725               |assumption
1726               ]
1727             ]
1728           |reflexivity
1729           ]
1730         |reflexivity
1731         ]
1732       |assumption
1733       ]
1734     |assumption
1735     ]
1736   |intros.split
1737     [split
1738       [split
1739         [split
1740           [split
1741             [apply (andb_true_true ? (p22 j i)).
1742              rewrite < H3
1743               [rewrite > H6.rewrite > H7.reflexivity
1744               |assumption
1745               |assumption
1746               ]
1747             |apply (andb_true_true_r (p21 j)).
1748              rewrite < H3
1749               [rewrite > H6.rewrite > H7.reflexivity
1750               |assumption
1751               |assumption
1752               ]
1753             ]
1754           |reflexivity
1755           ]
1756         |reflexivity
1757         ]
1758       |assumption
1759       ]
1760     |assumption
1761     ]
1762   ]
1763 qed.