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