X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Flibrary%2FZ%2Fmoebius.ma;fp=matita%2Flibrary%2FZ%2Fmoebius.ma;h=1eb35852155109194babd46f20c0992e24516182;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/library/Z/moebius.ma b/matita/library/Z/moebius.ma
new file mode 100644
index 000000000..1eb358521
--- /dev/null
+++ b/matita/library/Z/moebius.ma
@@ -0,0 +1,368 @@
+(**************************************************************************)
+(*       ___	                                                            *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        Matita is distributed under the terms of the          *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/Z/moebius".
+
+include "nat/factorization.ma".
+include "Z/sigma_p.ma".
+  
+let rec moebius_aux p n : Z \def
+  match p with 
+  [ O \Rightarrow pos O
+  | (S p1) \Rightarrow 
+    match p_ord n (nth_prime p1) with
+    [ (pair q r) \Rightarrow
+      match q with
+      [ O \Rightarrow moebius_aux p1 r
+      | (S q1) \Rightarrow
+	      match q1 with 
+	      [ O \Rightarrow Zopp (moebius_aux p1 r) 
+        | (S q2) \Rightarrow OZ
+        ]
+      ]
+    ]
+  ]
+.
+
+definition moebius : nat \to Z \def
+\lambda n.
+  let p \def (max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)) in
+  moebius_aux (S p) n.
+
+(*
+theorem moebius_O : moebius O = pos O.
+simplify. reflexivity.
+qed.
+      
+theorem moebius_SO : moebius (S O) = pos O.
+simplify.reflexivity.
+qed.  
+
+theorem moebius_SSO : moebius (S (S O)) = neg O.
+simplify.reflexivity.
+qed.  
+
+theorem moebius_SSSO : moebius (S (S (S O))) = neg O.
+simplify.reflexivity.
+qed.
+
+theorem moebius_SSSSO : moebius (S (S (S (S O)))) = OZ.
+simplify.reflexivity.
+qed.
+*)
+
+theorem not_divides_to_eq_moebius_aux: \forall n,p,p1.p \le p1 \to
+(\forall i. p \le i \to i \le p1 \to Not (divides (nth_prime i) n))
+\to moebius_aux p n = moebius_aux p1 n.
+intros 4.
+elim H
+  [reflexivity
+  |simplify.
+   rewrite > not_divides_to_p_ord_O
+    [simplify.apply H2.intros.
+     apply H3[assumption|apply le_S.assumption]
+    |apply H3[assumption|apply le_n_Sn]
+    ]
+  ]
+qed.
+
+theorem eq_moebius_moebius_aux: \forall n,p. 
+max_prime_factor n < p \to p \le n \to
+moebius n = moebius_aux p n.
+intros.
+unfold moebius.
+change with 
+(moebius_aux (S (max n (\lambda p:nat.eqb (n\mod nth_prime p) O))) n
+= moebius_aux p n).
+apply not_divides_to_eq_moebius_aux
+  [assumption
+  |intros.
+   apply divides_b_false_to_not_divides.
+   unfold divides_b.
+   apply (lt_max_to_false ? n i)
+    [assumption
+    |apply (trans_le ? p)[assumption|assumption]
+    ]
+  ]
+qed.
+
+theorem moebius_aux_SO: \forall p.moebius_aux p (S O) = pos O.
+intros.
+elim p
+  [simplify.reflexivity
+  |rewrite < H.
+   apply sym_eq.
+   apply not_divides_to_eq_moebius_aux
+   [apply le_n_Sn
+   |intros.unfold.intro.
+    absurd (nth_prime i \le S O)
+      [apply divides_to_le
+        [apply le_n|assumption]
+      |apply lt_to_not_le.
+       apply lt_SO_nth_prime_n.
+      ]
+    ]
+  ]
+qed.
+
+theorem p_ord_SO_SO_to_moebius : \forall n,p.
+  (S O) < n \to
+  p = max_prime_factor n \to
+  p_ord n (nth_prime p) = pair nat nat (S O) (S O) \to
+  moebius n = Zopp (pos O).
+intros.
+change with 
+  (moebius_aux (S (max_prime_factor n)) n = neg O).
+rewrite < H1.simplify.
+rewrite > H2.simplify.
+rewrite > moebius_aux_SO.
+reflexivity.
+qed.
+
+theorem p_ord_SO_r_to_moebius1 : \forall n,p,r.
+  (S O) < n \to 
+  p = max_prime_factor n \to
+  (S O) < r \to 
+  p_ord n (nth_prime p) = pair nat nat (S O) r \to
+  moebius n = Zopp (moebius r).
+intros.
+change with 
+  (moebius_aux (S (max_prime_factor n)) n = -(moebius r)).
+rewrite < H1.simplify.
+rewrite > H3.simplify.
+apply eq_f.
+apply sym_eq.
+change with 
+ (moebius_aux (S (max_prime_factor r)) r = moebius_aux p r).
+apply not_divides_to_eq_moebius_aux
+  [apply (p_ord_to_lt_max_prime_factor n p (S O) ? ? H1)
+    [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
+    |apply sym_eq. assumption
+    |assumption
+    ]
+  |intros.
+   lapply (decidable_le i r).
+   elim Hletin
+    [apply divides_b_false_to_not_divides.
+     apply (lt_max_to_false ? r i)[assumption|assumption]
+    |unfold.intro.apply H6.
+     apply (trans_le ? (nth_prime i))
+      [apply lt_to_le.
+       apply lt_n_nth_prime_n
+      |apply divides_to_le
+        [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
+        |assumption
+        ]
+      ]
+    ]
+  ]
+qed.
+
+theorem p_ord_SO_r_to_moebius : \forall n,p,r.
+  (S O) < n \to 
+  p = max_prime_factor n \to
+  p_ord n (nth_prime p) = pair nat nat (S O) r \to
+  moebius n = Zopp (moebius r).
+intros 5.
+apply (nat_case r);intro
+  [apply False_ind.
+   apply (p_ord_to_not_eq_O ? ? ? ? H H2).
+   reflexivity
+  |apply (nat_case m);intros
+    [simplify.apply (p_ord_SO_SO_to_moebius ? ? H H1 H2)
+    |apply (p_ord_SO_r_to_moebius1 ? ? ? H H1 ? H2).
+     apply le_S_S.apply le_S_S.apply le_O_n
+    ]
+  ]
+qed.    
+
+theorem p_ord_SSq_r_to_moebius : \forall n,p,q,r.
+  (S O) < n \to
+  p = max_prime_factor n \to
+  p_ord n (nth_prime p) = pair nat nat (S (S q)) r \to
+  moebius n = OZ.
+intros.
+change with
+  (moebius_aux (S (max n (\lambda p:nat.eqb (n\mod nth_prime p) O))) n =OZ).
+rewrite < H1.simplify.
+rewrite > H2.simplify.
+reflexivity.
+qed.
+
+theorem moebius_exp: \forall p,q,r:nat. O < r \to
+r = (S O) \lor (max_prime_factor r) < p \to
+(* r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to *)
+sigma_p (S (S q)) (\lambda y.true) (\lambda y.moebius (r*(exp (nth_prime p) y))) = O.
+intros.
+elim q
+  [rewrite > true_to_sigma_p_Sn
+    [rewrite > true_to_sigma_p_Sn
+      [rewrite > Zplus_z_OZ.
+       rewrite < times_n_SO.
+       rewrite > (p_ord_SO_r_to_moebius ? p r)
+        [rewrite > sym_Zplus.
+         rewrite > Zplus_Zopp.
+         reflexivity
+        |rewrite < exp_n_SO.
+         rewrite > sym_times.
+         rewrite > times_n_SO.
+         apply lt_to_le_to_lt_times
+          [apply lt_SO_nth_prime_n
+          |assumption
+          |assumption
+          ]
+        |apply eq_p_max
+          [apply le_n|assumption|assumption]
+        |apply p_ord_exp1
+          [apply lt_O_nth_prime_n
+          |apply lt_max_prime_factor_to_not_divides;assumption
+          |apply sym_times
+          ]
+        ]
+      |reflexivity
+      ]
+    |reflexivity
+    ]
+  |rewrite > true_to_sigma_p_Sn
+    [rewrite > H2.
+     rewrite > Zplus_z_OZ.
+     apply (p_ord_SSq_r_to_moebius ? p n r)
+      [rewrite > times_n_SO.
+       rewrite > sym_times in \vdash (? ? %).
+       apply lt_to_le_to_lt_times
+        [apply (trans_lt ? (nth_prime p))
+          [apply lt_SO_nth_prime_n
+            |rewrite > exp_n_SO in \vdash (? % ?).
+             apply lt_exp
+              [apply lt_SO_nth_prime_n
+              |apply le_S_S.apply le_S_S.apply le_O_n
+              ]
+            ]
+          |assumption
+          |assumption
+          ]
+        |apply eq_p_max
+          [apply le_S_S.apply le_O_n|assumption|assumption]  
+        |apply p_ord_exp1
+          [apply lt_O_nth_prime_n
+          |apply lt_max_prime_factor_to_not_divides;assumption        
+          |apply sym_times
+          ]
+        ]
+      |reflexivity
+      ]
+    ]   
+qed.
+  
+theorem sigma_p_moebius1: \forall n,m,p:nat.O < n \to O < m \to 
+n = (S O) \lor max_prime_factor n < p \to
+sigma_p (S (n*(exp (nth_prime p) m))) (\lambda y.divides_b y (n*(exp (nth_prime p) m))) moebius = O.
+intros.
+rewrite > sigma_p_divides_b
+  [apply (trans_eq ? ? (sigma_p (S n) (\lambda x:nat.divides_b x n) (\lambda x:nat.OZ)))
+    [apply eq_sigma_p1
+      [intros.reflexivity
+      |apply (lt_O_n_elim m H1).
+       intros.apply moebius_exp
+        [apply (divides_b_true_to_lt_O ? ? ? H4).
+         assumption
+        |elim H2
+          [left.rewrite > H5 in H3.
+           elim (le_to_or_lt_eq ? ? (le_S_S_to_le ? ? H3))
+            [apply False_ind.
+             apply (lt_to_not_le O x)
+              [apply (divides_b_true_to_lt_O n x H H4)
+              |apply le_S_S_to_le.assumption
+              ]
+            |assumption
+            ]
+          |right.
+           apply (le_to_lt_to_lt ? ? ? ? H5).
+           apply (divides_to_max_prime_factor1 x n)
+            [apply (divides_b_true_to_lt_O ? ? H H4)
+            |assumption
+            |apply divides_b_true_to_divides.
+             assumption
+            ]
+          ]
+        ]
+      ]
+    |generalize in match (\lambda x:nat.divides_b x n).
+     intro.
+     elim n
+      [simplify.elim (f O);reflexivity
+      |apply (bool_elim ? (f (S n1)))
+        [intro.
+         rewrite > true_to_sigma_p_Sn
+          [rewrite > H3.reflexivity|assumption]
+        |intro.
+         rewrite > false_to_sigma_p_Sn
+          [apply H3|assumption]
+        ]
+      ]
+    ]
+  |assumption
+  |apply prime_nth_prime
+  |apply lt_max_prime_factor_to_not_divides;assumption
+  ]
+qed.
+
+theorem sigma_p_moebius: \forall n. (S O) < n \to
+sigma_p (S n) (\lambda y.divides_b y n) moebius = O.
+intros.
+lapply (exp_ord (nth_prime (max_prime_factor n)) n)
+  [rewrite > sym_times in Hletin.
+   rewrite > Hletin.
+   apply sigma_p_moebius1
+    [apply lt_O_ord_rem
+      [apply lt_SO_nth_prime_n
+      |apply lt_to_le.assumption
+      ]
+    |unfold lt.
+     change with
+      (fst ? ? (pair ? ? (S O) (S O)) \leq ord n (nth_prime (max_prime_factor n))).
+     rewrite < (p_ord_p (nth_prime (max_prime_factor n)))
+      [apply (divides_to_le_ord ? (nth_prime (max_prime_factor n)) n)
+        [apply lt_O_nth_prime_n
+        |apply lt_to_le.assumption
+        |apply prime_nth_prime
+        |apply divides_max_prime_factor_n.
+         assumption
+        ]
+      |apply lt_SO_nth_prime_n
+      ]
+    |lapply (lt_O_ord_rem (nth_prime (max_prime_factor n)) n)
+      [elim (le_to_or_lt_eq ? ? Hletin1)
+        [right.
+         apply (p_ord_to_lt_max_prime_factor1 n (max_prime_factor n) 
+          (ord n (nth_prime (max_prime_factor n)))
+          (ord_rem n (nth_prime (max_prime_factor n))))
+          [apply lt_to_le.assumption
+          |apply le_n
+          |autobatch
+          |assumption
+          ]
+        |left.apply sym_eq.assumption
+        ]
+      |apply lt_SO_nth_prime_n
+      |apply lt_to_le.assumption
+      ]
+    ]
+  |apply lt_SO_nth_prime_n
+  |apply lt_to_le.assumption
+  ]
+qed.
+
+
+