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 "arithmetics/primes.ma".
13 include "arithmetics/bigops.ma".
15 theorem sigma_const: ∀n:nat. ∑_{i<n} 1 = n.
16 #n elim n // #n1 >bigop_Strue //
19 (* monotonicity; these roperty should be expressed at a more
23 ∀n.∀p:nat → bool.∀g1,g2:nat → nat.
24 (∀i.i<n → p i = true → g1 i ≤ g2 i ) →
25 ∏_{i < n | p i} (g1 i) ≤ ∏_{i < n | p i} (g2 i).
28 |#n1 #Hind #Hle cases (true_or_false (p n1)) #Hcase
29 [ >bigop_Strue // >bigop_Strue // @le_times
30 [@Hle // |@Hind #i #lti #Hpi @Hle [@lt_to_le @le_S_S @lti|@Hpi]]
31 |>bigop_Sfalse // >bigop_Sfalse // @Hind
32 #i #lti #Hpi @Hle [@lt_to_le @le_S_S @lti|@Hpi]
37 theorem exp_sigma: ∀n,a,p.
38 ∏_{i < n | p i} a = exp a (∑_{i < n | p i} 1).
39 #n #a #p elim n // #n1 cases (true_or_false (p n1)) #Hcase
40 [>bigop_Strue // >bigop_Strue // |>bigop_Sfalse // >bigop_Sfalse //]
43 theorem times_pi: ∀n,p,f,g.
44 ∏_{i<n|p i}(f i*g i) = ∏_{i<n|p i}(f i) * ∏_{i<n|p i}(g i).
45 #n #p #f #g elim n // #n1 cases (true_or_false (p n1)) #Hcase #Hind
46 [>bigop_Strue // >bigop_Strue // >bigop_Strue //
47 |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
52 ∏_{i < n | p i} 1 = 1.
53 #n #p elim n // #n1 #Hind cases (true_or_false (p n1)) #Hc
54 [>bigop_Strue >Hind // |>bigop_Sfalse // ]
57 theorem exp_pi: ∀n,m,p,f.
58 ∏_{i < n | p i}(exp (f i) m) = exp (∏_{i < n | p i}(f i)) m.
61 |#m1 #Hind >times_pi >Hind %
66 theorem true_to_pi_p_Sn: ∀n,p,g.
67 p n = true \to pi_p (S n) p g = (g n)*(pi_p n p g).
70 apply true_to_iter_p_gen_Sn.
74 theorem false_to_pi_p_Sn:
75 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
76 p n = false \to pi_p (S n) p g = pi_p n p g.
79 apply false_to_iter_p_gen_Sn.
83 theorem eq_pi_p: \forall p1,p2:nat \to bool.
84 \forall g1,g2: nat \to nat.\forall n.
85 (\forall x. x < n \to p1 x = p2 x) \to
86 (\forall x. x < n \to g1 x = g2 x) \to
87 pi_p n p1 g1 = pi_p n p2 g2.
94 theorem eq_pi_p1: \forall p1,p2:nat \to bool.
95 \forall g1,g2: nat \to nat.\forall n.
96 (\forall x. x < n \to p1 x = p2 x) \to
97 (\forall x. x < n \to p1 x = true \to g1 x = g2 x) \to
98 pi_p n p1 g1 = pi_p n p2 g2.
101 apply eq_iter_p_gen1;
106 \forall g: nat \to nat.\forall n.pi_p n (\lambda x.false) g = S O.
109 apply iter_p_gen_false.
112 theorem pi_p_times: \forall n,k:nat.\forall p:nat \to bool.
113 \forall g: nat \to nat.
115 = pi_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) * pi_p n p g.
118 apply (iter_p_gen_plusA nat n k p g (S O) times)
123 | apply associative_times
127 theorem false_to_eq_pi_p: \forall n,m:nat.n \le m \to
128 \forall p:nat \to bool.
129 \forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to
130 p i = false) \to pi_p m p g = pi_p n p g.
133 apply (false_to_eq_iter_p_gen);
137 theorem or_false_eq_SO_to_eq_pi_p:
138 \forall n,m:nat.\forall p:nat \to bool.
139 \forall g: nat \to nat.
140 n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = S O)
141 \to pi_p m p g = pi_p n p g.
144 apply or_false_eq_baseA_to_eq_iter_p_gen
145 [intros.simplify.rewrite < plus_n_O.reflexivity
153 \forall p1,p2:nat \to bool.
154 \forall g: nat \to nat \to nat.
156 (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
157 (\lambda x.g (div x m) (mod x m)) =
159 (\lambda x.pi_p m p2 (g x)).
162 apply (iter_p_gen2 n m p1 p2 nat g (S O) times)
164 | apply associative_times
173 \forall p1:nat \to bool.
174 \forall p2:nat \to nat \to bool.
175 \forall g: nat \to nat \to nat.
177 (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x m)))
178 (\lambda x.g (div x m) (mod x m)) =
180 (\lambda x.pi_p m (p2 x) (g x)).
183 apply (iter_p_gen2' n m p1 p2 nat g (S O) times)
185 | apply associative_times
192 lemma pi_p_gi: \forall g: nat \to nat.
193 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
194 pi_p n p g = g i * pi_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
197 apply (iter_p_gen_gi)
199 | apply associative_times
209 \forall g,h,h1: nat \to nat.\forall n,n1.
210 \forall p1,p2:nat \to bool.
211 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
212 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
213 (\forall i. i < n \to p1 i = true \to h i < n1) \to
214 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
215 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
216 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
217 pi_p n p1 (\lambda x.g(h x)) = pi_p n1 p2 g.
220 apply (eq_iter_p_gen_gh nat (S O) times ? ? ? g h h1 n n1 p1 p2)
222 | apply associative_times
235 theorem exp_sigma_p: \forall n,a,p.
236 pi_p n p (\lambda x.a) = (exp a (sigma_p n p (\lambda x.S O))).
240 |apply (bool_elim ? (p n1))
242 rewrite > true_to_pi_p_Sn
243 [rewrite > true_to_sigma_p_Sn
252 rewrite > false_to_pi_p_Sn
253 [rewrite > false_to_sigma_p_Sn
263 theorem exp_sigma_p1: \forall n,a,p,f.
264 pi_p n p (\lambda x.(exp a (f x))) = (exp a (sigma_p n p f)).
268 |apply (bool_elim ? (p n1))
270 rewrite > true_to_pi_p_Sn
271 [rewrite > true_to_sigma_p_Sn
274 rewrite > exp_plus_times.
281 rewrite > false_to_pi_p_Sn
282 [rewrite > false_to_sigma_p_Sn
292 theorem times_pi_p: \forall n,p,f,g.
293 pi_p n p (\lambda x.f x*g x) = pi_p n p f * pi_p n p g.
296 [simplify.reflexivity
297 |apply (bool_elim ? (p n1))
299 rewrite > true_to_pi_p_Sn
300 [rewrite > true_to_pi_p_Sn
301 [rewrite > true_to_pi_p_Sn
302 [rewrite > H.autobatch
310 rewrite > false_to_pi_p_Sn
311 [rewrite > false_to_pi_p_Sn
312 [rewrite > false_to_pi_p_Sn;assumption
322 theorem exp_times_pi_p: \forall n,m,k,p,f.
323 pi_p n p (\lambda x.exp k (m*(f x))) =
324 exp (pi_p n p (\lambda x.exp k (f x))) m.
326 apply (trans_eq ? ? (pi_p n p (\lambda x.(exp (exp k (f x)) m))))
327 [apply eq_pi_p;intros
329 |apply sym_eq.rewrite > sym_times.
338 \forall g: nat \to nat.
339 \forall h2:nat \to nat \to nat.
340 \forall h11,h12:nat \to nat.
342 \forall p1,p21:nat \to bool.
343 \forall p22:nat \to nat \to bool.
344 (\forall x. x < k \to p1 x = true \to
345 p21 (h11 x) = true ∧ p22 (h11 x) (h12 x) = true
346 \land h2 (h11 x) (h12 x) = x
347 \land (h11 x) < n \land (h12 x) < m) \to
348 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
349 p1 (h2 i j) = true \land
350 h11 (h2 i j) = i \land h12 (h2 i j) = j
353 Pi z < k | p1 z. g z =
354 Pi x < n | p21 x. Pi y < m | p22 x y.g (h2 x y).
357 pi_p n p21 (\lambda x:nat.pi_p m (p22 x) (\lambda y. g (h2 x y))).
359 unfold pi_p.unfold pi_p.
360 apply (iter_p_gen_knm nat (S O) times sym_times assoc_times ? ? ? h11 h12)
361 [intros.apply sym_eq.apply times_n_SO.
368 \forall g: nat \to nat \to nat.
369 \forall h11,h12,h21,h22: nat \to nat \to nat.
371 \forall p11,p21:nat \to bool.
372 \forall p12,p22:nat \to nat \to bool.
373 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
374 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
375 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
376 \land h11 i j < n1 \land h12 i j < m1) \to
377 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
378 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
379 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
380 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
382 (\lambda x:nat .pi_p m1 (p12 x) (\lambda y. g x y)) =
384 (\lambda x:nat .pi_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
386 unfold pi_p.unfold pi_p.
387 apply (iter_p_gen_2_eq ? ? ? sym_times assoc_times ? ? ? ? h21 h22)
388 [intros.apply sym_eq.apply times_n_SO.
395 \forall g: nat \to nat \to nat.
397 \forall p11,p21:nat \to bool.
398 \forall p12,p22:nat \to nat \to bool.
399 (\forall x,y. x < n \to y < m \to
400 (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
401 pi_p n p11 (\lambda x:nat.pi_p m (p12 x) (\lambda y. g x y)) =
402 pi_p m p21 (\lambda y:nat.pi_p n (p22 y) (\lambda x. g x y)).
404 unfold pi_p.unfold pi_p.
405 apply (iter_p_gen_iter_p_gen ? ? ? sym_times assoc_times)
406 [intros.apply sym_eq.apply times_n_SO.