Proof of the moebius inversion theorem

diff --git a/matita/library/Z/dirichlet_product.ma b/matita/library/Z/dirichlet_product.ma
new file mode 100644 (file)
index 0000000..c470637
--- /dev/null
+++ b/matita/library/Z/dirichlet_product.ma
@@ -0,0 +1,1022 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||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/dirichlet_product".
+
+include "Z/sigma_p.ma".
+include "Z/times.ma".
+
+definition dirichlet_product : (nat \to Z) \to (nat \to Z) \to nat \to Z \def
+\lambda f,g.\lambda n.
+sigma_p (S n) 
+ (\lambda d.divides_b d n) (\lambda d. (f d)*(g (div n d))).
+
+(* da spostare *)
+
+theorem mod_SO: \forall n:nat. mod n (S O) = O.
+intro.
+apply sym_eq.
+apply le_n_O_to_eq.
+apply le_S_S_to_le.
+apply lt_mod_m_m.
+apply le_n.
+qed.
+theorem div_SO: \forall n:nat. div n (S O) = n.
+intro.
+rewrite > (div_mod ? (S O)) in \vdash (? ? ? %)
+  [rewrite > mod_SO.
+   rewrite < plus_n_O.
+   apply times_n_SO
+  |apply le_n
+  ]
+qed.
+
+theorem and_true: \forall a,b:bool. 
+andb a b =true \to a =true \land b= true.
+intro.elim a
+  [split
+    [reflexivity|assumption]
+  |apply False_ind.
+   apply not_eq_true_false.
+   apply sym_eq.
+   assumption
+  ]
+qed.
+
+theorem lt_times_plus_times: \forall a,b,n,m:nat. 
+a < n \to b < m \to a*m + b < n*m.
+intros 3.
+apply (nat_case n)
+  [intros.apply False_ind.apply (not_le_Sn_O ? H)
+  |intros.simplify.
+   rewrite < sym_plus.
+   unfold.
+   change with (S b+a*m1 \leq m1+m*m1).
+   apply le_plus
+    [assumption
+    |apply le_times
+      [apply le_S_S_to_le.assumption
+      |apply le_n
+      ]
+    ]
+  ]
+qed.
+
+theorem divides_to_divides_b_true1 : \forall n,m:nat.
+O < m \to n \divides m \to divides_b n m = true.
+intro.
+elim (le_to_or_lt_eq O n (le_O_n n))
+  [apply divides_to_divides_b_true
+    [assumption|assumption]
+  |apply False_ind.
+   rewrite < H in H2.
+   elim H2.
+   simplify in H3.
+   apply (not_le_Sn_O O).
+   rewrite > H3 in H1.
+   assumption
+  ]
+qed.
+
+theorem divides_to_div: \forall n,m.divides n m \to m/n*n = m.
+intro.
+elim (le_to_or_lt_eq O n (le_O_n n))
+  [rewrite > plus_n_O.
+   rewrite < (divides_to_mod_O ? ? H H1).
+   apply sym_eq.
+   apply div_mod.
+   assumption
+  |elim H1.
+   generalize in match H2.
+   rewrite < H.
+   simplify.
+   intro.
+   rewrite > H3.
+   reflexivity
+  ]
+qed.
+
+theorem le_div: \forall n,m. O < n \to m/n \le m.
+intros.
+rewrite > (div_mod m n) in \vdash (? ? %)
+  [apply (trans_le ? (m/n*n))
+    [rewrite > times_n_SO in \vdash (? % ?).
+     apply le_times
+      [apply le_n|assumption]
+    |apply le_plus_n_r
+    ]
+  |assumption
+  ]
+qed.
+  
+theorem sigma_p2_eq: 
+\forall g: nat \to nat \to Z.
+\forall h11,h12,h21,h22: nat \to nat \to nat. 
+\forall n,m.
+\forall p11,p21:nat \to bool.
+\forall p12,p22:nat \to nat \to bool.
+(\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to 
+p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
+\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
+\land h11 i j < n \land h12 i j < m) \to
+(\forall i,j. i < n \to j < m \to p11 i = true \to p12 i j = true \to 
+p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
+\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
+\land (h21 i j) < n \land (h22 i j) < m) \to
+sigma_p n p11 (\lambda x:nat .sigma_p m (p12 x) (\lambda y. g x y)) =
+sigma_p n p21 (\lambda x:nat .sigma_p m (p22 x) (\lambda y. g (h11 x y) (h12 x y))).
+intros.
+rewrite < sigma_p2'.
+rewrite < sigma_p2'.
+apply sym_eq.
+letin h := (\lambda x.(h11 (x/m) (x\mod m))*m + (h12 (x/m) (x\mod m))).
+letin h1 := (\lambda x.(h21 (x/m) (x\mod m))*m + (h22 (x/m) (x\mod m))).
+apply (trans_eq ? ? 
+  (sigma_p (n*m) (\lambda x:nat.p21 (x/m)\land p22 (x/m) (x\mod m))
+  (\lambda x:nat.g ((h x)/m) ((h x)\mod m))))
+  [clear h.clear h1.
+   apply eq_sigma_p1
+    [intros.reflexivity
+    |intros.
+     cut (O < m)
+      [cut (x/m < n)
+        [cut (x \mod m < m)
+          [elim (and_true ? ? H3).
+           elim (H ? ? Hcut1 Hcut2 H4 H5).
+           elim H6.clear H6.
+           elim H8.clear H8.
+           elim H6.clear H6.
+           elim H8.clear H8.
+           apply eq_f2
+            [apply sym_eq.
+             apply div_plus_times.
+             assumption
+            |auto
+            ]
+          |apply lt_mod_m_m.
+           assumption
+          ]
+        |apply (lt_times_n_to_lt m)
+          [assumption
+          |apply (le_to_lt_to_lt ? x)
+            [apply (eq_plus_to_le ? ? (x \mod m)).
+             apply div_mod.
+             assumption
+            |assumption
+            ]
+          ]
+        ]
+      |apply not_le_to_lt.unfold.intro.
+       generalize in match H2.
+       apply (le_n_O_elim ? H4).
+       rewrite < times_n_O.
+       apply le_to_not_lt.
+       apply le_O_n  
+      ]      
+    ]
+  |apply (eq_sigma_p_gh ? h h1);intros
+    [cut (O < m)
+      [cut (i/m < n)
+        [cut (i \mod m < m)
+          [elim (and_true ? ? H3).
+           elim (H ? ? Hcut1 Hcut2 H4 H5).
+           elim H6.clear H6.
+           elim H8.clear H8.
+           elim H6.clear H6.
+           elim H8.clear H8.
+           cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))/m = 
+                 h11 (i/m) (i\mod m))
+            [cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))\mod m =
+                  h12 (i/m) (i\mod m))
+              [rewrite > Hcut3.
+               rewrite > Hcut4.
+               rewrite > H6.
+               rewrite > H12.
+               reflexivity
+              |apply mod_plus_times. 
+               assumption
+              ]
+            |apply div_plus_times.
+             assumption
+            ]
+          |apply lt_mod_m_m.
+           assumption
+          ]
+        |apply (lt_times_n_to_lt m)
+          [assumption
+          |apply (le_to_lt_to_lt ? i)
+            [apply (eq_plus_to_le ? ? (i \mod m)).
+             apply div_mod.
+             assumption
+            |assumption
+            ]
+          ]
+        ]
+      |apply not_le_to_lt.unfold.intro.
+       generalize in match H2.
+       apply (le_n_O_elim ? H4).
+       rewrite < times_n_O.
+       apply le_to_not_lt.
+       apply le_O_n  
+      ]      
+    |cut (O < m)
+      [cut (i/m < n)
+        [cut (i \mod m < m)
+          [elim (and_true ? ? H3).
+           elim (H ? ? Hcut1 Hcut2 H4 H5).
+           elim H6.clear H6.
+           elim H8.clear H8.
+           elim H6.clear H6.
+           elim H8.clear H8.
+           cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))/m = 
+                 h11 (i/m) (i\mod m))
+            [cut ((h11 (i/m) (i\mod m)*m+h12 (i/m) (i\mod m))\mod m =
+                  h12 (i/m) (i\mod m))
+              [rewrite > Hcut3.
+               rewrite > Hcut4.
+               rewrite > H10.
+               rewrite > H11.
+               apply sym_eq.
+               apply div_mod.
+               assumption
+              |apply mod_plus_times. 
+               assumption
+              ]
+            |apply div_plus_times.
+             assumption
+            ]
+          |apply lt_mod_m_m.
+           assumption
+          ]
+        |apply (lt_times_n_to_lt m)
+          [assumption
+          |apply (le_to_lt_to_lt ? i)
+            [apply (eq_plus_to_le ? ? (i \mod m)).
+             apply div_mod.
+             assumption
+            |assumption
+            ]
+          ]
+        ]
+      |apply not_le_to_lt.unfold.intro.
+       generalize in match H2.
+       apply (le_n_O_elim ? H4).
+       rewrite < times_n_O.
+       apply le_to_not_lt.
+       apply le_O_n  
+      ]      
+    |cut (O < m)
+      [cut (i/m < n)
+        [cut (i \mod m < m)
+          [elim (and_true ? ? H3).
+           elim (H ? ? Hcut1 Hcut2 H4 H5).
+           elim H6.clear H6.
+           elim H8.clear H8.
+           elim H6.clear H6.
+           elim H8.clear H8.
+           apply lt_times_plus_times
+            [assumption|assumption]
+          |apply lt_mod_m_m.
+           assumption
+          ]
+        |apply (lt_times_n_to_lt m)
+          [assumption
+          |apply (le_to_lt_to_lt ? i)
+            [apply (eq_plus_to_le ? ? (i \mod m)).
+             apply div_mod.
+             assumption
+            |assumption
+            ]
+          ]
+        ]
+      |apply not_le_to_lt.unfold.intro.
+       generalize in match H2.
+       apply (le_n_O_elim ? H4).
+       rewrite < times_n_O.
+       apply le_to_not_lt.
+       apply le_O_n  
+      ]
+    |cut (O < m)
+      [cut (j/m < n)
+        [cut (j \mod m < m)
+          [elim (and_true ? ? H3).
+           elim (H1 ? ? Hcut1 Hcut2 H4 H5).
+           elim H6.clear H6.
+           elim H8.clear H8.
+           elim H6.clear H6.
+           elim H8.clear H8.
+           cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))/m = 
+                 h21 (j/m) (j\mod m))
+            [cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))\mod m =
+                  h22 (j/m) (j\mod m))
+              [rewrite > Hcut3.
+               rewrite > Hcut4.
+               rewrite > H6.
+               rewrite > H12.
+               reflexivity
+              |apply mod_plus_times. 
+               assumption
+              ]
+            |apply div_plus_times.
+             assumption
+            ]
+          |apply lt_mod_m_m.
+           assumption
+          ] 
+        |apply (lt_times_n_to_lt m)
+          [assumption
+          |apply (le_to_lt_to_lt ? j)
+            [apply (eq_plus_to_le ? ? (j \mod m)).
+             apply div_mod.
+             assumption
+            |assumption
+            ]
+          ]
+        ]
+      |apply not_le_to_lt.unfold.intro.
+       generalize in match H2.
+       apply (le_n_O_elim ? H4).
+       rewrite < times_n_O.
+       apply le_to_not_lt.
+       apply le_O_n  
+      ] 
+    |cut (O < m)
+      [cut (j/m < n)
+        [cut (j \mod m < m)
+          [elim (and_true ? ? H3).
+           elim (H1 ? ? Hcut1 Hcut2 H4 H5).
+           elim H6.clear H6.
+           elim H8.clear H8.
+           elim H6.clear H6.
+           elim H8.clear H8.
+           cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))/m = 
+                 h21 (j/m) (j\mod m))
+            [cut ((h21 (j/m) (j\mod m)*m+h22 (j/m) (j\mod m))\mod m =
+                  h22 (j/m) (j\mod m))
+              [rewrite > Hcut3.
+               rewrite > Hcut4.               
+               rewrite > H10.
+               rewrite > H11.
+               apply sym_eq.
+               apply div_mod.
+               assumption
+              |apply mod_plus_times. 
+               assumption
+              ]
+            |apply div_plus_times.
+             assumption
+            ]
+          |apply lt_mod_m_m.
+           assumption
+          ] 
+        |apply (lt_times_n_to_lt m)
+          [assumption
+          |apply (le_to_lt_to_lt ? j)
+            [apply (eq_plus_to_le ? ? (j \mod m)).
+             apply div_mod.
+             assumption
+            |assumption
+            ]
+          ]
+        ]
+      |apply not_le_to_lt.unfold.intro.
+       generalize in match H2.
+       apply (le_n_O_elim ? H4).
+       rewrite < times_n_O.
+       apply le_to_not_lt.
+       apply le_O_n  
+      ] 
+    |cut (O < m)
+      [cut (j/m < n)
+        [cut (j \mod m < m)
+          [elim (and_true ? ? H3).
+           elim (H1 ? ? Hcut1 Hcut2 H4 H5).
+           elim H6.clear H6.
+           elim H8.clear H8.
+           elim H6.clear H6.
+           elim H8.clear H8.
+           apply (lt_times_plus_times ? ? ? m)
+            [assumption|assumption]
+          |apply lt_mod_m_m.
+           assumption
+          ] 
+        |apply (lt_times_n_to_lt m)
+          [assumption
+          |apply (le_to_lt_to_lt ? j)
+            [apply (eq_plus_to_le ? ? (j \mod m)).
+             apply div_mod.
+             assumption
+            |assumption
+            ]
+          ]
+        ]
+      |apply not_le_to_lt.unfold.intro.
+       generalize in match H2.
+       apply (le_n_O_elim ? H4).
+       rewrite < times_n_O.
+       apply le_to_not_lt.
+       apply le_O_n  
+      ]
+    ]
+  ]
+qed.
+     
+(* dirichlet_product is associative only up to extensional equality *)
+theorem associative_dirichlet_product: 
+\forall f,g,h:nat\to Z.\forall n:nat.O < n \to
+dirichlet_product (dirichlet_product f g) h n
+ = dirichlet_product f (dirichlet_product g h) n.
+intros.
+unfold dirichlet_product.
+unfold dirichlet_product.
+apply (trans_eq ? ? 
+(sigma_p (S n) (\lambda d:nat.divides_b d n)
+(\lambda d:nat
+ .sigma_p (S n) (\lambda d1:nat.divides_b d1 d) (\lambda d1:nat.f d1*g (d/d1)*h (n/d)))))
+  [apply eq_sigma_p1
+    [intros.reflexivity
+    |intros.
+     apply (trans_eq ? ? 
+     (sigma_p (S x) (\lambda d1:nat.divides_b d1 x) (\lambda d1:nat.f d1*g (x/d1)*h (n/x))))
+      [apply Ztimes_sigma_pr
+      |(* hint solleva unification uncertain ?? *)
+       apply sym_eq.
+       apply false_to_eq_sigma_p
+        [assumption
+        |intros.
+         apply not_divides_to_divides_b_false
+          [apply (lt_to_le_to_lt ? (S x))
+            [apply lt_O_S|assumption]
+          |unfold Not. intro.
+           apply (lt_to_not_le ? ? H3).
+           apply divides_to_le
+            [apply (divides_b_true_to_lt_O ? ? H H2).
+            |assumption
+            ]
+          ]
+        ]
+      ]
+    ]
+  |apply (trans_eq ? ?
+   (sigma_p (S n) (\lambda d:nat.divides_b d n)
+    (\lambda d:nat
+      .sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/d))
+      (\lambda d1:nat.f d*g d1*h ((n/d)/d1)))))
+    [apply (trans_eq ? ?
+      (sigma_p (S n) (\lambda d:nat.divides_b d n)
+       (\lambda d:nat
+        .sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/d))
+        (\lambda d1:nat.f d*g ((times d d1)/d)*h ((n/times d d1))))))
+      [apply (sigma_p2_eq 
+        (\lambda d,d1.f d1*g (d/d1)*h (n/d))
+        (\lambda d,d1:nat.times d d1) 
+        (\lambda d,d1:nat.d) 
+        (\lambda d,d1:nat.d1) 
+        (\lambda d,d1:nat.d/d1)
+        (S n)
+        (S n)
+        ?
+        ?
+        (\lambda d,d1:nat.divides_b d1 d)
+        (\lambda d,d1:nat.divides_b d1 (n/d))
+        )
+        [intros.
+         split
+          [split
+            [split
+              [split
+                [split
+                  [apply divides_to_divides_b_true1
+                    [assumption
+                    |apply (witness ? ? ((n/i)/j)).
+                     rewrite > assoc_times.
+                     rewrite > sym_times in \vdash (? ? ? (? ? %)).
+                     rewrite > divides_to_div
+                      [rewrite > sym_times. 
+                       rewrite > divides_to_div
+                        [reflexivity
+                        |apply divides_b_true_to_divides.
+                         assumption
+                        ]
+                      |apply divides_b_true_to_divides.
+                       assumption
+                      ]
+                    ]
+                  |apply divides_to_divides_b_true
+                    [apply (divides_b_true_to_lt_O ? ? H H3)
+                    |apply (witness ? ? j).
+                     reflexivity
+                    ]
+                  ]
+                |reflexivity
+                ]
+              |rewrite < sym_times.
+               rewrite > (plus_n_O (j*i)).
+               apply div_plus_times.
+               apply (divides_b_true_to_lt_O ? ? H H3)
+              ]
+            |apply (le_to_lt_to_lt ? (i*(n/i)))
+              [apply le_times
+                [apply le_n
+                |apply divides_to_le
+                  [elim (le_to_or_lt_eq ? ? (le_O_n (n/i)))
+                    [assumption
+                    |apply False_ind.
+                     apply (lt_to_not_le ? ? H).
+                     rewrite < (divides_to_div i n)
+                      [rewrite < H5.
+                       apply le_n
+                      |apply divides_b_true_to_divides.
+                       assumption
+                      ]
+                    ]
+                  |apply divides_b_true_to_divides.
+                   assumption
+                  ]
+                ]
+              |rewrite < sym_times.
+               rewrite > divides_to_div
+                [apply le_n
+                |apply divides_b_true_to_divides.
+                 assumption
+                ]
+              ]
+            ]
+          |assumption
+          ]
+        |intros.
+         split
+          [split
+            [split
+              [split
+                [split
+                  [apply divides_to_divides_b_true1
+                    [assumption
+                    |apply (transitive_divides ? i)
+                      [apply divides_b_true_to_divides.
+                       assumption
+                      |apply divides_b_true_to_divides.
+                       assumption
+                      ]
+                    ]
+                  |apply divides_to_divides_b_true
+                    [apply (divides_b_true_to_lt_O i (i/j))
+                      [apply (divides_b_true_to_lt_O ? ? ? H3).
+                       assumption
+                      |apply divides_to_divides_b_true1
+                        [apply (divides_b_true_to_lt_O ? ? ? H3).
+                         assumption
+                        |apply (witness ? ? j).
+                         apply sym_eq.
+                         apply divides_to_div.
+                         apply divides_b_true_to_divides.
+                         assumption
+                        ]
+                      ]
+                    |apply (witness ? ? (n/i)).
+                     apply (inj_times_l1 j)
+                      [apply (divides_b_true_to_lt_O ? ? ? H4).
+                       apply (divides_b_true_to_lt_O ? ? ? H3).
+                       assumption
+                      |rewrite > divides_to_div
+                        [rewrite > sym_times in \vdash (? ? ? (? % ?)).
+                         rewrite > assoc_times.
+                         rewrite > divides_to_div
+                          [rewrite > divides_to_div
+                            [reflexivity
+                            |apply divides_b_true_to_divides.
+                             assumption
+                            ]
+                          |apply divides_b_true_to_divides.
+                           assumption
+                          ]
+                        |apply (transitive_divides ? i)
+                          [apply divides_b_true_to_divides.
+                           assumption
+                          |apply divides_b_true_to_divides.
+                           assumption
+                          ]
+                        ]
+                      ]
+                    ]
+                  ]
+                |rewrite < sym_times.
+                 apply divides_to_div.
+                 apply divides_b_true_to_divides.
+                 assumption
+                ]
+              |reflexivity
+              ]
+            |assumption
+            ]
+          |apply (le_to_lt_to_lt ? i)
+            [apply le_div.
+             apply (divides_b_true_to_lt_O ? ? ? H4).
+             apply (divides_b_true_to_lt_O ? ? ? H3).
+             assumption
+            |assumption
+            ]
+          ]
+        ]
+      |apply eq_sigma_p1
+        [intros.reflexivity
+        |intros.
+         apply eq_sigma_p1
+          [intros.reflexivity
+          |intros.
+           apply eq_f2
+            [apply eq_f2
+              [reflexivity
+              |apply eq_f.
+               rewrite > sym_times.
+               rewrite > (plus_n_O (x1*x)).
+               apply div_plus_times.
+               apply (divides_b_true_to_lt_O ? ? ? H2).
+               assumption
+              ]
+            |apply eq_f.
+             cut (O < x)
+              [cut (O < x1)
+                [apply (inj_times_l1 (x*x1))
+                  [rewrite > (times_n_O O).
+                   apply lt_times;assumption
+                  |rewrite > divides_to_div
+                    [rewrite > sym_times in \vdash (? ? ? (? ? %)).
+                     rewrite < assoc_times.
+                     rewrite > divides_to_div
+                      [rewrite > divides_to_div
+                        [reflexivity
+                        |apply divides_b_true_to_divides.
+                         assumption
+                        ]
+                      |apply divides_b_true_to_divides.
+                       assumption
+                      ]
+                    |elim (divides_b_true_to_divides ? ? H4).
+                     apply (witness ? ? n2).
+                     rewrite > assoc_times.
+                     rewrite < H5.
+                     rewrite < sym_times.
+                     apply sym_eq.
+                     apply divides_to_div.
+                     apply divides_b_true_to_divides.
+                     assumption
+                    ]
+                  ]
+                |apply (divides_b_true_to_lt_O ? ? ? H4).
+                 apply (lt_times_n_to_lt x)
+                  [assumption
+                  |simplify.
+                   rewrite > divides_to_div
+                    [assumption
+                    |apply (divides_b_true_to_divides ? ? H2).
+                     assumption
+                    ]
+                  ]
+                ]
+              |apply (divides_b_true_to_lt_O ? ? ? H2).
+               assumption
+              ]
+            ]
+          ]
+        ]
+      ]
+    |apply eq_sigma_p1
+      [intros.reflexivity
+      |intros.
+       apply (trans_eq ? ? 
+       (sigma_p (S n) (\lambda d1:nat.divides_b d1 (n/x)) (\lambda d1:nat.f x*(g d1*h (n/x/d1)))))
+        [apply eq_sigma_p
+          [intros.reflexivity
+          |intros.apply assoc_Ztimes
+          ]
+        |apply (trans_eq ? ? 
+          (sigma_p (S (n/x)) (\lambda d1:nat.divides_b d1 (n/x)) (\lambda d1:nat.f x*(g d1*h (n/x/d1)))))
+          [apply false_to_eq_sigma_p
+            [apply le_S_S.
+             cut (O < x)
+              [apply (le_times_to_le x)
+                [assumption
+                |rewrite > sym_times.
+                 rewrite > divides_to_div
+                  [apply le_times_n.
+                   assumption
+                  |apply divides_b_true_to_divides.
+                   assumption
+                  ]
+                ]
+              |apply (divides_b_true_to_lt_O ? ? ? H2).
+               assumption
+              ]
+            |intros.
+             apply not_divides_to_divides_b_false
+              [apply (trans_le ? ? ? ? H3).
+               apply le_S_S.
+               apply le_O_n
+              |unfold Not.intro.
+               apply (le_to_not_lt ? ? H3).
+               apply le_S_S.
+               apply divides_to_le
+                [apply (lt_times_n_to_lt x)
+                  [apply (divides_b_true_to_lt_O ? ? ? H2).
+                   assumption
+                  |simplify.
+                   rewrite > divides_to_div
+                    [assumption
+                    |apply (divides_b_true_to_divides ? ? H2).
+                     assumption
+                    ]
+                  ]
+                |assumption
+                ]
+              ]
+            ]
+          |apply sym_eq.
+           apply Ztimes_sigma_pl
+          ]
+        ]
+      ]
+    ]
+  ]
+qed.
+
+definition is_one: nat \to Z \def 
+\lambda n.
+  match n with
+  [O \Rightarrow OZ
+  | (S p) \Rightarrow 
+    match p with
+    [ O \Rightarrow pos O
+    | (S q) \Rightarrow OZ]]
+.
+
+theorem is_one_OZ: \forall n. n \neq S O \to is_one n = OZ.
+intro.apply (nat_case n)
+  [intro.reflexivity
+  |intro. apply (nat_case m)
+    [intro.apply False_ind.apply H.reflexivity
+    |intros.reflexivity
+    ]
+  ]
+qed.
+
+(* da spostare in times *)
+definition Zone \def pos O.
+
+theorem Ztimes_Zone_l: \forall z:Z. Ztimes Zone z = z.
+intro.unfold Zone.simplify.
+elim z;simplify
+  [reflexivity
+  |rewrite < plus_n_O.reflexivity
+  |rewrite < plus_n_O.reflexivity
+  ]
+qed.
+
+theorem Ztimes_Zone_r: \forall z:Z. Ztimes z Zone = z.
+intro.
+rewrite < sym_Ztimes.
+apply Ztimes_Zone_l.
+qed.
+
+theorem injective_Zplus_l: \forall x:Z.injective Z Z (\lambda y.y+x).
+intro.simplify.intros (z y).
+rewrite < Zplus_z_OZ.
+rewrite < (Zplus_z_OZ y).
+rewrite < (Zplus_Zopp x).
+rewrite < (Zplus_Zopp x).
+rewrite < assoc_Zplus.
+rewrite < assoc_Zplus.
+apply eq_f2
+  [assumption|reflexivity]
+qed.
+
+theorem injective_Zplus_r: \forall x:Z.injective Z Z (\lambda y.x+y).
+intro.simplify.intros (z y).
+apply (injective_Zplus_l x).
+rewrite < sym_Zplus.
+rewrite > H.
+apply sym_Zplus.
+qed.
+
+theorem sigma_p_OZ:
+\forall p: nat \to bool.\forall n.sigma_p n p (\lambda m.OZ) = OZ.
+intros.elim n
+  [reflexivity
+  |apply (bool_elim ? (p n1));intro
+    [rewrite > true_to_sigma_p_Sn
+      [rewrite > sym_Zplus. 
+       rewrite > Zplus_z_OZ. 
+       assumption
+      |assumption
+      ]
+    |rewrite > false_to_sigma_p_Sn
+      [assumption
+      |assumption
+      ]
+    ]
+  ]
+qed.
+
+theorem dirichlet_product_is_one_r: 
+\forall f:nat\to Z.\forall n:nat.
+  dirichlet_product f is_one n = f n.
+intros.
+elim n
+  [unfold dirichlet_product.
+   rewrite > true_to_sigma_p_Sn
+    [rewrite > Ztimes_Zone_r.
+     rewrite > Zplus_z_OZ.
+     reflexivity
+    |reflexivity
+    ]
+  |unfold dirichlet_product.
+   rewrite > true_to_sigma_p_Sn
+    [rewrite > div_n_n
+      [rewrite > Ztimes_Zone_r.
+       rewrite < Zplus_z_OZ in \vdash (? ? ? %).
+       apply eq_f2
+        [reflexivity
+        |apply (trans_eq ? ? (sigma_p (S n1) 
+          (\lambda d:nat.divides_b d (S n1)) (\lambda d:nat.OZ)))
+          [apply eq_sigma_p1;intros
+            [reflexivity
+            |rewrite > is_one_OZ
+              [apply Ztimes_z_OZ
+              |unfold Not.intro.
+               apply (lt_to_not_le ? ? H1).
+               rewrite > (times_n_SO x).
+               rewrite > sym_times.
+               rewrite < H3.
+               rewrite > (div_mod ? x) in \vdash (? % ?)
+                [rewrite > divides_to_mod_O
+                  [rewrite < plus_n_O.
+                   apply le_n
+                  |apply (divides_b_true_to_lt_O ? ? ? H2).
+                   apply lt_O_S
+                  |apply divides_b_true_to_divides.
+                   assumption
+                  ]
+                |apply (divides_b_true_to_lt_O ? ? ? H2).
+                 apply lt_O_S
+                ]
+              ]
+            ]
+          |apply sigma_p_OZ
+          ]
+        ]
+      |apply lt_O_S
+      ]
+    |apply divides_to_divides_b_true
+      [apply lt_O_S
+      |apply divides_n_n
+      ]
+    ]
+  ]
+qed.           
+
+(* da spostare *)
+theorem notb_notb: \forall b:bool. notb (notb b) = b.
+intros.
+elim b;reflexivity.
+qed.
+
+theorem injective_notb: injective bool bool notb.
+unfold injective.
+intros.
+rewrite < notb_notb.
+rewrite < (notb_notb y).
+apply eq_f.
+assumption.
+qed.
+
+theorem divides_div: \forall d,n. divides d n \to divides (n/d) n.
+intros.
+apply (witness ? ? d).
+apply sym_eq.
+apply divides_to_div.
+assumption.
+qed.
+
+theorem divides_b_div_true: 
+\forall d,n. O < n \to 
+  divides_b d n = true \to divides_b (n/d) n = true.
+intros.
+apply divides_to_divides_b_true1
+  [assumption
+  |apply divides_div.
+   apply divides_b_true_to_divides.
+   assumption
+  ]
+qed.
+
+theorem div_div: \forall n,d:nat. O < n \to divides d n \to 
+n/(n/d) = d.
+intros.
+apply (inj_times_l1 (n/d))
+  [apply (lt_times_n_to_lt d)
+    [apply (divides_to_lt_O ? ? H H1).
+    |rewrite > divides_to_div;assumption
+    ]
+  |rewrite > divides_to_div
+    [rewrite > sym_times.
+     rewrite > divides_to_div
+      [reflexivity
+      |assumption
+      ]
+    |apply (witness ? ? d).
+     apply sym_eq.
+     apply divides_to_div.
+     assumption
+    ]
+  ]
+qed.
+
+theorem commutative_dirichlet_product: \forall f,g:nat \to Z.\forall n. O < n \to 
+dirichlet_product f g n = dirichlet_product g f n.
+intros.
+unfold dirichlet_product.
+apply (trans_eq ? ?
+  (sigma_p (S n) (\lambda d:nat.divides_b d n)
+  (\lambda d:nat.g (n/d) * f (n/(n/d)))))
+  [apply eq_sigma_p1;intros
+    [reflexivity
+    |rewrite > div_div
+      [apply sym_Ztimes.
+      |assumption
+      |apply divides_b_true_to_divides.
+       assumption
+      ]
+    ]
+  |apply (eq_sigma_p_gh ? (\lambda d.(n/d)) (\lambda d.(n/d))) 
+    [intros.
+     apply divides_b_div_true;assumption
+    |intros.
+     apply div_div
+      [assumption
+      |apply divides_b_true_to_divides.
+       assumption
+      ]
+    |intros.
+     apply le_S_S.
+     apply le_div.
+     apply (divides_b_true_to_lt_O ? ? H H2)
+    |intros.
+     apply divides_b_div_true;assumption
+    |intros.
+     apply div_div
+      [assumption
+      |apply divides_b_true_to_divides.
+       assumption
+      ]
+    |intros.
+     apply le_S_S.
+     apply le_div.
+     apply (divides_b_true_to_lt_O ? ? H H2)
+    ]
+  ]
+qed.
+
+theorem dirichlet_product_is_one_l: 
+\forall f:nat\to Z.\forall n:nat.
+O < n \to dirichlet_product is_one f n = f n.
+intros.
+rewrite > commutative_dirichlet_product.
+apply dirichlet_product_is_one_r.
+assumption.
+qed.
+
+theorem dirichlet_product_one_r: 
+\forall f:nat\to Z.\forall n:nat. O < n \to 
+dirichlet_product f (\lambda n.Zone) n = 
+sigma_p (S n) (\lambda d.divides_b d n) f.
+intros.
+unfold dirichlet_product.
+apply eq_sigma_p;intros
+  [reflexivity
+  |simplify in \vdash (? ? (? ? %) ?).
+   apply Ztimes_Zone_r
+  ]
+qed.
+              
+theorem dirichlet_product_one_l: 
+\forall f:nat\to Z.\forall n:nat. O < n \to 
+dirichlet_product (\lambda n.Zone) f n = 
+sigma_p (S n) (\lambda d.divides_b d n) f. 
+intros.
+rewrite > commutative_dirichlet_product
+  [apply dirichlet_product_one_r.
+   assumption
+  |assumption
+  ]
+qed.

