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