matita/matita/lib/arithmetics/sigma_pi.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 (* To be ported
  13 include "arithmetics/bigops.ma".
  14
  15 definition natAop ≝ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n))
  16    (λa,b,c.sym_eq ??? (associative_plus a b c)).
  17
  18 definition natACop ≝ mk_ACop nat 0 natAop commutative_plus.
  19
  20 definition natDop ≝ mk_Dop nat 0 natACop times (λn.(sym_eq ??? (times_n_O n)))
  21    distributive_times_plus.
  22
  23 unification hint  0 ≔ ;
  24    S ≟ natAop
  25 (* ---------------------------------------- *) ⊢
  26    plus ≡ op ? ? S.
  27
  28 unification hint  0 ≔ ;
  29    S ≟ natACop
  30 (* ---------------------------------------- *) ⊢
  31    plus ≡ op ? ? S.
  32
  33 unification hint  0 ≔ ;
  34    S ≟ natDop
  35 (* ---------------------------------------- *) ⊢
  36    plus ≡ sum ? ? S.
  37
  38 unification hint  0 ≔ ;
  39    S ≟ natDop
  40 (* ---------------------------------------- *) ⊢
  41    times ≡ prod ? ? S.
  42
  43 (* Sigma e Pi *)
  44
  45 notation "∑_{ ident i < n | p } f"
  46   with precedence 80
  47 for @{'bigop $n plus 0 (λ${ident i}.$p) (λ${ident i}. $f)}.
  48
  49 notation "∑_{ ident i < n } f"
  50   with precedence 80
  51 for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}.
  52
  53 notation "∑_{ ident j ∈ [a,b[ } f"
  54   with precedence 80
  55 for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
  56   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  57
  58 notation "∑_{ ident j ∈ [a,b[ | p } f"
  59   with precedence 80
  60 for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
  61   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  62
  63 notation "∏_{ ident i < n | p} f"
  64   with precedence 80
  65 for @{'bigop $n times 1 (λ${ident i}.$p) (λ${ident i}. $f)}.
  66
  67 notation "∏_{ ident i < n } f"
  68   with precedence 80
  69 for @{'bigop $n times 1 (λ${ident i}.true) (λ${ident i}. $f)}.
  70
  71 notation "∏_{ ident j ∈ [a,b[ } f"
  72   with precedence 80
  73 for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
  74   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  75
  76 notation "∏_{ ident j ∈ [a,b[ | p } f"
  77   with precedence 80
  78 for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
  79   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  80
  81
  82 (*
  83
  84 definition p_ord_times \def
  85 \lambda p,m,x.
  86   match p_ord x p with
  87   [pair q r \Rightarrow r*m+q].
  88
  89 theorem  eq_p_ord_times: \forall p,m,x.
  90 p_ord_times p m x = (ord_rem x p)*m+(ord x p).
  91 intros.unfold p_ord_times. unfold ord_rem.
  92 unfold ord.
  93 elim (p_ord x p).
  94 reflexivity.
  95 qed.
  96
  97 theorem div_p_ord_times:
  98 \forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
  99 intros.rewrite > eq_p_ord_times.
 100 apply div_plus_times.
 101 assumption.
 102 qed.
 103
 104 theorem mod_p_ord_times:
 105 \forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
 106 intros.rewrite > eq_p_ord_times.
 107 apply mod_plus_times.
 108 assumption.
 109 qed.
 110
 111 lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
 112 intros.
 113 elim (le_to_or_lt_eq O ? (le_O_n m))
 114   [assumption
 115   |apply False_ind.
 116    rewrite < H1 in H.
 117    rewrite < times_n_O in H.
 118    apply (not_le_Sn_O ? H)
 119   ]
 120 qed.
 121
 122 theorem iter_p_gen_knm:
 123 \forall A:Type.
 124 \forall baseA: A.
 125 \forall plusA: A \to A \to A.
 126 (symmetric A plusA) \to
 127 (associative A plusA) \to
 128 (\forall a:A.(plusA a  baseA) = a)\to
 129 \forall g: nat \to A.
 130 \forall h2:nat \to nat \to nat.
 131 \forall h11,h12:nat \to nat.
 132 \forall k,n,m.
 133 \forall p1,p21:nat \to bool.
 134 \forall p22:nat \to nat \to bool.
 135 (\forall x. x < k \to p1 x = true \to
 136 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
 137 \land h2 (h11 x) (h12 x) = x
 138 \land (h11 x) < n \land (h12 x) < m) \to
 139 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
 140 p1 (h2 i j) = true \land
 141 h11 (h2 i j) = i \land h12 (h2 i j) = j
 142 \land h2 i j < k) \to
 143 iter_p_gen k p1 A g baseA plusA =
 144 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.
 145 intros.
 146 rewrite < (iter_p_gen2' n m p21 p22 ? ? ? ? H H1 H2).
 147 apply sym_eq.
 148 apply (eq_iter_p_gen_gh A baseA plusA H H1 H2 g ? (\lambda x.(h11 x)*m+(h12 x)))
 149  [intros.
 150   elim (H4 (i/m) (i \mod m));clear H4
 151    [elim H7.clear H7.
 152     elim H4.clear H4.
 153     assumption
 154    |apply (lt_times_to_lt_div ? ? ? H5)
 155    |apply lt_mod_m_m.
 156     apply (lt_times_to_lt_O ? ? ? H5)
 157    |apply (andb_true_true ? ? H6)
 158    |apply (andb_true_true_r ? ? H6)
 159    ]
 160  |intros.
 161   elim (H4 (i/m) (i \mod m));clear H4
 162    [elim H7.clear H7.
 163     elim H4.clear H4.
 164     rewrite > H10.
 165     rewrite > H9.
 166     apply sym_eq.
 167     apply div_mod.
 168     apply (lt_times_to_lt_O ? ? ? H5)
 169    |apply (lt_times_to_lt_div ? ? ? H5)
 170    |apply lt_mod_m_m.
 171     apply (lt_times_to_lt_O ? ? ? H5)
 172    |apply (andb_true_true ? ? H6)
 173    |apply (andb_true_true_r ? ? H6)
 174    ]
 175  |intros.
 176   elim (H4 (i/m) (i \mod m));clear H4
 177    [elim H7.clear H7.
 178     elim H4.clear H4.
 179     assumption
 180    |apply (lt_times_to_lt_div ? ? ? H5)
 181    |apply lt_mod_m_m.
 182     apply (lt_times_to_lt_O ? ? ? H5)
 183    |apply (andb_true_true ? ? H6)
 184    |apply (andb_true_true_r ? ? H6)
 185    ]
 186  |intros.
 187   elim (H3 j H5 H6).
 188   elim H7.clear H7.
 189   elim H9.clear H9.
 190   elim H7.clear H7.
 191   rewrite > div_plus_times
 192    [rewrite > mod_plus_times
 193      [rewrite > H9.
 194       rewrite > H12.
 195       reflexivity.
 196      |assumption
 197      ]
 198    |assumption
 199    ]
 200  |intros.
 201   elim (H3 j H5 H6).
 202   elim H7.clear H7.
 203   elim H9.clear H9.
 204   elim H7.clear H7.
 205   rewrite > div_plus_times
 206    [rewrite > mod_plus_times
 207      [assumption
 208      |assumption
 209      ]
 210    |assumption
 211    ]
 212  |intros.
 213   elim (H3 j H5 H6).
 214   elim H7.clear H7.
 215   elim H9.clear H9.
 216   elim H7.clear H7.
 217   apply (lt_to_le_to_lt ? ((h11 j)*m+m))
 218    [apply monotonic_lt_plus_r.
 219     assumption
 220    |rewrite > sym_plus.
 221     change with ((S (h11 j)*m) \le n*m).
 222     apply monotonic_le_times_l.
 223     assumption
 224    ]
 225  ]
 226 qed.
 227
 228 theorem iter_p_gen_divides:
 229 \forall A:Type.
 230 \forall baseA: A.
 231 \forall plusA: A \to A \to A.
 232 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
 233 \forall g: nat \to A.
 234 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
 235
 236 \to
 237
 238 iter_p_gen (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) A g baseA plusA =
 239 iter_p_gen (S n) (\lambda x.divides_b x n) A
 240   (\lambda x.iter_p_gen (S m) (\lambda y.true) A (\lambda y.g (x*(exp p y))) baseA plusA) baseA plusA.
 241 intros.
 242 cut (O < p)
 243   [rewrite < (iter_p_gen2 ? ? ? ? ? ? ? ? H3 H4 H5).
 244    apply (trans_eq ? ?
 245     (iter_p_gen (S n*S m) (\lambda x:nat.divides_b (x/S m) n) A
 246        (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m)))  baseA plusA) )
 247     [apply sym_eq.
 248      apply (eq_iter_p_gen_gh ? ? ? ? ? ? g ? (p_ord_times p (S m)))
 249       [ assumption
 250       | assumption
 251       | assumption
 252       |intros.
 253        lapply (divides_b_true_to_lt_O ? ? H H7).
 254        apply divides_to_divides_b_true
 255         [rewrite > (times_n_O O).
 256          apply lt_times
 257           [assumption
 258           |apply lt_O_exp.assumption
 259           ]
 260         |apply divides_times
 261           [apply divides_b_true_to_divides.assumption
 262           |apply (witness ? ? (p \sup (m-i \mod (S m)))).
 263            rewrite < exp_plus_times.
 264            apply eq_f.
 265            rewrite > sym_plus.
 266            apply plus_minus_m_m.
 267            autobatch by le_S_S_to_le, lt_mod_m_m, lt_O_S;
 268           ]
 269         ]
 270       |intros.
 271        lapply (divides_b_true_to_lt_O ? ? H H7).
 272        unfold p_ord_times.
 273        rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
 274         [change with ((i/S m)*S m+i \mod S m=i).
 275          apply sym_eq.
 276          apply div_mod.
 277          apply lt_O_S
 278         |assumption
 279         |unfold Not.intro.
 280          apply H2.
 281          apply (trans_divides ? (i/ S m))
 282           [assumption|
 283            apply divides_b_true_to_divides;assumption]
 284         |apply sym_times.
 285         ]
 286       |intros.
 287        apply le_S_S.
 288        apply le_times
 289         [apply le_S_S_to_le.
 290          change with ((i/S m) < S n).
 291          apply (lt_times_to_lt_l m).
 292          apply (le_to_lt_to_lt ? i);[2:assumption]
 293          autobatch by eq_plus_to_le, div_mod, lt_O_S.
 294         |apply le_exp
 295           [assumption
 296           |apply le_S_S_to_le.
 297            apply lt_mod_m_m.
 298            apply lt_O_S
 299           ]
 300         ]
 301       |intros.
 302        cut (ord j p < S m)
 303         [rewrite > div_p_ord_times
 304           [apply divides_to_divides_b_true
 305             [apply lt_O_ord_rem
 306              [elim H1.assumption
 307              |apply (divides_b_true_to_lt_O ? ? ? H7).
 308                rewrite > (times_n_O O).
 309                apply lt_times
 310                [assumption|apply lt_O_exp.assumption]
 311              ]
 312            |cut (n = ord_rem (n*(exp p m)) p)
 313               [rewrite > Hcut2.
 314                apply divides_to_divides_ord_rem
 315                 [apply (divides_b_true_to_lt_O ? ? ? H7).
 316                  rewrite > (times_n_O O).
 317                  apply lt_times
 318                  [assumption|apply lt_O_exp.assumption]
 319                  |rewrite > (times_n_O O).
 320                    apply lt_times
 321                   [assumption|apply lt_O_exp.assumption]
 322                |assumption
 323                |apply divides_b_true_to_divides.
 324                 assumption
 325                ]
 326               |unfold ord_rem.
 327               rewrite > (p_ord_exp1 p ? m n)
 328                 [reflexivity
 329                |assumption
 330                 |assumption
 331                |apply sym_times
 332                ]
 333              ]
 334             ]
 335           |assumption
 336           ]
 337         |cut (m = ord (n*(exp p m)) p)
 338           [apply le_S_S.
 339            rewrite > Hcut1.
 340            apply divides_to_le_ord
 341             [apply (divides_b_true_to_lt_O ? ? ? H7).
 342              rewrite > (times_n_O O).
 343              apply lt_times
 344               [assumption|apply lt_O_exp.assumption]
 345             |rewrite > (times_n_O O).
 346              apply lt_times
 347               [assumption|apply lt_O_exp.assumption]
 348             |assumption
 349             |apply divides_b_true_to_divides.
 350              assumption
 351             ]
 352           |unfold ord.
 353            rewrite > (p_ord_exp1 p ? m n)
 354             [reflexivity
 355             |assumption
 356             |assumption
 357             |apply sym_times
 358             ]
 359           ]
 360         ]
 361       |intros.
 362        cut (ord j p < S m)
 363         [rewrite > div_p_ord_times
 364           [rewrite > mod_p_ord_times
 365             [rewrite > sym_times.
 366              apply sym_eq.
 367              apply exp_ord
 368               [elim H1.assumption
 369               |apply (divides_b_true_to_lt_O ? ? ? H7).
 370                rewrite > (times_n_O O).
 371                apply lt_times
 372                 [assumption|apply lt_O_exp.assumption]
 373               ]
 374            |cut (m = ord (n*(exp p m)) p)
 375              [apply le_S_S.
 376               rewrite > Hcut2.
 377               apply divides_to_le_ord
 378                [apply (divides_b_true_to_lt_O ? ? ? H7).
 379                 rewrite > (times_n_O O).
 380                 apply lt_times
 381                  [assumption|apply lt_O_exp.assumption]
 382                |rewrite > (times_n_O O).
 383                 apply lt_times
 384                  [assumption|apply lt_O_exp.assumption]
 385                |assumption
 386                |apply divides_b_true_to_divides.
 387                 assumption
 388                ]
 389              |unfold ord.
 390               rewrite > (p_ord_exp1 p ? m n)
 391                 [reflexivity
 392                 |assumption
 393                 |assumption
 394                 |apply sym_times
 395                 ]
 396               ]
 397             ]
 398           |assumption
 399           ]
 400         |cut (m = ord (n*(exp p m)) p)
 401           [apply le_S_S.
 402            rewrite > Hcut1.
 403            apply divides_to_le_ord
 404             [apply (divides_b_true_to_lt_O ? ? ? H7).
 405              rewrite > (times_n_O O).
 406              apply lt_times
 407               [assumption|apply lt_O_exp.assumption]
 408             |rewrite > (times_n_O O).
 409              apply lt_times
 410               [assumption|apply lt_O_exp.assumption]
 411             |assumption
 412             |apply divides_b_true_to_divides.
 413              assumption
 414             ]
 415           |unfold ord.
 416            rewrite > (p_ord_exp1 p ? m n)
 417             [reflexivity
 418             |assumption
 419             |assumption
 420             |apply sym_times
 421             ]
 422           ]
 423         ]
 424       |intros.
 425        rewrite > eq_p_ord_times.
 426        rewrite > sym_plus.
 427        apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
 428         [apply lt_plus_l.
 429          apply le_S_S.
 430          cut (m = ord (n*(p \sup m)) p)
 431           [rewrite > Hcut1.
 432            apply divides_to_le_ord
 433             [apply (divides_b_true_to_lt_O ? ? ? H7).
 434              rewrite > (times_n_O O).
 435              apply lt_times
 436               [assumption|apply lt_O_exp.assumption]
 437             |rewrite > (times_n_O O).
 438              apply lt_times
 439               [assumption|apply lt_O_exp.assumption]
 440             |assumption
 441             |apply divides_b_true_to_divides.
 442              assumption
 443             ]
 444           |unfold ord.
 445            rewrite > sym_times.
 446            rewrite > (p_ord_exp1 p ? m n)
 447             [reflexivity
 448             |assumption
 449             |assumption
 450             |reflexivity
 451             ]
 452           ]
 453         |change with (S (ord_rem j p)*S m \le S n*S m).
 454          apply le_times_l.
 455          apply le_S_S.
 456          cut (n = ord_rem (n*(p \sup m)) p)
 457           [rewrite > Hcut1.
 458            apply divides_to_le
 459             [apply lt_O_ord_rem
 460               [elim H1.assumption
 461               |rewrite > (times_n_O O).
 462                apply lt_times
 463                 [assumption|apply lt_O_exp.assumption]
 464               ]
 465             |apply divides_to_divides_ord_rem
 466               [apply (divides_b_true_to_lt_O ? ? ? H7).
 467                rewrite > (times_n_O O).
 468                apply lt_times
 469                 [assumption|apply lt_O_exp.assumption]
 470               |rewrite > (times_n_O O).
 471                apply lt_times
 472                 [assumption|apply lt_O_exp.assumption]
 473               |assumption
 474               |apply divides_b_true_to_divides.
 475                assumption
 476               ]
 477             ]
 478         |unfold ord_rem.
 479          rewrite > sym_times.
 480          rewrite > (p_ord_exp1 p ? m n)
 481           [reflexivity
 482           |assumption
 483           |assumption
 484           |reflexivity
 485           ]
 486         ]
 487       ]
 488     ]
 489   |apply eq_iter_p_gen
 490
 491     [intros.
 492      elim (divides_b (x/S m) n);reflexivity
 493     |intros.reflexivity
 494     ]
 495   ]
 496 |elim H1.apply lt_to_le.assumption
 497 ]
 498 qed.
 499
 500
 501
 502 theorem iter_p_gen_2_eq:
 503 \forall A:Type.
 504 \forall baseA: A.
 505 \forall plusA: A \to A \to A.
 506 (symmetric A plusA) \to
 507 (associative A plusA) \to
 508 (\forall a:A.(plusA a  baseA) = a)\to
 509 \forall g: nat \to nat \to A.
 510 \forall h11,h12,h21,h22: nat \to nat \to nat.
 511 \forall n1,m1,n2,m2.
 512 \forall p11,p21:nat \to bool.
 513 \forall p12,p22:nat \to nat \to bool.
 514 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
 515 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
 516 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
 517 \land h11 i j < n1 \land h12 i j < m1) \to
 518 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
 519 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
 520 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
 521 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
 522 iter_p_gen n1 p11 A
 523      (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA)
 524      baseA plusA =
 525 iter_p_gen n2 p21 A
 526     (\lambda x:nat .iter_p_gen m2 (p22 x) A  (\lambda y. g (h11 x y) (h12 x y)) baseA plusA )
 527     baseA plusA.
 528
 529 intros.
 530 rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
 531 letin ha:= (\lambda x,y.(((h11 x y)*m1) + (h12 x y))).
 532 letin ha12:= (\lambda x.(h21 (x/m1) (x \mod m1))).
 533 letin ha22:= (\lambda x.(h22 (x/m1) (x \mod m1))).
 534
 535 apply (trans_eq ? ?
 536 (iter_p_gen n2 p21 A (\lambda x:nat. iter_p_gen m2 (p22 x) A
 537  (\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))
 538 [
 539   apply (iter_p_gen_knm A baseA plusA H H1 H2 (\lambda e. (g (e/m1) (e \mod m1))) ha ha12 ha22);intros
 540   [ elim (and_true ? ? H6).
 541     cut(O \lt m1)
 542     [ cut(x/m1 < n1)
 543       [ cut((x \mod m1) < m1)
 544         [ elim (H4 ? ? Hcut1 Hcut2 H7 H8).
 545           elim H9.clear H9.
 546           elim H11.clear H11.
 547           elim H9.clear H9.
 548           elim H11.clear H11.
 549           split
 550           [ split
 551             [ split
 552               [ split
 553                 [ assumption
 554                 | assumption
 555                 ]
 556               | unfold ha.
 557                 unfold ha12.
 558                 unfold ha22.
 559                 rewrite > H14.
 560                 rewrite > H13.
 561                 apply sym_eq.
 562                 apply div_mod.
 563                 assumption
 564               ]
 565             | assumption
 566             ]
 567           | assumption
 568           ]
 569         | apply lt_mod_m_m.
 570           assumption
 571         ]
 572       | apply (lt_times_n_to_lt m1)
 573         [ assumption
 574         | apply (le_to_lt_to_lt ? x)
 575           [ apply (eq_plus_to_le ? ? (x \mod m1)).
 576             apply div_mod.
 577             assumption
 578           | assumption
 579         ]
 580       ]
 581     ]
 582     | apply not_le_to_lt.unfold.intro.
 583       generalize in match H5.
 584       apply (le_n_O_elim ? H9).
 585       rewrite < times_n_O.
 586       apply le_to_not_lt.
 587       apply le_O_n.
 588     ]
 589   | elim (H3 ? ? H5 H6 H7 H8).
 590     elim H9.clear H9.
 591     elim H11.clear H11.
 592     elim H9.clear H9.
 593     elim H11.clear H11.
 594     cut(((h11 i j)*m1 + (h12 i j))/m1 = (h11 i j))
 595     [ cut(((h11 i j)*m1 + (h12 i j)) \mod m1 = (h12 i j))
 596       [ split
 597         [ split
 598           [ split
 599             [ apply true_to_true_to_andb_true
 600               [ rewrite > Hcut.
 601                 assumption
 602               | rewrite > Hcut1.
 603                 rewrite > Hcut.
 604                 assumption
 605               ]
 606             | unfold ha.
 607               unfold ha12.
 608               rewrite > Hcut1.
 609               rewrite > Hcut.
 610               assumption
 611             ]
 612           | unfold ha.
 613             unfold ha22.
 614             rewrite > Hcut1.
 615             rewrite > Hcut.
 616             assumption
 617           ]
 618         | cut(O \lt m1)
 619           [ cut(O \lt n1)
 620             [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
 621               [ unfold ha.
 622                 apply (lt_plus_r).
 623                 assumption
 624               | rewrite > sym_plus.
 625                 rewrite > (sym_times (h11 i j) m1).
 626                 rewrite > times_n_Sm.
 627                 rewrite > sym_times.
 628                 apply (le_times_l).
 629                 assumption
 630               ]
 631             | apply not_le_to_lt.unfold.intro.
 632               generalize in match H12.
 633               apply (le_n_O_elim ? H11).
 634               apply le_to_not_lt.
 635               apply le_O_n
 636             ]
 637           | apply not_le_to_lt.unfold.intro.
 638             generalize in match H10.
 639             apply (le_n_O_elim ? H11).
 640             apply le_to_not_lt.
 641             apply le_O_n
 642           ]
 643         ]
 644       | rewrite > (mod_plus_times m1 (h11 i j) (h12 i j)).
 645         reflexivity.
 646         assumption
 647       ]
 648     | rewrite > (div_plus_times m1 (h11 i j) (h12 i j)).
 649       reflexivity.
 650       assumption
 651     ]
 652   ]
 653 | apply (eq_iter_p_gen1)
 654   [ intros. reflexivity
 655   | intros.
 656     apply (eq_iter_p_gen1)
 657     [ intros. reflexivity
 658     | intros.
 659       rewrite > (div_plus_times)
 660       [ rewrite > (mod_plus_times)
 661         [ reflexivity
 662         | elim (H3 x x1 H5 H7 H6 H8).
 663           assumption
 664         ]
 665       | elim (H3 x x1 H5 H7 H6 H8).
 666         assumption
 667       ]
 668     ]
 669   ]
 670 ]
 671 qed.
 672
 673 theorem iter_p_gen_iter_p_gen:
 674 \forall A:Type.
 675 \forall baseA: A.
 676 \forall plusA: A \to A \to A.
 677 (symmetric A plusA) \to
 678 (associative A plusA) \to
 679 (\forall a:A.(plusA a  baseA) = a)\to
 680 \forall g: nat \to nat \to A.
 681 \forall n,m.
 682 \forall p11,p21:nat \to bool.
 683 \forall p12,p22:nat \to nat \to bool.
 684 (\forall x,y. x < n \to y < m \to
 685  (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
 686 iter_p_gen n p11 A
 687   (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA)
 688   baseA plusA =
 689 iter_p_gen m p21 A
 690   (\lambda y:nat.iter_p_gen n (p22 y) A  (\lambda x. g x y) baseA plusA )
 691   baseA plusA.
 692 intros.
 693 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)
 694        n m m n p11 p21 p12 p22)
 695   [intros.split
 696     [split
 697       [split
 698         [split
 699           [split
 700             [apply (andb_true_true ? (p12 j i)).
 701              rewrite > H3
 702               [rewrite > H6.rewrite > H7.reflexivity
 703               |assumption
 704               |assumption
 705               ]
 706             |apply (andb_true_true_r (p11 j)).
 707              rewrite > H3
 708               [rewrite > H6.rewrite > H7.reflexivity
 709               |assumption
 710               |assumption
 711               ]
 712             ]
 713           |reflexivity
 714           ]
 715         |reflexivity
 716         ]
 717       |assumption
 718       ]
 719     |assumption
 720     ]
 721   |intros.split
 722     [split
 723       [split
 724         [split
 725           [split
 726             [apply (andb_true_true ? (p22 j i)).
 727              rewrite < H3
 728               [rewrite > H6.rewrite > H7.reflexivity
 729               |assumption
 730               |assumption
 731               ]
 732             |apply (andb_true_true_r (p21 j)).
 733              rewrite < H3
 734               [rewrite > H6.rewrite > H7.reflexivity
 735               |assumption
 736               |assumption
 737               ]
 738             ]
 739           |reflexivity
 740           ]
 741         |reflexivity
 742         ]
 743       |assumption
 744       ]
 745     |assumption
 746     ]
 747   ]
 748 qed. *)*)