diff --git a/matita/library/Z/inversion.ma b/matita/library/Z/inversion.ma
new file mode 100644 (file)
index 0000000..d93a752
--- /dev/null
+++ b/matita/library/Z/inversion.ma
@@ -0,0 +1,101 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||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/inversion".
+
+include "Z/dirichlet_product.ma".
+include "Z/moebius.ma".
+
+definition sigma_div: (nat \to Z) \to nat \to Z \def
+\lambda f.\lambda n. sigma_p (S n) (\lambda d.divides_b d n) f.
+
+theorem sigma_div_moebius:
+\forall n:nat. O < n \to sigma_div moebius n = is_one n.
+intros.elim H
+  [reflexivity
+  |rewrite > is_one_OZ  
+    [unfold sigma_div.
+     apply sigma_p_moebius.
+     apply le_S_S.
+     assumption
+    |unfold Not.intro.
+     apply (lt_to_not_eq ? ? H1).
+     apply injective_S.
+     apply sym_eq.
+     assumption
+    ]
+  ]
+qed.
+  
+(* moebius inversion theorem *)
+theorem inversion: \forall f:nat \to Z.\forall n:nat.O < n \to
+dirichlet_product moebius (sigma_div f) n = f n.
+intros.
+rewrite > commutative_dirichlet_product
+  [apply (trans_eq ? ? (dirichlet_product (dirichlet_product f (\lambda n.Zone)) moebius n))
+    [unfold dirichlet_product.
+     apply eq_sigma_p1;intros
+      [reflexivity
+      |apply eq_f2
+        [apply sym_eq.
+         unfold sigma_div.
+         apply dirichlet_product_one_r.
+         apply (divides_b_true_to_lt_O ? ? H H2)
+        |reflexivity
+        ]
+      ]
+    |rewrite > associative_dirichlet_product
+      [apply (trans_eq ? ? (dirichlet_product f (sigma_div moebius) n))
+        [unfold dirichlet_product.
+         apply eq_sigma_p1;intros
+          [reflexivity
+          |apply eq_f2
+            [reflexivity
+            |unfold sigma_div.
+             apply dirichlet_product_one_l.
+             apply (lt_times_n_to_lt x)
+              [apply (divides_b_true_to_lt_O ? ? H H2)
+              |rewrite > divides_to_div
+                [assumption
+                |apply (divides_b_true_to_divides ? ? H2)
+                ]
+              ]
+            ]
+          ]
+        |apply (trans_eq ? ? (dirichlet_product f is_one n))
+          [unfold dirichlet_product.
+           apply eq_sigma_p1;intros
+            [reflexivity
+            |apply eq_f2
+              [reflexivity
+              |apply sigma_div_moebius.
+               apply (lt_times_n_to_lt x)
+                [apply (divides_b_true_to_lt_O ? ? H H2)
+                |rewrite > divides_to_div
+                  [assumption
+                  |apply (divides_b_true_to_divides ? ? H2)
+                  ]
+                ]
+              ]
+            ]
+          |apply dirichlet_product_is_one_r
+          ]
+        ]
+      |assumption
+      ]
+    ]
+  |assumption
+  ]
+qed.
+        
\ No newline at end of file

