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
  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        autobatch
 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[autobatch|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|autobatch]
 331             |apply le_S.apply le_n
 332             ]
 333           ]
 334         |apply not_eq_to_eqb_false.
 335          apply lt_to_not_eq.
 336          unfold.autobatch
 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)[autobatch|autobatch]
 360         |assumption
 361         |rewrite < Hcut.assumption
 362         |rewrite < Hcut.intros.
 363          apply (H9 i H10).unfold.autobatch
 364        ]
 365      |apply sym_eq.
 366        apply plus_to_minus.
 367        autobatch.
 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                   [autobatch
 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                 [autobatch
 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 theorem eq_map_iter_p_transpose2: \forall p.\forall f.associative nat f \to
 582 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le n \to
 583 (p (S n) = true) \to (p k) = true
 584 \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.
 585 intros 10.
 586 cut (k = (S n)-(S n -k))
 587   [generalize in match H3.clear H3.
 588    generalize in match g.
 589    generalize in match H2.clear H2.
 590    rewrite > Hcut.
 591    (*generalize in match Hcut.clear Hcut.*)
 592    (* generalize in match H3.clear H3.*)
 593    (* something wrong here
 594      rewrite > Hcut in \vdash (?\rarr ?\rarr %). *)
 595    apply (nat_elim1 (S n - k)).
 596      intros.
 597      elim (decidable_n2 p n (S n -m) H4 H6)
 598       [apply (eq_map_iter_p_transpose1 p f H H1 f1 a)
 599         [assumption.
 600         |unfold.autobatch.
 601         |apply le_n
 602         |assumption
 603         |assumption
 604         |intros.apply H7
 605           [assumption|apply le_S_S_to_le.assumption]
 606         ]
 607       |elim H7.clear H7.
 608        elim H8.clear H8.
 609        elim H7.clear H7.
 610        elim H8.clear H8.
 611        apply (trans_eq  ? ?
 612         (map_iter_p (S n) p (\lambda i.f1 (transpose a1 (S n) (transpose (S n -m) a1 i))) a f))
 613         [apply (trans_eq  ? ?
 614          (map_iter_p (S n) p (\lambda i.f1 (transpose a1 (S n) i)) a f))
 615           [cut (a1 = (S n -(S n -a1)))
 616             [rewrite > Hcut1.
 617              apply H2
 618               [apply lt_plus_to_lt_minus
 619                 [apply le_S.assumption
 620                 |rewrite < sym_plus.
 621                  apply lt_minus_to_lt_plus.
 622                  assumption
 623                 ]
 624               |rewrite < Hcut1.
 625                apply (trans_lt ? (S n -m))[assumption|assumption]
 626               |rewrite < Hcut1.assumption
 627               |assumption
 628               |rewrite < Hcut1.assumption
 629               ]
 630            |apply minus_m_minus_mn.
 631             apply le_S.assumption
 632            ]
 633          |apply (eq_map_iter_p_transpose1 p f H H1)
 634           [assumption
 635           |assumption
 636           |apply le_S.assumption
 637           |assumption
 638           |assumption
 639           |assumption
 640           ]
 641         ]
 642       |apply (trans_eq  ? ?
 643         (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))
 644         [cut (a1 = (S n) -(S n -a1))
 645           [apply H2
 646             [apply lt_plus_to_lt_minus
 647               [apply le_S.assumption
 648               |rewrite < sym_plus.
 649                apply lt_minus_to_lt_plus.
 650                assumption
 651               ]
 652             |rewrite < Hcut1.
 653              apply (trans_lt ? (S n -m))[assumption|assumption]
 654             |rewrite < Hcut1.assumption
 655             |assumption
 656             |rewrite < Hcut1.assumption
 657             ]
 658           |apply minus_m_minus_mn.
 659            apply le_S.assumption
 660           ]
 661         |apply eq_map_iter_p.
 662          cut (a1 = (S n) -(S n -a1))
 663           [intros.
 664            apply eq_f.
 665            rewrite < Hcut1.
 666            rewrite < transpose_i_j_j_i.
 667            rewrite > (transpose_i_j_j_i (S n -m)).
 668            rewrite > (transpose_i_j_j_i a1 (S n)).
 669            rewrite > (transpose_i_j_j_i (S n -m)).
 670            apply sym_eq.
 671            apply eq_transpose
 672             [unfold.intro.
 673              apply (not_le_Sn_n n).
 674              rewrite < H12.assumption
 675             |unfold.intro.
 676              apply (not_le_Sn_n n).
 677              rewrite > H12.assumption
 678             |unfold.intro.
 679              apply (not_le_Sn_n a1).
 680              rewrite < H12 in \vdash (? (? %) ?).assumption
 681             ]
 682           |apply minus_m_minus_mn.
 683            apply le_S.assumption
 684           ]
 685         ]
 686       ]
 687     ]
 688   |apply minus_m_minus_mn.
 689    apply le_S.assumption
 690   ]
 691 qed.
 692
 693 theorem eq_map_iter_p_transpose3: \forall p.\forall f.associative nat f \to
 694 symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le (S n) \to
 695 (p (S n) = true) \to (p k) = true
 696 \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.
 697 intros.
 698 elim (le_to_or_lt_eq ? ? H3)
 699   [apply (eq_map_iter_p_transpose2 p f H H1 g a k n H2)
 700     [apply le_S_S_to_le.assumption|assumption|assumption]
 701   |rewrite > H6.
 702    apply eq_map_iter_p.
 703    intros.
 704    apply eq_f.apply sym_eq. apply transpose_i_i.
 705   ]
 706 qed.
 707
 708 lemma permut_p_O: \forall p.\forall h.\forall n.
 709 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).
 710 intros.unfold permut_p in H.
 711 apply not_le_to_lt.unfold.intro.
 712 elim (H (S m) H2 H3).
 713 elim H5.
 714 absurd (p (h (S m)) = true)
 715   [assumption
 716   |apply (le_n_O_elim ? H4).
 717    unfold.intro.
 718    apply not_eq_true_false.
 719    rewrite < H9.rewrite < H1.reflexivity
 720   ]
 721 qed.
 722
 723 theorem eq_map_iter_p_permut: \forall p.\forall f.associative nat f \to
 724 symmetric2 nat nat f \to \forall n.\forall g. \forall h.\forall a:nat.
 725 permut_p h p n \to p O = false \to
 726 map_iter_p n p g a f = map_iter_p n p (compose ? ? ? g h) a f .
 727 intros 5.
 728 elim n
 729   [simplify.reflexivity
 730   |apply (bool_elim ? (p (S n1)))
 731     [intro.
 732      apply (trans_eq ? ? (map_iter_p (S n1) p (\lambda m.g ((transpose (h (S n1)) (S n1)) m)) a f))
 733       [unfold permut_p in H3.
 734        elim (H3 (S n1) (le_n ?) H5).
 735        elim H6. clear H6.
 736        apply (eq_map_iter_p_transpose3 p f H H1 g a (h(S n1)) n1)
 737         [apply (permut_p_O ? ? ? H3 H4)
 738           [apply le_n|assumption]
 739         |assumption
 740         |assumption
 741         |assumption
 742         ]
 743       |apply (trans_eq ? ? (map_iter_p (S n1) p (\lambda m.
 744         (g(transpose (h (S n1)) (S n1)
 745          (transpose (h (S n1)) (S n1) (h m)))) ) a f))
 746         [rewrite > (map_iter_p_S_true ? ? ? ? ? H5).
 747          rewrite > (map_iter_p_S_true ? ? ? ? ? H5).
 748          apply eq_f2
 749           [rewrite > transpose_i_j_j.
 750            rewrite > transpose_i_j_i.
 751            rewrite > transpose_i_j_j.
 752            reflexivity
 753           |apply (H2 (\lambda m.(g(transpose (h (S n1)) (S n1) m))) ?)
 754             [unfold.intros.
 755              split
 756               [split
 757                 [simplify.
 758                  unfold permut_p in H3.
 759                  elim (H3 i (le_S ? ? H6) H7).
 760                  elim H8. clear H8.
 761                  elim (le_to_or_lt_eq ? ? H10)
 762                   [unfold transpose.
 763                    rewrite > (not_eq_to_eqb_false ? ? (lt_to_not_eq ? ? H8)).
 764                    cut (h i \neq h (S n1))
 765                     [rewrite > (not_eq_to_eqb_false ? ? Hcut).
 766                      simplify.
 767                      apply le_S_S_to_le.
 768                      assumption
 769                     |apply H9
 770                       [apply H5
 771                       |apply le_n
 772                       |apply lt_to_not_eq.
 773                        unfold.apply le_S_S.assumption
 774                       ]
 775                     ]
 776                   |rewrite > H8.
 777                    apply (eqb_elim (S n1) (h (S n1)))
 778                     [intro.
 779                      absurd (h i = h (S n1))
 780                       [rewrite > H8.
 781                        assumption
 782                       |apply H9
 783                         [assumption
 784                         |apply le_n
 785                         |apply lt_to_not_eq.
 786                          unfold.apply le_S_S.assumption
 787                         ]
 788                       ]
 789                     |intro.
 790                      unfold transpose.
 791                      rewrite > (not_eq_to_eqb_false ? ? H12).
 792                      rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S n1))).
 793                      simplify.
 794                      elim (H3 (S n1) (le_n ? ) H5).
 795                      elim H13.clear H13.
 796                      elim (le_to_or_lt_eq ? ? H15)
 797                       [apply le_S_S_to_le.assumption
 798                       |apply False_ind.
 799                        apply H12.
 800                        apply sym_eq.assumption
 801                       ]
 802                     ]
 803                   ]
 804                 |simplify.
 805                  unfold permut_p in H3.
 806                  unfold transpose.
 807                  apply (eqb_elim (h i) (S n1))
 808                   [intro.
 809                    apply (eqb_elim (h i) (h (S n1)))
 810                     [intro.simplify.assumption
 811                     |intro.simplify.
 812                      elim (H3 (S n1) (le_n ? ) H5).
 813                      elim H10. assumption
 814                     ]
 815                   |intro.
 816                    apply (eqb_elim (h i) (h (S n1)))
 817                     [intro.simplify.assumption
 818                     |intro.simplify.
 819                      elim (H3 i (le_S ? ? H6) H7).
 820                      elim H10. assumption
 821                     ]
 822                   ]
 823                 ]
 824               |simplify.intros.unfold Not.intro.
 825                unfold permut_p in H3.
 826                elim (H3 i (le_S i ? H6) H7).
 827                apply (H13 j H8 (le_S j ? H9) H10).
 828                apply (injective_transpose ? ? ? ? H11)
 829               ]
 830             |assumption
 831             ]
 832           ]
 833         |apply eq_map_iter_p.
 834          intros.
 835          rewrite > transpose_transpose.reflexivity
 836         ]
 837       ]
 838   |intro.
 839    rewrite > (map_iter_p_S_false ? ? ? ? ? H5).
 840    rewrite > (map_iter_p_S_false ? ? ? ? ? H5).
 841    apply H2
 842     [unfold permut_p.
 843      unfold permut_p in H3.
 844      intros.
 845      elim (H3 i (le_S i ? H6) H7).
 846      elim H8.
 847       split
 848         [split
 849           [elim (le_to_or_lt_eq ? ? H10)
 850             [apply le_S_S_to_le.assumption
 851             |absurd (p (h i) = true)
 852               [assumption
 853               |rewrite > H12.
 854                rewrite > H5.
 855                unfold.intro.apply not_eq_true_false.
 856                apply sym_eq.assumption
 857               ]
 858             ]
 859           |assumption
 860           ]
 861         |intros.
 862          apply H9
 863           [assumption|apply (le_S ? ? H13)|assumption]
 864         ]
 865       |assumption
 866       ]
 867     ]
 868   ]
 869 qed.
 870