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