]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/map_iter_p.ma
...
[helm.git] / helm / software / matita / library / nat / map_iter_p.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/permutation.ma".
16 include "nat/count.ma".
17
18 let rec map_iter_p n p (g:nat \to nat) (a:nat) f \def
19   match n with
20    [ O \Rightarrow a
21    | (S k) \Rightarrow 
22       match p (S k) with
23       [true \Rightarrow f (g (S k)) (map_iter_p k p g a f)
24       |false \Rightarrow map_iter_p k p g a f]
25    ].
26
27 theorem eq_map_iter_p: \forall g1,g2:nat \to nat.
28 \forall p:nat \to bool.
29 \forall f:nat \to nat \to nat. \forall a,n:nat.
30 (\forall m:nat. m \le n \to g1 m = g2 m) \to 
31 map_iter_p n p g1 a f = map_iter_p n p g2 a f.
32 intros 6.elim n
33   [simplify.reflexivity.
34   |simplify.elim (p (S n1))
35     [simplify.apply eq_f2
36       [apply H1.apply le_n
37       |simplify.apply H.intros.apply H1.
38        apply le_S.assumption
39       ]
40     |simplify.apply H.intros.apply H1.
41      apply le_S.assumption
42     ]
43  ]
44 qed.
45
46 (* useful since simplify simpifies too much *)
47
48 theorem map_iter_p_O: \forall p.\forall g.\forall f. \forall a:nat.
49 map_iter_p O p g a f = a.
50 intros.simplify.reflexivity.
51 qed.
52
53 theorem map_iter_p_S_true: \forall p.\forall g.\forall f. \forall a,n:nat.
54 p (S n) = true \to 
55 map_iter_p (S n) p g a f = f (g (S n)) (map_iter_p n p g a f).
56 intros.simplify.rewrite > H.reflexivity.
57 qed.
58
59 theorem map_iter_p_S_false: \forall p.\forall g.\forall f. \forall a,n:nat.
60 p (S n) = false \to 
61 map_iter_p (S n) p g a f = map_iter_p n p g a f.
62 intros.simplify.rewrite > H.reflexivity.
63 qed.
64
65 (* map_iter examples *)
66 definition pi_p \def \lambda p. \lambda n.
67 map_iter_p n p (\lambda n.n) (S O) times.
68
69 lemma pi_p_S: \forall n.\forall p.
70 pi_p p (S n) = 
71   match p (S n) with
72     [true \Rightarrow (S n)*(pi_p p n)
73     |false \Rightarrow (pi_p p n)
74     ].
75 intros.reflexivity.
76 qed.
77
78 lemma lt_O_pi_p: \forall n.\forall p.
79 O < pi_p p n.
80 intros.elim n
81   [simplify.apply le_n
82   |rewrite > pi_p_S.
83    elim p (S n1)
84     [change with (O < (S n1)*(pi_p p n1)).
85      rewrite >(times_n_O n1).
86      apply lt_times[apply le_n|assumption]
87     | assumption
88     ]
89   ]
90 qed.
91
92 let rec card n p \def 
93   match n with
94   [O \Rightarrow O
95   |(S m) \Rightarrow 
96       (bool_to_nat (p (S m))) + (card m p)].
97
98 lemma count_card: \forall p.\forall n.
99 p O = false \to count (S n) p = card n p.
100 intros.elim n
101   [simplify.rewrite > H. reflexivity
102   |simplify.
103    rewrite < plus_n_O.
104    apply eq_f.assumption
105   ]
106 qed.
107
108 lemma count_card1: \forall p.\forall n.
109 p O = false \to p n = false \to count n p = card n p.
110 intros 3.apply (nat_case n)
111   [intro.simplify.rewrite > H. reflexivity
112   |intros.rewrite > (count_card ? ? H).
113    simplify.rewrite > H1.reflexivity
114   ]
115 qed.
116  
117 lemma a_times_pi_p: \forall p. \forall a,n.
118 exp a (card n p) * pi_p p n = map_iter_p n p (\lambda n.a*n) (S O) times.
119 intros.elim n
120   [simplify.reflexivity
121   |simplify.apply (bool_elim ? (p (S n1)))
122     [intro.
123      change with 
124       (a*exp a (card n1 p) * ((S n1) * (pi_p p n1)) = 
125        a*(S n1)*map_iter_p n1 p (\lambda n.a*n) (S O) times).
126        rewrite < H.
127        autobatch
128     |intro.assumption
129     ]
130   ]
131 qed.
132
133 definition permut_p \def \lambda f. \lambda p:nat\to bool. \lambda n.
134 \forall i. i \le n \to p i = true \to ((f i \le n \land p (f i) = true)
135 \land (\forall j. p j = true \to j \le n \to i \neq j \to (f i \neq f j))).
136
137 definition extentional_eq_n \def \lambda f,g:nat \to nat.\lambda n.
138 \forall x. x \le n \to f x = g x.
139
140 lemma extentional_eq_n_to_permut_p: \forall f,g. \forall p. \forall n. 
141 extentional_eq_n f g n\to permut_p f p n \to permut_p g p n.
142 intros.unfold permut_p.
143 intros.
144 elim (H1 i H2 H3).
145 split
146   [elim H4.split
147     [rewrite < (H  i H2).assumption
148     |rewrite < (H  i H2).assumption
149     ]
150   |intros.
151    unfold.intro.apply (H5 j H6 H7 H8).
152      rewrite > (H  i H2).
153      rewrite > (H  j H7).assumption
154   ]
155 qed.
156
157 theorem permut_p_compose: \forall f,g.\forall p.\forall n.
158 permut_p f p n \to permut_p g p n \to permut_p (compose  ? ? ? g f) p n.
159 intros.unfold permut_p.intros.
160 elim (H i H2 H3).
161 elim H4.
162 elim (H1 (f i) H6 H7).
163 elim H8.
164 split
165   [split
166     [unfold compose.assumption
167     |unfold compose.rewrite < H11.reflexivity
168     ]
169   |intros.
170    unfold compose.
171    apply (H9 (f j))
172     [elim (H j H13 H12).elim H15.rewrite < H18.reflexivity
173     |elim (H j H13 H12).elim H15.assumption.
174     |apply (H5 j H12 H13 H14)
175     ]
176   ]
177 qed.
178
179 theorem permut_p_S_to_permut_p: \forall f.\forall p.\forall n.
180 permut_p f p (S n) \to (f (S n)) = (S n) \to permut_p f p n.
181 intros.
182 unfold permut_p.
183 intros.
184 split
185   [elim (H i (le_S i n H2) H3).split
186     [elim H4.
187      elim (le_to_or_lt_eq (f i) (S n))
188       [apply le_S_S_to_le.assumption
189       |absurd (f i = (S n))
190         [assumption
191         |rewrite < H1.
192          apply H5
193           [rewrite < H8.assumption
194           |apply le_n
195           |unfold.intro.
196            apply (not_le_Sn_n n).rewrite < H9.assumption
197           ]   
198         ]
199       |assumption
200       ]
201     |elim H4.assumption
202     ]
203   |intros.
204    elim (H i (le_S i n H2) H3).
205    apply H8
206     [assumption|apply le_S.assumption|assumption]
207   ]
208 qed.
209
210 lemma permut_p_transpose: \forall p.\forall i,j,n.
211 i \le n \to j \le n \to p i = p j \to
212 permut_p (transpose i j) p n.
213 unfold permut_p.intros.
214 split
215   [split
216     [unfold transpose.
217      apply (eqb_elim i1 i)
218       [intro.
219        apply (eqb_elim i1 j)
220         [simplify.intro.assumption
221         |simplify.intro.assumption
222         ]
223       |intro.
224        apply (eqb_elim i1 j)
225         [simplify.intro.assumption
226         |simplify.intro.assumption
227         ]
228       ]
229     |unfold transpose.
230      apply (eqb_elim i1 i)
231       [intro.
232        apply (eqb_elim i1 j)
233         [simplify.intro.rewrite < H6.assumption
234         |simplify.intro.rewrite < H2.rewrite < H5.assumption
235         ]
236       |intro.
237        apply (eqb_elim i1 j)
238         [simplify.intro.rewrite > H2.rewrite < H6.assumption
239         |simplify.intro.assumption
240         ]
241       ]
242     ]
243   |intros.unfold Not.
244    intro.apply H7.
245    apply (injective_transpose ? ? ? ? H8).
246   ]
247 qed.
248
249 theorem eq_map_iter_p_k: \forall f,g.\forall p.\forall a,k,n:nat.
250 p (S n-k) = true \to (\forall i. (S n)-k < i \to i \le (S n) \to (p i) = false) \to
251 map_iter_p (S n) p g a f = map_iter_p (S n-k) p g a f.
252 intros 5.
253 elim k 3
254   [rewrite < minus_n_O.reflexivity
255   |apply (nat_case n1)
256     [intros.
257      rewrite > map_iter_p_S_false
258       [reflexivity
259       |apply H2[simplify.apply lt_O_S.|apply le_n]
260       ]
261     |intros.
262      rewrite > map_iter_p_S_false
263       [rewrite > (H m H1)
264         [reflexivity
265         |intros.
266          apply (H2 i H3).
267          apply le_S.
268          assumption
269         ]
270       |apply H2[autobatch|apply le_n]
271       ]
272     ]
273   ]
274 qed.
275
276 theorem eq_map_iter_p_a: \forall p.\forall f.\forall g. \forall a,n:nat. 
277 (\forall i.i \le n \to p i = false) \to map_iter_p n p g a f = a.
278 intros 5.
279 elim n
280   [simplify.reflexivity
281   |rewrite > map_iter_p_S_false
282     [apply H.
283      intros.
284      apply H1.apply le_S.assumption
285     |apply H1.apply le_n
286     ]
287   ]
288 qed.
289  
290 theorem eq_map_iter_p_transpose: \forall p.\forall f.associative nat f \to
291 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. k < n \to
292 (p (S n) = true) \to (p (n-k)) = true \to (\forall i. n-k < i \to i \le n \to (p i) = false)
293 \to map_iter_p (S n) p g a f = map_iter_p (S n) p (\lambda m. g (transpose (n-k) (S n) m)) a f.
294 intros 8.
295 apply (nat_case n)
296   [intro.absurd (k < O)
297     [assumption|apply le_to_not_lt.apply le_O_n]
298   |intros.
299    rewrite > (map_iter_p_S_true ? ? ? ? ? H3).
300    rewrite > (map_iter_p_S_true ? ? ? ? ? H3).
301    rewrite > (eq_map_iter_p_k ? ? ? ? ? ? H4 H5).
302    rewrite > (eq_map_iter_p_k ? ? ? ? ? ? H4 H5).
303    generalize in match H4.
304    rewrite > minus_Sn_m
305     [intro.
306      rewrite > (map_iter_p_S_true ? ? ? ? ? H6).
307      rewrite > (map_iter_p_S_true ? ? ? ? ? H6).
308      rewrite > transpose_i_j_j.
309      rewrite > transpose_i_j_i.
310      cut (map_iter_p (m-k) p g a f =
311       map_iter_p (m-k) p (\lambda x.g (transpose (S(m-k)) (S(S m)) x)) a f)
312       [rewrite < Hcut.
313        rewrite < H.
314        rewrite < H1 in \vdash (? ? (? % ?) ?).
315        rewrite > H.
316        reflexivity
317       |apply eq_map_iter_p.
318        intros.unfold transpose.
319        cut (eqb m1 (S (m-k)) =false)
320         [cut (eqb m1 (S (S m)) =false)
321           [rewrite > Hcut.
322            rewrite > Hcut1.
323            reflexivity
324           |apply not_eq_to_eqb_false.
325            apply lt_to_not_eq.
326            apply (le_to_lt_to_lt ? m)
327             [apply (trans_le ? (m-k))
328               [assumption|autobatch]
329             |apply le_S.apply le_n
330             ]
331           ]
332         |apply not_eq_to_eqb_false.
333          apply lt_to_not_eq.
334          unfold.autobatch
335         ]
336       ]
337     |apply le_S_S_to_le.assumption
338     ]
339   ]
340 qed.
341
342 theorem eq_map_iter_p_transpose1: \forall p.\forall f.associative nat f \to
343 symmetric2 nat nat f \to \forall g. \forall a,k1,k2,n:nat. O < k1 \to k1 < k2 \to k2 \le n \to
344 (p k1) = true \to (p k2) = true \to (\forall i. k1 < i \to i < k2 \to (p i) = false)
345 \to map_iter_p n p g a f = map_iter_p n p (\lambda m. g (transpose k1 k2 m)) a f.
346 intros 10.
347 elim n 2
348   [absurd (k2 \le O)
349     [assumption|apply lt_to_not_le.apply (trans_lt ? k1 ? H2 H3)]
350   |apply (eqb_elim (S n1) k2)
351    [intro.
352     rewrite < H4.
353     intros.
354     cut (k1 = n1 - (n1 -k1))
355      [rewrite > Hcut.
356       apply (eq_map_iter_p_transpose p f H H1 g a (n1-k1))
357         [cut (k1 \le n1)[autobatch|autobatch]
358         |assumption
359         |rewrite < Hcut.assumption
360         |rewrite < Hcut.intros.
361          apply (H9 i H10).unfold.autobatch   
362        ]
363      |apply sym_eq.
364        apply plus_to_minus.
365        autobatch.
366      ]
367    |intros.
368      cut ((S n1) \neq k1)
369       [apply (bool_elim ? (p (S n1)))
370        [intro. 
371         rewrite > map_iter_p_S_true
372           [rewrite > map_iter_p_S_true
373             [cut ((transpose k1 k2 (S n1)) = (S n1))
374               [rewrite > Hcut1.
375                apply eq_f.
376                apply (H3 H5)
377                 [elim (le_to_or_lt_eq ? ? H6)
378                   [autobatch
379                   |absurd (S n1=k2)[apply sym_eq.assumption|assumption]
380                   ]
381                 |assumption
382                 |assumption
383                 |assumption
384                 ]
385               |unfold transpose.
386                rewrite > (not_eq_to_eqb_false ? ? Hcut).
387                rewrite > (not_eq_to_eqb_false ? ? H4).
388                reflexivity
389               ]
390             |assumption
391             ]
392           |assumption
393           ]
394         |intro.
395           rewrite > map_iter_p_S_false
396           [rewrite > map_iter_p_S_false
397             [apply (H3 H5)
398               [elim (le_to_or_lt_eq ? ? H6)
399                 [autobatch
400                 |absurd (S n1=k2)[apply sym_eq.assumption|assumption]
401                 ]
402               |assumption
403               |assumption
404               |assumption
405               ]
406             |assumption
407             ]
408           |assumption
409           ]
410         ]
411       |unfold.intro.
412        absurd (k1 < k2)
413         [assumption
414         |apply le_to_not_lt.
415          rewrite < H10.
416          assumption
417         ]
418       ]
419     ]
420   ]
421 qed.
422
423 lemma decidable_n:\forall p.\forall n.
424 (\forall m. m \le n \to (p m) = false) \lor 
425 (\exists m. m \le n \land (p m) = true \land 
426 \forall i. m < i \to i \le n \to (p i) = false).
427 intros.
428 elim n
429   [apply (bool_elim ? (p O))
430     [intro.right.
431      apply (ex_intro ? ? O).
432      split
433       [split[apply le_n|assumption]
434       |intros.absurd (O<i)[assumption|apply le_to_not_lt.assumption]
435       ]
436     |intro.left.
437      intros.apply (le_n_O_elim m H1).assumption
438     ]
439   |apply (bool_elim ? (p (S n1)))
440     [intro.right.
441      apply (ex_intro ? ? (S n1)).
442      split
443       [split[apply le_n|assumption]
444       |intros.absurd (S n1<i)[assumption|apply le_to_not_lt.assumption]
445       ]
446     |elim H
447       [left.
448        intros.
449        elim (le_to_or_lt_eq m (S n1) H3)
450         [apply H1.apply le_S_S_to_le.assumption
451         |rewrite > H4.assumption
452         ]
453       |right.
454        elim H1.elim H3.elim H4.
455        apply (ex_intro ? ? a).
456        split
457         [split[apply le_S.assumption|assumption]
458         |intros.elim (le_to_or_lt_eq i (S n1) H9)
459           [apply H5[assumption|apply le_S_S_to_le.assumption]
460           |rewrite > H10.assumption
461           ]
462         ]
463       ]
464     ]
465   ]
466 qed.
467
468 lemma decidable_n1:\forall p.\forall n,j. j \le n \to (p j)=true \to
469 (\forall m. j < m \to m \le n \to (p m) = false) \lor 
470 (\exists m. j < m \land m \le n \land (p m) = true \land 
471 \forall i. m < i \to i \le n \to (p i) = false).
472 intros.
473 elim (decidable_n p n)
474   [absurd ((p j)=true)
475     [assumption
476     |unfold.intro.
477      apply not_eq_true_false.
478      rewrite < H3.
479      apply H2.assumption
480     ]
481   |elim H2.clear H2.
482    apply (nat_compare_elim j a)
483     [intro.
484      right.
485      apply (ex_intro ? ? a).
486      elim H3.clear H3.
487      elim H4.clear H4.
488      split
489       [split
490         [split
491           [assumption|assumption]
492         |assumption
493         ]
494       |assumption
495       ]
496     |intro.
497      rewrite > H2.
498      left.
499      elim H3 2.assumption
500     |intro.
501      absurd (p j = true)
502       [assumption
503       |unfold.intro.
504        apply not_eq_true_false.
505        rewrite < H4.
506        elim H3.clear H3.
507        apply (H6 j H2).assumption
508       ]
509     ]
510   ]
511 qed.    
512
513 lemma decidable_n2:\forall p.\forall n,j. j \le n \to (p j)=true \to
514 (\forall m. j < m \to m \le n \to (p m) = false) \lor 
515 (\exists m. j < m \land m \le n \land (p m) = true \land 
516 \forall i. j < i \to i < m \to (p i) = false).
517 intros 3.
518 elim n
519   [left.
520    apply (le_n_O_elim j H).intros.
521    absurd (m \le O)
522     [assumption|apply lt_to_not_le.assumption]
523   |elim (le_to_or_lt_eq ? ? H1)
524     [cut (j \le n1)
525       [elim (H Hcut H2)
526         [apply (bool_elim ? (p (S n1)))
527           [intro.
528            right.
529            apply (ex_intro ? ? (S n1)).
530            split
531             [split
532               [split
533                 [assumption|apply le_n]
534               |assumption
535               ]
536             |intros.
537              apply (H4 i H6).
538              apply le_S_S_to_le.
539              assumption
540             ]
541           |intro.
542            left.
543            intros.
544            elim (le_to_or_lt_eq ? ? H7)
545             [apply H4
546               [assumption|apply le_S_S_to_le.assumption]
547             |rewrite > H8.assumption
548             ]
549           ]
550         |right.
551          elim H4.clear H4.
552          elim H5.clear H5.
553          elim H4.clear H4.
554          elim H5.clear H5.
555          apply (ex_intro ? ? a).
556          split
557           [split
558             [split[assumption|apply le_S.assumption]
559             |assumption
560             ]
561           |assumption
562           ]
563         ]
564       |apply le_S_S_to_le.
565        assumption
566       ]
567     |left.
568      intros.
569      absurd (j < m)
570       [assumption
571       |apply le_to_not_lt.
572        rewrite > H3.
573        assumption
574       ]
575     ]
576   ]
577 qed.
578
579 theorem eq_map_iter_p_transpose2: \forall p.\forall f.associative nat f \to
580 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le n \to
581 (p (S n) = true) \to (p k) = true 
582 \to map_iter_p (S n) p g a f = map_iter_p (S n) p (\lambda m. g (transpose k (S n) m)) a f.
583 intros 10.
584 cut (k = (S n)-(S n -k))
585   [generalize in match H3.clear H3.
586    generalize in match g.
587    generalize in match H2.clear H2.
588    rewrite > Hcut.
589    (*generalize in match Hcut.clear Hcut.*)
590    (* generalize in match H3.clear H3.*)
591    (* something wrong here 
592      rewrite > Hcut in \vdash (?\rarr ?\rarr %). *)
593    apply (nat_elim1 (S n - k)).
594      intros.
595      elim (decidable_n2 p n (S n -m) H4 H6)
596       [apply (eq_map_iter_p_transpose1 p f H H1 f1 a)
597         [assumption.
598         |unfold.autobatch.
599         |apply le_n
600         |assumption
601         |assumption
602         |intros.apply H7
603           [assumption|apply le_S_S_to_le.assumption]
604         ]
605       |elim H7.clear H7.
606        elim H8.clear H8.
607        elim H7.clear H7.
608        elim H8.clear H8.
609        apply (trans_eq  ? ? 
610         (map_iter_p (S n) p (\lambda i.f1 (transpose a1 (S n) (transpose (S n -m) a1 i))) a f))
611         [apply (trans_eq  ? ? 
612          (map_iter_p (S n) p (\lambda i.f1 (transpose a1 (S n) i)) a f))
613           [cut (a1 = (S n -(S n -a1)))
614             [rewrite > Hcut1.
615              apply H2
616               [apply lt_plus_to_lt_minus
617                 [apply le_S.assumption
618                 |rewrite < sym_plus.
619                  apply lt_minus_to_lt_plus.
620                  assumption
621                 ]
622               |rewrite < Hcut1.
623                apply (trans_lt ? (S n -m))[assumption|assumption]
624               |rewrite < Hcut1.assumption
625               |assumption
626               |rewrite < Hcut1.assumption
627               ]
628            |apply minus_m_minus_mn.
629             apply le_S.assumption
630            ]
631          |apply (eq_map_iter_p_transpose1 p f H H1)
632           [assumption
633           |assumption
634           |apply le_S.assumption
635           |assumption
636           |assumption
637           |assumption
638           ]
639         ]
640       |apply (trans_eq  ? ? 
641         (map_iter_p (S n) p (\lambda i.f1 (transpose a1 (S n) (transpose (S n -m) a1 (transpose (S n -(S n -a1)) (S n) i)))) a f)) 
642         [cut (a1 = (S n) -(S n -a1))
643           [apply H2 
644             [apply lt_plus_to_lt_minus
645               [apply le_S.assumption
646               |rewrite < sym_plus.
647                apply lt_minus_to_lt_plus.
648                assumption
649               ]
650             |rewrite < Hcut1.
651              apply (trans_lt ? (S n -m))[assumption|assumption]
652             |rewrite < Hcut1.assumption
653             |assumption
654             |rewrite < Hcut1.assumption
655             ]
656           |apply minus_m_minus_mn.
657            apply le_S.assumption
658           ]
659         |apply eq_map_iter_p.
660          cut (a1 = (S n) -(S n -a1))
661           [intros.
662            apply eq_f.
663            rewrite < Hcut1.
664            rewrite < transpose_i_j_j_i.
665            rewrite > (transpose_i_j_j_i (S n -m)).
666            rewrite > (transpose_i_j_j_i a1 (S n)).
667            rewrite > (transpose_i_j_j_i (S n -m)).
668            apply sym_eq.
669            apply eq_transpose
670             [unfold.intro.
671              apply (not_le_Sn_n n).
672              rewrite < H12.assumption
673             |unfold.intro.
674              apply (not_le_Sn_n n).
675              rewrite > H12.assumption
676             |unfold.intro.
677              apply (not_le_Sn_n a1).
678              rewrite < H12 in \vdash (? (? %) ?).assumption
679             ]
680           |apply minus_m_minus_mn.
681            apply le_S.assumption
682           ]
683         ]
684       ]
685     ]
686   |apply minus_m_minus_mn.
687    apply le_S.assumption
688   ]
689 qed.
690
691 theorem eq_map_iter_p_transpose3: \forall p.\forall f.associative nat f \to
692 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le (S n) \to
693 (p (S n) = true) \to (p k) = true 
694 \to map_iter_p (S n) p g a f = map_iter_p (S n) p (\lambda m. g (transpose k (S n) m)) a f.
695 intros.
696 elim (le_to_or_lt_eq ? ? H3)
697   [apply (eq_map_iter_p_transpose2 p f H H1 g a k n H2)
698     [apply le_S_S_to_le.assumption|assumption|assumption]
699   |rewrite > H6.
700    apply eq_map_iter_p.
701    intros.
702    apply eq_f.apply sym_eq. apply transpose_i_i. 
703   ]
704 qed.
705
706 lemma permut_p_O: \forall p.\forall h.\forall n.
707 permut_p h p n \to p O = false \to \forall m. (S m) \le n \to p (S m) = true \to O < h(S m).
708 intros.unfold permut_p in H.
709 apply not_le_to_lt.unfold.intro.
710 elim (H (S m) H2 H3).
711 elim H5.
712 absurd (p (h (S m)) = true)
713   [assumption
714   |apply (le_n_O_elim ? H4).
715    unfold.intro.
716    apply not_eq_true_false.
717    rewrite < H9.rewrite < H1.reflexivity
718   ]
719 qed.
720
721 theorem eq_map_iter_p_permut: \forall p.\forall f.associative nat f \to
722 symmetric2 nat nat f \to \forall n.\forall g. \forall h.\forall a:nat.
723 permut_p h p n \to p O = false \to
724 map_iter_p n p g a f = map_iter_p n p (compose ? ? ? g h) a f .
725 intros 5.
726 elim n
727   [simplify.reflexivity 
728   |apply (bool_elim ? (p (S n1)))
729     [intro.
730      apply (trans_eq ? ? (map_iter_p (S n1) p (\lambda m.g ((transpose (h (S n1)) (S n1)) m)) a f))
731       [unfold permut_p in H3.
732        elim (H3 (S n1) (le_n ?) H5).
733        elim H6. clear H6.
734        apply (eq_map_iter_p_transpose3 p f H H1 g a (h(S n1)) n1)
735         [apply (permut_p_O ? ? ? H3 H4)
736           [apply le_n|assumption]
737         |assumption
738         |assumption
739         |assumption
740         ]
741       |apply (trans_eq ? ? (map_iter_p (S n1) p (\lambda m.
742         (g(transpose (h (S n1)) (S n1) 
743          (transpose (h (S n1)) (S n1) (h m)))) ) a f))
744         [rewrite > (map_iter_p_S_true ? ? ? ? ? H5).
745          rewrite > (map_iter_p_S_true ? ? ? ? ? H5).
746          apply eq_f2
747           [rewrite > transpose_i_j_j.
748            rewrite > transpose_i_j_i.
749            rewrite > transpose_i_j_j.
750            reflexivity
751           |apply (H2 (\lambda m.(g(transpose (h (S n1)) (S n1) m))) ?)
752             [unfold.intros.
753              split
754               [split
755                 [simplify.
756                  unfold permut_p in H3.
757                  elim (H3 i (le_S ? ? H6) H7).
758                  elim H8. clear H8.
759                  elim (le_to_or_lt_eq ? ? H10)
760                   [unfold transpose.
761                    rewrite > (not_eq_to_eqb_false ? ? (lt_to_not_eq ? ? H8)). 
762                    cut (h i \neq h (S n1))
763                     [rewrite > (not_eq_to_eqb_false ? ? Hcut). 
764                      simplify.
765                      apply le_S_S_to_le.
766                      assumption
767                     |apply H9
768                       [apply H5
769                       |apply le_n
770                       |apply lt_to_not_eq.
771                        unfold.apply le_S_S.assumption
772                       ]
773                     ]
774                   |rewrite > H8.
775                    apply (eqb_elim (S n1) (h (S n1)))
776                     [intro.
777                      absurd (h i = h (S n1))
778                       [rewrite > H8.
779                        assumption
780                       |apply H9
781                         [assumption
782                         |apply le_n
783                         |apply lt_to_not_eq.
784                          unfold.apply le_S_S.assumption
785                         ]
786                       ]
787                     |intro.
788                      unfold transpose.
789                      rewrite > (not_eq_to_eqb_false ? ? H12).
790                      rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S n1))).
791                      simplify.
792                      elim (H3 (S n1) (le_n ? ) H5).
793                      elim H13.clear H13.
794                      elim (le_to_or_lt_eq ? ? H15)
795                       [apply le_S_S_to_le.assumption
796                       |apply False_ind.
797                        apply H12.
798                        apply sym_eq.assumption
799                       ]
800                     ]
801                   ]
802                 |simplify.
803                  unfold permut_p in H3.
804                  unfold transpose.
805                  apply (eqb_elim (h i) (S n1))
806                   [intro.
807                    apply (eqb_elim (h i) (h (S n1)))
808                     [intro.simplify.assumption
809                     |intro.simplify.
810                      elim (H3 (S n1) (le_n ? ) H5).
811                      elim H10. assumption
812                     ]
813                   |intro.
814                    apply (eqb_elim (h i) (h (S n1)))
815                     [intro.simplify.assumption
816                     |intro.simplify.
817                      elim (H3 i (le_S ? ? H6) H7).
818                      elim H10. assumption
819                     ]
820                   ]
821                 ]
822               |simplify.intros.unfold Not.intro.
823                unfold permut_p in H3.
824                elim (H3 i (le_S i ? H6) H7).
825                apply (H13 j H8 (le_S j ? H9) H10).
826                apply (injective_transpose ? ? ? ? H11)
827               ]
828             |assumption
829             ]
830           ]
831         |apply eq_map_iter_p.
832          intros.
833          rewrite > transpose_transpose.reflexivity
834         ]
835       ]
836   |intro.
837    rewrite > (map_iter_p_S_false ? ? ? ? ? H5).
838    rewrite > (map_iter_p_S_false ? ? ? ? ? H5).
839    apply H2
840     [unfold permut_p.
841      unfold permut_p in H3.
842      intros.
843      elim (H3 i (le_S i ? H6) H7).
844      elim H8.
845       split
846         [split
847           [elim (le_to_or_lt_eq ? ? H10)
848             [apply le_S_S_to_le.assumption
849             |absurd (p (h i) = true)
850               [assumption
851               |rewrite > H12.
852                rewrite > H5.
853                unfold.intro.apply not_eq_true_false.
854                apply sym_eq.assumption
855               ]
856             ]
857           |assumption
858           ]
859         |intros.
860          apply H9
861           [assumption|apply (le_S ? ? H13)|assumption]
862         ]
863       |assumption
864       ]
865     ]
866   ]           
867 qed.
868