]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/library/nat/count.ma
() around tactic terms
[helm.git] / 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.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 ? ? ? (\lambda i.g (div i (S n)) (mod i (S n)))).
127 rewrite > eq_map_iter_i_sigma.
128 rewrite > eq_sigma_sigma1.
129 apply (trans_eq ? ?
130 (sigma n (\lambda a.
131   sigma m (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))) O) O)).
132 apply eq_sigma.intros.
133 apply eq_sigma.intros.
134 rewrite > (div_mod_spec_to_eq (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) ((i1*(S n) + i) \mod (S n)) i1 i).
135 rewrite > (div_mod_spec_to_eq2 (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) ((i1*(S n) + i) \mod (S n)) i1 i).
136 rewrite > H3.
137 apply bool_to_nat_andb.
138 simplify.apply le_S_S.assumption.
139 simplify.apply le_S_S.assumption.
140 apply div_mod_spec_div_mod.
141 simplify.apply le_S_S.apply le_O_n.
142 constructor 1.simplify.apply le_S_S.assumption.
143 reflexivity.
144 apply div_mod_spec_div_mod.
145 simplify.apply le_S_S.apply le_O_n.
146 constructor 1.simplify.apply le_S_S.assumption.
147 reflexivity.
148 apply (trans_eq ? ? 
149 (sigma n (\lambda n.((bool_to_nat (f1 n)) *
150 (sigma m (\lambda n.bool_to_nat (f2 n)) O))) O)).
151 apply eq_sigma.
152 intros.
153 rewrite > sym_times.
154 apply (trans_eq ? ? 
155 (sigma m (\lambda n.(bool_to_nat (f2 n))*(bool_to_nat (f1 i))) O)).
156 reflexivity.
157 apply sym_eq. apply sigma_times.
158 change in match (pred (S n)) with n.
159 change in match (pred (S m)) with m.
160 apply sym_eq. apply sigma_times.
161 unfold permut.
162 split.
163 intros.
164 rewrite < plus_n_O.
165 apply le_S_S_to_le.
166 rewrite < S_pred in \vdash (? ? %).
167 change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
168 apply H.
169 apply lt_mod_m_m.
170 simplify. apply le_S_S.apply le_O_n.
171 apply (lt_times_to_lt_l n).
172 apply (le_to_lt_to_lt ? i).
173 rewrite > (div_mod i (S n)) in \vdash (? ? %).
174 rewrite > sym_plus.
175 apply le_plus_n.
176 simplify. apply le_S_S.apply le_O_n.
177 unfold lt.
178 rewrite > S_pred in \vdash (? ? %).
179 apply le_S_S.
180 rewrite > plus_n_O in \vdash (? ? %).
181 rewrite > sym_times. assumption.
182 rewrite > (times_n_O O).
183 apply lt_times.
184 simplify. apply le_S_S.apply le_O_n.
185 simplify. apply le_S_S.apply le_O_n.
186 rewrite > (times_n_O O).
187 apply lt_times.
188 simplify. apply le_S_S.apply le_O_n.
189 simplify. apply le_S_S.apply le_O_n.
190 rewrite < plus_n_O.
191 unfold injn.
192 intros.
193 cut (i < (S n)*(S m)).
194 cut (j < (S n)*(S m)).
195 cut ((i \mod (S n)) < (S n)).
196 cut ((i/(S n)) < (S m)).
197 cut ((j \mod (S n)) < (S n)).
198 cut ((j/(S n)) < (S m)).
199 rewrite > (div_mod i (S n)).
200 rewrite > (div_mod j (S n)).
201 rewrite < (H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3).
202 rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
203 rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
204 rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
205 rewrite > H6.reflexivity.
206 simplify. apply le_S_S.apply le_O_n.
207 simplify. apply le_S_S.apply le_O_n.
208 apply (lt_times_to_lt_l n).
209 apply (le_to_lt_to_lt ? j).
210 rewrite > (div_mod j (S n)) in \vdash (? ? %).
211 rewrite > sym_plus.
212 apply le_plus_n.
213 simplify. apply le_S_S.apply le_O_n.
214 rewrite < sym_times. assumption.
215 apply lt_mod_m_m.
216 simplify. apply le_S_S.apply le_O_n.
217 apply (lt_times_to_lt_l n).
218 apply (le_to_lt_to_lt ? i).
219 rewrite > (div_mod i (S n)) in \vdash (? ? %).
220 rewrite > sym_plus.
221 apply le_plus_n.
222 simplify. apply le_S_S.apply le_O_n.
223 rewrite < sym_times. assumption.
224 apply lt_mod_m_m.
225 simplify. apply le_S_S.apply le_O_n.
226 unfold lt.
227 rewrite > S_pred in \vdash (? ? %).
228 apply le_S_S.assumption.
229 rewrite > (times_n_O O).
230 apply lt_times.
231 simplify. apply le_S_S.apply le_O_n.
232 simplify. apply le_S_S.apply le_O_n.
233 unfold lt.
234 rewrite > S_pred in \vdash (? ? %).
235 apply le_S_S.assumption.
236 rewrite > (times_n_O O).
237 apply lt_times.
238 simplify. apply le_S_S.apply le_O_n.
239 simplify. apply le_S_S.apply le_O_n.
240 intros.
241 apply False_ind.
242 apply (not_le_Sn_O m1 H4).
243 qed.