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