helm/software/matita/library/nat/iteration2.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/nat/iteration2.ma".
  16
  17 include "nat/primes.ma".
  18 include "nat/ord.ma".
  19 include "nat/generic_sigma_p.ma".
  20
  21
  22 (* sigma_p on nautral numbers is a specialization of sigma_p_gen *)
  23 definition sigma_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def
  24 \lambda n, p, g. (sigma_p_gen n p nat g O plus).
  25
  26 theorem symmetricIntPlus: symmetric nat plus.
  27 change with (\forall a,b:nat. (plus a b) = (plus b a)).
  28 intros.
  29 rewrite > sym_plus.
  30 reflexivity.
  31 qed.
  32
  33 (*the following theorems on sigma_p in N are obtained by the more general ones
  34  * in sigma_p_gen.ma
  35  *)
  36 theorem true_to_sigma_p_Sn:
  37 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
  38 p n = true \to sigma_p (S n) p g =
  39 (g n)+(sigma_p n p g).
  40 intros.
  41 unfold sigma_p.
  42 apply true_to_sigma_p_Sn_gen.
  43 assumption.
  44 qed.
  45
  46 theorem false_to_sigma_p_Sn:
  47 \forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
  48 p n = false \to sigma_p (S n) p g = sigma_p n p g.
  49 intros.
  50 unfold sigma_p.
  51 apply false_to_sigma_p_Sn_gen.
  52 assumption.
  53
  54 qed.
  55
  56 theorem eq_sigma_p: \forall p1,p2:nat \to bool.
  57 \forall g1,g2: nat \to nat.\forall n.
  58 (\forall x.  x < n \to p1 x = p2 x) \to
  59 (\forall x.  x < n \to g1 x = g2 x) \to
  60 sigma_p n p1 g1 = sigma_p n p2 g2.
  61 intros.
  62 unfold sigma_p.
  63 apply eq_sigma_p_gen;
  64   assumption.
  65 qed.
  66
  67 theorem eq_sigma_p1: \forall p1,p2:nat \to bool.
  68 \forall g1,g2: nat \to nat.\forall n.
  69 (\forall x.  x < n \to p1 x = p2 x) \to
  70 (\forall x.  x < n \to p1 x = true \to g1 x = g2 x) \to
  71 sigma_p n p1 g1 = sigma_p n p2 g2.
  72 intros.
  73 unfold sigma_p.
  74 apply eq_sigma_p1_gen;
  75   assumption.
  76 qed.
  77
  78 theorem sigma_p_false:
  79 \forall g: nat \to nat.\forall n.sigma_p n (\lambda x.false) g = O.
  80 intros.
  81 unfold sigma_p.
  82 apply sigma_p_false_gen.
  83 qed.
  84
  85 theorem sigma_p_plus: \forall n,k:nat.\forall p:nat \to bool.
  86 \forall g: nat \to nat.
  87 sigma_p (k+n) p g
  88 = sigma_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) + sigma_p n p g.
  89 intros.
  90 unfold sigma_p.
  91 apply (sigma_p_plusA_gen nat n k p g O plus)
  92 [ apply symmetricIntPlus.
  93 | intros.
  94   apply sym_eq.
  95   apply plus_n_O
  96 | apply associative_plus
  97 ]
  98 qed.
  99
 100 theorem false_to_eq_sigma_p: \forall n,m:nat.n \le m \to
 101 \forall p:nat \to bool.
 102 \forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to
 103 p i = false) \to sigma_p m p g = sigma_p n p g.
 104 intros.
 105 unfold sigma_p.
 106 apply (false_to_eq_sigma_p_gen);
 107   assumption.
 108 qed.
 109
 110 theorem sigma_p2 :
 111 \forall n,m:nat.
 112 \forall p1,p2:nat \to bool.
 113 \forall g: nat \to nat \to nat.
 114 sigma_p (n*m)
 115   (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
 116   (\lambda x.g (div x m) (mod x m)) =
 117 sigma_p n p1
 118   (\lambda x.sigma_p m p2 (g x)).
 119 intros.
 120 unfold sigma_p.
 121 apply (sigma_p2_gen n m p1 p2 nat g O plus)
 122 [ apply symmetricIntPlus
 123 | apply associative_plus
 124 | intros.
 125   apply sym_eq.
 126   apply plus_n_O
 127 ]
 128 qed.
 129
 130 theorem sigma_p2' :
 131 \forall n,m:nat.
 132 \forall p1:nat \to bool.
 133 \forall p2:nat \to nat \to bool.
 134 \forall g: nat \to nat \to nat.
 135 sigma_p (n*m)
 136   (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x m)))
 137   (\lambda x.g (div x m) (mod x m)) =
 138 sigma_p n p1
 139   (\lambda x.sigma_p m (p2 x) (g x)).
 140 intros.
 141 unfold sigma_p.
 142 apply (sigma_p2_gen' n m p1 p2 nat g O plus)
 143 [ apply symmetricIntPlus
 144 | apply associative_plus
 145 | intros.
 146   apply sym_eq.
 147   apply plus_n_O
 148 ]
 149 qed.
 150
 151 lemma sigma_p_gi: \forall g: nat \to nat.
 152 \forall n,i.\forall p:nat \to bool.i < n \to p i = true \to
 153 sigma_p n p g = g i + sigma_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
 154 intros.
 155 unfold sigma_p.
 156 apply (sigma_p_gi_gen)
 157 [ apply symmetricIntPlus
 158 | apply associative_plus
 159 | intros.
 160   apply sym_eq.
 161   apply plus_n_O
 162 | assumption
 163 | assumption
 164 ]
 165 qed.
 166
 167 theorem eq_sigma_p_gh:
 168 \forall g,h,h1: nat \to nat.\forall n,n1.
 169 \forall p1,p2:nat \to bool.
 170 (\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
 171 (\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
 172 (\forall i. i < n \to p1 i = true \to h i < n1) \to
 173 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
 174 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
 175 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
 176 sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 (\lambda x.p2 x) g.
 177 intros.
 178 unfold sigma_p.
 179 apply (eq_sigma_p_gh_gen nat O plus ? ? ? g h h1 n n1 p1 p2)
 180 [ apply symmetricIntPlus
 181 | apply associative_plus
 182 | intros.
 183   apply sym_eq.
 184   apply plus_n_O
 185 | assumption
 186 | assumption
 187 | assumption
 188 | assumption
 189 | assumption
 190 | assumption
 191 ]
 192 qed.
 193
 194
 195 theorem sigma_p_divides:
 196 \forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
 197 \forall g: nat \to nat.
 198 sigma_p (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) g =
 199 sigma_p (S n) (\lambda x.divides_b x n)
 200   (\lambda x.sigma_p (S m) (\lambda y.true) (\lambda y.g (x*(exp p y)))).
 201 intros.
 202 unfold sigma_p.
 203 apply (sigma_p_divides_gen nat O plus n m p ? ? ? g)
 204 [ assumption
 205 | assumption
 206 | assumption
 207 | apply symmetricIntPlus
 208 | apply associative_plus
 209 | intros.
 210   apply sym_eq.
 211   apply plus_n_O
 212 ]
 213 qed.
 214
 215 theorem distributive_times_plus_sigma_p: \forall n,k:nat. \forall p:nat \to bool. \forall g:nat \to nat.
 216 k*(sigma_p n p g) = sigma_p n p (\lambda i:nat.k * (g i)).
 217 intros.
 218 apply (distributive_times_plus_sigma_p_generic nat plus O times n k p g)
 219 [ apply symmetricIntPlus
 220 | apply associative_plus
 221 | intros.
 222   apply sym_eq.
 223   apply plus_n_O
 224 | apply symmetric_times
 225 | apply distributive_times_plus
 226 | intros.
 227   rewrite < (times_n_O a).
 228   reflexivity
 229 ]
 230 qed.
 231