matita/contribs/library_auto/auto/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/library_autobatch/nat/count".
  16
  17 include "auto/nat/relevant_equations.ma".
  18 include "auto/nat/sigma_and_pi.ma".
  19 include "auto/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.
  24 elim n;simplify
  25 [ reflexivity
  26 | rewrite > H.
  27   autobatch
  28   (*rewrite > assoc_plus.
  29   rewrite < (assoc_plus (g (S (n1+m)))).
  30   rewrite > (sym_plus (g (S (n1+m)))).
  31   rewrite > (assoc_plus (sigma n1 f m)).
  32   rewrite < assoc_plus.
  33   reflexivity*)
  34 ]
  35 qed.
  36
  37 theorem sigma_plus: \forall n,p,m:nat.\forall f:nat \to nat.
  38 sigma (S (p+n)) f m = sigma p (\lambda x.(f ((S n) + x))) m + sigma n f m.
  39 intros.
  40 elim p;simplify
  41 [ autobatch
  42   (*rewrite < (sym_plus n m).
  43   reflexivity*)
  44 | rewrite > assoc_plus in \vdash (? ? ? %).
  45   rewrite < H.
  46   autobatch
  47   (*simplify.
  48   rewrite < plus_n_Sm.
  49   rewrite > (sym_plus n).
  50   rewrite > assoc_plus.
  51   rewrite < (sym_plus m).
  52   rewrite < (assoc_plus n1).
  53   reflexivity*)
  54 ]
  55 qed.
  56
  57 theorem sigma_plus1: \forall n,p,m:nat.\forall f:nat \to nat.
  58 sigma (p+(S n)) f m = sigma p (\lambda x.(f ((S n) + x))) m + sigma n f m.
  59 intros.
  60 elim p;simplify
  61 [ reflexivity
  62 | rewrite > assoc_plus in \vdash (? ? ? %).
  63   rewrite < H.
  64   rewrite < plus_n_Sm.
  65   autobatch
  66   (*rewrite < plus_n_Sm.simplify.
  67   rewrite < (sym_plus n).
  68   rewrite > assoc_plus.
  69   rewrite < (sym_plus m).
  70   rewrite < (assoc_plus n).
  71   reflexivity*)
  72 ]
  73 qed.
  74
  75 theorem eq_sigma_sigma : \forall n,m:nat.\forall f:nat \to nat.
  76 sigma (pred ((S n)*(S m))) f O =
  77 sigma m (\lambda a.(sigma n (\lambda b.f (b*(S m) + a)) O)) O.
  78 intro.
  79 elim n;simplify
  80 [ rewrite < plus_n_O.
  81   apply eq_sigma.
  82   intros.
  83   reflexivity
  84 | rewrite > sigma_f_g.
  85   rewrite < plus_n_O.
  86   rewrite < H.
  87   autobatch
  88
  89   (*rewrite > (S_pred ((S n1)*(S m)))
  90   [ apply sigma_plus1
  91   | simplify.
  92     unfold lt.
  93     apply le_S_S.
  94     apply le_O_n
  95   ]*)
  96 ]
  97 qed.
  98
  99 theorem eq_sigma_sigma1 : \forall n,m:nat.\forall f:nat \to nat.
 100 sigma (pred ((S n)*(S m))) f O =
 101 sigma n (\lambda a.(sigma m (\lambda b.f (b*(S n) + a)) O)) O.
 102 intros.
 103 rewrite > sym_times.
 104 apply eq_sigma_sigma.
 105 qed.
 106
 107 theorem sigma_times: \forall n,m,p:nat.\forall f:nat \to nat.
 108 (sigma n f m)*p = sigma n (\lambda i.(f i) * p) m.
 109 intro.
 110 elim n;simplify
 111 [ reflexivity
 112 | rewrite < H.
 113   apply times_plus_l
 114 ]
 115 qed.
 116
 117 definition bool_to_nat: bool \to nat \def
 118 \lambda b. match b with
 119 [ true \Rightarrow (S O)
 120 | false \Rightarrow O ].
 121
 122 theorem bool_to_nat_andb: \forall a,b:bool.
 123 bool_to_nat (andb a b) = (bool_to_nat a)*(bool_to_nat b).
 124 intros.
 125 elim a;autobatch.
 126 (*[elim b
 127   [ simplify.
 128     reflexivity
 129   | reflexivity
 130   ]
 131 | reflexivity
 132 ]*)
 133 qed.
 134
 135 definition count : nat \to (nat \to bool) \to nat \def
 136 \lambda n.\lambda f. sigma (pred n) (\lambda n.(bool_to_nat (f n))) O.
 137
 138 theorem count_times:\forall n,m:nat.
 139 \forall f,f1,f2:nat \to bool.
 140 \forall g:nat \to nat \to nat.
 141 \forall g1,g2: nat \to nat.
 142 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g b a) < (S n)*(S m)) \to
 143 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g1 (g b a)) = a) \to
 144 (\forall a,b:nat. a < (S n) \to b < (S m) \to (g2 (g b a)) = b) \to
 145 (\forall a,b:nat. a < (S n) \to b < (S m) \to f (g b a) = andb (f2 b) (f1 a)) \to
 146 (count ((S n)*(S m)) f) = (count (S n) f1)*(count (S m) f2).
 147 intros.unfold count.
 148 rewrite < eq_map_iter_i_sigma.
 149 rewrite > (permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ?
 150            (\lambda i.g (div i (S n)) (mod i (S n))))
 151 [ rewrite > eq_map_iter_i_sigma.
 152   rewrite > eq_sigma_sigma1.
 153   apply (trans_eq ? ?
 154   (sigma n (\lambda a.
 155     sigma m (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))) O) O))
 156   [ apply eq_sigma.intros.
 157     apply eq_sigma.intros.
 158     rewrite > (div_mod_spec_to_eq (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n))
 159                                           ((i1*(S n) + i) \mod (S n)) i1 i)
 160     [ rewrite > (div_mod_spec_to_eq2 (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n))
 161                                            ((i1*(S n) + i) \mod (S n)) i1 i)
 162       [ rewrite > H3;autobatch (*qui autobatch impiega parecchio tempo*)
 163         (*[ apply bool_to_nat_andb
 164         | unfold lt.
 165           apply le_S_S.
 166           assumption
 167         | unfold lt.
 168           apply le_S_S.
 169           assumption
 170         ]*)
 171       | autobatch
 172         (*apply div_mod_spec_div_mod.
 173         unfold lt.
 174         apply le_S_S.
 175         apply le_O_n*)
 176       | constructor 1;autobatch
 177         (*[ unfold lt.
 178           apply le_S_S.
 179           assumption
 180         | reflexivity
 181         ]*)
 182       ]
 183     | autobatch
 184       (*apply div_mod_spec_div_mod.
 185       unfold lt.
 186       apply le_S_S.
 187       apply le_O_n*)
 188     | constructor 1;autobatch
 189       (*[ unfold lt.
 190         apply le_S_S.
 191         assumption
 192       | reflexivity
 193       ]*)
 194     ]
 195   | apply (trans_eq ? ?
 196     (sigma n (\lambda n.((bool_to_nat (f1 n)) *
 197     (sigma m (\lambda n.bool_to_nat (f2 n)) O))) O))
 198     [ apply eq_sigma.
 199       intros.
 200       autobatch
 201       (*rewrite > sym_times.
 202       apply (trans_eq ? ?
 203       (sigma m (\lambda n.(bool_to_nat (f2 n))*(bool_to_nat (f1 i))) O))
 204       [ reflexivity.
 205       | apply sym_eq.
 206         apply sigma_times
 207       ]*)
 208     | autobatch
 209       (*simplify.
 210       apply sym_eq.
 211       apply sigma_times*)
 212     ]
 213   ]
 214 | unfold permut.
 215   split
 216   [ intros.
 217     rewrite < plus_n_O.
 218     apply le_S_S_to_le.
 219     rewrite < S_pred in \vdash (? ? %)
 220     [ change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
 221       apply H
 222       [ autobatch
 223         (*apply lt_mod_m_m.
 224         unfold lt.
 225         apply le_S_S.
 226         apply le_O_n*)
 227       | apply (lt_times_to_lt_l n).
 228         apply (le_to_lt_to_lt ? i)
 229         [ autobatch
 230           (*rewrite > (div_mod i (S n)) in \vdash (? ? %)
 231           [ rewrite > sym_plus.
 232             apply le_plus_n
 233           | unfold lt.
 234             apply le_S_S.
 235             apply le_O_n
 236           ]*)
 237         | unfold lt.
 238           rewrite > S_pred in \vdash (? ? %)
 239           [ apply le_S_S.
 240             autobatch
 241             (*rewrite > plus_n_O in \vdash (? ? %).
 242             rewrite > sym_times.
 243             assumption*)
 244           | autobatch
 245             (*rewrite > (times_n_O O).
 246             apply lt_times;
 247             unfold lt;apply le_S_S;apply le_O_n*)
 248           ]
 249         ]
 250       ]
 251     | autobatch
 252       (*rewrite > (times_n_O O).
 253       apply lt_times;
 254       unfold lt;apply le_S_S;apply le_O_n *)
 255     ]
 256   | rewrite < plus_n_O.
 257     unfold injn.
 258     intros.
 259     cut (i < (S n)*(S m))
 260     [ cut (j < (S n)*(S m))
 261       [ cut ((i \mod (S n)) < (S n))
 262         [ cut ((i/(S n)) < (S m))
 263           [ cut ((j \mod (S n)) < (S n))
 264             [ cut ((j/(S n)) < (S m))
 265               [ rewrite > (div_mod i (S n))
 266                 [ rewrite > (div_mod j (S n))
 267                   [ rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
 268                     rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
 269                     rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
 270                     rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
 271                     autobatch
 272                     (*rewrite > H6.
 273                     reflexivity*)
 274                   | autobatch
 275                     (*unfold lt.
 276                     apply le_S_S.
 277                     apply le_O_n*)
 278                   ]
 279                 | autobatch
 280                   (*unfold lt.
 281                   apply le_S_S.
 282                   apply le_O_n*)
 283                 ]
 284               | apply (lt_times_to_lt_l n).
 285                 apply (le_to_lt_to_lt ? j)
 286                 [ autobatch.
 287                   (*rewrite > (div_mod j (S n)) in \vdash (? ? %)
 288                   [ rewrite > sym_plus.
 289                     apply le_plus_n
 290                   | unfold lt.
 291                     apply le_S_S.
 292                     apply le_O_n
 293                   ]*)
 294                 | rewrite < sym_times.
 295                   assumption
 296                 ]
 297               ]
 298             | autobatch
 299               (*apply lt_mod_m_m.
 300               unfold lt. apply le_S_S.
 301               apply le_O_n*)
 302             ]
 303           | apply (lt_times_to_lt_l n).
 304             apply (le_to_lt_to_lt ? i)
 305             [ autobatch
 306               (*rewrite > (div_mod i (S n)) in \vdash (? ? %)
 307               [ rewrite > sym_plus.
 308                 apply le_plus_n
 309               | unfold lt.
 310                 apply le_S_S.
 311                 apply le_O_n
 312               ]*)
 313             | rewrite < sym_times.
 314               assumption
 315             ]
 316           ]
 317         | autobatch
 318           (*apply lt_mod_m_m.
 319           unfold lt. apply le_S_S.
 320           apply le_O_n*)
 321         ]
 322       | unfold lt.
 323         autobatch
 324         (*rewrite > S_pred in \vdash (? ? %)
 325         [ apply le_S_S.
 326           assumption
 327         | rewrite > (times_n_O O).
 328           apply lt_times;
 329             unfold lt; apply le_S_S;apply le_O_n
 330         ]*)
 331       ]
 332     | unfold lt.
 333       autobatch
 334       (*rewrite > S_pred in \vdash (? ? %)
 335       [ apply le_S_S.
 336         assumption
 337       | rewrite > (times_n_O O).
 338         apply lt_times;
 339           unfold lt; apply le_S_S;apply le_O_n
 340       ]*)
 341     ]
 342   ]
 343 | intros.
 344   apply False_ind.
 345   apply (not_le_Sn_O m1 H4)
 346 ]
 347 qed.