1 | include "basics/lists/list.ma". |
---|
2 | include "ASM/Util.ma". (* coercion from bool to Prop *) |
---|
3 | |
---|
4 | lemma All_map : ∀A,B,P,Q,f,l. |
---|
5 | All A P l → |
---|
6 | (∀a.P a → Q (f a)) → |
---|
7 | All B Q (map A B f l). |
---|
8 | #A #B #P #Q #f #l elim l // |
---|
9 | #h #t #IH * #Ph #Pt #F % [@(F ? Ph) | @(IH Pt F)] qed. |
---|
10 | |
---|
11 | lemma Exists_map : ∀A,B,P,Q,f,l. |
---|
12 | Exists A P l → |
---|
13 | (∀a.P a → Q (f a)) → |
---|
14 | Exists B Q (map A B f l). |
---|
15 | #A #B #P #Q #f #l elim l // |
---|
16 | #h #t #IH * #H #F |
---|
17 | [ %1 @(F ? H) | %2 @(IH H F) ] |
---|
18 | qed. |
---|
19 | |
---|
20 | lemma All_append : ∀A,P,l,r. All A P l → All A P r → All A P (l@r). |
---|
21 | #A #P #l elim l |
---|
22 | [ // |
---|
23 | | #hd #tl #IH #r * #H1 #H2 #H3 % // @IH // |
---|
24 | ] qed. |
---|
25 | |
---|
26 | lemma All_append_l : ∀A,P,l,r. All A P (l@r) → All A P l. |
---|
27 | #A #P #l elim l |
---|
28 | [ // |
---|
29 | | #hd #tl #IH #r * #H1 #H2 % /2/ |
---|
30 | ] qed. |
---|
31 | |
---|
32 | lemma All_append_r : ∀A,P,l,r. All A P (l@r) → All A P r. |
---|
33 | #A #P #l elim l |
---|
34 | [ // |
---|
35 | | #h #t #IH #r * /2/ |
---|
36 | ] qed. |
---|
37 | |
---|
38 | (* An alternative form of All that can be easier to use sometimes. *) |
---|
39 | lemma All_alt : ∀A,P,l. |
---|
40 | (∀a,pre,post. l = pre@a::post → P a) → |
---|
41 | All A P l. |
---|
42 | #A #P #l #H lapply (refl ? l) change with ([ ] @ l) in ⊢ (???% → ?); |
---|
43 | generalize in ⊢ (???(??%?) → ?); elim l in ⊢ (? → ???(???%) → %); |
---|
44 | [ #pre #E % |
---|
45 | | #a #tl #IH #pre #E % |
---|
46 | [ @(H a pre tl E) |
---|
47 | | @(IH (pre@[a])) >associative_append @E |
---|
48 | ] |
---|
49 | ] qed. |
---|
50 | |
---|
51 | lemma All_split : ∀A,P,l. All A P l → ∀pre,x,post.l = pre @ x :: post → P x. |
---|
52 | #A #P #l elim l |
---|
53 | [ * * normalize [2: #y #pre'] #x #post #ABS destruct(ABS) |
---|
54 | | #hd #tl #IH * #Phd #Ptl * normalize [2: #y #pre'] #x #post #EQ destruct(EQ) |
---|
55 | [ @(IH Ptl … (refl …)) |
---|
56 | | @Phd |
---|
57 | ] |
---|
58 | ] |
---|
59 | qed. |
---|
60 | |
---|
61 | let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝ |
---|
62 | match la with |
---|
63 | [ nil ⇒ match lb with [ nil ⇒ True | _ ⇒ False ] |
---|
64 | | cons ha ta ⇒ |
---|
65 | match lb with [ nil ⇒ False | cons hb tb ⇒ P ha hb ∧ All2 A B P ta tb ] |
---|
66 | ]. |
---|
67 | |
---|
68 | lemma All2_length : ∀A,B,P,la,lb. All2 A B P la lb → |la| = |lb|. |
---|
69 | #A #B #P #la elim la |
---|
70 | [ * [ // | #x #y * ] |
---|
71 | | #ha #ta #IH * [ * | #hb #tb * #H1 #H2 whd in ⊢ (??%%); >(IH … H2) @refl |
---|
72 | ] qed. |
---|
73 | |
---|
74 | lemma All2_mp : ∀A,B,P,Q,la,lb. (∀a,b. P a b → Q a b) → All2 A B P la lb → All2 A B Q la lb. |
---|
75 | #A #B #P #Q #la elim la |
---|
76 | [ * [ // | #h #t #_ * ] |
---|
77 | | #ha #ta #IH * [ // | #hb #tb #H * #H1 #H2 % [ @H @H1 | @(IH … H2) @H ] ] |
---|
78 | ] qed. |
---|
79 | |
---|
80 | let rec map_All (A,B:Type[0]) (P:A → Prop) (f:∀a. P a → B) (l:list A) (H:All A P l) on l : list B ≝ |
---|
81 | match l return λl. All A P l → ? with |
---|
82 | [ nil ⇒ λ_. nil B |
---|
83 | | cons hd tl ⇒ λH. cons B (f hd (proj1 … H)) (map_All A B P f tl (proj2 … H)) |
---|
84 | ] H. |
---|
85 | |
---|
86 | lemma All_rev : ∀A,P,l.All A P l → All A P (rev ? l). |
---|
87 | #A#P#l elim l // |
---|
88 | #h #t #Hi * #Ph #Pt normalize |
---|
89 | >rev_append_def |
---|
90 | @All_append |
---|
91 | [ @(Hi Pt) |
---|
92 | | %{Ph I} |
---|
93 | ] |
---|
94 | qed. |
---|
95 | |
---|
96 | lemma Exists_rev : ∀A,P,l.Exists A P l → Exists A P (rev ? l). |
---|
97 | #A#P#l elim l // |
---|
98 | #h #t #Hi normalize >rev_append_def |
---|
99 | * [ #Ph @Exists_append_r %{Ph} | #Pt @Exists_append_l @(Hi Pt)] |
---|
100 | qed. |
---|
101 | |
---|
102 | include "utilities/option.ma". |
---|
103 | |
---|
104 | lemma find_All : ∀A,B.∀P : A → Prop.∀Q : B → Prop.∀f.(∀x.P x → opt_All ? Q (f x)) → |
---|
105 | ∀l. All ? P l → opt_All ? Q (find … f l). |
---|
106 | #A#B#P#Q#f#H#l elim l [#_%] |
---|
107 | #x #l' #Hi |
---|
108 | * #Px #AllPl' |
---|
109 | whd in ⊢ (???%); |
---|
110 | lapply (H x Px) |
---|
111 | lapply (refl ? (f x)) |
---|
112 | generalize in ⊢ (???%→?); #o elim o [2: #b] #fx_eq >fx_eq [//] |
---|
113 | #_ whd in ⊢ (???%); @(Hi AllPl') |
---|
114 | qed. |
---|
115 | |
---|
116 | include "utilities/monad.ma". |
---|
117 | |
---|
118 | definition Append : ∀A.Aop ? (nil A) ≝ λA.mk_Aop ? ? (append ?) ? ? ?. |
---|
119 | // qed. |
---|
120 | |
---|
121 | definition List ≝ MakeMonadProps |
---|
122 | list |
---|
123 | (λX,x.[x]) |
---|
124 | (λX,Y,l,f.foldr … (λx.append ? (f x)) [ ] l) |
---|
125 | ????. normalize |
---|
126 | [ / by / |
---|
127 | | #X#m elim m normalize // |
---|
128 | | #X#Y#Z #m #f#g |
---|
129 | elim m normalize [//] |
---|
130 | #x#l' #Hi elim (f x) |
---|
131 | [@Hi] normalize #hd #tl #IH >associative_append >IH % |
---|
132 | |#X#Y#m #f #g #H elim m normalize [//] |
---|
133 | #hd #tl #IH >H >IH % |
---|
134 | ] qed. |
---|
135 | |
---|
136 | unification hint 0 ≔ X ; |
---|
137 | N ≟ max_def List |
---|
138 | (*---------------------------*)⊢ |
---|
139 | list X ≡ monad N X. |
---|
140 | |
---|
141 | definition In ≝ λA.λl : list A.λx : A.Exists A (eq ? x) l. |
---|
142 | |
---|
143 | lemma All_In : ∀A,P,l,x. All A P l → In A l x → P x. |
---|
144 | #A#P#l#x #Pl #xl elim (Exists_All … xl Pl) |
---|
145 | #x' * #EQx' >EQx' // |
---|
146 | qed. |
---|
147 | |
---|
148 | lemma In_All : ∀A,P,l.(∀x.In A l x → P x) → All A P l. |
---|
149 | #A#P#l elim l |
---|
150 | [#_ % |
---|
151 | |#x #l' #IH #H % |
---|
152 | [ @H % % |
---|
153 | | @IH #y #G @H %2 @G |
---|
154 | ] |
---|
155 | ] |
---|
156 | qed. |
---|
157 | |
---|
158 | |
---|
159 | lemma nth_opt_append_l : ∀A,l1,l2,n.|l1| > n → nth_opt A n (l1 @ l2) = nth_opt A n l1. |
---|
160 | #A#l1 elim l1 normalize |
---|
161 | [ #l2 #n #ABS elim (absurd ? ABS ?) // |
---|
162 | | #x #l' #IH #l2 #n cases n normalize |
---|
163 | [// |
---|
164 | | #n #H @IH @le_S_S_to_le assumption |
---|
165 | ] |
---|
166 | ] |
---|
167 | qed. |
---|
168 | |
---|
169 | lemma nth_opt_append_r : ∀A,l1,l2,n.|l1| ≤ n → nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2. |
---|
170 | #A#l1 elim l1 |
---|
171 | [#l2 #n #_ <minus_n_O % |
---|
172 | |#x #l' #IH #l2 #n normalize in match (|?|); whd in match (nth_opt ???); |
---|
173 | cases n -n |
---|
174 | [ #ABS elim (absurd ? ABS ?) // |
---|
175 | | #n #H whd in ⊢ (??%?); >minus_S_S @IH @le_S_S_to_le assumption |
---|
176 | ] |
---|
177 | ] |
---|
178 | qed. |
---|
179 | |
---|
180 | lemma nth_opt_append_hit_l : ∀A,l1,l2,n,x. nth_opt A n l1 = Some ? x → |
---|
181 | nth_opt A n (l1 @ l2) = Some ? x. |
---|
182 | #A #l1 elim l1 normalize |
---|
183 | [ #l2 #n #x #ABS destruct |
---|
184 | | #hd #tl #IH #l2 * [2: #n] #x normalize /2 by / |
---|
185 | ] |
---|
186 | qed. |
---|
187 | |
---|
188 | lemma nth_opt_append_miss_l : ∀A,l1,l2,n. nth_opt A n l1 = None ? → |
---|
189 | nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2. |
---|
190 | #A #l1 elim l1 normalize |
---|
191 | [ #l2 #n #_ <minus_n_O % |
---|
192 | | #hd #tl #IH #l2 * [2: #n] normalize |
---|
193 | [ @IH |
---|
194 | | #ABS destruct(ABS) |
---|
195 | ] |
---|
196 | ] |
---|
197 | qed. |
---|
198 | |
---|
199 | |
---|
200 | (* count occurrences satisfying a test *) |
---|
201 | let rec count A (f : A → bool) (l : list A) on l : ℕ ≝ |
---|
202 | match l with |
---|
203 | [ nil ⇒ 0 |
---|
204 | | cons x l' ⇒ (if f x then 1 else 0) + count A f l' |
---|
205 | ]. |
---|
206 | |
---|
207 | theorem count_append : ∀A,f,l1,l2.count A f (l1@l2) = count A f l1 + count A f l2. |
---|
208 | #A #f #l1 elim l1 |
---|
209 | [ #l2 % |
---|
210 | | #hd #tl #IH #l2 normalize elim (f hd) normalize >IH % |
---|
211 | ] |
---|
212 | qed. |
---|
213 | |
---|
214 | |
---|
215 | include "utilities/option.ma". |
---|
216 | |
---|
217 | lemma position_of_from_aux : ∀A,test,l,n. |
---|
218 | position_of_aux A test l n = !n' ← position_of A test l; return n + n'. |
---|
219 | #A #test #l elim l |
---|
220 | [ normalize #_ % |
---|
221 | | #hd #tl #IH #n |
---|
222 | normalize in ⊢ (??%?); >IH |
---|
223 | normalize elim (test hd) normalize |
---|
224 | [ <plus_n_O % |
---|
225 | | >(IH 1) whd in match (position_of ???); |
---|
226 | elim (position_of_aux ??? 0) normalize |
---|
227 | [ % | #x <plus_n_Sm % ] |
---|
228 | ] |
---|
229 | ] |
---|
230 | qed. |
---|
231 | |
---|
232 | definition position_of_safe ≝ λA,test,l.λprf : count A test l ≥ 1. |
---|
233 | opt_safe ? (position_of A test l) ?. |
---|
234 | lapply prf -prf elim l normalize |
---|
235 | [ #ABS elim (absurd ? ABS (not_le_Sn_O 0)) |
---|
236 | |#hd #tl #IH elim (test hd) normalize |
---|
237 | [2: >position_of_from_aux #H |
---|
238 | change with (position_of_aux ????) in match (position_of ???); |
---|
239 | >(opt_to_opt_safe … (IH H)) @opt_safe_elim normalize #x] |
---|
240 | #_ % #ABS destruct(ABS) |
---|
241 | qed. |
---|
242 | |
---|
243 | definition index_of ≝ |
---|
244 | λA,test,l.λprf : eqb (count A test l) 1.position_of_safe A test l ?. |
---|
245 | lapply prf -prf @eqb_elim #EQ * >EQ % |
---|
246 | qed. |
---|
247 | |
---|
248 | lemma position_of_append_hit : ∀A,test,l1,l2,x. |
---|
249 | position_of A test (l1@l2) = Some ? x → |
---|
250 | position_of A test l1 = Some ? x ∨ |
---|
251 | (position_of A test l1 = None ? ∧ |
---|
252 | ! p ← position_of A test l2 ; return (|l1| + p) = Some ? x). |
---|
253 | #A#test#l1 elim l1 |
---|
254 | [ #l2 #x change with l2 in match (? @ l2); #EQ >EQ %2 |
---|
255 | % % |
---|
256 | | #hd #tl #IH #l2 #x |
---|
257 | normalize elim (test hd) normalize |
---|
258 | [#H %{H} |
---|
259 | | >position_of_from_aux |
---|
260 | lapply (refl … (position_of A test (tl@l2))) |
---|
261 | generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq |
---|
262 | normalize #EQ destruct(EQ) |
---|
263 | elim (IH … Heq) -IH |
---|
264 | [ #G % |
---|
265 | | * #G #H |
---|
266 | lapply (refl … (position_of A test l2)) |
---|
267 | generalize in ⊢ (???%→?); * [2: #x'] #H' >H' in H; normalize |
---|
268 | #EQ destruct (EQ) %2 %] |
---|
269 | >position_of_from_aux |
---|
270 | [1,2: >G % | >H' %] |
---|
271 | ] |
---|
272 | ] |
---|
273 | qed. |
---|
274 | |
---|
275 | lemma position_of_hit : ∀A,test,l,x.position_of A test l = Some ? x → |
---|
276 | count A test l ≥ 1. |
---|
277 | #A#test#l elim l normalize |
---|
278 | [#x #ABS destruct(ABS) |
---|
279 | |#hd #tl #IH #x elim (test hd) normalize [#EQ destruct(EQ) //] |
---|
280 | >position_of_from_aux |
---|
281 | lapply (refl … (position_of ? test tl)) |
---|
282 | generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize |
---|
283 | #EQ destruct(EQ) @(IH … Heq) |
---|
284 | ] |
---|
285 | qed. |
---|
286 | |
---|
287 | lemma position_of_miss : ∀A,test,l.position_of A test l = None ? → |
---|
288 | count A test l = 0. |
---|
289 | #A#test#l elim l normalize |
---|
290 | [ #_ % |
---|
291 | |#hd #tl #IH elim (test hd) normalize [#EQ destruct(EQ)] |
---|
292 | >position_of_from_aux |
---|
293 | lapply (refl … (position_of ? test tl)) |
---|
294 | generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize |
---|
295 | #EQ destruct(EQ) @(IH … Heq) |
---|
296 | ] |
---|
297 | qed. |
---|
298 | |
---|
299 | |
---|
300 | lemma position_of_append_miss : ∀A,test,l1,l2. |
---|
301 | position_of A test (l1@l2) = None ? → |
---|
302 | position_of A test l1 = None ? ∧ position_of A test l2 = None ?. |
---|
303 | #A#test#l1 elim l1 |
---|
304 | [ #l2 change with l2 in match (? @ l2); #EQ >EQ % % |
---|
305 | | #hd #tl #IH #l2 |
---|
306 | normalize elim (test hd) normalize |
---|
307 | [#H destruct(H) |
---|
308 | | >position_of_from_aux |
---|
309 | lapply (refl … (position_of A test (tl@l2))) |
---|
310 | generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq |
---|
311 | normalize #EQ destruct(EQ) |
---|
312 | elim (IH … Heq) #H1 #H2 |
---|
313 | >position_of_from_aux |
---|
314 | >position_of_from_aux |
---|
315 | >H1 >H2 normalize % % |
---|
316 | ] |
---|
317 | ] |
---|
318 | qed. |
---|
319 | |
---|
320 | |
---|