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