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.fold simplify (transpose n (S n) (S n)).
 534 rewrite > transpose_i_j_i.
 535 rewrite > transpose_i_j_j.
 536 apply H1.
 537 intros.
 538 change with
 539 (f (g (S (S (m+n)))) (f (g (S (m+n))) (map_iter_i m g f n)) =
 540 f (g (transpose (S m + n) (S (S m) + n) (S (S m)+n)))
 541 (f (g (transpose (S m + n) (S (S m) + n) (S m+n)))
 542 (map_iter_i m (\lambda m1. g (transpose (S m+n) (S (S m)+n) m1)) f n))).
 543 rewrite > transpose_i_j_i.
 544 rewrite > transpose_i_j_j.
 545 rewrite < H.
 546 rewrite < H.
 547 rewrite < (H1 (g (S m + n))).
 548 apply eq_f.
 549 apply eq_map_iter_i.
 550 intros.simplify.unfold transpose.
 551 rewrite > (not_eq_to_eqb_false m1 (S m+n)).
 552 rewrite > (not_eq_to_eqb_false m1 (S (S m)+n)).
 553 simplify.
 554 reflexivity.
 555 apply (lt_to_not_eq m1 (S ((S m)+n))).
 556 unfold lt.apply le_S_S.change with (m1 \leq S (m+n)).apply le_S.assumption.
 557 apply (lt_to_not_eq m1 (S m+n)).
 558 simplify.unfold lt.apply le_S_S.assumption.
 559 qed.
 560
 561 theorem eq_map_iter_i_transpose_i_Si : \forall f:nat\to nat \to nat.associative nat f \to
 562 symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k,i:nat. n \le i \to i \le k+n \to
 563 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S i) m)) f n.
 564 intros 6.elim k.cut (i=n).
 565 rewrite > Hcut.
 566 apply (eq_map_iter_i_transpose_l f H H1 g n O).
 567 apply antisymmetric_le.assumption.assumption.
 568 cut (i < S n1 + n \lor i = S n1 + n).
 569 elim Hcut.
 570 change with
 571 (f (g (S (S n1)+n)) (map_iter_i (S n1) g f n) =
 572 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)).
 573 apply eq_f2.unfold transpose.
 574 rewrite > (not_eq_to_eqb_false (S (S n1)+n) i).
 575 rewrite > (not_eq_to_eqb_false (S (S n1)+n) (S i)).
 576 simplify.reflexivity.
 577 simplify.unfold Not.intro.
 578 apply (lt_to_not_eq i (S n1+n)).assumption.
 579 apply inj_S.apply sym_eq. assumption.
 580 simplify.unfold Not.intro.
 581 apply (lt_to_not_eq i (S (S n1+n))).simplify.unfold lt.
 582 apply le_S_S.assumption.
 583 apply sym_eq. assumption.
 584 apply H2.assumption.apply le_S_S_to_le.
 585 assumption.
 586 rewrite > H5.
 587 apply (eq_map_iter_i_transpose_l f H H1 g n (S n1)).
 588 apply le_to_or_lt_eq.assumption.
 589 qed.
 590
 591 theorem eq_map_iter_i_transpose:
 592 \forall f:nat\to nat \to nat.
 593 associative nat f \to symmetric2 nat nat f \to \forall n,k,o:nat.
 594 \forall g:nat \to nat. \forall i:nat. n \le i \to S (o + i) \le S k+n \to
 595 map_iter_i (S k) g  f n = map_iter_i (S k) (\lambda m. g (transpose i (S(o + i)) m)) f n.
 596 intros 6.
 597 apply (nat_elim1 o).
 598 intro.
 599 apply (nat_case m ?).
 600 intros.
 601 apply (eq_map_iter_i_transpose_i_Si ? H H1).
 602 exact H3.apply le_S_S_to_le.assumption.
 603 intros.
 604 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n)).
 605 apply H2.
 606 unfold lt. apply le_n.assumption.
 607 apply (trans_le ? (S(S (m1+i)))).
 608 apply le_S.apply le_n.assumption.
 609 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
 610 (transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n)).
 611 apply (H2 O ? ? (S(m1+i))).
 612 unfold lt.apply le_S_S.apply le_O_n.
 613 apply (trans_le ? i).assumption.
 614 change with (i \le (S m1)+i).apply le_plus_n.
 615 exact H4.
 616 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
 617 (transpose i (S(m1 + i))
 618 (transpose (S(m1 + i)) (S(S(m1 + i)))
 619 (transpose i (S(m1 + i)) m)))) f n)).
 620 apply (H2 m1).
 621 unfold lt. apply le_n.assumption.
 622 apply (trans_le ? (S(S (m1+i)))).
 623 apply le_S.apply le_n.assumption.
 624 apply eq_map_iter_i.
 625 intros.apply eq_f.
 626 apply sym_eq. apply eq_transpose.
 627 unfold Not. intro.
 628 apply (not_le_Sn_n i).
 629 rewrite < H7 in \vdash (? ? %).
 630 apply le_S_S.apply le_S.
 631 apply le_plus_n.
 632 unfold Not. intro.
 633 apply (not_le_Sn_n i).
 634 rewrite > H7 in \vdash (? ? %).
 635 apply le_S_S.
 636 apply le_plus_n.
 637 unfold Not. intro.
 638 apply (not_eq_n_Sn (S m1+i)).
 639 apply sym_eq.assumption.
 640 qed.
 641
 642 theorem eq_map_iter_i_transpose1: \forall f:nat\to nat \to nat.associative nat f \to
 643 symmetric2 nat nat f \to \forall n,k,i,j:nat.
 644 \forall g:nat \to nat. n \le i \to i < j \to j \le S k+n \to
 645 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
 646 intros.
 647 simplify in H3.
 648 cut ((S i) < j \lor (S i) = j).
 649 elim Hcut.
 650 cut (j = S ((j - (S i)) + i)).
 651 rewrite > Hcut1.
 652 apply (eq_map_iter_i_transpose f H H1 n k (j - (S i)) g i).
 653 assumption.
 654 rewrite < Hcut1.assumption.
 655 rewrite > plus_n_Sm.
 656 apply plus_minus_m_m.apply lt_to_le.assumption.
 657 rewrite < H5.
 658 apply (eq_map_iter_i_transpose_i_Si f H H1 g).
 659 simplify.
 660 assumption.apply le_S_S_to_le.
 661 apply (trans_le ? j).assumption.assumption.
 662 apply le_to_or_lt_eq.assumption.
 663 qed.
 664
 665 theorem eq_map_iter_i_transpose2: \forall f:nat\to nat \to nat.associative nat f \to
 666 symmetric2 nat nat f \to \forall n,k,i,j:nat.
 667 \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
 668 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
 669 intros.
 670 apply (nat_compare_elim i j).
 671 intro.apply (eq_map_iter_i_transpose1 f H H1 n k i j g H2 H6 H5).
 672 intro.rewrite > H6.
 673 apply eq_map_iter_i.intros.
 674 rewrite > (transpose_i_i j).reflexivity.
 675 intro.
 676 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m:nat.g (transpose j i m)) f n)).
 677 apply (eq_map_iter_i_transpose1 f H H1 n k j i g H4 H6 H3).
 678 apply eq_map_iter_i.
 679 intros.apply eq_f.apply transpose_i_j_j_i.
 680 qed.
 681
 682 theorem permut_to_eq_map_iter_i:\forall f:nat\to nat \to nat.associative nat f \to
 683 symmetric2 nat nat f \to \forall k,n:nat.\forall g,h:nat \to nat.
 684 permut h (k+n) \to (\forall m:nat. m \lt n \to h m = m) \to
 685 map_iter_i k g f n = map_iter_i k (\lambda m.g(h m)) f n.
 686 intros 4.elim k.
 687 simplify.rewrite > (permut_n_to_eq_n h).reflexivity.assumption.assumption.
 688 apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.g ((transpose (h (S n+n1)) (S n+n1)) m)) f n1)).
 689 unfold permut in H3.
 690 elim H3.
 691 apply (eq_map_iter_i_transpose2 f H H1 n1 n ? ? g).
 692 apply (permut_n_to_le h n1 (S n+n1)).
 693 apply le_plus_n.assumption.assumption.apply le_plus_n.apply le_n.
 694 apply H5.apply le_n.apply le_plus_n.apply le_n.
 695 apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.
 696 (g(transpose (h (S n+n1)) (S n+n1)
 697 (transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1)).
 698 simplify.fold simplify (transpose (h (S n+n1)) (S n+n1) (S n+n1)).
 699 apply eq_f2.apply eq_f.
 700 rewrite > transpose_i_j_j.
 701 rewrite > transpose_i_j_i.
 702 rewrite > transpose_i_j_j.reflexivity.
 703 apply (H2 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m)))).
 704 apply permut_S_to_permut_transpose.
 705 assumption.
 706 intros.
 707 unfold transpose.
 708 rewrite > (not_eq_to_eqb_false (h m) (h (S n+n1))).
 709 rewrite > (not_eq_to_eqb_false (h m) (S n+n1)).
 710 simplify.apply H4.assumption.
 711 rewrite > H4.
 712 apply lt_to_not_eq.apply (trans_lt ? n1).assumption.
 713 simplify.unfold lt.apply le_S_S.apply le_plus_n.assumption.
 714 unfold permut in H3.elim H3.
 715 simplify.unfold Not.intro.
 716 apply (lt_to_not_eq m (S n+n1)).apply (trans_lt ? n1).assumption.
 717 simplify.unfold lt.apply le_S_S.apply le_plus_n.
 718 unfold injn in H7.
 719 apply (H7 m (S n+n1)).apply (trans_le ? n1).
 720 apply lt_to_le.assumption.apply le_plus_n.apply le_n.
 721 assumption.
 722 apply eq_map_iter_i.intros.
 723 rewrite > transpose_transpose.reflexivity.
 724 qed.