matita/library/nat/generic_iter_p.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 include "nat/div_and_mod_diseq.ma".
  18 include "nat/primes.ma".
  19 include "nat/ord.ma".
  20
  21 (*a generic definition of summatory indexed over natural numbers:
  22  * n:N is the advanced end in the range of the sommatory
  23  * p: N -> bool is a predicate. if (p i) = true, then (g i) is summed, else it isn't
  24  * A is the type of the elements of the sum.
  25  * g:nat -> A, is the function which associates the nth element of the sum to the nth natural numbers
  26  * baseA (of type A) is the neutral element of A for plusA operation
  27  * plusA: A -> A -> A is the sum over elements in A.
  28  *)
  29
  30 let rec iter_p_gen (n:nat) (p: nat \to bool) (A:Type) (g: nat \to A)
  31    (baseA: A) (plusA: A \to A \to A)  \def
  32   match n with
  33    [ O \Rightarrow baseA
  34    | (S k) \Rightarrow
  35       match p k with
  36       [true \Rightarrow (plusA (g k) (iter_p_gen k p A g baseA plusA))
  37       |false \Rightarrow iter_p_gen k p A g baseA plusA]
  38    ].
  39
  40 theorem true_to_iter_p_gen_Sn:
  41 \forall n:nat. \forall p:nat \to bool. \forall A:Type. \forall g:nat \to A.
  42 \forall baseA:A. \forall plusA: A \to A \to A.
  43 p n = true \to iter_p_gen (S n) p A g baseA plusA =
  44 (plusA (g n) (iter_p_gen n p A g baseA plusA)).
  45 intros.
  46 simplify.
  47 rewrite > H.
  48 reflexivity.
  49 qed.
  50
  51 theorem false_to_iter_p_gen_Sn:
  52 \forall n:nat. \forall p:nat \to bool. \forall A:Type. \forall g:nat \to A.
  53 \forall baseA:A. \forall plusA: A \to A \to A.
  54 p n = false \to iter_p_gen (S n) p A g baseA plusA = iter_p_gen n p A g baseA plusA.
  55 intros.
  56 simplify.
  57 rewrite > H.
  58 reflexivity.
  59 qed.
  60
  61 theorem eq_iter_p_gen: \forall p1,p2:nat \to bool. \forall A:Type.
  62 \forall g1,g2: nat \to A. \forall baseA: A.
  63 \forall plusA: A \to A \to A. \forall n:nat.
  64 (\forall x.  x < n \to p1 x = p2 x) \to
  65 (\forall x.  x < n \to g1 x = g2 x) \to
  66 iter_p_gen n p1 A g1 baseA plusA = iter_p_gen n p2 A g2 baseA plusA.
  67 intros 8.
  68 elim n
  69 [ reflexivity
  70 | apply (bool_elim ? (p1 n1))
  71   [ intro.
  72     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
  73     rewrite > true_to_iter_p_gen_Sn
  74     [ apply eq_f2
  75       [ apply H2.apply le_n.
  76       | apply H
  77         [ intros.apply H1.apply le_S.assumption
  78         | intros.apply H2.apply le_S.assumption
  79         ]
  80       ]
  81     | rewrite < H3.apply sym_eq.apply H1.apply le_n
  82     ]
  83   | intro.
  84     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
  85     rewrite > false_to_iter_p_gen_Sn
  86     [ apply H
  87       [ intros.apply H1.apply le_S.assumption
  88       | intros.apply H2.apply le_S.assumption
  89       ]
  90     | rewrite < H3.apply sym_eq.apply H1.apply le_n
  91     ]
  92   ]
  93 ]
  94 qed.
  95
  96 theorem eq_iter_p_gen1: \forall p1,p2:nat \to bool. \forall A:Type.
  97 \forall g1,g2: nat \to A. \forall baseA: A.
  98 \forall plusA: A \to A \to A.\forall n:nat.
  99 (\forall x.  x < n \to p1 x = p2 x) \to
 100 (\forall x.  x < n \to p1 x = true \to g1 x = g2 x) \to
 101 iter_p_gen n p1 A g1 baseA plusA = iter_p_gen n p2 A g2 baseA plusA.
 102 intros 8.
 103 elim n
 104 [ reflexivity
 105 | apply (bool_elim ? (p1 n1))
 106   [ intro.
 107     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
 108     rewrite > true_to_iter_p_gen_Sn
 109     [ apply eq_f2
 110       [ apply H2
 111         [ apply le_n
 112         | assumption
 113         ]
 114       | apply H
 115         [ intros.apply H1.apply le_S.assumption
 116         | intros.apply H2
 117           [ apply le_S.assumption
 118           | assumption
 119           ]
 120         ]
 121       ]
 122     | rewrite < H3.
 123       apply sym_eq.apply H1.apply le_n
 124     ]
 125   | intro.
 126     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
 127     rewrite > false_to_iter_p_gen_Sn
 128     [ apply H
 129       [ intros.apply H1.apply le_S.assumption
 130       | intros.apply H2
 131         [ apply le_S.assumption
 132         | assumption
 133         ]
 134       ]
 135     | rewrite < H3.apply sym_eq.
 136       apply H1.apply le_n
 137     ]
 138   ]
 139 ]
 140 qed.
 141
 142 theorem iter_p_gen_false: \forall A:Type. \forall g: nat \to A. \forall baseA:A.
 143 \forall plusA: A \to A \to A. \forall n.
 144 iter_p_gen n (\lambda x.false) A g baseA plusA = baseA.
 145 intros.
 146 elim n
 147 [ reflexivity
 148 | simplify.
 149   assumption
 150 ]
 151 qed.
 152
 153 theorem iter_p_gen_plusA: \forall A:Type. \forall n,k:nat.\forall p:nat \to bool.
 154 \forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
 155 (symmetric A plusA) \to (\forall a:A. (plusA a baseA) = a) \to (associative A plusA)
 156 \to
 157 iter_p_gen (k + n) p A g baseA plusA
 158 = (plusA (iter_p_gen k (\lambda x.p (x+n)) A (\lambda x.g (x+n)) baseA plusA)
 159          (iter_p_gen n p A g baseA plusA)).
 160 intros.
 161
 162 elim k
 163 [ rewrite < (plus_n_O n).
 164   simplify.
 165   rewrite > H in \vdash (? ? ? %).
 166   rewrite > (H1 ?).
 167   reflexivity
 168 | apply (bool_elim ? (p (n1+n)))
 169   [ intro.
 170     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
 171     rewrite > (true_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4).
 172     rewrite > (H2 (g (n1 + n)) ? ?).
 173     rewrite < H3.
 174     reflexivity
 175   | intro.
 176     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
 177     rewrite > (false_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4).
 178     assumption
 179   ]
 180 ]
 181 qed.
 182
 183 theorem false_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool.
 184 \forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
 185 n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false)
 186 \to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA.
 187 intros 8.
 188 elim H
 189 [ reflexivity
 190 | simplify.
 191   rewrite > H3
 192   [ simplify.
 193     apply H2.
 194     intros.
 195     apply H3
 196     [ apply H4
 197     | apply le_S.
 198       assumption
 199     ]
 200   | assumption
 201   |apply le_n
 202   ]
 203 ]
 204 qed.
 205
 206 (* a therem slightly more general than the previous one *)
 207 theorem or_false_eq_baseA_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool.
 208 \forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
 209 (\forall a. plusA baseA a = a) \to
 210 n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = baseA)
 211 \to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA.
 212 intros 9.
 213 elim H1
 214 [reflexivity
 215 |apply (bool_elim ? (p n1));intro
 216   [elim (H4 n1)
 217     [apply False_ind.
 218      apply not_eq_true_false.
 219      rewrite < H5.
 220      rewrite < H6.
 221      reflexivity
 222     |rewrite > true_to_iter_p_gen_Sn
 223       [rewrite > H6.
 224        rewrite > H.
 225        apply H3.intros.
 226        apply H4
 227         [assumption
 228         |apply le_S.assumption
 229         ]
 230       |assumption
 231       ]
 232     |assumption
 233     |apply le_n
 234     ]
 235   |rewrite > false_to_iter_p_gen_Sn
 236     [apply H3.intros.
 237      apply H4
 238       [assumption
 239       |apply le_S.assumption
 240       ]
 241     |assumption
 242     ]
 243   ]
 244 ]
 245 qed.
 246
 247 theorem iter_p_gen2 :
 248 \forall n,m:nat.
 249 \forall p1,p2:nat \to bool.
 250 \forall A:Type.
 251 \forall g: nat \to nat \to A.
 252 \forall baseA: A.
 253 \forall plusA: A \to A \to A.
 254 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
 255 \to
 256 iter_p_gen (n*m)
 257   (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
 258   A
 259   (\lambda x.g (div x m) (mod x m))
 260   baseA
 261   plusA  =
 262 iter_p_gen n p1 A
 263   (\lambda x.iter_p_gen m p2 A (g x) baseA plusA)
 264   baseA plusA.
 265 intros.
 266 elim n
 267 [ simplify.
 268   reflexivity
 269 | apply (bool_elim ? (p1 n1))
 270   [ intro.
 271     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
 272     simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
 273     rewrite > iter_p_gen_plusA
 274     [ rewrite < H3.
 275       apply eq_f2
 276       [ apply eq_iter_p_gen
 277         [ intros.
 278           rewrite > sym_plus.
 279           rewrite > (div_plus_times ? ? ? H5).
 280           rewrite > (mod_plus_times ? ? ? H5).
 281           rewrite > H4.
 282           simplify.
 283           reflexivity
 284         | intros.
 285           rewrite > sym_plus.
 286           rewrite > (div_plus_times ? ? ? H5).
 287           rewrite > (mod_plus_times ? ? ? H5).
 288           rewrite > H4.
 289           simplify.reflexivity.
 290         ]
 291       | reflexivity
 292       ]
 293     | assumption
 294     | assumption
 295     | assumption
 296     ]
 297   | intro.
 298     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
 299     simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
 300     rewrite > iter_p_gen_plusA
 301     [ rewrite > H3.
 302       apply (trans_eq ? ? (plusA baseA
 303            (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m p2 A (g x) baseA plusA) baseA plusA )))
 304       [ apply eq_f2
 305         [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
 306           [ apply iter_p_gen_false
 307           | intros.
 308             rewrite > sym_plus.
 309             rewrite > (div_plus_times ? ? ? H5).
 310             rewrite > (mod_plus_times ? ? ? H5).
 311             rewrite > H4.
 312             simplify.reflexivity
 313           | intros.reflexivity.
 314           ]
 315         | reflexivity
 316         ]
 317       | rewrite < H.
 318         rewrite > H2.
 319         reflexivity.
 320       ]
 321     | assumption
 322     | assumption
 323     | assumption
 324     ]
 325   ]
 326 ]
 327 qed.
 328
 329 theorem iter_p_gen2':
 330 \forall n,m:nat.
 331 \forall p1: nat \to bool.
 332 \forall p2: nat \to nat \to bool.
 333 \forall A:Type.
 334 \forall g: nat \to nat \to A.
 335 \forall baseA: A.
 336 \forall plusA: A \to A \to A.
 337 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
 338 \to
 339 iter_p_gen (n*m)
 340   (\lambda x.andb (p1 (div x m)) (p2 (div x m)(mod x m)))
 341   A
 342   (\lambda x.g (div x m) (mod x m))
 343   baseA
 344   plusA  =
 345 iter_p_gen n p1 A
 346   (\lambda x.iter_p_gen m (p2 x) A (g x) baseA plusA)
 347   baseA plusA.
 348 intros.
 349 elim n
 350 [ simplify.
 351   reflexivity
 352 | apply (bool_elim ? (p1 n1))
 353   [ intro.
 354     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
 355     simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
 356     rewrite > iter_p_gen_plusA
 357     [ rewrite < H3.
 358       apply eq_f2
 359       [ apply eq_iter_p_gen
 360         [ intros.
 361           rewrite > sym_plus.
 362           rewrite > (div_plus_times ? ? ? H5).
 363           rewrite > (mod_plus_times ? ? ? H5).
 364           rewrite > H4.
 365           simplify.
 366           reflexivity
 367         | intros.
 368           rewrite > sym_plus.
 369           rewrite > (div_plus_times ? ? ? H5).
 370           rewrite > (mod_plus_times ? ? ? H5).
 371           rewrite > H4.
 372           simplify.reflexivity.
 373         ]
 374       | reflexivity
 375       ]
 376     | assumption
 377     | assumption
 378     | assumption
 379     ]
 380   | intro.
 381     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
 382     simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
 383     rewrite > iter_p_gen_plusA
 384     [ rewrite > H3.
 385       apply (trans_eq ? ? (plusA baseA
 386            (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m (p2 x) A (g x) baseA plusA) baseA plusA )))
 387       [ apply eq_f2
 388         [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
 389           [ apply iter_p_gen_false
 390           | intros.
 391             rewrite > sym_plus.
 392             rewrite > (div_plus_times ? ? ? H5).
 393             rewrite > (mod_plus_times ? ? ? H5).
 394             rewrite > H4.
 395             simplify.reflexivity
 396           | intros.reflexivity.
 397           ]
 398         | reflexivity
 399         ]
 400       | rewrite < H.
 401         rewrite > H2.
 402         reflexivity.
 403       ]
 404     | assumption
 405     | assumption
 406     | assumption
 407     ]
 408   ]
 409 ]
 410 qed.
 411
 412 lemma iter_p_gen_gi:
 413 \forall A:Type.
 414 \forall g: nat \to A.
 415 \forall baseA:A.
 416 \forall plusA: A \to A \to A.
 417 \forall n,i:nat.
 418 \forall p:nat \to bool.
 419 (symmetric A plusA) \to  (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
 420   \to
 421
 422 i < n \to p i = true \to
 423 (iter_p_gen n p A g baseA plusA) =
 424 (plusA (g i) (iter_p_gen n (\lambda x:nat. andb (p x) (notb (eqb x i))) A g baseA plusA)).
 425 intros 5.
 426 elim n
 427 [ apply False_ind.
 428   apply (not_le_Sn_O i).
 429   assumption
 430 | apply (bool_elim ? (p n1));intro
 431   [ elim (le_to_or_lt_eq i n1)
 432     [ rewrite > true_to_iter_p_gen_Sn
 433       [ rewrite > true_to_iter_p_gen_Sn
 434         [ rewrite < (H2 (g i) ? ?).
 435           rewrite > (H1 (g i) (g n1)).
 436           rewrite > (H2 (g n1) ? ?).
 437           apply eq_f2
 438           [ reflexivity
 439           | apply H
 440             [ assumption
 441             | assumption
 442             | assumption
 443             | assumption
 444             | assumption
 445             ]
 446           ]
 447         | rewrite > H6.simplify.
 448           change with (notb (eqb n1 i) = notb false).
 449           apply eq_f.
 450           apply not_eq_to_eqb_false.
 451           unfold Not.intro.
 452           apply (lt_to_not_eq ? ? H7).
 453           apply sym_eq.assumption
 454         ]
 455       | assumption
 456       ]
 457     | rewrite > true_to_iter_p_gen_Sn
 458       [ rewrite > H7.
 459         apply eq_f2
 460         [ reflexivity
 461         | rewrite > false_to_iter_p_gen_Sn
 462           [ apply eq_iter_p_gen
 463             [ intros.
 464               elim (p x)
 465               [ simplify.
 466                 change with (notb false = notb (eqb x n1)).
 467                 apply eq_f.
 468                 apply sym_eq.
 469                 apply not_eq_to_eqb_false.
 470                 apply (lt_to_not_eq ? ? H8)
 471               | reflexivity
 472               ]
 473             | intros.
 474               reflexivity
 475             ]
 476           | rewrite > H6.
 477             rewrite > (eq_to_eqb_true ? ? (refl_eq ? n1)).
 478             reflexivity
 479           ]
 480         ]
 481       | assumption
 482       ]
 483     | apply le_S_S_to_le.
 484       assumption
 485     ]
 486   | rewrite > false_to_iter_p_gen_Sn
 487     [ elim (le_to_or_lt_eq i n1)
 488       [ rewrite > false_to_iter_p_gen_Sn
 489         [ apply H
 490           [ assumption
 491           | assumption
 492           | assumption
 493           | assumption
 494           | assumption
 495           ]
 496         | rewrite > H6.reflexivity
 497         ]
 498       | apply False_ind.
 499         apply not_eq_true_false.
 500         rewrite < H5.
 501         rewrite > H7.
 502         assumption
 503       | apply le_S_S_to_le.
 504         assumption
 505       ]
 506     | assumption
 507     ]
 508   ]
 509 ]
 510 qed.
 511
 512 (* invariance under permutation; single sum *)
 513 theorem eq_iter_p_gen_gh:
 514 \forall A:Type.
 515 \forall baseA: A.
 516 \forall plusA: A \to A \to A.
 517 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a) \to
 518 \forall g: nat \to A.
 519 \forall h,h1: nat \to nat.
 520 \forall n,n1:nat.
 521 \forall p1,p2:nat \to bool.
 522 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
 523 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
 524 (\forall i. i < n \to p1 i = true \to h i < n1) \to
 525 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
 526 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
 527 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
 528
 529 iter_p_gen n p1 A (\lambda x.g(h x)) baseA plusA =
 530 iter_p_gen n1 p2 A g baseA plusA.
 531 intros 10.
 532 elim n
 533 [ generalize in match H8.
 534   elim n1
 535   [ reflexivity
 536   | apply (bool_elim ? (p2 n2));intro
 537     [ apply False_ind.
 538       apply (not_le_Sn_O (h1 n2)).
 539       apply H10
 540       [ apply le_n
 541       | assumption
 542       ]
 543     | rewrite > false_to_iter_p_gen_Sn
 544       [ apply H9.
 545         intros.
 546         apply H10
 547         [ apply le_S.
 548           apply H12
 549         | assumption
 550         ]
 551       | assumption
 552       ]
 553     ]
 554   ]
 555 | apply (bool_elim ? (p1 n1));intro
 556   [ rewrite > true_to_iter_p_gen_Sn
 557     [ rewrite > (iter_p_gen_gi A g baseA plusA n2 (h n1))
 558       [ apply eq_f2
 559         [ reflexivity
 560         | apply H3
 561           [ intros.
 562             rewrite > H4
 563             [ simplify.
 564               change with ((\not eqb (h i) (h n1))= \not false).
 565               apply eq_f.
 566               apply not_eq_to_eqb_false.
 567               unfold Not.
 568               intro.
 569               apply (lt_to_not_eq ? ? H11).
 570               rewrite < H5
 571               [ rewrite < (H5 n1)
 572                 [ apply eq_f.
 573                   assumption
 574                 | apply le_n
 575                 | assumption
 576                 ]
 577               | apply le_S.
 578                 assumption
 579               | assumption
 580               ]
 581             | apply le_S.assumption
 582             | assumption
 583             ]
 584           | intros.
 585             apply H5
 586             [ apply le_S.
 587               assumption
 588             | assumption
 589             ]
 590           | intros.
 591             apply H6
 592             [ apply le_S.assumption
 593             | assumption
 594             ]
 595           | intros.
 596             apply H7
 597             [ assumption
 598             | generalize in match H12.
 599               elim (p2 j)
 600               [ reflexivity
 601               | assumption
 602               ]
 603             ]
 604           | intros.
 605             apply H8
 606             [ assumption
 607             | generalize in match H12.
 608               elim (p2 j)
 609               [ reflexivity
 610               | assumption
 611               ]
 612             ]
 613           | intros.
 614             elim (le_to_or_lt_eq (h1 j) n1)
 615             [ assumption
 616             | generalize in match H12.
 617               elim (p2 j)
 618               [ simplify in H13.
 619                 absurd (j = (h n1))
 620                 [ rewrite < H13.
 621                   rewrite > H8
 622                   [ reflexivity
 623                   | assumption
 624                   | autobatch
 625                   ]
 626                 | apply eqb_false_to_not_eq.
 627                   generalize in match H14.
 628                   elim (eqb j (h n1))
 629                   [ apply sym_eq.assumption
 630                   | reflexivity
 631                   ]
 632                 ]
 633               | simplify in H14.
 634                 apply False_ind.
 635                 apply not_eq_true_false.
 636                 apply sym_eq.assumption
 637               ]
 638             | apply le_S_S_to_le.
 639               apply H9
 640               [ assumption
 641               | generalize in match H12.
 642                 elim (p2 j)
 643                 [ reflexivity
 644                 | assumption
 645                 ]
 646               ]
 647             ]
 648           ]
 649         ]
 650       | assumption
 651       | assumption
 652       | assumption
 653       | apply H6
 654         [ apply le_n
 655         | assumption
 656         ]
 657       | apply H4
 658         [ apply le_n
 659         | assumption
 660         ]
 661       ]
 662     | assumption
 663     ]
 664   | rewrite > false_to_iter_p_gen_Sn
 665     [ apply H3
 666       [ intros.
 667         apply H4[apply le_S.assumption|assumption]
 668       | intros.
 669         apply H5[apply le_S.assumption|assumption]
 670       | intros.
 671         apply H6[apply le_S.assumption|assumption]
 672       | intros.
 673         apply H7[assumption|assumption]
 674       | intros.
 675         apply H8[assumption|assumption]
 676       | intros.
 677         elim (le_to_or_lt_eq (h1 j) n1)
 678         [ assumption
 679         | absurd (j = (h n1))
 680           [ rewrite < H13.
 681             rewrite > H8
 682             [ reflexivity
 683             | assumption
 684             | assumption
 685             ]
 686           | unfold Not.intro.
 687             apply not_eq_true_false.
 688             rewrite < H10.
 689             rewrite < H13.
 690             rewrite > H7
 691             [ reflexivity
 692             | assumption
 693             | assumption
 694             ]
 695           ]
 696         | apply le_S_S_to_le.
 697           apply H9
 698           [ assumption
 699           | assumption
 700           ]
 701         ]
 702       ]
 703     | assumption
 704     ]
 705   ]
 706 ]
 707 qed.
 708
 709 theorem eq_iter_p_gen_pred:
 710 \forall A:Type.
 711 \forall baseA: A.
 712 \forall plusA: A \to A \to A.
 713 \forall n,p,g.
 714 p O = true \to
 715 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a) \to
 716 iter_p_gen (S n) (\lambda i.p (pred i)) A (\lambda i.g(pred i)) baseA plusA =
 717 plusA (iter_p_gen n p A g baseA plusA) (g O).
 718 intros.
 719 elim n
 720   [rewrite > true_to_iter_p_gen_Sn
 721     [simplify.apply H1
 722     |assumption
 723     ]
 724   |apply (bool_elim ? (p n1));intro
 725     [rewrite > true_to_iter_p_gen_Sn
 726       [rewrite > true_to_iter_p_gen_Sn in ⊢ (? ? ? %)
 727         [rewrite > H2 in ⊢ (? ? ? %).
 728          apply eq_f.assumption
 729         |assumption
 730         ]
 731       |assumption
 732       ]
 733     |rewrite > false_to_iter_p_gen_Sn
 734       [rewrite > false_to_iter_p_gen_Sn in ⊢ (? ? ? %);assumption
 735       |assumption
 736       ]
 737     ]
 738   ]
 739 qed.
 740
 741 definition p_ord_times \def
 742 \lambda p,m,x.
 743   match p_ord x p with
 744   [pair q r \Rightarrow r*m+q].
 745
 746 theorem  eq_p_ord_times: \forall p,m,x.
 747 p_ord_times p m x = (ord_rem x p)*m+(ord x p).
 748 intros.unfold p_ord_times. unfold ord_rem.
 749 unfold ord.
 750 elim (p_ord x p).
 751 reflexivity.
 752 qed.
 753
 754 theorem div_p_ord_times:
 755 \forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
 756 intros.rewrite > eq_p_ord_times.
 757 apply div_plus_times.
 758 assumption.
 759 qed.
 760
 761 theorem mod_p_ord_times:
 762 \forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
 763 intros.rewrite > eq_p_ord_times.
 764 apply mod_plus_times.
 765 assumption.
 766 qed.
 767
 768 lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
 769 intros.
 770 elim (le_to_or_lt_eq O ? (le_O_n m))
 771   [assumption
 772   |apply False_ind.
 773    rewrite < H1 in H.
 774    rewrite < times_n_O in H.
 775    apply (not_le_Sn_O ? H)
 776   ]
 777 qed.
 778
 779 theorem iter_p_gen_knm:
 780 \forall A:Type.
 781 \forall baseA: A.
 782 \forall plusA: A \to A \to A.
 783 (symmetric A plusA) \to
 784 (associative A plusA) \to
 785 (\forall a:A.(plusA a  baseA) = a)\to
 786 \forall g: nat \to A.
 787 \forall h2:nat \to nat \to nat.
 788 \forall h11,h12:nat \to nat.
 789 \forall k,n,m.
 790 \forall p1,p21:nat \to bool.
 791 \forall p22:nat \to nat \to bool.
 792 (\forall x. x < k \to p1 x = true \to
 793 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
 794 \land h2 (h11 x) (h12 x) = x
 795 \land (h11 x) < n \land (h12 x) < m) \to
 796 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
 797 p1 (h2 i j) = true \land
 798 h11 (h2 i j) = i \land h12 (h2 i j) = j
 799 \land h2 i j < k) \to
 800 iter_p_gen k p1 A g baseA plusA =
 801 iter_p_gen n p21 A (\lambda x:nat.iter_p_gen m (p22 x) A (\lambda y. g (h2 x y)) baseA plusA) baseA plusA.
 802 intros.
 803 rewrite < (iter_p_gen2' n m p21 p22 ? ? ? ? H H1 H2).
 804 apply sym_eq.
 805 apply (eq_iter_p_gen_gh A baseA plusA H H1 H2 g ? (\lambda x.(h11 x)*m+(h12 x)))
 806  [intros.
 807   elim (H4 (i/m) (i \mod m));clear H4
 808    [elim H7.clear H7.
 809     elim H4.clear H4.
 810     assumption
 811    |apply (lt_times_to_lt_div ? ? ? H5)
 812    |apply lt_mod_m_m.
 813     apply (lt_times_to_lt_O ? ? ? H5)
 814    |apply (andb_true_true ? ? H6)
 815    |apply (andb_true_true_r ? ? H6)
 816    ]
 817  |intros.
 818   elim (H4 (i/m) (i \mod m));clear H4
 819    [elim H7.clear H7.
 820     elim H4.clear H4.
 821     rewrite > H10.
 822     rewrite > H9.
 823     apply sym_eq.
 824     apply div_mod.
 825     apply (lt_times_to_lt_O ? ? ? H5)
 826    |apply (lt_times_to_lt_div ? ? ? H5)
 827    |apply lt_mod_m_m.
 828     apply (lt_times_to_lt_O ? ? ? H5)
 829    |apply (andb_true_true ? ? H6)
 830    |apply (andb_true_true_r ? ? H6)
 831    ]
 832  |intros.
 833   elim (H4 (i/m) (i \mod m));clear H4
 834    [elim H7.clear H7.
 835     elim H4.clear H4.
 836     assumption
 837    |apply (lt_times_to_lt_div ? ? ? H5)
 838    |apply lt_mod_m_m.
 839     apply (lt_times_to_lt_O ? ? ? H5)
 840    |apply (andb_true_true ? ? H6)
 841    |apply (andb_true_true_r ? ? H6)
 842    ]
 843  |intros.
 844   elim (H3 j H5 H6).
 845   elim H7.clear H7.
 846   elim H9.clear H9.
 847   elim H7.clear H7.
 848   rewrite > div_plus_times
 849    [rewrite > mod_plus_times
 850      [rewrite > H9.
 851       rewrite > H12.
 852       reflexivity.
 853      |assumption
 854      ]
 855    |assumption
 856    ]
 857  |intros.
 858   elim (H3 j H5 H6).
 859   elim H7.clear H7.
 860   elim H9.clear H9.
 861   elim H7.clear H7.
 862   rewrite > div_plus_times
 863    [rewrite > mod_plus_times
 864      [assumption
 865      |assumption
 866      ]
 867    |assumption
 868    ]
 869  |intros.
 870   elim (H3 j H5 H6).
 871   elim H7.clear H7.
 872   elim H9.clear H9.
 873   elim H7.clear H7.
 874   apply (lt_to_le_to_lt ? ((h11 j)*m+m))
 875    [apply monotonic_lt_plus_r.
 876     assumption
 877    |rewrite > sym_plus.
 878     change with ((S (h11 j)*m) \le n*m).
 879     apply monotonic_le_times_l.
 880     assumption
 881    ]
 882  ]
 883 qed.
 884
 885 theorem iter_p_gen_divides:
 886 \forall A:Type.
 887 \forall baseA: A.
 888 \forall plusA: A \to A \to A.
 889 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
 890 \forall g: nat \to A.
 891 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
 892
 893 \to
 894
 895 iter_p_gen (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) A g baseA plusA =
 896 iter_p_gen (S n) (\lambda x.divides_b x n) A
 897   (\lambda x.iter_p_gen (S m) (\lambda y.true) A (\lambda y.g (x*(exp p y))) baseA plusA) baseA plusA.
 898 intros.
 899 cut (O < p)
 900   [rewrite < (iter_p_gen2 ? ? ? ? ? ? ? ? H3 H4 H5).
 901    apply (trans_eq ? ?
 902     (iter_p_gen (S n*S m) (\lambda x:nat.divides_b (x/S m) n) A
 903        (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m)))  baseA plusA) )
 904     [apply sym_eq.
 905      apply (eq_iter_p_gen_gh ? ? ? ? ? ? g ? (p_ord_times p (S m)))
 906       [ assumption
 907       | assumption
 908       | assumption
 909       |intros.
 910        lapply (divides_b_true_to_lt_O ? ? H H7).
 911        apply divides_to_divides_b_true
 912         [rewrite > (times_n_O O).
 913          apply lt_times
 914           [assumption
 915           |apply lt_O_exp.assumption
 916           ]
 917         |apply divides_times
 918           [apply divides_b_true_to_divides.assumption
 919           |apply (witness ? ? (p \sup (m-i \mod (S m)))).
 920            rewrite < exp_plus_times.
 921            apply eq_f.
 922            rewrite > sym_plus.
 923            apply plus_minus_m_m.
 924            autobatch
 925           ]
 926         ]
 927       |intros.
 928        lapply (divides_b_true_to_lt_O ? ? H H7).
 929        unfold p_ord_times.
 930        rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
 931         [change with ((i/S m)*S m+i \mod S m=i).
 932          apply sym_eq.
 933          apply div_mod.
 934          apply lt_O_S
 935         |assumption
 936         |unfold Not.intro.
 937          apply H2.
 938          apply (trans_divides ? (i/ S m))
 939           [assumption|
 940            apply divides_b_true_to_divides;assumption]
 941         |apply sym_times.
 942         ]
 943       |intros.
 944        apply le_S_S.
 945        apply le_times
 946         [apply le_S_S_to_le.
 947          change with ((i/S m) < S n).
 948          apply (lt_times_to_lt_l m).
 949          apply (le_to_lt_to_lt ? i)
 950           [autobatch|assumption]
 951         |apply le_exp
 952           [assumption
 953           |apply le_S_S_to_le.
 954            apply lt_mod_m_m.
 955            apply lt_O_S
 956           ]
 957         ]
 958       |intros.
 959        cut (ord j p < S m)
 960         [rewrite > div_p_ord_times
 961           [apply divides_to_divides_b_true
 962             [apply lt_O_ord_rem
 963              [elim H1.assumption
 964              |apply (divides_b_true_to_lt_O ? ? ? H7).
 965                rewrite > (times_n_O O).
 966                apply lt_times
 967                [assumption|apply lt_O_exp.assumption]
 968              ]
 969            |cut (n = ord_rem (n*(exp p m)) p)
 970               [rewrite > Hcut2.
 971                apply divides_to_divides_ord_rem
 972                 [apply (divides_b_true_to_lt_O ? ? ? H7).
 973                  rewrite > (times_n_O O).
 974                  apply lt_times
 975                  [assumption|apply lt_O_exp.assumption]
 976                  |rewrite > (times_n_O O).
 977                    apply lt_times
 978                   [assumption|apply lt_O_exp.assumption]
 979                |assumption
 980                |apply divides_b_true_to_divides.
 981                 assumption
 982                ]
 983               |unfold ord_rem.
 984               rewrite > (p_ord_exp1 p ? m n)
 985                 [reflexivity
 986                |assumption
 987                 |assumption
 988                |apply sym_times
 989                ]
 990              ]
 991             ]
 992           |assumption
 993           ]
 994         |cut (m = ord (n*(exp p m)) p)
 995           [apply le_S_S.
 996            rewrite > Hcut1.
 997            apply divides_to_le_ord
 998             [apply (divides_b_true_to_lt_O ? ? ? H7).
 999              rewrite > (times_n_O O).
1000              apply lt_times
1001               [assumption|apply lt_O_exp.assumption]
1002             |rewrite > (times_n_O O).
1003              apply lt_times
1004               [assumption|apply lt_O_exp.assumption]
1005             |assumption
1006             |apply divides_b_true_to_divides.
1007              assumption
1008             ]
1009           |unfold ord.
1010            rewrite > (p_ord_exp1 p ? m n)
1011             [reflexivity
1012             |assumption
1013             |assumption
1014             |apply sym_times
1015             ]
1016           ]
1017         ]
1018       |intros.
1019        cut (ord j p < S m)
1020         [rewrite > div_p_ord_times
1021           [rewrite > mod_p_ord_times
1022             [rewrite > sym_times.
1023              apply sym_eq.
1024              apply exp_ord
1025               [elim H1.assumption
1026               |apply (divides_b_true_to_lt_O ? ? ? H7).
1027                rewrite > (times_n_O O).
1028                apply lt_times
1029                 [assumption|apply lt_O_exp.assumption]
1030               ]
1031            |cut (m = ord (n*(exp p m)) p)
1032              [apply le_S_S.
1033               rewrite > Hcut2.
1034               apply divides_to_le_ord
1035                [apply (divides_b_true_to_lt_O ? ? ? H7).
1036                 rewrite > (times_n_O O).
1037                 apply lt_times
1038                  [assumption|apply lt_O_exp.assumption]
1039                |rewrite > (times_n_O O).
1040                 apply lt_times
1041                  [assumption|apply lt_O_exp.assumption]
1042                |assumption
1043                |apply divides_b_true_to_divides.
1044                 assumption
1045                ]
1046              |unfold ord.
1047               rewrite > (p_ord_exp1 p ? m n)
1048                 [reflexivity
1049                 |assumption
1050                 |assumption
1051                 |apply sym_times
1052                 ]
1053               ]
1054             ]
1055           |assumption
1056           ]
1057         |cut (m = ord (n*(exp p m)) p)
1058           [apply le_S_S.
1059            rewrite > Hcut1.
1060            apply divides_to_le_ord
1061             [apply (divides_b_true_to_lt_O ? ? ? H7).
1062              rewrite > (times_n_O O).
1063              apply lt_times
1064               [assumption|apply lt_O_exp.assumption]
1065             |rewrite > (times_n_O O).
1066              apply lt_times
1067               [assumption|apply lt_O_exp.assumption]
1068             |assumption
1069             |apply divides_b_true_to_divides.
1070              assumption
1071             ]
1072           |unfold ord.
1073            rewrite > (p_ord_exp1 p ? m n)
1074             [reflexivity
1075             |assumption
1076             |assumption
1077             |apply sym_times
1078             ]
1079           ]
1080         ]
1081       |intros.
1082        rewrite > eq_p_ord_times.
1083        rewrite > sym_plus.
1084        apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
1085         [apply lt_plus_l.
1086          apply le_S_S.
1087          cut (m = ord (n*(p \sup m)) p)
1088           [rewrite > Hcut1.
1089            apply divides_to_le_ord
1090             [apply (divides_b_true_to_lt_O ? ? ? H7).
1091              rewrite > (times_n_O O).
1092              apply lt_times
1093               [assumption|apply lt_O_exp.assumption]
1094             |rewrite > (times_n_O O).
1095              apply lt_times
1096               [assumption|apply lt_O_exp.assumption]
1097             |assumption
1098             |apply divides_b_true_to_divides.
1099              assumption
1100             ]
1101           |unfold ord.
1102            rewrite > sym_times.
1103            rewrite > (p_ord_exp1 p ? m n)
1104             [reflexivity
1105             |assumption
1106             |assumption
1107             |reflexivity
1108             ]
1109           ]
1110         |change with (S (ord_rem j p)*S m \le S n*S m).
1111          apply le_times_l.
1112          apply le_S_S.
1113          cut (n = ord_rem (n*(p \sup m)) p)
1114           [rewrite > Hcut1.
1115            apply divides_to_le
1116             [apply lt_O_ord_rem
1117               [elim H1.assumption
1118               |rewrite > (times_n_O O).
1119                apply lt_times
1120                 [assumption|apply lt_O_exp.assumption]
1121               ]
1122             |apply divides_to_divides_ord_rem
1123               [apply (divides_b_true_to_lt_O ? ? ? H7).
1124                rewrite > (times_n_O O).
1125                apply lt_times
1126                 [assumption|apply lt_O_exp.assumption]
1127               |rewrite > (times_n_O O).
1128                apply lt_times
1129                 [assumption|apply lt_O_exp.assumption]
1130               |assumption
1131               |apply divides_b_true_to_divides.
1132                assumption
1133               ]
1134             ]
1135         |unfold ord_rem.
1136          rewrite > sym_times.
1137          rewrite > (p_ord_exp1 p ? m n)
1138           [reflexivity
1139           |assumption
1140           |assumption
1141           |reflexivity
1142           ]
1143         ]
1144       ]
1145     ]
1146   |apply eq_iter_p_gen
1147
1148     [intros.
1149      elim (divides_b (x/S m) n);reflexivity
1150     |intros.reflexivity
1151     ]
1152   ]
1153 |elim H1.apply lt_to_le.assumption
1154 ]
1155 qed.
1156
1157 (*distributive property for iter_p_gen*)
1158 theorem distributive_times_plus_iter_p_gen: \forall A:Type.
1159 \forall plusA: A \to A \to A. \forall basePlusA: A.
1160 \forall timesA: A \to A \to A.
1161 \forall n:nat. \forall k:A. \forall p:nat \to bool. \forall g:nat \to A.
1162 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  basePlusA) = a) \to
1163 (symmetric A timesA) \to (distributive A timesA plusA) \to
1164 (\forall a:A. (timesA a basePlusA) = basePlusA)
1165
1166   \to
1167
1168 ((timesA k (iter_p_gen n p A g basePlusA plusA)) =
1169  (iter_p_gen n p A (\lambda i:nat.(timesA k (g i))) basePlusA plusA)).
1170 intros.
1171 elim n
1172 [ simplify.
1173   apply H5
1174 | cut( (p n1) = true \lor (p n1) = false)
1175   [ elim Hcut
1176     [ rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
1177       rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
1178       rewrite > (H4).
1179       rewrite > (H3 k (g n1)).
1180       apply eq_f.
1181       assumption
1182     | rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
1183       rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
1184       assumption
1185     ]
1186   | elim ((p n1))
1187     [ left.
1188       reflexivity
1189     | right.
1190       reflexivity
1191     ]
1192   ]
1193 ]
1194 qed.
1195
1196 (* old version - proved without theorem iter_p_gen_knm
1197 theorem iter_p_gen_2_eq:
1198 \forall A:Type.
1199 \forall baseA: A.
1200 \forall plusA: A \to A \to A.
1201 (symmetric A plusA) \to
1202 (associative A plusA) \to
1203 (\forall a:A.(plusA a  baseA) = a)\to
1204 \forall g: nat \to nat \to A.
1205 \forall h11,h12,h21,h22: nat \to nat \to nat.
1206 \forall n1,m1,n2,m2.
1207 \forall p11,p21:nat \to bool.
1208 \forall p12,p22:nat \to nat \to bool.
1209 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
1210 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
1211 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
1212 \land h11 i j < n1 \land h12 i j < m1) \to
1213 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
1214 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
1215 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
1216 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
1217 iter_p_gen n1 p11 A
1218      (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA)
1219      baseA plusA =
1220 iter_p_gen n2 p21 A
1221     (\lambda x:nat .iter_p_gen m2 (p22 x) A  (\lambda y. g (h11 x y) (h12 x y)) baseA plusA )
1222     baseA plusA.
1223 intros.
1224 rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
1225 rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
1226 apply sym_eq.
1227 letin h := (\lambda x.(h11 (x/m2) (x\mod m2))*m1 + (h12 (x/m2) (x\mod m2))).
1228 letin h1 := (\lambda x.(h21 (x/m1) (x\mod m1))*m2 + (h22 (x/m1) (x\mod m1))).
1229 apply (trans_eq ? ?
1230   (iter_p_gen (n2*m2) (\lambda x:nat.p21 (x/m2)\land p22 (x/m2) (x\mod m2)) A
1231   (\lambda x:nat.g ((h x)/m1) ((h x)\mod m1)) baseA plusA ))
1232   [clear h.clear h1.
1233    apply eq_iter_p_gen1
1234     [intros.reflexivity
1235     |intros.
1236      cut (O < m2)
1237       [cut (x/m2 < n2)
1238         [cut (x \mod m2 < m2)
1239           [elim (and_true ? ? H6).
1240            elim (H3 ? ? Hcut1 Hcut2 H7 H8).
1241            elim H9.clear H9.
1242            elim H11.clear H11.
1243            elim H9.clear H9.
1244            elim H11.clear H11.
1245            apply eq_f2
1246             [apply sym_eq.
1247              apply div_plus_times.
1248              assumption
1249             | apply sym_eq.
1250               apply mod_plus_times.
1251               assumption
1252             ]
1253           |apply lt_mod_m_m.
1254            assumption
1255           ]
1256         |apply (lt_times_n_to_lt m2)
1257           [assumption
1258           |apply (le_to_lt_to_lt ? x)
1259             [apply (eq_plus_to_le ? ? (x \mod m2)).
1260              apply div_mod.
1261              assumption
1262             |assumption
1263             ]
1264           ]
1265         ]
1266       |apply not_le_to_lt.unfold.intro.
1267        generalize in match H5.
1268        apply (le_n_O_elim ? H7).
1269        rewrite < times_n_O.
1270        apply le_to_not_lt.
1271        apply le_O_n
1272       ]
1273     ]
1274   |apply (eq_iter_p_gen_gh ? ? ? H H1 H2 ? h h1);intros
1275     [cut (O < m2)
1276       [cut (i/m2 < n2)
1277         [cut (i \mod m2 < m2)
1278           [elim (and_true ? ? H6).
1279            elim (H3 ? ? Hcut1 Hcut2 H7 H8).
1280            elim H9.clear H9.
1281            elim H11.clear H11.
1282            elim H9.clear H9.
1283            elim H11.clear H11.
1284            cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 =
1285                  h11 (i/m2) (i\mod m2))
1286             [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
1287                   h12 (i/m2) (i\mod m2))
1288               [rewrite > Hcut3.
1289                rewrite > Hcut4.
1290                rewrite > H9.
1291                rewrite > H15.
1292                reflexivity
1293               |apply mod_plus_times.
1294                assumption
1295               ]
1296             |apply div_plus_times.
1297              assumption
1298             ]
1299           |apply lt_mod_m_m.
1300            assumption
1301           ]
1302         |apply (lt_times_n_to_lt m2)
1303           [assumption
1304           |apply (le_to_lt_to_lt ? i)
1305             [apply (eq_plus_to_le ? ? (i \mod m2)).
1306              apply div_mod.
1307              assumption
1308             |assumption
1309             ]
1310           ]
1311         ]
1312       |apply not_le_to_lt.unfold.intro.
1313        generalize in match H5.
1314        apply (le_n_O_elim ? H7).
1315        rewrite < times_n_O.
1316        apply le_to_not_lt.
1317        apply le_O_n
1318       ]
1319     |cut (O < m2)
1320       [cut (i/m2 < n2)
1321         [cut (i \mod m2 < m2)
1322           [elim (and_true ? ? H6).
1323            elim (H3 ? ? Hcut1 Hcut2 H7 H8).
1324            elim H9.clear H9.
1325            elim H11.clear H11.
1326            elim H9.clear H9.
1327            elim H11.clear H11.
1328            cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 =
1329                  h11 (i/m2) (i\mod m2))
1330             [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
1331                   h12 (i/m2) (i\mod m2))
1332               [rewrite > Hcut3.
1333                rewrite > Hcut4.
1334                rewrite > H13.
1335                rewrite > H14.
1336                apply sym_eq.
1337                apply div_mod.
1338                assumption
1339               |apply mod_plus_times.
1340                assumption
1341               ]
1342             |apply div_plus_times.
1343              assumption
1344             ]
1345           |apply lt_mod_m_m.
1346            assumption
1347           ]
1348         |apply (lt_times_n_to_lt m2)
1349           [assumption
1350           |apply (le_to_lt_to_lt ? i)
1351             [apply (eq_plus_to_le ? ? (i \mod m2)).
1352              apply div_mod.
1353              assumption
1354             |assumption
1355             ]
1356           ]
1357         ]
1358       |apply not_le_to_lt.unfold.intro.
1359        generalize in match H5.
1360        apply (le_n_O_elim ? H7).
1361        rewrite < times_n_O.
1362        apply le_to_not_lt.
1363        apply le_O_n
1364       ]
1365     |cut (O < m2)
1366       [cut (i/m2 < n2)
1367         [cut (i \mod m2 < m2)
1368           [elim (and_true ? ? H6).
1369            elim (H3 ? ? Hcut1 Hcut2 H7 H8).
1370            elim H9.clear H9.
1371            elim H11.clear H11.
1372            elim H9.clear H9.
1373            elim H11.clear H11.
1374            apply lt_times_plus_times
1375             [assumption|assumption]
1376           |apply lt_mod_m_m.
1377            assumption
1378           ]
1379         |apply (lt_times_n_to_lt m2)
1380           [assumption
1381           |apply (le_to_lt_to_lt ? i)
1382             [apply (eq_plus_to_le ? ? (i \mod m2)).
1383              apply div_mod.
1384              assumption
1385             |assumption
1386             ]
1387           ]
1388         ]
1389       |apply not_le_to_lt.unfold.intro.
1390        generalize in match H5.
1391        apply (le_n_O_elim ? H7).
1392        rewrite < times_n_O.
1393        apply le_to_not_lt.
1394        apply le_O_n
1395       ]
1396     |cut (O < m1)
1397       [cut (j/m1 < n1)
1398         [cut (j \mod m1 < m1)
1399           [elim (and_true ? ? H6).
1400            elim (H4 ? ? Hcut1 Hcut2 H7 H8).
1401            elim H9.clear H9.
1402            elim H11.clear H11.
1403            elim H9.clear H9.
1404            elim H11.clear H11.
1405            cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 =
1406                  h21 (j/m1) (j\mod m1))
1407             [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
1408                   h22 (j/m1) (j\mod m1))
1409               [rewrite > Hcut3.
1410                rewrite > Hcut4.
1411                rewrite > H9.
1412                rewrite > H15.
1413                reflexivity
1414               |apply mod_plus_times.
1415                assumption
1416               ]
1417             |apply div_plus_times.
1418              assumption
1419             ]
1420           |apply lt_mod_m_m.
1421            assumption
1422           ]
1423         |apply (lt_times_n_to_lt m1)
1424           [assumption
1425           |apply (le_to_lt_to_lt ? j)
1426             [apply (eq_plus_to_le ? ? (j \mod m1)).
1427              apply div_mod.
1428              assumption
1429             |assumption
1430             ]
1431           ]
1432         ]
1433       |apply not_le_to_lt.unfold.intro.
1434        generalize in match H5.
1435        apply (le_n_O_elim ? H7).
1436        rewrite < times_n_O.
1437        apply le_to_not_lt.
1438        apply le_O_n
1439       ]
1440     |cut (O < m1)
1441       [cut (j/m1 < n1)
1442         [cut (j \mod m1 < m1)
1443           [elim (and_true ? ? H6).
1444            elim (H4 ? ? Hcut1 Hcut2 H7 H8).
1445            elim H9.clear H9.
1446            elim H11.clear H11.
1447            elim H9.clear H9.
1448            elim H11.clear H11.
1449            cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 =
1450                  h21 (j/m1) (j\mod m1))
1451             [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
1452                   h22 (j/m1) (j\mod m1))
1453               [rewrite > Hcut3.
1454                rewrite > Hcut4.
1455                rewrite > H13.
1456                rewrite > H14.
1457                apply sym_eq.
1458                apply div_mod.
1459                assumption
1460               |apply mod_plus_times.
1461                assumption
1462               ]
1463             |apply div_plus_times.
1464              assumption
1465             ]
1466           |apply lt_mod_m_m.
1467            assumption
1468           ]
1469         |apply (lt_times_n_to_lt m1)
1470           [assumption
1471           |apply (le_to_lt_to_lt ? j)
1472             [apply (eq_plus_to_le ? ? (j \mod m1)).
1473              apply div_mod.
1474              assumption
1475             |assumption
1476             ]
1477           ]
1478         ]
1479       |apply not_le_to_lt.unfold.intro.
1480        generalize in match H5.
1481        apply (le_n_O_elim ? H7).
1482        rewrite < times_n_O.
1483        apply le_to_not_lt.
1484        apply le_O_n
1485       ]
1486     |cut (O < m1)
1487       [cut (j/m1 < n1)
1488         [cut (j \mod m1 < m1)
1489           [elim (and_true ? ? H6).
1490            elim (H4 ? ? Hcut1 Hcut2 H7 H8).
1491            elim H9.clear H9.
1492            elim H11.clear H11.
1493            elim H9.clear H9.
1494            elim H11.clear H11.
1495            apply (lt_times_plus_times ? ? ? m2)
1496             [assumption|assumption]
1497           |apply lt_mod_m_m.
1498            assumption
1499           ]
1500         |apply (lt_times_n_to_lt m1)
1501           [assumption
1502           |apply (le_to_lt_to_lt ? j)
1503             [apply (eq_plus_to_le ? ? (j \mod m1)).
1504              apply div_mod.
1505              assumption
1506             |assumption
1507             ]
1508           ]
1509         ]
1510       |apply not_le_to_lt.unfold.intro.
1511        generalize in match H5.
1512        apply (le_n_O_elim ? H7).
1513        rewrite < times_n_O.
1514        apply le_to_not_lt.
1515        apply le_O_n
1516       ]
1517     ]
1518   ]
1519 qed.*)
1520
1521
1522 theorem iter_p_gen_2_eq:
1523 \forall A:Type.
1524 \forall baseA: A.
1525 \forall plusA: A \to A \to A.
1526 (symmetric A plusA) \to
1527 (associative A plusA) \to
1528 (\forall a:A.(plusA a  baseA) = a)\to
1529 \forall g: nat \to nat \to A.
1530 \forall h11,h12,h21,h22: nat \to nat \to nat.
1531 \forall n1,m1,n2,m2.
1532 \forall p11,p21:nat \to bool.
1533 \forall p12,p22:nat \to nat \to bool.
1534 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
1535 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
1536 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
1537 \land h11 i j < n1 \land h12 i j < m1) \to
1538 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
1539 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
1540 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
1541 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
1542 iter_p_gen n1 p11 A
1543      (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA)
1544      baseA plusA =
1545 iter_p_gen n2 p21 A
1546     (\lambda x:nat .iter_p_gen m2 (p22 x) A  (\lambda y. g (h11 x y) (h12 x y)) baseA plusA )
1547     baseA plusA.
1548
1549 intros.
1550 rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
1551 letin ha:= (\lambda x,y.(((h11 x y)*m1) + (h12 x y))).
1552 letin ha12:= (\lambda x.(h21 (x/m1) (x \mod m1))).
1553 letin ha22:= (\lambda x.(h22 (x/m1) (x \mod m1))).
1554
1555 apply (trans_eq ? ?
1556 (iter_p_gen n2 p21 A (\lambda x:nat. iter_p_gen m2 (p22 x) A
1557  (\lambda y:nat.(g (((h11 x y)*m1+(h12 x y))/m1) (((h11 x y)*m1+(h12 x y))\mod m1))) baseA plusA ) baseA plusA))
1558 [
1559   apply (iter_p_gen_knm A baseA plusA H H1 H2 (\lambda e. (g (e/m1) (e \mod m1))) ha ha12 ha22);intros
1560   [ elim (and_true ? ? H6).
1561     cut(O \lt m1)
1562     [ cut(x/m1 < n1)
1563       [ cut((x \mod m1) < m1)
1564         [ elim (H4 ? ? Hcut1 Hcut2 H7 H8).
1565           elim H9.clear H9.
1566           elim H11.clear H11.
1567           elim H9.clear H9.
1568           elim H11.clear H11.
1569           split
1570           [ split
1571             [ split
1572               [ split
1573                 [ assumption
1574                 | assumption
1575                 ]
1576               | rewrite > H14.
1577                 rewrite > H13.
1578                 apply sym_eq.
1579                 apply div_mod.
1580                 assumption
1581               ]
1582             | assumption
1583             ]
1584           | assumption
1585           ]
1586         | apply lt_mod_m_m.
1587           assumption
1588         ]
1589       | apply (lt_times_n_to_lt m1)
1590         [ assumption
1591         | apply (le_to_lt_to_lt ? x)
1592           [ apply (eq_plus_to_le ? ? (x \mod m1)).
1593             apply div_mod.
1594             assumption
1595           | assumption
1596         ]
1597       ]
1598     ]
1599     | apply not_le_to_lt.unfold.intro.
1600       generalize in match H5.
1601       apply (le_n_O_elim ? H9).
1602       rewrite < times_n_O.
1603       apply le_to_not_lt.
1604       apply le_O_n.
1605     ]
1606   | elim (H3 ? ? H5 H6 H7 H8).
1607     elim H9.clear H9.
1608     elim H11.clear H11.
1609     elim H9.clear H9.
1610     elim H11.clear H11.
1611     cut(((h11 i j)*m1 + (h12 i j))/m1 = (h11 i j))
1612     [ cut(((h11 i j)*m1 + (h12 i j)) \mod m1 = (h12 i j))
1613       [ split
1614         [ split
1615           [ split
1616             [ apply true_to_true_to_andb_true
1617               [ rewrite > Hcut.
1618                 assumption
1619               | rewrite > Hcut1.
1620                 rewrite > Hcut.
1621                 assumption
1622               ]
1623             | rewrite > Hcut1.
1624               rewrite > Hcut.
1625               assumption
1626             ]
1627           | rewrite > Hcut1.
1628             rewrite > Hcut.
1629             assumption
1630           ]
1631         | cut(O \lt m1)
1632           [ cut(O \lt n1)
1633             [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
1634               [ apply (lt_plus_r).
1635                 assumption
1636               | rewrite > sym_plus.
1637                 rewrite > (sym_times (h11 i j) m1).
1638                 rewrite > times_n_Sm.
1639                 rewrite > sym_times.
1640                 apply (le_times_l).
1641                 assumption
1642               ]
1643             | apply not_le_to_lt.unfold.intro.
1644               generalize in match H12.
1645               apply (le_n_O_elim ? H11).
1646               apply le_to_not_lt.
1647               apply le_O_n
1648             ]
1649           | apply not_le_to_lt.unfold.intro.
1650             generalize in match H10.
1651             apply (le_n_O_elim ? H11).
1652             apply le_to_not_lt.
1653             apply le_O_n
1654           ]
1655         ]
1656       | rewrite > (mod_plus_times m1 (h11 i j) (h12 i j)).
1657         reflexivity.
1658         assumption
1659       ]
1660     | rewrite > (div_plus_times m1 (h11 i j) (h12 i j)).
1661       reflexivity.
1662       assumption
1663     ]
1664   ]
1665 | apply (eq_iter_p_gen1)
1666   [ intros. reflexivity
1667   | intros.
1668     apply (eq_iter_p_gen1)
1669     [ intros. reflexivity
1670     | intros.
1671       rewrite > (div_plus_times)
1672       [ rewrite > (mod_plus_times)
1673         [ reflexivity
1674         | elim (H3 x x1 H5 H7 H6 H8).
1675           assumption
1676         ]
1677       | elim (H3 x x1 H5 H7 H6 H8).
1678         assumption
1679       ]
1680     ]
1681   ]
1682 ]
1683 qed.
1684
1685 theorem iter_p_gen_iter_p_gen:
1686 \forall A:Type.
1687 \forall baseA: A.
1688 \forall plusA: A \to A \to A.
1689 (symmetric A plusA) \to
1690 (associative A plusA) \to
1691 (\forall a:A.(plusA a  baseA) = a)\to
1692 \forall g: nat \to nat \to A.
1693 \forall n,m.
1694 \forall p11,p21:nat \to bool.
1695 \forall p12,p22:nat \to nat \to bool.
1696 (\forall x,y. x < n \to y < m \to
1697  (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
1698 iter_p_gen n p11 A
1699   (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA)
1700   baseA plusA =
1701 iter_p_gen m p21 A
1702   (\lambda y:nat.iter_p_gen n (p22 y) A  (\lambda x. g x y) baseA plusA )
1703   baseA plusA.
1704 intros.
1705 apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y) (\lambda x,y.x) (\lambda x,y.y) (\lambda x,y.x)
1706        n m m n p11 p21 p12 p22)
1707   [intros.split
1708     [split
1709       [split
1710         [split
1711           [split
1712             [apply (andb_true_true ? (p12 j i)).
1713              rewrite > H3
1714               [rewrite > H6.rewrite > H7.reflexivity
1715               |assumption
1716               |assumption
1717               ]
1718             |apply (andb_true_true_r (p11 j)).
1719              rewrite > H3
1720               [rewrite > H6.rewrite > H7.reflexivity
1721               |assumption
1722               |assumption
1723               ]
1724             ]
1725           |reflexivity
1726           ]
1727         |reflexivity
1728         ]
1729       |assumption
1730       ]
1731     |assumption
1732     ]
1733   |intros.split
1734     [split
1735       [split
1736         [split
1737           [split
1738             [apply (andb_true_true ? (p22 j i)).
1739              rewrite < H3
1740               [rewrite > H6.rewrite > H7.reflexivity
1741               |assumption
1742               |assumption
1743               ]
1744             |apply (andb_true_true_r (p21 j)).
1745              rewrite < H3
1746               [rewrite > H6.rewrite > H7.reflexivity
1747               |assumption
1748               |assumption
1749               ]
1750             ]
1751           |reflexivity
1752           ]
1753         |reflexivity
1754         ]
1755       |assumption
1756       ]
1757     |assumption
1758     ]
1759   ]
1760 qed.
1761
1762
1763