]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/iteration2.ma
e1cd09a207e369c1280a7b20b02fd1069d478c01
[helm.git] / helm / software / matita / library / nat / iteration2.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/nat/iteration2.ma".
16
17 include "nat/primes.ma".
18 include "nat/ord.ma".
19 include "nat/generic_sigma_p.ma".
20
21
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).
25
26 theorem symmetricIntPlus: symmetric nat plus.
27 change with (\forall a,b:nat. (plus a b) = (plus b a)).
28 intros.
29 rewrite > sym_plus.
30 reflexivity.
31 qed.
32    
33 (*the following theorems on sigma_p in N are obtained by the more general ones
34  * in sigma_p_gen.ma
35  *)
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).
40 intros.
41 unfold sigma_p.
42 apply true_to_sigma_p_Sn_gen.
43 assumption.
44 qed.
45    
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.
49 intros.
50 unfold sigma_p.
51 apply false_to_sigma_p_Sn_gen.
52 assumption.
53
54 qed.
55
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.
61 intros.
62 unfold sigma_p.
63 apply eq_sigma_p_gen;
64   assumption.
65 qed.
66
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.
72 intros.
73 unfold sigma_p.
74 apply eq_sigma_p1_gen;
75   assumption.
76 qed.
77
78 theorem sigma_p_false: 
79 \forall g: nat \to nat.\forall n.sigma_p n (\lambda x.false) g = O.
80 intros.
81 unfold sigma_p.
82 apply sigma_p_false_gen.
83 qed.
84
85 theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool.
86 \forall g: nat \to nat.
87 sigma_p (k+n) p g 
88 = sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g.
89 intros.
90 unfold sigma_p.
91 apply (sigma_p_plusA_gen nat n k p g O plus)
92 [ apply symmetricIntPlus.
93 | intros.
94   apply sym_eq.
95   apply plus_n_O
96 | apply associative_plus
97 ]
98 qed.
99
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.
104 intros.
105 unfold sigma_p.
106 apply (false_to_eq_sigma_p_gen);
107   assumption.
108 qed.
109
110 theorem sigma_p2 : 
111 \forall n,m:nat.
112 \forall p1,p2:nat \to bool.
113 \forall g: nat \to nat \to nat.
114 sigma_p (n*m) 
115   (\lambda x.andb (p1 (div x m)) (p2 (mod x m))) 
116   (\lambda x.g (div x m) (mod x m)) =
117 sigma_p n p1 
118   (\lambda x.sigma_p m p2 (g x)).
119 intros.
120 unfold sigma_p.
121 apply (sigma_p2_gen n m p1 p2 nat g O plus)
122 [ apply symmetricIntPlus
123 | apply associative_plus
124 | intros.
125   apply sym_eq.
126   apply plus_n_O
127 ]
128 qed.
129
130 theorem sigma_p2' : 
131 \forall n,m:nat.
132 \forall p1:nat \to bool.
133 \forall p2:nat \to nat \to bool.
134 \forall g: nat \to nat \to nat.
135 sigma_p (n*m) 
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)) =
138 sigma_p n p1 
139   (\lambda x.sigma_p m (p2 x) (g x)).
140 intros.
141 unfold sigma_p.
142 apply (sigma_p2_gen' n m p1 p2 nat g O plus)
143 [ apply symmetricIntPlus
144 | apply associative_plus
145 | intros.
146   apply sym_eq.
147   apply plus_n_O
148 ]
149 qed.
150
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.
154 intros.
155 unfold sigma_p.
156 apply (sigma_p_gi_gen)
157 [ apply symmetricIntPlus
158 | apply associative_plus
159 | intros.
160   apply sym_eq.
161   apply plus_n_O
162 | assumption
163 | assumption
164 ]
165 qed.
166
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.
177 intros.
178 unfold sigma_p.
179 apply (eq_sigma_p_gh_gen nat O plus ? ? ? g h h1 n n1 p1 p2)
180 [ apply symmetricIntPlus
181 | apply associative_plus
182 | intros.
183   apply sym_eq.
184   apply plus_n_O
185 | assumption
186 | assumption
187 | assumption
188 | assumption
189 | assumption
190 | assumption
191 ]
192 qed.
193
194
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)))).
201 intros.
202 unfold sigma_p.
203 apply (sigma_p_divides_gen nat O plus n m p ? ? ? g)
204 [ assumption
205 | assumption
206 | assumption
207 | apply symmetricIntPlus
208 | apply associative_plus
209 | intros.
210   apply sym_eq.
211   apply plus_n_O
212 ]
213 qed.
214
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)).
217 intros.
218 apply (distributive_times_plus_sigma_p_generic nat plus O times n k p g)
219 [ apply symmetricIntPlus
220 | apply associative_plus
221 | intros.
222   apply sym_eq.
223   apply plus_n_O
224 | apply symmetric_times
225 | apply distributive_times_plus
226 | intros.
227   rewrite < (times_n_O a).
228   reflexivity
229 ]
230 qed.
231