matita/contribs/library_auto/auto/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/library_autobatch/nat/permutation".
  16
  17 include "auto/nat/compare.ma".
  18 include "auto/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.
  26 unfold injn.
  27 intros.
  28 apply H;autobatch.
  29 (*[ apply le_S.
  30   assumption
  31 | apply le_S.
  32   assumption
  33 | assumption
  34 ]*)
  35 qed.
  36
  37 theorem injective_to_injn: \forall f:nat \to nat. \forall n:nat.
  38 injective nat nat f \to injn f n.
  39 unfold injective.
  40 unfold injn.
  41 intros.autobatch.
  42 (*apply H.
  43 assumption.*)
  44 qed.
  45
  46 definition permut : (nat \to nat) \to nat \to Prop
  47 \def \lambda f:nat \to nat. \lambda m:nat.
  48 (\forall i:nat. i \le m \to f i \le m )\land injn f m.
  49
  50 theorem permut_O_to_eq_O: \forall h:nat \to nat.
  51 permut h O \to (h O) = O.
  52 intros.
  53 unfold permut in H.
  54 elim H.
  55 apply sym_eq.autobatch.
  56 (*apply le_n_O_to_eq.
  57 apply H1.
  58 apply le_n.*)
  59 qed.
  60
  61 theorem permut_S_to_permut: \forall f:nat \to nat. \forall m:nat.
  62 permut f (S m) \to f (S m) = (S m) \to permut f m.
  63 unfold permut.
  64 intros.
  65 elim H.
  66 split
  67 [ intros.
  68   cut (f i < S m \lor f i = S m)
  69   [ elim Hcut
  70     [ autobatch
  71       (*apply le_S_S_to_le.
  72       assumption*)
  73     | apply False_ind.
  74       apply (not_le_Sn_n m).
  75       cut ((S m) = i)
  76       [ rewrite > Hcut1.
  77         assumption
  78       | apply H3
  79         [ apply le_n
  80         | autobatch
  81           (*apply le_S.
  82           assumption*)
  83         | autobatch
  84           (*rewrite > H5.
  85           assumption*)
  86         ]
  87       ]
  88     ]
  89   | apply le_to_or_lt_eq.
  90     autobatch
  91     (*apply H2.
  92     apply le_S.
  93     assumption*)
  94   ]
  95 | apply (injn_Sn_n f m H3)
  96 ]
  97 qed.
  98
  99 (* transpositions *)
 100
 101 definition transpose : nat \to nat \to nat \to nat \def
 102 \lambda i,j,n:nat.
 103 match eqb n i with
 104   [ true \Rightarrow j
 105   | false \Rightarrow
 106       match eqb n j with
 107       [ true \Rightarrow i
 108       | false \Rightarrow n]].
 109
 110 notation < "(❲i↹j❳)n"
 111   right associative with precedence 71
 112 for @{ 'transposition $i $j $n}.
 113
 114 notation < "(❲i \atop j❳)n"
 115   right associative with precedence 71
 116 for @{ 'transposition $i $j $n}.
 117
 118 interpretation "natural transposition" 'transposition i j n =
 119   (cic:/matita/library_autobatch/nat/permutation/transpose.con i j n).
 120
 121 lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j.
 122 intros.
 123 unfold transpose.
 124 (*dopo circa 6 minuti, l'esecuzione di autobatch in questo punto non era ancora terminata*)
 125 rewrite > (eqb_n_n i).autobatch.
 126 (*simplify.
 127 reflexivity.*)
 128 qed.
 129
 130 lemma transpose_i_j_j: \forall i,j:nat. transpose i j j = i.
 131 intros.
 132 unfold transpose.
 133 apply (eqb_elim j i)
 134 [ autobatch
 135   (*simplify.
 136   intro.
 137   assumption*)
 138 | rewrite > (eqb_n_n j).
 139   simplify.
 140   intros.
 141   reflexivity
 142 ]
 143 qed.
 144
 145 theorem transpose_i_i:  \forall i,n:nat. (transpose  i i n) = n.
 146 intros.
 147 unfold transpose.
 148 apply (eqb_elim n i)
 149 [ autobatch
 150   (*intro.
 151   simplify.
 152   apply sym_eq.
 153   assumption*)
 154 | intro.
 155   autobatch
 156   (*simplify.
 157   reflexivity*)
 158 ]
 159 qed.
 160
 161 theorem transpose_i_j_j_i: \forall i,j,n:nat.
 162 transpose i j n = transpose j i n.
 163 intros.
 164 unfold transpose.
 165 apply (eqb_elim n i)
 166 [ apply (eqb_elim n j)
 167   [ intros.
 168     (*l'esecuzione di autobatch in questo punto, dopo circa 300 secondi, non era ancora terminata*)
 169     simplify.autobatch
 170     (*rewrite < H.
 171     rewrite < H1.
 172     reflexivity*)
 173   | intros.
 174     autobatch
 175     (*simplify.
 176     reflexivity*)
 177   ]
 178 | apply (eqb_elim n j)
 179   [ intros.autobatch
 180     (*simplify.reflexivity *)
 181   | intros.autobatch
 182     (*simplify.reflexivity*)
 183   ]
 184 ]
 185 qed.
 186
 187 theorem transpose_transpose: \forall i,j,n:nat.
 188 (transpose i j (transpose i j n)) = n.
 189 intros.
 190 unfold transpose.
 191 unfold transpose.
 192 apply (eqb_elim n i)
 193 [ simplify.
 194   intro.
 195   apply (eqb_elim j i)
 196   [ simplify.
 197     intros.
 198     autobatch
 199     (*rewrite > H.
 200     rewrite > H1.
 201     reflexivity*)
 202   | rewrite > (eqb_n_n j).
 203     simplify.
 204     intros.
 205     autobatch
 206     (*apply sym_eq.
 207     assumption*)
 208   ]
 209 | apply (eqb_elim n j)
 210   [ simplify.
 211     rewrite > (eqb_n_n i).
 212     intros.
 213     autobatch
 214     (*simplify.
 215     apply sym_eq.
 216     assumption*)
 217   | simplify.
 218     intros.
 219     (*l'esecuzione di autobatch in questo punto, dopo piu' di 6 minuti non era ancora terminata*)
 220     rewrite > (not_eq_to_eqb_false n i H1).
 221     (*l'esecuzione di autobatch in questo punto, dopo piu' alcuni minuti non era ancora terminata*)
 222     rewrite > (not_eq_to_eqb_false n j H).autobatch
 223     (*simplify.
 224     reflexivity*)
 225   ]
 226 ]
 227 qed.
 228
 229 theorem injective_transpose : \forall i,j:nat.
 230 injective nat nat (transpose i j).
 231 unfold injective.
 232 intros.autobatch.
 233 (*rewrite < (transpose_transpose i j x).
 234 rewrite < (transpose_transpose i j y).
 235 apply eq_f.
 236 assumption.*)
 237 qed.
 238
 239 variant inj_transpose: \forall i,j,n,m:nat.
 240 transpose i j n = transpose i j m \to n = m \def
 241 injective_transpose.
 242
 243 theorem permut_transpose: \forall i,j,n:nat. i \le n \to j \le n \to
 244 permut (transpose i j) n.
 245 unfold permut.
 246 intros.
 247 split
 248 [ unfold transpose.
 249   intros.
 250   elim (eqb i1 i)
 251   [ (*qui autobatch non chiude il goal*)
 252     simplify.
 253     assumption
 254   | elim (eqb i1 j)
 255     [ (*aui autobatch non chiude il goal*)
 256       simplify.
 257       assumption
 258     | (*aui autobatch non chiude il goal*)
 259       simplify.
 260       assumption
 261     ]
 262   ]
 263 | autobatch
 264   (*apply (injective_to_injn (transpose i j) n).
 265   apply injective_transpose*)
 266 ]
 267 qed.
 268
 269 theorem permut_fg: \forall f,g:nat \to nat. \forall n:nat.
 270 permut f n \to permut g n \to permut (\lambda m.(f(g m))) n.
 271 unfold permut.
 272 intros.
 273 elim H.
 274 elim H1.
 275 split
 276 [ intros.
 277   simplify.
 278   autobatch
 279   (*apply H2.
 280   apply H4.
 281   assumption*)
 282 | simplify.
 283   intros.
 284   apply H5
 285   [ assumption
 286   | assumption
 287   | apply H3
 288     [ autobatch
 289       (*apply H4.
 290       assumption*)
 291     | autobatch
 292       (*apply H4.
 293       assumption*)
 294     | assumption
 295     ]
 296   ]
 297 ]
 298 qed.
 299
 300 theorem permut_transpose_l:
 301 \forall f:nat \to nat. \forall m,i,j:nat.
 302 i \le m \to j \le m \to permut f m \to permut (\lambda n.transpose i j (f n)) m.
 303 intros.
 304 autobatch.
 305 (*apply (permut_fg (transpose i j) f m ? ?)
 306 [ apply permut_transpose;assumption
 307 | assumption
 308 ]*)
 309 qed.
 310
 311 theorem permut_transpose_r:
 312 \forall f:nat \to nat. \forall m,i,j:nat.
 313 i \le m \to j \le m \to permut f m \to permut (\lambda n.f (transpose i j n)) m.
 314 intros.autobatch.
 315 (*apply (permut_fg f (transpose i j) m ? ?)
 316 [ assumption
 317 | apply permut_transpose;assumption
 318 ]*)
 319 qed.
 320
 321 theorem eq_transpose : \forall i,j,k,n:nat. \lnot j=i \to
 322  \lnot i=k \to \lnot j=k \to
 323 transpose i j n = transpose i k (transpose k j (transpose i k n)).
 324 (* uffa: triplo unfold? *)
 325 intros.unfold transpose.
 326 unfold transpose.
 327 unfold transpose.
 328 apply (eqb_elim n i)
 329 [ intro.
 330   simplify.
 331   rewrite > (eqb_n_n k).
 332   simplify.
 333   rewrite > (not_eq_to_eqb_false j i H).
 334   rewrite > (not_eq_to_eqb_false j k H2).
 335   reflexivity
 336 | intro.
 337   apply (eqb_elim n j)
 338   [ intro.
 339     cut (\lnot n = k)
 340     [ cut (\lnot n = i)
 341       [ rewrite > (not_eq_to_eqb_false n k Hcut).
 342         simplify.
 343         rewrite > (not_eq_to_eqb_false n k Hcut).
 344         rewrite > (eq_to_eqb_true n j H4).
 345         simplify.
 346         rewrite > (not_eq_to_eqb_false k i)
 347         [ rewrite > (eqb_n_n k).
 348           autobatch
 349           (*simplify.
 350           reflexivity*)
 351         | unfold Not.
 352           intro.autobatch
 353           (*apply H1.
 354           apply sym_eq.
 355           assumption*)
 356         ]
 357       | assumption
 358       ]
 359     | unfold Not.
 360       intro.autobatch
 361       (*apply H2.
 362       apply (trans_eq ? ? n)
 363       [ apply sym_eq.
 364         assumption
 365       | assumption
 366       ]*)
 367     ]
 368   | intro.
 369     apply (eqb_elim n k)
 370     [ intro.
 371       simplify.
 372       rewrite > (not_eq_to_eqb_false i k H1).
 373       rewrite > (not_eq_to_eqb_false i j)
 374       [ simplify.
 375         rewrite > (eqb_n_n i).
 376         autobatch
 377         (*simplify.
 378         assumption*)
 379       | unfold Not.
 380         intro.autobatch
 381         (*apply H.
 382         apply sym_eq.
 383         assumption*)
 384       ]
 385     | intro.
 386       simplify.
 387       rewrite > (not_eq_to_eqb_false n k H5).
 388       rewrite > (not_eq_to_eqb_false n j H4).
 389       simplify.
 390       rewrite > (not_eq_to_eqb_false n i H3).
 391       rewrite > (not_eq_to_eqb_false n k H5).
 392       autobatch
 393       (*simplify.
 394       reflexivity*)
 395     ]
 396   ]
 397 ]
 398 qed.
 399
 400 theorem permut_S_to_permut_transpose: \forall f:nat \to nat.
 401 \forall m:nat. permut f (S m) \to permut (\lambda n.transpose (f (S m)) (S m)
 402 (f n)) m.
 403 unfold permut.
 404 intros.
 405 elim H.
 406 split
 407 [ intros.
 408   simplify.
 409   unfold transpose.
 410   apply (eqb_elim (f i) (f (S m)))
 411   [ intro.
 412     apply False_ind.
 413     cut (i = (S m))
 414     [ apply (not_le_Sn_n m).
 415       rewrite < Hcut.
 416       assumption
 417     | apply H2;autobatch
 418       (*[ apply le_S.
 419         assumption
 420       | apply le_n
 421       | assumption
 422       ]*)
 423     ]
 424   | intro.
 425     simplify.
 426     apply (eqb_elim (f i) (S m))
 427     [ intro.
 428       cut (f (S m) \lt (S m) \lor f (S m) = (S m))
 429       [ elim Hcut
 430         [ apply le_S_S_to_le.
 431           (*NB qui autobatch non chiude il goal*)
 432           assumption
 433         | apply False_ind.
 434           autobatch
 435           (*apply H4.
 436           rewrite > H6.
 437           assumption*)
 438         ]
 439       | autobatch
 440         (*apply le_to_or_lt_eq.
 441         apply H1.
 442         apply le_n*)
 443       ]
 444     | intro.simplify.
 445       cut (f i \lt (S m) \lor f i = (S m))
 446       [ elim Hcut
 447         [ autobatch
 448           (*apply le_S_S_to_le.
 449           assumption*)
 450         | apply False_ind.
 451           autobatch
 452           (*apply H5.
 453           assumption*)
 454         ]
 455       | apply le_to_or_lt_eq.
 456         autobatch
 457         (*apply H1.
 458         apply le_S.
 459         assumption*)
 460       ]
 461     ]
 462   ]
 463 | unfold injn.
 464   intros.
 465   apply H2;autobatch
 466   (*[ apply le_S.
 467     assumption
 468   | apply le_S.
 469     assumption
 470   | apply (inj_transpose (f (S m)) (S m)).
 471     apply H5
 472   ]*)
 473 ]
 474 qed.
 475
 476 (* bounded bijectivity *)
 477
 478 definition bijn : (nat \to nat) \to nat \to Prop \def
 479 \lambda f:nat \to nat. \lambda n. \forall m:nat. m \le n \to
 480 ex nat (\lambda p. p \le n \land f p = m).
 481
 482 theorem eq_to_bijn:  \forall f,g:nat\to nat. \forall n:nat.
 483 (\forall i:nat. i \le n \to (f i) = (g i)) \to
 484 bijn f n \to bijn g n.
 485 intros 4.
 486 unfold bijn.
 487 intros.
 488 elim (H1 m)
 489 [ apply (ex_intro ? ? a).
 490   rewrite < (H a)
 491   [ assumption
 492   | elim H3.
 493     assumption
 494   ]
 495 | assumption
 496 ]
 497 qed.
 498
 499 theorem bijn_Sn_n: \forall f:nat \to nat. \forall n:nat.
 500 bijn f (S n) \to f (S n) = (S n) \to bijn f n.
 501 unfold bijn.
 502 intros.
 503 elim (H m)
 504 [ elim H3.
 505   apply (ex_intro ? ? a).
 506   split
 507   [ cut (a < S n \lor a = S n)
 508     [ elim Hcut
 509       [ autobatch
 510         (*apply le_S_S_to_le.
 511         assumption*)
 512       | apply False_ind.
 513         apply (not_le_Sn_n n).
 514         rewrite < H1.
 515         rewrite < H6.
 516         rewrite > H5.
 517         assumption
 518       ]
 519     | autobatch
 520       (*apply le_to_or_lt_eq.
 521       assumption*)
 522     ]
 523   | assumption
 524   ]
 525 | autobatch
 526   (*apply le_S.
 527   assumption*)
 528 ]
 529 qed.
 530
 531 theorem bijn_n_Sn: \forall f:nat \to nat. \forall n:nat.
 532 bijn f n \to f (S n) = (S n) \to bijn f (S n).
 533 unfold bijn.
 534 intros.
 535 cut (m < S n \lor m = S n)
 536 [ elim Hcut
 537   [ elim (H m)
 538     [ elim H4.
 539       apply (ex_intro ? ? a).
 540       autobatch
 541       (*split
 542       [ apply le_S.
 543         assumption
 544       | assumption
 545       ]*)
 546     | autobatch
 547       (*apply le_S_S_to_le.
 548       assumption*)
 549     ]
 550   | autobatch
 551     (*apply (ex_intro ? ? (S n)).
 552     split
 553     [ apply le_n
 554     | rewrite > H3.
 555       assumption
 556     ]*)
 557   ]
 558 | autobatch
 559   (*apply le_to_or_lt_eq.
 560   assumption*)
 561 ]
 562 qed.
 563
 564 theorem bijn_fg: \forall f,g:nat\to nat. \forall n:nat.
 565 bijn f n \to bijn g n \to bijn (\lambda p.f(g p)) n.
 566 unfold bijn.
 567 intros.
 568 simplify.
 569 elim (H m)
 570 [ elim H3.
 571   elim (H1 a)
 572   [ elim H6.
 573     autobatch
 574     (*apply (ex_intro ? ? a1).
 575     split
 576     [ assumption
 577     | rewrite > H8.
 578       assumption
 579     ]*)
 580   | assumption
 581   ]
 582 | assumption
 583 ]
 584 qed.
 585
 586 theorem bijn_transpose : \forall n,i,j. i \le n \to j \le n \to
 587 bijn (transpose i j) n.
 588 intros.
 589 unfold bijn.
 590 unfold transpose.
 591 intros.
 592 cut (m = i \lor \lnot m = i)
 593 [ elim Hcut
 594   [ apply (ex_intro ? ? j).
 595     split
 596     [ assumption
 597     | apply (eqb_elim j i)
 598       [ intro.
 599         (*dopo circa 360 secondi l'esecuzione di autobatch in questo punto non era ancora terminata*)
 600         simplify.
 601         autobatch
 602         (*rewrite > H3.
 603         rewrite > H4.
 604         reflexivity*)
 605       | rewrite > (eqb_n_n j).
 606         simplify.
 607         intros.
 608         autobatch
 609         (*apply sym_eq.
 610         assumption*)
 611       ]
 612     ]
 613   | cut (m = j \lor \lnot m = j)
 614     [ elim Hcut1
 615       [ apply (ex_intro ? ? i).
 616         split
 617         [ assumption
 618         | (*dopo circa 5 minuti, l'esecuzione di autobatch in questo punto non era ancora terminata*)
 619           rewrite > (eqb_n_n i).
 620           autobatch
 621           (*simplify.
 622           apply sym_eq.
 623           assumption*)
 624         ]
 625       | apply (ex_intro ? ? m).
 626         split
 627         [ assumption
 628         | rewrite > (not_eq_to_eqb_false m i)
 629           [ (*dopo circa 5 minuti, l'esecuzione di autobatch in questo punto non era ancora terminata*)
 630             rewrite > (not_eq_to_eqb_false m j)
 631             [ autobatch
 632               (*simplify.
 633               reflexivity*)
 634             | assumption
 635             ]
 636           | assumption
 637           ]
 638         ]
 639       ]
 640     | apply (decidable_eq_nat m j)
 641     ]
 642   ]
 643 | apply (decidable_eq_nat m i)
 644 ]
 645 qed.
 646
 647 theorem bijn_transpose_r: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
 648 bijn f n \to bijn (\lambda p.f (transpose i j p)) n.
 649 intros.autobatch.
 650 (*apply (bijn_fg f ?)
 651 [ assumption
 652 | apply (bijn_transpose n i j)
 653   [ assumption
 654   | assumption
 655   ]
 656 ]*)
 657 qed.
 658
 659 theorem bijn_transpose_l: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
 660 bijn f n \to bijn (\lambda p.transpose i j (f p)) n.
 661 intros.
 662 autobatch.
 663 (*apply (bijn_fg ? f)
 664 [ apply (bijn_transpose n i j)
 665   [ assumption
 666   | assumption
 667   ]
 668 | assumption
 669 ]*)
 670 qed.
 671
 672 theorem permut_to_bijn: \forall n:nat.\forall f:nat\to nat.
 673 permut f n \to bijn f n.
 674 intro.
 675 elim n
 676 [ unfold bijn.
 677   intros.
 678   apply (ex_intro ? ? m).
 679   split
 680   [ assumption
 681   | apply (le_n_O_elim m ? (\lambda p. f p = p))
 682     [ assumption
 683     | unfold permut in H.
 684       elim H.
 685       apply sym_eq.
 686       autobatch
 687       (*apply le_n_O_to_eq.
 688       apply H2.
 689       apply le_n*)
 690     ]
 691   ]
 692 | apply (eq_to_bijn (\lambda p.
 693   (transpose (f (S n1)) (S n1)) (transpose (f (S n1)) (S n1) (f p))) f)
 694   [ intros.
 695     apply transpose_transpose
 696   | apply (bijn_fg (transpose (f (S n1)) (S n1)))
 697     [ apply bijn_transpose
 698       [ unfold permut in H1.
 699         elim H1.autobatch
 700         (*apply H2.
 701         apply le_n*)
 702       | apply le_n
 703       ]
 704     | apply bijn_n_Sn
 705       [ apply H.
 706         autobatch
 707         (*apply permut_S_to_permut_transpose.
 708         assumption*)
 709       | autobatch
 710         (*unfold transpose.
 711         rewrite > (eqb_n_n (f (S n1))).
 712         simplify.
 713         reflexivity*)
 714       ]
 715     ]
 716   ]
 717 ]
 718 qed.
 719
 720 let rec invert_permut n f m \def
 721   match eqb m (f n) with
 722   [true \Rightarrow n
 723   |false \Rightarrow
 724      match n with
 725      [O \Rightarrow O
 726      |(S p) \Rightarrow invert_permut p f m]].
 727
 728 theorem invert_permut_f: \forall f:nat \to nat. \forall n,m:nat.
 729 m \le n \to injn f n\to invert_permut n f (f m) = m.
 730 intros 4.
 731 elim H
 732 [ apply (nat_case1 m)
 733   [ intro.
 734     simplify.
 735     (*l'applicazione di autobatch in questo punto, dopo alcuni minuti, non aveva ancora dato risultati*)
 736     rewrite > (eqb_n_n (f O)).
 737     autobatch
 738     (*simplify.
 739     reflexivity*)
 740   | intros.simplify.
 741     (*l'applicazione di autobatch in questo punto, dopo alcuni minuti, non aveva ancora dato risultati*)
 742     rewrite > (eqb_n_n (f (S m1))).
 743     autobatch
 744     (*simplify.
 745     reflexivity*)
 746   ]
 747 | simplify.
 748   rewrite > (not_eq_to_eqb_false (f m) (f (S n1)))
 749   [ (*l'applicazione di autobatch in questo punto, dopo parecchi secondi, non aveva ancora prodotto un risultato*)
 750     simplify.
 751     autobatch
 752     (*apply H2.
 753     apply injn_Sn_n.
 754     assumption*)
 755   | unfold Not.
 756     intro.
 757     absurd (m = S n1)
 758     [ apply H3;autobatch
 759       (*[ apply le_S.
 760         assumption
 761       | apply le_n
 762       | assumption
 763       ]*)
 764     | unfold Not.
 765       intro.
 766       apply (not_le_Sn_n n1).
 767       rewrite < H5.
 768       assumption
 769     ]
 770   ]
 771 ]
 772 qed.
 773
 774 theorem injective_invert_permut: \forall f:nat \to nat. \forall n:nat.
 775 permut f n \to injn (invert_permut n f) n.
 776 intros.
 777 unfold injn.
 778 intros.
 779 cut (bijn f n)
 780 [ unfold bijn in Hcut.
 781   generalize in match (Hcut i H1).
 782   intro.
 783   generalize in match (Hcut j H2).
 784   intro.
 785   elim H4.
 786   elim H6.
 787   elim H5.
 788   elim H9.
 789   rewrite < H8.
 790   rewrite < H11.
 791   apply eq_f.
 792   rewrite < (invert_permut_f f n a)
 793   [ rewrite < (invert_permut_f f n a1)
 794     [ rewrite > H8.
 795       rewrite > H11.
 796       assumption
 797     | assumption
 798     | unfold permut in H.elim H.
 799       assumption
 800     ]
 801   | assumption
 802   | unfold permut in H.
 803     elim H.
 804     assumption
 805   ]
 806 | autobatch
 807   (*apply permut_to_bijn.
 808   assumption*)
 809 ]
 810 qed.
 811
 812 theorem permut_invert_permut: \forall f:nat \to nat. \forall n:nat.
 813 permut f n \to permut (invert_permut n f) n.
 814 intros.
 815 unfold permut.
 816 split
 817 [ intros.
 818   simplify.
 819   elim n
 820   [ simplify.
 821     elim (eqb i (f O));autobatch
 822     (*[ simplify.
 823       apply le_n
 824     | simplify.
 825       apply le_n
 826     ]*)
 827   | simplify.
 828     elim (eqb i (f (S n1)))
 829     [ autobatch
 830       (*simplify.
 831       apply le_n*)
 832     | simplify.
 833       autobatch
 834       (*apply le_S.
 835       assumption*)
 836     ]
 837   ]
 838 | autobatch
 839   (*apply injective_invert_permut.
 840   assumption.*)
 841 ]
 842 qed.
 843
 844 theorem f_invert_permut: \forall f:nat \to nat. \forall n,m:nat.
 845 m \le n \to permut f n\to f (invert_permut n f m) = m.
 846 intros.
 847 apply (injective_invert_permut f n H1)
 848 [ unfold permut in H1.
 849   elim H1.
 850   apply H2.
 851   cut (permut (invert_permut n f) n)
 852   [ unfold permut in Hcut.
 853     elim Hcut.autobatch
 854     (*apply H4.
 855     assumption*)
 856   | apply permut_invert_permut.
 857     (*NB qui autobatch non chiude il goal*)
 858     assumption
 859   ]
 860 | assumption
 861 | apply invert_permut_f
 862   [ cut (permut (invert_permut n f) n)
 863     [ unfold permut in Hcut.
 864       elim Hcut.
 865       autobatch
 866       (*apply H2.
 867       assumption*)
 868     | autobatch
 869       (*apply permut_invert_permut.
 870       assumption*)
 871     ]
 872   | unfold permut in H1.
 873     elim H1.
 874     assumption
 875   ]
 876 ]
 877 qed.
 878
 879 theorem permut_n_to_eq_n: \forall h:nat \to nat.\forall n:nat.
 880 permut h n \to (\forall m:nat. m < n \to h m = m) \to h n = n.
 881 intros.
 882 unfold permut in H.
 883 elim H.
 884 cut (invert_permut n h n < n \lor invert_permut n h n = n)
 885 [ elim Hcut
 886   [ rewrite < (f_invert_permut h n n) in \vdash (? ? ? %)
 887     [ apply eq_f.
 888       rewrite < (f_invert_permut h n n) in \vdash (? ? % ?)
 889       [ autobatch
 890         (*apply H1.
 891         assumption*)
 892       | apply le_n
 893       | (*qui autobatch NON chiude il goal*)
 894         assumption
 895       ]
 896     | apply le_n
 897     | (*qui autobatch NON chiude il goal*)
 898       assumption
 899     ]
 900   | rewrite < H4 in \vdash (? ? % ?).
 901     apply (f_invert_permut h)
 902     [ apply le_n
 903     | (*qui autobatch NON chiude il goal*)
 904       assumption
 905     ]
 906   ]
 907 | apply le_to_or_lt_eq.
 908   cut (permut (invert_permut n h) n)
 909   [ unfold permut in Hcut.
 910     elim Hcut.
 911     autobatch
 912     (*apply H4.
 913     apply le_n*)
 914   | apply permut_invert_permut.
 915     (*NB aui autobatch non chiude il goal*)
 916     assumption
 917   ]
 918 ]
 919 qed.
 920
 921 theorem permut_n_to_le: \forall h:nat \to nat.\forall k,n:nat.
 922 k \le n \to permut h n \to (\forall m:nat. m < k \to h m = m) \to
 923 \forall j. k \le j \to j \le n \to k \le h j.
 924 intros.
 925 unfold permut in H1.
 926 elim H1.
 927 cut (h j < k \lor \not(h j < k))
 928 [ elim Hcut
 929   [ absurd (k \le j)
 930     [ assumption
 931     | apply lt_to_not_le.
 932       cut (h j = j)
 933       [ rewrite < Hcut1.
 934         assumption
 935       | apply H6;autobatch
 936         (*[ apply H5.
 937           assumption
 938         | assumption
 939         | apply H2.
 940           assumption
 941         ]*)
 942       ]
 943     ]
 944   | autobatch
 945     (*apply not_lt_to_le.
 946     assumption*)
 947   ]
 948 | apply (decidable_lt (h j) k)
 949 ]
 950 qed.
 951
 952 (* applications *)
 953
 954 let rec map_iter_i k (g:nat \to nat) f (i:nat) \def
 955   match k with
 956    [ O \Rightarrow g i
 957    | (S k) \Rightarrow f (g (S (k+i))) (map_iter_i k g f i)].
 958
 959 theorem eq_map_iter_i: \forall g1,g2:nat \to nat.
 960 \forall f:nat \to nat \to nat. \forall n,i:nat.
 961 (\forall m:nat. i\le m \to m \le n+i \to g1 m = g2 m) \to
 962 map_iter_i n g1 f i = map_iter_i n g2 f i.
 963 intros 5.
 964 elim n
 965 [ simplify.
 966   autobatch
 967   (*apply H
 968   [ apply le_n
 969   | apply le_n
 970   ]*)
 971 | simplify.
 972   apply eq_f2
 973   [ autobatch
 974     (*apply H1
 975     [ simplify.
 976       apply le_S.
 977       apply le_plus_n
 978     | simplify.
 979       apply le_n
 980     ]*)
 981   | apply H.
 982     intros.
 983     apply H1;autobatch
 984     (*[ assumption
 985     | simplify.
 986       apply le_S.
 987       assumption
 988     ]*)
 989   ]
 990 ]
 991 qed.
 992
 993 (* map_iter examples *)
 994
 995 theorem eq_map_iter_i_sigma: \forall g:nat \to nat. \forall n,m:nat.
 996 map_iter_i n g plus m = sigma n g m.
 997 intros.
 998 elim n
 999 [ autobatch
1000   (*simplify.
1001   reflexivity*)
1002 | simplify.
1003   autobatch
1004   (*apply eq_f.
1005   assumption*)
1006 ]
1007 qed.
1008
1009 theorem eq_map_iter_i_pi: \forall g:nat \to nat. \forall n,m:nat.
1010 map_iter_i n g times m = pi n g m.
1011 intros.
1012 elim n
1013 [ autobatch
1014   (*simplify.
1015   reflexivity*)
1016 | simplify.
1017   autobatch
1018   (*apply eq_f.
1019   assumption*)
1020 ]
1021 qed.
1022
1023 theorem eq_map_iter_i_fact: \forall n:nat.
1024 map_iter_i n (\lambda m.m) times (S O) = (S n)!.
1025 intros.
1026 elim n
1027 [ autobatch
1028   (*simplify.
1029   reflexivity*)
1030 | change with
1031   (((S n1)+(S O))*(map_iter_i n1 (\lambda m.m) times (S O)) = (S(S n1))*(S n1)!).
1032   rewrite < plus_n_Sm.
1033   rewrite < plus_n_O.
1034   apply eq_f.
1035   (*NB: qui autobatch non chiude il goal!!!*)
1036   assumption
1037 ]
1038 qed.
1039
1040
1041 theorem eq_map_iter_i_transpose_l : \forall f:nat\to nat \to nat.associative nat f \to
1042 symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k:nat.
1043 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.
1044 intros.
1045 apply (nat_case1 k)
1046 [ intros.
1047   simplify.
1048   fold simplify (transpose n (S n) (S n)).
1049   autobatch
1050   (*rewrite > transpose_i_j_i.
1051   rewrite > transpose_i_j_j.
1052   apply H1*)
1053 | intros.
1054   change with
1055   (f (g (S (S (m+n)))) (f (g (S (m+n))) (map_iter_i m g f n)) =
1056   f (g (transpose (S m + n) (S (S m) + n) (S (S m)+n)))
1057   (f (g (transpose (S m + n) (S (S m) + n) (S m+n)))
1058   (map_iter_i m (\lambda m1. g (transpose (S m+n) (S (S m)+n) m1)) f n))).
1059   rewrite > transpose_i_j_i.
1060   rewrite > transpose_i_j_j.
1061   rewrite < H.
1062   rewrite < H.
1063   rewrite < (H1 (g (S m + n))).
1064   apply eq_f.
1065   apply eq_map_iter_i.
1066   intros.
1067   simplify.
1068   unfold transpose.
1069   rewrite > (not_eq_to_eqb_false m1 (S m+n))
1070   [ rewrite > (not_eq_to_eqb_false m1 (S (S m)+n))
1071     [ autobatch
1072       (*simplify.
1073       reflexivity*)
1074     | apply (lt_to_not_eq m1 (S ((S m)+n))).
1075       autobatch
1076       (*unfold lt.
1077       apply le_S_S.
1078       change with (m1 \leq S (m+n)).
1079       apply le_S.
1080       assumption*)
1081     ]
1082   | apply (lt_to_not_eq m1 (S m+n)).
1083     simplify.autobatch
1084     (*unfold lt.
1085     apply le_S_S.
1086     assumption*)
1087   ]
1088 ]
1089 qed.
1090
1091 theorem eq_map_iter_i_transpose_i_Si : \forall f:nat\to nat \to nat.associative nat f \to
1092 symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k,i:nat. n \le i \to i \le k+n \to
1093 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S i) m)) f n.
1094 intros 6.
1095 elim k
1096 [ cut (i=n)
1097   [ rewrite > Hcut.
1098     (*qui autobatch non chiude il goal*)
1099     apply (eq_map_iter_i_transpose_l f H H1 g n O)
1100   | apply antisymmetric_le
1101     [ assumption
1102     | assumption
1103     ]
1104   ]
1105 | cut (i < S n1 + n \lor i = S n1 + n)
1106   [ elim Hcut
1107     [ change with
1108       (f (g (S (S n1)+n)) (map_iter_i (S n1) g f n) =
1109       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)).
1110       apply eq_f2
1111       [ unfold transpose.
1112         rewrite > (not_eq_to_eqb_false (S (S n1)+n) i)
1113         [ rewrite > (not_eq_to_eqb_false (S (S n1)+n) (S i))
1114           [ autobatch
1115             (*simplify.
1116             reflexivity*)
1117           | simplify.
1118             unfold Not.
1119             intro.
1120             apply (lt_to_not_eq i (S n1+n))
1121             [ assumption
1122             | autobatch
1123               (*apply inj_S.
1124               apply sym_eq.
1125               assumption*)
1126             ]
1127           ]
1128         | simplify.
1129           unfold Not.
1130           intro.
1131           apply (lt_to_not_eq i (S (S n1+n)))
1132           [ autobatch
1133             (*simplify.
1134             unfold lt.
1135             apply le_S_S.
1136             assumption*)
1137           | autobatch
1138             (*apply sym_eq.
1139             assumption*)
1140           ]
1141         ]
1142       | apply H2;autobatch
1143         (*[ assumption
1144         | apply le_S_S_to_le.
1145           assumption
1146         ]*)
1147       ]
1148     | rewrite > H5.
1149       (*qui autobatch non chiude il goal*)
1150       apply (eq_map_iter_i_transpose_l f H H1 g n (S n1)).
1151     ]
1152   | autobatch
1153     (*apply le_to_or_lt_eq.
1154     assumption*)
1155   ]
1156 ]
1157 qed.
1158
1159 theorem eq_map_iter_i_transpose:
1160 \forall f:nat\to nat \to nat.
1161 associative nat f \to symmetric2 nat nat f \to \forall n,k,o:nat.
1162 \forall g:nat \to nat. \forall i:nat. n \le i \to S (o + i) \le S k+n \to
1163 map_iter_i (S k) g  f n = map_iter_i (S k) (\lambda m. g (transpose i (S(o + i)) m)) f n.
1164 intros 6.
1165 apply (nat_elim1 o).
1166 intro.
1167 apply (nat_case m ?)
1168 [ intros.
1169   apply (eq_map_iter_i_transpose_i_Si ? H H1);autobatch
1170   (*[ exact H3
1171   | apply le_S_S_to_le.
1172     assumption
1173   ]*)
1174 | intros.
1175   apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n))
1176   [ apply H2
1177     [ autobatch
1178       (*unfold lt.
1179       apply le_n*)
1180     | assumption
1181     | apply (trans_le ? (S(S (m1+i))))
1182       [ autobatch
1183         (*apply le_S.
1184         apply le_n*)
1185       | (*qui autobatch non chiude il goal, chiuso invece da assumption*)
1186         assumption
1187       ]
1188     ]
1189   | apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
1190     (transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n))
1191     [ (*qui autobatch dopo alcuni minuti non aveva ancora terminato la propria esecuzione*)
1192       apply (H2 O ? ? (S(m1+i)))
1193       [ autobatch
1194         (*unfold lt.
1195         apply le_S_S.
1196         apply le_O_n*)
1197       | autobatch
1198         (*apply (trans_le ? i)
1199         [ assumption
1200         | change with (i \le (S m1)+i).
1201           apply le_plus_n
1202         ]*)
1203       | (*qui autobatch non chiude il goal*)
1204         exact H4
1205       ]
1206     | apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
1207        (transpose i (S(m1 + i))
1208        (transpose (S(m1 + i)) (S(S(m1 + i)))
1209        (transpose i (S(m1 + i)) m)))) f n))
1210       [ (*qui autobatch dopo alcuni minuti non aveva ancora terminato la propria esecuzione*)
1211         apply (H2 m1)
1212         [ autobatch
1213           (*unfold lt.
1214           apply le_n*)
1215         | assumption
1216         | apply (trans_le ? (S(S (m1+i))))
1217           [ autobatch
1218             (*apply le_S.
1219             apply le_n*)
1220           | (*qui autobatch NON CHIUDE il goal*)
1221             assumption
1222           ]
1223         ]
1224       | apply eq_map_iter_i.
1225         intros.
1226         apply eq_f.
1227         apply sym_eq.
1228         apply eq_transpose
1229         [ unfold Not.
1230           intro.
1231           apply (not_le_Sn_n i).
1232           rewrite < H7 in \vdash (? ? %).
1233           autobatch
1234           (*apply le_S_S.
1235           apply le_S.
1236           apply le_plus_n*)
1237         | unfold Not.
1238           intro.
1239           apply (not_le_Sn_n i).
1240           rewrite > H7 in \vdash (? ? %).
1241           autobatch
1242           (*apply le_S_S.
1243           apply le_plus_n*)
1244         | unfold Not.
1245           intro.
1246           autobatch
1247           (*apply (not_eq_n_Sn (S m1+i)).
1248           apply sym_eq.
1249           assumption*)
1250         ]
1251       ]
1252     ]
1253   ]
1254 ]
1255 qed.
1256
1257 theorem eq_map_iter_i_transpose1: \forall f:nat\to nat \to nat.associative nat f \to
1258 symmetric2 nat nat f \to \forall n,k,i,j:nat.
1259 \forall g:nat \to nat. n \le i \to i < j \to j \le S k+n \to
1260 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
1261 intros.
1262 simplify in H3.
1263 cut ((S i) < j \lor (S i) = j)
1264 [ elim Hcut
1265   [ cut (j = S ((j - (S i)) + i))
1266     [ rewrite > Hcut1.
1267       apply (eq_map_iter_i_transpose f H H1 n k (j - (S i)) g i)
1268       [ assumption
1269       | rewrite < Hcut1.
1270         assumption
1271       ]
1272     | rewrite > plus_n_Sm.
1273       autobatch
1274       (*apply plus_minus_m_m.
1275       apply lt_to_le.
1276       assumption*)
1277     ]
1278   | rewrite < H5.
1279     apply (eq_map_iter_i_transpose_i_Si f H H1 g)
1280     [ autobatch
1281       (*simplify.
1282       assumption*)
1283     | apply le_S_S_to_le.
1284       autobatch
1285       (*apply (trans_le ? j)
1286       [ assumption
1287       | assumption
1288       ]*)
1289     ]
1290   ]
1291 | autobatch
1292   (*apply le_to_or_lt_eq.
1293   assumption*)
1294 ]
1295 qed.
1296
1297 theorem eq_map_iter_i_transpose2: \forall f:nat\to nat \to nat.associative nat f \to
1298 symmetric2 nat nat f \to \forall n,k,i,j:nat.
1299 \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
1300 map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
1301 intros.
1302 apply (nat_compare_elim i j)
1303 [ intro.
1304   (*qui autobatch non chiude il goal*)
1305   apply (eq_map_iter_i_transpose1 f H H1 n k i j g H2 H6 H5)
1306 | intro.
1307   rewrite > H6.
1308   apply eq_map_iter_i.
1309   intros.
1310   autobatch
1311   (*rewrite > (transpose_i_i j).
1312   reflexivity*)
1313 | intro.
1314   apply (trans_eq ? ? (map_iter_i (S k) (\lambda m:nat.g (transpose j i m)) f n))
1315   [ apply (eq_map_iter_i_transpose1 f H H1 n k j i g H4 H6 H3)
1316   | apply eq_map_iter_i.
1317     intros.
1318     autobatch
1319     (*apply eq_f.
1320     apply transpose_i_j_j_i*)
1321   ]
1322 ]
1323 qed.
1324
1325 theorem permut_to_eq_map_iter_i:\forall f:nat\to nat \to nat.associative nat f \to
1326 symmetric2 nat nat f \to \forall k,n:nat.\forall g,h:nat \to nat.
1327 permut h (k+n) \to (\forall m:nat. m \lt n \to h m = m) \to
1328 map_iter_i k g f n = map_iter_i k (\lambda m.g(h m)) f n.
1329 intros 4.
1330 elim k
1331 [ simplify.
1332   rewrite > (permut_n_to_eq_n h)
1333   [ reflexivity
1334   | (*qui autobatch non chiude il goal*)
1335     assumption
1336   | (*qui autobatch non chiude il goal*)
1337     assumption
1338   ]
1339 | apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.g ((transpose (h (S n+n1)) (S n+n1)) m)) f n1))
1340   [ unfold permut in H3.
1341     elim H3.
1342     apply (eq_map_iter_i_transpose2 f H H1 n1 n ? ? g)
1343     [ apply (permut_n_to_le h n1 (S n+n1))
1344       [ apply le_plus_n
1345       | (*qui autobatch non chiude il goal*)
1346         assumption
1347       | (*qui autobatch non chiude il goal*)
1348         assumption
1349       | apply le_plus_n
1350       | apply le_n
1351       ]
1352     | autobatch
1353       (*apply H5.
1354       apply le_n*)
1355     | apply le_plus_n
1356     | apply le_n
1357     ]
1358   | apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.
1359      (g(transpose (h (S n+n1)) (S n+n1)
1360      (transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1))
1361     [ simplify.
1362       fold simplify (transpose (h (S n+n1)) (S n+n1) (S n+n1)).
1363       apply eq_f2
1364       [ autobatch
1365         (*apply eq_f.
1366         rewrite > transpose_i_j_j.
1367         rewrite > transpose_i_j_i.
1368         rewrite > transpose_i_j_j.
1369         reflexivity.*)
1370       | apply (H2 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m))))
1371         [ apply permut_S_to_permut_transpose.
1372           (*qui autobatch non chiude il goal*)
1373           assumption
1374         | intros.
1375           unfold transpose.
1376           rewrite > (not_eq_to_eqb_false (h m) (h (S n+n1)))
1377           [ rewrite > (not_eq_to_eqb_false (h m) (S n+n1))
1378             [ simplify.
1379               autobatch
1380               (*apply H4.
1381               assumption*)
1382             | rewrite > H4
1383               [ autobatch
1384                 (*apply lt_to_not_eq.
1385                 apply (trans_lt ? n1)
1386                 [ assumption
1387                 | simplify.
1388                   unfold lt.
1389                   apply le_S_S.
1390                   apply le_plus_n
1391                 ]*)
1392               | assumption
1393               ]
1394             ]
1395           | unfold permut in H3.
1396             elim H3.
1397             simplify.
1398             unfold Not.
1399             intro.
1400             apply (lt_to_not_eq m (S n+n1))
1401             [ autobatch
1402               (*apply (trans_lt ? n1)
1403               [ assumption
1404               | simplify.
1405                 unfold lt.
1406                 apply le_S_S.
1407                 apply le_plus_n
1408               ]*)
1409             | unfold injn in H7.
1410               apply (H7 m (S n+n1))
1411               [ autobatch
1412                 (*apply (trans_le ? n1)
1413                 [ apply lt_to_le.
1414                   assumption
1415                 | apply le_plus_n
1416                 ]*)
1417               | apply le_n
1418               | assumption
1419               ]
1420             ]
1421           ]
1422         ]
1423       ]
1424     | apply eq_map_iter_i.
1425       intros.
1426       autobatch
1427       (*rewrite > transpose_transpose.
1428       reflexivity*)
1429     ]
1430   ]
1431 ]
1432 qed.