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