diff --git a/matita/library/Z/moebius.ma b/matita/library/Z/moebius.ma
index e91bf8df912b6b1748868ff8ab2d4580ac43b871..98ffccd40f29c59b52c65e3b6c1b813ed69059bc 100644 (file)
--- a/matita/library/Z/moebius.ma
+++ b/matita/library/Z/moebius.ma
@@ -527,3 +527,6 @@ lapply (exp_ord (nth_prime (max_prime_factor n)) n)
   |apply lt_to_le.assumption
   ]
 qed.
+
+
+

diff --git a/matita/library/Z/sigma_p.ma b/matita/library/Z/sigma_p.ma
index 27baf8db5b81580ae37095d4602f824976ffa729..73b29a38c0773b14f86ee84f07403a2419441498 100644 (file)
--- a/matita/library/Z/sigma_p.ma
+++ b/matita/library/Z/sigma_p.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/Z/sigma_p.ma".
 
-include "Z/plus.ma".
+include "Z/times.ma".
 include "nat/primes.ma".
 include "nat/ord.ma".
 
@@ -220,6 +220,68 @@ elim n
   ]
 qed.
 
+(* a stronger, dependent version, required e.g. for dirichlet product *)
+theorem sigma_p2' : 
+\forall n,m:nat.
+\forall p1:nat \to bool.
+\forall p2:nat \to nat \to bool.
+\forall g: nat \to nat \to Z.
+sigma_p (n*m) 
+  (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x m))) 
+  (\lambda x.g (div x m) (mod x m)) =
+sigma_p n p1 
+  (\lambda x.sigma_p m (p2 x) (g x)).
+intros.
+elim n
+  [simplify.reflexivity
+  |apply (bool_elim ? (p1 n1))
+    [intro.
+     rewrite > (true_to_sigma_p_Sn ? ? ? H1).
+     simplify in \vdash (? ? (? % ? ?) ?);
+     rewrite > sigma_p_plus.
+     rewrite < H.
+     apply eq_f2
+      [apply eq_sigma_p
+        [intros.
+         rewrite > sym_plus.
+         rewrite > (div_plus_times ? ? ? H2).
+         rewrite > (mod_plus_times ? ? ? H2).
+         rewrite > H1.
+         simplify.reflexivity
+        |intros.
+         rewrite > sym_plus.
+         rewrite > (div_plus_times ? ? ? H2).
+         rewrite > (mod_plus_times ? ? ? H2).
+         rewrite > H1.
+         simplify.reflexivity.   
+        ]
+      |reflexivity
+      ]
+    |intro.
+     rewrite > (false_to_sigma_p_Sn ? ? ? H1).
+     simplify in \vdash (? ? (? % ? ?) ?);
+     rewrite > sigma_p_plus.
+     rewrite > H.
+     apply (trans_eq ? ? (O+(sigma_p n1 p1 (\lambda x:nat.sigma_p m (p2 x) (g x)))))
+      [apply eq_f2
+        [rewrite > (eq_sigma_p ? (\lambda x.false) ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
+          [apply sigma_p_false
+          |intros.
+           rewrite > sym_plus.
+           rewrite > (div_plus_times ? ? ? H2).
+           rewrite > (mod_plus_times ? ? ? H2).
+           rewrite > H1.
+           simplify.reflexivity
+          |intros.reflexivity.
+          ]
+        |reflexivity
+        ]
+      |reflexivity   
+      ]
+    ]
+  ]
+qed.
+
 lemma sigma_p_gi: \forall g: nat \to Z.
 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to 
 sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
@@ -431,45 +493,41 @@ elim n
   ]
 qed.
 
