1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/pi_p".
17 include "nat/primes.ma".
18 (* include "nat/ord.ma". *)
19 include "nat/generic_iter_p.ma".
20 (* include "nat/count.ma". necessary just to use bool_to_nat and bool_to_nat_andb*)
21 include "nat/iteration2.ma".
23 (* pi_p on nautral numbers is a specialization of iter_p_gen *)
24 definition pi_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def
25 \lambda n, p, g. (iter_p_gen n p nat g (S O) times).
27 theorem true_to_pi_p_Sn:
28 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
29 p n = true \to pi_p (S n) p g = (g n)*(pi_p n p g).
32 apply true_to_iter_p_gen_Sn.
36 theorem false_to_pi_p_Sn:
37 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
38 p n = false \to pi_p (S n) p g = pi_p n p g.
41 apply false_to_iter_p_gen_Sn.
45 theorem eq_pi_p: \forall p1,p2:nat \to bool.
46 \forall g1,g2: nat \to nat.\forall n.
47 (\forall x. x < n \to p1 x = p2 x) \to
48 (\forall x. x < n \to g1 x = g2 x) \to
49 pi_p n p1 g1 = pi_p n p2 g2.
56 theorem eq_pi_p1: \forall p1,p2:nat \to bool.
57 \forall g1,g2: nat \to nat.\forall n.
58 (\forall x. x < n \to p1 x = p2 x) \to
59 (\forall x. x < n \to p1 x = true \to g1 x = g2 x) \to
60 pi_p n p1 g1 = pi_p n p2 g2.
68 \forall g: nat \to nat.\forall n.pi_p n (\lambda x.false) g = S O.
71 apply iter_p_gen_false.
74 theorem pi_p_times: \forall n,k:nat.\forall p:nat \to bool.
75 \forall g: nat \to nat.
77 = pi_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) * pi_p n p g.
80 apply (iter_p_gen_plusA nat n k p g (S O) times)
85 | apply associative_times
89 theorem false_to_eq_pi_p: \forall n,m:nat.n \le m \to
90 \forall p:nat \to bool.
91 \forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to
92 p i = false) \to pi_p m p g = pi_p n p g.
95 apply (false_to_eq_iter_p_gen);
99 theorem or_false_eq_SO_to_eq_pi_p:
100 \forall n,m:nat.\forall p:nat \to bool.
101 \forall g: nat \to nat.
102 n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = S O)
103 \to pi_p m p g = pi_p n p g.
106 apply or_false_eq_baseA_to_eq_iter_p_gen
107 [intros.simplify.rewrite < plus_n_O.reflexivity
115 \forall p1,p2:nat \to bool.
116 \forall g: nat \to nat \to nat.
118 (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
119 (\lambda x.g (div x m) (mod x m)) =
121 (\lambda x.pi_p m p2 (g x)).
124 apply (iter_p_gen2 n m p1 p2 nat g (S O) times)
126 | apply associative_times
135 \forall p1:nat \to bool.
136 \forall p2:nat \to nat \to bool.
137 \forall g: nat \to nat \to nat.
139 (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x m)))
140 (\lambda x.g (div x m) (mod x m)) =
142 (\lambda x.pi_p m (p2 x) (g x)).
145 apply (iter_p_gen2' n m p1 p2 nat g (S O) times)
147 | apply associative_times
154 lemma pi_p_gi: \forall g: nat \to nat.
155 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
156 pi_p n p g = g i * pi_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
159 apply (iter_p_gen_gi)
161 | apply associative_times
171 \forall g,h,h1: nat \to nat.\forall n,n1.
172 \forall p1,p2:nat \to bool.
173 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
174 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
175 (\forall i. i < n \to p1 i = true \to h i < n1) \to
176 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
177 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
178 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
179 pi_p n p1 (\lambda x.g(h x)) = pi_p n1 p2 g.
182 apply (eq_iter_p_gen_gh nat (S O) times ? ? ? g h h1 n n1 p1 p2)
184 | apply associative_times
199 \forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.
200 (\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to
201 pi_p n p g1 \le pi_p n p g2.
203 generalize in match H.
206 |apply (bool_elim ? (p n1));intros
207 [rewrite > true_to_pi_p_Sn
208 [rewrite > true_to_pi_p_Sn in ⊢ (? ? %)
210 [apply H2[apply le_n|assumption]
213 apply H2[apply le_S.assumption|assumption]
219 |rewrite > false_to_pi_p_Sn
220 [rewrite > false_to_pi_p_Sn in ⊢ (? ? %)
223 apply H2[apply le_S.assumption|assumption]
232 theorem exp_sigma_p: \forall n,a,p.
233 pi_p n p (\lambda x.a) = (exp a (sigma_p n p (\lambda x.S O))).
237 |apply (bool_elim ? (p n1))
239 rewrite > true_to_pi_p_Sn
240 [rewrite > true_to_sigma_p_Sn
249 rewrite > false_to_pi_p_Sn
250 [rewrite > false_to_sigma_p_Sn
260 theorem times_pi_p: \forall n,p,f,g.
261 pi_p n p (\lambda x.f x*g x) = pi_p n p f * pi_p n p g.
264 [simplify.reflexivity
265 |apply (bool_elim ? (p n1))
267 rewrite > true_to_pi_p_Sn
268 [rewrite > true_to_pi_p_Sn
269 [rewrite > true_to_pi_p_Sn
270 [rewrite > H.autobatch
278 rewrite > false_to_pi_p_Sn
279 [rewrite > false_to_pi_p_Sn
280 [rewrite > false_to_pi_p_Sn;assumption
289 theorem pi_p_SO: \forall n,p.
290 pi_p n p (\lambda i.S O) = S O.
293 |simplify.elim (p n1)
294 [simplify.rewrite < plus_n_O.assumption
300 theorem exp_pi_p: \forall n,m,p,f.
301 pi_p n p (\lambda x.exp (f x) m) = exp (pi_p n p f) m.
304 [simplify.apply pi_p_SO
306 rewrite > times_pi_p.
312 theorem exp_times_pi_p: \forall n,m,k,p,f.
313 pi_p n p (\lambda x.exp k (m*(f x))) =
314 exp (pi_p n p (\lambda x.exp k (f x))) m.
316 apply (trans_eq ? ? (pi_p n p (\lambda x.(exp (exp k (f x)) m))))
317 [apply eq_pi_p;intros
319 |apply sym_eq.rewrite > sym_times.
328 \forall g: nat \to nat.
329 \forall h2:nat \to nat \to nat.
330 \forall h11,h12:nat \to nat.
332 \forall p1,p21:nat \to bool.
333 \forall p22:nat \to nat \to bool.
334 (\forall x. x < k \to p1 x = true \to
335 p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
336 \land h2 (h11 x) (h12 x) = x
337 \land (h11 x) < n \land (h12 x) < m) \to
338 (\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
339 p1 (h2 i j) = true \land
340 h11 (h2 i j) = i \land h12 (h2 i j) = j
341 \land h2 i j < k) \to
343 pi_p n p21 (\lambda x:nat.pi_p m (p22 x) (\lambda y. g (h2 x y))).
345 unfold pi_p.unfold pi_p.
346 apply (iter_p_gen_knm nat (S O) times sym_times assoc_times ? ? ? h11 h12)
347 [intros.apply sym_eq.apply times_n_SO.
354 \forall g: nat \to nat \to nat.
355 \forall h11,h12,h21,h22: nat \to nat \to nat.
357 \forall p11,p21:nat \to bool.
358 \forall p12,p22:nat \to nat \to bool.
359 (\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
360 p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
361 \land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
362 \land h11 i j < n1 \land h12 i j < m1) \to
363 (\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
364 p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
365 \land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
366 \land (h21 i j) < n2 \land (h22 i j) < m2) \to
368 (\lambda x:nat .pi_p m1 (p12 x) (\lambda y. g x y)) =
370 (\lambda x:nat .pi_p m2 (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
372 unfold pi_p.unfold pi_p.
373 apply (iter_p_gen_2_eq ? ? ? sym_times assoc_times ? ? ? ? h21 h22)
374 [intros.apply sym_eq.apply times_n_SO.
381 \forall g: nat \to nat \to nat.
383 \forall p11,p21:nat \to bool.
384 \forall p12,p22:nat \to nat \to bool.
385 (\forall x,y. x < n \to y < m \to
386 (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
387 pi_p n p11 (\lambda x:nat.pi_p m (p12 x) (\lambda y. g x y)) =
388 pi_p m p21 (\lambda y:nat.pi_p n (p22 y) (\lambda x. g x y)).
390 unfold pi_p.unfold pi_p.
391 apply (iter_p_gen_iter_p_gen ? ? ? sym_times assoc_times)
392 [intros.apply sym_eq.apply times_n_SO.