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