-definition p_ord_times \def
-\lambda p,m,x.
-  match p_ord x p with
-  [pair q r \Rightarrow r*m+q].
-  
-theorem  eq_p_ord_times: \forall p,m,x.
-p_ord_times p m x = (ord_rem x p)*m+(ord x p).
-intros.unfold p_ord_times. unfold ord_rem.
-unfold ord.
-elim (p_ord x p).
-reflexivity.
-qed.
-
-theorem div_p_ord_times: 
-\forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
-intros.rewrite > eq_p_ord_times.
-apply div_plus_times.
-assumption.
-qed.
-
-theorem mod_p_ord_times: 
-\forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
-intros.rewrite > eq_p_ord_times.
-apply mod_plus_times.
-assumption.
-qed.
-
-theorem times_O_to_O: \forall n,m:nat.n*m = O \to n = O \lor m= O.
-apply nat_elim2;intros
-  [left.reflexivity
-  |right.reflexivity
-  |apply False_ind.
-   simplify in H1.
-   apply (not_eq_O_S ? (sym_eq  ? ? ? H1))
+(* sigma_p and Ztimes *)
+lemma Ztimes_sigma_pl: \forall z:Z.\forall n:nat.\forall p. \forall f.
+z * (sigma_p n p f) = sigma_p n p (\lambda i.z*(f i)).
+intros.
+elim n
+  [rewrite > Ztimes_z_OZ.reflexivity
+  |apply (bool_elim ? (p n1)); intro
+    [rewrite > true_to_sigma_p_Sn
+      [rewrite > true_to_sigma_p_Sn 
+        [rewrite < H.
+         apply distr_Ztimes_Zplus
+        |assumption
+        ]
+      |assumption
+      ]
+    |rewrite > false_to_sigma_p_Sn
+      [rewrite > false_to_sigma_p_Sn
+        [assumption
+        |assumption
+        ]
+      |assumption
+      ] 
+    ]
   ]
 qed.
 
-theorem prime_to_lt_O: \forall p. prime p \to O < p.
-intros.elim H.apply lt_to_le.assumption.
+lemma Ztimes_sigma_pr: \forall z:Z.\forall n:nat.\forall p. \forall f.
+(sigma_p n p f) * z = sigma_p n p (\lambda i.(f i)*z).
+intros.
+rewrite < sym_Ztimes.
+rewrite > Ztimes_sigma_pl.
+apply eq_sigma_p
+  [intros.reflexivity
+  |intros.apply sym_Ztimes
+  ]
 qed.
 
 theorem divides_exp_to_lt_ord:\forall n,m,j,p. O < n \to prime p \to
@@ -563,7 +621,7 @@ cut (O < p)
     (sigma_p (S n*S m) (\lambda x:nat.divides_b (x/S m) n)
        (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m)))))
     [apply sym_eq.
-     apply (eq_sigma_p_gh g ? (p_ord_times p (S m)))
+     apply (eq_sigma_p_gh g ? (p_ord_inv p (S m)))
       [intros.
        lapply (divides_b_true_to_lt_O ? ? H H4).
        apply divides_to_divides_b_true
@@ -584,7 +642,7 @@ cut (O < p)
         ]
       |intros.
        lapply (divides_b_true_to_lt_O ? ? H H4).
-       unfold p_ord_times.
+       unfold p_ord_inv.
        rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
         [change with ((i/S m)*S m+i \mod S m=i).
          apply sym_eq.
@@ -615,7 +673,7 @@ cut (O < p)
         ]
       |intros.
        cut (ord j p < S m)
-        [rewrite > div_p_ord_times
+        [rewrite > div_p_ord_inv
           [apply divides_to_divides_b_true
             [apply lt_O_ord_rem
               [elim H1.assumption
@@ -636,8 +694,8 @@ cut (O < p)
         ]
       |intros.
        cut (ord j p < S m)
-        [rewrite > div_p_ord_times
-          [rewrite > mod_p_ord_times
+        [rewrite > div_p_ord_inv
+          [rewrite > mod_p_ord_inv
             [rewrite > sym_times.
              apply sym_eq.
              apply exp_ord
@@ -658,7 +716,7 @@ cut (O < p)
          apply (divides_b_true_to_lt_O ? ? H4).
         ]
       |intros.
-       rewrite > eq_p_ord_times.
+       rewrite > eq_p_ord_inv.
        rewrite > sym_plus.
        apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
         [apply lt_plus_l.