helm/matita/library/nat/count.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/count".
  16
  17 include "nat/relevant_equations.ma".
  18 include "nat/sigma_and_pi.ma".
  19 include "nat/permutation.ma".
  20
  21 theorem sigma_f_g : \forall n,m:nat.\forall f,g:nat \to nat.
  22 sigma n (\lambda p.f p + g p) m = sigma n f m + sigma n g m.
  23 intros.elim n.
  24 simplify.reflexivity.
  25 simplify.rewrite > H.
  26 rewrite > assoc_plus.
  27 rewrite < (assoc_plus (g (S (n1+m)))).
  28 rewrite > (sym_plus (g (S (n1+m)))).
  29 rewrite > (assoc_plus (sigma n1 f m)).
  30 rewrite < assoc_plus.
  31 reflexivity.
  32 qed.
  33
  34 theorem sigma_plus: \forall n,p,m:nat.\forall f:nat \to nat.
  35 sigma (S (p+n)) f m = sigma p (\lambda x.(f ((S n) + x))) m + sigma n f m.
  36 intros. elim p.
  37 simplify.
  38 rewrite < (sym_plus n m).reflexivity.
  39 simplify.
  40 rewrite > assoc_plus in \vdash (? ? ? %).
  41 rewrite < H.
  42 simplify.
  43 rewrite < plus_n_Sm.
  44 rewrite > (sym_plus n).
  45 rewrite > assoc_plus.
  46 rewrite < (sym_plus m).
  47 rewrite < (assoc_plus n1).
  48 reflexivity.
  49 qed.
  50
  51 theorem sigma_plus1: \forall n,p,m:nat.\forall f:nat \to nat.
  52 sigma (p+(S n)) f m = sigma p (\lambda x.(f ((S n) + x))) m + sigma n f m.
  53 intros. elim p.
  54 simplify.reflexivity.
  55 simplify.
  56 rewrite > assoc_plus in \vdash (? ? ? %).
  57 rewrite < H.
  58 rewrite < plus_n_Sm.
  59 rewrite < plus_n_Sm.simplify.
  60 rewrite < (sym_plus n).
  61 rewrite > assoc_plus.
  62 rewrite < (sym_plus m).
  63 rewrite < (assoc_plus n).
  64 reflexivity.
  65 qed.
  66
  67 theorem eq_sigma_sigma : \forall n,m:nat.\forall f:nat \to nat.
  68 sigma (pred ((S n)*(S m))) f O =
  69 sigma m (\lambda a.(sigma n (\lambda b.f (b*(S m) + a)) O)) O.
  70 intro.elim n.simplify.
  71 rewrite < plus_n_O.
  72 apply eq_sigma.intros.reflexivity.
  73 change with
  74 (sigma (m+(S n1)*(S m)) f O =
  75 sigma m (\lambda a.(f ((S(n1+O))*(S m)+a)) + (sigma n1 (\lambda b.f (b*(S m)+a)) O)) O).
  76 rewrite > sigma_f_g.
  77 rewrite < plus_n_O.
  78 rewrite < H.
  79 rewrite > (S_pred ((S n1)*(S m))).
  80 apply sigma_plus1.
  81 simplify.unfold lt.apply le_S_S.apply le_O_n.
  82 qed.
  83
  84 theorem eq_sigma_sigma1 : \forall n,m:nat.\forall f:nat \to nat.
  85 sigma (pred ((S n)*(S m))) f O =
  86 sigma n (\lambda a.(sigma m (\lambda b.f (b*(S n) + a)) O)) O.
  87 intros.
  88 rewrite > sym_times.
  89 apply eq_sigma_sigma.
  90 qed.
  91
  92 theorem sigma_times: \forall n,m,p:nat.\forall f:nat \to nat.
  93 (sigma n f m)*p = sigma n (\lambda i.(f i) * p) m.
  94 intro. elim n.simplify.reflexivity.
  95 simplify.rewrite < H.
  96 apply times_plus_l.
  97 qed.
  98
  99 definition bool_to_nat: bool \to nat \def
 100 \lambda b. match b with
 101 [ true \Rightarrow (S O)
 102 | false \Rightarrow O ].
 103
 104 theorem bool_to_nat_andb: \forall a,b:bool.
 105 bool_to_nat (andb a b) = (bool_to_nat a)*(bool_to_nat b).
 106 intros. elim a.elim b.
 107 simplify.reflexivity.
 108 reflexivity.
 109 reflexivity.
 110 qed.
 111
 112 definition count : nat \to (nat \to bool) \to nat \def
 113 \lambda n.\lambda f. sigma (pred n) (\lambda n.(bool_to_nat (f n))) O.
 114
 115 theorem count_times:\forall n,m:nat.
 116 \forall f,f1,f2:nat \to bool.
 117 \forall g:nat \to nat \to nat.
 118 \forall g1,g2: nat \to nat.
 119 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g b a) < (S n)*(S m)) \to
 120 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g1 (g b a)) = a) \to
 121 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g2 (g b a)) = b) \to
 122 (\forall a,b:nat. a < (S n) \to b < (S m) \to f (g b a) = andb (f2 b) (f1 a)) \to
 123 (count ((S n)*(S m)) f) = (count (S n) f1)*(count (S m) f2).
 124 intros.unfold count.
 125 rewrite < eq_map_iter_i_sigma.
 126 rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ?
 127            (\lambda i.g (div i (S n)) (mod i (S n)))).
 128 rewrite > eq_map_iter_i_sigma.
 129 rewrite > eq_sigma_sigma1.
 130 apply (trans_eq ? ?
 131 (sigma n (\lambda a.
 132   sigma m (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))) O) O)).
 133 apply eq_sigma.intros.
 134 apply eq_sigma.intros.
 135 rewrite > (div_mod_spec_to_eq (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n))
 136                                         ((i1*(S n) + i) \mod (S n)) i1 i).
 137 rewrite > (div_mod_spec_to_eq2 (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n))
 138                                         ((i1*(S n) + i) \mod (S n)) i1 i).
 139 rewrite > H3.
 140 apply bool_to_nat_andb.
 141 unfold lt.apply le_S_S.assumption.
 142 unfold lt.apply le_S_S.assumption.
 143 apply div_mod_spec_div_mod.
 144 unfold lt.apply le_S_S.apply le_O_n.
 145 constructor 1.unfold lt.apply le_S_S.assumption.
 146 reflexivity.
 147 apply div_mod_spec_div_mod.
 148 unfold lt.apply le_S_S.apply le_O_n.
 149 constructor 1.unfold lt.apply le_S_S.assumption.
 150 reflexivity.
 151 apply (trans_eq ? ?
 152 (sigma n (\lambda n.((bool_to_nat (f1 n)) *
 153 (sigma m (\lambda n.bool_to_nat (f2 n)) O))) O)).
 154 apply eq_sigma.
 155 intros.
 156 rewrite > sym_times.
 157 apply (trans_eq ? ?
 158 (sigma m (\lambda n.(bool_to_nat (f2 n))*(bool_to_nat (f1 i))) O)).
 159 reflexivity.
 160 apply sym_eq. apply sigma_times.
 161 change in match (pred (S n)) with n.
 162 change in match (pred (S m)) with m.
 163 apply sym_eq. apply sigma_times.
 164 unfold permut.
 165 split.
 166 intros.
 167 rewrite < plus_n_O.
 168 apply le_S_S_to_le.
 169 rewrite < S_pred in \vdash (? ? %).
 170 change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
 171 apply H.
 172 apply lt_mod_m_m.
 173 unfold lt. apply le_S_S.apply le_O_n.
 174 apply (lt_times_to_lt_l n).
 175 apply (le_to_lt_to_lt ? i).
 176 rewrite > (div_mod i (S n)) in \vdash (? ? %).
 177 rewrite > sym_plus.
 178 apply le_plus_n.
 179 unfold lt. apply le_S_S.apply le_O_n.
 180 unfold lt.
 181 rewrite > S_pred in \vdash (? ? %).
 182 apply le_S_S.
 183 rewrite > plus_n_O in \vdash (? ? %).
 184 rewrite > sym_times. assumption.
 185 rewrite > (times_n_O O).
 186 apply lt_times.
 187 unfold lt. apply le_S_S.apply le_O_n.
 188 unfold lt. apply le_S_S.apply le_O_n.
 189 rewrite > (times_n_O O).
 190 apply lt_times.
 191 unfold lt. apply le_S_S.apply le_O_n.
 192 unfold lt. apply le_S_S.apply le_O_n.
 193 rewrite < plus_n_O.
 194 unfold injn.
 195 intros.
 196 cut (i < (S n)*(S m)).
 197 cut (j < (S n)*(S m)).
 198 cut ((i \mod (S n)) < (S n)).
 199 cut ((i/(S n)) < (S m)).
 200 cut ((j \mod (S n)) < (S n)).
 201 cut ((j/(S n)) < (S m)).
 202 rewrite > (div_mod i (S n)).
 203 rewrite > (div_mod j (S n)).
 204 rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
 205 rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
 206 rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
 207 rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
 208 rewrite > H6.reflexivity.
 209 unfold lt. apply le_S_S.apply le_O_n.
 210 unfold lt. apply le_S_S.apply le_O_n.
 211 apply (lt_times_to_lt_l n).
 212 apply (le_to_lt_to_lt ? j).
 213 rewrite > (div_mod j (S n)) in \vdash (? ? %).
 214 rewrite > sym_plus.
 215 apply le_plus_n.
 216 unfold lt. apply le_S_S.apply le_O_n.
 217 rewrite < sym_times. assumption.
 218 apply lt_mod_m_m.
 219 unfold lt. apply le_S_S.apply le_O_n.
 220 apply (lt_times_to_lt_l n).
 221 apply (le_to_lt_to_lt ? i).
 222 rewrite > (div_mod i (S n)) in \vdash (? ? %).
 223 rewrite > sym_plus.
 224 apply le_plus_n.
 225 unfold lt. apply le_S_S.apply le_O_n.
 226 rewrite < sym_times. assumption.
 227 apply lt_mod_m_m.
 228 unfold lt. apply le_S_S.apply le_O_n.
 229 unfold lt.
 230 rewrite > S_pred in \vdash (? ? %).
 231 apply le_S_S.assumption.
 232 rewrite > (times_n_O O).
 233 apply lt_times.
 234 unfold lt. apply le_S_S.apply le_O_n.
 235 unfold lt. apply le_S_S.apply le_O_n.
 236 unfold lt.
 237 rewrite > S_pred in \vdash (? ? %).
 238 apply le_S_S.assumption.
 239 rewrite > (times_n_O O).
 240 apply lt_times.
 241 unfold lt. apply le_S_S.apply le_O_n.
 242 unfold lt. apply le_S_S.apply le_O_n.
 243 intros.
 244 apply False_ind.
 245 apply (not_le_Sn_O m1 H4).
 246 qed.