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