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/iteration2".
17 include "nat/primes.ma".
19 include "nat/generic_sigma_p.ma".
22 (* sigma_p on nautral numbers is a specialization of sigma_p_gen *)
23 definition sigma_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def
24 \lambda n, p, g. (sigma_p_gen n p nat g O plus).
26 theorem symmetricIntPlus: symmetric nat plus.
27 change with (\forall a,b:nat. (plus a b) = (plus b a)).
33 (*the following theorems on sigma_p in N are obtained by the more general ones
36 theorem true_to_sigma_p_Sn:
37 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
38 p n = true \to sigma_p (S n) p g =
39 (g n)+(sigma_p n p g).
42 apply true_to_sigma_p_Sn_gen.
46 theorem false_to_sigma_p_Sn:
47 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
48 p n = false \to sigma_p (S n) p g = sigma_p n p g.
51 apply false_to_sigma_p_Sn_gen.
56 theorem eq_sigma_p: \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 g1 x = g2 x) \to
60 sigma_p n p1 g1 = sigma_p n p2 g2.
67 theorem eq_sigma_p1: \forall p1,p2:nat \to bool.
68 \forall g1,g2: nat \to nat.\forall n.
69 (\forall x. x < n \to p1 x = p2 x) \to
70 (\forall x. x < n \to p1 x = true \to g1 x = g2 x) \to
71 sigma_p n p1 g1 = sigma_p n p2 g2.
74 apply eq_sigma_p1_gen;
78 theorem sigma_p_false:
79 \forall g: nat \to nat.\forall n.sigma_p n (\lambda x.false) g = O.
82 apply sigma_p_false_gen.
85 theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool.
86 \forall g: nat \to nat.
88 = sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g.
91 apply (sigma_p_plusA_gen nat n k p g O plus)
92 [ apply symmetricIntPlus.
96 | apply associative_plus
100 theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to
101 \forall p:nat \to bool.
102 \forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to
103 p i = false) \to sigma_p m p g = sigma_p n p g.
106 apply (false_to_eq_sigma_p_gen);
112 \forall p1,p2:nat \to bool.
113 \forall g: nat \to nat \to nat.
115 (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
116 (\lambda x.g (div x m) (mod x m)) =
118 (\lambda x.sigma_p m p2 (g x)).
121 apply (sigma_p2_gen n m p1 p2 nat g O plus)
122 [ apply symmetricIntPlus
123 | apply associative_plus
132 \forall p1:nat \to bool.
133 \forall p2:nat \to nat \to bool.
134 \forall g: nat \to nat \to nat.
136 (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x m)))
137 (\lambda x.g (div x m) (mod x m)) =
139 (\lambda x.sigma_p m (p2 x) (g x)).
142 apply (sigma_p2_gen' n m p1 p2 nat g O plus)
143 [ apply symmetricIntPlus
144 | apply associative_plus
151 lemma sigma_p_gi: \forall g: nat \to nat.
152 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
153 sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
156 apply (sigma_p_gi_gen)
157 [ apply symmetricIntPlus
158 | apply associative_plus
167 theorem eq_sigma_p_gh:
168 \forall g,h,h1: nat \to nat.\forall n,n1.
169 \forall p1,p2:nat \to bool.
170 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
171 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
172 (\forall i. i < n \to p1 i = true \to h i < n1) \to
173 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
174 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
175 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
176 sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 (\lambda x.p2 x) g.
179 apply (eq_sigma_p_gh_gen nat O plus ? ? ? g h h1 n n1 p1 p2)
180 [ apply symmetricIntPlus
181 | apply associative_plus
195 theorem sigma_p_divides:
196 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
197 \forall g: nat \to nat.
198 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
199 sigma_p (S n) (\lambda x.divides_b x n)
200 (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
203 apply (sigma_p_divides_gen nat O plus n m p ? ? ? g)
207 | apply symmetricIntPlus
208 | apply associative_plus
215 theorem distributive_times_plus_sigma_p: \forall n,k:nat. \forall p:nat \to bool. \forall g:nat \to nat.
216 k*(sigma_p n p g) = sigma_p n p (\lambda i:nat.k * (g i)).
218 apply (distributive_times_plus_sigma_p_generic nat plus O times n k p g)
219 [ apply symmetricIntPlus
220 | apply associative_plus
224 | apply symmetric_times
225 | apply distributive_times_plus
227 rewrite < (times_n_O a).