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