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