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.