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