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