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