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