]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/Z/sigma_p.ma
simplified version of a theorem.
[helm.git] / helm / software / matita / library / Z / sigma_p.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/Z/sigma_p".
16
17 include "Z/times.ma".
18 include "nat/primes.ma".
19 include "nat/ord.ma".
20 include "nat/generic_iter_p.ma".
21
22 (* sigma_p in Z is a specialization of iter_p_gen *)
23 definition sigma_p: nat \to (nat \to bool) \to (nat \to Z) \to Z \def
24 \lambda n, p, g. (iter_p_gen n p Z g OZ Zplus).
25
26 theorem symmetricZPlus: symmetric Z Zplus.
27 change with (\forall a,b:Z. (Zplus a b) = (Zplus b a)).
28 intros.
29 rewrite > sym_Zplus.
30 reflexivity.
31 qed.
32    
33 theorem true_to_sigma_p_Sn: 
34 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to Z.
35 p n = true \to sigma_p (S n) p g = 
36 (g n)+(sigma_p n p g).
37 intros.
38 unfold sigma_p.
39 apply true_to_iter_p_gen_Sn.
40 assumption.
41 qed.
42    
43 theorem false_to_sigma_p_Sn: 
44 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to Z.
45 p n = false \to sigma_p (S n) p g = sigma_p n p g.
46 intros.
47 unfold sigma_p.
48 apply false_to_iter_p_gen_Sn.
49 assumption.
50 qed.
51
52 theorem eq_sigma_p: \forall p1,p2:nat \to bool.
53 \forall g1,g2: nat \to Z.\forall n.
54 (\forall x.  x < n \to p1 x = p2 x) \to
55 (\forall x.  x < n \to g1 x = g2 x) \to
56 sigma_p n p1 g1 = sigma_p n p2 g2.
57 intros.
58 unfold sigma_p.
59 apply eq_iter_p_gen;
60   assumption.
61 qed.
62
63 theorem eq_sigma_p1: \forall p1,p2:nat \to bool.
64 \forall g1,g2: nat \to Z.\forall n.
65 (\forall x.  x < n \to p1 x = p2 x) \to
66 (\forall x.  x < n \to p1 x = true \to g1 x = g2 x) \to
67 sigma_p n p1 g1 = sigma_p n p2 g2.
68 intros.
69 unfold sigma_p.
70 apply eq_iter_p_gen1;
71   assumption.
72 qed.
73
74 theorem sigma_p_false: 
75 \forall g: nat \to Z.\forall n.sigma_p n (\lambda x.false) g = O.
76 intros.
77 unfold sigma_p.
78 apply iter_p_gen_false.
79 qed.
80
81 theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool.
82 \forall g: nat \to Z.
83 sigma_p (k+n) p g 
84 = sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g.
85 intros.
86 unfold sigma_p.
87 apply (iter_p_gen_plusA Z n k p g OZ Zplus)
88 [ apply symmetricZPlus.
89 | intros.
90   apply cic:/matita/Z/plus/Zplus_z_OZ.con
91 | apply associative_Zplus
92 ]
93 qed.
94
95 theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to
96 \forall p:nat \to bool.
97 \forall g: nat \to Z. (\forall i:nat. n \le i \to i < m \to
98 p i = false) \to sigma_p m p g = sigma_p n p g.
99 intros.
100 unfold sigma_p.
101 apply (false_to_eq_iter_p_gen);
102   assumption.
103 qed.
104
105 theorem sigma_p2 : 
106 \forall n,m:nat.
107 \forall p1,p2:nat \to bool.
108 \forall g: nat \to nat \to Z.
109 sigma_p (n*m) 
110   (\lambda x.andb (p1 (div x m)) (p2 (mod x m))) 
111   (\lambda x.g (div x m) (mod x m)) =
112 sigma_p n p1 
113   (\lambda x.sigma_p m p2 (g x)).
114 intros.
115 unfold sigma_p.
116 apply (iter_p_gen2 n m p1 p2 Z g OZ Zplus)
117 [ apply symmetricZPlus
118 | apply associative_Zplus
119 | intros.
120   apply Zplus_z_OZ
121 ]
122 qed.
123
124 (* a stronger, dependent version, required e.g. for dirichlet product *)
125
126 theorem sigma_p2' : 
127 \forall n,m:nat.
128 \forall p1:nat \to bool.
129 \forall p2:nat \to nat \to bool.
130 \forall g: nat \to nat \to Z.
131 sigma_p (n*m) 
132   (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x m))) 
133   (\lambda x.g (div x m) (mod x m)) =
134 sigma_p n p1 
135   (\lambda x.sigma_p m (p2 x) (g x)).
136 intros.
137 unfold sigma_p.
138 apply (iter_p_gen2' n m p1 p2 Z g OZ Zplus)
139 [ apply symmetricZPlus
140 | apply associative_Zplus
141 | intros.
142   apply Zplus_z_OZ
143 ]
144 qed.
145
146 lemma sigma_p_gi: \forall g: nat \to Z.
147 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to 
148 sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
149 intros.
150 unfold sigma_p.
151 apply (iter_p_gen_gi)
152 [ apply symmetricZPlus
153 | apply associative_Zplus
154 | intros.
155   apply Zplus_z_OZ
156 | assumption
157 | assumption
158 ]
159 qed.
160
161 theorem eq_sigma_p_gh: 
162 \forall g: nat \to Z.
163 \forall h,h1: nat \to nat.\forall n,n1.
164 \forall p1,p2:nat \to bool.
165 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
166 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to 
167 (\forall i. i < n \to p1 i = true \to h i < n1) \to 
168 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
169 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to 
170 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to 
171 sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 p2 g.
172 intros.
173 unfold sigma_p.
174 apply (eq_iter_p_gen_gh Z OZ Zplus ? ? ? g h h1 n n1 p1 p2)
175 [ apply symmetricZPlus
176 | apply associative_Zplus
177 | intros.
178   apply Zplus_z_OZ
179 | assumption
180 | assumption
181 | assumption
182 | assumption
183 | assumption
184 | assumption
185 ]
186 qed.
187
188
189 theorem divides_exp_to_lt_ord:\forall n,m,j,p. O < n \to prime p \to
190 p \ndivides n \to j \divides n*(exp p m) \to ord j p < S m.
191 intros.
192 cut (m = ord (n*(exp p m)) p)
193   [apply le_S_S.
194    rewrite > Hcut.
195    apply divides_to_le_ord
196     [elim (le_to_or_lt_eq ? ? (le_O_n j))
197       [assumption
198       |apply False_ind.
199        apply (lt_to_not_eq ? ? H).
200        elim H3.
201        rewrite < H4 in H5.simplify in H5.
202        elim (times_O_to_O ? ? H5)
203         [apply sym_eq.assumption
204         |apply False_ind.
205          apply (not_le_Sn_n O).
206          rewrite < H6 in \vdash (? ? %).
207          apply lt_O_exp.
208          elim H1.apply lt_to_le.assumption
209         ]
210       ]
211     |rewrite > (times_n_O O).
212      apply lt_times
213       [assumption|apply lt_O_exp.apply (prime_to_lt_O ? H1)]
214     |assumption
215     |assumption
216     ]
217   |unfold ord.
218    rewrite > (p_ord_exp1 p ? m n)
219     [reflexivity
220     |apply (prime_to_lt_O ? H1)
221     |assumption
222     |apply sym_times
223     ]
224   ]
225 qed.
226
227 theorem divides_exp_to_divides_ord_rem:\forall n,m,j,p. O < n \to prime p \to
228 p \ndivides n \to j \divides n*(exp p m) \to ord_rem j p \divides n.
229 intros.
230 cut (O < j)
231   [cut (n = ord_rem (n*(exp p m)) p)
232     [rewrite > Hcut1.
233      apply divides_to_divides_ord_rem
234       [assumption   
235       |rewrite > (times_n_O O).
236        apply lt_times
237         [assumption|apply lt_O_exp.apply (prime_to_lt_O ? H1)]
238       |assumption
239       |assumption
240       ]
241     |unfold ord_rem.
242      rewrite > (p_ord_exp1 p ? m n)
243       [reflexivity
244       |apply (prime_to_lt_O ? H1)
245       |assumption
246       |apply sym_times
247       ]
248     ]
249   |elim (le_to_or_lt_eq ? ? (le_O_n j))
250     [assumption
251     |apply False_ind.
252      apply (lt_to_not_eq ? ? H).
253      elim H3.
254      rewrite < H4 in H5.simplify in H5.
255      elim (times_O_to_O ? ? H5)
256       [apply sym_eq.assumption
257       |apply False_ind.
258        apply (not_le_Sn_n O).
259        rewrite < H6 in \vdash (? ? %).
260        apply lt_O_exp.
261        elim H1.apply lt_to_le.assumption
262       ]
263     ]
264   ] 
265 qed.
266
267
268 theorem sigma_p_divides_b: 
269 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to 
270 \forall g: nat \to Z.
271 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
272 sigma_p (S n) (\lambda x.divides_b x n)
273   (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
274 intros.
275 unfold sigma_p.
276 apply (iter_p_gen_divides Z OZ Zplus n m p ? ? ? g)
277 [ assumption
278 | assumption
279 | assumption
280 | apply symmetricZPlus
281 | apply associative_Zplus
282 | intros.
283   apply Zplus_z_OZ
284 ]
285 qed.
286
287     
288 (* sigma_p and Ztimes *)
289 lemma Ztimes_sigma_pl: \forall z:Z.\forall n:nat.\forall p. \forall f.
290 z * (sigma_p n p f) = sigma_p n p (\lambda i.z*(f i)).
291 intros.
292 apply (distributive_times_plus_iter_p_gen Z Zplus OZ Ztimes n z p f)
293 [ apply symmetricZPlus
294 | apply associative_Zplus
295 | intros.
296   apply Zplus_z_OZ
297 | apply symmetric_Ztimes
298 | apply distributive_Ztimes_Zplus
299 | intros.
300   rewrite > (Ztimes_z_OZ a).
301   reflexivity
302 ]
303 qed.
304
305 lemma Ztimes_sigma_pr: \forall z:Z.\forall n:nat.\forall p. \forall f.
306 (sigma_p n p f) * z = sigma_p n p (\lambda i.(f i)*z).
307 intros.
308 rewrite < sym_Ztimes.
309 rewrite > Ztimes_sigma_pl.
310 apply eq_sigma_p
311   [intros.reflexivity
312   |intros.apply sym_Ztimes
313   ]
314 qed.