helm/software/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 elim n in H ⊢ %
 290   [apply le_n.
 291   |apply (bool_elim ? (p n1));intros
 292     [rewrite > true_to_sigma_p_Sn
 293       [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
 294         [apply le_plus
 295           [apply H1[apply le_n|assumption]
 296           |apply H.
 297            intros.
 298            apply H1[apply le_S.assumption|assumption]
 299           ]
 300         |assumption
 301         ]
 302       |assumption
 303       ]
 304     |rewrite > false_to_sigma_p_Sn
 305       [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
 306         [apply H.
 307          intros.
 308          apply H1[apply le_S.assumption|assumption]
 309         |assumption
 310         ]
 311       |assumption
 312       ]
 313     ]
 314   ]
 315 qed.
 316
 317 (* a slightly more general result *)
 318 theorem le_sigma_p1:
 319 \forall n:nat. \forall p1,p2:nat \to bool. \forall g1,g2:nat \to nat.
 320 (\forall i. i < n \to
 321 bool_to_nat (p1 i)*(g1 i) \le bool_to_nat (p2 i)*g2 i) \to
 322 sigma_p n p1 g1 \le sigma_p n p2 g2.
 323 intros.
 324 elim n in H ⊢ %
 325   [apply le_n.
 326   |apply (bool_elim ? (p1 n1));intros
 327     [apply (bool_elim ? (p2 n1));intros
 328       [rewrite > true_to_sigma_p_Sn
 329         [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
 330           [apply le_plus
 331             [lapply (H1 n1) as H5
 332               [rewrite > H2 in H5.
 333                rewrite > H3 in H5.
 334                simplify in H5.
 335                rewrite < plus_n_O in H5.
 336                rewrite < plus_n_O in H5.
 337                assumption
 338               |apply le_S_S.apply le_n
 339               ]
 340             |apply H.intros.
 341              apply H1.apply le_S.assumption
 342             ]
 343           |assumption
 344           ]
 345         |assumption
 346         ]
 347       |rewrite > true_to_sigma_p_Sn
 348         [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
 349           [change in ⊢ (? ? %) with (O + sigma_p n1 p2 g2).
 350            apply le_plus
 351             [lapply (H1 n1) as H5
 352               [rewrite > H2 in H5.
 353                rewrite > H3 in H5.
 354                simplify in H5.
 355                rewrite < plus_n_O in H5.
 356                assumption
 357               |apply le_S_S.apply le_n
 358               ]
 359             |apply H.intros.
 360              apply H1.apply le_S.assumption
 361             ]
 362           |assumption
 363           ]
 364         |assumption
 365         ]
 366       ]
 367     |apply (bool_elim ? (p2 n1));intros
 368       [rewrite > false_to_sigma_p_Sn
 369         [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
 370           [change in ⊢ (? % ?) with (O + sigma_p n1 p1 g1).
 371            apply le_plus
 372             [lapply (H1 n1) as H5
 373               [rewrite > H2 in H5.
 374                rewrite > H3 in H5.
 375                simplify in H5.
 376                rewrite < plus_n_O in H5.
 377                assumption
 378               |apply le_S_S.apply le_n
 379               ]
 380             |apply H.intros.
 381              apply H1.apply le_S.assumption
 382             ]
 383           |assumption
 384           ]
 385         |assumption
 386         ]
 387       |rewrite > false_to_sigma_p_Sn
 388         [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
 389           [apply H.intros.
 390            apply H1.apply le_S.assumption
 391           |assumption
 392           ]
 393         |assumption
 394         ]
 395       ]
 396     ]
 397   ]
 398 qed.
 399
 400 theorem lt_sigma_p:
 401 \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.
 402 (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to
 403 (\exists i. i < n \and (p i = true) \and (g1 i < g2 i)) \to
 404 sigma_p n p g1 < sigma_p n p g2.
 405 intros 4.
 406 elim n
 407   [elim H1.clear H1.
 408    elim H2.clear H2.
 409    elim H1.clear H1.
 410    apply False_ind.
 411    apply (lt_to_not_le ? ? H2).
 412    apply le_O_n
 413   |apply (bool_elim ? (p n1));intros
 414     [apply (bool_elim ? (leb (S (g1 n1)) (g2 n1)));intros
 415       [rewrite > true_to_sigma_p_Sn
 416         [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
 417           [change with
 418            (S (g1 n1)+sigma_p n1 p g1 \le g2 n1+sigma_p n1 p g2).
 419            apply le_plus
 420             [apply leb_true_to_le.assumption
 421             |apply le_sigma_p.intros.
 422              apply H1
 423               [apply lt_to_le.apply le_S_S.assumption
 424               |assumption
 425               ]
 426             ]
 427           |assumption
 428           ]
 429         |assumption
 430         ]
 431       |rewrite > true_to_sigma_p_Sn
 432         [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
 433           [unfold lt.
 434            rewrite > plus_n_Sm.
 435            apply le_plus
 436             [apply H1
 437               [apply le_n
 438               |assumption
 439               ]
 440             |apply H
 441               [intros.apply H1
 442                 [apply lt_to_le.apply le_S_S.assumption
 443                 |assumption
 444                 ]
 445               |elim H2.clear H2.
 446                elim H5.clear H5.
 447                elim H2.clear H2.
 448                apply (ex_intro ? ? a).
 449                split
 450                 [split
 451                   [elim (le_to_or_lt_eq a n1)
 452                     [assumption
 453                     |absurd (g1 a < g2 a)
 454                       [assumption
 455                       |apply leb_false_to_not_le.
 456                        rewrite > H2.
 457                        assumption
 458                       ]
 459                     |apply le_S_S_to_le.
 460                      assumption
 461                     ]
 462                   |assumption
 463                   ]
 464                 |assumption
 465                 ]
 466               ]
 467             ]
 468           |assumption
 469           ]
 470         |assumption
 471         ]
 472       ]
 473     |rewrite > false_to_sigma_p_Sn
 474       [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
 475         [apply H
 476           [intros.apply H1
 477             [apply lt_to_le.apply le_S_S.assumption
 478             |assumption
 479             ]
 480           |elim H2.clear H2.
 481            elim H4.clear H4.
 482            elim H2.clear H2.
 483            apply (ex_intro ? ? a).
 484            split
 485             [split
 486               [elim (le_to_or_lt_eq a n1)
 487                 [assumption
 488                 |apply False_ind.
 489                  apply not_eq_true_false.
 490                  rewrite < H6.
 491                  rewrite < H3.
 492                  rewrite < H2.
 493                  reflexivity
 494                 |apply le_S_S_to_le.
 495                  assumption
 496                 ]
 497               |assumption
 498               ]
 499             |assumption
 500             ]
 501           ]
 502         |assumption
 503         ]
 504       |assumption
 505       ]
 506     ]
 507   ]
 508 qed.
 509
 510 theorem sigma_p_divides:
 511 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
 512 \forall g: nat \to nat.
 513 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
 514 sigma_p (S n) (\lambda x.divides_b x n)
 515   (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
 516 intros.
 517 unfold sigma_p.
 518 apply (iter_p_gen_divides nat O plus n m p ? ? ? g)
 519 [ assumption
 520 | assumption
 521 | assumption
 522 | apply symmetricIntPlus
 523 | apply associative_plus
 524 | intros.
 525   apply sym_eq.
 526   apply plus_n_O
 527 ]
 528 qed.
 529
 530 theorem distributive_times_plus_sigma_p: \forall n,k:nat. \forall p:nat \to bool. \forall g:nat \to nat.
 531 k*(sigma_p n p g) = sigma_p n p (\lambda i:nat.k * (g i)).
 532 intros.
 533 apply (distributive_times_plus_iter_p_gen nat plus O times n k p g)
 534 [ apply symmetricIntPlus
 535 | apply associative_plus
 536 | intros.
 537   apply sym_eq.
 538   apply plus_n_O
 539 | apply symmetric_times
 540 | apply distributive_times_plus
 541 | intros.
 542   rewrite < (times_n_O a).
 543   reflexivity
 544 ]
 545 qed.
 546
 547 (*some properties of sigma_p invoked with an "always true" predicate (in this
 548   way sigma_p just counts the elements, without doing any control) or with
 549   the nat \to nat function which always returns (S O).
 550   It 's not easily possible proving these theorems in a general form
 551   in generic_sigma_p.ma
 552  *)
 553
 554 theorem sigma_p_true: \forall n:nat.
 555 (sigma_p n (\lambda x.true) (\lambda x.S O)) = n.
 556 intros.
 557 elim n
 558 [ simplify.
 559   reflexivity
 560 | rewrite > (true_to_sigma_p_Sn n1 (\lambda x:nat.true) (\lambda x:nat.S O))
 561   [ rewrite > H.
 562     simplify.
 563     reflexivity
 564   | reflexivity
 565   ]
 566 ]
 567 qed.
 568
 569 theorem sigma_P_SO_to_sigma_p_true: \forall n:nat. \forall g:nat \to bool.
 570 sigma_p n g (\lambda n:nat. (S O)) =
 571 sigma_p n (\lambda x:nat.true) (\lambda i:nat.bool_to_nat (g i)).
 572 intros.
 573 elim n
 574 [ simplify.
 575   reflexivity
 576 | cut ((g n1) = true \lor (g n1) = false)
 577   [ rewrite > true_to_sigma_p_Sn in \vdash (? ? ? %)
 578     [ elim Hcut
 579       [ rewrite > H1.
 580         rewrite > true_to_sigma_p_Sn in \vdash (? ? % ?)
 581         [ simplify.
 582           apply eq_f.
 583           assumption
 584         | assumption
 585         ]
 586       | rewrite > H1.
 587         rewrite > false_to_sigma_p_Sn in \vdash (? ? % ?)
 588         [ simplify.
 589           assumption
 590         | assumption
 591         ]
 592       ]
 593     | reflexivity
 594     ]
 595   | elim (g n1)
 596     [ left.
 597       reflexivity
 598     | right.
 599       reflexivity
 600     ]
 601   ]
 602 ]
 603 qed.
 604
 605 (* I introduce an equivalence in the form map_iter_i in order to use
 606  * the existing result about permutation in that part of the library.
 607  *)
 608
 609 theorem eq_map_iter_i_sigma_p_alwaysTrue:  \forall n:nat.\forall g:nat \to nat.
 610 map_iter_i n g plus O = sigma_p (S n) (\lambda c:nat.true) g.
 611 intros.
 612 elim n
 613 [ simplify.
 614   rewrite < plus_n_O.
 615   reflexivity
 616 | rewrite > true_to_sigma_p_Sn
 617   [ simplify in \vdash (? ? % ?).
 618     rewrite < plus_n_O.
 619     apply eq_f.
 620     assumption
 621   | reflexivity
 622   ]
 623 ]
 624 qed.
 625
 626 theorem sigma_p_plus_1: \forall n:nat. \forall f,g:nat \to nat.
 627 \forall p.
 628 sigma_p n p (\lambda a:nat.(f a) + (g a)) =
 629 sigma_p n p f + sigma_p n p g.
 630 intros.
 631 elim n
 632 [ simplify.
 633   reflexivity
 634 | apply (bool_elim ? (p n1)); intro;
 635   [ rewrite > true_to_sigma_p_Sn
 636     [ rewrite > (true_to_sigma_p_Sn n1 p f)
 637       [ rewrite > (true_to_sigma_p_Sn n1 p g)
 638         [ rewrite > assoc_plus in \vdash (? ? ? %).
 639           rewrite < assoc_plus in \vdash (? ? ? (? ? %)).
 640           rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))).
 641           rewrite > assoc_plus in \vdash (? ? ? (? ? %)).
 642           rewrite < assoc_plus in \vdash (? ? ? %).
 643           apply eq_f.
 644           assumption]]]
 645    assumption
 646  | rewrite > false_to_sigma_p_Sn
 647     [ rewrite > (false_to_sigma_p_Sn n1 p f)
 648       [ rewrite > (false_to_sigma_p_Sn n1 p g)
 649         [assumption]]]
 650    assumption
 651 ]]
 652 qed.
 653
 654 theorem eq_sigma_p_sigma_p_times1 : \forall n,m:nat.\forall f:nat \to nat.
 655 sigma_p (n*m) (\lambda x:nat.true) f =
 656 sigma_p m (\lambda x:nat.true)
 657     (\lambda a.(sigma_p n (\lambda x:nat.true) (\lambda b.f (b*m + a)))).
 658 intro.
 659 elim n
 660 [ simplify.
 661   elim m
 662   [ simplify.
 663     reflexivity
 664   | rewrite > true_to_sigma_p_Sn
 665     [ rewrite < H.
 666       reflexivity
 667     | reflexivity
 668     ]
 669   ]
 670 | change in \vdash (? ? ? (? ? ? (\lambda a:?.%))) with ((f ((n1*m)+a)) +
 671   (sigma_p n1 (\lambda x:nat.true) (\lambda b:nat.f (b*m +a)))).
 672   rewrite > sigma_p_plus_1 in \vdash (? ? ? %).
 673   rewrite > (sym_times (S n1) m).
 674   rewrite < (times_n_Sm m  n1).
 675   rewrite > sigma_p_plus in \vdash (? ? % ?).
 676   apply eq_f2
 677   [ rewrite < (sym_times m n1).
 678     apply eq_sigma_p
 679     [ intros.
 680       reflexivity
 681     | intros.
 682       rewrite < (sym_plus ? (m * n1)).
 683       reflexivity
 684     ]
 685   | rewrite > (sym_times m n1).
 686     apply H
 687   ]
 688 ]
 689 qed.
 690
 691 theorem eq_sigma_p_sigma_p_times2 : \forall n,m:nat.\forall f:nat \to nat.
 692 sigma_p (n *m) (\lambda c:nat.true) f =
 693 sigma_p  n (\lambda c:nat.true)
 694   (\lambda a.(sigma_p m (\lambda c:nat.true) (\lambda b:nat.f (b* n + a)))).
 695 intros.
 696 rewrite > sym_times.
 697 apply eq_sigma_p_sigma_p_times1.
 698 qed.
 699
 700 theorem sigma_p_times:\forall n,m:nat.
 701 \forall f,f1,f2:nat \to bool.
 702 \forall g:nat \to nat \to nat.
 703 \forall g1,g2: nat \to nat.
 704 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g b a) < (S n)*(S m)) \to
 705 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g1 (g b a)) = a) \to
 706 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g2 (g b a)) = b) \to
 707 (\forall a,b:nat. a < (S n) \to b < (S m) \to f (g b a) = andb (f2 b) (f1 a)) \to
 708 (sigma_p ((S n) * (S m)) f (\lambda c:nat.(S O))) =
 709 sigma_p (S n) f1 (\lambda c:nat.(S O)) * sigma_p (S m) f2 (\lambda c:nat.(S O)).
 710 intros.
 711
 712 rewrite > (sigma_P_SO_to_sigma_p_true ).
 713 rewrite > (S_pred ((S n)*(S m))) in \vdash (? ? (? % ? ?) ?)
 714 [ rewrite < (eq_map_iter_i_sigma_p_alwaysTrue (pred ((S n)* (S m)))).
 715   rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ?
 716            (\lambda i.g (div i (S n)) (mod i (S n))))
 717   [ rewrite > eq_map_iter_i_sigma_p_alwaysTrue.
 718     rewrite < S_pred
 719     [ rewrite > eq_sigma_p_sigma_p_times2.
 720       apply (trans_eq ? ? (sigma_p (S n)  (\lambda c:nat.true)
 721         (\lambda a. sigma_p (S m) (\lambda c:nat.true)
 722                 (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))))))
 723       [ apply eq_sigma_p;intros
 724         [ reflexivity
 725         | apply eq_sigma_p;intros
 726           [ reflexivity
 727           |
 728             rewrite > (div_mod_spec_to_eq (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
 729                                                   ((x1*(S n) + x) \mod (S n)) x1 x)
 730             [ rewrite > (div_mod_spec_to_eq2 (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
 731                                                   ((x1*(S n) + x) \mod (S n)) x1 x)
 732               [ rewrite > H3
 733                 [ apply bool_to_nat_andb
 734                 | assumption
 735                 | assumption
 736                 ]
 737               | apply div_mod_spec_div_mod.
 738                 apply lt_O_S
 739               | constructor 1
 740                 [ assumption
 741                 | reflexivity
 742                 ]
 743               ]
 744             | apply div_mod_spec_div_mod.
 745               apply lt_O_S
 746             | constructor 1
 747               [ assumption
 748               | reflexivity
 749               ]
 750             ]
 751           ]
 752         ]
 753       | apply (trans_eq ? ?
 754          (sigma_p (S n) (\lambda c:nat.true) (\lambda n.((bool_to_nat (f1 n)) *
 755          (sigma_p (S m) (\lambda c:nat.true) (\lambda n.bool_to_nat (f2 n)))))))
 756         [ apply eq_sigma_p;intros
 757           [ reflexivity
 758           | rewrite > distributive_times_plus_sigma_p.
 759             apply eq_sigma_p;intros
 760             [ reflexivity
 761             | rewrite > sym_times.
 762               reflexivity
 763             ]
 764           ]
 765         | apply sym_eq.
 766           rewrite > sigma_P_SO_to_sigma_p_true.
 767           rewrite > sigma_P_SO_to_sigma_p_true in \vdash (? ? (? ? %) ?).
 768           rewrite > sym_times.
 769           rewrite > distributive_times_plus_sigma_p.
 770           apply eq_sigma_p;intros
 771           [ reflexivity
 772           | rewrite > distributive_times_plus_sigma_p.
 773             rewrite < sym_times.
 774             rewrite > distributive_times_plus_sigma_p.
 775             apply eq_sigma_p;
 776               intros; reflexivity
 777           ]
 778         ]
 779       ]
 780     | apply lt_O_times_S_S
 781     ]
 782
 783   | unfold permut.
 784     split
 785     [ intros.
 786       rewrite < plus_n_O.
 787       apply le_S_S_to_le.
 788       rewrite < S_pred in \vdash (? ? %)
 789       [ change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
 790         apply H
 791         [ apply lt_mod_m_m.
 792           unfold lt.
 793           apply le_S_S.
 794           apply le_O_n
 795         | apply (lt_times_to_lt_l n).
 796           apply (le_to_lt_to_lt ? i)
 797           [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
 798             [ rewrite > sym_plus.
 799               apply le_plus_n
 800             | unfold lt.
 801               apply le_S_S.
 802               apply le_O_n
 803             ]
 804           | unfold lt.
 805             rewrite > S_pred in \vdash (? ? %)
 806             [ apply le_S_S.
 807               rewrite > plus_n_O in \vdash (? ? %).
 808               rewrite > sym_times.
 809               assumption
 810             | apply lt_O_times_S_S
 811             ]
 812           ]
 813         ]
 814       | apply lt_O_times_S_S
 815       ]
 816     | rewrite < plus_n_O.
 817       unfold injn.
 818       intros.
 819       cut (i < (S n)*(S m))
 820       [ cut (j < (S n)*(S m))
 821         [ cut ((i \mod (S n)) < (S n))
 822           [ cut ((i/(S n)) < (S m))
 823             [ cut ((j \mod (S n)) < (S n))
 824               [ cut ((j/(S n)) < (S m))
 825                 [ rewrite > (div_mod i (S n))
 826                   [ rewrite > (div_mod j (S n))
 827                     [ rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
 828                       rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
 829                       rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
 830                       rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
 831                       rewrite > H6.
 832                       reflexivity
 833                     | unfold lt.
 834                       apply le_S_S.
 835                       apply le_O_n
 836                     ]
 837                   | unfold lt.
 838                     apply le_S_S.
 839                     apply le_O_n
 840                   ]
 841                 | apply (lt_times_to_lt_l n).
 842                   apply (le_to_lt_to_lt ? j)
 843                   [ rewrite > (div_mod j (S n)) in \vdash (? ? %)
 844                     [ rewrite > sym_plus.
 845                       apply le_plus_n
 846                     | unfold lt. apply le_S_S.
 847                       apply le_O_n
 848                     ]
 849                   | rewrite < sym_times.
 850                     assumption
 851                   ]
 852                 ]
 853               | apply lt_mod_m_m.
 854                 unfold lt.
 855                 apply le_S_S.
 856                 apply le_O_n
 857               ]
 858             | apply (lt_times_to_lt_l n).
 859               apply (le_to_lt_to_lt ? i)
 860               [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
 861                 [ rewrite > sym_plus.
 862                   apply le_plus_n
 863                 | unfold lt.
 864                   apply le_S_S.
 865                   apply le_O_n
 866                 ]
 867               | rewrite < sym_times.
 868                 assumption
 869               ]
 870             ]
 871           | apply lt_mod_m_m.
 872             unfold lt.
 873             apply le_S_S.
 874             apply le_O_n
 875           ]
 876         | unfold lt.
 877           rewrite > S_pred in \vdash (? ? %)
 878           [ apply le_S_S.
 879             assumption
 880           | apply lt_O_times_S_S
 881           ]
 882         ]
 883       | unfold lt.
 884         rewrite > S_pred in \vdash (? ? %)
 885         [ apply le_S_S.
 886           assumption
 887         | apply lt_O_times_S_S
 888         ]
 889       ]
 890     ]
 891   | intros.
 892     apply False_ind.
 893     apply (not_le_Sn_O m1 H4)
 894   ]
 895 | apply lt_O_times_S_S
 896 ]
 897 qed.
 898
 899 theorem sigma_p_knm:
 900 \forall g: nat \to nat.
 901 \forall h2:nat \to nat \to nat.
 902 \forall h11,h12:nat \to nat.
 903 \forall k,n,m.
 904 \forall p1,p21:nat \to bool.
 905 \forall p22:nat \to nat \to bool.
 906 (\forall x. x < k \to p1 x = true \to
 907 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
 908 \land h2 (h11 x) (h12 x) = x
 909 \land (h11 x) < n \land (h12 x) < m) \to
 910 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
 911 p1 (h2 i j) = true \land
 912 h11 (h2 i j) = i \land h12 (h2 i j) = j
 913 \land h2 i j < k) \to
 914 sigma_p k p1 g=
 915 sigma_p n p21 (\lambda x:nat.sigma_p m (p22 x) (\lambda y. g (h2 x y))).
 916 intros.
 917 unfold sigma_p.
 918 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
 919 apply iter_p_gen_knm
 920   [apply symmetricIntPlus
 921   |apply associative_plus
 922   |intro.rewrite < plus_n_O.reflexivity
 923   |exact h11
 924   |exact h12
 925   |assumption
 926   |assumption
 927   ]
 928 qed.
 929
 930
 931 theorem sigma_p2_eq:
 932 \forall g: nat \to nat \to nat.
 933 \forall h11,h12,h21,h22: nat \to nat \to nat.
 934 \forall n1,m1,n2,m2.
 935 \forall p11,p21:nat \to bool.
 936 \forall p12,p22:nat \to nat \to bool.
 937 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
 938 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
 939 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
 940 \land h11 i j < n1 \land h12 i j < m1) \to
 941 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
 942 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
 943 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
 944 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
 945 sigma_p n1 p11 (\lambda x:nat .sigma_p m1 (p12 x) (\lambda y. g x y)) =
 946 sigma_p n2 p21 (\lambda x:nat .sigma_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
 947 intros.
 948 unfold sigma_p.
 949 unfold sigma_p in \vdash (? ? (? ? ? ? (\lambda x:?.%) ? ?) ?).
 950 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
 951
 952 apply(iter_p_gen_2_eq nat O plus ? ? ? g h11 h12 h21 h22 n1 m1 n2 m2 p11 p21 p12 p22)
 953 [ apply symmetricIntPlus
 954 | apply associative_plus
 955 | intro.
 956   rewrite < (plus_n_O).
 957   reflexivity
 958 | assumption
 959 | assumption
 960 ]
 961 qed.
 962
 963 theorem sigma_p_sigma_p:
 964 \forall g: nat \to nat \to nat.
 965 \forall n,m.
 966 \forall p11,p21:nat \to bool.
 967 \forall p12,p22:nat \to nat \to bool.
 968 (\forall x,y. x < n \to y < m \to
 969  (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
 970 sigma_p n p11 (\lambda x:nat.sigma_p m (p12 x) (\lambda y. g x y)) =
 971 sigma_p m p21 (\lambda y:nat.sigma_p n (p22 y) (\lambda x. g x y)).
 972 intros.
 973 unfold sigma_p.unfold sigma_p.
 974 apply (iter_p_gen_iter_p_gen ? ? ? sym_plus assoc_plus)
 975   [intros.apply sym_eq.apply plus_n_O.
 976   |assumption
 977   ]
 978 qed.