1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 include "nat/compare.ma".
16 include "nat/sigma_and_pi.ma".
18 definition injn: (nat \to nat) \to nat \to Prop \def
19 \lambda f:nat \to nat.\lambda n:nat.\forall i,j:nat.
20 i \le n \to j \le n \to f i = f j \to i = j.
22 theorem injn_Sn_n: \forall f:nat \to nat. \forall n:nat.
23 injn f (S n) \to injn f n.unfold injn.
25 apply le_S.assumption.
26 apply le_S.assumption.
30 theorem injective_to_injn: \forall f:nat \to nat. \forall n:nat.
31 injective nat nat f \to injn f n.
32 unfold injective.unfold injn.intros.apply H.assumption.
35 definition permut : (nat \to nat) \to nat \to Prop
36 \def \lambda f:nat \to nat. \lambda m:nat.
37 (\forall i:nat. i \le m \to f i \le m )\land injn f m.
39 theorem permut_O_to_eq_O: \forall h:nat \to nat.
40 permut h O \to (h O) = O.
41 intros.unfold permut in H.
42 elim H.apply sym_eq.apply le_n_O_to_eq.
46 theorem permut_S_to_permut: \forall f:nat \to nat. \forall m:nat.
47 permut f (S m) \to f (S m) = (S m) \to permut f m.
51 cut (f i < S m \lor f i = S m).
53 apply le_S_S_to_le.assumption.
55 apply (not_le_Sn_n m).
57 rewrite > Hcut1.assumption.
58 apply H3.apply le_n.apply le_S.assumption.
59 rewrite > H5.assumption.
60 apply le_to_or_lt_eq.apply H2.apply le_S.assumption.
61 apply (injn_Sn_n f m H3).
66 definition transpose : nat \to nat \to nat \to nat \def
73 | false \Rightarrow n]].
75 notation < "(❲i↹j❳)n" with precedence 71
76 for @{ 'transposition $i $j $n}.
78 notation < "(❲i \atop j❳)n" with precedence 71
79 for @{ 'transposition $i $j $n}.
81 interpretation "natural transposition" 'transposition i j n = (transpose i j n).
83 lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j.
84 intros.unfold transpose.
85 rewrite > (eqb_n_n i).simplify. reflexivity.
88 lemma transpose_i_j_j: \forall i,j:nat. transpose i j j = i.
89 intros.unfold transpose.
90 apply (eqb_elim j i).simplify.intro.assumption.
91 rewrite > (eqb_n_n j).simplify.
95 theorem transpose_i_i: \forall i,n:nat. (transpose i i n) = n.
96 intros.unfold transpose.
98 intro.simplify.apply sym_eq. assumption.
99 intro.simplify.reflexivity.
102 theorem transpose_i_j_j_i: \forall i,j,n:nat.
103 transpose i j n = transpose j i n.
104 intros.unfold transpose.
105 apply (eqb_elim n i).
106 apply (eqb_elim n j).
107 intros. simplify.rewrite < H. rewrite < H1.
109 intros.simplify.reflexivity.
110 apply (eqb_elim n j).
111 intros.simplify.reflexivity.
112 intros.simplify.reflexivity.
115 theorem transpose_transpose: \forall i,j,n:nat.
116 (transpose i j (transpose i j n)) = n.
117 intros.unfold transpose. unfold transpose.
118 apply (eqb_elim n i).simplify.
120 apply (eqb_elim j i).
121 simplify.intros.rewrite > H. rewrite > H1.reflexivity.
122 rewrite > (eqb_n_n j).simplify.intros.
125 apply (eqb_elim n j).simplify.
126 rewrite > (eqb_n_n i).intros.simplify.
127 apply sym_eq. assumption.
129 rewrite > (not_eq_to_eqb_false n i H1).
130 rewrite > (not_eq_to_eqb_false n j H).
131 simplify.reflexivity.
134 theorem injective_transpose : \forall i,j:nat.
135 injective nat nat (transpose i j).
138 rewrite < (transpose_transpose i j x).
139 rewrite < (transpose_transpose i j y).
140 apply eq_f.assumption.
143 variant inj_transpose: \forall i,j,n,m:nat.
144 transpose i j n = transpose i j m \to n = m \def
147 theorem permut_transpose: \forall i,j,n:nat. i \le n \to j \le n \to
148 permut (transpose i j) n.
149 unfold permut.intros.
150 split.unfold transpose.
152 elim (eqb i1 i).simplify.assumption.
153 elim (eqb i1 j).simplify.assumption.
155 apply (injective_to_injn (transpose i j) n).
156 apply injective_transpose.
159 theorem permut_fg: \forall f,g:nat \to nat. \forall n:nat.
160 permut f n \to permut g n \to permut (\lambda m.(f(g m))) n.
161 unfold permut. intros.
163 split.intros.simplify.apply H2.
166 apply H5.assumption.assumption.
167 apply H3.apply H4.assumption.apply H4.assumption.
171 theorem permut_transpose_l:
172 \forall f:nat \to nat. \forall m,i,j:nat.
173 i \le m \to j \le m \to permut f m \to permut (\lambda n.transpose i j (f n)) m.
174 intros.apply (permut_fg (transpose i j) f m ? ?).
175 apply permut_transpose.assumption.assumption.
179 theorem permut_transpose_r:
180 \forall f:nat \to nat. \forall m,i,j:nat.
181 i \le m \to j \le m \to permut f m \to permut (\lambda n.f (transpose i j n)) m.
182 intros.apply (permut_fg f (transpose i j) m ? ?).
183 assumption.apply permut_transpose.assumption.assumption.
186 theorem eq_transpose : \forall i,j,k,n:nat. \lnot j=i \to
187 \lnot i=k \to \lnot j=k \to
188 transpose i j n = transpose i k (transpose k j (transpose i k n)).
189 (* uffa: triplo unfold? *)
190 intros.unfold transpose.unfold transpose.unfold transpose.
191 apply (eqb_elim n i).intro.
192 simplify.rewrite > (eqb_n_n k).
193 simplify.rewrite > (not_eq_to_eqb_false j i H).
194 rewrite > (not_eq_to_eqb_false j k H2).
196 intro.apply (eqb_elim n j).
200 rewrite > (not_eq_to_eqb_false n k Hcut).
202 rewrite > (not_eq_to_eqb_false n k Hcut).
203 rewrite > (eq_to_eqb_true n j H4).
205 rewrite > (not_eq_to_eqb_false k i).
206 rewrite > (eqb_n_n k).
207 simplify.reflexivity.
208 unfold Not.intro.apply H1.apply sym_eq.assumption.
210 unfold Not.intro.apply H2.apply (trans_eq ? ? n).
211 apply sym_eq.assumption.assumption.
212 intro.apply (eqb_elim n k).intro.
214 rewrite > (not_eq_to_eqb_false i k H1).
215 rewrite > (not_eq_to_eqb_false i j).
217 rewrite > (eqb_n_n i).
219 unfold Not.intro.apply H.apply sym_eq.assumption.
221 rewrite > (not_eq_to_eqb_false n k H5).
222 rewrite > (not_eq_to_eqb_false n j H4).
224 rewrite > (not_eq_to_eqb_false n i H3).
225 rewrite > (not_eq_to_eqb_false n k H5).
226 simplify.reflexivity.
229 theorem permut_S_to_permut_transpose: \forall f:nat \to nat.
230 \forall m:nat. permut f (S m) \to permut (\lambda n.transpose (f (S m)) (S m)
232 unfold permut.intros.
234 split.intros.simplify.unfold transpose.
235 apply (eqb_elim (f i) (f (S m))).
236 intro.apply False_ind.
238 apply (not_le_Sn_n m).
239 rewrite < Hcut.assumption.
240 apply H2.apply le_S.assumption.apply le_n.assumption.
242 apply (eqb_elim (f i) (S m)).
244 cut (f (S m) \lt (S m) \lor f (S m) = (S m)).
245 elim Hcut.apply le_S_S_to_le.assumption.
246 apply False_ind.apply H4.rewrite > H6.assumption.
247 apply le_to_or_lt_eq.apply H1.apply le_n.
249 cut (f i \lt (S m) \lor f i = (S m)).
250 elim Hcut.apply le_S_S_to_le.assumption.
251 apply False_ind.apply H5.assumption.
252 apply le_to_or_lt_eq.apply H1.apply le_S.assumption.
254 apply H2.apply le_S.assumption.apply le_S.assumption.
255 apply (inj_transpose (f (S m)) (S m)).
259 (* bounded bijectivity *)
261 definition bijn : (nat \to nat) \to nat \to Prop \def
262 \lambda f:nat \to nat. \lambda n. \forall m:nat. m \le n \to
263 ex nat (\lambda p. p \le n \land f p = m).
265 theorem eq_to_bijn: \forall f,g:nat\to nat. \forall n:nat.
266 (\forall i:nat. i \le n \to (f i) = (g i)) \to
267 bijn f n \to bijn g n.
268 intros 4.unfold bijn.
270 apply (ex_intro ? ? a).
271 rewrite < (H a).assumption.
272 elim H3.assumption.assumption.
275 theorem bijn_Sn_n: \forall f:nat \to nat. \forall n:nat.
276 bijn f (S n) \to f (S n) = (S n) \to bijn f n.
277 unfold bijn.intros.elim (H m).
279 apply (ex_intro ? ? a).split.
280 cut (a < S n \lor a = S n).
281 elim Hcut.apply le_S_S_to_le.assumption.
283 apply (not_le_Sn_n n).
284 rewrite < H1.rewrite < H6.rewrite > H5.assumption.
285 apply le_to_or_lt_eq.assumption.assumption.
286 apply le_S.assumption.
289 theorem bijn_n_Sn: \forall f:nat \to nat. \forall n:nat.
290 bijn f n \to f (S n) = (S n) \to bijn f (S n).
292 cut (m < S n \lor m = S n).
296 apply (ex_intro ? ? a).split.
297 apply le_S.assumption.assumption.
298 apply le_S_S_to_le.assumption.
299 apply (ex_intro ? ? (S n)).
301 rewrite > H3.assumption.
302 apply le_to_or_lt_eq.assumption.
305 theorem bijn_fg: \forall f,g:nat\to nat. \forall n:nat.
306 bijn f n \to bijn g n \to bijn (\lambda p.f(g p)) n.
311 apply (ex_intro ? ? a1).
313 rewrite > H8.assumption.
314 assumption.assumption.
317 theorem bijn_transpose : \forall n,i,j. i \le n \to j \le n \to
318 bijn (transpose i j) n.
319 intros.unfold bijn.unfold transpose.intros.
320 cut (m = i \lor \lnot m = i).
322 apply (ex_intro ? ? j).
324 apply (eqb_elim j i).
325 intro.simplify.rewrite > H3.rewrite > H4.reflexivity.
326 rewrite > (eqb_n_n j).simplify.
327 intros. apply sym_eq.assumption.
328 cut (m = j \lor \lnot m = j).
330 apply (ex_intro ? ? i).
332 rewrite > (eqb_n_n i).simplify.
333 apply sym_eq. assumption.
334 apply (ex_intro ? ? m).
336 rewrite > (not_eq_to_eqb_false m i).
337 rewrite > (not_eq_to_eqb_false m j).
338 simplify. reflexivity.
341 apply (decidable_eq_nat m j).
342 apply (decidable_eq_nat m i).
345 theorem bijn_transpose_r: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
346 bijn f n \to bijn (\lambda p.f (transpose i j p)) n.
348 apply (bijn_fg f ?).assumption.
349 apply (bijn_transpose n i j).assumption.assumption.
352 theorem bijn_transpose_l: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
353 bijn f n \to bijn (\lambda p.transpose i j (f p)) n.
356 apply (bijn_transpose n i j).assumption.assumption.
360 theorem permut_to_bijn: \forall n:nat.\forall f:nat\to nat.
361 permut f n \to bijn f n.
363 elim n.unfold bijn.intros.
364 apply (ex_intro ? ? m).
366 apply (le_n_O_elim m ? (\lambda p. f p = p)).
367 assumption.unfold permut in H.
368 elim H.apply sym_eq. apply le_n_O_to_eq.apply H2.apply le_n.
369 apply (eq_to_bijn (\lambda p.
370 (transpose (f (S n1)) (S n1)) (transpose (f (S n1)) (S n1) (f p))) f).
371 intros.apply transpose_transpose.
372 apply (bijn_fg (transpose (f (S n1)) (S n1))).
373 apply bijn_transpose.
375 elim H1.apply H2.apply le_n.apply le_n.
378 apply permut_S_to_permut_transpose.
379 assumption.unfold transpose.
380 rewrite > (eqb_n_n (f (S n1))).simplify.reflexivity.
383 let rec invert_permut n f m \def
384 match eqb m (f n) with
389 |(S p) \Rightarrow invert_permut p f m]].
391 theorem invert_permut_f: \forall f:nat \to nat. \forall n,m:nat.
392 m \le n \to injn f n\to invert_permut n f (f m) = m.
397 rewrite > (eqb_n_n (f O)).simplify.reflexivity.
399 rewrite > (eqb_n_n (f (S m1))).simplify.reflexivity.
401 rewrite > (not_eq_to_eqb_false (f m) (f (S n1))).
403 apply injn_Sn_n. assumption.
404 unfold Not.intro.absurd (m = S n1).
405 apply H3.apply le_S.assumption.apply le_n.assumption.
407 apply (not_le_Sn_n n1).rewrite < H5.assumption.
410 theorem injective_invert_permut: \forall f:nat \to nat. \forall n:nat.
411 permut f n \to injn (invert_permut n f) n.
416 generalize in match (Hcut i H1).intro.
417 generalize in match (Hcut j H2).intro.
423 rewrite < (invert_permut_f f n a).
424 rewrite < (invert_permut_f f n a1).
427 assumption.assumption.
428 unfold permut in H.elim H. assumption.
430 unfold permut in H.elim H. assumption.
431 apply permut_to_bijn.assumption.
434 theorem permut_invert_permut: \forall f:nat \to nat. \forall n:nat.
435 permut f n \to permut (invert_permut n f) n.
436 intros.unfold permut.split.
437 intros.simplify.elim n.
438 simplify.elim (eqb i (f O)).simplify.apply le_n.simplify.apply le_n.
439 simplify.elim (eqb i (f (S n1))).simplify.apply le_n.
440 simplify.apply le_S. assumption.
441 apply injective_invert_permut.assumption.
444 theorem f_invert_permut: \forall f:nat \to nat. \forall n,m:nat.
445 m \le n \to permut f n\to f (invert_permut n f m) = m.
447 apply (injective_invert_permut f n H1).
448 unfold permut in H1.elim H1.
450 cut (permut (invert_permut n f) n).unfold permut in Hcut.
451 elim Hcut.apply H4.assumption.
452 apply permut_invert_permut.assumption.assumption.
453 apply invert_permut_f.
454 cut (permut (invert_permut n f) n).unfold permut in Hcut.
455 elim Hcut.apply H2.assumption.
456 apply permut_invert_permut.assumption.
457 unfold permut in H1.elim H1.assumption.
460 theorem permut_n_to_eq_n: \forall h:nat \to nat.\forall n:nat.
461 permut h n \to (\forall m:nat. m < n \to h m = m) \to h n = n.
462 intros.unfold permut in H.elim H.
463 cut (invert_permut n h n < n \lor invert_permut n h n = n).
465 rewrite < (f_invert_permut h n n) in \vdash (? ? ? %).
467 rewrite < (f_invert_permut h n n) in \vdash (? ? % ?).
468 apply H1.assumption.apply le_n.assumption.apply le_n.assumption.
469 rewrite < H4 in \vdash (? ? % ?).
470 apply (f_invert_permut h).apply le_n.assumption.
471 apply le_to_or_lt_eq.
472 cut (permut (invert_permut n h) n).
473 unfold permut in Hcut.elim Hcut.
475 apply permut_invert_permut.assumption.
478 theorem permut_n_to_le: \forall h:nat \to nat.\forall k,n:nat.
479 k \le n \to permut h n \to (\forall m:nat. m < k \to h m = m) \to
480 \forall j. k \le j \to j \le n \to k \le h j.
481 intros.unfold permut in H1.elim H1.
482 cut (h j < k \lor \not(h j < k)).
483 elim Hcut.absurd (k \le j).assumption.
485 cut (h j = j).rewrite < Hcut1.assumption.
486 apply H6.apply H5.assumption.assumption.
488 apply not_lt_to_le.assumption.
489 apply (decidable_lt (h j) k).
494 let rec map_iter_i k (g:nat \to nat) f (i:nat) \def
497 | (S k) \Rightarrow f (g (S (k+i))) (map_iter_i k g f i)].
499 theorem eq_map_iter_i: \forall g1,g2:nat \to nat.
500 \forall f:nat \to nat \to nat. \forall n,i:nat.
501 (\forall m:nat. i\le m \to m \le n+i \to g1 m = g2 m) \to
502 map_iter_i n g1 f i = map_iter_i n g2 f i.
503 intros 5.elim n.simplify.apply H.apply le_n.
504 apply le_n.simplify.apply eq_f2.apply H1.simplify.
505 apply le_S.apply le_plus_n.simplify.apply le_n.
506 apply H.intros.apply H1.assumption.simplify.apply le_S.assumption.
509 (* map_iter examples *)
511 theorem eq_map_iter_i_sigma: \forall g:nat \to nat. \forall n,m:nat.
512 map_iter_i n g plus m = sigma n g m.
513 intros.elim n.simplify.reflexivity.
515 apply eq_f.assumption.
518 theorem eq_map_iter_i_pi: \forall g:nat \to nat. \forall n,m:nat.
519 map_iter_i n g times m = pi n g m.
520 intros.elim n.simplify.reflexivity.
522 apply eq_f.assumption.
525 theorem eq_map_iter_i_fact: \forall n:nat.
526 map_iter_i n (\lambda m.m) times (S O) = (S n)!.
528 simplify.reflexivity.
530 (((S n1)+(S O))*(map_iter_i n1 (\lambda m.m) times (S O)) = (S(S n1))*(S n1)!).
531 rewrite < plus_n_Sm.rewrite < plus_n_O.
532 apply eq_f.assumption.
535 theorem eq_map_iter_i_transpose_l : \forall f:nat\to nat \to nat.associative nat f \to
536 symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k:nat.
537 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose (k+n) (S k+n) m)) f n.
538 intros.apply (nat_case1 k).
539 intros.simplify.fold simplify (transpose n (S n) (S n)).
540 rewrite > transpose_i_j_i.
541 rewrite > transpose_i_j_j.
545 (f (g (S (S (m+n)))) (f (g (S (m+n))) (map_iter_i m g f n)) =
546 f (g (transpose (S m + n) (S (S m) + n) (S (S m)+n)))
547 (f (g (transpose (S m + n) (S (S m) + n) (S m+n)))
548 (map_iter_i m (\lambda m1. g (transpose (S m+n) (S (S m)+n) m1)) f n))).
549 rewrite > transpose_i_j_i.
550 rewrite > transpose_i_j_j.
553 rewrite < (H1 (g (S m + n))).
556 intros.simplify.unfold transpose.
557 rewrite > (not_eq_to_eqb_false m1 (S m+n)).
558 rewrite > (not_eq_to_eqb_false m1 (S (S m)+n)).
561 apply (lt_to_not_eq m1 (S ((S m)+n))).
562 unfold lt.apply le_S_S.change with (m1 \leq S (m+n)).apply le_S.assumption.
563 apply (lt_to_not_eq m1 (S m+n)).
564 simplify.unfold lt.apply le_S_S.assumption.
567 theorem eq_map_iter_i_transpose_i_Si : \forall f:nat\to nat \to nat.associative nat f \to
568 symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k,i:nat. n \le i \to i \le k+n \to
569 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S i) m)) f n.
570 intros 6.elim k.cut (i=n).
572 apply (eq_map_iter_i_transpose_l f H H1 g n O).
573 apply antisymmetric_le.assumption.assumption.
574 cut (i < S n1 + n \lor i = S n1 + n).
577 (f (g (S (S n1)+n)) (map_iter_i (S n1) g f n) =
578 f (g (transpose i (S i) (S (S n1)+n))) (map_iter_i (S n1) (\lambda m. g (transpose i (S i) m)) f n)).
579 apply eq_f2.unfold transpose.
580 rewrite > (not_eq_to_eqb_false (S (S n1)+n) i).
581 rewrite > (not_eq_to_eqb_false (S (S n1)+n) (S i)).
582 simplify.reflexivity.
583 simplify.unfold Not.intro.
584 apply (lt_to_not_eq i (S n1+n)).assumption.
585 apply inj_S.apply sym_eq. assumption.
586 simplify.unfold Not.intro.
587 apply (lt_to_not_eq i (S (S n1+n))).simplify.unfold lt.
588 apply le_S_S.assumption.
589 apply sym_eq. assumption.
590 apply H2.assumption.apply le_S_S_to_le.
593 apply (eq_map_iter_i_transpose_l f H H1 g n (S n1)).
594 apply le_to_or_lt_eq.assumption.
597 theorem eq_map_iter_i_transpose:
598 \forall f:nat\to nat \to nat.
599 associative nat f \to symmetric2 nat nat f \to \forall n,k,o:nat.
600 \forall g:nat \to nat. \forall i:nat. n \le i \to S (o + i) \le S k+n \to
601 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S(o + i)) m)) f n.
605 apply (nat_case m ?).
607 apply (eq_map_iter_i_transpose_i_Si ? H H1).
608 exact H3.apply le_S_S_to_le.assumption.
610 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n)).
612 unfold lt. apply le_n.assumption.
613 apply (trans_le ? (S(S (m1+i)))).
614 apply le_S.apply le_n.assumption.
615 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
616 (transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n)).
617 apply (H2 O ? ? (S(m1+i))).
618 unfold lt.apply le_S_S.apply le_O_n.id.
619 apply (trans_le ? i).assumption.
620 change with (i \le (S m1)+i).apply le_plus_n.
622 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
623 (transpose i (S(m1 + i))
624 (transpose (S(m1 + i)) (S(S(m1 + i)))
625 (transpose i (S(m1 + i)) m)))) f n)).
627 unfold lt. apply le_n.assumption.
628 apply (trans_le ? (S(S (m1+i)))).
629 apply le_S.apply le_n.assumption.
632 apply sym_eq. apply eq_transpose.
634 apply (not_le_Sn_n i).
635 rewrite < H7 in \vdash (? ? %).
636 apply le_S_S.apply le_S.
639 apply (not_le_Sn_n i).
640 rewrite > H7 in \vdash (? ? %).
644 apply (not_eq_n_Sn (S m1+i)).
645 apply sym_eq.assumption.
648 theorem eq_map_iter_i_transpose1: \forall f:nat\to nat \to nat.associative nat f \to
649 symmetric2 nat nat f \to \forall n,k,i,j:nat.
650 \forall g:nat \to nat. n \le i \to i < j \to j \le S k+n \to
651 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
654 cut ((S i) < j \lor (S i) = j).
656 cut (j = S ((j - (S i)) + i)).
658 apply (eq_map_iter_i_transpose f H H1 n k (j - (S i)) g i).
660 rewrite < Hcut1.assumption.
662 apply plus_minus_m_m.apply lt_to_le.assumption.
664 apply (eq_map_iter_i_transpose_i_Si f H H1 g).
666 assumption.apply le_S_S_to_le.
667 apply (trans_le ? j).assumption.assumption.
668 apply le_to_or_lt_eq.assumption.
671 theorem eq_map_iter_i_transpose2: \forall f:nat\to nat \to nat.associative nat f \to
672 symmetric2 nat nat f \to \forall n,k,i,j:nat.
673 \forall g:nat \to nat. n \le i \to i \le (S k+n) \to n \le j \to j \le (S k+n) \to
674 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
676 apply (nat_compare_elim i j).
677 intro.apply (eq_map_iter_i_transpose1 f H H1 n k i j g H2 H6 H5).
679 apply eq_map_iter_i.intros.
680 rewrite > (transpose_i_i j).reflexivity.
682 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m:nat.g (transpose j i m)) f n)).
683 apply (eq_map_iter_i_transpose1 f H H1 n k j i g H4 H6 H3).
685 intros.apply eq_f.apply transpose_i_j_j_i.
688 theorem permut_to_eq_map_iter_i:\forall f:nat\to nat \to nat.associative nat f \to
689 symmetric2 nat nat f \to \forall k,n:nat.\forall g,h:nat \to nat.
690 permut h (k+n) \to (\forall m:nat. m \lt n \to h m = m) \to
691 map_iter_i k g f n = map_iter_i k (\lambda m.g(h m)) f n.
693 [simplify.rewrite > (permut_n_to_eq_n h)
694 [reflexivity|assumption|assumption]
695 |apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.g ((transpose (h (S n+n1)) (S n+n1)) m)) f n1))
696 [unfold permut in H3.
698 apply (eq_map_iter_i_transpose2 f H H1 n1 n ? ? g)
699 [apply (permut_n_to_le h n1 (S n+n1))
700 [apply le_plus_n|assumption|assumption|apply le_plus_n|apply le_n]
705 |apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.
706 (g(transpose (h (S n+n1)) (S n+n1)
707 (transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1))
708 [simplify.fold simplify (transpose (h (S n+n1)) (S n+n1) (S n+n1)).
711 rewrite > transpose_i_j_j.
712 rewrite > transpose_i_j_i.
713 rewrite > transpose_i_j_j.
715 |apply (H2 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m))))
716 [apply permut_S_to_permut_transpose.assumption
719 rewrite > (not_eq_to_eqb_false (h m) (h (S n+n1)))
720 [rewrite > (not_eq_to_eqb_false (h m) (S n+n1))
721 [simplify.apply H4.assumption
724 apply (trans_lt ? n1)
725 [assumption|simplify.unfold lt.apply le_S_S.apply le_plus_n]
729 |unfold permut in H3.elim H3.
730 simplify.unfold Not.intro.
731 apply (lt_to_not_eq m (S n+n1))
732 [apply (trans_lt ? n1)
733 [assumption|simplify.unfold lt.apply le_S_S.apply le_plus_n]
735 apply (H7 m (S n+n1))
736 [apply (trans_le ? n1)
737 [apply lt_to_le.assumption|apply le_plus_n]
745 |apply eq_map_iter_i.intros.
746 rewrite > transpose_transpose.reflexivity