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