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