helm/software/matita/library/nat/permutation.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 set "baseuri" "cic:/matita/nat/permutation".
  16
  17 include "nat/compare.ma".
  18 include "nat/sigma_and_pi.ma".
  19
  20 definition injn: (nat \to nat) \to nat \to Prop \def
  21 \lambda f:nat \to nat.\lambda n:nat.\forall i,j:nat.
  22 i \le n \to j \le n \to f i = f j \to i = j.
  23
  24 theorem injn_Sn_n: \forall f:nat \to nat. \forall n:nat.
  25 injn f (S n) \to injn f n.unfold injn.
  26 intros.apply H.
  27 apply le_S.assumption.
  28 apply le_S.assumption.
  29 assumption.
  30 qed.
  31
  32 theorem injective_to_injn: \forall f:nat \to nat. \forall n:nat.
  33 injective nat nat f \to injn f n.
  34 unfold injective.unfold injn.intros.apply H.assumption.
  35 qed.
  36
  37 definition permut : (nat \to nat) \to nat \to Prop
  38 \def \lambda f:nat \to nat. \lambda m:nat.
  39 (\forall i:nat. i \le m \to f i \le m )\land injn f m.
  40
  41 theorem permut_O_to_eq_O: \forall h:nat \to nat.
  42 permut h O \to (h O) = O.
  43 intros.unfold permut in H.
  44 elim H.apply sym_eq.apply le_n_O_to_eq.
  45 apply H1.apply le_n.
  46 qed.
  47
  48 theorem permut_S_to_permut: \forall f:nat \to nat. \forall m:nat.
  49 permut f (S m) \to f (S m) = (S m) \to permut f m.
  50 unfold permut.intros.
  51 elim H.
  52 split.intros.
  53 cut (f i < S m \lor f i = S m).
  54 elim Hcut.
  55 apply le_S_S_to_le.assumption.
  56 apply False_ind.
  57 apply (not_le_Sn_n m).
  58 cut ((S m) = i).
  59 rewrite > Hcut1.assumption.
  60 apply H3.apply le_n.apply le_S.assumption.
  61 rewrite > H5.assumption.
  62 apply le_to_or_lt_eq.apply H2.apply le_S.assumption.
  63 apply (injn_Sn_n f m H3).
  64 qed.
  65
  66 (* transpositions *)
  67
  68 definition transpose : nat \to nat \to nat \to nat \def
  69 \lambda i,j,n:nat.
  70 match eqb n i with
  71   [ true \Rightarrow j
  72   | false \Rightarrow
  73       match eqb n j with
  74       [ true \Rightarrow i
  75       | false \Rightarrow n]].
  76
  77 lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j.
  78 intros.unfold transpose.
  79 rewrite > (eqb_n_n i).simplify. reflexivity.
  80 qed.
  81
  82 lemma transpose_i_j_j: \forall i,j:nat. transpose i j j = i.
  83 intros.unfold transpose.
  84 apply (eqb_elim j i).simplify.intro.assumption.
  85 rewrite > (eqb_n_n j).simplify.
  86 intros. reflexivity.
  87 qed.
  88
  89 theorem transpose_i_i:  \forall i,n:nat. (transpose  i i n) = n.
  90 intros.unfold transpose.
  91 apply (eqb_elim n i).
  92 intro.simplify.apply sym_eq. assumption.
  93 intro.simplify.reflexivity.
  94 qed.
  95
  96 theorem transpose_i_j_j_i: \forall i,j,n:nat.
  97 transpose i j n = transpose j i n.
  98 intros.unfold transpose.
  99 apply (eqb_elim n i).
 100 apply (eqb_elim n j).
 101 intros. simplify.rewrite < H. rewrite < H1.
 102 reflexivity.
 103 intros.simplify.reflexivity.
 104 apply (eqb_elim n j).
 105 intros.simplify.reflexivity.
 106 intros.simplify.reflexivity.
 107 qed.
 108
 109 theorem transpose_transpose: \forall i,j,n:nat.
 110 (transpose i j (transpose i j n)) = n.
 111 intros.unfold transpose. unfold transpose.
 112 apply (eqb_elim n i).simplify.
 113 intro.
 114 apply (eqb_elim j i).
 115 simplify.intros.rewrite > H. rewrite > H1.reflexivity.
 116 rewrite > (eqb_n_n j).simplify.intros.
 117 apply sym_eq.
 118 assumption.
 119 apply (eqb_elim n j).simplify.
 120 rewrite > (eqb_n_n i).intros.simplify.
 121 apply sym_eq. assumption.
 122 simplify.intros.
 123 rewrite > (not_eq_to_eqb_false n i H1).
 124 rewrite > (not_eq_to_eqb_false n j H).
 125 simplify.reflexivity.
 126 qed.
 127
 128 theorem injective_transpose : \forall i,j:nat.
 129 injective nat nat (transpose i j).
 130 unfold injective.
 131 intros.
 132 rewrite < (transpose_transpose i j x).
 133 rewrite < (transpose_transpose i j y).
 134 apply eq_f.assumption.
 135 qed.
 136
 137 variant inj_transpose: \forall i,j,n,m:nat.
 138 transpose i j n = transpose i j m \to n = m \def
 139 injective_transpose.
 140
 141 theorem permut_transpose: \forall i,j,n:nat. i \le n \to j \le n \to
 142 permut (transpose i j) n.
 143 unfold permut.intros.
 144 split.unfold transpose.
 145 intros.
 146 elim (eqb i1 i).simplify.assumption.
 147 elim (eqb i1 j).simplify.assumption.
 148 simplify.assumption.
 149 apply (injective_to_injn (transpose i j) n).
 150 apply injective_transpose.
 151 qed.
 152
 153 theorem permut_fg: \forall f,g:nat \to nat. \forall n:nat.
 154 permut f n \to permut g n \to permut (\lambda m.(f(g m))) n.
 155 unfold permut. intros.
 156 elim H.elim H1.
 157 split.intros.simplify.apply H2.
 158 apply H4.assumption.
 159 simplify.intros.
 160 apply H5.assumption.assumption.
 161 apply H3.apply H4.assumption.apply H4.assumption.
 162 assumption.
 163 qed.
 164
 165 theorem permut_transpose_l:
 166 \forall f:nat \to nat. \forall m,i,j:nat.
 167 i \le m \to j \le m \to permut f m \to permut (\lambda n.transpose i j (f n)) m.
 168 intros.apply (permut_fg (transpose i j) f m ? ?).
 169 apply permut_transpose.assumption.assumption.
 170 assumption.
 171 qed.
 172
 173 theorem permut_transpose_r:
 174 \forall f:nat \to nat. \forall m,i,j:nat.
 175 i \le m \to j \le m \to permut f m \to permut (\lambda n.f (transpose i j n)) m.
 176 intros.apply (permut_fg f (transpose i j) m ? ?).
 177 assumption.apply permut_transpose.assumption.assumption.
 178 qed.
 179
 180 theorem eq_transpose : \forall i,j,k,n:nat. \lnot j=i \to
 181  \lnot i=k \to \lnot j=k \to
 182 transpose i j n = transpose i k (transpose k j (transpose i k n)).
 183 (* uffa: triplo unfold? *)
 184 intros.unfold transpose.unfold transpose.unfold transpose.
 185 apply (eqb_elim n i).intro.
 186 simplify.rewrite > (eqb_n_n k).
 187 simplify.rewrite > (not_eq_to_eqb_false j i H).
 188 rewrite > (not_eq_to_eqb_false j k H2).
 189 reflexivity.
 190 intro.apply (eqb_elim n j).
 191 intro.
 192 cut (\lnot n = k).
 193 cut (\lnot n = i).
 194 rewrite > (not_eq_to_eqb_false n k Hcut).
 195 simplify.
 196 rewrite > (not_eq_to_eqb_false n k Hcut).
 197 rewrite > (eq_to_eqb_true n j H4).
 198 simplify.
 199 rewrite > (not_eq_to_eqb_false k i).
 200 rewrite > (eqb_n_n k).
 201 simplify.reflexivity.
 202 unfold Not.intro.apply H1.apply sym_eq.assumption.
 203 assumption.
 204 unfold Not.intro.apply H2.apply (trans_eq ? ? n).
 205 apply sym_eq.assumption.assumption.
 206 intro.apply (eqb_elim n k).intro.
 207 simplify.
 208 rewrite > (not_eq_to_eqb_false i k H1).
 209 rewrite > (not_eq_to_eqb_false i j).
 210 simplify.
 211 rewrite > (eqb_n_n i).
 212 simplify.assumption.
 213 unfold Not.intro.apply H.apply sym_eq.assumption.
 214 intro.simplify.
 215 rewrite > (not_eq_to_eqb_false n k H5).
 216 rewrite > (not_eq_to_eqb_false n j H4).
 217 simplify.
 218 rewrite > (not_eq_to_eqb_false n i H3).
 219 rewrite > (not_eq_to_eqb_false n k H5).
 220 simplify.reflexivity.
 221 qed.
 222
 223 theorem permut_S_to_permut_transpose: \forall f:nat \to nat.
 224 \forall m:nat. permut f (S m) \to permut (\lambda n.transpose (f (S m)) (S m)
 225 (f n)) m.
 226 unfold permut.intros.
 227 elim H.
 228 split.intros.simplify.unfold transpose.
 229 apply (eqb_elim (f i) (f (S m))).
 230 intro.apply False_ind.
 231 cut (i = (S m)).
 232 apply (not_le_Sn_n m).
 233 rewrite < Hcut.assumption.
 234 apply H2.apply le_S.assumption.apply le_n.assumption.
 235 intro.simplify.
 236 apply (eqb_elim (f i) (S m)).
 237 intro.
 238 cut (f (S m) \lt (S m) \lor f (S m) = (S m)).
 239 elim Hcut.apply le_S_S_to_le.assumption.
 240 apply False_ind.apply H4.rewrite > H6.assumption.
 241 apply le_to_or_lt_eq.apply H1.apply le_n.
 242 intro.simplify.
 243 cut (f i \lt (S m) \lor f i = (S m)).
 244 elim Hcut.apply le_S_S_to_le.assumption.
 245 apply False_ind.apply H5.assumption.
 246 apply le_to_or_lt_eq.apply H1.apply le_S.assumption.
 247 unfold injn.intros.
 248 apply H2.apply le_S.assumption.apply le_S.assumption.
 249 apply (inj_transpose (f (S m)) (S m)).
 250 apply H5.
 251 qed.
 252
 253 (* bounded bijectivity *)
 254
 255 definition bijn : (nat \to nat) \to nat \to Prop \def
 256 \lambda f:nat \to nat. \lambda n. \forall m:nat. m \le n \to
 257 ex nat (\lambda p. p \le n \land f p = m).
 258
 259 theorem eq_to_bijn:  \forall f,g:nat\to nat. \forall n:nat.
 260 (\forall i:nat. i \le n \to (f i) = (g i)) \to
 261 bijn f n \to bijn g n.
 262 intros 4.unfold bijn.
 263 intros.elim (H1 m).
 264 apply (ex_intro ? ? a).
 265 rewrite < (H a).assumption.
 266 elim H3.assumption.assumption.
 267 qed.
 268
 269 theorem bijn_Sn_n: \forall f:nat \to nat. \forall n:nat.
 270 bijn f (S n) \to f (S n) = (S n) \to bijn f n.
 271 unfold bijn.intros.elim (H m).
 272 elim H3.
 273 apply (ex_intro ? ? a).split.
 274 cut (a < S n \lor a = S n).
 275 elim Hcut.apply le_S_S_to_le.assumption.
 276 apply False_ind.
 277 apply (not_le_Sn_n n).
 278 rewrite < H1.rewrite < H6.rewrite > H5.assumption.
 279 apply le_to_or_lt_eq.assumption.assumption.
 280 apply le_S.assumption.
 281 qed.
 282
 283 theorem bijn_n_Sn: \forall f:nat \to nat. \forall n:nat.
 284 bijn f n \to f (S n) = (S n) \to bijn f (S n).
 285 unfold bijn.intros.
 286 cut (m < S n \lor m = S n).
 287 elim Hcut.
 288 elim (H m).
 289 elim H4.
 290 apply (ex_intro ? ? a).split.
 291 apply le_S.assumption.assumption.
 292 apply le_S_S_to_le.assumption.
 293 apply (ex_intro ? ? (S n)).
 294 split.apply le_n.
 295 rewrite > H3.assumption.
 296 apply le_to_or_lt_eq.assumption.
 297 qed.
 298
 299 theorem bijn_fg: \forall f,g:nat\to nat. \forall n:nat.
 300 bijn f n \to bijn g n \to bijn (\lambda p.f(g p)) n.
 301 unfold bijn.
 302 intros.simplify.
 303 elim (H m).elim H3.
 304 elim (H1 a).elim H6.
 305 apply (ex_intro ? ? a1).
 306 split.assumption.
 307 rewrite > H8.assumption.
 308 assumption.assumption.
 309 qed.
 310
 311 theorem bijn_transpose : \forall n,i,j. i \le n \to j \le n \to
 312 bijn (transpose i j) n.
 313 intros.unfold bijn.unfold transpose.intros.
 314 cut (m = i \lor \lnot m = i).
 315 elim Hcut.
 316 apply (ex_intro ? ? j).
 317 split.assumption.
 318 apply (eqb_elim j i).
 319 intro.simplify.rewrite > H3.rewrite > H4.reflexivity.
 320 rewrite > (eqb_n_n j).simplify.
 321 intros. apply sym_eq.assumption.
 322 cut (m = j \lor \lnot m = j).
 323 elim Hcut1.
 324 apply (ex_intro ? ? i).
 325 split.assumption.
 326 rewrite > (eqb_n_n i).simplify.
 327 apply sym_eq. assumption.
 328 apply (ex_intro ? ? m).
 329 split.assumption.
 330 rewrite > (not_eq_to_eqb_false m i).
 331 rewrite > (not_eq_to_eqb_false m j).
 332 simplify. reflexivity.
 333 assumption.
 334 assumption.
 335 apply (decidable_eq_nat m j).
 336 apply (decidable_eq_nat m i).
 337 qed.
 338
 339 theorem bijn_transpose_r: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
 340 bijn f n \to bijn (\lambda p.f (transpose i j p)) n.
 341 intros.
 342 apply (bijn_fg f ?).assumption.
 343 apply (bijn_transpose n i j).assumption.assumption.
 344 qed.
 345
 346 theorem bijn_transpose_l: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
 347 bijn f n \to bijn (\lambda p.transpose i j (f p)) n.
 348 intros.
 349 apply (bijn_fg ? f).
 350 apply (bijn_transpose n i j).assumption.assumption.
 351 assumption.
 352 qed.
 353
 354 theorem permut_to_bijn: \forall n:nat.\forall f:nat\to nat.
 355 permut f n \to bijn f n.
 356 intro.
 357 elim n.unfold bijn.intros.
 358 apply (ex_intro ? ? m).
 359 split.assumption.
 360 apply (le_n_O_elim m ? (\lambda p. f p = p)).
 361 assumption.unfold permut in H.
 362 elim H.apply sym_eq. apply le_n_O_to_eq.apply H2.apply le_n.
 363 apply (eq_to_bijn (\lambda p.
 364 (transpose (f (S n1)) (S n1)) (transpose (f (S n1)) (S n1) (f p))) f).
 365 intros.apply transpose_transpose.
 366 apply (bijn_fg (transpose (f (S n1)) (S n1))).
 367 apply bijn_transpose.
 368 unfold permut in H1.
 369 elim H1.apply H2.apply le_n.apply le_n.
 370 apply bijn_n_Sn.
 371 apply H.
 372 apply permut_S_to_permut_transpose.
 373 assumption.unfold transpose.
 374 rewrite > (eqb_n_n (f (S n1))).simplify.reflexivity.
 375 qed.
 376
 377 let rec invert_permut n f m \def
 378   match eqb m (f n) with
 379   [true \Rightarrow n
 380   |false \Rightarrow
 381      match n with
 382      [O \Rightarrow O
 383      |(S p) \Rightarrow invert_permut p f m]].
 384
 385 theorem invert_permut_f: \forall f:nat \to nat. \forall n,m:nat.
 386 m \le n \to injn f n\to invert_permut n f (f m) = m.
 387 intros 4.
 388 elim H.
 389 apply (nat_case1 m).
 390 intro.simplify.
 391 rewrite > (eqb_n_n (f O)).simplify.reflexivity.
 392 intros.simplify.
 393 rewrite > (eqb_n_n (f (S m1))).simplify.reflexivity.
 394 simplify.
 395 rewrite > (not_eq_to_eqb_false (f m) (f (S n1))).
 396 simplify.apply H2.
 397 apply injn_Sn_n. assumption.
 398 unfold Not.intro.absurd (m = S n1).
 399 apply H3.apply le_S.assumption.apply le_n.assumption.
 400 unfold Not.intro.
 401 apply (not_le_Sn_n n1).rewrite < H5.assumption.
 402 qed.
 403
 404 theorem injective_invert_permut: \forall f:nat \to nat. \forall n:nat.
 405 permut f n \to injn (invert_permut n f) n.
 406 intros.
 407 unfold injn.intros.
 408 cut (bijn f n).
 409 unfold bijn in Hcut.
 410 generalize in match (Hcut i H1).intro.
 411 generalize in match (Hcut j H2).intro.
 412 elim H4.elim H6.
 413 elim H5.elim H9.
 414 rewrite < H8.
 415 rewrite < H11.
 416 apply eq_f.
 417 rewrite < (invert_permut_f f n a).
 418 rewrite < (invert_permut_f f n a1).
 419 rewrite > H8.
 420 rewrite > H11.
 421 assumption.assumption.
 422 unfold permut in H.elim H. assumption.
 423 assumption.
 424 unfold permut in H.elim H. assumption.
 425 apply permut_to_bijn.assumption.
 426 qed.
 427
 428 theorem permut_invert_permut: \forall f:nat \to nat. \forall n:nat.
 429 permut f n \to permut (invert_permut n f) n.
 430 intros.unfold permut.split.
 431 intros.simplify.elim n.
 432 simplify.elim (eqb i (f O)).simplify.apply le_n.simplify.apply le_n.
 433 simplify.elim (eqb i (f (S n1))).simplify.apply le_n.
 434 simplify.apply le_S. assumption.
 435 apply injective_invert_permut.assumption.
 436 qed.
 437
 438 theorem f_invert_permut: \forall f:nat \to nat. \forall n,m:nat.
 439 m \le n \to permut f n\to f (invert_permut n f m) = m.
 440 intros.
 441 apply (injective_invert_permut f n H1).
 442 unfold permut in H1.elim H1.
 443 apply H2.
 444 cut (permut (invert_permut n f) n).unfold permut in Hcut.
 445 elim Hcut.apply H4.assumption.
 446 apply permut_invert_permut.assumption.assumption.
 447 apply invert_permut_f.
 448 cut (permut (invert_permut n f) n).unfold permut in Hcut.
 449 elim Hcut.apply H2.assumption.
 450 apply permut_invert_permut.assumption.
 451 unfold permut in H1.elim H1.assumption.
 452 qed.
 453
 454 theorem permut_n_to_eq_n: \forall h:nat \to nat.\forall n:nat.
 455 permut h n \to (\forall m:nat. m < n \to h m = m) \to h n = n.
 456 intros.unfold permut in H.elim H.
 457 cut (invert_permut n h n < n \lor invert_permut n h n = n).
 458 elim Hcut.
 459 rewrite < (f_invert_permut h n n) in \vdash (? ? ? %).
 460 apply eq_f.
 461 rewrite < (f_invert_permut h n n) in \vdash (? ? % ?).
 462 apply H1.assumption.apply le_n.assumption.apply le_n.assumption.
 463 rewrite < H4 in \vdash (? ? % ?).
 464 apply (f_invert_permut h).apply le_n.assumption.
 465 apply le_to_or_lt_eq.
 466 cut (permut (invert_permut n h) n).
 467 unfold permut in Hcut.elim Hcut.
 468 apply H4.apply le_n.
 469 apply permut_invert_permut.assumption.
 470 qed.
 471
 472 theorem permut_n_to_le: \forall h:nat \to nat.\forall k,n:nat.
 473 k \le n \to permut h n \to (\forall m:nat. m < k \to h m = m) \to
 474 \forall j. k \le j \to j \le n \to k \le h j.
 475 intros.unfold permut in H1.elim H1.
 476 cut (h j < k \lor \not(h j < k)).
 477 elim Hcut.absurd (k \le j).assumption.
 478 apply lt_to_not_le.
 479 cut (h j = j).rewrite < Hcut1.assumption.
 480 apply H6.apply H5.assumption.assumption.
 481 apply H2.assumption.
 482 apply not_lt_to_le.assumption.
 483 apply (decidable_lt (h j) k).
 484 qed.
 485
 486 (* applications *)
 487
 488 let rec map_iter_i k (g:nat \to nat) f (i:nat) \def
 489   match k with
 490    [ O \Rightarrow g i
 491    | (S k) \Rightarrow f (g (S (k+i))) (map_iter_i k g f i)].
 492
 493 theorem eq_map_iter_i: \forall g1,g2:nat \to nat.
 494 \forall f:nat \to nat \to nat. \forall n,i:nat.
 495 (\forall m:nat. i\le m \to m \le n+i \to g1 m = g2 m) \to
 496 map_iter_i n g1 f i = map_iter_i n g2 f i.
 497 intros 5.elim n.simplify.apply H.apply le_n.
 498 apply le_n.simplify.apply eq_f2.apply H1.simplify.
 499 apply le_S.apply le_plus_n.simplify.apply le_n.
 500 apply H.intros.apply H1.assumption.simplify.apply le_S.assumption.
 501 qed.
 502
 503 (* map_iter examples *)
 504
 505 theorem eq_map_iter_i_sigma: \forall g:nat \to nat. \forall n,m:nat.
 506 map_iter_i n g plus m = sigma n g m.
 507 intros.elim n.simplify.reflexivity.
 508 simplify.
 509 apply eq_f.assumption.
 510 qed.
 511
 512 theorem eq_map_iter_i_pi: \forall g:nat \to nat. \forall n,m:nat.
 513 map_iter_i n g times m = pi n g m.
 514 intros.elim n.simplify.reflexivity.
 515 simplify.
 516 apply eq_f.assumption.
 517 qed.
 518
 519 theorem eq_map_iter_i_fact: \forall n:nat.
 520 map_iter_i n (\lambda m.m) times (S O) = (S n)!.
 521 intros.elim n.
 522 simplify.reflexivity.
 523 change with
 524 (((S n1)+(S O))*(map_iter_i n1 (\lambda m.m) times (S O)) = (S(S n1))*(S n1)!).
 525 rewrite < plus_n_Sm.rewrite < plus_n_O.
 526 apply eq_f.assumption.
 527 qed.
 528
 529 theorem eq_map_iter_i_transpose_l : \forall f:nat\to nat \to nat.associative nat f \to
 530 symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k:nat.
 531 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.
 532 intros.apply (nat_case1 k).
 533 intros.simplify.
 534 change with
 535 (f (g (S n)) (g n) =
 536 f (g (transpose n (S n) (S n))) (g (transpose n (S n) n))).
 537 rewrite > transpose_i_j_i.
 538 rewrite > transpose_i_j_j.
 539 apply H1.
 540 intros.
 541 change with
 542 (f (g (S (S (m+n)))) (f (g (S (m+n))) (map_iter_i m g f n)) =
 543 f (g (transpose (S m + n) (S (S m) + n) (S (S m)+n)))
 544 (f (g (transpose (S m + n) (S (S m) + n) (S m+n)))
 545 (map_iter_i m (\lambda m1. g (transpose (S m+n) (S (S m)+n) m1)) f n))).
 546 rewrite > transpose_i_j_i.
 547 rewrite > transpose_i_j_j.
 548 rewrite < H.
 549 rewrite < H.
 550 rewrite < (H1 (g (S m + n))).
 551 apply eq_f.
 552 apply eq_map_iter_i.
 553 intros.simplify.unfold transpose.
 554 rewrite > (not_eq_to_eqb_false m1 (S m+n)).
 555 rewrite > (not_eq_to_eqb_false m1 (S (S m)+n)).
 556 simplify.
 557 reflexivity.
 558 apply (lt_to_not_eq m1 (S ((S m)+n))).
 559 unfold lt.apply le_S_S.change with (m1 \leq S (m+n)).apply le_S.assumption.
 560 apply (lt_to_not_eq m1 (S m+n)).
 561 simplify.unfold lt.apply le_S_S.assumption.
 562 qed.
 563
 564 theorem eq_map_iter_i_transpose_i_Si : \forall f:nat\to nat \to nat.associative nat f \to
 565 symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k,i:nat. n \le i \to i \le k+n \to
 566 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S i) m)) f n.
 567 intros 6.elim k.cut (i=n).
 568 rewrite > Hcut.
 569 apply (eq_map_iter_i_transpose_l f H H1 g n O).
 570 apply antisymmetric_le.assumption.assumption.
 571 cut (i < S n1 + n \lor i = S n1 + n).
 572 elim Hcut.
 573 change with
 574 (f (g (S (S n1)+n)) (map_iter_i (S n1) g f n) =
 575 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)).
 576 apply eq_f2.unfold transpose.
 577 rewrite > (not_eq_to_eqb_false (S (S n1)+n) i).
 578 rewrite > (not_eq_to_eqb_false (S (S n1)+n) (S i)).
 579 simplify.reflexivity.
 580 simplify.unfold Not.intro.
 581 apply (lt_to_not_eq i (S n1+n)).assumption.
 582 apply inj_S.apply sym_eq. assumption.
 583 simplify.unfold Not.intro.
 584 apply (lt_to_not_eq i (S (S n1+n))).simplify.unfold lt.
 585 apply le_S_S.assumption.
 586 apply sym_eq. assumption.
 587 apply H2.assumption.apply le_S_S_to_le.
 588 assumption.
 589 rewrite > H5.
 590 apply (eq_map_iter_i_transpose_l f H H1 g n (S n1)).
 591 apply le_to_or_lt_eq.assumption.
 592 qed.
 593
 594 theorem eq_map_iter_i_transpose:
 595 \forall f:nat\to nat \to nat.
 596 associative nat f \to symmetric2 nat nat f \to \forall n,k,o:nat.
 597 \forall g:nat \to nat. \forall i:nat. n \le i \to S (o + i) \le S k+n \to
 598 map_iter_i (S k) g  f n = map_iter_i (S k) (\lambda m. g (transpose i (S(o + i)) m)) f n.
 599 intros 6.
 600 apply (nat_elim1 o).
 601 intro.
 602 apply (nat_case m ?).
 603 intros.
 604 apply (eq_map_iter_i_transpose_i_Si ? H H1).
 605 exact H3.apply le_S_S_to_le.assumption.
 606 intros.
 607 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n)).
 608 apply H2.
 609 unfold lt. apply le_n.assumption.
 610 apply (trans_le ? (S(S (m1+i)))).
 611 apply le_S.apply le_n.assumption.
 612 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
 613 (transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n)).
 614 apply (H2 O ? ? (S(m1+i))).
 615 unfold lt.apply le_S_S.apply le_O_n.
 616 apply (trans_le ? i).assumption.
 617 change with (i \le (S m1)+i).apply le_plus_n.
 618 exact H4.
 619 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
 620 (transpose i (S(m1 + i))
 621 (transpose (S(m1 + i)) (S(S(m1 + i)))
 622 (transpose i (S(m1 + i)) m)))) f n)).
 623 apply (H2 m1).
 624 unfold lt. apply le_n.assumption.
 625 apply (trans_le ? (S(S (m1+i)))).
 626 apply le_S.apply le_n.assumption.
 627 apply eq_map_iter_i.
 628 intros.apply eq_f.
 629 apply sym_eq. apply eq_transpose.
 630 unfold Not. intro.
 631 apply (not_le_Sn_n i).
 632 rewrite < H7 in \vdash (? ? %).
 633 apply le_S_S.apply le_S.
 634 apply le_plus_n.
 635 unfold Not. intro.
 636 apply (not_le_Sn_n i).
 637 rewrite > H7 in \vdash (? ? %).
 638 apply le_S_S.
 639 apply le_plus_n.
 640 unfold Not. intro.
 641 apply (not_eq_n_Sn (S m1+i)).
 642 apply sym_eq.assumption.
 643 qed.
 644
 645 theorem eq_map_iter_i_transpose1: \forall f:nat\to nat \to nat.associative nat f \to
 646 symmetric2 nat nat f \to \forall n,k,i,j:nat.
 647 \forall g:nat \to nat. n \le i \to i < j \to j \le S k+n \to
 648 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
 649 intros.
 650 simplify in H3.
 651 cut ((S i) < j \lor (S i) = j).
 652 elim Hcut.
 653 cut (j = S ((j - (S i)) + i)).
 654 rewrite > Hcut1.
 655 apply (eq_map_iter_i_transpose f H H1 n k (j - (S i)) g i).
 656 assumption.
 657 rewrite < Hcut1.assumption.
 658 rewrite > plus_n_Sm.
 659 apply plus_minus_m_m.apply lt_to_le.assumption.
 660 rewrite < H5.
 661 apply (eq_map_iter_i_transpose_i_Si f H H1 g).
 662 simplify.
 663 assumption.apply le_S_S_to_le.
 664 apply (trans_le ? j).assumption.assumption.
 665 apply le_to_or_lt_eq.assumption.
 666 qed.
 667
 668 theorem eq_map_iter_i_transpose2: \forall f:nat\to nat \to nat.associative nat f \to
 669 symmetric2 nat nat f \to \forall n,k,i,j:nat.
 670 \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
 671 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
 672 intros.
 673 apply (nat_compare_elim i j).
 674 intro.apply (eq_map_iter_i_transpose1 f H H1 n k i j g H2 H6 H5).
 675 intro.rewrite > H6.
 676 apply eq_map_iter_i.intros.
 677 rewrite > (transpose_i_i j).reflexivity.
 678 intro.
 679 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m:nat.g (transpose j i m)) f n)).
 680 apply (eq_map_iter_i_transpose1 f H H1 n k j i g H4 H6 H3).
 681 apply eq_map_iter_i.
 682 intros.apply eq_f.apply transpose_i_j_j_i.
 683 qed.
 684
 685 theorem permut_to_eq_map_iter_i:\forall f:nat\to nat \to nat.associative nat f \to
 686 symmetric2 nat nat f \to \forall k,n:nat.\forall g,h:nat \to nat.
 687 permut h (k+n) \to (\forall m:nat. m \lt n \to h m = m) \to
 688 map_iter_i k g f n = map_iter_i k (\lambda m.g(h m)) f n.
 689 intros 4.elim k.
 690 simplify.rewrite > (permut_n_to_eq_n h).reflexivity.assumption.assumption.
 691 apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.g ((transpose (h (S n+n1)) (S n+n1)) m)) f n1)).
 692 unfold permut in H3.
 693 elim H3.
 694 apply (eq_map_iter_i_transpose2 f H H1 n1 n ? ? g).
 695 apply (permut_n_to_le h n1 (S n+n1)).
 696 apply le_plus_n.assumption.assumption.apply le_plus_n.apply le_n.
 697 apply H5.apply le_n.apply le_plus_n.apply le_n.
 698 apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.
 699 (g(transpose (h (S n+n1)) (S n+n1)
 700 (transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1)).
 701 change with
 702 (f (g (transpose (h (S n+n1)) (S n+n1) (S n+n1)))
 703 (map_iter_i n (\lambda m.
 704 g (transpose (h (S n+n1)) (S n+n1) m)) f n1)
 705 =
 706 f
 707 (g(transpose (h (S n+n1)) (S n+n1)
 708 (transpose (h (S n+n1)) (S n+n1) (h (S n+n1)))))
 709 (map_iter_i n
 710 (\lambda m.
 711 (g(transpose (h (S n+n1)) (S n+n1)
 712 (transpose (h (S n+n1)) (S n+n1) (h m))))) f n1)).
 713 apply eq_f2.apply eq_f.
 714 rewrite > transpose_i_j_j.
 715 rewrite > transpose_i_j_i.
 716 rewrite > transpose_i_j_j.reflexivity.
 717 apply (H2 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m)))).
 718 apply permut_S_to_permut_transpose.
 719 assumption.
 720 intros.
 721 unfold transpose.
 722 rewrite > (not_eq_to_eqb_false (h m) (h (S n+n1))).
 723 rewrite > (not_eq_to_eqb_false (h m) (S n+n1)).
 724 simplify.apply H4.assumption.
 725 rewrite > H4.
 726 apply lt_to_not_eq.apply (trans_lt ? n1).assumption.
 727 simplify.unfold lt.apply le_S_S.apply le_plus_n.assumption.
 728 unfold permut in H3.elim H3.
 729 simplify.unfold Not.intro.
 730 apply (lt_to_not_eq m (S n+n1)).apply (trans_lt ? n1).assumption.
 731 simplify.unfold lt.apply le_S_S.apply le_plus_n.
 732 unfold injn in H7.
 733 apply (H7 m (S n+n1)).apply (trans_le ? n1).
 734 apply lt_to_le.assumption.apply le_plus_n.apply le_n.
 735 assumption.
 736 apply eq_map_iter_i.intros.
 737 rewrite > transpose_transpose.reflexivity.
 738 qed.