]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/Z/moebius.ma
Dummy dependent types are no longer cleaned in inductive type arities.
[helm.git] / helm / software / matita / library / Z / moebius.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 (*       \ /        Matita 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/moebius".
16
17 include "nat/factorization.ma".
18 include "Z/sigma_p.ma".
19   
20 let rec moebius_aux p n : Z \def
21   match p with 
22   [ O \Rightarrow pos O
23   | (S p1) \Rightarrow 
24     match p_ord n (nth_prime p1) with
25     [ (pair q r) \Rightarrow
26       match q with
27       [ O \Rightarrow moebius_aux p1 r
28       | (S q1) \Rightarrow
29               match q1 with 
30               [ O \Rightarrow Zopp (moebius_aux p1 r) 
31         | (S q2) \Rightarrow OZ
32         ]
33       ]
34     ]
35   ]
36 .
37
38 definition moebius : nat \to Z \def
39 \lambda n.
40   let p \def (max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)) in
41   moebius_aux (S p) n.
42
43 (*
44 theorem moebius_O : moebius O = pos O.
45 simplify. reflexivity.
46 qed.
47       
48 theorem moebius_SO : moebius (S O) = pos O.
49 simplify.reflexivity.
50 qed.  
51
52 theorem moebius_SSO : moebius (S (S O)) = neg O.
53 simplify.reflexivity.
54 qed.  
55
56 theorem moebius_SSSO : moebius (S (S (S O))) = neg O.
57 simplify.reflexivity.
58 qed.
59
60 theorem moebius_SSSSO : moebius (S (S (S (S O)))) = OZ.
61 simplify.reflexivity.
62 qed.
63 *)
64
65 theorem not_divides_to_eq_moebius_aux: \forall n,p,p1.p \le p1 \to
66 (\forall i. p \le i \to i \le p1 \to Not (divides (nth_prime i) n))
67 \to moebius_aux p n = moebius_aux p1 n.
68 intros 4.
69 elim H
70   [reflexivity
71   |simplify.
72    rewrite > not_divides_to_p_ord_O
73     [simplify.apply H2.intros.
74      apply H3[assumption|apply le_S.assumption]
75     |apply H3[assumption|apply le_n_Sn]
76     ]
77   ]
78 qed.
79
80 theorem eq_moebius_moebius_aux: \forall n,p. 
81 max_prime_factor n < p \to p \le n \to
82 moebius n = moebius_aux p n.
83 intros.
84 unfold moebius.
85 change with 
86 (moebius_aux (S (max n (\lambda p:nat.eqb (n\mod nth_prime p) O))) n
87 = moebius_aux p n).
88 apply not_divides_to_eq_moebius_aux
89   [assumption
90   |intros.
91    apply divides_b_false_to_not_divides.
92    unfold divides_b.
93    apply (lt_max_to_false ? n i)
94     [assumption
95     |apply (trans_le ? p)[assumption|assumption]
96     ]
97   ]
98 qed.
99
100 theorem moebius_aux_SO: \forall p.moebius_aux p (S O) = pos O.
101 intros.
102 elim p
103   [simplify.reflexivity
104   |rewrite < H.
105    apply sym_eq.
106    apply not_divides_to_eq_moebius_aux
107    [apply le_n_Sn
108    |intros.unfold.intro.
109     absurd (nth_prime i \le S O)
110       [apply divides_to_le
111         [apply le_n|assumption]
112       |apply lt_to_not_le.
113        apply lt_SO_nth_prime_n.
114       ]
115     ]
116   ]
117 qed.
118
119 theorem p_ord_SO_SO_to_moebius : \forall n,p.
120   (S O) < n \to
121   p = max_prime_factor n \to
122   p_ord n (nth_prime p) = pair nat nat (S O) (S O) \to
123   moebius n = Zopp (pos O).
124 intros.
125 change with 
126   (moebius_aux (S (max_prime_factor n)) n = neg O).
127 rewrite < H1.simplify.
128 rewrite > H2.simplify.
129 rewrite > moebius_aux_SO.
130 reflexivity.
131 qed.
132
133 theorem p_ord_SO_r_to_moebius1 : \forall n,p,r.
134   (S O) < n \to 
135   p = max_prime_factor n \to
136   (S O) < r \to 
137   p_ord n (nth_prime p) = pair nat nat (S O) r \to
138   moebius n = Zopp (moebius r).
139 intros.
140 change with 
141   (moebius_aux (S (max_prime_factor n)) n = -(moebius r)).
142 rewrite < H1.simplify.
143 rewrite > H3.simplify.
144 apply eq_f.
145 apply sym_eq.
146 change with 
147  (moebius_aux (S (max_prime_factor r)) r = moebius_aux p r).
148 apply not_divides_to_eq_moebius_aux
149   [apply (p_ord_to_lt_max_prime_factor n p (S O) ? ? H1)
150     [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
151     |apply sym_eq. assumption
152     |assumption
153     ]
154   |intros.
155    lapply (decidable_le i r).
156    elim Hletin
157     [apply divides_b_false_to_not_divides.
158      apply (lt_max_to_false ? r i)[assumption|assumption]
159     |unfold.intro.apply H6.
160      apply (trans_le ? (nth_prime i))
161       [apply lt_to_le.
162        apply lt_n_nth_prime_n
163       |apply divides_to_le
164         [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
165         |assumption
166         ]
167       ]
168     ]
169   ]
170 qed.
171
172 theorem p_ord_SO_r_to_moebius : \forall n,p,r.
173   (S O) < n \to 
174   p = max_prime_factor n \to
175   p_ord n (nth_prime p) = pair nat nat (S O) r \to
176   moebius n = Zopp (moebius r).
177 intros 5.
178 apply (nat_case r);intro
179   [apply False_ind.
180    apply (p_ord_to_not_eq_O ? ? ? ? H H2).
181    reflexivity
182   |apply (nat_case m);intros
183     [simplify.apply (p_ord_SO_SO_to_moebius ? ? H H1 H2)
184     |apply (p_ord_SO_r_to_moebius1 ? ? ? H H1 ? H2).
185      apply le_S_S.apply le_S_S.apply le_O_n
186     ]
187   ]
188 qed.    
189
190 theorem p_ord_SSq_r_to_moebius : \forall n,p,q,r.
191   (S O) < n \to
192   p = max_prime_factor n \to
193   p_ord n (nth_prime p) = pair nat nat (S (S q)) r \to
194   moebius n = OZ.
195 intros.
196 change with
197   (moebius_aux (S (max n (\lambda p:nat.eqb (n\mod nth_prime p) O))) n =OZ).
198 rewrite < H1.simplify.
199 rewrite > H2.simplify.
200 reflexivity.
201 qed.
202
203 theorem moebius_exp: \forall p,q,r:nat. O < r \to
204 r = (S O) \lor (max_prime_factor r) < p \to
205 (* r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to *)
206 sigma_p (S (S q)) (\lambda y.true) (\lambda y.moebius (r*(exp (nth_prime p) y))) = O.
207 intros.
208 elim q
209   [rewrite > true_to_sigma_p_Sn
210     [rewrite > true_to_sigma_p_Sn
211       [rewrite > Zplus_z_OZ.
212        rewrite < times_n_SO.
213        rewrite > (p_ord_SO_r_to_moebius ? p r)
214         [rewrite > sym_Zplus.
215          rewrite > Zplus_Zopp.
216          reflexivity
217         |rewrite < exp_n_SO.
218          rewrite > sym_times.
219          rewrite > times_n_SO.
220          apply lt_to_le_to_lt_times
221           [apply lt_SO_nth_prime_n
222           |assumption
223           |assumption
224           ]
225         |apply eq_p_max
226           [apply le_n|assumption|assumption]
227         |apply p_ord_exp1
228           [apply lt_O_nth_prime_n
229           |apply lt_max_prime_factor_to_not_divides;assumption
230           |apply sym_times
231           ]
232         ]
233       |reflexivity
234       ]
235     |reflexivity
236     ]
237   |rewrite > true_to_sigma_p_Sn
238     [rewrite > H2.
239      rewrite > Zplus_z_OZ.
240      apply (p_ord_SSq_r_to_moebius ? p n r)
241       [rewrite > times_n_SO.
242        rewrite > sym_times in \vdash (? ? %).
243        apply lt_to_le_to_lt_times
244         [apply (trans_lt ? (nth_prime p))
245           [apply lt_SO_nth_prime_n
246             |rewrite > exp_n_SO in \vdash (? % ?).
247              apply lt_exp
248               [apply lt_SO_nth_prime_n
249               |apply le_S_S.apply le_S_S.apply le_O_n
250               ]
251             ]
252           |assumption
253           |assumption
254           ]
255         |apply eq_p_max
256           [apply le_S_S.apply le_O_n|assumption|assumption]  
257         |apply p_ord_exp1
258           [apply lt_O_nth_prime_n
259           |apply lt_max_prime_factor_to_not_divides;assumption        
260           |apply sym_times
261           ]
262         ]
263       |reflexivity
264       ]
265     ]   
266 qed.
267   
268 theorem sigma_p_moebius1: \forall n,m,p:nat.O < n \to O < m \to 
269 n = (S O) \lor max_prime_factor n < p \to
270 sigma_p (S (n*(exp (nth_prime p) m))) (\lambda y.divides_b y (n*(exp (nth_prime p) m))) moebius = O.
271 intros.
272 rewrite > sigma_p_divides_b
273   [apply (trans_eq ? ? (sigma_p (S n) (\lambda x:nat.divides_b x n) (\lambda x:nat.OZ)))
274     [apply eq_sigma_p1
275       [intros.reflexivity
276       |apply (lt_O_n_elim m H1).
277        intros.apply moebius_exp
278         [apply (divides_b_true_to_lt_O ? ? ? H4).
279          assumption
280         |elim H2
281           [left.rewrite > H5 in H3.
282            elim (le_to_or_lt_eq ? ? (le_S_S_to_le ? ? H3))
283             [apply False_ind.
284              apply (lt_to_not_le O x)
285               [apply (divides_b_true_to_lt_O n x H H4)
286               |apply le_S_S_to_le.assumption
287               ]
288             |assumption
289             ]
290           |right.
291            apply (le_to_lt_to_lt ? ? ? ? H5).
292            apply (divides_to_max_prime_factor1 x n)
293             [apply (divides_b_true_to_lt_O ? ? H H4)
294             |assumption
295             |apply divides_b_true_to_divides.
296              assumption
297             ]
298           ]
299         ]
300       ]
301     |generalize in match (\lambda x:nat.divides_b x n).
302      intro.
303      elim n
304       [simplify.elim (f O);reflexivity
305       |apply (bool_elim ? (f (S n1)))
306         [intro.
307          rewrite > true_to_sigma_p_Sn
308           [rewrite > H3.reflexivity|assumption]
309         |intro.
310          rewrite > false_to_sigma_p_Sn
311           [apply H3|assumption]
312         ]
313       ]
314     ]
315   |assumption
316   |apply prime_nth_prime
317   |apply lt_max_prime_factor_to_not_divides;assumption
318   ]
319 qed.
320
321 theorem sigma_p_moebius: \forall n. (S O) < n \to
322 sigma_p (S n) (\lambda y.divides_b y n) moebius = O.
323 intros.
324 lapply (exp_ord (nth_prime (max_prime_factor n)) n)
325   [rewrite > sym_times in Hletin.
326    rewrite > Hletin.
327    apply sigma_p_moebius1
328     [apply lt_O_ord_rem
329       [apply lt_SO_nth_prime_n
330       |apply lt_to_le.assumption
331       ]
332     |unfold lt.
333      change with
334       (fst ? ? (pair ? ? (S O) (S O)) \leq ord n (nth_prime (max_prime_factor n))).
335      rewrite < (p_ord_p (nth_prime (max_prime_factor n)))
336       [apply (divides_to_le_ord ? (nth_prime (max_prime_factor n)) n)
337         [apply lt_O_nth_prime_n
338         |apply lt_to_le.assumption
339         |apply prime_nth_prime
340         |apply divides_max_prime_factor_n.
341          assumption
342         ]
343       |apply lt_SO_nth_prime_n
344       ]
345     |lapply (lt_O_ord_rem (nth_prime (max_prime_factor n)) n)
346       [elim (le_to_or_lt_eq ? ? Hletin1)
347         [right.
348          apply (p_ord_to_lt_max_prime_factor1 n (max_prime_factor n) 
349           (ord n (nth_prime (max_prime_factor n)))
350           (ord_rem n (nth_prime (max_prime_factor n))))
351           [apply lt_to_le.assumption
352           |apply le_n
353           |autobatch
354           |assumption
355           ]
356         |left.apply sym_eq.assumption
357         ]
358       |apply lt_SO_nth_prime_n
359       |apply lt_to_le.assumption
360       ]
361     ]
362   |apply lt_SO_nth_prime_n
363   |apply lt_to_le.assumption
364   ]
365 qed.
366
367
368