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 (\forall p:nat. f m = f p \to m = p) \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.assumption.
 398 simplify.intro.absurd m = S n1.
 399 apply H3.assumption.simplify.intro.
 400 apply not_le_Sn_n n1.rewrite < H5.assumption.
 401 qed.
 402
 403 (* applications *)
 404
 405 let rec map_iter n (g:nat \to nat) f (a:nat) \def
 406   match n with
 407    [ O \Rightarrow a
 408    | (S p) \Rightarrow f (g p) (map_iter p g f a)].
 409
 410 theorem eq_map_iter: \forall g1,g2:nat \to nat.
 411 \forall f:nat \to nat \to nat. \forall n,a:nat.
 412 (\forall m:nat. m \lt n \to g1 m = g2 m) \to
 413 map_iter n g1 f a = map_iter n g2 f a.
 414 intros 5.elim n.simplify.reflexivity.
 415 simplify.apply eq_f2.apply H1.simplify.apply le_n.
 416 apply H.intros.apply H1.apply trans_lt ? n1.assumption.
 417 simplify.apply le_n.
 418 qed.
 419
 420 (* map_iter examples *)
 421 theorem eq_map_iter_sigma: \forall g:nat \to nat. \forall n:nat.
 422 map_iter n g plus O = sigma n g.
 423 intros.elim n.simplify.reflexivity.
 424 simplify.
 425 apply eq_f.assumption.
 426 qed.
 427
 428 theorem eq_map_iter_pi: \forall g:nat \to nat. \forall n:nat.
 429 map_iter n g times (S O) = pi n g.
 430 intros.elim n.simplify.reflexivity.
 431 simplify.
 432 apply eq_f.assumption.
 433 qed.
 434
 435 theorem eq_map_iter_transpose_i_Si : \forall f:nat\to nat \to nat.associative nat f \to
 436 symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,i,a:nat. i \lt n \to
 437 map_iter (S n) g f a = map_iter (S n) (\lambda m. g (transpose i (S i) m)) f a.
 438 intros 5.elim n.apply False_ind.apply not_le_Sn_O i H2.
 439 simplify in H3.
 440 cut i < n1 \lor i = n1.
 441 change with
 442 f (g (S n1)) (map_iter (S n1) g f a) =
 443 f (g (transpose i (S i) (S n1))) (map_iter (S n1) (\lambda m. g (transpose i (S i) m)) f a).
 444 elim Hcut.
 445 cut g (transpose i (S i) (S n1)) = g (S n1).
 446 rewrite > Hcut1.
 447 rewrite < H2 i a H4.reflexivity.
 448 unfold transpose.
 449 rewrite > not_eq_to_eqb_false (S n1) i.
 450 rewrite > not_eq_to_eqb_false (S n1) (S i).
 451 simplify.reflexivity.
 452 simplify.intro.
 453 apply lt_to_not_eq i n1 H4.
 454 apply injective_S i.apply sym_eq.assumption.
 455 simplify. intro.
 456 apply lt_to_not_eq i (S n1).
 457 apply trans_lt ? n1.assumption.simplify.apply le_n.
 458 apply sym_eq.assumption.
 459 (* interesting case *)
 460 rewrite > H4.
 461 change with f (g (S n1)) (f (g n1) (map_iter n1 g f a)) =
 462 f (g (transpose n1 (S n1) (S n1)))
 463 (f (g (transpose n1 (S n1) n1))
 464 (map_iter n1 (\lambda m. g (transpose n1 (S n1) m)) f a)).
 465 cut (g (transpose n1 (S n1) (S n1))) = g n1.
 466 cut (g (transpose n1 (S n1) n1)) = g (S n1).
 467 cut map_iter n1 (\lambda m. g (transpose n1 (S n1) m)) f a = map_iter n1 g f a.
 468 rewrite > Hcut1.rewrite > Hcut2.rewrite > Hcut3.
 469 rewrite < H.
 470 rewrite > H1 (g (S n1)).
 471 rewrite > H.reflexivity.
 472 apply eq_map_iter.
 473 intros.unfold transpose.
 474 rewrite > not_eq_to_eqb_false m n1.
 475 rewrite > not_eq_to_eqb_false m (S n1).
 476 simplify.reflexivity.
 477 simplify. intro.apply lt_to_not_eq m (S n1).
 478 apply trans_lt ? n1.assumption.simplify. apply le_n.
 479 assumption.
 480 simplify. intro.apply lt_to_not_eq m n1.
 481 assumption.assumption.
 482 unfold transpose.
 483 rewrite > eqb_n_n n1.simplify.reflexivity.
 484 unfold transpose.
 485 rewrite > not_eq_to_eqb_false.simplify.
 486 rewrite > eqb_n_n n1.simplify.reflexivity.
 487 simplify. intro.
 488 apply not_eq_n_Sn n1. apply sym_eq.assumption.
 489 apply le_to_or_lt_eq.
 490 apply le_S_S_to_le.assumption.
 491 qed.
 492
 493 theorem eq_map_iter_transpose: \forall f:nat\to nat \to nat.associative nat f \to
 494 symmetric2 nat nat f \to \forall n,a,k:nat.
 495 \forall g:nat \to nat. \forall i:nat. S (k + i) \le n \to
 496 map_iter (S n) g  f a = map_iter (S n) (\lambda m. g (transpose i (S(k + i)) m)) f a.
 497 intros 6.
 498 apply nat_elim1 k.
 499 intro.
 500 apply nat_case m ?.
 501 intros.
 502 apply eq_map_iter_transpose_i_Si ? H H1.
 503 exact H3.
 504 intros.
 505 apply trans_eq ? ? (map_iter (S n) (\lambda m. g (transpose i (S(m1 + i)) m)) f a).
 506 apply H2.
 507 simplify. apply le_n.
 508 apply trans_le ? (S(S (m1+i))).
 509 apply le_S.apply le_n.assumption.
 510 apply trans_eq ? ? (map_iter (S n) (\lambda m. g
 511 (transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f a).
 512 apply H2 O ? ? (S(m1+i)).
 513 simplify.apply le_S_S.apply le_O_n.
 514 exact H3.
 515 apply trans_eq ? ? (map_iter (S n) (\lambda m. g
 516 (transpose i (S(m1 + i))
 517 (transpose (S(m1 + i)) (S(S(m1 + i)))
 518 (transpose i (S(m1 + i)) m)))) f a).
 519 apply H2 m1 ?.
 520 simplify. apply le_n.
 521 apply trans_le ? (S(S (m1+i))).
 522 apply le_S.apply le_n.assumption.
 523 apply eq_map_iter.
 524 intros.apply eq_f.
 525 apply sym_eq. apply eq_transpose.
 526 simplify. intro.
 527 apply not_le_Sn_n i.
 528 rewrite < H5 in \vdash (? ? %).
 529 apply le_S_S.apply le_S.
 530 apply le_plus_n.
 531 simplify. intro.
 532 apply not_le_Sn_n i.
 533 rewrite > H5 in \vdash (? ? %).
 534 apply le_S_S.
 535 apply le_plus_n.
 536 simplify. intro.
 537 apply not_eq_n_Sn (S m1+i).
 538 apply sym_eq.assumption.
 539 qed.
 540
 541 theorem eq_map_iter_transpose1: \forall f:nat\to nat \to nat.associative nat f \to
 542 symmetric2 nat nat f \to \forall n,a,i,j:nat.
 543 \forall g:nat \to nat. i < j \to j \le n \to
 544 map_iter (S n) g f a = map_iter (S n) (\lambda m. g (transpose i j m)) f a.
 545 intros.
 546 simplify in H2.
 547 cut (S i) < j \lor (S i) = j.
 548 elim Hcut.
 549 cut j = S ((j - (S i)) + i).
 550 rewrite > Hcut1.
 551 apply eq_map_iter_transpose f H H1 n a (j - (S i)) g i.
 552 rewrite < Hcut1.assumption.
 553 rewrite > plus_n_Sm.
 554 apply plus_minus_m_m.apply lt_to_le.assumption.
 555 rewrite < H4.
 556 apply eq_map_iter_transpose_i_Si f H H1 g.
 557 simplify.
 558 apply trans_le ? j.assumption.assumption.
 559 apply le_to_or_lt_eq.assumption.
 560 qed.
 561
 562 theorem eq_map_iter_transpose2: \forall f:nat\to nat \to nat.associative nat f \to
 563 symmetric2 nat nat f \to \forall n,a,i,j:nat.
 564 \forall g:nat \to nat. i \le n \to j \le n \to
 565 map_iter (S n) g f a = map_iter (S n) (\lambda m. g (transpose i j m)) f a.
 566 intros.
 567 apply nat_compare_elim i j.
 568 intro.apply eq_map_iter_transpose1 f H H1 n a  i j g H4 H3.
 569 intro.rewrite > H4.
 570 apply eq_map_iter.intros.
 571 rewrite > transpose_i_i j.reflexivity.
 572 intro.
 573 apply trans_eq ? ? (map_iter (S n) (\lambda m:nat.g (transpose j i m)) f a).
 574 apply eq_map_iter_transpose1 f H H1 n a j i g H4 H2.
 575 apply eq_map_iter.
 576 intros.apply eq_f.apply transpose_i_j_j_i.
 577 qed.
 578
 579 theorem permut_to_eq_map_iter:\forall f:nat\to nat \to nat.associative nat f \to
 580 symmetric2 nat nat f \to \forall a,n:nat.\forall g,h:nat \to nat.
 581 permut h n \to
 582 map_iter (S n) g f a = map_iter (S n) (\lambda m.g(h m)) f a.
 583 intros 5.elim n.
 584 simplify.rewrite > permut_O_to_eq_O h.reflexivity.assumption.
 585 apply trans_eq ? ? (map_iter (S(S n1)) (\lambda m.g ((transpose (h (S n1)) (S n1)) m)) f a).
 586 apply eq_map_iter_transpose2 f H H1 (S n1) a ? ? g.
 587 unfold permut in H3.
 588 elim H3.apply H4.apply le_n.apply le_n.
 589 apply trans_eq ? ? (map_iter (S(S n1)) (\lambda m.
 590 (g(transpose (h (S n1)) (S n1)
 591 (transpose (h (S n1)) (S n1) (h m)))) )f a).
 592 change with
 593 f (g (transpose (h (S n1)) (S n1) (S n1)))
 594 (map_iter (S n1) (\lambda m.
 595 g (transpose (h (S n1)) (S n1) m)) f a)
 596 =
 597 f
 598 (g(transpose (h (S n1)) (S n1)
 599 (transpose (h (S n1)) (S n1) (h (S n1)))))
 600 (map_iter (S n1)
 601 (\lambda m.
 602 (g(transpose (h (S n1)) (S n1)
 603 (transpose (h (S n1)) (S n1) (h m))))) f a).
 604 apply eq_f2.apply eq_f.
 605 rewrite > transpose_i_j_j.
 606 rewrite > transpose_i_j_i.
 607 rewrite > transpose_i_j_j.reflexivity.
 608 apply H2 (\lambda m.(g(transpose (h (S n1)) (S n1) m))).
 609 apply permut_S_to_permut_transpose.
 610 assumption.
 611 apply eq_map_iter.intros.
 612 rewrite > transpose_transpose.reflexivity.
 613 qed.
 614
 615 theorem eq_sigma_transpose_i_Si: \forall n,i:nat. \forall f:nat \to nat. i \lt n \to
 616 sigma (S n) f = sigma (S n) (\lambda m. f (transpose i (S i) m)).
 617 intro.elim n.apply False_ind.apply not_le_Sn_O i H.
 618 simplify in H1.
 619 cut i < n1 \lor i = n1.
 620 change with
 621 (f (S n1))+(sigma (S n1) f) =
 622 (f (transpose i (S i) (S n1)))+(sigma (S n1) (\lambda m. f (transpose i (S i) m))).
 623 elim Hcut.
 624 cut f (transpose i (S i) (S n1)) = f (S n1).
 625 rewrite > Hcut1.
 626 rewrite < H i f.reflexivity.
 627 assumption.unfold transpose.
 628 rewrite > not_eq_to_eqb_false (S n1) i.
 629 rewrite > not_eq_to_eqb_false (S n1) (S i).
 630 simplify.reflexivity.
 631 simplify.intro.
 632 apply lt_to_not_eq i n1 H2.
 633 apply injective_S i.apply sym_eq.assumption.
 634 simplify. intro.
 635 apply lt_to_not_eq i (S n1).
 636 apply trans_lt ? n1.assumption.simplify.apply le_n.
 637 apply sym_eq.assumption.
 638 rewrite > H2.
 639 change with (f (S n1))+((f n1)+(sigma n1 f)) =
 640 (f (transpose n1 (S n1) (S n1)))+
 641 ((f (transpose n1 (S n1) n1))+
 642 (sigma n1 (\lambda m. f (transpose n1 (S n1) m)))).
 643 cut (f (transpose n1 (S n1) (S n1))) = f n1.
 644 cut (f (transpose n1 (S n1) n1)) = f (S n1).
 645 cut sigma n1 (\lambda m. f (transpose n1 (S n1) m)) = sigma n1 f.
 646 rewrite > Hcut1.rewrite > Hcut2.rewrite > Hcut3.
 647 rewrite < assoc_plus.rewrite > sym_plus (f (S n1)).
 648 rewrite > assoc_plus.reflexivity.
 649 apply eq_sigma.
 650 intros.unfold transpose.
 651 rewrite > not_eq_to_eqb_false m n1.
 652 rewrite > not_eq_to_eqb_false m (S n1).
 653 simplify.reflexivity.
 654 simplify. intro.apply lt_to_not_eq m (S n1).
 655 apply trans_lt ? n1.assumption.simplify. apply le_n.
 656 assumption.
 657 simplify. intro.apply lt_to_not_eq m n1.
 658 assumption.assumption.
 659 unfold transpose.
 660 rewrite > eqb_n_n n1.simplify.reflexivity.
 661 unfold transpose.
 662 rewrite > not_eq_to_eqb_false.simplify.
 663 rewrite > eqb_n_n n1.simplify.reflexivity.
 664 simplify. intro.
 665 apply not_eq_n_Sn n1. apply sym_eq.assumption.
 666 apply le_to_or_lt_eq.
 667 apply le_S_S_to_le.assumption.
 668 qed.
 669
 670 theorem eq_sigma_transpose: \forall n,k:nat. \forall f:nat \to nat.
 671 \forall i. S (k + i) \le n \to
 672 sigma (S n) f = sigma (S n) (\lambda m. f (transpose i (S(k + i)) m)).
 673 intros 2.
 674 apply nat_elim1 k.
 675 intro.
 676 apply nat_case m ?.
 677 intros.
 678 apply eq_sigma_transpose_i_Si n i f.
 679 exact H1.
 680 intros.
 681 apply trans_eq ? ? (sigma (S n) (\lambda m. f (transpose i (S(m1 + i)) m))).
 682 apply H m1 ? f ?.
 683 simplify. apply le_n.
 684 apply trans_le ? (S(S (m1+i))).
 685 apply le_S.apply le_n.assumption.
 686 apply trans_eq ? ? (sigma (S n) (\lambda m. f
 687 (transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m)))).
 688 apply H O ? ? (S(m1+i)) ?.
 689 simplify.apply le_S_S.apply le_O_n.
 690 exact H1.
 691 apply trans_eq ? ? (sigma (S n) (\lambda m. f
 692 (transpose i (S(m1 + i))
 693 (transpose (S(m1 + i)) (S(S(m1 + i)))
 694 (transpose i (S(m1 + i)) m))))).
 695 apply H m1 ? ? i.
 696 simplify. apply le_n.
 697 apply trans_le ? (S(S (m1+i))).
 698 apply le_S.apply le_n.assumption.
 699 apply eq_sigma.
 700 intros.apply eq_f.
 701 apply sym_eq. apply eq_transpose.
 702 simplify. intro.
 703 apply not_le_Sn_n i.
 704 rewrite < H3 in \vdash (? ? %).
 705 apply le_S_S.apply le_S.
 706 apply le_plus_n.
 707 simplify. intro.
 708 apply not_le_Sn_n i.
 709 rewrite > H3 in \vdash (? ? %).
 710 apply le_S_S.
 711 apply le_plus_n.
 712 simplify. intro.
 713 apply not_eq_n_Sn (S m1+i).
 714 apply sym_eq.assumption.
 715 qed.
 716
 717 (*
 718 theorem bad: \forall n:nat. \forall f:nat \to nat.
 719 permut f n \to sigma (S n) f = sigma (S n) (\lambda n.n).
 720 intro.elim n.
 721 simplify.unfold permut in H.elim H O.
 722 rewrite < (le_n_O_to_eq (f O)).simplify. reflexivity.apply le_n.
 723 cut permut (\lambda n.transpose (f (S n1)) (S n1) (f n)) n1.
 724 apply trans_eq ? ?
 725 (sigma (S(S n1)) (\lambda n.transpose (f (S n1)) (S n1) (f n))).
 726 *)