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