matita/matita/lib/arithmetics/bigops.ma

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