]> matita.cs.unibo.it Git - helm.git/blob - matita/library/nat/generic_iter_p.ma
fixed propagation under Fix/Lambda/Case of coercions, better names are
[helm.git] / 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.ma".
16
17 include "nat/primes.ma".
18 include "nat/ord.ma".
19
20
21
22 (*a generic definition of summatory indexed over natural numbers:
23  * n:N is the advanced end in the range of the sommatory 
24  * p: N -> bool is a predicate. if (p i) = true, then (g i) is summed, else it isn't 
25  * A is the type of the elements of the sum.
26  * g:nat -> A, is the function which associates the nth element of the sum to the nth natural numbers 
27  * baseA (of type A) is the neutral element of A for plusA operation
28  * plusA: A -> A -> A is the sum over elements in A. 
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
52
53 theorem false_to_iter_p_gen_Sn: 
54 \forall n:nat. \forall p:nat \to bool. \forall A:Type. \forall g:nat \to A.
55 \forall baseA:A. \forall plusA: A \to A \to A.
56 p n = false \to iter_p_gen (S n) p A g baseA plusA = iter_p_gen n p A g baseA plusA.
57 intros.
58 simplify.
59 rewrite > H.
60 reflexivity.
61 qed.
62
63
64 theorem eq_iter_p_gen: \forall p1,p2:nat \to bool. \forall A:Type.
65 \forall g1,g2: nat \to A. \forall baseA: A. 
66 \forall plusA: A \to A \to A. \forall n:nat.
67 (\forall x.  x < n \to p1 x = p2 x) \to
68 (\forall x.  x < n \to g1 x = g2 x) \to
69 iter_p_gen n p1 A g1 baseA plusA = iter_p_gen n p2 A g2 baseA plusA.
70 intros 8.
71 elim n
72 [ reflexivity
73 | apply (bool_elim ? (p1 n1))
74   [ intro.
75     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
76     rewrite > true_to_iter_p_gen_Sn     
77     [ apply eq_f2
78       [ apply H2.apply le_n.
79       | apply H
80         [ intros.apply H1.apply le_S.assumption
81         | intros.apply H2.apply le_S.assumption
82         ]
83       ]
84     | rewrite < H3.apply sym_eq.apply H1.apply le_n
85     ]
86   | intro.
87     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
88     rewrite > false_to_iter_p_gen_Sn
89     [ apply H
90       [ intros.apply H1.apply le_S.assumption
91       | intros.apply H2.apply le_S.assumption
92       ]
93     | rewrite < H3.apply sym_eq.apply H1.apply le_n
94     ]
95   ]
96 ]
97 qed.
98
99 theorem eq_iter_p_gen1: \forall p1,p2:nat \to bool. \forall A:Type.
100 \forall g1,g2: nat \to A. \forall baseA: A. 
101 \forall plusA: A \to A \to A.\forall n:nat.
102 (\forall x.  x < n \to p1 x = p2 x) \to
103 (\forall x.  x < n \to p1 x = true \to g1 x = g2 x) \to
104 iter_p_gen n p1 A g1 baseA plusA = iter_p_gen n p2 A g2 baseA plusA.
105 intros 8.
106 elim n
107 [ reflexivity
108 | apply (bool_elim ? (p1 n1))
109   [ intro.
110     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
111     rewrite > true_to_iter_p_gen_Sn
112     [ apply eq_f2
113       [ apply H2
114         [ apply le_n
115         | assumption
116         ]
117       | apply H
118         [ intros.apply H1.apply le_S.assumption
119         | intros.apply H2
120           [ apply le_S.assumption
121           | assumption
122           ]
123         ]
124       ]
125     | rewrite < H3.
126       apply sym_eq.apply H1.apply le_n
127     ]
128   | intro.
129     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
130     rewrite > false_to_iter_p_gen_Sn
131     [ apply H
132       [ intros.apply H1.apply le_S.assumption
133       | intros.apply H2
134         [ apply le_S.assumption
135         | assumption
136         ]
137       ]
138     | rewrite < H3.apply sym_eq.
139       apply H1.apply le_n
140     ]
141   ]
142 ]
143 qed.
144
145 theorem iter_p_gen_false: \forall A:Type. \forall g: nat \to A. \forall baseA:A.
146 \forall plusA: A \to A \to A. \forall n.
147 iter_p_gen n (\lambda x.false) A g baseA plusA = baseA.
148 intros.
149 elim n
150 [ reflexivity
151 | simplify.
152   assumption
153 ]
154 qed.
155
156 theorem iter_p_gen_plusA: \forall A:Type. \forall n,k:nat.\forall p:nat \to bool.
157 \forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
158 (symmetric A plusA) \to (\forall a:A. (plusA a baseA) = a) \to (associative A plusA)
159 \to
160 iter_p_gen (k + n) p A g baseA plusA 
161 = (plusA (iter_p_gen k (\lambda x.p (x+n)) A (\lambda x.g (x+n)) baseA plusA)
162          (iter_p_gen n p A g baseA plusA)).
163 intros.
164
165 elim k
166 [ rewrite < (plus_n_O n).
167   simplify.
168   rewrite > H in \vdash (? ? ? %).
169   rewrite > (H1 ?).
170   reflexivity
171 | apply (bool_elim ? (p (n1+n)))
172   [ intro.     
173     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
174     rewrite > (true_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4).
175     rewrite > (H2 (g (n1 + n)) ? ?).
176     rewrite < H3.
177     reflexivity
178   | intro.
179     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
180     rewrite > (false_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4).
181     assumption
182   ]
183 ]
184 qed.
185
186 theorem false_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool.
187 \forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A. 
188 n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false)
189 \to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA.
190 intros 8.
191 elim H
192 [ reflexivity
193 | simplify.
194   rewrite > H3
195   [ simplify.
196     apply H2.
197     intros.
198     apply H3
199     [ apply H4
200     | apply le_S.
201       assumption
202     ]
203   | assumption
204   |apply le_n
205   ]
206 ]
207 qed.
208
209 theorem iter_p_gen2 : 
210 \forall n,m:nat.
211 \forall p1,p2:nat \to bool.
212 \forall A:Type.
213 \forall g: nat \to nat \to A.
214 \forall baseA: A.
215 \forall plusA: A \to A \to A.
216 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
217 \to
218 iter_p_gen (n*m) 
219   (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
220   A 
221   (\lambda x.g (div x m) (mod x m)) 
222   baseA
223   plusA  =
224 iter_p_gen n p1 A
225   (\lambda x.iter_p_gen m p2 A (g x) baseA plusA)
226   baseA plusA.
227 intros.
228 elim n
229 [ simplify.
230   reflexivity
231 | apply (bool_elim ? (p1 n1))
232   [ intro.
233     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
234     simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
235     rewrite > iter_p_gen_plusA
236     [ rewrite < H3.
237       apply eq_f2
238       [ apply eq_iter_p_gen
239         [ intros.
240           rewrite > sym_plus.
241           rewrite > (div_plus_times ? ? ? H5).
242           rewrite > (mod_plus_times ? ? ? H5).
243           rewrite > H4.
244           simplify.
245           reflexivity
246         | intros.
247           rewrite > sym_plus.
248           rewrite > (div_plus_times ? ? ? H5).
249           rewrite > (mod_plus_times ? ? ? H5).
250           rewrite > H4.
251           simplify.reflexivity.   
252         ]
253       | reflexivity
254       ]
255     | assumption
256     | assumption
257     | assumption
258     ]
259   | intro.
260     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
261     simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
262     rewrite > iter_p_gen_plusA
263     [ rewrite > H3.
264       apply (trans_eq ? ? (plusA baseA
265            (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m p2 A (g x) baseA plusA) baseA plusA )))
266       [ apply eq_f2
267         [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
268           [ apply iter_p_gen_false
269           | intros.
270             rewrite > sym_plus.
271             rewrite > (div_plus_times ? ? ? H5).
272             rewrite > (mod_plus_times ? ? ? H5).
273             rewrite > H4.
274             simplify.reflexivity
275           | intros.reflexivity.
276           ]
277         | reflexivity
278         ]
279       | rewrite < H.
280         rewrite > H2.
281         reflexivity.  
282       ]
283     | assumption
284     | assumption
285     | assumption
286     ]
287   ]
288 ]
289 qed.
290
291
292 theorem iter_p_gen2': 
293 \forall n,m:nat.
294 \forall p1: nat \to bool.
295 \forall p2: nat \to nat \to bool.
296 \forall A:Type.
297 \forall g: nat \to nat \to A.
298 \forall baseA: A.
299 \forall plusA: A \to A \to A.
300 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
301 \to
302 iter_p_gen (n*m) 
303   (\lambda x.andb (p1 (div x m)) (p2 (div x m)(mod x m)))
304   A 
305   (\lambda x.g (div x m) (mod x m)) 
306   baseA
307   plusA  =
308 iter_p_gen n p1 A
309   (\lambda x.iter_p_gen m (p2 x) A (g x) baseA plusA)
310   baseA plusA.
311 intros.
312 elim n
313 [ simplify.
314   reflexivity
315 | apply (bool_elim ? (p1 n1))
316   [ intro.
317     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
318     simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
319     rewrite > iter_p_gen_plusA
320     [ rewrite < H3.
321       apply eq_f2
322       [ apply eq_iter_p_gen
323         [ intros.
324           rewrite > sym_plus.
325           rewrite > (div_plus_times ? ? ? H5).
326           rewrite > (mod_plus_times ? ? ? H5).
327           rewrite > H4.
328           simplify.
329           reflexivity
330         | intros.
331           rewrite > sym_plus.
332           rewrite > (div_plus_times ? ? ? H5).
333           rewrite > (mod_plus_times ? ? ? H5).
334           rewrite > H4.
335           simplify.reflexivity.   
336         ]
337       | reflexivity
338       ]
339     | assumption
340     | assumption
341     | assumption
342     ]
343   | intro.
344     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
345     simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
346     rewrite > iter_p_gen_plusA
347     [ rewrite > H3.
348       apply (trans_eq ? ? (plusA baseA
349            (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m (p2 x) A (g x) baseA plusA) baseA plusA )))
350       [ apply eq_f2
351         [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
352           [ apply iter_p_gen_false
353           | intros.
354             rewrite > sym_plus.
355             rewrite > (div_plus_times ? ? ? H5).
356             rewrite > (mod_plus_times ? ? ? H5).
357             rewrite > H4.
358             simplify.reflexivity
359           | intros.reflexivity.
360           ]
361         | reflexivity
362         ]
363       | rewrite < H.
364         rewrite > H2.
365         reflexivity.  
366       ]
367     | assumption
368     | assumption
369     | assumption
370     ]
371   ]
372 ]
373 qed.
374
375 lemma iter_p_gen_gi: 
376 \forall A:Type.
377 \forall g: nat \to A.
378 \forall baseA:A.
379 \forall plusA: A \to A \to A.
380 \forall n,i:nat.
381 \forall p:nat \to bool.
382 (symmetric A plusA) \to  (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a) 
383   \to 
384   
385 i < n \to p i = true \to
386 (iter_p_gen n p A g baseA plusA) = 
387 (plusA (g i) (iter_p_gen n (\lambda x:nat. andb (p x) (notb (eqb x i))) A g baseA plusA)).
388 intros 5.
389 elim n
390 [ apply False_ind.
391   apply (not_le_Sn_O i).
392   assumption
393 | apply (bool_elim ? (p n1));intro
394   [ elim (le_to_or_lt_eq i n1)
395     [ rewrite > true_to_iter_p_gen_Sn
396       [ rewrite > true_to_iter_p_gen_Sn
397         [ rewrite < (H2 (g i) ? ?).
398           rewrite > (H1 (g i) (g n1)).
399           rewrite > (H2 (g n1) ? ?).
400           apply eq_f2
401           [ reflexivity
402           | apply H
403             [ assumption
404             | assumption
405             | assumption 
406             | assumption
407             | assumption
408             ]
409           ]
410         | rewrite > H6.simplify.
411           change with (notb (eqb n1 i) = notb false).
412           apply eq_f.
413           apply not_eq_to_eqb_false.
414           unfold Not.intro.
415           apply (lt_to_not_eq ? ? H7).
416           apply sym_eq.assumption
417         ]
418       | assumption
419       ]
420     | rewrite > true_to_iter_p_gen_Sn
421       [ rewrite > H7.
422         apply eq_f2
423         [ reflexivity
424         | rewrite > false_to_iter_p_gen_Sn
425           [ apply eq_iter_p_gen
426             [ intros.
427               elim (p x)
428               [ simplify.
429                 change with (notb false = notb (eqb x n1)).
430                 apply eq_f.
431                 apply sym_eq. 
432                 apply not_eq_to_eqb_false.
433                 apply (lt_to_not_eq ? ? H8)
434               | reflexivity
435               ]
436             | intros.
437               reflexivity
438             ]
439           | rewrite > H6.
440             rewrite > (eq_to_eqb_true ? ? (refl_eq ? n1)).
441             reflexivity
442           ]
443         ]
444       | assumption
445       ]
446     | apply le_S_S_to_le.
447       assumption
448     ]
449   | rewrite > false_to_iter_p_gen_Sn
450     [ elim (le_to_or_lt_eq i n1)
451       [ rewrite > false_to_iter_p_gen_Sn
452         [ apply H
453           [ assumption
454           | assumption
455           | assumption
456           | assumption
457           | assumption
458           ]
459         | rewrite > H6.reflexivity
460         ]
461       | apply False_ind. 
462         apply not_eq_true_false.
463         rewrite < H5.
464         rewrite > H7.
465         assumption
466       | apply le_S_S_to_le.
467         assumption
468       ]
469     | assumption
470     ]
471   ] 
472
473 qed.
474
475
476 theorem eq_iter_p_gen_gh: 
477 \forall A:Type.
478 \forall baseA: A.
479 \forall plusA: A \to A \to A.
480 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a) \to
481 \forall g: nat \to A.
482 \forall h,h1: nat \to nat.
483 \forall n,n1:nat.
484 \forall p1,p2:nat \to bool.
485 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
486 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to 
487 (\forall i. i < n \to p1 i = true \to h i < n1) \to 
488 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
489 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to 
490 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to 
491
492 iter_p_gen n p1 A (\lambda x.g(h x)) baseA plusA = 
493 iter_p_gen n1 (\lambda x.p2 x) A g baseA plusA.
494 intros 10.
495 elim n
496 [ generalize in match H8.
497   elim n1
498   [ reflexivity
499   | apply (bool_elim ? (p2 n2));intro
500     [ apply False_ind.
501       apply (not_le_Sn_O (h1 n2)).
502       apply H10
503       [ apply le_n
504       | assumption
505       ]
506     | rewrite > false_to_iter_p_gen_Sn
507       [ apply H9.
508         intros.  
509         apply H10
510         [ apply le_S.
511           apply H12
512         | assumption
513         ]
514       | assumption
515       ]
516     ]
517   ]
518 | apply (bool_elim ? (p1 n1));intro
519   [ rewrite > true_to_iter_p_gen_Sn
520     [ rewrite > (iter_p_gen_gi A g baseA plusA n2 (h n1))
521       [ apply eq_f2
522         [ reflexivity
523         | apply H3
524           [ intros.
525             rewrite > H4
526             [ simplify.
527               change with ((\not eqb (h i) (h n1))= \not false).
528               apply eq_f.
529               apply not_eq_to_eqb_false.
530               unfold Not.
531               intro.
532               apply (lt_to_not_eq ? ? H11).
533               rewrite < H5
534               [ rewrite < (H5 n1)
535                 [ apply eq_f.
536                   assumption
537                 | apply le_n
538                 | assumption
539                 ]
540               | apply le_S.
541                 assumption
542               | assumption
543               ]
544             | apply le_S.assumption
545             | assumption
546             ]
547           | intros.
548             apply H5
549             [ apply le_S.
550               assumption
551             | assumption
552             ]
553           | intros.
554             apply H6
555             [ apply le_S.assumption
556             | assumption
557             ]
558           | intros.
559             apply H7
560             [ assumption
561             | generalize in match H12.
562               elim (p2 j)
563               [ reflexivity
564               | assumption
565               ]
566             ]
567           | intros.
568             apply H8
569             [ assumption
570             | generalize in match H12.
571               elim (p2 j)
572               [ reflexivity
573               | assumption
574               ]
575             ]
576           | intros.
577             elim (le_to_or_lt_eq (h1 j) n1)
578             [ assumption
579             | generalize in match H12.
580               elim (p2 j)
581               [ simplify in H13.
582                 absurd (j = (h n1))
583                 [ rewrite < H13.
584                   rewrite > H8
585                   [ reflexivity
586                   | assumption
587                   | autobatch
588                   ]
589                 | apply eqb_false_to_not_eq.
590                   generalize in match H14.
591                   elim (eqb j (h n1))
592                   [ apply sym_eq.assumption
593                   | reflexivity
594                   ]
595                 ]
596               | simplify in H14.
597                 apply False_ind.
598                 apply not_eq_true_false.
599                 apply sym_eq.assumption
600               ]
601             | apply le_S_S_to_le.
602               apply H9
603               [ assumption
604               | generalize in match H12.
605                 elim (p2 j)
606                 [ reflexivity
607                 | assumption
608                 ]
609               ]
610             ]
611           ]
612         ]
613       | assumption  
614       | assumption
615       | assumption  
616       | apply H6
617         [ apply le_n
618         | assumption
619         ]
620       | apply H4
621         [ apply le_n
622         | assumption
623         ]
624       ]
625     | assumption
626     ]
627   | rewrite > false_to_iter_p_gen_Sn
628     [ apply H3
629       [ intros.
630         apply H4[apply le_S.assumption|assumption]
631       | intros.
632         apply H5[apply le_S.assumption|assumption]
633       | intros.
634         apply H6[apply le_S.assumption|assumption]
635       | intros.
636         apply H7[assumption|assumption]
637       | intros.
638         apply H8[assumption|assumption]
639       | intros.
640         elim (le_to_or_lt_eq (h1 j) n1)
641         [ assumption
642         | absurd (j = (h n1))
643           [ rewrite < H13.
644             rewrite > H8
645             [ reflexivity
646             | assumption
647             | assumption
648             ]
649           | unfold Not.intro.
650             apply not_eq_true_false.
651             rewrite < H10.
652             rewrite < H13.
653             rewrite > H7
654             [ reflexivity
655             | assumption
656             | assumption
657             ]
658           ]
659         | apply le_S_S_to_le.
660           apply H9
661           [ assumption
662           | assumption
663           ]
664         ]
665       ]
666     | assumption
667     ]
668   ]
669 ]
670 qed.
671
672
673
674 definition p_ord_times \def
675 \lambda p,m,x.
676   match p_ord x p with
677   [pair q r \Rightarrow r*m+q].
678   
679 theorem  eq_p_ord_times: \forall p,m,x.
680 p_ord_times p m x = (ord_rem x p)*m+(ord x p).
681 intros.unfold p_ord_times. unfold ord_rem.
682 unfold ord.
683 elim (p_ord x p).
684 reflexivity.
685 qed.
686
687 theorem div_p_ord_times: 
688 \forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
689 intros.rewrite > eq_p_ord_times.
690 apply div_plus_times.
691 assumption.
692 qed.
693
694 theorem mod_p_ord_times: 
695 \forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
696 intros.rewrite > eq_p_ord_times.
697 apply mod_plus_times.
698 assumption.
699 qed.
700
701 theorem iter_p_gen_divides:
702 \forall A:Type.
703 \forall baseA: A.
704 \forall plusA: A \to A \to A. 
705 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to 
706 \forall g: nat \to A.
707 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
708
709 \to
710
711 iter_p_gen (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) A g baseA plusA =
712 iter_p_gen (S n) (\lambda x.divides_b x n) A
713   (\lambda x.iter_p_gen (S m) (\lambda y.true) A (\lambda y.g (x*(exp p y))) baseA plusA) baseA plusA.
714 intros.
715 cut (O < p)
716   [rewrite < (iter_p_gen2 ? ? ? ? ? ? ? ? H3 H4 H5).
717    apply (trans_eq ? ? 
718     (iter_p_gen (S n*S m) (\lambda x:nat.divides_b (x/S m) n) A
719        (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m)))  baseA plusA) )
720     [apply sym_eq.
721      apply (eq_iter_p_gen_gh ? ? ? ? ? ? g ? (p_ord_times p (S m)))
722       [ assumption
723       | assumption
724       | assumption
725       |intros.
726        lapply (divides_b_true_to_lt_O ? ? H H7).
727        apply divides_to_divides_b_true
728         [rewrite > (times_n_O O).
729          apply lt_times
730           [assumption
731           |apply lt_O_exp.assumption
732           ]
733         |apply divides_times
734           [apply divides_b_true_to_divides.assumption
735           |apply (witness ? ? (p \sup (m-i \mod (S m)))).
736            rewrite < exp_plus_times.
737            apply eq_f.
738            rewrite > sym_plus.
739            apply plus_minus_m_m.
740            autobatch
741           ]
742         ]
743       |intros.
744        lapply (divides_b_true_to_lt_O ? ? H H7).
745        unfold p_ord_times.
746        rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
747         [change with ((i/S m)*S m+i \mod S m=i).
748          apply sym_eq.
749          apply div_mod.
750          apply lt_O_S
751         |assumption
752         |unfold Not.intro.
753          apply H2.
754          apply (trans_divides ? (i/ S m))
755           [assumption|
756            apply divides_b_true_to_divides;assumption]
757         |apply sym_times.
758         ]
759       |intros.
760        apply le_S_S.
761        apply le_times
762         [apply le_S_S_to_le.
763          change with ((i/S m) < S n).
764          apply (lt_times_to_lt_l m).
765          apply (le_to_lt_to_lt ? i)
766           [autobatch|assumption]
767         |apply le_exp
768           [assumption
769           |apply le_S_S_to_le.
770            apply lt_mod_m_m.
771            apply lt_O_S
772           ]
773         ]
774       |intros.
775        cut (ord j p < S m)
776         [rewrite > div_p_ord_times
777           [apply divides_to_divides_b_true
778             [apply lt_O_ord_rem
779              [elim H1.assumption
780              |apply (divides_b_true_to_lt_O ? ? ? H7).
781                rewrite > (times_n_O O).
782                apply lt_times
783                [assumption|apply lt_O_exp.assumption]
784              ]
785            |cut (n = ord_rem (n*(exp p m)) p)
786               [rewrite > Hcut2.
787                apply divides_to_divides_ord_rem
788                 [apply (divides_b_true_to_lt_O ? ? ? H7).
789                  rewrite > (times_n_O O).
790                  apply lt_times
791                  [assumption|apply lt_O_exp.assumption]
792                  |rewrite > (times_n_O O).
793                    apply lt_times
794                   [assumption|apply lt_O_exp.assumption]
795                |assumption
796                |apply divides_b_true_to_divides.
797                 assumption
798                ]
799               |unfold ord_rem.
800               rewrite > (p_ord_exp1 p ? m n)
801                 [reflexivity
802                |assumption
803                 |assumption
804                |apply sym_times
805                ]
806              ]
807             ]
808           |assumption
809           ]
810         |cut (m = ord (n*(exp p m)) p)
811           [apply le_S_S.
812            rewrite > Hcut1.
813            apply divides_to_le_ord
814             [apply (divides_b_true_to_lt_O ? ? ? H7).
815              rewrite > (times_n_O O).
816              apply lt_times
817               [assumption|apply lt_O_exp.assumption]
818             |rewrite > (times_n_O O).
819              apply lt_times
820               [assumption|apply lt_O_exp.assumption]
821             |assumption
822             |apply divides_b_true_to_divides.
823              assumption
824             ]
825           |unfold ord.
826            rewrite > (p_ord_exp1 p ? m n)
827             [reflexivity
828             |assumption
829             |assumption
830             |apply sym_times
831             ]
832           ]
833         ]
834       |intros.
835        cut (ord j p < S m)
836         [rewrite > div_p_ord_times
837           [rewrite > mod_p_ord_times
838             [rewrite > sym_times.
839              apply sym_eq.
840              apply exp_ord
841               [elim H1.assumption
842               |apply (divides_b_true_to_lt_O ? ? ? H7).
843                rewrite > (times_n_O O).
844                apply lt_times
845                 [assumption|apply lt_O_exp.assumption]
846               ]
847            |cut (m = ord (n*(exp p m)) p)
848              [apply le_S_S.
849               rewrite > Hcut2.
850               apply divides_to_le_ord
851                [apply (divides_b_true_to_lt_O ? ? ? H7).
852                 rewrite > (times_n_O O).
853                 apply lt_times
854                  [assumption|apply lt_O_exp.assumption]
855                |rewrite > (times_n_O O).
856                 apply lt_times
857                  [assumption|apply lt_O_exp.assumption]
858                |assumption
859                |apply divides_b_true_to_divides.
860                 assumption
861                ]
862              |unfold ord.
863               rewrite > (p_ord_exp1 p ? m n)
864                 [reflexivity
865                 |assumption
866                 |assumption
867                 |apply sym_times
868                 ]
869               ]
870             ]
871           |assumption
872           ]
873         |cut (m = ord (n*(exp p m)) p)
874           [apply le_S_S.
875            rewrite > Hcut1.
876            apply divides_to_le_ord
877             [apply (divides_b_true_to_lt_O ? ? ? H7).
878              rewrite > (times_n_O O).
879              apply lt_times
880               [assumption|apply lt_O_exp.assumption]
881             |rewrite > (times_n_O O).
882              apply lt_times
883               [assumption|apply lt_O_exp.assumption]
884             |assumption
885             |apply divides_b_true_to_divides.
886              assumption
887             ]
888           |unfold ord.
889            rewrite > (p_ord_exp1 p ? m n)
890             [reflexivity
891             |assumption
892             |assumption
893             |apply sym_times
894             ]
895           ]
896         ]
897       |intros.
898        rewrite > eq_p_ord_times.
899        rewrite > sym_plus.
900        apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
901         [apply lt_plus_l.
902          apply le_S_S.
903          cut (m = ord (n*(p \sup m)) p)
904           [rewrite > Hcut1.
905            apply divides_to_le_ord
906             [apply (divides_b_true_to_lt_O ? ? ? H7).
907              rewrite > (times_n_O O).
908              apply lt_times
909               [assumption|apply lt_O_exp.assumption]
910             |rewrite > (times_n_O O).
911              apply lt_times
912               [assumption|apply lt_O_exp.assumption]
913             |assumption
914             |apply divides_b_true_to_divides.
915              assumption
916             ]
917           |unfold ord.
918            rewrite > sym_times.
919            rewrite > (p_ord_exp1 p ? m n)
920             [reflexivity
921             |assumption
922             |assumption
923             |reflexivity
924             ]
925           ]
926         |change with (S (ord_rem j p)*S m \le S n*S m).
927          apply le_times_l.
928          apply le_S_S.
929          cut (n = ord_rem (n*(p \sup m)) p)
930           [rewrite > Hcut1.
931            apply divides_to_le
932             [apply lt_O_ord_rem
933               [elim H1.assumption
934               |rewrite > (times_n_O O).
935                apply lt_times
936                 [assumption|apply lt_O_exp.assumption]
937               ]
938             |apply divides_to_divides_ord_rem
939               [apply (divides_b_true_to_lt_O ? ? ? H7).
940                rewrite > (times_n_O O).
941                apply lt_times
942                 [assumption|apply lt_O_exp.assumption]
943               |rewrite > (times_n_O O).
944                apply lt_times
945                 [assumption|apply lt_O_exp.assumption]
946               |assumption
947               |apply divides_b_true_to_divides.
948                assumption
949               ]
950             ]
951         |unfold ord_rem.
952          rewrite > sym_times.
953          rewrite > (p_ord_exp1 p ? m n)
954           [reflexivity
955           |assumption
956           |assumption
957           |reflexivity
958           ]
959         ]
960       ]
961     ]
962   |apply eq_iter_p_gen
963   
964     [intros.
965      elim (divides_b (x/S m) n);reflexivity
966     |intros.reflexivity
967     ]
968   ]
969 |elim H1.apply lt_to_le.assumption
970 ]
971 qed.
972     
973 (*distributive property for iter_p_gen*)
974 theorem distributive_times_plus_iter_p_gen: \forall A:Type.
975 \forall plusA: A \to A \to A. \forall basePlusA: A.
976 \forall timesA: A \to A \to A. 
977 \forall n:nat. \forall k:A. \forall p:nat \to bool. \forall g:nat \to A.
978 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  basePlusA) = a) \to
979 (symmetric A timesA) \to (distributive A timesA plusA) \to
980 (\forall a:A. (timesA a basePlusA) = basePlusA)
981  
982   \to
983
984 ((timesA k (iter_p_gen n p A g basePlusA plusA)) = 
985  (iter_p_gen n p A (\lambda i:nat.(timesA k (g i))) basePlusA plusA)).
986 intros.
987 elim n
988 [ simplify.
989   apply H5
990 | cut( (p n1) = true \lor (p n1) = false)
991   [ elim Hcut
992     [ rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
993       rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
994       rewrite > (H4).
995       rewrite > (H3 k (g n1)).
996       apply eq_f.
997       assumption
998     | rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
999       rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
1000       assumption
1001     ]
1002   | elim ((p n1))
1003     [ left.
1004       reflexivity
1005     | right.
1006       reflexivity
1007     ]
1008   ]
1009 ]
1010 qed.
1011
1012