1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/library_autobatch/nat/count".
17 include "auto/nat/relevant_equations.ma".
18 include "auto/nat/sigma_and_pi.ma".
19 include "auto/nat/permutation.ma".
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.
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)).
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.
42 (*rewrite < (sym_plus n m).
44 | rewrite > assoc_plus in \vdash (? ? ? %).
49 rewrite > (sym_plus n).
51 rewrite < (sym_plus m).
52 rewrite < (assoc_plus n1).
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.
62 | rewrite > assoc_plus in \vdash (? ? ? %).
66 (*rewrite < plus_n_Sm.simplify.
67 rewrite < (sym_plus n).
69 rewrite < (sym_plus m).
70 rewrite < (assoc_plus n).
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.
84 | rewrite > sigma_f_g.
89 (*rewrite > (S_pred ((S n1)*(S m)))
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.
104 apply eq_sigma_sigma.
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.
117 definition bool_to_nat: bool \to nat \def
118 \lambda b. match b with
119 [ true \Rightarrow (S O)
120 | false \Rightarrow O ].
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).
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.
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).
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.
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
172 (*apply div_mod_spec_div_mod.
176 | constructor 1;autobatch
184 (*apply div_mod_spec_div_mod.
188 | constructor 1;autobatch
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))
201 (*rewrite > sym_times.
203 (sigma m (\lambda n.(bool_to_nat (f2 n))*(bool_to_nat (f1 i))) O))
219 rewrite < S_pred in \vdash (? ? %)
220 [ change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
227 | apply (lt_times_to_lt_l n).
228 apply (le_to_lt_to_lt ? i)
230 (*rewrite > (div_mod i (S n)) in \vdash (? ? %)
231 [ rewrite > sym_plus.
238 rewrite > S_pred in \vdash (? ? %)
241 (*rewrite > plus_n_O in \vdash (? ? %).
245 (*rewrite > (times_n_O O).
247 unfold lt;apply le_S_S;apply le_O_n*)
252 (*rewrite > (times_n_O O).
254 unfold lt;apply le_S_S;apply le_O_n *)
256 | rewrite < plus_n_O.
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 (? ? ? (? % ?)).
284 | apply (lt_times_to_lt_l n).
285 apply (le_to_lt_to_lt ? j)
287 (*rewrite > (div_mod j (S n)) in \vdash (? ? %)
288 [ rewrite > sym_plus.
294 | rewrite < sym_times.
300 unfold lt. apply le_S_S.
303 | apply (lt_times_to_lt_l n).
304 apply (le_to_lt_to_lt ? i)
306 (*rewrite > (div_mod i (S n)) in \vdash (? ? %)
307 [ rewrite > sym_plus.
313 | rewrite < sym_times.
319 unfold lt. apply le_S_S.
324 (*rewrite > S_pred in \vdash (? ? %)
327 | rewrite > (times_n_O O).
329 unfold lt; apply le_S_S;apply le_O_n
334 (*rewrite > S_pred in \vdash (? ? %)
337 | rewrite > (times_n_O O).
339 unfold lt; apply le_S_S;apply le_O_n
345 apply (not_le_Sn_O m1 H4)