matita/library_auto/auto/nat/map_iter_p.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_auto/nat/map_iter_p.ma".
  16
  17 include "auto/nat/permutation.ma".
  18 include "auto/nat/count.ma".
  19
  20 let rec map_iter_p n p (g:nat \to nat) (a:nat) f \def
  21   match n with
  22    [ O \Rightarrow a
  23    | (S k) \Rightarrow
  24       match p (S k) with
  25       [true \Rightarrow f (g (S k)) (map_iter_p k p g a f)
  26       |false \Rightarrow map_iter_p k p g a f]
  27    ].
  28
  29 theorem eq_map_iter_p: \forall g1,g2:nat \to nat.
  30 \forall p:nat \to bool.
  31 \forall f:nat \to nat \to nat. \forall a,n:nat.
  32 (\forall m:nat. m \le n \to g1 m = g2 m) \to
  33 map_iter_p n p g1 a f = map_iter_p n p g2 a f.
  34 intros 6.
  35 elim n
  36 [ auto
  37   (*simplify.
  38   reflexivity*)
  39 | simplify.
  40   elim (p (S n1))
  41   [ simplify.
  42     apply eq_f2
  43     [ auto
  44       (*apply H1.
  45       apply le_n*)
  46     | simplify.
  47       apply H.
  48       intros.
  49       auto
  50       (*apply H1.
  51       apply le_S.
  52       assumption*)
  53     ]
  54   | simplify.
  55     apply H.
  56     intros.
  57     auto
  58     (*apply H1.
  59     apply le_S.
  60     assumption*)
  61   ]
  62 ]
  63 qed.
  64
  65 (* useful since simplify simpifies too much *)
  66
  67 theorem map_iter_p_O: \forall p.\forall g.\forall f. \forall a:nat.
  68 map_iter_p O p g a f = a.
  69 intros.
  70 auto.
  71 (*simplify.reflexivity.*)
  72 qed.
  73
  74 theorem map_iter_p_S_true: \forall p.\forall g.\forall f. \forall a,n:nat.
  75 p (S n) = true \to
  76 map_iter_p (S n) p g a f = f (g (S n)) (map_iter_p n p g a f).
  77 intros.simplify.rewrite > H.reflexivity.
  78 qed.
  79
  80 theorem map_iter_p_S_false: \forall p.\forall g.\forall f. \forall a,n:nat.
  81 p (S n) = false \to
  82 map_iter_p (S n) p g a f = map_iter_p n p g a f.
  83 intros.simplify.rewrite > H.reflexivity.
  84 qed.
  85
  86 (* map_iter examples *)
  87 definition pi_p \def \lambda p. \lambda n.
  88 map_iter_p n p (\lambda n.n) (S O) times.
  89
  90 lemma pi_p_S: \forall n.\forall p.
  91 pi_p p (S n) =
  92   match p (S n) with
  93     [true \Rightarrow (S n)*(pi_p p n)
  94     |false \Rightarrow (pi_p p n)
  95     ].
  96 intros.reflexivity.
  97 qed.
  98
  99 lemma lt_O_pi_p: \forall n.\forall p.
 100 O < pi_p p n.
 101 intros.
 102 elim n
 103 [ auto
 104   (*simplify.
 105   apply le_n*)
 106 | rewrite > pi_p_S.
 107   elim p (S n1)
 108   [ change with (O < (S n1)*(pi_p p n1)).
 109     auto
 110     (*rewrite >(times_n_O n1).
 111     apply lt_times
 112     [ apply le_n
 113     | assumption
 114     ]*)
 115   | assumption
 116   ]
 117 ]
 118 qed.
 119
 120 let rec card n p \def
 121   match n with
 122   [O \Rightarrow O
 123   |(S m) \Rightarrow
 124       (bool_to_nat (p (S m))) + (card m p)].
 125
 126 lemma count_card: \forall p.\forall n.
 127 p O = false \to count (S n) p = card n p.
 128 intros.
 129 elim n
 130 [ simplify.
 131   auto
 132   (*rewrite > H.
 133   reflexivity*)
 134 | simplify.
 135   rewrite < plus_n_O.
 136   apply eq_f.
 137   (*qui auto non chiude un goal chiuso invece dal solo assumption*)
 138   assumption
 139 ]
 140 qed.
 141
 142 lemma count_card1: \forall p.\forall n.
 143 p O = false \to p n = false \to count n p = card n p.
 144 intros 3.
 145 apply (nat_case n)
 146 [ intro.
 147   simplify.
 148   auto
 149   (*rewrite > H.
 150   reflexivity*)
 151 | intros.rewrite > (count_card ? ? H).
 152   simplify.
 153   auto
 154   (*rewrite > H1.
 155   reflexivity*)
 156 ]
 157 qed.
 158
 159 lemma a_times_pi_p: \forall p. \forall a,n.
 160 exp a (card n p) * pi_p p n = map_iter_p n p (\lambda n.a*n) (S O) times.
 161 intros.
 162 elim n
 163 [ auto
 164   (*simplify.
 165   reflexivity*)
 166 | simplify.
 167   apply (bool_elim ? (p (S n1)))
 168   [ intro.
 169     change with
 170       (a*exp a (card n1 p) * ((S n1) * (pi_p p n1)) =
 171        a*(S n1)*map_iter_p n1 p (\lambda n.a*n) (S O) times).
 172     rewrite < H.
 173     auto
 174   | intro.
 175     (*la chiamata di auto in questo punto dopo circa 8 minuti non aveva
 176      * ancora generato un risultato
 177      *)
 178     assumption
 179   ]
 180 ]
 181 qed.
 182
 183 definition permut_p \def \lambda f. \lambda p:nat\to bool. \lambda n.
 184 \forall i. i \le n \to p i = true \to ((f i \le n \land p (f i) = true)
 185 \land (\forall j. p j = true \to j \le n \to i \neq j \to (f i \neq f j))).
 186
 187 definition extentional_eq_n \def \lambda f,g:nat \to nat.\lambda n.
 188 \forall x. x \le n \to f x = g x.
 189
 190 lemma extentional_eq_n_to_permut_p: \forall f,g. \forall p. \forall n.
 191 extentional_eq_n f g n\to permut_p f p n \to permut_p g p n.
 192 intros.
 193 unfold permut_p.
 194 intros.
 195 elim (H1 i H2 H3).
 196 split
 197 [ elim H4.
 198   split
 199   [ rewrite < (H  i H2).
 200     assumption
 201   | rewrite < (H  i H2).
 202     assumption
 203   ]
 204 | intros.
 205   unfold.
 206   intro.
 207   apply (H5 j H6 H7 H8).
 208   rewrite > (H  i H2).
 209   rewrite > (H  j H7).
 210   assumption
 211 ]
 212 qed.
 213
 214 theorem permut_p_compose: \forall f,g.\forall p.\forall n.
 215 permut_p f p n \to permut_p g p n \to permut_p (compose  ? ? ? g f) p n.
 216 intros.
 217 unfold permut_p.
 218 intros.
 219 elim (H i H2 H3).
 220 elim H4.
 221 elim (H1 (f i) H6 H7).
 222 elim H8.
 223 split
 224 [ split
 225   [ unfold compose.
 226     assumption
 227   | unfold compose.
 228     auto
 229     (*rewrite < H11.
 230     reflexivity*)
 231   ]
 232 | intros.
 233   unfold compose.
 234   apply (H9 (f j))
 235   [ elim (H j H13 H12).
 236     auto
 237     (*elim H15.
 238     rewrite < H18.
 239     reflexivity*)
 240   | elim (H j H13 H12).
 241     elim H15.
 242     assumption.
 243   | apply (H5 j H12 H13 H14)
 244   ]
 245 ]
 246 qed.
 247
 248
 249 theorem permut_p_S_to_permut_p: \forall f.\forall p.\forall n.
 250 permut_p f p (S n) \to (f (S n)) = (S n) \to permut_p f p n.
 251 intros.
 252 unfold permut_p.
 253 intros.
 254 split
 255 [ elim (H i (le_S i n H2) H3).
 256   split
 257   [ elim H4.
 258     elim (le_to_or_lt_eq (f i) (S n))
 259     [ auto
 260       (*apply le_S_S_to_le.
 261       assumption*)
 262     | absurd (f i = (S n))
 263       [ assumption
 264       | rewrite < H1.
 265         apply H5
 266         [ auto
 267           (*rewrite < H8.
 268           assumption*)
 269         | apply le_n
 270         | unfold.intro.rewrite > H8 in H2.
 271           apply (not_le_Sn_n n).rewrite < H9.
 272           assumption
 273         ]
 274       ]
 275     | assumption
 276     ]
 277   | auto
 278     (*elim H4.
 279     assumption*)
 280   ]
 281 | intros.
 282   elim (H i (le_S i n H2) H3).
 283   auto
 284   (*apply H8
 285   [ assumption
 286   | apply le_S.
 287     assumption
 288   | assumption
 289   ]*)
 290 ]
 291 qed.
 292
 293 lemma permut_p_transpose: \forall p.\forall i,j,n.
 294 i \le n \to j \le n \to p i = p j \to
 295 permut_p (transpose i j) p n.
 296 unfold permut_p.
 297 intros.
 298 split
 299 [ split
 300   [ unfold transpose.
 301     apply (eqb_elim i1 i)
 302     [ intro.
 303       apply (eqb_elim i1 j)
 304       [ simplify.intro.assumption
 305       | simplify.intro.assumption
 306       ]
 307     | intro.
 308       apply (eqb_elim i1 j)
 309       [ simplify.intro.assumption
 310       | simplify.intro.assumption
 311       ]
 312     ]
 313   | unfold transpose.
 314     apply (eqb_elim i1 i)
 315     [ intro.
 316       apply (eqb_elim i1 j)
 317       [ simplify.intro.
 318         auto
 319         (*rewrite < H6.
 320         assumption*)
 321       | simplify.intro.
 322         auto
 323         (*rewrite < H2.
 324         rewrite < H5.
 325         assumption*)
 326       ]
 327     | intro.
 328       apply (eqb_elim i1 j)
 329       [ simplify.intro.
 330         auto
 331         (*rewrite > H2.
 332         rewrite < H6.
 333         assumption*)
 334       | simplify.intro.
 335         assumption
 336       ]
 337     ]
 338   ]
 339 | intros.
 340   unfold Not.
 341   intro.
 342   auto
 343   (*apply H7.
 344   apply (injective_transpose ? ? ? ? H8)*)
 345 ]
 346 qed.
 347
 348
 349 theorem eq_map_iter_p_k: \forall f,g.\forall p.\forall a,k,n:nat.
 350 p (S n-k) = true \to (\forall i. (S n)-k < i \to i \le (S n) \to (p i) = false) \to
 351 map_iter_p (S n) p g a f = map_iter_p (S n-k) p g a f.
 352 intros 5.
 353 elim k 3
 354 [ auto
 355   (*rewrite < minus_n_O.
 356   reflexivity*)
 357 | apply (nat_case n1)
 358   [ intros.
 359     rewrite > map_iter_p_S_false
 360     [ reflexivity
 361     | auto
 362       (*apply H2
 363       [ simplify.
 364         apply lt_O_S.
 365       | apply le_n
 366       ]*)
 367     ]
 368   | intros.
 369     rewrite > map_iter_p_S_false
 370     [ rewrite > (H m H1)
 371       [ reflexivity
 372       | intros.
 373         apply (H2 i H3).
 374         auto
 375         (*apply le_S.
 376         assumption*)
 377       ]
 378     | auto
 379       (*apply H2
 380       [ auto
 381       | apply le_n
 382       ]*)
 383     ]
 384   ]
 385 ]
 386 qed.
 387
 388
 389
 390 theorem eq_map_iter_p_a: \forall p.\forall f.\forall g. \forall a,n:nat.
 391 (\forall i.i \le n \to p i = false) \to map_iter_p n p g a f = a.
 392 intros 5.
 393 elim n
 394 [ auto
 395   (*simplify.
 396   reflexivity*)
 397 | rewrite > map_iter_p_S_false
 398   [ apply H.
 399     intros.
 400     auto
 401     (*apply H1.
 402     apply le_S.
 403     assumption*)
 404   | auto
 405     (*apply H1.
 406     apply le_n*)
 407   ]
 408 ]
 409 qed.
 410
 411 theorem eq_map_iter_p_transpose: \forall p.\forall f.associative nat f \to
 412 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. k < n \to
 413 (p (S n) = true) \to (p (n-k)) = true \to (\forall i. n-k < i \to i \le n \to (p i) = false)
 414 \to map_iter_p (S n) p g a f = map_iter_p (S n) p (\lambda m. g (transpose (n-k) (S n) m)) a f.
 415 intros 8.
 416 apply (nat_case n)
 417 [ intro.
 418   absurd (k < O)
 419   [ assumption
 420   | auto
 421     (*apply le_to_not_lt.
 422     apply le_O_n*)
 423   ]
 424 | intros.
 425   rewrite > (map_iter_p_S_true ? ? ? ? ? H3).
 426   rewrite > (map_iter_p_S_true ? ? ? ? ? H3).
 427   rewrite > (eq_map_iter_p_k ? ? ? ? ? ? H4 H5).
 428   rewrite > (eq_map_iter_p_k ? ? ? ? ? ? H4 H5).
 429   generalize in match H4.
 430   rewrite > minus_Sn_m
 431   [ intro.
 432     rewrite > (map_iter_p_S_true ? ? ? ? ? H6).
 433     rewrite > (map_iter_p_S_true ? ? ? ? ? H6).
 434     rewrite > transpose_i_j_j.
 435     rewrite > transpose_i_j_i.
 436     cut (map_iter_p (m-k) p g a f =
 437       map_iter_p (m-k) p (\lambda x.g (transpose (S(m-k)) (S(S m)) x)) a f)
 438     [ rewrite < Hcut.
 439       rewrite < H.
 440       rewrite < H1 in \vdash (? ? (? % ?) ?).
 441       auto
 442       (*rewrite > H.
 443       reflexivity*)
 444     | apply eq_map_iter_p.
 445       intros.
 446       unfold transpose.
 447       cut (eqb m1 (S (m-k)) =false)
 448       [ cut (eqb m1 (S (S m)) =false)
 449         [ rewrite > Hcut.
 450           rewrite > Hcut1.
 451           reflexivity
 452         | apply not_eq_to_eqb_false.
 453           apply lt_to_not_eq.
 454           apply (le_to_lt_to_lt ? m)
 455           [ auto
 456             (*apply (trans_le ? (m-k))
 457             [ assumption
 458             | auto
 459             ]*)
 460           | auto
 461             (*apply le_S.
 462             apply le_n*)
 463           ]
 464         ]
 465       | apply not_eq_to_eqb_false.
 466         apply lt_to_not_eq.
 467         auto
 468         (*unfold.
 469         auto*)
 470       ]
 471     ]
 472   | auto
 473     (*apply le_S_S_to_le.
 474     assumption*)
 475   ]
 476 ]
 477 qed.
 478
 479 theorem eq_map_iter_p_transpose1: \forall p.\forall f.associative nat f \to
 480 symmetric2 nat nat f \to \forall g. \forall a,k1,k2,n:nat. O < k1 \to k1 < k2 \to k2 \le n \to
 481 (p k1) = true \to (p k2) = true \to (\forall i. k1 < i \to i < k2 \to (p i) = false)
 482 \to map_iter_p n p g a f = map_iter_p n p (\lambda m. g (transpose k1 k2 m)) a f.
 483 intros 10.
 484 elim n 2
 485 [ absurd (k2 \le O)
 486   [ assumption
 487   | auto
 488     (*apply lt_to_not_le.
 489     apply (trans_lt ? k1 ? H2 H3)*)
 490   ]
 491 | apply (eqb_elim (S n1) k2)
 492   [ intro.
 493     rewrite < H4.
 494     intros.
 495     cut (k1 = n1 - (n1 -k1))
 496     [ rewrite > Hcut.
 497       apply (eq_map_iter_p_transpose p f H H1 g a (n1-k1))
 498       [ cut (k1 \le n1);auto
 499       | assumption
 500       | auto
 501         (*rewrite < Hcut.
 502         assumption*)
 503       | rewrite < Hcut.
 504         intros.
 505         apply (H9 i H10).
 506         auto
 507         (*unfold.
 508         auto*)
 509       ]
 510     | apply sym_eq.
 511       auto
 512       (*apply plus_to_minus.
 513       auto*)
 514     ]
 515   | intros.
 516     cut ((S n1) \neq k1)
 517     [ apply (bool_elim ? (p (S n1)))
 518       [ intro.
 519         rewrite > map_iter_p_S_true
 520         [ rewrite > map_iter_p_S_true
 521           [ cut ((transpose k1 k2 (S n1)) = (S n1))
 522             [ rewrite > Hcut1.
 523               apply eq_f.
 524               apply (H3 H5)
 525               [ elim (le_to_or_lt_eq ? ? H6)
 526                 [ auto
 527                 | absurd (S n1=k2)
 528                   [ auto
 529                     (*apply sym_eq.
 530                     assumption*)
 531                   | assumption
 532                   ]
 533                 ]
 534               | assumption
 535               | assumption
 536               | assumption
 537               ]
 538             | unfold transpose.
 539               rewrite > (not_eq_to_eqb_false ? ? Hcut).
 540               rewrite > (not_eq_to_eqb_false ? ? H4).
 541               reflexivity
 542             ]
 543           | assumption
 544           ]
 545         | assumption
 546         ]
 547       | intro.
 548         rewrite > map_iter_p_S_false
 549         [ rewrite > map_iter_p_S_false
 550           [ apply (H3 H5)
 551             [ elim (le_to_or_lt_eq ? ? H6)
 552               [ auto
 553               | (*l'invocazione di auto qui genera segmentation fault*)
 554                 absurd (S n1=k2)
 555                 [ auto
 556                   (*apply sym_eq.
 557                   assumption*)
 558                 | assumption
 559                 ]
 560               ]
 561             | assumption
 562             | assumption
 563             | assumption
 564             ]
 565           | assumption
 566           ]
 567         | assumption
 568         ]
 569       ]
 570     | unfold.
 571       intro.
 572       absurd (k1 < k2)
 573       [ assumption
 574       | apply le_to_not_lt.
 575         rewrite < H10.
 576         assumption
 577       ]
 578     ]
 579   ]
 580 ]
 581 qed.
 582
 583 lemma decidable_n:\forall p.\forall n.
 584 (\forall m. m \le n \to (p m) = false) \lor
 585 (\exists m. m \le n \land (p m) = true \land
 586 \forall i. m < i \to i \le n \to (p i) = false).
 587 intros.
 588 elim n
 589 [ apply (bool_elim ? (p O))
 590   [ intro.
 591     right.
 592     apply (ex_intro ? ? O).
 593     split
 594     [ auto
 595       (*split
 596       [ apply le_n
 597       | assumption
 598       ]*)
 599     | intros.
 600       absurd (O<i)
 601       [ assumption
 602       | auto
 603         (*apply le_to_not_lt.
 604         assumption*)
 605       ]
 606     ]
 607   | intro.
 608     left.
 609     intros.
 610     apply (le_n_O_elim m H1).
 611     assumption
 612   ]
 613 | apply (bool_elim ? (p (S n1)))
 614   [ intro.
 615     right.
 616     apply (ex_intro ? ? (S n1)).
 617     split
 618     [ split
 619       [ apply le_n
 620       | assumption
 621       ]
 622     | intros.
 623       absurd (S n1<i)
 624       [ assumption
 625       | auto
 626         (*apply le_to_not_lt.
 627         assumption*)
 628       ]
 629     ]
 630   | elim H
 631     [ left.
 632       intros.
 633       elim (le_to_or_lt_eq m (S n1) H3)
 634       [ auto
 635         (*apply H1.
 636         apply le_S_S_to_le.
 637         assumption*)
 638       | auto
 639         (*rewrite > H4.
 640         assumption*)
 641       ]
 642     | right.
 643       elim H1.
 644       elim H3.
 645       elim H4.
 646       apply (ex_intro ? ? a).
 647       split
 648       [ auto
 649         (*split
 650         [ apply le_S.
 651           assumption
 652         | assumption
 653         ]*)
 654       | intros.
 655         elim (le_to_or_lt_eq i (S n1) H9)
 656         [ auto
 657           (*apply H5
 658           [ assumption
 659           | apply le_S_S_to_le.
 660             assumption
 661           ]*)
 662         | auto
 663           (*rewrite > H10.
 664           assumption*)
 665         ]
 666       ]
 667     ]
 668   ]
 669 ]
 670 qed.
 671
 672 lemma decidable_n1:\forall p.\forall n,j. j \le n \to (p j)=true \to
 673 (\forall m. j < m \to m \le n \to (p m) = false) \lor
 674 (\exists m. j < m \land m \le n \land (p m) = true \land
 675 \forall i. m < i \to i \le n \to (p i) = false).
 676 intros.
 677 elim (decidable_n p n)
 678 [ absurd ((p j)=true)
 679   [ assumption
 680   | unfold.
 681     intro.
 682     apply not_eq_true_false.
 683     auto
 684     (*rewrite < H3.
 685     apply H2.
 686     assumption*)
 687   ]
 688 | elim H2.
 689   clear H2.
 690   apply (nat_compare_elim j a)
 691   [ intro.
 692     right.
 693     apply (ex_intro ? ? a).
 694     elim H3.clear H3.
 695     elim H4.clear H4.
 696     split
 697     [ auto
 698       (*split
 699       [ split
 700         [ assumption
 701         | assumption
 702         ]
 703       | assumption
 704       ]*)
 705     | assumption
 706     ]
 707   | intro.
 708     rewrite > H2.
 709     left.
 710     elim H3 2.
 711     (*qui la tattica auto non conclude il goal, concluso invece con l'invocazione
 712      *della sola tattica assumption
 713      *)
 714     assumption
 715   | intro.
 716     absurd (p j = true)
 717     [ assumption
 718     | unfold.
 719       intro.
 720       apply not_eq_true_false.
 721       rewrite < H4.
 722       elim H3.
 723       auto
 724       (*clear H3.
 725       apply (H6 j H2).assumption*)
 726     ]
 727   ]
 728 ]
 729 qed.
 730
 731 lemma decidable_n2:\forall p.\forall n,j. j \le n \to (p j)=true \to
 732 (\forall m. j < m \to m \le n \to (p m) = false) \lor
 733 (\exists m. j < m \land m \le n \land (p m) = true \land
 734 \forall i. j < i \to i < m \to (p i) = false).
 735 intros 3.
 736 elim n
 737 [ left.
 738   apply (le_n_O_elim j H).
 739   intros.
 740   absurd (m \le O)
 741   [ assumption
 742   | auto
 743     (*apply lt_to_not_le.
 744     assumption*)
 745   ]
 746 | elim (le_to_or_lt_eq ? ? H1)
 747   [ cut (j \le n1)
 748     [ elim (H Hcut H2)
 749       [ apply (bool_elim ? (p (S n1)))
 750         [ intro.
 751           right.
 752           apply (ex_intro ? ? (S n1)).
 753           split
 754           [ auto
 755             (*split
 756             [ split
 757               [ assumption
 758               | apply le_n
 759               ]
 760             | assumption
 761             ]*)
 762           | intros.
 763             auto
 764             (*apply (H4 i H6).
 765             apply le_S_S_to_le.
 766             assumption*)
 767           ]
 768         | intro.
 769           left.
 770           intros.
 771           elim (le_to_or_lt_eq ? ? H7)
 772           [ auto
 773             (*apply H4
 774             [ assumption
 775             | apply le_S_S_to_le.
 776               assumption
 777             ]*)
 778           | auto
 779             (*rewrite > H8.
 780             assumption*)
 781           ]
 782         ]
 783       | right.
 784         elim H4.clear H4.
 785         elim H5.clear H5.
 786         elim H4.clear H4.
 787         elim H5.clear H5.
 788         apply (ex_intro ? ? a).
 789         split
 790         [ split
 791           [ auto
 792             (*split
 793             [ assumption
 794             | apply le_S.
 795               assumption
 796             ]*)
 797           | assumption
 798           ]
 799         | (*qui auto non chiude il goal, chiuso invece mediante l'invocazione
 800            *della sola tattica assumption
 801            *)
 802           assumption
 803         ]
 804       ]
 805     | auto
 806       (*apply le_S_S_to_le.
 807       assumption*)
 808     ]
 809   | left.
 810     intros.
 811     absurd (j < m)
 812     [ assumption
 813     | apply le_to_not_lt.
 814       rewrite > H3.
 815       assumption
 816     ]
 817   ]
 818 ]
 819 qed.
 820
 821 (* tutti d spostare *)
 822 theorem lt_minus_to_lt_plus:
 823 \forall n,m,p. n - m < p \to n < m + p.
 824 intros 2.
 825 apply (nat_elim2 ? ? ? ? n m)
 826 [ simplify.
 827   intros.
 828   auto
 829 | intros 2.
 830   auto
 831   (*rewrite < minus_n_O.
 832   intro.
 833   assumption*)
 834 | intros.
 835   simplify.
 836   cut (n1 < m1+p)
 837   [ auto
 838   | apply H.
 839     apply H1
 840   ]
 841 ]
 842 qed.
 843
 844 theorem lt_plus_to_lt_minus:
 845 \forall n,m,p. m \le n \to n < m + p \to n - m < p.
 846 intros 2.
 847 apply (nat_elim2 ? ? ? ? n m)
 848 [ simplify.
 849   intros 3.
 850   apply (le_n_O_elim ? H).
 851   auto
 852   (*simplify.
 853   intros.
 854   assumption*)
 855 | simplify.
 856   intros.
 857   assumption
 858 | intros.
 859   simplify.
 860   apply H
 861   [ auto
 862     (*apply le_S_S_to_le.
 863     assumption*)
 864   | apply le_S_S_to_le.
 865     apply H2
 866   ]
 867 ]
 868 qed.
 869
 870 theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n).
 871 intros.
 872 apply sym_eq.
 873 auto.
 874 (*apply plus_to_minus.
 875 auto.*)
 876 qed.
 877
 878 theorem eq_map_iter_p_transpose2: \forall p.\forall f.associative nat f \to
 879 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le n \to
 880 (p (S n) = true) \to (p k) = true
 881 \to map_iter_p (S n) p g a f = map_iter_p (S n) p (\lambda m. g (transpose k (S n) m)) a f.
 882 intros 10.
 883 cut (k = (S n)-(S n -k))
 884 [ generalize in match H3.
 885   clear H3.
 886   generalize in match g.
 887   generalize in match H2.
 888   clear H2.
 889   rewrite > Hcut.
 890    (*generalize in match Hcut.clear Hcut.*)
 891    (* generalize in match H3.clear H3.*)
 892    (* something wrong here
 893      rewrite > Hcut in \vdash (?\rarr ?\rarr %). *)
 894   apply (nat_elim1 (S n - k)).
 895   intros.
 896   elim (decidable_n2 p n (S n -m) H4 H6)
 897   [ apply (eq_map_iter_p_transpose1 p f H H1 f1 a)
 898     [ assumption
 899     | auto
 900       (*unfold.
 901       auto*)
 902     | apply le_n
 903     | assumption
 904     | assumption
 905     | intros.
 906       auto
 907       (*apply H7
 908       [ assumption
 909       | apply le_S_S_to_le.
 910         assumption
 911       ]*)
 912     ]
 913   | elim H7.
 914     clear H7.
 915     elim H8.clear H8.
 916     elim H7.clear H7.
 917     elim H8.clear H8.
 918     apply (trans_eq  ? ?
 919      (map_iter_p (S n) p (\lambda i.f1 (transpose a1 (S n) (transpose (S n -m) a1 i))) a f))
 920     [ apply (trans_eq  ? ?
 921        (map_iter_p (S n) p (\lambda i.f1 (transpose a1 (S n) i)) a f))
 922       [ cut (a1 = (S n -(S n -a1)))
 923         [ rewrite > Hcut1.
 924           apply H2
 925           [ apply lt_plus_to_lt_minus
 926             [ auto
 927               (*apply le_S.
 928               assumption*)
 929             | rewrite < sym_plus.
 930               auto
 931               (*apply lt_minus_to_lt_plus.
 932               assumption*)
 933             ]
 934           | rewrite < Hcut1.
 935             auto
 936             (*apply (trans_lt ? (S n -m));
 937                 assumption*)
 938           | rewrite < Hcut1.
 939             assumption
 940           | assumption
 941           | auto
 942             (*rewrite < Hcut1.
 943             assumption*)
 944           ]
 945         | auto
 946           (*apply minus_m_minus_mn.
 947           apply le_S.
 948           assumption*)
 949         ]
 950       | apply (eq_map_iter_p_transpose1 p f H H1)
 951         [ assumption
 952         | assumption
 953         | auto
 954           (*apply le_S.
 955           assumption*)
 956         | assumption
 957         | assumption
 958         | (*qui auto non chiude il goal, chiuso dall'invocazione della singola
 959            * tattica assumption
 960            *)
 961           assumption
 962         ]
 963       ]
 964     | apply (trans_eq  ? ?
 965        (map_iter_p (S n) p (\lambda i.f1 (transpose a1 (S n) (transpose (S n -m) a1 (transpose (S n -(S n -a1)) (S n) i)))) a f))
 966       [ cut (a1 = (S n) -(S n -a1))
 967         [ apply H2
 968           [ apply lt_plus_to_lt_minus
 969             [ auto
 970               (*apply le_S.
 971               assumption*)
 972             | rewrite < sym_plus.
 973               auto
 974               (*apply lt_minus_to_lt_plus.
 975               assumption*)
 976             ]
 977           | rewrite < Hcut1.
 978             auto
 979             (*apply (trans_lt ? (S n -m))
 980             [ assumption
 981             | assumption
 982             ]*)
 983           | rewrite < Hcut1.
 984             assumption
 985           | assumption
 986           | auto
 987             (*rewrite < Hcut1.
 988             assumption*)
 989           ]
 990         | auto
 991           (*apply minus_m_minus_mn.
 992           apply le_S.
 993           assumption*)
 994         ]
 995       | apply eq_map_iter_p.
 996         cut (a1 = (S n) -(S n -a1))
 997         [ intros.
 998           apply eq_f.
 999           rewrite < Hcut1.
1000           rewrite < transpose_i_j_j_i.
1001           rewrite > (transpose_i_j_j_i (S n -m)).
1002           rewrite > (transpose_i_j_j_i a1 (S n)).
1003           rewrite > (transpose_i_j_j_i (S n -m)).
1004           apply sym_eq.
1005           apply eq_transpose
1006           [ unfold.
1007             intro.
1008             apply (not_le_Sn_n n).
1009             rewrite < H12.
1010             assumption
1011           | unfold.
1012             intro.
1013             apply (not_le_Sn_n n).
1014             rewrite > H12.
1015             assumption
1016           | unfold.
1017             intro.
1018             apply (not_le_Sn_n a1).
1019             rewrite < H12 in \vdash (? (? %) ?).
1020             assumption
1021           ]
1022         | auto
1023           (*apply minus_m_minus_mn.
1024           apply le_S.
1025           assumption*)
1026         ]
1027       ]
1028     ]
1029   ]
1030 | auto
1031   (*apply minus_m_minus_mn.
1032   apply le_S.
1033   assumption*)
1034 ]
1035 qed.
1036
1037 theorem eq_map_iter_p_transpose3: \forall p.\forall f.associative nat f \to
1038 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le (S n) \to
1039 (p (S n) = true) \to (p k) = true
1040 \to map_iter_p (S n) p g a f = map_iter_p (S n) p (\lambda m. g (transpose k (S n) m)) a f.
1041 intros.
1042 elim (le_to_or_lt_eq ? ? H3)
1043 [ apply (eq_map_iter_p_transpose2 p f H H1 g a k n H2);auto
1044   (*[ apply le_S_S_to_le.
1045     assumption
1046   | assumption
1047   | assumption
1048   ]*)
1049 | rewrite > H6.
1050   apply eq_map_iter_p.
1051   intros.
1052   auto
1053   (*apply eq_f.
1054   apply sym_eq.
1055   apply transpose_i_i.*)
1056 ]
1057 qed.
1058
1059 lemma permut_p_O: \forall p.\forall h.\forall n.
1060 permut_p h p n \to p O = false \to \forall m. (S m) \le n \to p (S m) = true \to O < h(S m).
1061 intros.
1062 unfold permut_p in H.
1063 apply not_le_to_lt.unfold.
1064 intro.
1065 elim (H (S m) H2 H3).
1066 elim H5.
1067 absurd (p (h (S m)) = true)
1068 [ assumption
1069 | apply (le_n_O_elim ? H4).
1070   unfold.
1071   intro.
1072   (*l'invocazione di auto in questo punto genera segmentation fault*)
1073   apply not_eq_true_false.
1074   (*l'invocazione di auto in questo punto genera segmentation fault*)
1075   rewrite < H9.
1076   (*l'invocazione di auto in questo punto genera segmentation fault*)
1077   rewrite < H1.
1078   (*l'invocazione di auto in questo punto genera segmentation fault*)
1079   reflexivity
1080 ]
1081 qed.
1082
1083 theorem eq_map_iter_p_permut: \forall p.\forall f.associative nat f \to
1084 symmetric2 nat nat f \to \forall n.\forall g. \forall h.\forall a:nat.
1085 permut_p h p n \to p O = false \to
1086 map_iter_p n p g a f = map_iter_p n p (compose ? ? ? g h) a f .
1087 intros 5.
1088 elim n
1089 [ auto
1090   (*simplify.
1091   reflexivity*)
1092 | apply (bool_elim ? (p (S n1)))
1093   [ intro.
1094     apply (trans_eq ? ? (map_iter_p (S n1) p (\lambda m.g ((transpose (h (S n1)) (S n1)) m)) a f))
1095     [ unfold permut_p in H3.
1096       elim (H3 (S n1) (le_n ?) H5).
1097       elim H6.
1098       clear H6.
1099       apply (eq_map_iter_p_transpose3 p f H H1 g a (h(S n1)) n1)
1100       [ apply (permut_p_O ? ? ? H3 H4);auto
1101         (*[ apply le_n
1102         | assumption
1103         ]*)
1104       | assumption
1105       | assumption
1106       | assumption
1107       ]
1108     | apply (trans_eq ? ? (map_iter_p (S n1) p (\lambda m.
1109        (g(transpose (h (S n1)) (S n1)
1110        (transpose (h (S n1)) (S n1) (h m)))) ) a f))
1111       [ rewrite > (map_iter_p_S_true ? ? ? ? ? H5).
1112         rewrite > (map_iter_p_S_true ? ? ? ? ? H5).
1113         apply eq_f2
1114         [ rewrite > transpose_i_j_j.
1115           rewrite > transpose_i_j_i.
1116           rewrite > transpose_i_j_j.
1117           reflexivity
1118         | apply (H2 (\lambda m.(g(transpose (h (S n1)) (S n1) m))) ?)
1119           [ unfold.
1120             intros.
1121             split
1122             [ split
1123               [ simplify.
1124                 unfold permut_p in H3.
1125                 elim (H3 i (le_S ? ? H6) H7).
1126                 elim H8.
1127                 clear H8.
1128                 elim (le_to_or_lt_eq ? ? H10)
1129                 [ unfold transpose.
1130                   rewrite > (not_eq_to_eqb_false ? ? (lt_to_not_eq ? ? H8)).
1131                   cut (h i \neq h (S n1))
1132                   [ rewrite > (not_eq_to_eqb_false ? ? Hcut).
1133                     simplify.
1134                     auto
1135                     (*apply le_S_S_to_le.
1136                     assumption*)
1137                   | apply H9
1138                     [ apply H5
1139                     | apply le_n
1140                     | apply lt_to_not_eq.
1141                       auto
1142                       (*unfold.
1143                       apply le_S_S.
1144                       assumption*)
1145                     ]
1146                   ]
1147                 | rewrite > H8.
1148                   apply (eqb_elim (S n1) (h (S n1)))
1149                   [ intro.
1150                     absurd (h i = h (S n1))
1151                     [ auto
1152                       (*rewrite > H8.
1153                       assumption*)
1154                     | apply H9
1155                       [ assumption
1156                       | apply le_n
1157                       | apply lt_to_not_eq.
1158                         auto
1159                         (*unfold.
1160                         apply le_S_S.
1161                         assumption*)
1162                       ]
1163                     ]
1164                   | intro.
1165                     unfold transpose.
1166                     rewrite > (not_eq_to_eqb_false ? ? H12).
1167                     rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S n1))).
1168                     simplify.
1169                     elim (H3 (S n1) (le_n ? ) H5).
1170                     elim H13.clear H13.
1171                     elim (le_to_or_lt_eq ? ? H15)
1172                     [ auto
1173                       (*apply le_S_S_to_le.
1174                       assumption*)
1175                     | apply False_ind.
1176                       auto
1177                       (*apply H12.
1178                       apply sym_eq.
1179                       assumption*)
1180                     ]
1181                   ]
1182                 ]
1183
1184               | simplify.
1185                 unfold permut_p in H3.
1186                 unfold transpose.
1187                 apply (eqb_elim (h i) (S n1))
1188                 [ intro.
1189                   apply (eqb_elim (h i) (h (S n1)))
1190                   [ intro.
1191                     (*NB: qui auto non chiude il goal*)
1192                     simplify.
1193                     assumption
1194                   | intro.
1195                     simplify.
1196                     elim (H3 (S n1) (le_n ? ) H5).
1197                     auto
1198                     (*elim H10.
1199                     assumption*)
1200                   ]
1201                 | intro.
1202                   apply (eqb_elim (h i) (h (S n1)))
1203                   [ intro.
1204                   (*NB: qui auto non chiude il goal*)
1205                     simplify.
1206                     assumption
1207                   | intro.
1208                     simplify.
1209                     elim (H3 i (le_S ? ? H6) H7).
1210                     auto
1211                     (*elim H10.
1212                     assumption*)
1213                   ]
1214                 ]
1215               ]
1216             | simplify.
1217               intros.
1218               unfold Not.
1219               intro.
1220               unfold permut_p in H3.
1221               elim (H3 i (le_S i ? H6) H7).
1222               apply (H13 j H8 (le_S j ? H9) H10).
1223               apply (injective_transpose ? ? ? ? H11)
1224             ]
1225           | assumption
1226           ]
1227         ]
1228       | apply eq_map_iter_p.
1229         intros.
1230         auto
1231         (*rewrite > transpose_transpose.
1232         reflexivity*)
1233       ]
1234     ]
1235   | intro.
1236     rewrite > (map_iter_p_S_false ? ? ? ? ? H5).
1237     rewrite > (map_iter_p_S_false ? ? ? ? ? H5).
1238     apply H2
1239     [ unfold permut_p.
1240       unfold permut_p in H3.
1241       intros.
1242       elim (H3 i (le_S i ? H6) H7).
1243       elim H8.
1244       split
1245       [ split
1246         [ elim (le_to_or_lt_eq ? ? H10)
1247           [ auto
1248             (*apply le_S_S_to_le.assumption*)
1249           | absurd (p (h i) = true)
1250             [ assumption
1251             | rewrite > H12.
1252               rewrite > H5.
1253               unfold.intro.
1254               (*l'invocazione di auto qui genera segmentation fault*)
1255               apply not_eq_true_false.
1256               (*l'invocazione di auto qui genera segmentation fault*)
1257               apply sym_eq.
1258               (*l'invocazione di auto qui genera segmentation fault*)
1259               assumption
1260             ]
1261           ]
1262         | assumption
1263         ]
1264       | intros.
1265         apply H9;auto
1266         (*[ assumption
1267         | apply (le_S ? ? H13)
1268         | assumption
1269         ]*)
1270       ]
1271     | assumption
1272
1273     ]
1274
1275   ]
1276
1277 ]
1278 qed.
1279