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.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "basics/types.ma".
13 include "arithmetics/div_and_mod.ma".
15 definition sameF_upto: nat → ∀A.relation(nat→A) ≝
16 λk.λA.λf,g.∀i. i < k → f i = g i.
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.
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/
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/
32 definition sumF ≝ λA.λf,g:nat → A.λn,i.
33 if_then_else ? (leb n i) (g (i-n)) (f i).
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).
40 λA,B.λf:nat→A.λg:nat→B.λm,x.〈 f(div x m), g(mod x m) 〉.
43 let rec bigop (n:nat) (p:nat → bool) (B:Type[0])
44 (nil: B) (op: B → B → B) (f: nat → B) ≝
49 [true ⇒ op (f k) (bigop k p B nil op f)
50 |false ⇒ bigop k p B nil op f]
53 notation "\big [ op , nil ]_{ ident i < n | p } f"
55 for @{'bigop $n $op $nil (λ${ident i}. $p) (λ${ident i}. $f)}.
57 notation "\big [ op , nil ]_{ ident i < n } f"
59 for @{'bigop $n $op $nil (λ${ident i}.true) (λ${ident i}. $f)}.
61 interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f).
63 notation "\big [ op , nil ]_{ ident j ∈ [a,b[ | p } f"
65 for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
66 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
68 notation "\big [ op , nil ]_{ ident j ∈ [a,b[ } f"
70 for @{'bigop ($b-$a) $op $nil (λ${ident j}.((λ${ident j}.$true) (${ident j}+$a)))
71 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
73 (* notation "\big [ op , nil ]_{( term 50) a ≤ ident j < b | p } f"
75 for @{\big[$op,$nil]_{${ident j} < ($b-$a) | ((λ${ident j}.$p) (${ident j}+$a))}((λ${ident j}.$f)(${ident j}+$a))}.
78 interpretation "bigop" 'bigop n op nil p f = (bigop n p ? nil op f).
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.
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.
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) //
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) //
108 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
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
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 //
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 //
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 //
138 theorem bigop_sumI: ∀a,b,c,p,B.∀nil.∀op:Aop B nil.∀f:nat→B.
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 //
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/
168 record ACop (A:Type[0]) (nil:A) : Type[0] ≝
170 comm: ∀a,b.aop a b = aop b a
173 lemma bigop_diff: ∀p,B.∀nil.∀op:ACop B nil.∀f:nat → B.∀i,n.
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)
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 //
187 |<Hi >bigop_Strue // @eq_f >bigop_Sfalse
188 [@same_bigop // #k #ltki >not_eq_to_eqb_false /2/
196 record range (A:Type[0]): Type[0] ≝
197 {enum:nat→A; upto:nat; filter:nat→bool}.
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 →
202 ∧ filter A J (h i) = true
205 definition iso: ∀A:Type[0].relation (range A) ≝
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.
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/
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/
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/
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 % // % //
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
241 [@(Hind ? (le_O_n ?)) [/2/ | @(transitive_sub … (sub_lt …) sub2) //]
242 |@(sub0_to_false … sub2) //
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 //
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
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)) //
268 (* Sigma e Pi - da generalizzare *)
269 notation "Σ_{ ident i < n | p } f"
271 for @{'bigop $n plus 0 (λ${ident i}.p) (λ${ident i}. $f)}.
273 notation "Σ_{ ident i < n } f"
275 for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}.
277 notation "Σ_{ ident j ∈ [a,b[ } f"
279 for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
280 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
282 notation "Σ_{ ident j ∈ [a,b[ | p } f"
284 for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
285 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
287 notation "Π_{ ident i < n | p} f"
289 for @{'bigop $n times 1 (λ${ident i}.$p) (λ${ident i}. $f)}.
291 notation "Π_{ ident i < n } f"
293 for @{'bigop $n times 1 (λ${ident i}.true) (λ${ident i}. $f)}.
295 notation "Π_{ ident j ∈ [a,b[ } f"
297 for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
298 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
300 notation "Π_{ ident j ∈ [a,b[ | p } f"
302 for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
303 (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
307 definition p_ord_times \def
310 [pair q r \Rightarrow r*m+q].
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.
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.
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.
334 lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
336 elim (le_to_or_lt_eq O ? (le_O_n m))
340 rewrite < times_n_O in H.
341 apply (not_le_Sn_O ? H)
345 theorem iter_p_gen_knm:
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.
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.
369 rewrite < (iter_p_gen2' n m p21 p22 ? ? ? ? H H1 H2).
371 apply (eq_iter_p_gen_gh A baseA plusA H H1 H2 g ? (\lambda x.(h11 x)*m+(h12 x)))
373 elim (H4 (i/m) (i \mod m));clear H4
377 |apply (lt_times_to_lt_div ? ? ? H5)
379 apply (lt_times_to_lt_O ? ? ? H5)
380 |apply (andb_true_true ? ? H6)
381 |apply (andb_true_true_r ? ? H6)
384 elim (H4 (i/m) (i \mod m));clear H4
391 apply (lt_times_to_lt_O ? ? ? H5)
392 |apply (lt_times_to_lt_div ? ? ? H5)
394 apply (lt_times_to_lt_O ? ? ? H5)
395 |apply (andb_true_true ? ? H6)
396 |apply (andb_true_true_r ? ? H6)
399 elim (H4 (i/m) (i \mod m));clear H4
403 |apply (lt_times_to_lt_div ? ? ? H5)
405 apply (lt_times_to_lt_O ? ? ? H5)
406 |apply (andb_true_true ? ? H6)
407 |apply (andb_true_true_r ? ? H6)
414 rewrite > div_plus_times
415 [rewrite > mod_plus_times
428 rewrite > div_plus_times
429 [rewrite > mod_plus_times
440 apply (lt_to_le_to_lt ? ((h11 j)*m+m))
441 [apply monotonic_lt_plus_r.
444 change with ((S (h11 j)*m) \le n*m).
445 apply monotonic_le_times_l.
451 theorem iter_p_gen_divides:
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)
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.
466 [rewrite < (iter_p_gen2 ? ? ? ? ? ? ? ? H3 H4 H5).
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) )
471 apply (eq_iter_p_gen_gh ? ? ? ? ? ? g ? (p_ord_times p (S m)))
476 lapply (divides_b_true_to_lt_O ? ? H H7).
477 apply divides_to_divides_b_true
478 [rewrite > (times_n_O O).
481 |apply lt_O_exp.assumption
484 [apply divides_b_true_to_divides.assumption
485 |apply (witness ? ? (p \sup (m-i \mod (S m)))).
486 rewrite < exp_plus_times.
489 apply plus_minus_m_m.
490 autobatch by le_S_S_to_le, lt_mod_m_m, lt_O_S;
494 lapply (divides_b_true_to_lt_O ? ? H H7).
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).
504 apply (trans_divides ? (i/ S m))
506 apply divides_b_true_to_divides;assumption]
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.
526 [rewrite > div_p_ord_times
527 [apply divides_to_divides_b_true
530 |apply (divides_b_true_to_lt_O ? ? ? H7).
531 rewrite > (times_n_O O).
533 [assumption|apply lt_O_exp.assumption]
535 |cut (n = ord_rem (n*(exp p m)) p)
537 apply divides_to_divides_ord_rem
538 [apply (divides_b_true_to_lt_O ? ? ? H7).
539 rewrite > (times_n_O O).
541 [assumption|apply lt_O_exp.assumption]
542 |rewrite > (times_n_O O).
544 [assumption|apply lt_O_exp.assumption]
546 |apply divides_b_true_to_divides.
550 rewrite > (p_ord_exp1 p ? m n)
560 |cut (m = ord (n*(exp p m)) p)
563 apply divides_to_le_ord
564 [apply (divides_b_true_to_lt_O ? ? ? H7).
565 rewrite > (times_n_O O).
567 [assumption|apply lt_O_exp.assumption]
568 |rewrite > (times_n_O O).
570 [assumption|apply lt_O_exp.assumption]
572 |apply divides_b_true_to_divides.
576 rewrite > (p_ord_exp1 p ? m n)
586 [rewrite > div_p_ord_times
587 [rewrite > mod_p_ord_times
588 [rewrite > sym_times.
592 |apply (divides_b_true_to_lt_O ? ? ? H7).
593 rewrite > (times_n_O O).
595 [assumption|apply lt_O_exp.assumption]
597 |cut (m = ord (n*(exp p m)) p)
600 apply divides_to_le_ord
601 [apply (divides_b_true_to_lt_O ? ? ? H7).
602 rewrite > (times_n_O O).
604 [assumption|apply lt_O_exp.assumption]
605 |rewrite > (times_n_O O).
607 [assumption|apply lt_O_exp.assumption]
609 |apply divides_b_true_to_divides.
613 rewrite > (p_ord_exp1 p ? m n)
623 |cut (m = ord (n*(exp p m)) p)
626 apply divides_to_le_ord
627 [apply (divides_b_true_to_lt_O ? ? ? H7).
628 rewrite > (times_n_O O).
630 [assumption|apply lt_O_exp.assumption]
631 |rewrite > (times_n_O O).
633 [assumption|apply lt_O_exp.assumption]
635 |apply divides_b_true_to_divides.
639 rewrite > (p_ord_exp1 p ? m n)
648 rewrite > eq_p_ord_times.
650 apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
653 cut (m = ord (n*(p \sup m)) p)
655 apply divides_to_le_ord
656 [apply (divides_b_true_to_lt_O ? ? ? H7).
657 rewrite > (times_n_O O).
659 [assumption|apply lt_O_exp.assumption]
660 |rewrite > (times_n_O O).
662 [assumption|apply lt_O_exp.assumption]
664 |apply divides_b_true_to_divides.
669 rewrite > (p_ord_exp1 p ? m n)
676 |change with (S (ord_rem j p)*S m \le S n*S m).
679 cut (n = ord_rem (n*(p \sup m)) p)
684 |rewrite > (times_n_O O).
686 [assumption|apply lt_O_exp.assumption]
688 |apply divides_to_divides_ord_rem
689 [apply (divides_b_true_to_lt_O ? ? ? H7).
690 rewrite > (times_n_O O).
692 [assumption|apply lt_O_exp.assumption]
693 |rewrite > (times_n_O O).
695 [assumption|apply lt_O_exp.assumption]
697 |apply divides_b_true_to_divides.
703 rewrite > (p_ord_exp1 p ? m n)
715 elim (divides_b (x/S m) n);reflexivity
719 |elim H1.apply lt_to_le.assumption
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)
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)).
740 | cut( (p n1) = true \lor (p n1) = false)
742 [ rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
743 rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
745 rewrite > (H3 k (g n1)).
748 | rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
749 rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
762 theorem iter_p_gen_2_eq:
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.
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
783 (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA)
786 (\lambda x:nat .iter_p_gen m2 (p22 x) A (\lambda y. g (h11 x y) (h12 x y)) baseA plusA )
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))).
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))
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).
803 [ cut((x \mod m1) < m1)
804 [ elim (H4 ? ? Hcut1 Hcut2 H7 H8).
832 | apply (lt_times_n_to_lt m1)
834 | apply (le_to_lt_to_lt ? x)
835 [ apply (eq_plus_to_le ? ? (x \mod m1)).
842 | apply not_le_to_lt.unfold.intro.
843 generalize in match H5.
844 apply (le_n_O_elim ? H9).
849 | elim (H3 ? ? H5 H6 H7 H8).
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))
859 [ apply true_to_true_to_andb_true
880 [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
884 | rewrite > sym_plus.
885 rewrite > (sym_times (h11 i j) m1).
886 rewrite > times_n_Sm.
891 | apply not_le_to_lt.unfold.intro.
892 generalize in match H12.
893 apply (le_n_O_elim ? H11).
897 | apply not_le_to_lt.unfold.intro.
898 generalize in match H10.
899 apply (le_n_O_elim ? H11).
904 | rewrite > (mod_plus_times m1 (h11 i j) (h12 i j)).
908 | rewrite > (div_plus_times m1 (h11 i j) (h12 i j)).
913 | apply (eq_iter_p_gen1)
914 [ intros. reflexivity
916 apply (eq_iter_p_gen1)
917 [ intros. reflexivity
919 rewrite > (div_plus_times)
920 [ rewrite > (mod_plus_times)
922 | elim (H3 x x1 H5 H7 H6 H8).
925 | elim (H3 x x1 H5 H7 H6 H8).
933 theorem iter_p_gen_iter_p_gen:
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.
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
947 (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA)
950 (\lambda y:nat.iter_p_gen n (p22 y) A (\lambda x. g x y) baseA plusA )
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)
960 [apply (andb_true_true ? (p12 j i)).
962 [rewrite > H6.rewrite > H7.reflexivity
966 |apply (andb_true_true_r (p11 j)).
968 [rewrite > H6.rewrite > H7.reflexivity
986 [apply (andb_true_true ? (p22 j i)).
988 [rewrite > H6.rewrite > H7.reflexivity
992 |apply (andb_true_true_r (p21 j)).
994 [rewrite > H6.rewrite > H7.reflexivity