matita/matita/lib/arithmetics/bigops.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "basics/types.ma".
  13 include "arithmetics/div_and_mod.ma".
  14
  15 definition sameF_upto: nat → ∀A.relation(nat→A)  ≝
  16 λk.λA.λf,g.∀i. i < k → f i = g i.
  17
  18 definition sameF_p: nat → (nat → bool) →∀A.relation(nat→A)  ≝
  19 λk,p,A,f,g.∀i. i < k → p i = true → f i = g i.
  20
  21 lemma sameF_upto_le: ∀A,f,g,n,m.
  22  n ≤m → sameF_upto m A f g → sameF_upto n A f g.
  23 #A #f #g #n #m #lenm #samef #i #ltin @samef /2 by lt_to_le_to_lt/
  24 qed.
  25
  26 lemma sameF_p_le: ∀A,p,f,g,n,m.
  27  n ≤m → sameF_p m p A f g → sameF_p n p A f g.
  28 #A #p #f #g #n #m #lenm #samef #i #ltin #pi @samef /2 by lt_to_le_to_lt/
  29 qed.
  30
  31 (*
  32 definition sumF ≝ λA.λf,g:nat → A.λn,i.
  33 if_then_else ? (leb n i) (g (i-n)) (f i).
  34
  35 lemma sumF_unfold: ∀A,f,g,n,i.
  36 sumF A f g n i = if_then_else ? (leb n i) (g (i-n)) (f i).
  37 // qed. *)
  38
  39 definition prodF ≝
  40  λA,B.λf:nat→A.λg:nat→B.λm,x.〈 f(div x m), g(mod x m) 〉.
  41
  42 (* bigop *)
  43 let rec bigop (n:nat) (p:nat → bool) (B:Type[0])
  44    (nil: B) (op: B → B → B)  (f: nat → B) ≝
  45   match n with
  46    [ O ⇒ nil
  47    | S k ⇒
  48       match p k with
  49       [true ⇒ op (f k) (bigop k p B nil op f)
  50       |false ⇒ bigop k p B nil op f]
  51    ].
  52
  53 notation "\big  [ op , nil ]_{ ident i < n | p } f"
  54   with precedence 80
  55 for @{'bigop $n $op $nil (λ${ident i}. $p) (λ${ident i}. $f)}.
  56
  57 notation "\big [ op , nil ]_{ ident i < n } f"
  58   with precedence 80
  59 for @{'bigop $n $op $nil (λ${ident i}.true) (λ${ident i}. $f)}.
  60
  61 interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f).
  62
  63 notation "\big  [ op , nil ]_{ ident j ∈ [a,b[ | p } f"
  64   with precedence 80
  65 for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
  66   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  67
  68 notation "\big  [ op , nil ]_{ ident j ∈ [a,b[ } f"
  69   with precedence 80
  70 for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
  71   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
  72
  73 (* notation "\big  [ op , nil ]_{( term 55) a ≤ ident j < b | p } f"
  74   with precedence 80
  75 for @{\big[$op,$nil]_{${ident j} < ($b-$a) | ((λ${ident j}.$p) (${ident j}+$a))}((λ${ident j}.$f)(${ident j}+$a))}.
  76 *)
  77
  78 interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f).
  79
  80 lemma bigop_Strue: ∀k,p,B,nil,op.∀f:nat→B. p k = true →
  81   \big[op,nil]_{i < S k | p i}(f i) =
  82     op (f k) (\big[op,nil]_{i < k | p i}(f i)).
  83 #k #p #B #nil #op #f #H normalize >H // qed.
  84
  85 lemma bigop_Sfalse: ∀k,p,B,nil,op.∀f:nat→B. p k = false →
  86   \big[op,nil]_{ i < S k | p i}(f i) =
  87     \big[op,nil]_{i < k | p i}(f i).
  88 #k #p #B #nil #op #f #H normalize >H // qed.
  89
  90 lemma same_bigop : ∀k,p1,p2,B,nil,op.∀f,g:nat→B.
  91   sameF_upto k bool p1 p2 → sameF_p k p1 B f g →
  92   \big[op,nil]_{i < k | p1 i}(f i) =
  93     \big[op,nil]_{i < k | p2 i}(g i).
  94 #k #p1 #p2 #B #nil #op #f #g (elim k) //
  95 #n #Hind #samep #samef normalize >Hind /2/
  96 <(samep … (le_n …)) cases(true_or_false (p1 n)) #H1 >H1
  97 normalize // <(samef … (le_n …) H1) //
  98 qed.
  99
 100 theorem pad_bigop: ∀k,n,p,B,nil,op.∀f:nat→B. n ≤ k →
 101 \big[op,nil]_{i < n | p i}(f i)
 102   = \big[op,nil]_{i < k | if leb n i then false else p i}(f i).
 103 #k #n #p #B #nil #op #f #lenk (elim lenk)
 104   [@same_bigop #i #lti // >(not_le_to_leb_false …) /2/
 105   |#j #leup #Hind >bigop_Sfalse >(le_to_leb_true … leup) //
 106   ] qed.
 107
 108 theorem pad_bigop1: ∀k,n,p,B,nil,op.∀f:nat→B. n ≤ k →
 109   (∀i. n ≤ i → i < k → p i = false) →
 110   \big[op,nil]_{i < n | p i}(f i)
 111     = \big[op,nil]_{i < k | p i}(f i).
 112 #k #n #p #B #nil #op #f #lenk (elim lenk)
 113   [#_ @same_bigop #i #lti //
 114   |#j #leup #Hind #Hfalse >bigop_Sfalse
 115     [@Hind #i #leni #ltij @Hfalse // @le_S //
 116     |@Hfalse //
 117     ]
 118   ]
 119 qed.
 120
 121 theorem bigop_false: ∀n,B,nil,op.∀f:nat→B.
 122   \big[op,nil]_{i < n | false }(f i) = nil.
 123 #n #B #nil #op #f elim n // #n1 #Hind
 124 >bigop_Sfalse //
 125 qed.
 126
 127 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
 128   {op :2> A → A → A;
 129    nill:∀a. op nil a = a;
 130    nilr:∀a. op a nil = a;
 131    assoc: ∀a,b,c.op a (op b c) = op (op a b) c
 132   }.
 133
 134 theorem pad_bigop_nil: ∀k,n,p,B,nil.∀op:Aop B nil.∀f:nat→B. n ≤ k →
 135   (∀i. n ≤ i → i < k → p i = false ∨ f i = nil) →
 136   \big[op,nil]_{i < n | p i}(f i)
 137     = \big[op,nil]_{i < k | p i}(f i).
 138 #k #n #p #B #nil #op #f #lenk (elim lenk)
 139   [#_ @same_bigop #i #lti //
 140   |#j #leup #Hind #Hfalse cases (true_or_false (p j)) #Hpj
 141     [>bigop_Strue //
 142      cut (f j = nil)
 143       [cases (Hfalse j leup (le_n … )) // >Hpj #H destruct (H)] #Hfj
 144      >Hfj >nill @Hind #i #leni #ltij
 145      cases (Hfalse i leni (le_S … ltij)) /2/
 146     |>bigop_Sfalse // @Hind #i #leni #ltij
 147      cases (Hfalse i leni (le_S … ltij)) /2/
 148     ]
 149   ]
 150 qed.
 151
 152 theorem bigop_sum: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f,g:nat→B.
 153 op (\big[op,nil]_{i<k1|p1 i}(f i)) \big[op,nil]_{i<k2|p2 i}(g i) =
 154       \big[op,nil]_{i<k1+k2|if leb k2 i then p1 (i-k2) else p2 i}
 155         (if leb k2 i then f (i-k2) else g i).
 156 #k1 #k2 #p1 #p2 #B #nil #op #f #g (elim k1)
 157   [normalize >nill @same_bigop #i #lti
 158    >(lt_to_leb_false … lti) normalize /2/
 159   |#i #Hind normalize <minus_plus_m_m (cases (p1 i))
 160    >(le_to_leb_true … (le_plus_n …)) normalize <Hind //
 161    <assoc //
 162   ]
 163 qed.
 164
 165 lemma plus_minus1: ∀a,b,c. c ≤ b → a + (b -c) = a + b -c.
 166 #a #b #c #lecb @sym_eq @plus_to_minus >(commutative_plus c)
 167 >associative_plus <plus_minus_m_m //
 168 qed.
 169
 170 theorem bigop_I: ∀n,p,B.∀nil.∀op:Aop B nil.∀f:nat→B.
 171 \big[op,nil]_{i∈[0,n[ |p i}(f i) = \big[op,nil]_{i < n|p i}(f i).
 172 #n #p #B #nil #op #f <minus_n_O @same_bigop //
 173 qed.
 174
 175 theorem bigop_sumI: ∀a,b,c,p,B.∀nil.∀op:Aop B nil.∀f:nat→B.
 176 a ≤ b → b ≤ c →
 177 \big[op,nil]_{i∈[a,c[ |p i}(f i) =
 178   op (\big[op,nil]_{i ∈ [b,c[ |p i}(f i))
 179       \big[op,nil]_{i ∈ [a,b[ |p i}(f i).
 180 #a #b # c #p #B #nil #op #f #leab #lebc
 181 >(plus_minus_m_m (c-a) (b-a)) in ⊢ (??%?); /2/
 182 >minus_plus >(commutative_plus a) <plus_minus_m_m //
 183 >bigop_sum (cut (∀i. b -a ≤ i → i+a = i-(b-a)+b))
 184   [#i #lei >plus_minus // <plus_minus1
 185      [@eq_f @sym_eq @plus_to_minus /2/ | /2/]]
 186 #H @same_bigop #i #ltic @leb_elim normalize // #lei <H //
 187 qed.
 188
 189 theorem bigop_a: ∀a,b,B.∀nil.∀op:Aop B nil.∀f:nat→B. a ≤ b →
 190 \big[op,nil]_{i∈[a,S b[ }(f i) =
 191   op (\big[op,nil]_{i ∈ [a,b[ }(f (S i))) (f a).
 192 #a #b #B #nil #op #f #leab
 193 >(bigop_sumI a (S a) (S b)) [|@le_S_S //|//] @eq_f2
 194   [@same_bigop // |<minus_Sn_n normalize @nilr]
 195 qed.
 196
 197 theorem bigop_0: ∀n,B.∀nil.∀op:Aop B nil.∀f:nat→B.
 198 \big[op,nil]_{i < S n}(f i) =
 199   op (\big[op,nil]_{i < n}(f (S i))) (f 0).
 200 #n #B #nil #op #f
 201 <bigop_I >bigop_a [|//] @eq_f2 [|//] <minus_n_O
 202 @same_bigop //
 203 qed.
 204
 205 theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f: nat →nat → B.
 206 \big[op,nil]_{x<k1|p1 x}(\big[op,nil]_{i<k2|p2 x i}(f x i)) =
 207   \big[op,nil]_{i<k1*k2|andb (p1 (i/k2)) (p2 (i/k2) (i \mod k2))}
 208      (f (i/k2) (i \mod k2)).
 209 #k1 #k2 #p1 #p2 #B #nil #op #f (elim k1) //
 210 #n #Hind cases(true_or_false (p1 n)) #Hp1
 211   [>bigop_Strue // >Hind >bigop_sum @same_bigop
 212    #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2 by plus_minus/
 213    #eqi [|#H] >eqi in ⊢ (???%);
 214      >div_plus_times /2 by monotonic_lt_minus_l/
 215      >Hp1 >(mod_plus_times …) /2 by refl, monotonic_lt_minus_l, eq_f/
 216   |>bigop_Sfalse // >Hind >(pad_bigop (S n*k2)) // @same_bigop
 217    #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/
 218    #eqi >eqi in ⊢ (???%); >div_plus_times /2/
 219   ]
 220 qed.
 221
 222 record ACop (A:Type[0]) (nil:A) : Type[0] ≝
 223   {aop :> Aop A nil;
 224    comm: ∀a,b.aop a b = aop b a
 225   }.
 226
 227 lemma bigop_op: ∀k,p,B.∀nil.∀op:ACop B nil.∀f,g: nat → B.
 228 op (\big[op,nil]_{i<k|p i}(f i)) (\big[op,nil]_{i<k|p i}(g i)) =
 229   \big[op,nil]_{i<k|p i}(op (f i) (g i)).
 230 #k #p #B #nil #op #f #g (elim k) [normalize @nill]
 231 -k #k #Hind (cases (true_or_false (p k))) #H
 232   [>bigop_Strue // >bigop_Strue // >bigop_Strue //
 233    normalize <assoc <assoc in ⊢ (???%); @eq_f >assoc >comm in ⊢ (??(????%?)?);
 234    <assoc @eq_f @Hind
 235   |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
 236   ]
 237 qed.
 238
 239 lemma bigop_diff: ∀p,B.∀nil.∀op:ACop B nil.∀f:nat → B.∀i,n.
 240   i < n → p i = true →
 241   \big[op,nil]_{x<n|p x}(f x)=
 242     op (f i) (\big[op,nil]_{x<n|andb(notb(eqb i x))(p x)}(f x)).
 243 #p #B #nil #op #f #i #n (elim n)
 244   [#ltO @False_ind /2/
 245   |#n #Hind #lein #pi cases (le_to_or_lt_eq … (le_S_S_to_le …lein)) #Hi
 246     [cut (andb(notb(eqb i n))(p n) = (p n))
 247       [>(not_eq_to_eqb_false … (lt_to_not_eq … Hi)) //] #Hcut
 248      cases (true_or_false (p n)) #pn
 249       [>bigop_Strue // >bigop_Strue //
 250        normalize >assoc >(comm ?? op (f i) (f n)) <assoc >Hind //
 251       |>bigop_Sfalse // >bigop_Sfalse // >Hind //
 252       ]
 253     |<Hi >bigop_Strue // @eq_f >bigop_Sfalse
 254        [@same_bigop // #k #ltki >not_eq_to_eqb_false /2/
 255        |>eq_to_eqb_true //
 256        ]
 257      ]
 258    ]
 259 qed.
 260
 261 (* range *)
 262 record range (A:Type[0]): Type[0] ≝
 263   {enum:nat→A; upto:nat; filter:nat→bool}.
 264
 265 definition sub_hk: (nat→nat)→(nat→nat)→∀A:Type[0].relation (range A) ≝
 266 λh,k,A,I,J.∀i.i<(upto A I) → (filter A I i)=true →
 267   (h i < upto A J
 268   ∧ filter A J (h i) = true
 269   ∧ k (h i) = i).
 270
 271 definition iso: ∀A:Type[0].relation (range A) ≝
 272   λA,I,J.∃h,k.
 273     (∀i. i < (upto A I) → (filter A I i) = true →
 274        enum A I i = enum A J (h i)) ∧
 275     sub_hk h k A I J ∧ sub_hk k h A J I.
 276
 277 lemma sub_hkO: ∀h,k,A,I,J. upto A I = 0 → sub_hk h k A I J.
 278 #h #k #A #I #J #up0 #i #lti >up0 @False_ind /2/
 279 qed.
 280
 281 lemma sub0_to_false: ∀h,k,A,I,J. upto A I = 0 → sub_hk h k A J I →
 282   ∀i. i < upto A J → filter A J i = false.
 283 #h #k #A #I #J #up0 #sub #i #lti cases(true_or_false (filter A J i)) //
 284 #ptrue (cases (sub i lti ptrue)) * #hi @False_ind /2/
 285 qed.
 286
 287 lemma sub_lt: ∀A,e,p,n,m. n ≤ m →
 288   sub_hk (λx.x) (λx.x) A (mk_range A e n p) (mk_range A e m p).
 289 #A #e #f #n #m #lenm #i #lti #fi % // % /2 by lt_to_le_to_lt/
 290 qed.
 291
 292 theorem transitive_sub: ∀h1,k1,h2,k2,A,I,J,K.
 293   sub_hk h1 k1 A I J → sub_hk h2 k2 A J K →
 294     sub_hk (λx.h2(h1 x)) (λx.k1(k2 x)) A I K.
 295 #h1 #k1 #h2 #k2 #A #I #J #K #sub1 #sub2 #i #lti #fi
 296 cases(sub1 i lti fi) * #lth1i #fh1i #ei
 297 cases(sub2 (h1 i) lth1i fh1i) * #H1 #H2 #H3 % // % //
 298 qed.
 299
 300 theorem bigop_iso: ∀n1,n2,p1,p2,B.∀nil.∀op:ACop B nil.∀f1,f2.
 301   iso B (mk_range B f1 n1 p1) (mk_range B f2 n2 p2) →
 302   \big[op,nil]_{i<n1|p1 i}(f1 i) = \big[op,nil]_{i<n2|p2 i}(f2 i).
 303 #n1 #n2 #p1 #p2 #B #nil #op #f1 #f2 * #h * #k * * #same
 304 @(le_gen ? n1) #i lapply p2 (elim i)
 305   [(elim n2) // #m #Hind #p2 #_ #sub1 #sub2
 306    >bigop_Sfalse
 307     [@(Hind ? (le_O_n ?)) [/2/ | @(transitive_sub … (sub_lt …) sub2) //]
 308     |@(sub0_to_false … sub2) //
 309     ]
 310   |#n #Hind #p2 #ltn #sub1 #sub2 (cut (n ≤n1)) [/2/] #len
 311    cases(true_or_false (p1 n)) #p1n
 312     [>bigop_Strue // (cases (sub1 n (le_n …) p1n)) * #hn #p2hn #eqn
 313      >(bigop_diff … (h n) n2) // >same //
 314      @eq_f @(Hind ? len)
 315       [#i #ltin #p1i (cases (sub1 i (le_S … ltin) p1i)) *
 316        #h1i #p2h1i #eqi % // % // >not_eq_to_eqb_false normalize //
 317        @(not_to_not ??? (lt_to_not_eq ? ? ltin)) //
 318       |#j #ltj #p2j (cases (sub2 j ltj (andb_true_r …p2j))) *
 319        #ltkj #p1kj #eqj % // % //
 320        (cases (le_to_or_lt_eq …(le_S_S_to_le …ltkj))) //
 321        #eqkj @False_ind lapply p2j @eqb_elim
 322        normalize /2/
 323       ]
 324     |>bigop_Sfalse // @(Hind ? len)
 325       [@(transitive_sub … (sub_lt …) sub1) //
 326       |#i #lti #p2i cases(sub2 i lti p2i) * #ltki #p1ki #eqi
 327        % // % // cases(le_to_or_lt_eq …(le_S_S_to_le …ltki)) //
 328        #eqki @False_ind /2/
 329       ]
 330     ]
 331   ]
 332 qed.
 333
 334 (* lemma div_mod_exchange: ∀i,n,m. i < n*m → i\n = i mod m. *)
 335
 336 (* commutation *)
 337 theorem bigop_commute: ∀n,m,p11,p12,p21,p22,B.∀nil.∀op:ACop B nil.∀f.
 338 0 < n → 0 < m →
 339 (∀i,j. i < n → j < m → (p11 i ∧ p12 i j) = (p21 j ∧ p22 i j)) →
 340 \big[op,nil]_{i<n|p11 i}(\big[op,nil]_{j<m|p12 i j}(f i j)) =
 341    \big[op,nil]_{j<m|p21 j}(\big[op,nil]_{i<n|p22 i j}(f i j)).
 342 #n #m #p11 #p12 #p21 #p22 #B #nil #op #f #posn #posm #Heq
 343 >bigop_prod >bigop_prod @bigop_iso
 344 %{(λi.(i\mod m)*n + i/m)} %{(λi.(i\mod n)*m + i/n)} %
 345   [%
 346     [#i #lti #Heq (* whd in ⊢ (???(?(?%?)?)); *) @eq_f2
 347       [@sym_eq @mod_plus_times /2 by lt_times_to_lt_div/
 348       |@sym_eq @div_plus_times /2 by lt_times_to_lt_div/
 349       ]
 350     |#i #lti #Hi
 351      cut ((i\mod m*n+i/m)\mod n=i/m)
 352       [@mod_plus_times @lt_times_to_lt_div //] #H1
 353      cut ((i\mod m*n+i/m)/n=i \mod m)
 354       [@div_plus_times @lt_times_to_lt_div //] #H2
 355      %[%[@(lt_to_le_to_lt ? (i\mod m*n+n))
 356           [whd >plus_n_Sm @monotonic_le_plus_r @lt_times_to_lt_div //
 357           |>commutative_plus @(le_times (S(i \mod m)) m n n) // @lt_mod_m_m //
 358           ]
 359         |lapply (Heq (i/m) (i \mod m) ??)
 360           [@lt_mod_m_m // |@lt_times_to_lt_div //|>Hi >H1 >H2 //]
 361         ]
 362       |>H1 >H2 //
 363       ]
 364     ]
 365   |#i #lti #Hi
 366    cut ((i\mod n*m+i/n)\mod m=i/n)
 367     [@mod_plus_times @lt_times_to_lt_div //] #H1
 368    cut ((i\mod n*m+i/n)/m=i \mod n)
 369     [@div_plus_times @lt_times_to_lt_div //] #H2
 370    %[%[@(lt_to_le_to_lt ? (i\mod n*m+m))
 371         [whd >plus_n_Sm @monotonic_le_plus_r @lt_times_to_lt_div //
 372         |>commutative_plus @(le_times (S(i \mod n)) n m m) // @lt_mod_m_m //
 373         ]
 374       |lapply (Heq (i \mod n) (i/n) ??)
 375         [@lt_times_to_lt_div // |@lt_mod_m_m // |>Hi >H1 >H2 //]
 376       ]
 377     |>H1 >H2 //
 378     ]
 379   ]
 380 qed.
 381
 382 (* distributivity *)
 383
 384 record Dop (A:Type[0]) (nil:A): Type[0] ≝
 385   {sum : ACop A nil;
 386    prod: A → A →A;
 387    null: \forall a. prod a nil = nil;
 388    distr: ∀a,b,c:A. prod a (sum b c) = sum (prod a b) (prod a c)
 389   }.
 390
 391 theorem bigop_distr: ∀n,p,B,nil.∀R:Dop B nil.∀f,a.
 392   let aop ≝ sum B nil R in
 393   let mop ≝ prod B nil R in
 394   mop a \big[aop,nil]_{i<n|p i}(f i) =
 395    \big[aop,nil]_{i<n|p i}(mop a (f i)).
 396 #n #p #B #nil #R #f #a normalize (elim n) [@null]
 397 #n #Hind (cases (true_or_false (p n))) #H
 398   [>bigop_Strue // >bigop_Strue // >(distr B nil R) >Hind //
 399   |>bigop_Sfalse // >bigop_Sfalse //
 400   ]
 401 qed.
 402
 403 (* Sigma e Pi *)
 404
 405 notation "∑_{ ident i < n | p } f"
 406   with precedence 80
 407 for @{'bigop $n plus 0 (λ${ident i}. $p) (λ${ident i}. $f)}.
 408
 409 notation "∑_{ ident i < n } f"
 410   with precedence 80
 411 for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}.
 412
 413 notation "∑_{ ident j ∈ [a,b[ } f"
 414   with precedence 80
 415 for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
 416   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
 417
 418 notation "∑_{ ident j ∈ [a,b[ | p } f"
 419   with precedence 80
 420 for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
 421   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
 422
 423 notation "∏_{ ident i < n | p} f"
 424   with precedence 80
 425 for @{'bigop $n times 1 (λ${ident i}.$p) (λ${ident i}. $f)}.
 426
 427 notation "∏_{ ident i < n } f"
 428   with precedence 80
 429 for @{'bigop $n times 1 (λ${ident i}.true) (λ${ident i}. $f)}.
 430
 431 notation "∏_{ ident j ∈ [a,b[ } f"
 432   with precedence 80
 433 for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
 434   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
 435
 436 notation "∏_{ ident j ∈ [a,b[ | p } f"
 437   with precedence 80
 438 for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
 439   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
 440
 441
 442 (*
 443
 444 definition p_ord_times \def
 445 \lambda p,m,x.
 446   match p_ord x p with
 447   [pair q r \Rightarrow r*m+q].
 448
 449 theorem  eq_p_ord_times: \forall p,m,x.
 450 p_ord_times p m x = (ord_rem x p)*m+(ord x p).
 451 intros.unfold p_ord_times. unfold ord_rem.
 452 unfold ord.
 453 elim (p_ord x p).
 454 reflexivity.
 455 qed.
 456
 457 theorem div_p_ord_times:
 458 \forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
 459 intros.rewrite > eq_p_ord_times.
 460 apply div_plus_times.
 461 assumption.
 462 qed.
 463
 464 theorem mod_p_ord_times:
 465 \forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
 466 intros.rewrite > eq_p_ord_times.
 467 apply mod_plus_times.
 468 assumption.
 469 qed.
 470
 471 lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
 472 intros.
 473 elim (le_to_or_lt_eq O ? (le_O_n m))
 474   [assumption
 475   |apply False_ind.
 476    rewrite < H1 in H.
 477    rewrite < times_n_O in H.
 478    apply (not_le_Sn_O ? H)
 479   ]
 480 qed.
 481
 482 theorem iter_p_gen_knm:
 483 \forall A:Type.
 484 \forall baseA: A.
 485 \forall plusA: A \to A \to A.
 486 (symmetric A plusA) \to
 487 (associative A plusA) \to
 488 (\forall a:A.(plusA a  baseA) = a)\to
 489 \forall g: nat \to A.
 490 \forall h2:nat \to nat \to nat.
 491 \forall h11,h12:nat \to nat.
 492 \forall k,n,m.
 493 \forall p1,p21:nat \to bool.
 494 \forall p22:nat \to nat \to bool.
 495 (\forall x. x < k \to p1 x = true \to
 496 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
 497 \land h2 (h11 x) (h12 x) = x
 498 \land (h11 x) < n \land (h12 x) < m) \to
 499 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
 500 p1 (h2 i j) = true \land
 501 h11 (h2 i j) = i \land h12 (h2 i j) = j
 502 \land h2 i j < k) \to
 503 iter_p_gen k p1 A g baseA plusA =
 504 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.
 505 intros.
 506 rewrite < (iter_p_gen2' n m p21 p22 ? ? ? ? H H1 H2).
 507 apply sym_eq.
 508 apply (eq_iter_p_gen_gh A baseA plusA H H1 H2 g ? (\lambda x.(h11 x)*m+(h12 x)))
 509  [intros.
 510   elim (H4 (i/m) (i \mod m));clear H4
 511    [elim H7.clear H7.
 512     elim H4.clear H4.
 513     assumption
 514    |apply (lt_times_to_lt_div ? ? ? H5)
 515    |apply lt_mod_m_m.
 516     apply (lt_times_to_lt_O ? ? ? H5)
 517    |apply (andb_true_true ? ? H6)
 518    |apply (andb_true_true_r ? ? H6)
 519    ]
 520  |intros.
 521   elim (H4 (i/m) (i \mod m));clear H4
 522    [elim H7.clear H7.
 523     elim H4.clear H4.
 524     rewrite > H10.
 525     rewrite > H9.
 526     apply sym_eq.
 527     apply div_mod.
 528     apply (lt_times_to_lt_O ? ? ? H5)
 529    |apply (lt_times_to_lt_div ? ? ? H5)
 530    |apply lt_mod_m_m.
 531     apply (lt_times_to_lt_O ? ? ? H5)
 532    |apply (andb_true_true ? ? H6)
 533    |apply (andb_true_true_r ? ? H6)
 534    ]
 535  |intros.
 536   elim (H4 (i/m) (i \mod m));clear H4
 537    [elim H7.clear H7.
 538     elim H4.clear H4.
 539     assumption
 540    |apply (lt_times_to_lt_div ? ? ? H5)
 541    |apply lt_mod_m_m.
 542     apply (lt_times_to_lt_O ? ? ? H5)
 543    |apply (andb_true_true ? ? H6)
 544    |apply (andb_true_true_r ? ? H6)
 545    ]
 546  |intros.
 547   elim (H3 j H5 H6).
 548   elim H7.clear H7.
 549   elim H9.clear H9.
 550   elim H7.clear H7.
 551   rewrite > div_plus_times
 552    [rewrite > mod_plus_times
 553      [rewrite > H9.
 554       rewrite > H12.
 555       reflexivity.
 556      |assumption
 557      ]
 558    |assumption
 559    ]
 560  |intros.
 561   elim (H3 j H5 H6).
 562   elim H7.clear H7.
 563   elim H9.clear H9.
 564   elim H7.clear H7.
 565   rewrite > div_plus_times
 566    [rewrite > mod_plus_times
 567      [assumption
 568      |assumption
 569      ]
 570    |assumption
 571    ]
 572  |intros.
 573   elim (H3 j H5 H6).
 574   elim H7.clear H7.
 575   elim H9.clear H9.
 576   elim H7.clear H7.
 577   apply (lt_to_le_to_lt ? ((h11 j)*m+m))
 578    [apply monotonic_lt_plus_r.
 579     assumption
 580    |rewrite > sym_plus.
 581     change with ((S (h11 j)*m) \le n*m).
 582     apply monotonic_le_times_l.
 583     assumption
 584    ]
 585  ]
 586 qed.
 587
 588 theorem iter_p_gen_divides:
 589 \forall A:Type.
 590 \forall baseA: A.
 591 \forall plusA: A \to A \to A.
 592 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
 593 \forall g: nat \to A.
 594 (symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a)
 595
 596 \to
 597
 598 iter_p_gen (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) A g baseA plusA =
 599 iter_p_gen (S n) (\lambda x.divides_b x n) A
 600   (\lambda x.iter_p_gen (S m) (\lambda y.true) A (\lambda y.g (x*(exp p y))) baseA plusA) baseA plusA.
 601 intros.
 602 cut (O < p)
 603   [rewrite < (iter_p_gen2 ? ? ? ? ? ? ? ? H3 H4 H5).
 604    apply (trans_eq ? ?
 605     (iter_p_gen (S n*S m) (\lambda x:nat.divides_b (x/S m) n) A
 606        (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m)))  baseA plusA) )
 607     [apply sym_eq.
 608      apply (eq_iter_p_gen_gh ? ? ? ? ? ? g ? (p_ord_times p (S m)))
 609       [ assumption
 610       | assumption
 611       | assumption
 612       |intros.
 613        lapply (divides_b_true_to_lt_O ? ? H H7).
 614        apply divides_to_divides_b_true
 615         [rewrite > (times_n_O O).
 616          apply lt_times
 617           [assumption
 618           |apply lt_O_exp.assumption
 619           ]
 620         |apply divides_times
 621           [apply divides_b_true_to_divides.assumption
 622           |apply (witness ? ? (p \sup (m-i \mod (S m)))).
 623            rewrite < exp_plus_times.
 624            apply eq_f.
 625            rewrite > sym_plus.
 626            apply plus_minus_m_m.
 627            autobatch by le_S_S_to_le, lt_mod_m_m, lt_O_S;
 628           ]
 629         ]
 630       |intros.
 631        lapply (divides_b_true_to_lt_O ? ? H H7).
 632        unfold p_ord_times.
 633        rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
 634         [change with ((i/S m)*S m+i \mod S m=i).
 635          apply sym_eq.
 636          apply div_mod.
 637          apply lt_O_S
 638         |assumption
 639         |unfold Not.intro.
 640          apply H2.
 641          apply (trans_divides ? (i/ S m))
 642           [assumption|
 643            apply divides_b_true_to_divides;assumption]
 644         |apply sym_times.
 645         ]
 646       |intros.
 647        apply le_S_S.
 648        apply le_times
 649         [apply le_S_S_to_le.
 650          change with ((i/S m) < S n).
 651          apply (lt_times_to_lt_l m).
 652          apply (le_to_lt_to_lt ? i);[2:assumption]
 653          autobatch by eq_plus_to_le, div_mod, lt_O_S.
 654         |apply le_exp
 655           [assumption
 656           |apply le_S_S_to_le.
 657            apply lt_mod_m_m.
 658            apply lt_O_S
 659           ]
 660         ]
 661       |intros.
 662        cut (ord j p < S m)
 663         [rewrite > div_p_ord_times
 664           [apply divides_to_divides_b_true
 665             [apply lt_O_ord_rem
 666              [elim H1.assumption
 667              |apply (divides_b_true_to_lt_O ? ? ? H7).
 668                rewrite > (times_n_O O).
 669                apply lt_times
 670                [assumption|apply lt_O_exp.assumption]
 671              ]
 672            |cut (n = ord_rem (n*(exp p m)) p)
 673               [rewrite > Hcut2.
 674                apply divides_to_divides_ord_rem
 675                 [apply (divides_b_true_to_lt_O ? ? ? H7).
 676                  rewrite > (times_n_O O).
 677                  apply lt_times
 678                  [assumption|apply lt_O_exp.assumption]
 679                  |rewrite > (times_n_O O).
 680                    apply lt_times
 681                   [assumption|apply lt_O_exp.assumption]
 682                |assumption
 683                |apply divides_b_true_to_divides.
 684                 assumption
 685                ]
 686               |unfold ord_rem.
 687               rewrite > (p_ord_exp1 p ? m n)
 688                 [reflexivity
 689                |assumption
 690                 |assumption
 691                |apply sym_times
 692                ]
 693              ]
 694             ]
 695           |assumption
 696           ]
 697         |cut (m = ord (n*(exp p m)) p)
 698           [apply le_S_S.
 699            rewrite > Hcut1.
 700            apply divides_to_le_ord
 701             [apply (divides_b_true_to_lt_O ? ? ? H7).
 702              rewrite > (times_n_O O).
 703              apply lt_times
 704               [assumption|apply lt_O_exp.assumption]
 705             |rewrite > (times_n_O O).
 706              apply lt_times
 707               [assumption|apply lt_O_exp.assumption]
 708             |assumption
 709             |apply divides_b_true_to_divides.
 710              assumption
 711             ]
 712           |unfold ord.
 713            rewrite > (p_ord_exp1 p ? m n)
 714             [reflexivity
 715             |assumption
 716             |assumption
 717             |apply sym_times
 718             ]
 719           ]
 720         ]
 721       |intros.
 722        cut (ord j p < S m)
 723         [rewrite > div_p_ord_times
 724           [rewrite > mod_p_ord_times
 725             [rewrite > sym_times.
 726              apply sym_eq.
 727              apply exp_ord
 728               [elim H1.assumption
 729               |apply (divides_b_true_to_lt_O ? ? ? H7).
 730                rewrite > (times_n_O O).
 731                apply lt_times
 732                 [assumption|apply lt_O_exp.assumption]
 733               ]
 734            |cut (m = ord (n*(exp p m)) p)
 735              [apply le_S_S.
 736               rewrite > Hcut2.
 737               apply divides_to_le_ord
 738                [apply (divides_b_true_to_lt_O ? ? ? H7).
 739                 rewrite > (times_n_O O).
 740                 apply lt_times
 741                  [assumption|apply lt_O_exp.assumption]
 742                |rewrite > (times_n_O O).
 743                 apply lt_times
 744                  [assumption|apply lt_O_exp.assumption]
 745                |assumption
 746                |apply divides_b_true_to_divides.
 747                 assumption
 748                ]
 749              |unfold ord.
 750               rewrite > (p_ord_exp1 p ? m n)
 751                 [reflexivity
 752                 |assumption
 753                 |assumption
 754                 |apply sym_times
 755                 ]
 756               ]
 757             ]
 758           |assumption
 759           ]
 760         |cut (m = ord (n*(exp p m)) p)
 761           [apply le_S_S.
 762            rewrite > Hcut1.
 763            apply divides_to_le_ord
 764             [apply (divides_b_true_to_lt_O ? ? ? H7).
 765              rewrite > (times_n_O O).
 766              apply lt_times
 767               [assumption|apply lt_O_exp.assumption]
 768             |rewrite > (times_n_O O).
 769              apply lt_times
 770               [assumption|apply lt_O_exp.assumption]
 771             |assumption
 772             |apply divides_b_true_to_divides.
 773              assumption
 774             ]
 775           |unfold ord.
 776            rewrite > (p_ord_exp1 p ? m n)
 777             [reflexivity
 778             |assumption
 779             |assumption
 780             |apply sym_times
 781             ]
 782           ]
 783         ]
 784       |intros.
 785        rewrite > eq_p_ord_times.
 786        rewrite > sym_plus.
 787        apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
 788         [apply lt_plus_l.
 789          apply le_S_S.
 790          cut (m = ord (n*(p \sup m)) p)
 791           [rewrite > Hcut1.
 792            apply divides_to_le_ord
 793             [apply (divides_b_true_to_lt_O ? ? ? H7).
 794              rewrite > (times_n_O O).
 795              apply lt_times
 796               [assumption|apply lt_O_exp.assumption]
 797             |rewrite > (times_n_O O).
 798              apply lt_times
 799               [assumption|apply lt_O_exp.assumption]
 800             |assumption
 801             |apply divides_b_true_to_divides.
 802              assumption
 803             ]
 804           |unfold ord.
 805            rewrite > sym_times.
 806            rewrite > (p_ord_exp1 p ? m n)
 807             [reflexivity
 808             |assumption
 809             |assumption
 810             |reflexivity
 811             ]
 812           ]
 813         |change with (S (ord_rem j p)*S m \le S n*S m).
 814          apply le_times_l.
 815          apply le_S_S.
 816          cut (n = ord_rem (n*(p \sup m)) p)
 817           [rewrite > Hcut1.
 818            apply divides_to_le
 819             [apply lt_O_ord_rem
 820               [elim H1.assumption
 821               |rewrite > (times_n_O O).
 822                apply lt_times
 823                 [assumption|apply lt_O_exp.assumption]
 824               ]
 825             |apply divides_to_divides_ord_rem
 826               [apply (divides_b_true_to_lt_O ? ? ? H7).
 827                rewrite > (times_n_O O).
 828                apply lt_times
 829                 [assumption|apply lt_O_exp.assumption]
 830               |rewrite > (times_n_O O).
 831                apply lt_times
 832                 [assumption|apply lt_O_exp.assumption]
 833               |assumption
 834               |apply divides_b_true_to_divides.
 835                assumption
 836               ]
 837             ]
 838         |unfold ord_rem.
 839          rewrite > sym_times.
 840          rewrite > (p_ord_exp1 p ? m n)
 841           [reflexivity
 842           |assumption
 843           |assumption
 844           |reflexivity
 845           ]
 846         ]
 847       ]
 848     ]
 849   |apply eq_iter_p_gen
 850
 851     [intros.
 852      elim (divides_b (x/S m) n);reflexivity
 853     |intros.reflexivity
 854     ]
 855   ]
 856 |elim H1.apply lt_to_le.assumption
 857 ]
 858 qed.
 859
 860
 861
 862 theorem iter_p_gen_2_eq:
 863 \forall A:Type.
 864 \forall baseA: A.
 865 \forall plusA: A \to A \to A.
 866 (symmetric A plusA) \to
 867 (associative A plusA) \to
 868 (\forall a:A.(plusA a  baseA) = a)\to
 869 \forall g: nat \to nat \to A.
 870 \forall h11,h12,h21,h22: nat \to nat \to nat.
 871 \forall n1,m1,n2,m2.
 872 \forall p11,p21:nat \to bool.
 873 \forall p12,p22:nat \to nat \to bool.
 874 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
 875 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
 876 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
 877 \land h11 i j < n1 \land h12 i j < m1) \to
 878 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
 879 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
 880 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
 881 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
 882 iter_p_gen n1 p11 A
 883      (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA)
 884      baseA plusA =
 885 iter_p_gen n2 p21 A
 886     (\lambda x:nat .iter_p_gen m2 (p22 x) A  (\lambda y. g (h11 x y) (h12 x y)) baseA plusA )
 887     baseA plusA.
 888
 889 intros.
 890 rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
 891 letin ha:= (\lambda x,y.(((h11 x y)*m1) + (h12 x y))).
 892 letin ha12:= (\lambda x.(h21 (x/m1) (x \mod m1))).
 893 letin ha22:= (\lambda x.(h22 (x/m1) (x \mod m1))).
 894
 895 apply (trans_eq ? ?
 896 (iter_p_gen n2 p21 A (\lambda x:nat. iter_p_gen m2 (p22 x) A
 897  (\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))
 898 [
 899   apply (iter_p_gen_knm A baseA plusA H H1 H2 (\lambda e. (g (e/m1) (e \mod m1))) ha ha12 ha22);intros
 900   [ elim (and_true ? ? H6).
 901     cut(O \lt m1)
 902     [ cut(x/m1 < n1)
 903       [ cut((x \mod m1) < m1)
 904         [ elim (H4 ? ? Hcut1 Hcut2 H7 H8).
 905           elim H9.clear H9.
 906           elim H11.clear H11.
 907           elim H9.clear H9.
 908           elim H11.clear H11.
 909           split
 910           [ split
 911             [ split
 912               [ split
 913                 [ assumption
 914                 | assumption
 915                 ]
 916               | unfold ha.
 917                 unfold ha12.
 918                 unfold ha22.
 919                 rewrite > H14.
 920                 rewrite > H13.
 921                 apply sym_eq.
 922                 apply div_mod.
 923                 assumption
 924               ]
 925             | assumption
 926             ]
 927           | assumption
 928           ]
 929         | apply lt_mod_m_m.
 930           assumption
 931         ]
 932       | apply (lt_times_n_to_lt m1)
 933         [ assumption
 934         | apply (le_to_lt_to_lt ? x)
 935           [ apply (eq_plus_to_le ? ? (x \mod m1)).
 936             apply div_mod.
 937             assumption
 938           | assumption
 939         ]
 940       ]
 941     ]
 942     | apply not_le_to_lt.unfold.intro.
 943       generalize in match H5.
 944       apply (le_n_O_elim ? H9).
 945       rewrite < times_n_O.
 946       apply le_to_not_lt.
 947       apply le_O_n.
 948     ]
 949   | elim (H3 ? ? H5 H6 H7 H8).
 950     elim H9.clear H9.
 951     elim H11.clear H11.
 952     elim H9.clear H9.
 953     elim H11.clear H11.
 954     cut(((h11 i j)*m1 + (h12 i j))/m1 = (h11 i j))
 955     [ cut(((h11 i j)*m1 + (h12 i j)) \mod m1 = (h12 i j))
 956       [ split
 957         [ split
 958           [ split
 959             [ apply true_to_true_to_andb_true
 960               [ rewrite > Hcut.
 961                 assumption
 962               | rewrite > Hcut1.
 963                 rewrite > Hcut.
 964                 assumption
 965               ]
 966             | unfold ha.
 967               unfold ha12.
 968               rewrite > Hcut1.
 969               rewrite > Hcut.
 970               assumption
 971             ]
 972           | unfold ha.
 973             unfold ha22.
 974             rewrite > Hcut1.
 975             rewrite > Hcut.
 976             assumption
 977           ]
 978         | cut(O \lt m1)
 979           [ cut(O \lt n1)
 980             [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
 981               [ unfold ha.
 982                 apply (lt_plus_r).
 983                 assumption
 984               | rewrite > sym_plus.
 985                 rewrite > (sym_times (h11 i j) m1).
 986                 rewrite > times_n_Sm.
 987                 rewrite > sym_times.
 988                 apply (le_times_l).
 989                 assumption
 990               ]
 991             | apply not_le_to_lt.unfold.intro.
 992               generalize in match H12.
 993               apply (le_n_O_elim ? H11).
 994               apply le_to_not_lt.
 995               apply le_O_n
 996             ]
 997           | apply not_le_to_lt.unfold.intro.
 998             generalize in match H10.
 999             apply (le_n_O_elim ? H11).
1000             apply le_to_not_lt.
1001             apply le_O_n
1002           ]
1003         ]
1004       | rewrite > (mod_plus_times m1 (h11 i j) (h12 i j)).
1005         reflexivity.
1006         assumption
1007       ]
1008     | rewrite > (div_plus_times m1 (h11 i j) (h12 i j)).
1009       reflexivity.
1010       assumption
1011     ]
1012   ]
1013 | apply (eq_iter_p_gen1)
1014   [ intros. reflexivity
1015   | intros.
1016     apply (eq_iter_p_gen1)
1017     [ intros. reflexivity
1018     | intros.
1019       rewrite > (div_plus_times)
1020       [ rewrite > (mod_plus_times)
1021         [ reflexivity
1022         | elim (H3 x x1 H5 H7 H6 H8).
1023           assumption
1024         ]
1025       | elim (H3 x x1 H5 H7 H6 H8).
1026         assumption
1027       ]
1028     ]
1029   ]
1030 ]
1031 qed.
1032
1033 theorem iter_p_gen_iter_p_gen:
1034 \forall A:Type.
1035 \forall baseA: A.
1036 \forall plusA: A \to A \to A.
1037 (symmetric A plusA) \to
1038 (associative A plusA) \to
1039 (\forall a:A.(plusA a  baseA) = a)\to
1040 \forall g: nat \to nat \to A.
1041 \forall n,m.
1042 \forall p11,p21:nat \to bool.
1043 \forall p12,p22:nat \to nat \to bool.
1044 (\forall x,y. x < n \to y < m \to
1045  (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
1046 iter_p_gen n p11 A
1047   (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA)
1048   baseA plusA =
1049 iter_p_gen m p21 A
1050   (\lambda y:nat.iter_p_gen n (p22 y) A  (\lambda x. g x y) baseA plusA )
1051   baseA plusA.
1052 intros.
1053 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)
1054        n m m n p11 p21 p12 p22)
1055   [intros.split
1056     [split
1057       [split
1058         [split
1059           [split
1060             [apply (andb_true_true ? (p12 j i)).
1061              rewrite > H3
1062               [rewrite > H6.rewrite > H7.reflexivity
1063               |assumption
1064               |assumption
1065               ]
1066             |apply (andb_true_true_r (p11 j)).
1067              rewrite > H3
1068               [rewrite > H6.rewrite > H7.reflexivity
1069               |assumption
1070               |assumption
1071               ]
1072             ]
1073           |reflexivity
1074           ]
1075         |reflexivity
1076         ]
1077       |assumption
1078       ]
1079     |assumption
1080     ]
1081   |intros.split
1082     [split
1083       [split
1084         [split
1085           [split
1086             [apply (andb_true_true ? (p22 j i)).
1087              rewrite < H3
1088               [rewrite > H6.rewrite > H7.reflexivity
1089               |assumption
1090               |assumption
1091               ]
1092             |apply (andb_true_true_r (p21 j)).
1093              rewrite < H3
1094               [rewrite > H6.rewrite > H7.reflexivity
1095               |assumption
1096               |assumption
1097               ]
1098             ]
1099           |reflexivity
1100           ]
1101         |reflexivity
1102         ]
1103       |assumption
1104       ]
1105     |assumption
1106     ]
1107   ]
1108 qed. *)