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.ma".
  16
  17 include "Z/times.ma".
  18 include "nat/primes.ma".
  19 include "nat/ord.ma".
  20 include "nat/generic_sigma_p.ma".
  21
  22 (* sigma_p in Z is a specialization of sigma_p_gen *)
  23 definition sigma_p: nat \to (nat \to bool) \to (nat \to Z) \to Z \def
  24 \lambda n, p, g. (sigma_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_sigma_p_Sn_gen.
  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_sigma_p_Sn_gen.
  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_sigma_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_sigma_p1_gen;
  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 sigma_p_false_gen.
  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 (sigma_p_plusA_gen 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_sigma_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 (sigma_p2_gen 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 (sigma_p2_gen' 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 (sigma_p_gi_gen)
 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 (\lambda x.p2 x) g.
 172 intros.
 173 unfold sigma_p.
 174 apply (eq_sigma_p_gh_gen 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 sigma_p_divides_b:
 190 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
 191 \forall g: nat \to Z.
 192 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
 193 sigma_p (S n) (\lambda x.divides_b x n)
 194   (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
 195 intros.
 196 unfold sigma_p.
 197 apply (sigma_p_divides_gen Z OZ Zplus n m p ? ? ? g)
 198 [ assumption
 199 | assumption
 200 | assumption
 201 | apply symmetricZPlus
 202 | apply associative_Zplus
 203 | intros.
 204   apply Zplus_z_OZ
 205 ]
 206 qed.
 207
 208
 209 (* sigma_p and Ztimes *)
 210 lemma Ztimes_sigma_pl: \forall z:Z.\forall n:nat.\forall p. \forall f.
 211 z * (sigma_p n p f) = sigma_p n p (\lambda i.z*(f i)).
 212 intros.
 213 apply (distributive_times_plus_sigma_p_generic Z Zplus OZ Ztimes n z p f)
 214 [ apply symmetricZPlus
 215 | apply associative_Zplus
 216 | intros.
 217   apply Zplus_z_OZ
 218 | apply symmetric_Ztimes
 219 | apply distributive_Ztimes_Zplus
 220 | intros.
 221   rewrite > (Ztimes_z_OZ a).
 222   reflexivity
 223 ]
 224 qed.
 225
 226 lemma Ztimes_sigma_pr: \forall z:Z.\forall n:nat.\forall p. \forall f.
 227 (sigma_p n p f) * z = sigma_p n p (\lambda i.(f i)*z).
 228 intros.
 229 rewrite < sym_Ztimes.
 230 rewrite > Ztimes_sigma_pl.
 231 apply eq_sigma_p
 232   [intros.reflexivity
 233   |intros.apply sym_Ztimes
 234   ]
 235 qed.