helm/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.simplify.
  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 simplify.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 simplify.intro.apply H1.apply sym_eq.assumption.
 203 assumption.
 204 simplify.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 simplify.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.
 229 apply eqb_elim (f i) (f (S m)).simplify.
 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).simplify.
 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.simplify.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
 355 theorem permut_to_bijn: \forall n:nat.\forall f:nat\to nat.
 356 permut f n \to bijn f n.
 357 intro.
 358 elim n.simplify.intros.
 359 apply ex_intro ? ? m.
 360 split.assumption.
 361 apply le_n_O_elim m ? (\lambda p. f p = p).
 362 assumption.unfold permut in H.
 363 elim H.apply sym_eq. apply le_n_O_to_eq.apply H2.apply le_n.
 364 apply eq_to_bijn (\lambda p.
 365 (transpose (f (S n1)) (S n1)) (transpose (f (S n1)) (S n1) (f p))) f.
 366 intros.apply transpose_transpose.
 367 apply bijn_fg (transpose (f (S n1)) (S n1)).
 368 apply bijn_transpose.
 369 unfold permut in H1.
 370 elim H1.apply H2.apply le_n.apply le_n.
 371 apply bijn_n_Sn.
 372 apply H.
 373 apply permut_S_to_permut_transpose.
 374 assumption.simplify.
 375 rewrite > eqb_n_n (f (S n1)).simplify.reflexivity.
 376 qed.
 377
 378 let rec invert_permut n f m \def
 379   match eqb m (f n) with
 380   [true \Rightarrow n
 381   |false \Rightarrow
 382      match n with
 383      [O \Rightarrow O
 384      |(S p) \Rightarrow invert_permut p f m]].
 385
 386 theorem invert_permut_f: \forall f:nat \to nat. \forall n,m:nat.
 387 m \le n \to injn f n\to invert_permut n f (f m) = m.
 388 intros 4.
 389 elim H.
 390 apply nat_case1 m.
 391 intro.simplify.
 392 rewrite > eqb_n_n (f O).simplify.reflexivity.
 393 intros.simplify.
 394 rewrite > eqb_n_n (f (S m1)).simplify.reflexivity.
 395 simplify.
 396 rewrite > not_eq_to_eqb_false (f m) (f (S n1)).
 397 simplify.apply H2.
 398 apply injn_Sn_n. assumption.
 399 simplify.intro.absurd m = S n1.
 400 apply H3.apply le_S.assumption.apply le_n.assumption.
 401 simplify.intro.
 402 apply not_le_Sn_n n1.rewrite < H5.assumption.
 403 qed.
 404
 405 theorem injective_invert_permut: \forall f:nat \to nat. \forall n:nat.
 406 permut f n \to injn (invert_permut n f) n.
 407 intros.
 408 unfold injn.intros.
 409 cut bijn f n.
 410 unfold bijn in Hcut.
 411 generalize in match Hcut i H1.intro.
 412 generalize in match Hcut j H2.intro.
 413 elim H4.elim H6.
 414 elim H5.elim H9.
 415 rewrite < H8.
 416 rewrite < H11.
 417 apply eq_f.
 418 rewrite < invert_permut_f f n a.
 419 rewrite < invert_permut_f f n a1.
 420 rewrite > H8.
 421 rewrite > H11.
 422 assumption.assumption.
 423 unfold permut in H.elim H. assumption.
 424 assumption.
 425 unfold permut in H.elim H. assumption.
 426 apply permut_to_bijn.assumption.
 427 qed.
 428
 429 theorem permut_invert_permut: \forall f:nat \to nat. \forall n:nat.
 430 permut f n \to permut (invert_permut n f) n.
 431 intros.unfold permut.split.
 432 intros.simplify.elim n.
 433 simplify.elim eqb i (f O).simplify.apply le_n.simplify.apply le_n.
 434 simplify.elim eqb i (f (S n1)).simplify.apply le_n.
 435 simplify.apply le_S. assumption.
 436 apply injective_invert_permut.assumption.
 437 qed.
 438
 439 theorem f_invert_permut: \forall f:nat \to nat. \forall n,m:nat.
 440 m \le n \to permut f n\to f (invert_permut n f m) = m.
 441 intros.
 442 apply injective_invert_permut f n H1.
 443 unfold permut in H1.elim H1.
 444 apply H2.
 445 cut permut (invert_permut n f) n.unfold permut in Hcut.
 446 elim Hcut.apply H4.assumption.
 447 apply permut_invert_permut.assumption.assumption.
 448 (* uffa: lo ha espanso troppo *)
 449 change with invert_permut n f (f (invert_permut n f m)) = invert_permut n f m.
 450 apply invert_permut_f.
 451 cut permut (invert_permut n f) n.unfold permut in Hcut.
 452 elim Hcut.apply H2.assumption.
 453 apply permut_invert_permut.assumption.
 454 unfold permut in H1.elim H1.assumption.
 455 qed.
 456
 457 theorem permut_n_to_eq_n: \forall h:nat \to nat.\forall n:nat.
 458 permut h n \to (\forall m:nat. m < n \to h m = m) \to h n = n.
 459 intros.unfold permut in H.elim H.
 460 cut invert_permut n h n < n \lor invert_permut n h n = n.
 461 elim Hcut.
 462 rewrite < f_invert_permut h n n in \vdash (? ? ? %).
 463 apply eq_f.
 464 rewrite < f_invert_permut h n n in \vdash (? ? % ?).
 465 apply H1.assumption.apply le_n.assumption.apply le_n.assumption.
 466 rewrite < H4 in \vdash (? ? % ?).
 467 apply f_invert_permut h.apply le_n.assumption.
 468 apply le_to_or_lt_eq.
 469 cut permut (invert_permut n h) n.
 470 unfold permut in Hcut.elim Hcut.
 471 apply H4.apply le_n.
 472 apply permut_invert_permut.assumption.
 473 qed.
 474
 475 theorem permut_n_to_le: \forall h:nat \to nat.\forall k,n:nat.
 476 k \le n \to permut h n \to (\forall m:nat. m < k \to h m = m) \to
 477 \forall j. k \le j \to j \le n \to k \le h j.
 478 intros.unfold permut in H1.elim H1.
 479 cut h j < k \lor \not(h j < k).
 480 elim Hcut.absurd k \le j.assumption.
 481 apply lt_to_not_le.
 482 cut h j = j.rewrite < Hcut1.assumption.
 483 apply H6.apply H5.assumption.assumption.
 484 apply H2.assumption.
 485 apply not_lt_to_le.assumption.
 486 apply decidable_lt (h j) k.
 487 qed.
 488
 489 (* applications *)
 490
 491 let rec map_iter_i k (g:nat \to nat) f (i:nat) \def
 492   match k with
 493    [ O \Rightarrow g i
 494    | (S k) \Rightarrow f (g (S (k+i))) (map_iter_i k g f i)].
 495
 496 theorem eq_map_iter_i: \forall g1,g2:nat \to nat.
 497 \forall f:nat \to nat \to nat. \forall n,i:nat.
 498 (\forall m:nat. i\le m \to m \le n+i \to g1 m = g2 m) \to
 499 map_iter_i n g1 f i = map_iter_i n g2 f i.
 500 intros 5.elim n.simplify.apply H.apply le_n.
 501 apply le_n.simplify.apply eq_f2.apply H1.simplify.
 502 apply le_S.apply le_plus_n.simplify.apply le_n.
 503 apply H.intros.apply H1.assumption.simplify.apply le_S.assumption.
 504 qed.
 505
 506 (* map_iter examples *)
 507
 508 theorem eq_map_iter_i_sigma: \forall g:nat \to nat. \forall n,m:nat.
 509 map_iter_i n g plus m = sigma n g m.
 510 intros.elim n.simplify.reflexivity.
 511 simplify.
 512 apply eq_f.assumption.
 513 qed.
 514
 515 theorem eq_map_iter_i_pi: \forall g:nat \to nat. \forall n,m:nat.
 516 map_iter_i n g times m = pi n g m.
 517 intros.elim n.simplify.reflexivity.
 518 simplify.
 519 apply eq_f.assumption.
 520 qed.
 521
 522 theorem eq_map_iter_i_fact: \forall n:nat.
 523 map_iter_i n (\lambda m.m) times (S O) = (S n)!.
 524 intros.elim n.
 525 simplify.reflexivity.
 526 change with
 527 ((S n1)+(S O))*(map_iter_i n1 (\lambda m.m) times (S O)) = (S(S n1))*(S n1)!.
 528 rewrite < plus_n_Sm.rewrite < plus_n_O.
 529 apply eq_f.assumption.
 530 qed.
 531
 532 theorem eq_map_iter_i_transpose_l : \forall f:nat\to nat \to nat.associative nat f \to
 533 symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k:nat.
 534 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.
 535 intros.apply nat_case1 k.
 536 intros.simplify.
 537 change with
 538 f (g (S n)) (g n) =
 539 f (g (transpose n (S n) (S n))) (g (transpose n (S n) 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.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 simplify.apply le_S_S.apply le_S.assumption.
 563 apply lt_to_not_eq m1 (S m+n).
 564 simplify.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.intro.
 584 apply lt_to_not_eq i (S n1+n).assumption.
 585 apply inj_S.apply sym_eq. assumption.
 586 simplify.intro.
 587 apply lt_to_not_eq i (S (S n1+n)).simplify.
 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 simplify. 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 simplify.apply le_S_S.apply le_O_n.
 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 simplify. 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 simplify. 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 simplify. intro.
 639 apply not_le_Sn_n i.
 640 rewrite > H7 in \vdash (? ? %).
 641 apply le_S_S.
 642 apply le_plus_n.
 643 simplify. 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.reflexivity.assumption.assumption.
 694 apply trans_eq ? ? (map_iter_i (S n) (\lambda m.g ((transpose (h (S n+n1)) (S n+n1)) m)) f n1).
 695 unfold permut in H3.
 696 elim H3.
 697 apply eq_map_iter_i_transpose2 f H H1 n1 n ? ? g.
 698 apply permut_n_to_le h n1 (S n+n1).
 699 apply le_plus_n.assumption.assumption.apply le_plus_n.apply le_n.
 700 apply H5.apply le_n.apply le_plus_n.apply le_n.
 701 apply trans_eq ? ? (map_iter_i (S n) (\lambda m.
 702 (g(transpose (h (S n+n1)) (S n+n1)
 703 (transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1).
 704 change with
 705 f (g (transpose (h (S n+n1)) (S n+n1) (S n+n1)))
 706 (map_iter_i n (\lambda m.
 707 g (transpose (h (S n+n1)) (S n+n1) m)) f n1)
 708 =
 709 f
 710 (g(transpose (h (S n+n1)) (S n+n1)
 711 (transpose (h (S n+n1)) (S n+n1) (h (S n+n1)))))
 712 (map_iter_i n
 713 (\lambda m.
 714 (g(transpose (h (S n+n1)) (S n+n1)
 715 (transpose (h (S n+n1)) (S n+n1) (h m))))) f n1).
 716 apply eq_f2.apply eq_f.
 717 rewrite > transpose_i_j_j.
 718 rewrite > transpose_i_j_i.
 719 rewrite > transpose_i_j_j.reflexivity.
 720 apply H2 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m))).
 721 apply permut_S_to_permut_transpose.
 722 assumption.
 723 intros.
 724 unfold transpose.
 725 rewrite > not_eq_to_eqb_false (h m) (h (S n+n1)).
 726 rewrite > not_eq_to_eqb_false (h m) (S n+n1).
 727 simplify.apply H4.assumption.
 728 rewrite > H4.
 729 apply lt_to_not_eq.apply trans_lt ? n1.assumption.
 730 simplify.apply le_S_S.apply le_plus_n.assumption.
 731 unfold permut in H3.elim H3.
 732 simplify.intro.
 733 apply lt_to_not_eq m (S n+n1).apply trans_lt ? n1.assumption.
 734 simplify.apply le_S_S.apply le_plus_n.
 735 unfold injn in H7.
 736 apply H7 m (S n+n1).apply trans_le ? n1.
 737 apply lt_to_le.assumption.apply le_plus_n.apply le_n.
 738 assumption.
 739 apply eq_map_iter_i.intros.
 740 rewrite > transpose_transpose.reflexivity.
 741 qed.
 742