matita/library/nat/iteration2.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/primes.ma".
  16 include "nat/ord.ma".
  17 include "nat/generic_iter_p.ma".
  18 include "nat/count.ma".(*necessary just to use bool_to_nat and bool_to_nat_andb*)
  19
  20 (* sigma_p on nautral numbers is a specialization of sigma_p_gen *)
  21 definition sigma_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def
  22 \lambda n, p, g. (iter_p_gen n p nat g O plus).
  23
  24 theorem symmetricIntPlus: symmetric nat plus.
  25 change with (\forall a,b:nat. (plus a b) = (plus b a)).
  26 intros.
  27 rewrite > sym_plus.
  28 reflexivity.
  29 qed.
  30
  31 (*the following theorems on sigma_p in N are obtained by the more general ones
  32  * in sigma_p_gen.ma
  33  *)
  34 theorem true_to_sigma_p_Sn:
  35 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
  36 p n = true \to sigma_p (S n) p g =
  37 (g n)+(sigma_p n p g).
  38 intros.
  39 unfold sigma_p.
  40 apply true_to_iter_p_gen_Sn.
  41 assumption.
  42 qed.
  43
  44 theorem false_to_sigma_p_Sn:
  45 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
  46 p n = false \to sigma_p (S n) p g = sigma_p n p g.
  47 intros.
  48 unfold sigma_p.
  49 apply false_to_iter_p_gen_Sn.
  50 assumption.
  51 qed.
  52
  53 theorem eq_sigma_p: \forall p1,p2:nat \to bool.
  54 \forall g1,g2: nat \to nat.\forall n.
  55 (\forall x.  x < n \to p1 x = p2 x) \to
  56 (\forall x.  x < n \to g1 x = g2 x) \to
  57 sigma_p n p1 g1 = sigma_p n p2 g2.
  58 intros.
  59 unfold sigma_p.
  60 apply eq_iter_p_gen;
  61   assumption.
  62 qed.
  63
  64 theorem eq_sigma_p1: \forall p1,p2:nat \to bool.
  65 \forall g1,g2: nat \to nat.\forall n.
  66 (\forall x.  x < n \to p1 x = p2 x) \to
  67 (\forall x.  x < n \to p1 x = true \to g1 x = g2 x) \to
  68 sigma_p n p1 g1 = sigma_p n p2 g2.
  69 intros.
  70 unfold sigma_p.
  71 apply eq_iter_p_gen1;
  72   assumption.
  73 qed.
  74
  75 theorem sigma_p_false:
  76 \forall g: nat \to nat.\forall n.sigma_p n (\lambda x.false) g = O.
  77 intros.
  78 unfold sigma_p.
  79 apply iter_p_gen_false.
  80 qed.
  81
  82 theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool.
  83 \forall g: nat \to nat.
  84 sigma_p (k+n) p g
  85 = sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g.
  86 intros.
  87 unfold sigma_p.
  88 apply (iter_p_gen_plusA nat n k p g O plus)
  89 [ apply symmetricIntPlus.
  90 | intros.
  91   apply sym_eq.
  92   apply plus_n_O
  93 | apply associative_plus
  94 ]
  95 qed.
  96
  97 theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to
  98 \forall p:nat \to bool.
  99 \forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to
 100 p i = false) \to sigma_p m p g = sigma_p n p g.
 101 intros.
 102 unfold sigma_p.
 103 apply (false_to_eq_iter_p_gen);
 104   assumption.
 105 qed.
 106
 107 theorem or_false_to_eq_sigma_p:
 108 \forall n,m:nat.\forall p:nat \to bool.
 109 \forall g: nat \to nat.
 110 n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = O)
 111 \to sigma_p m p g = sigma_p n p g.
 112 intros.
 113 unfold sigma_p.
 114 apply or_false_eq_baseA_to_eq_iter_p_gen
 115   [intros.reflexivity
 116   |assumption
 117   |assumption
 118   ]
 119 qed.
 120
 121 theorem bool_to_nat_to_eq_sigma_p:
 122 \forall n:nat.\forall p1,p2:nat \to bool.
 123 \forall g1,g2: nat \to nat.
 124 (\forall i:nat.
 125 bool_to_nat (p1 i)*(g1 i) = bool_to_nat (p2 i)*(g2 i))
 126 \to sigma_p n p1 g1 = sigma_p n p2 g2.
 127 intros.elim n
 128   [reflexivity
 129   |generalize in match (H n1).
 130    apply (bool_elim ? (p1 n1));intro
 131     [apply (bool_elim ? (p2 n1));intros
 132       [rewrite > true_to_sigma_p_Sn
 133         [rewrite > true_to_sigma_p_Sn
 134           [apply eq_f2
 135             [simplify in H4.
 136              rewrite > plus_n_O.
 137              rewrite > plus_n_O in ⊢ (? ? ? %).
 138              assumption
 139             |assumption
 140             ]
 141           |assumption
 142           ]
 143         |assumption
 144         ]
 145       |rewrite > true_to_sigma_p_Sn
 146         [rewrite > false_to_sigma_p_Sn
 147           [change in ⊢ (? ? ? %) with (O + sigma_p n1 p2 g2).
 148            apply eq_f2
 149             [simplify in H4.
 150              rewrite > plus_n_O.
 151              assumption
 152             |assumption
 153             ]
 154           |assumption
 155           ]
 156         |assumption
 157         ]
 158       ]
 159     |apply (bool_elim ? (p2 n1));intros
 160       [rewrite > false_to_sigma_p_Sn
 161         [rewrite > true_to_sigma_p_Sn
 162           [change in ⊢ (? ? % ?) with (O + sigma_p n1 p1 g1).
 163            apply eq_f2
 164             [simplify in H4.
 165              rewrite < plus_n_O in H4.
 166              assumption
 167             |assumption
 168             ]
 169           |assumption
 170           ]
 171         |assumption
 172         ]
 173       |rewrite > false_to_sigma_p_Sn
 174         [rewrite > false_to_sigma_p_Sn
 175           [assumption
 176           |assumption
 177           ]
 178         |assumption
 179         ]
 180       ]
 181     ]
 182   ]
 183 qed.
 184
 185 theorem sigma_p2 :
 186 \forall n,m:nat.
 187 \forall p1,p2:nat \to bool.
 188 \forall g: nat \to nat \to nat.
 189 sigma_p (n*m)
 190   (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
 191   (\lambda x.g (div x m) (mod x m)) =
 192 sigma_p n p1
 193   (\lambda x.sigma_p m p2 (g x)).
 194 intros.
 195 unfold sigma_p.
 196 apply (iter_p_gen2 n m p1 p2 nat g O plus)
 197 [ apply symmetricIntPlus
 198 | apply associative_plus
 199 | intros.
 200   apply sym_eq.
 201   apply plus_n_O
 202 ]
 203 qed.
 204
 205 theorem sigma_p2' :
 206 \forall n,m:nat.
 207 \forall p1:nat \to bool.
 208 \forall p2:nat \to nat \to bool.
 209 \forall g: nat \to nat \to nat.
 210 sigma_p (n*m)
 211   (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x  m)))
 212   (\lambda x.g (div x m) (mod x m)) =
 213 sigma_p n p1
 214   (\lambda x.sigma_p m (p2 x) (g x)).
 215 intros.
 216 unfold sigma_p.
 217 apply (iter_p_gen2' n m p1 p2 nat g O plus)
 218 [ apply symmetricIntPlus
 219 | apply associative_plus
 220 | intros.
 221   apply sym_eq.
 222   apply plus_n_O
 223 ]
 224 qed.
 225
 226 lemma sigma_p_gi: \forall g: nat \to nat.
 227 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
 228 sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
 229 intros.
 230 unfold sigma_p.
 231 apply (iter_p_gen_gi)
 232 [ apply symmetricIntPlus
 233 | apply associative_plus
 234 | intros.
 235   apply sym_eq.
 236   apply plus_n_O
 237 | assumption
 238 | assumption
 239 ]
 240 qed.
 241
 242 theorem eq_sigma_p_gh:
 243 \forall g,h,h1: nat \to nat.\forall n,n1.
 244 \forall p1,p2:nat \to bool.
 245 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
 246 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
 247 (\forall i. i < n \to p1 i = true \to h i < n1) \to
 248 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
 249 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
 250 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
 251 sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 p2 g.
 252 intros.
 253 unfold sigma_p.
 254 apply (eq_iter_p_gen_gh nat O plus ? ? ? g h h1 n n1 p1 p2)
 255 [ apply symmetricIntPlus
 256 | apply associative_plus
 257 | intros.
 258   apply sym_eq.
 259   apply plus_n_O
 260 | assumption
 261 | assumption
 262 | assumption
 263 | assumption
 264 | assumption
 265 | assumption
 266 ]
 267 qed.
 268
 269 theorem eq_sigma_p_pred:
 270 \forall n,p,g. p O = true \to
 271 sigma_p (S n) (\lambda i.p (pred i)) (\lambda i.g(pred i)) =
 272 plus (sigma_p n p g) (g O).
 273 intros.
 274 unfold sigma_p.
 275 apply eq_iter_p_gen_pred
 276   [assumption
 277   |apply symmetricIntPlus
 278   |apply associative_plus
 279   |intros.apply sym_eq.apply plus_n_O
 280   ]
 281 qed.
 282
 283 (* monotonicity *)
 284 theorem le_sigma_p:
 285 \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.
 286 (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to
 287 sigma_p n p g1 \le sigma_p n p g2.
 288 intros.
 289 generalize in match H.
 290 elim n
 291   [apply le_n.
 292   |apply (bool_elim ? (p n1));intros
 293     [rewrite > true_to_sigma_p_Sn
 294       [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
 295         [apply le_plus
 296           [apply H2[apply le_n|assumption]
 297           |apply H1.
 298            intros.
 299            apply H2[apply le_S.assumption|assumption]
 300           ]
 301         |assumption
 302         ]
 303       |assumption
 304       ]
 305     |rewrite > false_to_sigma_p_Sn
 306       [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
 307         [apply H1.
 308          intros.
 309          apply H2[apply le_S.assumption|assumption]
 310         |assumption
 311         ]
 312       |assumption
 313       ]
 314     ]
 315   ]
 316 qed.
 317
 318 (* a slightly more general result *)
 319 theorem le_sigma_p1:
 320 \forall n:nat. \forall p1,p2:nat \to bool. \forall g1,g2:nat \to nat.
 321 (\forall i. i < n \to
 322 bool_to_nat (p1 i)*(g1 i) \le bool_to_nat (p2 i)*g2 i) \to
 323 sigma_p n p1 g1 \le sigma_p n p2 g2.
 324 intros.
 325 generalize in match H.
 326 elim n
 327   [apply le_n.
 328   |apply (bool_elim ? (p1 n1));intros
 329     [apply (bool_elim ? (p2 n1));intros
 330       [rewrite > true_to_sigma_p_Sn
 331         [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
 332           [apply le_plus
 333             [lapply (H2 n1) as H5
 334               [rewrite > H3 in H5.
 335                rewrite > H4 in H5.
 336                simplify in H5.
 337                rewrite < plus_n_O in H5.
 338                rewrite < plus_n_O in H5.
 339                assumption
 340               |apply le_S_S.apply le_n
 341               ]
 342             |apply H1.intros.
 343              apply H2.apply le_S.assumption
 344             ]
 345           |assumption
 346           ]
 347         |assumption
 348         ]
 349       |rewrite > true_to_sigma_p_Sn
 350         [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
 351           [change in ⊢ (? ? %) with (O + sigma_p n1 p2 g2).
 352            apply le_plus
 353             [lapply (H2 n1) as H5
 354               [rewrite > H3 in H5.
 355                rewrite > H4 in H5.
 356                simplify in H5.
 357                rewrite < plus_n_O in H5.
 358                assumption
 359               |apply le_S_S.apply le_n
 360               ]
 361             |apply H1.intros.
 362              apply H2.apply le_S.assumption
 363             ]
 364           |assumption
 365           ]
 366         |assumption
 367         ]
 368       ]
 369     |apply (bool_elim ? (p2 n1));intros
 370       [rewrite > false_to_sigma_p_Sn
 371         [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
 372           [change in ⊢ (? % ?) with (O + sigma_p n1 p1 g1).
 373            apply le_plus
 374             [lapply (H2 n1) as H5
 375               [rewrite > H3 in H5.
 376                rewrite > H4 in H5.
 377                simplify in H5.
 378                rewrite < plus_n_O in H5.
 379                assumption
 380               |apply le_S_S.apply le_n
 381               ]
 382             |apply H1.intros.
 383              apply H2.apply le_S.assumption
 384             ]
 385           |assumption
 386           ]
 387         |assumption
 388         ]
 389       |rewrite > false_to_sigma_p_Sn
 390         [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
 391           [apply H1.intros.
 392            apply H2.apply le_S.assumption
 393           |assumption
 394           ]
 395         |assumption
 396         ]
 397       ]
 398     ]
 399   ]
 400 qed.
 401
 402 theorem lt_sigma_p:
 403 \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.
 404 (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to
 405 (\exists i. i < n \and (p i = true) \and (g1 i < g2 i)) \to
 406 sigma_p n p g1 < sigma_p n p g2.
 407 intros 4.
 408 elim n
 409   [elim H1.clear H1.
 410    elim H2.clear H2.
 411    elim H1.clear H1.
 412    apply False_ind.
 413    apply (lt_to_not_le ? ? H2).
 414    apply le_O_n
 415   |apply (bool_elim ? (p n1));intros
 416     [apply (bool_elim ? (leb (S (g1 n1)) (g2 n1)));intros
 417       [rewrite > true_to_sigma_p_Sn
 418         [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
 419           [change with
 420            (S (g1 n1)+sigma_p n1 p g1 \le g2 n1+sigma_p n1 p g2).
 421            apply le_plus
 422             [apply leb_true_to_le.assumption
 423             |apply le_sigma_p.intros.
 424              apply H1
 425               [apply lt_to_le.apply le_S_S.assumption
 426               |assumption
 427               ]
 428             ]
 429           |assumption
 430           ]
 431         |assumption
 432         ]
 433       |rewrite > true_to_sigma_p_Sn
 434         [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
 435           [unfold lt.
 436            rewrite > plus_n_Sm.
 437            apply le_plus
 438             [apply H1
 439               [apply le_n
 440               |assumption
 441               ]
 442             |apply H
 443               [intros.apply H1
 444                 [apply lt_to_le.apply le_S_S.assumption
 445                 |assumption
 446                 ]
 447               |elim H2.clear H2.
 448                elim H5.clear H5.
 449                elim H2.clear H2.
 450                apply (ex_intro ? ? a).
 451                split
 452                 [split
 453                   [elim (le_to_or_lt_eq a n1)
 454                     [assumption
 455                     |absurd (g1 a < g2 a)
 456                       [assumption
 457                       |apply leb_false_to_not_le.
 458                        rewrite > H2.
 459                        assumption
 460                       ]
 461                     |apply le_S_S_to_le.
 462                      assumption
 463                     ]
 464                   |assumption
 465                   ]
 466                 |assumption
 467                 ]
 468               ]
 469             ]
 470           |assumption
 471           ]
 472         |assumption
 473         ]
 474       ]
 475     |rewrite > false_to_sigma_p_Sn
 476       [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
 477         [apply H
 478           [intros.apply H1
 479             [apply lt_to_le.apply le_S_S.assumption
 480             |assumption
 481             ]
 482           |elim H2.clear H2.
 483            elim H4.clear H4.
 484            elim H2.clear H2.
 485            apply (ex_intro ? ? a).
 486            split
 487             [split
 488               [elim (le_to_or_lt_eq a n1)
 489                 [assumption
 490                 |apply False_ind.
 491                  apply not_eq_true_false.
 492                  rewrite < H6.
 493                  rewrite < H3.
 494                  rewrite < H2.
 495                  reflexivity
 496                 |apply le_S_S_to_le.
 497                  assumption
 498                 ]
 499               |assumption
 500               ]
 501             |assumption
 502             ]
 503           ]
 504         |assumption
 505         ]
 506       |assumption
 507       ]
 508     ]
 509   ]
 510 qed.
 511
 512 theorem sigma_p_divides:
 513 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
 514 \forall g: nat \to nat.
 515 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
 516 sigma_p (S n) (\lambda x.divides_b x n)
 517   (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
 518 intros.
 519 unfold sigma_p.
 520 apply (iter_p_gen_divides nat O plus n m p ? ? ? g)
 521 [ assumption
 522 | assumption
 523 | assumption
 524 | apply symmetricIntPlus
 525 | apply associative_plus
 526 | intros.
 527   apply sym_eq.
 528   apply plus_n_O
 529 ]
 530 qed.
 531
 532 theorem distributive_times_plus_sigma_p: \forall n,k:nat. \forall p:nat \to bool. \forall g:nat \to nat.
 533 k*(sigma_p n p g) = sigma_p n p (\lambda i:nat.k * (g i)).
 534 intros.
 535 apply (distributive_times_plus_iter_p_gen nat plus O times n k p g)
 536 [ apply symmetricIntPlus
 537 | apply associative_plus
 538 | intros.
 539   apply sym_eq.
 540   apply plus_n_O
 541 | apply symmetric_times
 542 | apply distributive_times_plus
 543 | intros.
 544   rewrite < (times_n_O a).
 545   reflexivity
 546 ]
 547 qed.
 548
 549 (*some properties of sigma_p invoked with an "always true" predicate (in this
 550   way sigma_p just counts the elements, without doing any control) or with
 551   the nat \to nat function which always returns (S O).
 552   It 's not easily possible proving these theorems in a general form
 553   in generic_sigma_p.ma
 554  *)
 555
 556 theorem sigma_p_true: \forall n:nat.
 557 (sigma_p n (\lambda x.true) (\lambda x.S O)) = n.
 558 intros.
 559 elim n
 560 [ simplify.
 561   reflexivity
 562 | rewrite > (true_to_sigma_p_Sn n1 (\lambda x:nat.true) (\lambda x:nat.S O))
 563   [ rewrite > H.
 564     simplify.
 565     reflexivity
 566   | reflexivity
 567   ]
 568 ]
 569 qed.
 570
 571 theorem sigma_P_SO_to_sigma_p_true: \forall n:nat. \forall g:nat \to bool.
 572 sigma_p n g (\lambda n:nat. (S O)) =
 573 sigma_p n (\lambda x:nat.true) (\lambda i:nat.bool_to_nat (g i)).
 574 intros.
 575 elim n
 576 [ simplify.
 577   reflexivity
 578 | cut ((g n1) = true \lor (g n1) = false)
 579   [ rewrite > true_to_sigma_p_Sn in \vdash (? ? ? %)
 580     [ elim Hcut
 581       [ rewrite > H1.
 582         rewrite > true_to_sigma_p_Sn in \vdash (? ? % ?)
 583         [ simplify.
 584           apply eq_f.
 585           assumption
 586         | assumption
 587         ]
 588       | rewrite > H1.
 589         rewrite > false_to_sigma_p_Sn in \vdash (? ? % ?)
 590         [ simplify.
 591           assumption
 592         | assumption
 593         ]
 594       ]
 595     | reflexivity
 596     ]
 597   | elim (g n1)
 598     [ left.
 599       reflexivity
 600     | right.
 601       reflexivity
 602     ]
 603   ]
 604 ]
 605 qed.
 606
 607 (* I introduce an equivalence in the form map_iter_i in order to use
 608  * the existing result about permutation in that part of the library.
 609  *)
 610
 611 theorem eq_map_iter_i_sigma_p_alwaysTrue:  \forall n:nat.\forall g:nat \to nat.
 612 map_iter_i n g plus O = sigma_p (S n) (\lambda c:nat.true) g.
 613 intros.
 614 elim n
 615 [ simplify.
 616   rewrite < plus_n_O.
 617   reflexivity
 618 | rewrite > true_to_sigma_p_Sn
 619   [ simplify in \vdash (? ? % ?).
 620     rewrite < plus_n_O.
 621     apply eq_f.
 622     assumption
 623   | reflexivity
 624   ]
 625 ]
 626 qed.
 627
 628 theorem sigma_p_plus_1: \forall n:nat. \forall f,g:nat \to nat.
 629 \forall p.
 630 sigma_p n p (\lambda a:nat.(f a) + (g a)) =
 631 sigma_p n p f + sigma_p n p g.
 632 intros.
 633 elim n
 634 [ simplify.
 635   reflexivity
 636 | apply (bool_elim ? (p n1)); intro;
 637   [ rewrite > true_to_sigma_p_Sn
 638     [ rewrite > (true_to_sigma_p_Sn n1 p f)
 639       [ rewrite > (true_to_sigma_p_Sn n1 p g)
 640         [ rewrite > assoc_plus in \vdash (? ? ? %).
 641           rewrite < assoc_plus in \vdash (? ? ? (? ? %)).
 642           rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))).
 643           rewrite > assoc_plus in \vdash (? ? ? (? ? %)).
 644           rewrite < assoc_plus in \vdash (? ? ? %).
 645           apply eq_f.
 646           assumption]]]
 647    assumption
 648  | rewrite > false_to_sigma_p_Sn
 649     [ rewrite > (false_to_sigma_p_Sn n1 p f)
 650       [ rewrite > (false_to_sigma_p_Sn n1 p g)
 651         [assumption]]]
 652    assumption
 653 ]]
 654 qed.
 655
 656 theorem eq_sigma_p_sigma_p_times1 : \forall n,m:nat.\forall f:nat \to nat.
 657 sigma_p (n*m) (\lambda x:nat.true) f =
 658 sigma_p m (\lambda x:nat.true)
 659     (\lambda a.(sigma_p n (\lambda x:nat.true) (\lambda b.f (b*m + a)))).
 660 intro.
 661 elim n
 662 [ simplify.
 663   elim m
 664   [ simplify.
 665     reflexivity
 666   | rewrite > true_to_sigma_p_Sn
 667     [ rewrite < H.
 668       reflexivity
 669     | reflexivity
 670     ]
 671   ]
 672 | change in \vdash (? ? ? (? ? ? (\lambda a:?.%))) with ((f ((n1*m)+a)) +
 673   (sigma_p n1 (\lambda x:nat.true) (\lambda b:nat.f (b*m +a)))).
 674   rewrite > sigma_p_plus_1 in \vdash (? ? ? %).
 675   rewrite > (sym_times (S n1) m).
 676   rewrite < (times_n_Sm m  n1).
 677   rewrite > sigma_p_plus in \vdash (? ? % ?).
 678   apply eq_f2
 679   [ rewrite < (sym_times m n1).
 680     apply eq_sigma_p
 681     [ intros.
 682       reflexivity
 683     | intros.
 684       rewrite < (sym_plus ? (m * n1)).
 685       reflexivity
 686     ]
 687   | rewrite > (sym_times m n1).
 688     apply H
 689   ]
 690 ]
 691 qed.
 692
 693 theorem eq_sigma_p_sigma_p_times2 : \forall n,m:nat.\forall f:nat \to nat.
 694 sigma_p (n *m) (\lambda c:nat.true) f =
 695 sigma_p  n (\lambda c:nat.true)
 696   (\lambda a.(sigma_p m (\lambda c:nat.true) (\lambda b:nat.f (b* n + a)))).
 697 intros.
 698 rewrite > sym_times.
 699 apply eq_sigma_p_sigma_p_times1.
 700 qed.
 701
 702 theorem sigma_p_times:\forall n,m:nat.
 703 \forall f,f1,f2:nat \to bool.
 704 \forall g:nat \to nat \to nat.
 705 \forall g1,g2: nat \to nat.
 706 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g b a) < (S n)*(S m)) \to
 707 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g1 (g b a)) = a) \to
 708 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g2 (g b a)) = b) \to
 709 (\forall a,b:nat. a < (S n) \to b < (S m) \to f (g b a) = andb (f2 b) (f1 a)) \to
 710 (sigma_p ((S n) * (S m)) f (\lambda c:nat.(S O))) =
 711 sigma_p (S n) f1 (\lambda c:nat.(S O)) * sigma_p (S m) f2 (\lambda c:nat.(S O)).
 712 intros.
 713
 714 rewrite > (sigma_P_SO_to_sigma_p_true ).
 715 rewrite > (S_pred ((S n)*(S m))) in \vdash (? ? (? % ? ?) ?)
 716 [ rewrite < (eq_map_iter_i_sigma_p_alwaysTrue (pred ((S n)* (S m)))).
 717   rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ?
 718            (\lambda i.g (div i (S n)) (mod i (S n))))
 719   [ rewrite > eq_map_iter_i_sigma_p_alwaysTrue.
 720     rewrite < S_pred
 721     [ rewrite > eq_sigma_p_sigma_p_times2.
 722       apply (trans_eq ? ? (sigma_p (S n)  (\lambda c:nat.true)
 723         (\lambda a. sigma_p (S m) (\lambda c:nat.true)
 724                 (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))))))
 725       [ apply eq_sigma_p;intros
 726         [ reflexivity
 727         | apply eq_sigma_p;intros
 728           [ reflexivity
 729           |
 730             rewrite > (div_mod_spec_to_eq (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
 731                                                   ((x1*(S n) + x) \mod (S n)) x1 x)
 732             [ rewrite > (div_mod_spec_to_eq2 (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
 733                                                   ((x1*(S n) + x) \mod (S n)) x1 x)
 734               [ rewrite > H3
 735                 [ apply bool_to_nat_andb
 736                 | assumption
 737                 | assumption
 738                 ]
 739               | apply div_mod_spec_div_mod.
 740                 apply lt_O_S
 741               | constructor 1
 742                 [ assumption
 743                 | reflexivity
 744                 ]
 745               ]
 746             | apply div_mod_spec_div_mod.
 747               apply lt_O_S
 748             | constructor 1
 749               [ assumption
 750               | reflexivity
 751               ]
 752             ]
 753           ]
 754         ]
 755       | apply (trans_eq ? ?
 756          (sigma_p (S n) (\lambda c:nat.true) (\lambda n.((bool_to_nat (f1 n)) *
 757          (sigma_p (S m) (\lambda c:nat.true) (\lambda n.bool_to_nat (f2 n)))))))
 758         [ apply eq_sigma_p;intros
 759           [ reflexivity
 760           | rewrite > distributive_times_plus_sigma_p.
 761             apply eq_sigma_p;intros
 762             [ reflexivity
 763             | rewrite > sym_times.
 764               reflexivity
 765             ]
 766           ]
 767         | apply sym_eq.
 768           rewrite > sigma_P_SO_to_sigma_p_true.
 769           rewrite > sigma_P_SO_to_sigma_p_true in \vdash (? ? (? ? %) ?).
 770           rewrite > sym_times.
 771           rewrite > distributive_times_plus_sigma_p.
 772           apply eq_sigma_p;intros
 773           [ reflexivity
 774           | rewrite > distributive_times_plus_sigma_p.
 775             rewrite < sym_times.
 776             rewrite > distributive_times_plus_sigma_p.
 777             apply eq_sigma_p;
 778               intros; reflexivity
 779           ]
 780         ]
 781       ]
 782     | apply lt_O_times_S_S
 783     ]
 784
 785   | unfold permut.
 786     split
 787     [ intros.
 788       rewrite < plus_n_O.
 789       apply le_S_S_to_le.
 790       rewrite < S_pred in \vdash (? ? %)
 791       [ change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
 792         apply H
 793         [ apply lt_mod_m_m.
 794           unfold lt.
 795           apply le_S_S.
 796           apply le_O_n
 797         | apply (lt_times_to_lt_l n).
 798           apply (le_to_lt_to_lt ? i)
 799           [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
 800             [ rewrite > sym_plus.
 801               apply le_plus_n
 802             | unfold lt.
 803               apply le_S_S.
 804               apply le_O_n
 805             ]
 806           | unfold lt.
 807             rewrite > S_pred in \vdash (? ? %)
 808             [ apply le_S_S.
 809               rewrite > plus_n_O in \vdash (? ? %).
 810               rewrite > sym_times.
 811               assumption
 812             | apply lt_O_times_S_S
 813             ]
 814           ]
 815         ]
 816       | apply lt_O_times_S_S
 817       ]
 818     | rewrite < plus_n_O.
 819       unfold injn.
 820       intros.
 821       cut (i < (S n)*(S m))
 822       [ cut (j < (S n)*(S m))
 823         [ cut ((i \mod (S n)) < (S n))
 824           [ cut ((i/(S n)) < (S m))
 825             [ cut ((j \mod (S n)) < (S n))
 826               [ cut ((j/(S n)) < (S m))
 827                 [ rewrite > (div_mod i (S n))
 828                   [ rewrite > (div_mod j (S n))
 829                     [ rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
 830                       rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
 831                       rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
 832                       rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
 833                       rewrite > H6.
 834                       reflexivity
 835                     | unfold lt.
 836                       apply le_S_S.
 837                       apply le_O_n
 838                     ]
 839                   | unfold lt.
 840                     apply le_S_S.
 841                     apply le_O_n
 842                   ]
 843                 | apply (lt_times_to_lt_l n).
 844                   apply (le_to_lt_to_lt ? j)
 845                   [ rewrite > (div_mod j (S n)) in \vdash (? ? %)
 846                     [ rewrite > sym_plus.
 847                       apply le_plus_n
 848                     | unfold lt. apply le_S_S.
 849                       apply le_O_n
 850                     ]
 851                   | rewrite < sym_times.
 852                     assumption
 853                   ]
 854                 ]
 855               | apply lt_mod_m_m.
 856                 unfold lt.
 857                 apply le_S_S.
 858                 apply le_O_n
 859               ]
 860             | apply (lt_times_to_lt_l n).
 861               apply (le_to_lt_to_lt ? i)
 862               [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
 863                 [ rewrite > sym_plus.
 864                   apply le_plus_n
 865                 | unfold lt.
 866                   apply le_S_S.
 867                   apply le_O_n
 868                 ]
 869               | rewrite < sym_times.
 870                 assumption
 871               ]
 872             ]
 873           | apply lt_mod_m_m.
 874             unfold lt.
 875             apply le_S_S.
 876             apply le_O_n
 877           ]
 878         | unfold lt.
 879           rewrite > S_pred in \vdash (? ? %)
 880           [ apply le_S_S.
 881             assumption
 882           | apply lt_O_times_S_S
 883           ]
 884         ]
 885       | unfold lt.
 886         rewrite > S_pred in \vdash (? ? %)
 887         [ apply le_S_S.
 888           assumption
 889         | apply lt_O_times_S_S
 890         ]
 891       ]
 892     ]
 893   | intros.
 894     apply False_ind.
 895     apply (not_le_Sn_O m1 H4)
 896   ]
 897 | apply lt_O_times_S_S
 898 ]
 899 qed.
 900
 901 theorem sigma_p_knm:
 902 \forall g: nat \to nat.
 903 \forall h2:nat \to nat \to nat.
 904 \forall h11,h12:nat \to nat.
 905 \forall k,n,m.
 906 \forall p1,p21:nat \to bool.
 907 \forall p22:nat \to nat \to bool.
 908 (\forall x. x < k \to p1 x = true \to
 909 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
 910 \land h2 (h11 x) (h12 x) = x
 911 \land (h11 x) < n \land (h12 x) < m) \to
 912 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
 913 p1 (h2 i j) = true \land
 914 h11 (h2 i j) = i \land h12 (h2 i j) = j
 915 \land h2 i j < k) \to
 916 sigma_p k p1 g=
 917 sigma_p n p21 (\lambda x:nat.sigma_p m (p22 x) (\lambda y. g (h2 x y))).
 918 intros.
 919 unfold sigma_p.
 920 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
 921 apply iter_p_gen_knm
 922   [apply symmetricIntPlus
 923   |apply associative_plus
 924   |intro.rewrite < plus_n_O.reflexivity
 925   |exact h11
 926   |exact h12
 927   |assumption
 928   |assumption
 929   ]
 930 qed.
 931
 932
 933 theorem sigma_p2_eq:
 934 \forall g: nat \to nat \to nat.
 935 \forall h11,h12,h21,h22: nat \to nat \to nat.
 936 \forall n1,m1,n2,m2.
 937 \forall p11,p21:nat \to bool.
 938 \forall p12,p22:nat \to nat \to bool.
 939 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
 940 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
 941 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
 942 \land h11 i j < n1 \land h12 i j < m1) \to
 943 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
 944 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
 945 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
 946 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
 947 sigma_p n1 p11 (\lambda x:nat .sigma_p m1 (p12 x) (\lambda y. g x y)) =
 948 sigma_p n2 p21 (\lambda x:nat .sigma_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
 949 intros.
 950 unfold sigma_p.
 951 unfold sigma_p in \vdash (? ? (? ? ? ? (\lambda x:?.%) ? ?) ?).
 952 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
 953
 954 apply(iter_p_gen_2_eq nat O plus ? ? ? g h11 h12 h21 h22 n1 m1 n2 m2 p11 p21 p12 p22)
 955 [ apply symmetricIntPlus
 956 | apply associative_plus
 957 | intro.
 958   rewrite < (plus_n_O).
 959   reflexivity
 960 | assumption
 961 | assumption
 962 ]
 963 qed.
 964
 965 theorem sigma_p_sigma_p:
 966 \forall g: nat \to nat \to nat.
 967 \forall n,m.
 968 \forall p11,p21:nat \to bool.
 969 \forall p12,p22:nat \to nat \to bool.
 970 (\forall x,y. x < n \to y < m \to
 971  (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
 972 sigma_p n p11 (\lambda x:nat.sigma_p m (p12 x) (\lambda y. g x y)) =
 973 sigma_p m p21 (\lambda y:nat.sigma_p n (p22 y) (\lambda x. g x y)).
 974 intros.
 975 unfold sigma_p.unfold sigma_p.
 976 apply (iter_p_gen_iter_p_gen ? ? ? sym_plus assoc_plus)
 977   [intros.apply sym_eq.apply plus_n_O.
 978   |assumption
 979   ]
 980 qed.