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