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.ma".
  16
  17 include "nat/primes.ma".
  18 include "nat/ord.ma".
  19
  20
  21
  22 (*a generic definition of summatory indexed over natural numbers:
  23  * n:N is the advanced end in the range of the sommatory
  24  * p: N -> bool is a predicate. if (p i) = true, then (g i) is summed, else it isn't
  25  * A is the type of the elements of the sum.
  26  * g:nat -> A, is the function which associates the nth element of the sum to the nth natural numbers
  27  * baseA (of type A) is the neutral element of A for plusA operation
  28  * plusA: A -> A -> A is the sum over elements in A.
  29  *)
  30 let rec iter_p_gen (n:nat) (p: nat \to bool) (A:Type) (g: nat \to A)
  31    (baseA: A) (plusA: A \to A \to A)  \def
  32   match n with
  33    [ O \Rightarrow baseA
  34    | (S k) \Rightarrow
  35       match p k with
  36       [true \Rightarrow (plusA (g k) (iter_p_gen k p A g baseA plusA))
  37       |false \Rightarrow iter_p_gen k p A g baseA plusA]
  38    ].
  39
  40 theorem true_to_iter_p_gen_Sn:
  41 \forall n:nat. \forall p:nat \to bool. \forall A:Type. \forall g:nat \to A.
  42 \forall baseA:A. \forall plusA: A \to A \to A.
  43 p n = true \to iter_p_gen (S n) p A g baseA plusA =
  44 (plusA (g n) (iter_p_gen n p A g baseA plusA)).
  45 intros.
  46 simplify.
  47 rewrite > H.
  48 reflexivity.
  49 qed.
  50
  51
  52
  53 theorem false_to_iter_p_gen_Sn:
  54 \forall n:nat. \forall p:nat \to bool. \forall A:Type. \forall g:nat \to A.
  55 \forall baseA:A. \forall plusA: A \to A \to A.
  56 p n = false \to iter_p_gen (S n) p A g baseA plusA = iter_p_gen n p A g baseA plusA.
  57 intros.
  58 simplify.
  59 rewrite > H.
  60 reflexivity.
  61 qed.
  62
  63
  64 theorem eq_iter_p_gen: \forall p1,p2:nat \to bool. \forall A:Type.
  65 \forall g1,g2: nat \to A. \forall baseA: A.
  66 \forall plusA: A \to A \to A. \forall n:nat.
  67 (\forall x.  x < n \to p1 x = p2 x) \to
  68 (\forall x.  x < n \to g1 x = g2 x) \to
  69 iter_p_gen n p1 A g1 baseA plusA = iter_p_gen n p2 A g2 baseA plusA.
  70 intros 8.
  71 elim n
  72 [ reflexivity
  73 | apply (bool_elim ? (p1 n1))
  74   [ intro.
  75     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
  76     rewrite > true_to_iter_p_gen_Sn
  77     [ apply eq_f2
  78       [ apply H2.apply le_n.
  79       | apply H
  80         [ intros.apply H1.apply le_S.assumption
  81         | intros.apply H2.apply le_S.assumption
  82         ]
  83       ]
  84     | rewrite < H3.apply sym_eq.apply H1.apply le_n
  85     ]
  86   | intro.
  87     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
  88     rewrite > false_to_iter_p_gen_Sn
  89     [ apply H
  90       [ intros.apply H1.apply le_S.assumption
  91       | intros.apply H2.apply le_S.assumption
  92       ]
  93     | rewrite < H3.apply sym_eq.apply H1.apply le_n
  94     ]
  95   ]
  96 ]
  97 qed.
  98
  99 theorem eq_iter_p_gen1: \forall p1,p2:nat \to bool. \forall A:Type.
 100 \forall g1,g2: nat \to A. \forall baseA: A.
 101 \forall plusA: A \to A \to A.\forall n:nat.
 102 (\forall x.  x < n \to p1 x = p2 x) \to
 103 (\forall x.  x < n \to p1 x = true \to g1 x = g2 x) \to
 104 iter_p_gen n p1 A g1 baseA plusA = iter_p_gen n p2 A g2 baseA plusA.
 105 intros 8.
 106 elim n
 107 [ reflexivity
 108 | apply (bool_elim ? (p1 n1))
 109   [ intro.
 110     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
 111     rewrite > true_to_iter_p_gen_Sn
 112     [ apply eq_f2
 113       [ apply H2
 114         [ apply le_n
 115         | assumption
 116         ]
 117       | apply H
 118         [ intros.apply H1.apply le_S.assumption
 119         | intros.apply H2
 120           [ apply le_S.assumption
 121           | assumption
 122           ]
 123         ]
 124       ]
 125     | rewrite < H3.
 126       apply sym_eq.apply H1.apply le_n
 127     ]
 128   | intro.
 129     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H3).
 130     rewrite > false_to_iter_p_gen_Sn
 131     [ apply H
 132       [ intros.apply H1.apply le_S.assumption
 133       | intros.apply H2
 134         [ apply le_S.assumption
 135         | assumption
 136         ]
 137       ]
 138     | rewrite < H3.apply sym_eq.
 139       apply H1.apply le_n
 140     ]
 141   ]
 142 ]
 143 qed.
 144
 145 theorem iter_p_gen_false: \forall A:Type. \forall g: nat \to A. \forall baseA:A.
 146 \forall plusA: A \to A \to A. \forall n.
 147 iter_p_gen n (\lambda x.false) A g baseA plusA = baseA.
 148 intros.
 149 elim n
 150 [ reflexivity
 151 | simplify.
 152   assumption
 153 ]
 154 qed.
 155
 156 theorem iter_p_gen_plusA: \forall A:Type. \forall n,k:nat.\forall p:nat \to bool.
 157 \forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
 158 (symmetric A plusA) \to (\forall a:A. (plusA a baseA) = a) \to (associative A plusA)
 159 \to
 160 iter_p_gen (k + n) p A g baseA plusA
 161 = (plusA (iter_p_gen k (\lambda x.p (x+n)) A (\lambda x.g (x+n)) baseA plusA)
 162          (iter_p_gen n p A g baseA plusA)).
 163 intros.
 164
 165 elim k
 166 [ rewrite < (plus_n_O n).
 167   simplify.
 168   rewrite > H in \vdash (? ? ? %).
 169   rewrite > (H1 ?).
 170   reflexivity
 171 | apply (bool_elim ? (p (n1+n)))
 172   [ intro.
 173     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
 174     rewrite > (true_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4).
 175     rewrite > (H2 (g (n1 + n)) ? ?).
 176     rewrite < H3.
 177     reflexivity
 178   | intro.
 179     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
 180     rewrite > (false_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4).
 181     assumption
 182   ]
 183 ]
 184 qed.
 185
 186 theorem false_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool.
 187 \forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
 188 n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false)
 189 \to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA.
 190 intros 8.
 191 elim H
 192 [ reflexivity
 193 | simplify.
 194   rewrite > H3
 195   [ simplify.
 196     apply H2.
 197     intros.
 198     apply H3
 199     [ apply H4
 200     | apply le_S.
 201       assumption
 202     ]
 203   | assumption
 204   |apply le_n
 205   ]
 206 ]
 207 qed.
 208
 209 theorem iter_p_gen2 :
 210 \forall n,m:nat.
 211 \forall p1,p2:nat \to bool.
 212 \forall A:Type.
 213 \forall g: nat \to nat \to A.
 214 \forall baseA: A.
 215 \forall plusA: A \to A \to A.
 216 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
 217 \to
 218 iter_p_gen (n*m)
 219   (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
 220   A
 221   (\lambda x.g (div x m) (mod x m))
 222   baseA
 223   plusA  =
 224 iter_p_gen n p1 A
 225   (\lambda x.iter_p_gen m p2 A (g x) baseA plusA)
 226   baseA plusA.
 227 intros.
 228 elim n
 229 [ simplify.
 230   reflexivity
 231 | apply (bool_elim ? (p1 n1))
 232   [ intro.
 233     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
 234     simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
 235     rewrite > iter_p_gen_plusA
 236     [ rewrite < H3.
 237       apply eq_f2
 238       [ apply eq_iter_p_gen
 239         [ intros.
 240           rewrite > sym_plus.
 241           rewrite > (div_plus_times ? ? ? H5).
 242           rewrite > (mod_plus_times ? ? ? H5).
 243           rewrite > H4.
 244           simplify.
 245           reflexivity
 246         | intros.
 247           rewrite > sym_plus.
 248           rewrite > (div_plus_times ? ? ? H5).
 249           rewrite > (mod_plus_times ? ? ? H5).
 250           rewrite > H4.
 251           simplify.reflexivity.
 252         ]
 253       | reflexivity
 254       ]
 255     | assumption
 256     | assumption
 257     | assumption
 258     ]
 259   | intro.
 260     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
 261     simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
 262     rewrite > iter_p_gen_plusA
 263     [ rewrite > H3.
 264       apply (trans_eq ? ? (plusA baseA
 265            (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m p2 A (g x) baseA plusA) baseA plusA )))
 266       [ apply eq_f2
 267         [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
 268           [ apply iter_p_gen_false
 269           | intros.
 270             rewrite > sym_plus.
 271             rewrite > (div_plus_times ? ? ? H5).
 272             rewrite > (mod_plus_times ? ? ? H5).
 273             rewrite > H4.
 274             simplify.reflexivity
 275           | intros.reflexivity.
 276           ]
 277         | reflexivity
 278         ]
 279       | rewrite < H.
 280         rewrite > H2.
 281         reflexivity.
 282       ]
 283     | assumption
 284     | assumption
 285     | assumption
 286     ]
 287   ]
 288 ]
 289 qed.
 290
 291
 292 theorem iter_p_gen2':
 293 \forall n,m:nat.
 294 \forall p1: nat \to bool.
 295 \forall p2: nat \to nat \to bool.
 296 \forall A:Type.
 297 \forall g: nat \to nat \to A.
 298 \forall baseA: A.
 299 \forall plusA: A \to A \to A.
 300 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
 301 \to
 302 iter_p_gen (n*m)
 303   (\lambda x.andb (p1 (div x m)) (p2 (div x m)(mod x m)))
 304   A
 305   (\lambda x.g (div x m) (mod x m))
 306   baseA
 307   plusA  =
 308 iter_p_gen n p1 A
 309   (\lambda x.iter_p_gen m (p2 x) A (g x) baseA plusA)
 310   baseA plusA.
 311 intros.
 312 elim n
 313 [ simplify.
 314   reflexivity
 315 | apply (bool_elim ? (p1 n1))
 316   [ intro.
 317     rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
 318     simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
 319     rewrite > iter_p_gen_plusA
 320     [ rewrite < H3.
 321       apply eq_f2
 322       [ apply eq_iter_p_gen
 323         [ intros.
 324           rewrite > sym_plus.
 325           rewrite > (div_plus_times ? ? ? H5).
 326           rewrite > (mod_plus_times ? ? ? H5).
 327           rewrite > H4.
 328           simplify.
 329           reflexivity
 330         | intros.
 331           rewrite > sym_plus.
 332           rewrite > (div_plus_times ? ? ? H5).
 333           rewrite > (mod_plus_times ? ? ? H5).
 334           rewrite > H4.
 335           simplify.reflexivity.
 336         ]
 337       | reflexivity
 338       ]
 339     | assumption
 340     | assumption
 341     | assumption
 342     ]
 343   | intro.
 344     rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
 345     simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
 346     rewrite > iter_p_gen_plusA
 347     [ rewrite > H3.
 348       apply (trans_eq ? ? (plusA baseA
 349            (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m (p2 x) A (g x) baseA plusA) baseA plusA )))
 350       [ apply eq_f2
 351         [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
 352           [ apply iter_p_gen_false
 353           | intros.
 354             rewrite > sym_plus.
 355             rewrite > (div_plus_times ? ? ? H5).
 356             rewrite > (mod_plus_times ? ? ? H5).
 357             rewrite > H4.
 358             simplify.reflexivity
 359           | intros.reflexivity.
 360           ]
 361         | reflexivity
 362         ]
 363       | rewrite < H.
 364         rewrite > H2.
 365         reflexivity.
 366       ]
 367     | assumption
 368     | assumption
 369     | assumption
 370     ]
 371   ]
 372 ]
 373 qed.
 374
 375 lemma iter_p_gen_gi:
 376 \forall A:Type.
 377 \forall g: nat \to A.
 378 \forall baseA:A.
 379 \forall plusA: A \to A \to A.
 380 \forall n,i:nat.
 381 \forall p:nat \to bool.
 382 (symmetric A plusA) \to  (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
 383   \to
 384
 385 i < n \to p i = true \to
 386 (iter_p_gen n p A g baseA plusA) =
 387 (plusA (g i) (iter_p_gen n (\lambda x:nat. andb (p x) (notb (eqb x i))) A g baseA plusA)).
 388 intros 5.
 389 elim n
 390 [ apply False_ind.
 391   apply (not_le_Sn_O i).
 392   assumption
 393 | apply (bool_elim ? (p n1));intro
 394   [ elim (le_to_or_lt_eq i n1)
 395     [ rewrite > true_to_iter_p_gen_Sn
 396       [ rewrite > true_to_iter_p_gen_Sn
 397         [ rewrite < (H2 (g i) ? ?).
 398           rewrite > (H1 (g i) (g n1)).
 399           rewrite > (H2 (g n1) ? ?).
 400           apply eq_f2
 401           [ reflexivity
 402           | apply H
 403             [ assumption
 404             | assumption
 405             | assumption
 406             | assumption
 407             | assumption
 408             ]
 409           ]
 410         | rewrite > H6.simplify.
 411           change with (notb (eqb n1 i) = notb false).
 412           apply eq_f.
 413           apply not_eq_to_eqb_false.
 414           unfold Not.intro.
 415           apply (lt_to_not_eq ? ? H7).
 416           apply sym_eq.assumption
 417         ]
 418       | assumption
 419       ]
 420     | rewrite > true_to_iter_p_gen_Sn
 421       [ rewrite > H7.
 422         apply eq_f2
 423         [ reflexivity
 424         | rewrite > false_to_iter_p_gen_Sn
 425           [ apply eq_iter_p_gen
 426             [ intros.
 427               elim (p x)
 428               [ simplify.
 429                 change with (notb false = notb (eqb x n1)).
 430                 apply eq_f.
 431                 apply sym_eq.
 432                 apply not_eq_to_eqb_false.
 433                 apply (lt_to_not_eq ? ? H8)
 434               | reflexivity
 435               ]
 436             | intros.
 437               reflexivity
 438             ]
 439           | rewrite > H6.
 440             rewrite > (eq_to_eqb_true ? ? (refl_eq ? n1)).
 441             reflexivity
 442           ]
 443         ]
 444       | assumption
 445       ]
 446     | apply le_S_S_to_le.
 447       assumption
 448     ]
 449   | rewrite > false_to_iter_p_gen_Sn
 450     [ elim (le_to_or_lt_eq i n1)
 451       [ rewrite > false_to_iter_p_gen_Sn
 452         [ apply H
 453           [ assumption
 454           | assumption
 455           | assumption
 456           | assumption
 457           | assumption
 458           ]
 459         | rewrite > H6.reflexivity
 460         ]
 461       | apply False_ind.
 462         apply not_eq_true_false.
 463         rewrite < H5.
 464         rewrite > H7.
 465         assumption
 466       | apply le_S_S_to_le.
 467         assumption
 468       ]
 469     | assumption
 470     ]
 471   ]
 472 ]
 473 qed.
 474
 475
 476 theorem eq_iter_p_gen_gh:
 477 \forall A:Type.
 478 \forall baseA: A.
 479 \forall plusA: A \to A \to A.
 480 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a) \to
 481 \forall g: nat \to A.
 482 \forall h,h1: nat \to nat.
 483 \forall n,n1:nat.
 484 \forall p1,p2:nat \to bool.
 485 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
 486 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
 487 (\forall i. i < n \to p1 i = true \to h i < n1) \to
 488 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
 489 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
 490 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
 491
 492 iter_p_gen n p1 A (\lambda x.g(h x)) baseA plusA =
 493 iter_p_gen n1 (\lambda x.p2 x) A g baseA plusA.
 494 intros 10.
 495 elim n
 496 [ generalize in match H8.
 497   elim n1
 498   [ reflexivity
 499   | apply (bool_elim ? (p2 n2));intro
 500     [ apply False_ind.
 501       apply (not_le_Sn_O (h1 n2)).
 502       apply H10
 503       [ apply le_n
 504       | assumption
 505       ]
 506     | rewrite > false_to_iter_p_gen_Sn
 507       [ apply H9.
 508         intros.
 509         apply H10
 510         [ apply le_S.
 511           apply H12
 512         | assumption
 513         ]
 514       | assumption
 515       ]
 516     ]
 517   ]
 518 | apply (bool_elim ? (p1 n1));intro
 519   [ rewrite > true_to_iter_p_gen_Sn
 520     [ rewrite > (iter_p_gen_gi A g baseA plusA n2 (h n1))
 521       [ apply eq_f2
 522         [ reflexivity
 523         | apply H3
 524           [ intros.
 525             rewrite > H4
 526             [ simplify.
 527               change with ((\not eqb (h i) (h n1))= \not false).
 528               apply eq_f.
 529               apply not_eq_to_eqb_false.
 530               unfold Not.
 531               intro.
 532               apply (lt_to_not_eq ? ? H11).
 533               rewrite < H5
 534               [ rewrite < (H5 n1)
 535                 [ apply eq_f.
 536                   assumption
 537                 | apply le_n
 538                 | assumption
 539                 ]
 540               | apply le_S.
 541                 assumption
 542               | assumption
 543               ]
 544             | apply le_S.assumption
 545             | assumption
 546             ]
 547           | intros.
 548             apply H5
 549             [ apply le_S.
 550               assumption
 551             | assumption
 552             ]
 553           | intros.
 554             apply H6
 555             [ apply le_S.assumption
 556             | assumption
 557             ]
 558           | intros.
 559             apply H7
 560             [ assumption
 561             | generalize in match H12.
 562               elim (p2 j)
 563               [ reflexivity
 564               | assumption
 565               ]
 566             ]
 567           | intros.
 568             apply H8
 569             [ assumption
 570             | generalize in match H12.
 571               elim (p2 j)
 572               [ reflexivity
 573               | assumption
 574               ]
 575             ]
 576           | intros.
 577             elim (le_to_or_lt_eq (h1 j) n1)
 578             [ assumption
 579             | generalize in match H12.
 580               elim (p2 j)
 581               [ simplify in H13.
 582                 absurd (j = (h n1))
 583                 [ rewrite < H13.
 584                   rewrite > H8
 585                   [ reflexivity
 586                   | assumption
 587                   | autobatch
 588                   ]
 589                 | apply eqb_false_to_not_eq.
 590                   generalize in match H14.
 591                   elim (eqb j (h n1))
 592                   [ apply sym_eq.assumption
 593                   | reflexivity
 594                   ]
 595                 ]
 596               | simplify in H14.
 597                 apply False_ind.
 598                 apply not_eq_true_false.
 599                 apply sym_eq.assumption
 600               ]
 601             | apply le_S_S_to_le.
 602               apply H9
 603               [ assumption
 604               | generalize in match H12.
 605                 elim (p2 j)
 606                 [ reflexivity
 607                 | assumption
 608                 ]
 609               ]
 610             ]
 611           ]
 612         ]
 613       | assumption
 614       | assumption
 615       | assumption
 616       | apply H6
 617         [ apply le_n
 618         | assumption
 619         ]
 620       | apply H4
 621         [ apply le_n
 622         | assumption
 623         ]
 624       ]
 625     | assumption
 626     ]
 627   | rewrite > false_to_iter_p_gen_Sn
 628     [ apply H3
 629       [ intros.
 630         apply H4[apply le_S.assumption|assumption]
 631       | intros.
 632         apply H5[apply le_S.assumption|assumption]
 633       | intros.
 634         apply H6[apply le_S.assumption|assumption]
 635       | intros.
 636         apply H7[assumption|assumption]
 637       | intros.
 638         apply H8[assumption|assumption]
 639       | intros.
 640         elim (le_to_or_lt_eq (h1 j) n1)
 641         [ assumption
 642         | absurd (j = (h n1))
 643           [ rewrite < H13.
 644             rewrite > H8
 645             [ reflexivity
 646             | assumption
 647             | assumption
 648             ]
 649           | unfold Not.intro.
 650             apply not_eq_true_false.
 651             rewrite < H10.
 652             rewrite < H13.
 653             rewrite > H7
 654             [ reflexivity
 655             | assumption
 656             | assumption
 657             ]
 658           ]
 659         | apply le_S_S_to_le.
 660           apply H9
 661           [ assumption
 662           | assumption
 663           ]
 664         ]
 665       ]
 666     | assumption
 667     ]
 668   ]
 669 ]
 670 qed.
 671
 672
 673
 674 definition p_ord_times \def
 675 \lambda p,m,x.
 676   match p_ord x p with
 677   [pair q r \Rightarrow r*m+q].
 678
 679 theorem  eq_p_ord_times: \forall p,m,x.
 680 p_ord_times p m x = (ord_rem x p)*m+(ord x p).
 681 intros.unfold p_ord_times. unfold ord_rem.
 682 unfold ord.
 683 elim (p_ord x p).
 684 reflexivity.
 685 qed.
 686
 687 theorem div_p_ord_times:
 688 \forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
 689 intros.rewrite > eq_p_ord_times.
 690 apply div_plus_times.
 691 assumption.
 692 qed.
 693
 694 theorem mod_p_ord_times:
 695 \forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
 696 intros.rewrite > eq_p_ord_times.
 697 apply mod_plus_times.
 698 assumption.
 699 qed.
 700
 701 theorem iter_p_gen_divides:
 702 \forall A:Type.
 703 \forall baseA: A.
 704 \forall plusA: A \to A \to A.
 705 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
 706 \forall g: nat \to A.
 707 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
 708
 709 \to
 710
 711 iter_p_gen (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) A g baseA plusA =
 712 iter_p_gen (S n) (\lambda x.divides_b x n) A
 713   (\lambda x.iter_p_gen (S m) (\lambda y.true) A (\lambda y.g (x*(exp p y))) baseA plusA) baseA plusA.
 714 intros.
 715 cut (O < p)
 716   [rewrite < (iter_p_gen2 ? ? ? ? ? ? ? ? H3 H4 H5).
 717    apply (trans_eq ? ?
 718     (iter_p_gen (S n*S m) (\lambda x:nat.divides_b (x/S m) n) A
 719        (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m)))  baseA plusA) )
 720     [apply sym_eq.
 721      apply (eq_iter_p_gen_gh ? ? ? ? ? ? g ? (p_ord_times p (S m)))
 722       [ assumption
 723       | assumption
 724       | assumption
 725       |intros.
 726        lapply (divides_b_true_to_lt_O ? ? H H7).
 727        apply divides_to_divides_b_true
 728         [rewrite > (times_n_O O).
 729          apply lt_times
 730           [assumption
 731           |apply lt_O_exp.assumption
 732           ]
 733         |apply divides_times
 734           [apply divides_b_true_to_divides.assumption
 735           |apply (witness ? ? (p \sup (m-i \mod (S m)))).
 736            rewrite < exp_plus_times.
 737            apply eq_f.
 738            rewrite > sym_plus.
 739            apply plus_minus_m_m.
 740            autobatch
 741           ]
 742         ]
 743       |intros.
 744        lapply (divides_b_true_to_lt_O ? ? H H7).
 745        unfold p_ord_times.
 746        rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
 747         [change with ((i/S m)*S m+i \mod S m=i).
 748          apply sym_eq.
 749          apply div_mod.
 750          apply lt_O_S
 751         |assumption
 752         |unfold Not.intro.
 753          apply H2.
 754          apply (trans_divides ? (i/ S m))
 755           [assumption|
 756            apply divides_b_true_to_divides;assumption]
 757         |apply sym_times.
 758         ]
 759       |intros.
 760        apply le_S_S.
 761        apply le_times
 762         [apply le_S_S_to_le.
 763          change with ((i/S m) < S n).
 764          apply (lt_times_to_lt_l m).
 765          apply (le_to_lt_to_lt ? i)
 766           [autobatch|assumption]
 767         |apply le_exp
 768           [assumption
 769           |apply le_S_S_to_le.
 770            apply lt_mod_m_m.
 771            apply lt_O_S
 772           ]
 773         ]
 774       |intros.
 775        cut (ord j p < S m)
 776         [rewrite > div_p_ord_times
 777           [apply divides_to_divides_b_true
 778             [apply lt_O_ord_rem
 779              [elim H1.assumption
 780              |apply (divides_b_true_to_lt_O ? ? ? H7).
 781                rewrite > (times_n_O O).
 782                apply lt_times
 783                [assumption|apply lt_O_exp.assumption]
 784              ]
 785            |cut (n = ord_rem (n*(exp p m)) p)
 786               [rewrite > Hcut2.
 787                apply divides_to_divides_ord_rem
 788                 [apply (divides_b_true_to_lt_O ? ? ? H7).
 789                  rewrite > (times_n_O O).
 790                  apply lt_times
 791                  [assumption|apply lt_O_exp.assumption]
 792                  |rewrite > (times_n_O O).
 793                    apply lt_times
 794                   [assumption|apply lt_O_exp.assumption]
 795                |assumption
 796                |apply divides_b_true_to_divides.
 797                 assumption
 798                ]
 799               |unfold ord_rem.
 800               rewrite > (p_ord_exp1 p ? m n)
 801                 [reflexivity
 802                |assumption
 803                 |assumption
 804                |apply sym_times
 805                ]
 806              ]
 807             ]
 808           |assumption
 809           ]
 810         |cut (m = ord (n*(exp p m)) p)
 811           [apply le_S_S.
 812            rewrite > Hcut1.
 813            apply divides_to_le_ord
 814             [apply (divides_b_true_to_lt_O ? ? ? H7).
 815              rewrite > (times_n_O O).
 816              apply lt_times
 817               [assumption|apply lt_O_exp.assumption]
 818             |rewrite > (times_n_O O).
 819              apply lt_times
 820               [assumption|apply lt_O_exp.assumption]
 821             |assumption
 822             |apply divides_b_true_to_divides.
 823              assumption
 824             ]
 825           |unfold ord.
 826            rewrite > (p_ord_exp1 p ? m n)
 827             [reflexivity
 828             |assumption
 829             |assumption
 830             |apply sym_times
 831             ]
 832           ]
 833         ]
 834       |intros.
 835        cut (ord j p < S m)
 836         [rewrite > div_p_ord_times
 837           [rewrite > mod_p_ord_times
 838             [rewrite > sym_times.
 839              apply sym_eq.
 840              apply exp_ord
 841               [elim H1.assumption
 842               |apply (divides_b_true_to_lt_O ? ? ? H7).
 843                rewrite > (times_n_O O).
 844                apply lt_times
 845                 [assumption|apply lt_O_exp.assumption]
 846               ]
 847            |cut (m = ord (n*(exp p m)) p)
 848              [apply le_S_S.
 849               rewrite > Hcut2.
 850               apply divides_to_le_ord
 851                [apply (divides_b_true_to_lt_O ? ? ? H7).
 852                 rewrite > (times_n_O O).
 853                 apply lt_times
 854                  [assumption|apply lt_O_exp.assumption]
 855                |rewrite > (times_n_O O).
 856                 apply lt_times
 857                  [assumption|apply lt_O_exp.assumption]
 858                |assumption
 859                |apply divides_b_true_to_divides.
 860                 assumption
 861                ]
 862              |unfold ord.
 863               rewrite > (p_ord_exp1 p ? m n)
 864                 [reflexivity
 865                 |assumption
 866                 |assumption
 867                 |apply sym_times
 868                 ]
 869               ]
 870             ]
 871           |assumption
 872           ]
 873         |cut (m = ord (n*(exp p m)) p)
 874           [apply le_S_S.
 875            rewrite > Hcut1.
 876            apply divides_to_le_ord
 877             [apply (divides_b_true_to_lt_O ? ? ? H7).
 878              rewrite > (times_n_O O).
 879              apply lt_times
 880               [assumption|apply lt_O_exp.assumption]
 881             |rewrite > (times_n_O O).
 882              apply lt_times
 883               [assumption|apply lt_O_exp.assumption]
 884             |assumption
 885             |apply divides_b_true_to_divides.
 886              assumption
 887             ]
 888           |unfold ord.
 889            rewrite > (p_ord_exp1 p ? m n)
 890             [reflexivity
 891             |assumption
 892             |assumption
 893             |apply sym_times
 894             ]
 895           ]
 896         ]
 897       |intros.
 898        rewrite > eq_p_ord_times.
 899        rewrite > sym_plus.
 900        apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
 901         [apply lt_plus_l.
 902          apply le_S_S.
 903          cut (m = ord (n*(p \sup m)) p)
 904           [rewrite > Hcut1.
 905            apply divides_to_le_ord
 906             [apply (divides_b_true_to_lt_O ? ? ? H7).
 907              rewrite > (times_n_O O).
 908              apply lt_times
 909               [assumption|apply lt_O_exp.assumption]
 910             |rewrite > (times_n_O O).
 911              apply lt_times
 912               [assumption|apply lt_O_exp.assumption]
 913             |assumption
 914             |apply divides_b_true_to_divides.
 915              assumption
 916             ]
 917           |unfold ord.
 918            rewrite > sym_times.
 919            rewrite > (p_ord_exp1 p ? m n)
 920             [reflexivity
 921             |assumption
 922             |assumption
 923             |reflexivity
 924             ]
 925           ]
 926         |change with (S (ord_rem j p)*S m \le S n*S m).
 927          apply le_times_l.
 928          apply le_S_S.
 929          cut (n = ord_rem (n*(p \sup m)) p)
 930           [rewrite > Hcut1.
 931            apply divides_to_le
 932             [apply lt_O_ord_rem
 933               [elim H1.assumption
 934               |rewrite > (times_n_O O).
 935                apply lt_times
 936                 [assumption|apply lt_O_exp.assumption]
 937               ]
 938             |apply divides_to_divides_ord_rem
 939               [apply (divides_b_true_to_lt_O ? ? ? H7).
 940                rewrite > (times_n_O O).
 941                apply lt_times
 942                 [assumption|apply lt_O_exp.assumption]
 943               |rewrite > (times_n_O O).
 944                apply lt_times
 945                 [assumption|apply lt_O_exp.assumption]
 946               |assumption
 947               |apply divides_b_true_to_divides.
 948                assumption
 949               ]
 950             ]
 951         |unfold ord_rem.
 952          rewrite > sym_times.
 953          rewrite > (p_ord_exp1 p ? m n)
 954           [reflexivity
 955           |assumption
 956           |assumption
 957           |reflexivity
 958           ]
 959         ]
 960       ]
 961     ]
 962   |apply eq_iter_p_gen
 963
 964     [intros.
 965      elim (divides_b (x/S m) n);reflexivity
 966     |intros.reflexivity
 967     ]
 968   ]
 969 |elim H1.apply lt_to_le.assumption
 970 ]
 971 qed.
 972
 973 (*distributive property for iter_p_gen*)
 974 theorem distributive_times_plus_iter_p_gen: \forall A:Type.
 975 \forall plusA: A \to A \to A. \forall basePlusA: A.
 976 \forall timesA: A \to A \to A.
 977 \forall n:nat. \forall k:A. \forall p:nat \to bool. \forall g:nat \to A.
 978 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  basePlusA) = a) \to
 979 (symmetric A timesA) \to (distributive A timesA plusA) \to
 980 (\forall a:A. (timesA a basePlusA) = basePlusA)
 981
 982   \to
 983
 984 ((timesA k (iter_p_gen n p A g basePlusA plusA)) =
 985  (iter_p_gen n p A (\lambda i:nat.(timesA k (g i))) basePlusA plusA)).
 986 intros.
 987 elim n
 988 [ simplify.
 989   apply H5
 990 | cut( (p n1) = true \lor (p n1) = false)
 991   [ elim Hcut
 992     [ rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
 993       rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
 994       rewrite > (H4).
 995       rewrite > (H3 k (g n1)).
 996       apply eq_f.
 997       assumption
 998     | rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
 999       rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
1000       assumption
1001     ]
1002   | elim ((p n1))
1003     [ left.
1004       reflexivity
1005     | right.
1006       reflexivity
1007     ]
1008   ]
1009 ]
1010 qed.
1011
1012