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