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 set "baseuri" "cic:/matita/nat/iteration2".
  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 sigma_p2 :
 111 \forall n,m:nat.
 112 \forall p1,p2:nat \to bool.
 113 \forall g: nat \to nat \to nat.
 114 sigma_p (n*m)
 115   (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
 116   (\lambda x.g (div x m) (mod x m)) =
 117 sigma_p n p1
 118   (\lambda x.sigma_p m p2 (g x)).
 119 intros.
 120 unfold sigma_p.
 121 apply (iter_p_gen2 n m p1 p2 nat g O plus)
 122 [ apply symmetricIntPlus
 123 | apply associative_plus
 124 | intros.
 125   apply sym_eq.
 126   apply plus_n_O
 127 ]
 128 qed.
 129
 130 theorem sigma_p2' :
 131 \forall n,m:nat.
 132 \forall p1:nat \to bool.
 133 \forall p2:nat \to nat \to bool.
 134 \forall g: nat \to nat \to nat.
 135 sigma_p (n*m)
 136   (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x  m)))
 137   (\lambda x.g (div x m) (mod x m)) =
 138 sigma_p n p1
 139   (\lambda x.sigma_p m (p2 x) (g x)).
 140 intros.
 141 unfold sigma_p.
 142 apply (iter_p_gen2' n m p1 p2 nat g O plus)
 143 [ apply symmetricIntPlus
 144 | apply associative_plus
 145 | intros.
 146   apply sym_eq.
 147   apply plus_n_O
 148 ]
 149 qed.
 150
 151 lemma sigma_p_gi: \forall g: nat \to nat.
 152 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
 153 sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
 154 intros.
 155 unfold sigma_p.
 156 apply (iter_p_gen_gi)
 157 [ apply symmetricIntPlus
 158 | apply associative_plus
 159 | intros.
 160   apply sym_eq.
 161   apply plus_n_O
 162 | assumption
 163 | assumption
 164 ]
 165 qed.
 166
 167 theorem eq_sigma_p_gh:
 168 \forall g,h,h1: nat \to nat.\forall n,n1.
 169 \forall p1,p2:nat \to bool.
 170 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
 171 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
 172 (\forall i. i < n \to p1 i = true \to h i < n1) \to
 173 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
 174 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
 175 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
 176 sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 p2 g.
 177 intros.
 178 unfold sigma_p.
 179 apply (eq_iter_p_gen_gh nat O plus ? ? ? g h h1 n n1 p1 p2)
 180 [ apply symmetricIntPlus
 181 | apply associative_plus
 182 | intros.
 183   apply sym_eq.
 184   apply plus_n_O
 185 | assumption
 186 | assumption
 187 | assumption
 188 | assumption
 189 | assumption
 190 | assumption
 191 ]
 192 qed.
 193
 194 (* monotonicity *)
 195 theorem le_sigma_p:
 196 \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.
 197 (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to
 198 sigma_p n p g1 \le sigma_p n p g2.
 199 intros.
 200 generalize in match H.
 201 elim n
 202   [apply le_n.
 203   |apply (bool_elim ? (p n1));intros
 204     [rewrite > true_to_sigma_p_Sn
 205       [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
 206         [apply le_plus
 207           [apply H2[apply le_n|assumption]
 208           |apply H1.
 209            intros.
 210            apply H2[apply le_S.assumption|assumption]
 211           ]
 212         |assumption
 213         ]
 214       |assumption
 215       ]
 216     |rewrite > false_to_sigma_p_Sn
 217       [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
 218         [apply H1.
 219          intros.
 220          apply H2[apply le_S.assumption|assumption]
 221         |assumption
 222         ]
 223       |assumption
 224       ]
 225     ]
 226   ]
 227 qed.
 228
 229 theorem lt_sigma_p:
 230 \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.
 231 (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to
 232 (\exists i. i < n \and (p i = true) \and (g1 i < g2 i)) \to
 233 sigma_p n p g1 < sigma_p n p g2.
 234 intros 4.
 235 elim n
 236   [elim H1.clear H1.
 237    elim H2.clear H2.
 238    elim H1.clear H1.
 239    apply False_ind.
 240    apply (lt_to_not_le ? ? H2).
 241    apply le_O_n
 242   |apply (bool_elim ? (p n1));intros
 243     [apply (bool_elim ? (leb (S (g1 n1)) (g2 n1)));intros
 244       [rewrite > true_to_sigma_p_Sn
 245         [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
 246           [change with
 247            (S (g1 n1)+sigma_p n1 p g1 \le g2 n1+sigma_p n1 p g2).
 248            apply le_plus
 249             [apply leb_true_to_le.assumption
 250             |apply le_sigma_p.intros.
 251              apply H1
 252               [apply lt_to_le.apply le_S_S.assumption
 253               |assumption
 254               ]
 255             ]
 256           |assumption
 257           ]
 258         |assumption
 259         ]
 260       |rewrite > true_to_sigma_p_Sn
 261         [rewrite > true_to_sigma_p_Sn in ⊢ (? ? %)
 262           [unfold lt.
 263            rewrite > plus_n_Sm.
 264            apply le_plus
 265             [apply H1
 266               [apply le_n
 267               |assumption
 268               ]
 269             |apply H
 270               [intros.apply H1
 271                 [apply lt_to_le.apply le_S_S.assumption
 272                 |assumption
 273                 ]
 274               |elim H2.clear H2.
 275                elim H5.clear H5.
 276                elim H2.clear H2.
 277                apply (ex_intro ? ? a).
 278                split
 279                 [split
 280                   [elim (le_to_or_lt_eq a n1)
 281                     [assumption
 282                     |absurd (g1 a < g2 a)
 283                       [assumption
 284                       |apply leb_false_to_not_le.
 285                        rewrite > H2.
 286                        assumption
 287                       ]
 288                     |apply le_S_S_to_le.
 289                      assumption
 290                     ]
 291                   |assumption
 292                   ]
 293                 |assumption
 294                 ]
 295               ]
 296             ]
 297           |assumption
 298           ]
 299         |assumption
 300         ]
 301       ]
 302     |rewrite > false_to_sigma_p_Sn
 303       [rewrite > false_to_sigma_p_Sn in ⊢ (? ? %)
 304         [apply H
 305           [intros.apply H1
 306             [apply lt_to_le.apply le_S_S.assumption
 307             |assumption
 308             ]
 309           |elim H2.clear H2.
 310            elim H4.clear H4.
 311            elim H2.clear H2.
 312            apply (ex_intro ? ? a).
 313            split
 314             [split
 315               [elim (le_to_or_lt_eq a n1)
 316                 [assumption
 317                 |apply False_ind.
 318                  apply not_eq_true_false.
 319                  rewrite < H6.
 320                  rewrite < H3.
 321                  rewrite < H2.
 322                  reflexivity
 323                 |apply le_S_S_to_le.
 324                  assumption
 325                 ]
 326               |assumption
 327               ]
 328             |assumption
 329             ]
 330           ]
 331         |assumption
 332         ]
 333       |assumption
 334       ]
 335     ]
 336   ]
 337 qed.
 338
 339 theorem sigma_p_divides:
 340 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
 341 \forall g: nat \to nat.
 342 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
 343 sigma_p (S n) (\lambda x.divides_b x n)
 344   (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
 345 intros.
 346 unfold sigma_p.
 347 apply (iter_p_gen_divides nat O plus n m p ? ? ? g)
 348 [ assumption
 349 | assumption
 350 | assumption
 351 | apply symmetricIntPlus
 352 | apply associative_plus
 353 | intros.
 354   apply sym_eq.
 355   apply plus_n_O
 356 ]
 357 qed.
 358
 359 theorem distributive_times_plus_sigma_p: \forall n,k:nat. \forall p:nat \to bool. \forall g:nat \to nat.
 360 k*(sigma_p n p g) = sigma_p n p (\lambda i:nat.k * (g i)).
 361 intros.
 362 apply (distributive_times_plus_iter_p_gen nat plus O times n k p g)
 363 [ apply symmetricIntPlus
 364 | apply associative_plus
 365 | intros.
 366   apply sym_eq.
 367   apply plus_n_O
 368 | apply symmetric_times
 369 | apply distributive_times_plus
 370 | intros.
 371   rewrite < (times_n_O a).
 372   reflexivity
 373 ]
 374 qed.
 375
 376 (*some properties of sigma_p invoked with an "always true" predicate (in this
 377   way sigma_p just counts the elements, without doing any control) or with
 378   the nat \to nat function which always returns (S O).
 379   It 's not easily possible proving these theorems in a general form
 380   in generic_sigma_p.ma
 381  *)
 382
 383 theorem sigma_p_true: \forall n:nat.
 384 (sigma_p n (\lambda x.true) (\lambda x.S O)) = n.
 385 intros.
 386 elim n
 387 [ simplify.
 388   reflexivity
 389 | rewrite > (true_to_sigma_p_Sn n1 (\lambda x:nat.true) (\lambda x:nat.S O))
 390   [ rewrite > H.
 391     simplify.
 392     reflexivity
 393   | reflexivity
 394   ]
 395 ]
 396 qed.
 397
 398 theorem sigma_P_SO_to_sigma_p_true: \forall n:nat. \forall g:nat \to bool.
 399 sigma_p n g (\lambda n:nat. (S O)) =
 400 sigma_p n (\lambda x:nat.true) (\lambda i:nat.bool_to_nat (g i)).
 401 intros.
 402 elim n
 403 [ simplify.
 404   reflexivity
 405 | cut ((g n1) = true \lor (g n1) = false)
 406   [ rewrite > true_to_sigma_p_Sn in \vdash (? ? ? %)
 407     [ elim Hcut
 408       [ rewrite > H1.
 409         rewrite > true_to_sigma_p_Sn in \vdash (? ? % ?)
 410         [ simplify.
 411           apply eq_f.
 412           assumption
 413         | assumption
 414         ]
 415       | rewrite > H1.
 416         rewrite > false_to_sigma_p_Sn in \vdash (? ? % ?)
 417         [ simplify.
 418           assumption
 419         | assumption
 420         ]
 421       ]
 422     | reflexivity
 423     ]
 424   | elim (g n1)
 425     [ left.
 426       reflexivity
 427     | right.
 428       reflexivity
 429     ]
 430   ]
 431 ]
 432 qed.
 433
 434 (* I introduce an equivalence in the form map_iter_i in order to use
 435  * the existing result about permutation in that part of the library.
 436  *)
 437
 438 theorem eq_map_iter_i_sigma_p_alwaysTrue:  \forall n:nat.\forall g:nat \to nat.
 439 map_iter_i n g plus O = sigma_p (S n) (\lambda c:nat.true) g.
 440 intros.
 441 elim n
 442 [ simplify.
 443   rewrite < plus_n_O.
 444   reflexivity
 445 | rewrite > true_to_sigma_p_Sn
 446   [ simplify in \vdash (? ? % ?).
 447     rewrite < plus_n_O.
 448     apply eq_f.
 449     assumption
 450   | reflexivity
 451   ]
 452 ]
 453 qed.
 454
 455 theorem sigma_p_plus_1: \forall n:nat. \forall f,g:nat \to nat.
 456 sigma_p n (\lambda b:nat. true) (\lambda a:nat.(f a) + (g a)) =
 457 sigma_p n (\lambda b:nat. true) f + sigma_p n (\lambda b:nat. true) g.
 458 intros.
 459 elim n
 460 [ simplify.
 461   reflexivity
 462 | rewrite > true_to_sigma_p_Sn
 463   [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) f)
 464     [ rewrite > (true_to_sigma_p_Sn n1 (\lambda c:nat.true) g)
 465       [ rewrite > assoc_plus in \vdash (? ? ? %).
 466         rewrite < assoc_plus in \vdash (? ? ? (? ? %)).
 467         rewrite < sym_plus in \vdash (? ? ? (? ? (? % ?))).
 468         rewrite > assoc_plus in \vdash (? ? ? (? ? %)).
 469         rewrite < assoc_plus in \vdash (? ? ? %).
 470         apply eq_f.
 471         assumption
 472       | reflexivity
 473       ]
 474     | reflexivity
 475     ]
 476   | reflexivity
 477   ]
 478 ]
 479 qed.
 480
 481
 482 theorem eq_sigma_p_sigma_p_times1 : \forall n,m:nat.\forall f:nat \to nat.
 483 sigma_p (n*m) (\lambda x:nat.true) f =
 484 sigma_p m (\lambda x:nat.true)
 485     (\lambda a.(sigma_p n (\lambda x:nat.true) (\lambda b.f (b*m + a)))).
 486 intro.
 487 elim n
 488 [ simplify.
 489   elim m
 490   [ simplify.
 491     reflexivity
 492   | rewrite > true_to_sigma_p_Sn
 493     [ rewrite < H.
 494       reflexivity
 495     | reflexivity
 496     ]
 497   ]
 498 | change in \vdash (? ? ? (? ? ? (\lambda a:?.%))) with ((f ((n1*m)+a)) +
 499   (sigma_p n1 (\lambda x:nat.true) (\lambda b:nat.f (b*m +a)))).
 500   rewrite > sigma_p_plus_1 in \vdash (? ? ? %).
 501   rewrite > (sym_times (S n1) m).
 502   rewrite < (times_n_Sm m  n1).
 503   rewrite > sigma_p_plus in \vdash (? ? % ?).
 504   apply eq_f2
 505   [ rewrite < (sym_times m n1).
 506     apply eq_sigma_p
 507     [ intros.
 508       reflexivity
 509     | intros.
 510       rewrite < (sym_plus ? (m * n1)).
 511       reflexivity
 512     ]
 513   | rewrite > (sym_times m n1).
 514     apply H
 515   ]
 516 ]
 517 qed.
 518
 519 theorem eq_sigma_p_sigma_p_times2 : \forall n,m:nat.\forall f:nat \to nat.
 520 sigma_p (n *m) (\lambda c:nat.true) f =
 521 sigma_p  n (\lambda c:nat.true)
 522   (\lambda a.(sigma_p m (\lambda c:nat.true) (\lambda b:nat.f (b* n + a)))).
 523 intros.
 524 rewrite > sym_times.
 525 apply eq_sigma_p_sigma_p_times1.
 526 qed.
 527
 528
 529 theorem sigma_p_times:\forall n,m:nat.
 530 \forall f,f1,f2:nat \to bool.
 531 \forall g:nat \to nat \to nat.
 532 \forall g1,g2: nat \to nat.
 533 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g b a) < (S n)*(S m)) \to
 534 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g1 (g b a)) = a) \to
 535 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g2 (g b a)) = b) \to
 536 (\forall a,b:nat. a < (S n) \to b < (S m) \to f (g b a) = andb (f2 b) (f1 a)) \to
 537 (sigma_p ((S n) * (S m)) f (\lambda c:nat.(S O))) =
 538 sigma_p (S n) f1 (\lambda c:nat.(S O)) * sigma_p (S m) f2 (\lambda c:nat.(S O)).
 539 intros.
 540
 541 rewrite > (sigma_P_SO_to_sigma_p_true ).
 542 rewrite > (S_pred ((S n)*(S m))) in \vdash (? ? (? % ? ?) ?)
 543 [ rewrite < (eq_map_iter_i_sigma_p_alwaysTrue (pred ((S n)* (S m)))).
 544   rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ?
 545            (\lambda i.g (div i (S n)) (mod i (S n))))
 546   [ rewrite > eq_map_iter_i_sigma_p_alwaysTrue.
 547     rewrite < S_pred
 548     [ rewrite > eq_sigma_p_sigma_p_times2.
 549       apply (trans_eq ? ? (sigma_p (S n)  (\lambda c:nat.true)
 550         (\lambda a. sigma_p (S m) (\lambda c:nat.true)
 551                 (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))))))
 552       [ apply eq_sigma_p;intros
 553         [ reflexivity
 554         | apply eq_sigma_p;intros
 555           [ reflexivity
 556           |
 557             rewrite > (div_mod_spec_to_eq (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
 558                                                   ((x1*(S n) + x) \mod (S n)) x1 x)
 559             [ rewrite > (div_mod_spec_to_eq2 (x1*(S n) + x) (S n) ((x1*(S n) + x)/(S n))
 560                                                   ((x1*(S n) + x) \mod (S n)) x1 x)
 561               [ rewrite > H3
 562                 [ apply bool_to_nat_andb
 563                 | assumption
 564                 | assumption
 565                 ]
 566               | apply div_mod_spec_div_mod.
 567                 apply lt_O_S
 568               | constructor 1
 569                 [ assumption
 570                 | reflexivity
 571                 ]
 572               ]
 573             | apply div_mod_spec_div_mod.
 574               apply lt_O_S
 575             | constructor 1
 576               [ assumption
 577               | reflexivity
 578               ]
 579             ]
 580           ]
 581         ]
 582       | apply (trans_eq ? ?
 583          (sigma_p (S n) (\lambda c:nat.true) (\lambda n.((bool_to_nat (f1 n)) *
 584          (sigma_p (S m) (\lambda c:nat.true) (\lambda n.bool_to_nat (f2 n)))))))
 585         [ apply eq_sigma_p;intros
 586           [ reflexivity
 587           | rewrite > distributive_times_plus_sigma_p.
 588             apply eq_sigma_p;intros
 589             [ reflexivity
 590             | rewrite > sym_times.
 591               reflexivity
 592             ]
 593           ]
 594         | apply sym_eq.
 595           rewrite > sigma_P_SO_to_sigma_p_true.
 596           rewrite > sigma_P_SO_to_sigma_p_true in \vdash (? ? (? ? %) ?).
 597           rewrite > sym_times.
 598           rewrite > distributive_times_plus_sigma_p.
 599           apply eq_sigma_p;intros
 600           [ reflexivity
 601           | rewrite > distributive_times_plus_sigma_p.
 602             rewrite < sym_times.
 603             rewrite > distributive_times_plus_sigma_p.
 604             apply eq_sigma_p;
 605               intros; reflexivity
 606           ]
 607         ]
 608       ]
 609     | apply lt_O_times_S_S
 610     ]
 611
 612   | unfold permut.
 613     split
 614     [ intros.
 615       rewrite < plus_n_O.
 616       apply le_S_S_to_le.
 617       rewrite < S_pred in \vdash (? ? %)
 618       [ change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
 619         apply H
 620         [ apply lt_mod_m_m.
 621           unfold lt.
 622           apply le_S_S.
 623           apply le_O_n
 624         | apply (lt_times_to_lt_l n).
 625           apply (le_to_lt_to_lt ? i)
 626           [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
 627             [ rewrite > sym_plus.
 628               apply le_plus_n
 629             | unfold lt.
 630               apply le_S_S.
 631               apply le_O_n
 632             ]
 633           | unfold lt.
 634             rewrite > S_pred in \vdash (? ? %)
 635             [ apply le_S_S.
 636               rewrite > plus_n_O in \vdash (? ? %).
 637               rewrite > sym_times.
 638               assumption
 639             | apply lt_O_times_S_S
 640             ]
 641           ]
 642         ]
 643       | apply lt_O_times_S_S
 644       ]
 645     | rewrite < plus_n_O.
 646       unfold injn.
 647       intros.
 648       cut (i < (S n)*(S m))
 649       [ cut (j < (S n)*(S m))
 650         [ cut ((i \mod (S n)) < (S n))
 651           [ cut ((i/(S n)) < (S m))
 652             [ cut ((j \mod (S n)) < (S n))
 653               [ cut ((j/(S n)) < (S m))
 654                 [ rewrite > (div_mod i (S n))
 655                   [ rewrite > (div_mod j (S n))
 656                     [ rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
 657                       rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
 658                       rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
 659                       rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
 660                       rewrite > H6.
 661                       reflexivity
 662                     | unfold lt.
 663                       apply le_S_S.
 664                       apply le_O_n
 665                     ]
 666                   | unfold lt.
 667                     apply le_S_S.
 668                     apply le_O_n
 669                   ]
 670                 | apply (lt_times_to_lt_l n).
 671                   apply (le_to_lt_to_lt ? j)
 672                   [ rewrite > (div_mod j (S n)) in \vdash (? ? %)
 673                     [ rewrite > sym_plus.
 674                       apply le_plus_n
 675                     | unfold lt. apply le_S_S.
 676                       apply le_O_n
 677                     ]
 678                   | rewrite < sym_times.
 679                     assumption
 680                   ]
 681                 ]
 682               | apply lt_mod_m_m.
 683                 unfold lt.
 684                 apply le_S_S.
 685                 apply le_O_n
 686               ]
 687             | apply (lt_times_to_lt_l n).
 688               apply (le_to_lt_to_lt ? i)
 689               [ rewrite > (div_mod i (S n)) in \vdash (? ? %)
 690                 [ rewrite > sym_plus.
 691                   apply le_plus_n
 692                 | unfold lt.
 693                   apply le_S_S.
 694                   apply le_O_n
 695                 ]
 696               | rewrite < sym_times.
 697                 assumption
 698               ]
 699             ]
 700           | apply lt_mod_m_m.
 701             unfold lt.
 702             apply le_S_S.
 703             apply le_O_n
 704           ]
 705         | unfold lt.
 706           rewrite > S_pred in \vdash (? ? %)
 707           [ apply le_S_S.
 708             assumption
 709           | apply lt_O_times_S_S
 710           ]
 711         ]
 712       | unfold lt.
 713         rewrite > S_pred in \vdash (? ? %)
 714         [ apply le_S_S.
 715           assumption
 716         | apply lt_O_times_S_S
 717         ]
 718       ]
 719     ]
 720   | intros.
 721     apply False_ind.
 722     apply (not_le_Sn_O m1 H4)
 723   ]
 724 | apply lt_O_times_S_S
 725 ]
 726 qed.
 727
 728 theorem sigma_p_knm:
 729 \forall g: nat \to nat.
 730 \forall h2:nat \to nat \to nat.
 731 \forall h11,h12:nat \to nat.
 732 \forall k,n,m.
 733 \forall p1,p21:nat \to bool.
 734 \forall p22:nat \to nat \to bool.
 735 (\forall x. x < k \to p1 x = true \to
 736 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
 737 \land h2 (h11 x) (h12 x) = x
 738 \land (h11 x) < n \land (h12 x) < m) \to
 739 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
 740 p1 (h2 i j) = true \land
 741 h11 (h2 i j) = i \land h12 (h2 i j) = j
 742 \land h2 i j < k) \to
 743 sigma_p k p1 g=
 744 sigma_p n p21 (\lambda x:nat.sigma_p m (p22 x) (\lambda y. g (h2 x y))).
 745 intros.
 746 unfold sigma_p.
 747 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
 748 apply iter_p_gen_knm
 749   [apply symmetricIntPlus
 750   |apply associative_plus
 751   |intro.rewrite < plus_n_O.reflexivity
 752   |exact h11
 753   |exact h12
 754   |assumption
 755   |assumption
 756   ]
 757 qed.
 758
 759
 760 theorem sigma_p2_eq:
 761 \forall g: nat \to nat \to nat.
 762 \forall h11,h12,h21,h22: nat \to nat \to nat.
 763 \forall n1,m1,n2,m2.
 764 \forall p11,p21:nat \to bool.
 765 \forall p12,p22:nat \to nat \to bool.
 766 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
 767 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
 768 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
 769 \land h11 i j < n1 \land h12 i j < m1) \to
 770 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
 771 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
 772 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
 773 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
 774 sigma_p n1 p11 (\lambda x:nat .sigma_p m1 (p12 x) (\lambda y. g x y)) =
 775 sigma_p n2 p21 (\lambda x:nat .sigma_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
 776 intros.
 777 unfold sigma_p.
 778 unfold sigma_p in \vdash (? ? (? ? ? ? (\lambda x:?.%) ? ?) ?).
 779 unfold sigma_p in \vdash (? ? ? (? ? ? ? (\lambda x:?.%) ? ?)).
 780
 781 apply(iter_p_gen_2_eq nat O plus ? ? ? g h11 h12 h21 h22 n1 m1 n2 m2 p11 p21 p12 p22)
 782 [ apply symmetricIntPlus
 783 | apply associative_plus
 784 | intro.
 785   rewrite < (plus_n_O).
 786   reflexivity
 787 | assumption
 788 | assumption
 789 ]
 790 qed.