matita/library/nat/iteration.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/iteration.ma".
  16
  17 include "nat/permutation.ma".
  18 include "nat/count.ma".
  19
  20 lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
  21 apply nat_elim2
  22   [intros.apply le_n_O_to_eq.assumption
  23   |intros.apply sym_eq.apply le_n_O_to_eq.assumption
  24   |intros.apply eq_f.apply H
  25     [apply le_S_S_to_le.assumption
  26     |apply le_S_S_to_le.assumption
  27     ]
  28   ]
  29 qed.
  30
  31 let rec map_iter_P n p (g:nat \to nat) (a:nat) f \def
  32   match n with
  33    [ O \Rightarrow a
  34    | (S k) \Rightarrow
  35       match p (S k) with
  36       [true \Rightarrow f (g (S k)) (map_iter_P k p g a f)
  37       |false \Rightarrow map_iter_P k p g a f]
  38    ].
  39
  40 theorem eq_map_iter_P: \forall g1,g2:nat \to nat.
  41 \forall p:nat \to bool.
  42 \forall f:nat \to nat \to nat. \forall a,n:nat.
  43 (\forall m:nat. m \le n \to g1 m = g2 m) \to
  44 map_iter_P n p g1 a f = map_iter_P n p g2 a f.
  45 intros 6.elim n
  46   [simplify.reflexivity.
  47   |simplify.elim (p (S n1))
  48     [simplify.apply eq_f2
  49       [apply H1.apply le_n
  50       |simplify.apply H.intros.apply H1.
  51        apply le_S.assumption
  52       ]
  53     |simplify.apply H.intros.apply H1.
  54      apply le_S.assumption
  55     ]
  56  ]
  57 qed.
  58
  59 (* useful since simply simpifies too much *)
  60
  61 theorem map_iter_P_O: \forall p.\forall g.\forall f. \forall a:nat.
  62 map_iter_P O p g a f = a.
  63 intros.simplify.reflexivity.
  64 qed.
  65
  66 theorem map_iter_P_S_true: \forall p.\forall g.\forall f. \forall a,n:nat.
  67 p (S n) = true \to
  68 map_iter_P (S n) p g a f = f (g (S n)) (map_iter_P n p g a f).
  69 intros.simplify.rewrite > H.reflexivity.
  70 qed.
  71
  72 theorem map_iter_P_S_false: \forall p.\forall g.\forall f. \forall a,n:nat.
  73 p (S n) = false \to
  74 map_iter_P (S n) p g a f = map_iter_P n p g a f.
  75 intros.simplify.rewrite > H.reflexivity.
  76 qed.
  77
  78 (* map_iter examples *)
  79 definition Pi_P \def \lambda p. \lambda n.
  80 map_iter_P n p (\lambda n.n) (S O) times.
  81
  82 lemma Pi_P_S: \forall n.\forall p.
  83 Pi_P p (S n) =
  84   match p (S n) with
  85     [true \Rightarrow (S n)*(Pi_P p n)
  86     |false \Rightarrow (Pi_P p n)
  87     ].
  88 intros.reflexivity.
  89 qed.
  90
  91 lemma lt_O_Pi_P: \forall n.\forall p.
  92 O < Pi_P p n.
  93 intros.elim n
  94   [simplify.apply le_n
  95   |rewrite > Pi_P_S.
  96    elim p (S n1)
  97     [change with (O < (S n1)*(Pi_P p n1)).
  98      rewrite >(times_n_O n1).
  99      apply lt_times[apply le_n|assumption]
 100     | assumption
 101     ]
 102   ]
 103 qed.
 104
 105 let rec card n p \def
 106   match n with
 107   [O \Rightarrow O
 108   |(S m) \Rightarrow
 109       (bool_to_nat (p (S m))) + (card m p)].
 110
 111 lemma a_times_Pi_P: \forall p. \forall a,n.
 112 exp a (card n p) * Pi_P p n = map_iter_P n p (\lambda n.a*n) (S O) times.
 113 intros.elim n
 114   [simplify.reflexivity
 115   |simplify.apply (bool_elim ? (p (S n1)))
 116     [intro.
 117      change with
 118       (a*exp a (card n1 p) * ((S n1) * (Pi_P p n1)) =
 119        a*(S n1)*map_iter_P n1 p (\lambda n.a*n) (S O) times).
 120        rewrite < H.
 121        auto
 122     |intro.assumption
 123     ]
 124   ]
 125 qed.
 126
 127 definition permut_p \def \lambda f. \lambda p:nat\to bool. \lambda n.
 128 \forall i. i \le n \to p i = true \to ((f i \le n \land p (f i) = true)
 129 \land (\forall j. p j = true \to j \le n \to i \neq j \to (f i \neq f j))).
 130
 131 definition extentional_eq_n \def \lambda f,g:nat \to nat.\lambda n.
 132 \forall x. x \le n \to f x = g x.
 133
 134 lemma extentional_eq_n_to_permut_p: \forall f,g. \forall p. \forall n.
 135 extentional_eq_n f g n\to permut_p f p n \to permut_p g p n.
 136 intros.unfold permut_p.
 137 intros.
 138 elim (H1 i H2 H3).
 139 split
 140   [elim H4.split
 141     [rewrite < (H  i H2).assumption
 142     |rewrite < (H  i H2).assumption
 143     ]
 144   |intros.
 145    unfold.intro.apply (H5 j H6 H7 H8).
 146      rewrite > (H  i H2).
 147      rewrite > (H  j H7).assumption
 148   ]
 149 qed.
 150
 151 theorem permut_p_compose: \forall f,g.\forall p.\forall n.
 152 permut_p f p n \to permut_p g p n \to permut_p (compose  ? ? ? g f) p n.
 153 intros.unfold permut_p.intros.
 154 elim (H i H2 H3).
 155 elim H4.
 156 elim (H1 (f i) H6 H7).
 157 elim H8.
 158 split
 159   [split
 160     [unfold compose.assumption
 161     |unfold compose.rewrite < H11.reflexivity
 162     ]
 163   |intros.
 164    unfold compose.
 165    apply (H9 (f j))
 166     [elim (H j H13 H12).elim H15.rewrite < H18.reflexivity
 167     |elim (H j H13 H12).elim H15.assumption.
 168     |apply (H5 j H12 H13 H14)
 169     ]
 170   ]
 171 qed.
 172
 173 theorem permut_p_S_to_permut_p: \forall f.\forall p.\forall n.
 174 permut_p f p (S n) \to (f (S n)) = (S n) \to permut_p f p n.
 175 intros.
 176 unfold permut_p.
 177 intros.
 178 split
 179   [elim (H i (le_S i n H2) H3).split
 180     [elim H4.
 181      elim (le_to_or_lt_eq (f i) (S n))
 182       [apply le_S_S_to_le.assumption
 183       |absurd (f i = (S n))
 184         [assumption
 185         |rewrite < H1.
 186          apply H5
 187           [rewrite < H8.assumption
 188           |apply le_n
 189           |unfold.intro.rewrite > H8 in H2.
 190            apply (not_le_Sn_n n).rewrite < H9.assumption
 191           ]
 192         ]
 193       |assumption
 194       ]
 195     |elim H4.assumption
 196     ]
 197   |intros.
 198    elim (H i (le_S i n H2) H3).
 199    apply H8
 200     [assumption|apply le_S.assumption|assumption]
 201   ]
 202 qed.
 203
 204 lemma permut_p_transpose: \forall p.\forall i,j,n.
 205 i \le n \to j \le n \to p i = p j \to
 206 permut_p (transpose i j) p n.
 207 unfold permut_p.intros.
 208 split
 209   [split
 210     [unfold transpose.
 211      apply (eqb_elim i1 i)
 212       [intro.
 213        apply (eqb_elim i1 j)
 214         [simplify.intro.assumption
 215         |simplify.intro.assumption
 216         ]
 217       |intro.
 218        apply (eqb_elim i1 j)
 219         [simplify.intro.assumption
 220         |simplify.intro.assumption
 221         ]
 222       ]
 223     |unfold transpose.
 224      apply (eqb_elim i1 i)
 225       [intro.
 226        apply (eqb_elim i1 j)
 227         [simplify.intro.rewrite < H6.assumption
 228         |simplify.intro.rewrite < H2.rewrite < H5.assumption
 229         ]
 230       |intro.
 231        apply (eqb_elim i1 j)
 232         [simplify.intro.rewrite > H2.rewrite < H6.assumption
 233         |simplify.intro.assumption
 234         ]
 235       ]
 236     ]
 237   |intros.unfold Not.
 238    intro.apply H7.
 239    apply (injective_transpose ? ? ? ? H8).
 240   ]
 241 qed.
 242
 243 theorem eq_map_iter_P_k: \forall f,g.\forall p.\forall a,k,n:nat.
 244 p (S n-k) = true \to (\forall i. (S n)-k < i \to i \le (S n) \to (p i) = false) \to
 245 map_iter_P (S n) p g a f = map_iter_P (S n-k) p g a f.
 246 intros 5.
 247 elim k 3
 248   [rewrite < minus_n_O.reflexivity
 249   |apply (nat_case n1)
 250     [intros.
 251      rewrite > map_iter_P_S_false
 252       [reflexivity
 253       |apply H2[simplify.apply lt_O_S.|apply le_n]
 254       ]
 255     |intros.
 256      rewrite > map_iter_P_S_false
 257       [rewrite > (H m H1)
 258         [reflexivity
 259         |intros.
 260          apply (H2 i H3).
 261          apply le_S.
 262          assumption
 263         ]
 264       |apply H2[auto|apply le_n]
 265       ]
 266     ]
 267   ]
 268 qed.
 269
 270 theorem eq_map_iter_p_a: \forall p.\forall f.\forall g. \forall a,n:nat.
 271 (\forall i.i \le n \to p i = false) \to map_iter_P n p g a f = a.
 272 intros 5.
 273 elim n
 274   [simplify.reflexivity
 275   |rewrite > map_iter_P_S_false
 276     [apply H.
 277      intros.
 278      apply H1.apply le_S.assumption
 279     |apply H1.apply le_n
 280     ]
 281   ]
 282 qed.
 283
 284 theorem eq_map_iter_p_transpose: \forall p.\forall f.associative nat f \to
 285 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. k < n \to
 286 (p (S n) = true) \to (p (n-k)) = true \to (\forall i. n-k < i \to i \le n \to (p i) = false)
 287 \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.
 288 intros 8.
 289 apply (nat_case n)
 290   [intro.absurd (k < O)
 291     [assumption|apply le_to_not_lt.apply le_O_n]
 292   |intros.
 293    rewrite > (map_iter_P_S_true ? ? ? ? ? H3).
 294    rewrite > (map_iter_P_S_true ? ? ? ? ? H3).
 295    rewrite > (eq_map_iter_P_k ? ? ? ? ? ? H4 H5).
 296    rewrite > (eq_map_iter_P_k ? ? ? ? ? ? H4 H5).
 297    generalize in match H4.
 298    rewrite > minus_Sn_m
 299     [intro.
 300      rewrite > (map_iter_P_S_true ? ? ? ? ? H6).
 301      rewrite > (map_iter_P_S_true ? ? ? ? ? H6).
 302      rewrite > transpose_i_j_j.
 303      rewrite > transpose_i_j_i.
 304      cut (map_iter_P (m-k) p g a f =
 305       map_iter_P (m-k) p (\lambda x.g (transpose (S(m-k)) (S(S m)) x)) a f)
 306       [rewrite < Hcut.
 307        rewrite < H.
 308        rewrite < H1 in \vdash (? ? (? % ?) ?).
 309        rewrite > H.
 310        reflexivity
 311       |apply eq_map_iter_P.
 312        intros.unfold transpose.
 313        cut (eqb m1 (S (m-k)) =false)
 314         [cut (eqb m1 (S (S m)) =false)
 315           [rewrite > Hcut.
 316            rewrite > Hcut1.
 317            reflexivity
 318           |apply not_eq_to_eqb_false.
 319            apply lt_to_not_eq.
 320            apply (le_to_lt_to_lt ? m)
 321             [apply (trans_le ? (m-k))
 322               [assumption|auto]
 323             |apply le_S.apply le_n
 324             ]
 325           ]
 326         |apply not_eq_to_eqb_false.
 327          apply lt_to_not_eq.
 328          unfold.auto
 329         ]
 330       ]
 331     |apply le_S_S_to_le.assumption
 332     ]
 333   ]
 334 qed.
 335
 336 theorem eq_map_iter_p_transpose1: \forall p.\forall f.associative nat f \to
 337 symmetric2 nat nat f \to \forall g. \forall a,k1,k2,n:nat. O < k1 \to k1 < k2 \to k2 \le n \to
 338 (p k1) = true \to (p k2) = true \to (\forall i. k1 < i \to i < k2 \to (p i) = false)
 339 \to map_iter_P n p g a f = map_iter_P n p (\lambda m. g (transpose k1 k2 m)) a f.
 340 intros 10.
 341 elim n 2
 342   [absurd (k2 \le O)
 343     [assumption|apply lt_to_not_le.apply (trans_lt ? k1 ? H2 H3)]
 344   |apply (eqb_elim (S n1) k2)
 345    [intro.
 346     rewrite < H4.
 347     intros.
 348     cut (k1 = n1 - (n1 -k1))
 349      [rewrite > Hcut.
 350       apply (eq_map_iter_p_transpose p f H H1 g a (n1-k1))
 351         [cut (k1 \le n1)[auto|auto]
 352         |assumption
 353         |rewrite < Hcut.assumption
 354         |rewrite < Hcut.intros.
 355          apply (H9 i H10).unfold.auto
 356        ]
 357      |apply sym_eq.
 358        apply plus_to_minus.
 359        auto.
 360      ]
 361    |intros.
 362      cut ((S n1) \neq k1)
 363       [apply (bool_elim ? (p (S n1)))
 364        [intro.
 365         rewrite > map_iter_P_S_true
 366           [rewrite > map_iter_P_S_true
 367             [cut ((transpose k1 k2 (S n1)) = (S n1))
 368               [rewrite > Hcut1.
 369                apply eq_f.
 370                apply (H3 H5)
 371                 [elim (le_to_or_lt_eq ? ? H6)
 372                   [auto
 373                   |absurd (S n1=k2)[apply sym_eq.assumption|assumption]
 374                   ]
 375                 |assumption
 376                 |assumption
 377                 |assumption
 378                 ]
 379               |unfold transpose.
 380                rewrite > (not_eq_to_eqb_false ? ? Hcut).
 381                rewrite > (not_eq_to_eqb_false ? ? H4).
 382                reflexivity
 383               ]
 384             |assumption
 385             ]
 386           |assumption
 387           ]
 388         |intro.
 389           rewrite > map_iter_P_S_false
 390           [rewrite > map_iter_P_S_false
 391             [apply (H3 H5)
 392               [elim (le_to_or_lt_eq ? ? H6)
 393                 [auto
 394                 |absurd (S n1=k2)[apply sym_eq.assumption|assumption]
 395                 ]
 396               |assumption
 397               |assumption
 398               |assumption
 399               ]
 400             |assumption
 401             ]
 402           |assumption
 403           ]
 404         ]
 405       |unfold.intro.
 406        absurd (k1 < k2)
 407         [assumption
 408         |apply le_to_not_lt.
 409          rewrite < H10.
 410          assumption
 411         ]
 412       ]
 413     ]
 414   ]
 415 qed.
 416
 417 lemma decidable_n:\forall p.\forall n.
 418 (\forall m. m \le n \to (p m) = false) \lor
 419 (\exists m. m \le n \land (p m) = true \land
 420 \forall i. m < i \to i \le n \to (p i) = false).
 421 intros.
 422 elim n
 423   [apply (bool_elim ? (p O))
 424     [intro.right.
 425      apply (ex_intro ? ? O).
 426      split
 427       [split[apply le_n|assumption]
 428       |intros.absurd (O<i)[assumption|apply le_to_not_lt.assumption]
 429       ]
 430     |intro.left.
 431      intros.apply (le_n_O_elim m H1).assumption
 432     ]
 433   |apply (bool_elim ? (p (S n1)))
 434     [intro.right.
 435      apply (ex_intro ? ? (S n1)).
 436      split
 437       [split[apply le_n|assumption]
 438       |intros.absurd (S n1<i)[assumption|apply le_to_not_lt.assumption]
 439       ]
 440     |elim H
 441       [left.
 442        intros.
 443        elim (le_to_or_lt_eq m (S n1) H3)
 444         [apply H1.apply le_S_S_to_le.assumption
 445         |rewrite > H4.assumption
 446         ]
 447       |right.
 448        elim H1.elim H3.elim H4.
 449        apply (ex_intro ? ? a).
 450        split
 451         [split[apply le_S.assumption|assumption]
 452         |intros.elim (le_to_or_lt_eq i (S n1) H9)
 453           [apply H5[assumption|apply le_S_S_to_le.assumption]
 454           |rewrite > H10.assumption
 455           ]
 456         ]
 457       ]
 458     ]
 459   ]
 460 qed.
 461
 462 lemma decidable_n1:\forall p.\forall n,j. j \le n \to (p j)=true \to
 463 (\forall m. j < m \to m \le n \to (p m) = false) \lor
 464 (\exists m. j < m \land m \le n \land (p m) = true \land
 465 \forall i. m < i \to i \le n \to (p i) = false).
 466 intros.
 467 elim (decidable_n p n)
 468   [absurd ((p j)=true)
 469     [assumption
 470     |unfold.intro.
 471      apply not_eq_true_false.
 472      rewrite < H3.
 473      apply H2.assumption
 474     ]
 475   |elim H2.clear H2.
 476    apply (nat_compare_elim j a)
 477     [intro.
 478      right.
 479      apply (ex_intro ? ? a).
 480      elim H3.clear H3.
 481      elim H4.clear H4.
 482      split
 483       [split
 484         [split
 485           [assumption|assumption]
 486         |assumption
 487         ]
 488       |assumption
 489       ]
 490     |intro.
 491      rewrite > H2.
 492      left.
 493      elim H3 2.assumption
 494     |intro.
 495      absurd (p j = true)
 496       [assumption
 497       |unfold.intro.
 498        apply not_eq_true_false.
 499        rewrite < H4.
 500        elim H3.clear H3.
 501        apply (H6 j H2).assumption
 502       ]
 503     ]
 504   ]
 505 qed.
 506
 507 lemma decidable_n2:\forall p.\forall n,j. j \le n \to (p j)=true \to
 508 (\forall m. j < m \to m \le n \to (p m) = false) \lor
 509 (\exists m. j < m \land m \le n \land (p m) = true \land
 510 \forall i. j < i \to i < m \to (p i) = false).
 511 intros 3.
 512 elim n
 513   [left.
 514    apply (le_n_O_elim j H).intros.
 515    absurd (m \le O)
 516     [assumption|apply lt_to_not_le.assumption]
 517   |elim (le_to_or_lt_eq ? ? H1)
 518     [cut (j \le n1)
 519       [elim (H Hcut H2)
 520         [apply (bool_elim ? (p (S n1)))
 521           [intro.
 522            right.
 523            apply (ex_intro ? ? (S n1)).
 524            split
 525             [split
 526               [split
 527                 [assumption|apply le_n]
 528               |assumption
 529               ]
 530             |intros.
 531              apply (H4 i H6).
 532              apply le_S_S_to_le.
 533              assumption
 534             ]
 535           |intro.
 536            left.
 537            intros.
 538            elim (le_to_or_lt_eq ? ? H7)
 539             [apply H4
 540               [assumption|apply le_S_S_to_le.assumption]
 541             |rewrite > H8.assumption
 542             ]
 543           ]
 544         |right.
 545          elim H4.clear H4.
 546          elim H5.clear H5.
 547          elim H4.clear H4.
 548          elim H5.clear H5.
 549          apply (ex_intro ? ? a).
 550          split
 551           [split
 552             [split[assumption|apply le_S.assumption]
 553             |assumption
 554             ]
 555           |assumption
 556           ]
 557         ]
 558       |apply le_S_S_to_le.
 559        assumption
 560       ]
 561     |left.
 562      intros.
 563      absurd (j < m)
 564       [assumption
 565       |apply le_to_not_lt.
 566        rewrite > H3.
 567        assumption
 568       ]
 569     ]
 570   ]
 571 qed.
 572
 573 (* tutti d spostare *)
 574 theorem lt_minus_to_lt_plus:
 575 \forall n,m,p. n - m < p \to n < m + p.
 576 intros 2.
 577 apply (nat_elim2 ? ? ? ? n m)
 578   [simplify.intros.auto.
 579   |intros 2.rewrite < minus_n_O.
 580    intro.assumption
 581   |intros.
 582    simplify.
 583    cut (n1 < m1+p)
 584     [auto
 585     |apply H.
 586      apply H1
 587     ]
 588   ]
 589 qed.
 590
 591 theorem lt_plus_to_lt_minus:
 592 \forall n,m,p. m \le n \to n < m + p \to n - m < p.
 593 intros 2.
 594 apply (nat_elim2 ? ? ? ? n m)
 595   [simplify.intros 3.
 596    apply (le_n_O_elim ? H).
 597    simplify.intros.assumption
 598   |simplify.intros.assumption.
 599   |intros.
 600    simplify.
 601    apply H
 602     [apply le_S_S_to_le.assumption
 603     |apply le_S_S_to_le.apply H2
 604     ]
 605   ]
 606 qed.
 607
 608 theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n).
 609 intros.
 610 apply sym_eq.
 611 apply plus_to_minus.
 612 auto.
 613 qed.
 614
 615 theorem eq_map_iter_p_transpose2: \forall p.\forall f.associative nat f \to
 616 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le n \to
 617 (p (S n) = true) \to (p k) = true
 618 \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.
 619 intros 10.
 620 cut (k = (S n)-(S n -k))
 621   [generalize in match H3.clear H3.
 622    generalize in match g.
 623    generalize in match H2.clear H2.
 624    rewrite > Hcut.
 625    (*generalize in match Hcut.clear Hcut.*)
 626    (* generalize in match H3.clear H3.*)
 627    (* something wrong here
 628      rewrite > Hcut in \vdash (?\rarr ?\rarr %). *)
 629    apply (nat_elim1 (S n - k)).
 630      intros.
 631      elim (decidable_n2 p n (S n -m) H4 H6)
 632       [apply (eq_map_iter_p_transpose1 p f H H1 f1 a)
 633         [assumption.
 634         |unfold.auto.
 635         |apply le_n
 636         |assumption
 637         |assumption
 638         |intros.apply H7
 639           [assumption|apply le_S_S_to_le.assumption]
 640         ]
 641       |elim H7.clear H7.
 642        elim H8.clear H8.
 643        elim H7.clear H7.
 644        elim H8.clear H8.
 645        apply (trans_eq  ? ?
 646         (map_iter_P (S n) p (\lambda i.f1 (transpose a1 (S n) (transpose (S n -m) a1 i))) a f))
 647         [apply (trans_eq  ? ?
 648          (map_iter_P (S n) p (\lambda i.f1 (transpose a1 (S n) i)) a f))
 649           [cut (a1 = (S n -(S n -a1)))
 650             [rewrite > Hcut1.
 651              apply H2
 652               [apply lt_plus_to_lt_minus
 653                 [apply le_S.assumption
 654                 |rewrite < sym_plus.
 655                  apply lt_minus_to_lt_plus.
 656                  assumption
 657                 ]
 658               |rewrite < Hcut1.
 659                apply (trans_lt ? (S n -m))[assumption|assumption]
 660               |rewrite < Hcut1.assumption
 661               |assumption
 662               |rewrite < Hcut1.assumption
 663               ]
 664            |apply minus_m_minus_mn.
 665             apply le_S.assumption
 666            ]
 667          |apply (eq_map_iter_p_transpose1 p f H H1)
 668           [assumption
 669           |assumption
 670           |apply le_S.assumption
 671           |assumption
 672           |assumption
 673           |assumption
 674           ]
 675         ]
 676       |apply (trans_eq  ? ?
 677         (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))
 678         [cut (a1 = (S n) -(S n -a1))
 679           [apply H2
 680             [apply lt_plus_to_lt_minus
 681               [apply le_S.assumption
 682               |rewrite < sym_plus.
 683                apply lt_minus_to_lt_plus.
 684                assumption
 685               ]
 686             |rewrite < Hcut1.
 687              apply (trans_lt ? (S n -m))[assumption|assumption]
 688             |rewrite < Hcut1.assumption
 689             |assumption
 690             |rewrite < Hcut1.assumption
 691             ]
 692           |apply minus_m_minus_mn.
 693            apply le_S.assumption
 694           ]
 695         |apply eq_map_iter_P.
 696          cut (a1 = (S n) -(S n -a1))
 697           [intros.
 698            apply eq_f.
 699            rewrite < Hcut1.
 700            rewrite < transpose_i_j_j_i.
 701            rewrite > (transpose_i_j_j_i (S n -m)).
 702            rewrite > (transpose_i_j_j_i a1 (S n)).
 703            rewrite > (transpose_i_j_j_i (S n -m)).
 704            apply sym_eq.
 705            apply eq_transpose
 706             [unfold.intro.
 707              apply (not_le_Sn_n n).
 708              rewrite < H12.assumption
 709             |unfold.intro.
 710              apply (not_le_Sn_n n).
 711              rewrite > H12.assumption
 712             |unfold.intro.
 713              apply (not_le_Sn_n a1).
 714              rewrite < H12 in \vdash (? (? %) ?).assumption
 715             ]
 716           |apply minus_m_minus_mn.
 717            apply le_S.assumption
 718           ]
 719         ]
 720       ]
 721     ]
 722   |apply minus_m_minus_mn.
 723    apply le_S.assumption
 724   ]
 725 qed.
 726
 727 theorem eq_map_iter_p_transpose3: \forall p.\forall f.associative nat f \to
 728 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le (S n) \to
 729 (p (S n) = true) \to (p k) = true
 730 \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.
 731 intros.
 732 elim (le_to_or_lt_eq ? ? H3)
 733   [apply (eq_map_iter_p_transpose2 p f H H1 g a k n H2)
 734     [apply le_S_S_to_le.assumption|assumption|assumption]
 735   |rewrite > H6.
 736    apply eq_map_iter_P.
 737    intros.
 738    apply eq_f.apply sym_eq. apply transpose_i_i.
 739   ]
 740 qed.
 741
 742 lemma permut_p_O: \forall p.\forall h.\forall n.
 743 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).
 744 intros.unfold permut_p in H.
 745 apply not_le_to_lt.unfold.intro.
 746 elim (H (S m) H2 H3).
 747 elim H5.
 748 absurd (p (h (S m)) = true)
 749   [assumption
 750   |apply (le_n_O_elim ? H4).
 751    unfold.intro.
 752    apply not_eq_true_false.
 753    rewrite < H9.rewrite < H1.reflexivity
 754   ]
 755 qed.
 756
 757 theorem eq_map_iter_p_permut: \forall p.\forall f.associative nat f \to
 758 symmetric2 nat nat f \to \forall n.\forall g. \forall h.\forall a:nat.
 759 permut_p h p n \to p O = false \to
 760 map_iter_P n p g a f = map_iter_P n p (compose ? ? ? g h) a f .
 761 intros 5.
 762 elim n
 763   [simplify.reflexivity
 764   |apply (bool_elim ? (p (S n1)))
 765     [intro.
 766      apply (trans_eq ? ? (map_iter_P (S n1) p (\lambda m.g ((transpose (h (S n1)) (S n1)) m)) a f))
 767       [unfold permut_p in H3.
 768        elim (H3 (S n1) (le_n ?) H5).
 769        elim H6. clear H6.
 770        apply (eq_map_iter_p_transpose3 p f H H1 g a (h(S n1)) n1)
 771         [apply (permut_p_O ? ? ? H3 H4)
 772           [apply le_n|assumption]
 773         |assumption
 774         |assumption
 775         |assumption
 776         ]
 777       |apply (trans_eq ? ? (map_iter_P (S n1) p (\lambda m.
 778         (g(transpose (h (S n1)) (S n1)
 779          (transpose (h (S n1)) (S n1) (h m)))) ) a f))
 780         [rewrite > (map_iter_P_S_true ? ? ? ? ? H5).
 781          rewrite > (map_iter_P_S_true ? ? ? ? ? H5).
 782          apply eq_f2
 783           [rewrite > transpose_i_j_j.
 784            rewrite > transpose_i_j_i.
 785            rewrite > transpose_i_j_j.
 786            reflexivity
 787           |apply (H2 (\lambda m.(g(transpose (h (S n1)) (S n1) m))) ?)
 788             [unfold.intros.
 789              split
 790               [split
 791                 [simplify.
 792                  unfold permut_p in H3.
 793                  elim (H3 i (le_S ? ? H6) H7).
 794                  elim H8. clear H8.
 795                  elim (le_to_or_lt_eq ? ? H10)
 796                   [unfold transpose.
 797                    rewrite > (not_eq_to_eqb_false ? ? (lt_to_not_eq ? ? H8)).
 798                    cut (h i \neq h (S n1))
 799                     [rewrite > (not_eq_to_eqb_false ? ? Hcut).
 800                      simplify.
 801                      apply le_S_S_to_le.
 802                      assumption
 803                     |apply H9
 804                       [apply H5
 805                       |apply le_n
 806                       |apply lt_to_not_eq.
 807                        unfold.apply le_S_S.assumption
 808                       ]
 809                     ]
 810                   |rewrite > H8.
 811                    apply (eqb_elim (S n1) (h (S n1)))
 812                     [intro.
 813                      absurd (h i = h (S n1))
 814                       [rewrite > H8.
 815                        assumption
 816                       |apply H9
 817                         [assumption
 818                         |apply le_n
 819                         |apply lt_to_not_eq.
 820                          unfold.apply le_S_S.assumption
 821                         ]
 822                       ]
 823                     |intro.
 824                      unfold transpose.
 825                      rewrite > (not_eq_to_eqb_false ? ? H12).
 826                      rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S n1))).
 827                      simplify.
 828                      elim (H3 (S n1) (le_n ? ) H5).
 829                      elim H13.clear H13.
 830                      elim (le_to_or_lt_eq ? ? H15)
 831                       [apply le_S_S_to_le.assumption
 832                       |apply False_ind.
 833                        apply H12.
 834                        apply sym_eq.assumption
 835                       ]
 836                     ]
 837                   ]
 838                 |simplify.
 839                  unfold permut_p in H3.
 840                  unfold transpose.
 841                  apply (eqb_elim (h i) (S n1))
 842                   [intro.
 843                    apply (eqb_elim (h i) (h (S n1)))
 844                     [intro.simplify.assumption
 845                     |intro.simplify.
 846                      elim (H3 (S n1) (le_n ? ) H5).
 847                      elim H10. assumption
 848                     ]
 849                   |intro.
 850                    apply (eqb_elim (h i) (h (S n1)))
 851                     [intro.simplify.assumption
 852                     |intro.simplify.
 853                      elim (H3 i (le_S ? ? H6) H7).
 854                      elim H10. assumption
 855                     ]
 856                   ]
 857                 ]
 858               |simplify.intros.unfold Not.intro.
 859                unfold permut_p in H3.
 860                elim (H3 i (le_S i ? H6) H7).
 861                apply (H13 j H8 (le_S j ? H9) H10).
 862                apply (injective_transpose ? ? ? ? H11)
 863               ]
 864             |assumption
 865             ]
 866           ]
 867         |apply eq_map_iter_P.
 868          intros.
 869          rewrite > transpose_transpose.reflexivity
 870         ]
 871       ]
 872   |intro.
 873    rewrite > (map_iter_P_S_false ? ? ? ? ? H5).
 874    rewrite > (map_iter_P_S_false ? ? ? ? ? H5).
 875    apply H2
 876     [unfold permut_p.
 877      unfold permut_p in H3.
 878      intros.
 879      elim (H3 i (le_S i ? H6) H7).
 880      elim H8.
 881       split
 882         [split
 883           [elim (le_to_or_lt_eq ? ? H10)
 884             [apply le_S_S_to_le.assumption
 885             |absurd (p (h i) = true)
 886               [assumption
 887               |rewrite > H12.
 888                rewrite > H5.
 889                unfold.intro.apply not_eq_true_false.
 890                apply sym_eq.assumption
 891               ]
 892             ]
 893           |assumption
 894           ]
 895         |intros.
 896          apply H9
 897           [assumption|apply (le_S ? ? H13)|assumption]
 898         ]
 899       |assumption
 900       ]
 901     ]
 902   ]
 903 qed.
 904