]> matita.cs.unibo.it Git - helm.git/blob - weblib/arithmetics/sigma_pi.ma
- support for atomic arities and candidates of reducibility started
[helm.git] / weblib / arithmetics / sigma_pi.ma
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department of the University of Bologna, Italy.                     
5     ||I||                                                                 
6     ||T||  
7     ||A||  This file is distributed under the terms of the 
8     \   /  GNU General Public License Version 2        
9      \ /      
10       V_______________________________________________________________ *)
11
12 include "arithmetics/bigops.ma".
13
14 definition natAop ≝ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n)) 
15    (λa,b,c.sym_eq ??? (associative_plus a b c)).
16    
17 definition natACop ≝ mk_ACop nat 0 natAop commutative_plus.
18
19 definition natDop ≝ mk_Dop nat 0 natACop times (λn.(sym_eq ??? (times_n_O n))) 
20    distributive_times_plus.
21
22 unification hint  0 ≔ ;
23    S ≟ natAop
24 (* ---------------------------------------- *) ⊢ 
25    plus ≡ op ? ? S.
26
27 unification hint  0 ≔ ;
28    S ≟ natACop
29 (* ---------------------------------------- *) ⊢ 
30    plus ≡ op ? ? S.
31
32 unification hint  0 ≔ ;
33    S ≟ natDop
34 (* ---------------------------------------- *) ⊢ 
35    plus ≡ sum ? ? S.
36    
37 unification hint  0 ≔ ;
38    S ≟ natDop
39 (* ---------------------------------------- *) ⊢ 
40    times ≡ prod ? ? S.   
41    
42 (* Sigma e Pi *)
43
44 notation "∑_{ ident i < n | p } f"
45   with precedence 80
46 for @{'bigop $n plus 0 (λ${ident i}.$p) (λ${ident i}. $f)}.
47
48 notation "∑_{ ident i < n } f"
49   with precedence 80
50 for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}.
51
52 notation "∑_{ ident j ∈ [a,b[ } f"
53   with precedence 80
54 for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
55   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
56   
57 notation "∑_{ ident j ∈ [a,b[ | p } f"
58   with precedence 80
59 for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
60   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
61  
62 notation "∏_{ ident i < n | p} f"
63   with precedence 80
64 for @{'bigop $n times 1 (λ${ident i}.$p) (λ${ident i}. $f)}.
65  
66 notation "∏_{ ident i < n } f"
67   with precedence 80
68 for @{'bigop $n times 1 (λ${ident i}.true) (λ${ident i}. $f)}.
69
70 notation "∏_{ ident j ∈ [a,b[ } f"
71   with precedence 80
72 for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
73   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
74   
75 notation "∏_{ ident j ∈ [a,b[ | p } f"
76   with precedence 80
77 for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
78   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
79
80  
81 (*
82     
83 definition p_ord_times \def
84 \lambda p,m,x.
85   match p_ord x p with
86   [pair q r \Rightarrow r*m+q].
87   
88 theorem  eq_p_ord_times: \forall p,m,x.
89 p_ord_times p m x = (ord_rem x p)*m+(ord x p).
90 intros.unfold p_ord_times. unfold ord_rem.
91 unfold ord.
92 elim (p_ord x p).
93 reflexivity.
94 qed.
95
96 theorem div_p_ord_times: 
97 \forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
98 intros.rewrite > eq_p_ord_times.
99 apply div_plus_times.
100 assumption.
101 qed.
102
103 theorem mod_p_ord_times: 
104 \forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
105 intros.rewrite > eq_p_ord_times.
106 apply mod_plus_times.
107 assumption.
108 qed.
109
110 lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
111 intros.
112 elim (le_to_or_lt_eq O ? (le_O_n m))
113   [assumption
114   |apply False_ind.
115    rewrite < H1 in H.
116    rewrite < times_n_O in H.
117    apply (not_le_Sn_O ? H)
118   ]
119 qed.
120
121 theorem iter_p_gen_knm:
122 \forall A:Type.
123 \forall baseA: A.
124 \forall plusA: A \to A \to A. 
125 (symmetric A plusA) \to 
126 (associative A plusA) \to 
127 (\forall a:A.(plusA a  baseA) = a)\to
128 \forall g: nat \to A.
129 \forall h2:nat \to nat \to nat.
130 \forall h11,h12:nat \to nat. 
131 \forall k,n,m.
132 \forall p1,p21:nat \to bool.
133 \forall p22:nat \to nat \to bool.
134 (\forall x. x < k \to p1 x = true \to 
135 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
136 \land h2 (h11 x) (h12 x) = x 
137 \land (h11 x) < n \land (h12 x) < m) \to
138 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to 
139 p1 (h2 i j) = true \land 
140 h11 (h2 i j) = i \land h12 (h2 i j) = j
141 \land h2 i j < k) \to
142 iter_p_gen k p1 A g baseA plusA =
143 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.
144 intros.
145 rewrite < (iter_p_gen2' n m p21 p22 ? ? ? ? H H1 H2).
146 apply sym_eq.
147 apply (eq_iter_p_gen_gh A baseA plusA H H1 H2 g ? (\lambda x.(h11 x)*m+(h12 x)))
148  [intros.
149   elim (H4 (i/m) (i \mod m));clear H4
150    [elim H7.clear H7.
151     elim H4.clear H4.
152     assumption
153    |apply (lt_times_to_lt_div ? ? ? H5)
154    |apply lt_mod_m_m.
155     apply (lt_times_to_lt_O ? ? ? H5)
156    |apply (andb_true_true ? ? H6)
157    |apply (andb_true_true_r ? ? H6)
158    ]
159  |intros.
160   elim (H4 (i/m) (i \mod m));clear H4
161    [elim H7.clear H7.
162     elim H4.clear H4.
163     rewrite > H10.
164     rewrite > H9.
165     apply sym_eq.
166     apply div_mod.
167     apply (lt_times_to_lt_O ? ? ? H5)
168    |apply (lt_times_to_lt_div ? ? ? H5)
169    |apply lt_mod_m_m.
170     apply (lt_times_to_lt_O ? ? ? H5)  
171    |apply (andb_true_true ? ? H6)
172    |apply (andb_true_true_r ? ? H6)
173    ]
174  |intros.
175   elim (H4 (i/m) (i \mod m));clear H4
176    [elim H7.clear H7.
177     elim H4.clear H4.
178     assumption
179    |apply (lt_times_to_lt_div ? ? ? H5)
180    |apply lt_mod_m_m.
181     apply (lt_times_to_lt_O ? ? ? H5)
182    |apply (andb_true_true ? ? H6)
183    |apply (andb_true_true_r ? ? H6)
184    ]
185  |intros.
186   elim (H3 j H5 H6).
187   elim H7.clear H7.
188   elim H9.clear H9.
189   elim H7.clear H7.
190   rewrite > div_plus_times
191    [rewrite > mod_plus_times
192      [rewrite > H9.
193       rewrite > H12.
194       reflexivity.
195      |assumption
196      ]
197    |assumption
198    ]
199  |intros.
200   elim (H3 j H5 H6).
201   elim H7.clear H7.
202   elim H9.clear H9.
203   elim H7.clear H7. 
204   rewrite > div_plus_times
205    [rewrite > mod_plus_times
206      [assumption
207      |assumption
208      ]
209    |assumption
210    ]
211  |intros.
212   elim (H3 j H5 H6).
213   elim H7.clear H7.
214   elim H9.clear H9.
215   elim H7.clear H7. 
216   apply (lt_to_le_to_lt ? ((h11 j)*m+m))
217    [apply monotonic_lt_plus_r.
218     assumption
219    |rewrite > sym_plus.
220     change with ((S (h11 j)*m) \le n*m).
221     apply monotonic_le_times_l.
222     assumption
223    ]
224  ]
225 qed.
226
227 theorem iter_p_gen_divides:
228 \forall A:Type.
229 \forall baseA: A.
230 \forall plusA: A \to A \to A. 
231 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to 
232 \forall g: nat \to A.
233 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
234
235 \to
236
237 iter_p_gen (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) A g baseA plusA =
238 iter_p_gen (S n) (\lambda x.divides_b x n) A
239   (\lambda x.iter_p_gen (S m) (\lambda y.true) A (\lambda y.g (x*(exp p y))) baseA plusA) baseA plusA.
240 intros.
241 cut (O < p)
242   [rewrite < (iter_p_gen2 ? ? ? ? ? ? ? ? H3 H4 H5).
243    apply (trans_eq ? ? 
244     (iter_p_gen (S n*S m) (\lambda x:nat.divides_b (x/S m) n) A
245        (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m)))  baseA plusA) )
246     [apply sym_eq.
247      apply (eq_iter_p_gen_gh ? ? ? ? ? ? g ? (p_ord_times p (S m)))
248       [ assumption
249       | assumption
250       | assumption
251       |intros.
252        lapply (divides_b_true_to_lt_O ? ? H H7).
253        apply divides_to_divides_b_true
254         [rewrite > (times_n_O O).
255          apply lt_times
256           [assumption
257           |apply lt_O_exp.assumption
258           ]
259         |apply divides_times
260           [apply divides_b_true_to_divides.assumption
261           |apply (witness ? ? (p \sup (m-i \mod (S m)))).
262            rewrite < exp_plus_times.
263            apply eq_f.
264            rewrite > sym_plus.
265            apply plus_minus_m_m.
266            autobatch by le_S_S_to_le, lt_mod_m_m, lt_O_S;
267           ]
268         ]
269       |intros.
270        lapply (divides_b_true_to_lt_O ? ? H H7).
271        unfold p_ord_times.
272        rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
273         [change with ((i/S m)*S m+i \mod S m=i).
274          apply sym_eq.
275          apply div_mod.
276          apply lt_O_S
277         |assumption
278         |unfold Not.intro.
279          apply H2.
280          apply (trans_divides ? (i/ S m))
281           [assumption|
282            apply divides_b_true_to_divides;assumption]
283         |apply sym_times.
284         ]
285       |intros.
286        apply le_S_S.
287        apply le_times
288         [apply le_S_S_to_le.
289          change with ((i/S m) < S n).
290          apply (lt_times_to_lt_l m).
291          apply (le_to_lt_to_lt ? i);[2:assumption]
292          autobatch by eq_plus_to_le, div_mod, lt_O_S.
293         |apply le_exp
294           [assumption
295           |apply le_S_S_to_le.
296            apply lt_mod_m_m.
297            apply lt_O_S
298           ]
299         ]
300       |intros.
301        cut (ord j p < S m)
302         [rewrite > div_p_ord_times
303           [apply divides_to_divides_b_true
304             [apply lt_O_ord_rem
305              [elim H1.assumption
306              |apply (divides_b_true_to_lt_O ? ? ? H7).
307                rewrite > (times_n_O O).
308                apply lt_times
309                [assumption|apply lt_O_exp.assumption]
310              ]
311            |cut (n = ord_rem (n*(exp p m)) p)
312               [rewrite > Hcut2.
313                apply divides_to_divides_ord_rem
314                 [apply (divides_b_true_to_lt_O ? ? ? H7).
315                  rewrite > (times_n_O O).
316                  apply lt_times
317                  [assumption|apply lt_O_exp.assumption]
318                  |rewrite > (times_n_O O).
319                    apply lt_times
320                   [assumption|apply lt_O_exp.assumption]
321                |assumption
322                |apply divides_b_true_to_divides.
323                 assumption
324                ]
325               |unfold ord_rem.
326               rewrite > (p_ord_exp1 p ? m n)
327                 [reflexivity
328                |assumption
329                 |assumption
330                |apply sym_times
331                ]
332              ]
333             ]
334           |assumption
335           ]
336         |cut (m = ord (n*(exp p m)) p)
337           [apply le_S_S.
338            rewrite > Hcut1.
339            apply divides_to_le_ord
340             [apply (divides_b_true_to_lt_O ? ? ? H7).
341              rewrite > (times_n_O O).
342              apply lt_times
343               [assumption|apply lt_O_exp.assumption]
344             |rewrite > (times_n_O O).
345              apply lt_times
346               [assumption|apply lt_O_exp.assumption]
347             |assumption
348             |apply divides_b_true_to_divides.
349              assumption
350             ]
351           |unfold ord.
352            rewrite > (p_ord_exp1 p ? m n)
353             [reflexivity
354             |assumption
355             |assumption
356             |apply sym_times
357             ]
358           ]
359         ]
360       |intros.
361        cut (ord j p < S m)
362         [rewrite > div_p_ord_times
363           [rewrite > mod_p_ord_times
364             [rewrite > sym_times.
365              apply sym_eq.
366              apply exp_ord
367               [elim H1.assumption
368               |apply (divides_b_true_to_lt_O ? ? ? H7).
369                rewrite > (times_n_O O).
370                apply lt_times
371                 [assumption|apply lt_O_exp.assumption]
372               ]
373            |cut (m = ord (n*(exp p m)) p)
374              [apply le_S_S.
375               rewrite > Hcut2.
376               apply divides_to_le_ord
377                [apply (divides_b_true_to_lt_O ? ? ? H7).
378                 rewrite > (times_n_O O).
379                 apply lt_times
380                  [assumption|apply lt_O_exp.assumption]
381                |rewrite > (times_n_O O).
382                 apply lt_times
383                  [assumption|apply lt_O_exp.assumption]
384                |assumption
385                |apply divides_b_true_to_divides.
386                 assumption
387                ]
388              |unfold ord.
389               rewrite > (p_ord_exp1 p ? m n)
390                 [reflexivity
391                 |assumption
392                 |assumption
393                 |apply sym_times
394                 ]
395               ]
396             ]
397           |assumption
398           ]
399         |cut (m = ord (n*(exp p m)) p)
400           [apply le_S_S.
401            rewrite > Hcut1.
402            apply divides_to_le_ord
403             [apply (divides_b_true_to_lt_O ? ? ? H7).
404              rewrite > (times_n_O O).
405              apply lt_times
406               [assumption|apply lt_O_exp.assumption]
407             |rewrite > (times_n_O O).
408              apply lt_times
409               [assumption|apply lt_O_exp.assumption]
410             |assumption
411             |apply divides_b_true_to_divides.
412              assumption
413             ]
414           |unfold ord.
415            rewrite > (p_ord_exp1 p ? m n)
416             [reflexivity
417             |assumption
418             |assumption
419             |apply sym_times
420             ]
421           ]
422         ]
423       |intros.
424        rewrite > eq_p_ord_times.
425        rewrite > sym_plus.
426        apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
427         [apply lt_plus_l.
428          apply le_S_S.
429          cut (m = ord (n*(p \sup m)) p)
430           [rewrite > Hcut1.
431            apply divides_to_le_ord
432             [apply (divides_b_true_to_lt_O ? ? ? H7).
433              rewrite > (times_n_O O).
434              apply lt_times
435               [assumption|apply lt_O_exp.assumption]
436             |rewrite > (times_n_O O).
437              apply lt_times
438               [assumption|apply lt_O_exp.assumption]
439             |assumption
440             |apply divides_b_true_to_divides.
441              assumption
442             ]
443           |unfold ord.
444            rewrite > sym_times.
445            rewrite > (p_ord_exp1 p ? m n)
446             [reflexivity
447             |assumption
448             |assumption
449             |reflexivity
450             ]
451           ]
452         |change with (S (ord_rem j p)*S m \le S n*S m).
453          apply le_times_l.
454          apply le_S_S.
455          cut (n = ord_rem (n*(p \sup m)) p)
456           [rewrite > Hcut1.
457            apply divides_to_le
458             [apply lt_O_ord_rem
459               [elim H1.assumption
460               |rewrite > (times_n_O O).
461                apply lt_times
462                 [assumption|apply lt_O_exp.assumption]
463               ]
464             |apply divides_to_divides_ord_rem
465               [apply (divides_b_true_to_lt_O ? ? ? H7).
466                rewrite > (times_n_O O).
467                apply lt_times
468                 [assumption|apply lt_O_exp.assumption]
469               |rewrite > (times_n_O O).
470                apply lt_times
471                 [assumption|apply lt_O_exp.assumption]
472               |assumption
473               |apply divides_b_true_to_divides.
474                assumption
475               ]
476             ]
477         |unfold ord_rem.
478          rewrite > sym_times.
479          rewrite > (p_ord_exp1 p ? m n)
480           [reflexivity
481           |assumption
482           |assumption
483           |reflexivity
484           ]
485         ]
486       ]
487     ]
488   |apply eq_iter_p_gen
489   
490     [intros.
491      elim (divides_b (x/S m) n);reflexivity
492     |intros.reflexivity
493     ]
494   ]
495 |elim H1.apply lt_to_le.assumption
496 ]
497 qed.
498     
499
500
501 theorem iter_p_gen_2_eq: 
502 \forall A:Type.
503 \forall baseA: A.
504 \forall plusA: A \to A \to A. 
505 (symmetric A plusA) \to 
506 (associative A plusA) \to 
507 (\forall a:A.(plusA a  baseA) = a)\to
508 \forall g: nat \to nat \to A.
509 \forall h11,h12,h21,h22: nat \to nat \to nat. 
510 \forall n1,m1,n2,m2.
511 \forall p11,p21:nat \to bool.
512 \forall p12,p22:nat \to nat \to bool.
513 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to 
514 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
515 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
516 \land h11 i j < n1 \land h12 i j < m1) \to
517 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to 
518 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
519 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
520 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
521 iter_p_gen n1 p11 A 
522      (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA) 
523      baseA plusA =
524 iter_p_gen n2 p21 A 
525     (\lambda x:nat .iter_p_gen m2 (p22 x) A  (\lambda y. g (h11 x y) (h12 x y)) baseA plusA )
526     baseA plusA.
527
528 intros.
529 rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
530 letin ha:= (\lambda x,y.(((h11 x y)*m1) + (h12 x y))).
531 letin ha12:= (\lambda x.(h21 (x/m1) (x \mod m1))).
532 letin ha22:= (\lambda x.(h22 (x/m1) (x \mod m1))).
533
534 apply (trans_eq ? ? 
535 (iter_p_gen n2 p21 A (\lambda x:nat. iter_p_gen m2 (p22 x) A
536  (\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))
537 [
538   apply (iter_p_gen_knm A baseA plusA H H1 H2 (\lambda e. (g (e/m1) (e \mod m1))) ha ha12 ha22);intros
539   [ elim (and_true ? ? H6).
540     cut(O \lt m1)
541     [ cut(x/m1 < n1)
542       [ cut((x \mod m1) < m1)
543         [ elim (H4 ? ? Hcut1 Hcut2 H7 H8).
544           elim H9.clear H9.
545           elim H11.clear H11.
546           elim H9.clear H9.
547           elim H11.clear H11.
548           split
549           [ split
550             [ split
551               [ split
552                 [ assumption
553                 | assumption
554                 ]
555               | unfold ha.
556                 unfold ha12.
557                 unfold ha22.
558                 rewrite > H14.
559                 rewrite > H13.
560                 apply sym_eq.
561                 apply div_mod.
562                 assumption
563               ]
564             | assumption
565             ]
566           | assumption
567           ]
568         | apply lt_mod_m_m.
569           assumption
570         ]
571       | apply (lt_times_n_to_lt m1)
572         [ assumption
573         | apply (le_to_lt_to_lt ? x)
574           [ apply (eq_plus_to_le ? ? (x \mod m1)).
575             apply div_mod.
576             assumption
577           | assumption
578         ]
579       ]  
580     ]
581     | apply not_le_to_lt.unfold.intro.
582       generalize in match H5.
583       apply (le_n_O_elim ? H9).
584       rewrite < times_n_O.
585       apply le_to_not_lt.
586       apply le_O_n.              
587     ]
588   | elim (H3 ? ? H5 H6 H7 H8).
589     elim H9.clear H9.
590     elim H11.clear H11.
591     elim H9.clear H9.
592     elim H11.clear H11.
593     cut(((h11 i j)*m1 + (h12 i j))/m1 = (h11 i j))
594     [ cut(((h11 i j)*m1 + (h12 i j)) \mod m1 = (h12 i j))
595       [ split
596         [ split
597           [ split
598             [ apply true_to_true_to_andb_true
599               [ rewrite > Hcut.
600                 assumption
601               | rewrite > Hcut1.
602                 rewrite > Hcut.
603                 assumption
604               ] 
605             | unfold ha.
606               unfold ha12.
607               rewrite > Hcut1.
608               rewrite > Hcut.
609               assumption
610             ]
611           | unfold ha.
612             unfold ha22.
613             rewrite > Hcut1.
614             rewrite > Hcut.
615             assumption            
616           ]
617         | cut(O \lt m1)
618           [ cut(O \lt n1)      
619             [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
620               [ unfold ha.
621                 apply (lt_plus_r).
622                 assumption
623               | rewrite > sym_plus.
624                 rewrite > (sym_times (h11 i j) m1).
625                 rewrite > times_n_Sm.
626                 rewrite > sym_times.
627                 apply (le_times_l).
628                 assumption  
629               ]
630             | apply not_le_to_lt.unfold.intro.
631               generalize in match H12.
632               apply (le_n_O_elim ? H11).       
633               apply le_to_not_lt.
634               apply le_O_n
635             ]
636           | apply not_le_to_lt.unfold.intro.
637             generalize in match H10.
638             apply (le_n_O_elim ? H11).       
639             apply le_to_not_lt.
640             apply le_O_n
641           ]  
642         ]
643       | rewrite > (mod_plus_times m1 (h11 i j) (h12 i j)).
644         reflexivity.
645         assumption
646       ]     
647     | rewrite > (div_plus_times m1 (h11 i j) (h12 i j)).
648       reflexivity.
649       assumption
650     ]
651   ]
652 | apply (eq_iter_p_gen1)
653   [ intros. reflexivity 
654   | intros.
655     apply (eq_iter_p_gen1)
656     [ intros. reflexivity
657     | intros.
658       rewrite > (div_plus_times)
659       [ rewrite > (mod_plus_times)
660         [ reflexivity
661         | elim (H3 x x1 H5 H7 H6 H8).
662           assumption
663         ]
664       | elim (H3 x x1 H5 H7 H6 H8).       
665         assumption
666       ]
667     ]
668   ]
669 ]
670 qed.
671
672 theorem iter_p_gen_iter_p_gen: 
673 \forall A:Type.
674 \forall baseA: A.
675 \forall plusA: A \to A \to A. 
676 (symmetric A plusA) \to 
677 (associative A plusA) \to 
678 (\forall a:A.(plusA a  baseA) = a)\to
679 \forall g: nat \to nat \to A.
680 \forall n,m.
681 \forall p11,p21:nat \to bool.
682 \forall p12,p22:nat \to nat \to bool.
683 (\forall x,y. x < n \to y < m \to 
684  (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
685 iter_p_gen n p11 A 
686   (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA) 
687   baseA plusA =
688 iter_p_gen m p21 A 
689   (\lambda y:nat.iter_p_gen n (p22 y) A  (\lambda x. g x y) baseA plusA )
690   baseA plusA.
691 intros.
692 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)
693        n m m n p11 p21 p12 p22)
694   [intros.split
695     [split
696       [split
697         [split
698           [split
699             [apply (andb_true_true ? (p12 j i)).
700              rewrite > H3
701               [rewrite > H6.rewrite > H7.reflexivity
702               |assumption
703               |assumption
704               ]
705             |apply (andb_true_true_r (p11 j)).
706              rewrite > H3
707               [rewrite > H6.rewrite > H7.reflexivity
708               |assumption
709               |assumption
710               ]
711             ]
712           |reflexivity
713           ]
714         |reflexivity
715         ]
716       |assumption
717       ]
718     |assumption
719     ]
720   |intros.split
721     [split
722       [split
723         [split
724           [split
725             [apply (andb_true_true ? (p22 j i)).
726              rewrite < H3
727               [rewrite > H6.rewrite > H7.reflexivity
728               |assumption
729               |assumption
730               ]
731             |apply (andb_true_true_r (p21 j)).
732              rewrite < H3
733               [rewrite > H6.rewrite > H7.reflexivity
734               |assumption
735               |assumption
736               ]
737             ]
738           |reflexivity
739           ]
740         |reflexivity
741         ]
742       |assumption
743       ]
744     |assumption
745     ]
746   ]
747 qed. *)