1 | include "basics/types.ma". |
---|
2 | include "utilities/binary/positive.ma". |
---|
3 | include "ASM/Util.ma". (* bool_to_Prop *) |
---|
4 | |
---|
5 | inductive positive_map (A:Type[0]) : Type[0] ≝ |
---|
6 | | pm_leaf : positive_map A |
---|
7 | | pm_node : option A → positive_map A → positive_map A → positive_map A. |
---|
8 | |
---|
9 | let rec lookup_opt (A:Type[0]) (b:Pos) (t:positive_map A) on t : option A ≝ |
---|
10 | match t with |
---|
11 | [ pm_leaf ⇒ None ? |
---|
12 | | pm_node a l r ⇒ |
---|
13 | match b with |
---|
14 | [ one ⇒ a |
---|
15 | | p0 tl ⇒ lookup_opt A tl l |
---|
16 | | p1 tl ⇒ lookup_opt A tl r |
---|
17 | ] |
---|
18 | ]. |
---|
19 | |
---|
20 | definition lookup: ∀A:Type[0].Pos → positive_map A → A → A ≝ |
---|
21 | λA.λb.λt.λx. |
---|
22 | match lookup_opt A b t with |
---|
23 | [ None ⇒ x |
---|
24 | | Some r ⇒ r |
---|
25 | ]. |
---|
26 | |
---|
27 | let rec pm_set (A:Type[0]) (b:Pos) (a:option A) (t:positive_map A) on b : positive_map A ≝ |
---|
28 | match b with |
---|
29 | [ one ⇒ |
---|
30 | match t with |
---|
31 | [ pm_leaf ⇒ pm_node A a (pm_leaf A) (pm_leaf A) |
---|
32 | | pm_node _ l r ⇒ pm_node A a l r |
---|
33 | ] |
---|
34 | | p0 tl ⇒ |
---|
35 | match t with |
---|
36 | [ pm_leaf ⇒ pm_node A (None ?) (pm_set A tl a (pm_leaf A)) (pm_leaf A) |
---|
37 | | pm_node x l r ⇒ pm_node A x (pm_set A tl a l) r |
---|
38 | ] |
---|
39 | | p1 tl ⇒ |
---|
40 | match t with |
---|
41 | [ pm_leaf ⇒ pm_node A (None ?) (pm_leaf A) (pm_set A tl a (pm_leaf A)) |
---|
42 | | pm_node x l r ⇒ pm_node A x l (pm_set A tl a r) |
---|
43 | ] |
---|
44 | ]. |
---|
45 | |
---|
46 | definition insert : ∀A:Type[0]. Pos → A → positive_map A → positive_map A ≝ |
---|
47 | λA,p,a. pm_set A p (Some ? a). |
---|
48 | |
---|
49 | let rec update (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : option (positive_map A) ≝ |
---|
50 | match b with |
---|
51 | [ one ⇒ |
---|
52 | match t with |
---|
53 | [ pm_leaf ⇒ None ? |
---|
54 | | pm_node x l r ⇒ option_map ?? (λ_. pm_node A (Some ? a) l r) x |
---|
55 | ] |
---|
56 | | p0 tl ⇒ |
---|
57 | match t with |
---|
58 | [ pm_leaf ⇒ None ? |
---|
59 | | pm_node x l r ⇒ option_map ?? (λl. pm_node A x l r) (update A tl a l) |
---|
60 | ] |
---|
61 | | p1 tl ⇒ |
---|
62 | match t with |
---|
63 | [ pm_leaf ⇒ None ? |
---|
64 | | pm_node x l r ⇒ option_map ?? (λr. pm_node A x l r) (update A tl a r) |
---|
65 | ] |
---|
66 | ]. |
---|
67 | |
---|
68 | lemma lookup_opt_pm_set_hit : |
---|
69 | ∀A:Type[0].∀v:option A.∀b:Pos.∀t:positive_map A. |
---|
70 | lookup_opt … b (pm_set … b v t) = v. |
---|
71 | #A #v #b elim b |
---|
72 | [ * // |
---|
73 | | #tl #IH * |
---|
74 | [ whd in ⊢ (??%%); @IH |
---|
75 | | #x #l #r @IH |
---|
76 | ] |
---|
77 | | #tl #IH * |
---|
78 | [ whd in ⊢ (??%%); @IH |
---|
79 | | #x #l #r @IH |
---|
80 | ] |
---|
81 | ] qed. |
---|
82 | |
---|
83 | lemma lookup_opt_insert_hit : |
---|
84 | ∀A:Type[0].∀v:A.∀b:Pos.∀t:positive_map A. |
---|
85 | lookup_opt … b (insert … b v t) = Some A v. |
---|
86 | #A #v #b elim b |
---|
87 | [ * // |
---|
88 | | #tl #IH * |
---|
89 | [ whd in ⊢ (??%%); @IH |
---|
90 | | #x #l #r @IH |
---|
91 | ] |
---|
92 | | #tl #IH * |
---|
93 | [ whd in ⊢ (??%%); @IH |
---|
94 | | #x #l #r @IH |
---|
95 | ] |
---|
96 | ] qed. |
---|
97 | |
---|
98 | lemma lookup_insert_hit: |
---|
99 | ∀a: Type[0]. |
---|
100 | ∀v: a. |
---|
101 | ∀b: Pos. |
---|
102 | ∀t: positive_map a. |
---|
103 | ∀d: a. |
---|
104 | lookup … b (insert … b v t) d = v. |
---|
105 | #A #v #b #t #d whd in ⊢ (??%?); >lookup_opt_insert_hit % |
---|
106 | qed. |
---|
107 | |
---|
108 | lemma lookup_opt_pm_set_miss: |
---|
109 | ∀A:Type[0].∀v:option A.∀b,c:Pos.∀t:positive_map A. |
---|
110 | b ≠ c → lookup_opt … b (pm_set … c v t) = lookup_opt … b t. |
---|
111 | #A #v #b elim b |
---|
112 | [ * [ #t * #H elim (H (refl …)) |
---|
113 | | *: #c' #t #NE cases t // |
---|
114 | ] |
---|
115 | | #b' #IH * |
---|
116 | [ * [ #NE @refl | #x #l #r #NE @refl ] |
---|
117 | | #c' * [ #NE whd in ⊢ (??%%); @IH /2/ |
---|
118 | | #x #l #r #NE whd in ⊢ (??%%); @IH /2/ |
---|
119 | ] |
---|
120 | | #c' * // |
---|
121 | ] |
---|
122 | | #b' #IH * |
---|
123 | [ * [ #NE @refl | #x #l #r #NE @refl ] |
---|
124 | | #c' * // |
---|
125 | | #c' * [ #NE whd in ⊢ (??%%); @IH /2/ |
---|
126 | | #x #l #r #NE whd in ⊢ (??%%); @IH /2/ |
---|
127 | ] |
---|
128 | ] |
---|
129 | ] qed. |
---|
130 | |
---|
131 | lemma lookup_opt_insert_miss: |
---|
132 | ∀A:Type[0].∀v:A.∀b,c:Pos.∀t:positive_map A. |
---|
133 | b ≠ c → lookup_opt … b (insert … c v t) = lookup_opt … b t. |
---|
134 | #A #v #b elim b |
---|
135 | [ * [ #t * #H elim (H (refl …)) |
---|
136 | | *: #c' #t #NE cases t // |
---|
137 | ] |
---|
138 | | #b' #IH * |
---|
139 | [ * [ #NE @refl | #x #l #r #NE @refl ] |
---|
140 | | #c' * [ #NE whd in ⊢ (??%%); @IH /2/ |
---|
141 | | #x #l #r #NE whd in ⊢ (??%%); @IH /2/ |
---|
142 | ] |
---|
143 | | #c' * // |
---|
144 | ] |
---|
145 | | #b' #IH * |
---|
146 | [ * [ #NE @refl | #x #l #r #NE @refl ] |
---|
147 | | #c' * // |
---|
148 | | #c' * [ #NE whd in ⊢ (??%%); @IH /2/ |
---|
149 | | #x #l #r #NE whd in ⊢ (??%%); @IH /2/ |
---|
150 | ] |
---|
151 | ] |
---|
152 | ] qed. |
---|
153 | |
---|
154 | let rec fold (A, B: Type[0]) (f: Pos → A → B → B) |
---|
155 | (t: positive_map A) (b: B) on t: B ≝ |
---|
156 | match t with |
---|
157 | [ pm_leaf ⇒ b |
---|
158 | | pm_node a l r ⇒ |
---|
159 | let b ≝ match a with [ None ⇒ b | Some a ⇒ f one a b ] in |
---|
160 | let b ≝ fold A B (λx.f (p0 x)) l b in |
---|
161 | fold A B (λx.f (p1 x)) r b |
---|
162 | ]. |
---|
163 | |
---|
164 | definition domain_of_pm : ∀A. positive_map A → positive_map unit ≝ |
---|
165 | λA,t. fold A (positive_map unit) (λp,a,b. insert unit p it b) t (pm_leaf unit). |
---|
166 | |
---|
167 | (* Build some results about fold using domain_of_pm. *) |
---|
168 | |
---|
169 | lemma pm_fold_ignore_adding_junk : ∀A. ∀m. ∀f,g:Pos → Pos. ∀s. |
---|
170 | (∀p,q. f p ≠ g q) → |
---|
171 | ∀p. lookup_opt unit (f p) (fold A ? (λx,a,b. insert unit (g x) it b) m s) = lookup_opt unit (f p) s. |
---|
172 | #A #m elim m |
---|
173 | [ normalize // |
---|
174 | | #oa #l #r #IHl #IHr |
---|
175 | #f #g #s #not_g #p |
---|
176 | normalize |
---|
177 | >IHr |
---|
178 | [ >IHl |
---|
179 | [ cases oa |
---|
180 | [ normalize % |
---|
181 | | #a normalize >(lookup_opt_insert_miss ?? (f p)) [ % | @not_g ] |
---|
182 | ] |
---|
183 | | #x #y % #E cases (not_g x (p0 y)) #H @H @E |
---|
184 | ] |
---|
185 | | #x #y % #E cases (not_g x (p1 y)) #H @H @E |
---|
186 | ] |
---|
187 | ] qed. |
---|
188 | |
---|
189 | lemma pm_fold_ind_gen : ∀A,B,m,f,b. |
---|
190 | ∀pre:Pos→Pos. (∀x,y.pre x = pre y → x = y) → ∀ps. (∀p. lookup_opt ? (pre p) ps = None ?) → |
---|
191 | ∀P:B → positive_map unit → Prop. |
---|
192 | P b ps → |
---|
193 | (∀p,ps,a,b. lookup_opt unit (pre p) ps = None unit → lookup_opt A p m = Some A a → P b ps → P (f (pre p) a b) (insert unit (pre p) it ps)) → |
---|
194 | P (fold A B (λx. f (pre x)) m b) (fold ?? (λp,a,b. insert unit (pre p) it b) m ps). |
---|
195 | #A #B #m elim m |
---|
196 | [ // |
---|
197 | | #oa #l #r #IHl #IHr |
---|
198 | #f #b #pre #PRE #ps #PS #P #emp #step whd in ⊢ (?%%); |
---|
199 | @IHr |
---|
200 | [ #x #y #E lapply (PRE … E) #E' destruct // |
---|
201 | | #p change with ((λx. pre (p1 x)) p) in match (pre (p1 p)); >pm_fold_ignore_adding_junk |
---|
202 | [ cases oa [ @PS | #a >(lookup_opt_insert_miss ?? (pre (p1 p))) [ @PS | % #E lapply (PRE … E) #E' destruct ] ] |
---|
203 | | #p #q % #E lapply (PRE … E) #E' destruct |
---|
204 | ] |
---|
205 | | @IHl |
---|
206 | [ #x #y #E lapply (PRE … E) #E' destruct // |
---|
207 | | #p cases oa [ @PS | #a >(lookup_opt_insert_miss ?? (pre (p0 p))) [ @PS | % #E lapply (PRE … E) #E' destruct ] ] |
---|
208 | | cases oa in step ⊢ %; [ #_ @emp | #a #step normalize @step [ @PS | % | @emp ] ] |
---|
209 | | #p #ps' #a #b' @step |
---|
210 | ] |
---|
211 | | #p #ps' #a #b' @step |
---|
212 | ] |
---|
213 | ] qed. |
---|
214 | |
---|
215 | lemma pm_fold_ext : ∀A,B,m,f,b. |
---|
216 | fold A B f m b = fold A B (λx:Pos. f x) m b. |
---|
217 | #A #B #m elim m /4/ |
---|
218 | qed. |
---|
219 | |
---|
220 | (* Main result about folds. (Rather than producing a result about just the |
---|
221 | domain of m we could use the whole mapping, but we'd need a function to |
---|
222 | canonicalise maps because their representation can contain some junk.) *) |
---|
223 | |
---|
224 | lemma pm_fold_ind : ∀A,B,f,m,b. ∀P:B → positive_map unit → Prop. |
---|
225 | P b (pm_leaf unit) → |
---|
226 | (∀p,ps,a,b. lookup_opt unit p ps = None unit → lookup_opt A p m = Some A a → P b ps → P (f p a b) (insert unit p it ps)) → |
---|
227 | P (fold A B f m b) (domain_of_pm A m). |
---|
228 | #A #B #f #m #b #P #emp #step |
---|
229 | >pm_fold_ext |
---|
230 | whd in ⊢ (??%); |
---|
231 | @(pm_fold_ind_gen A B m f b (λx.x) ? (pm_leaf unit) ???) |
---|
232 | [ // |
---|
233 | | // |
---|
234 | | @emp |
---|
235 | | @step |
---|
236 | ] qed. |
---|
237 | |
---|
238 | lemma pm_fold_eq : ∀A,B,b,f. |
---|
239 | (∀p,k:Pos. ∀a,s1,s2. lookup_opt B p s1 = lookup_opt B p s2 → lookup_opt B p (f k a s1) = lookup_opt B p (f k a s2)) → |
---|
240 | ∀p,s1,s2. |
---|
241 | lookup_opt B p s1 = lookup_opt B p s2 → |
---|
242 | lookup_opt B p (fold A (positive_map B) f b s1) = lookup_opt B p (fold A (positive_map B) f b s2). |
---|
243 | #A #B #b elim b |
---|
244 | [ #f #H #p #s1 #s2 #H @H |
---|
245 | | #oa #l #r #IHl #IHr #f #H #p #s1 #s2 #H' |
---|
246 | whd in match (fold ???? s1); |
---|
247 | whd in match (fold ???? s2); |
---|
248 | @IHr [ #q #k #a #s1' #s2' #H'' @H @H'' ] |
---|
249 | @IHl [ #q #k #a #s1' #s2' #H'' @H @H'' ] |
---|
250 | cases oa [ @H' | #a @H @H' ] |
---|
251 | ] qed. |
---|
252 | |
---|
253 | |
---|
254 | lemma pm_fold_ignore_prefix : ∀A. ∀m. ∀pre:Pos → Pos. (∀x,y. pre x = pre y → x = y) → |
---|
255 | ∀p. ∀pre'. |
---|
256 | lookup_opt unit (pre p) (fold A ? (λx,a,b. insert unit (pre (pre' x)) it b) m (pm_leaf ?)) = |
---|
257 | lookup_opt unit p (fold A ? (λx,a,b. insert unit (pre' x) it b) m (pm_leaf ?)). |
---|
258 | #A #m #pre #PRE |
---|
259 | cut (∀p. lookup_opt unit (pre p) (pm_leaf unit) = lookup_opt unit p (pm_leaf unit)) [ // ] |
---|
260 | generalize in match (pm_leaf unit) in ⊢ ((? → ??%?) → ? → ? → ??%?); |
---|
261 | generalize in match (pm_leaf unit); |
---|
262 | elim m |
---|
263 | [ #s1 #s2 #S #p #pre' @S |
---|
264 | | #oa #l #r #IHl #IHr |
---|
265 | #s1 #s2 #S #p #pre' |
---|
266 | whd in ⊢ (??(???%)(???%)); |
---|
267 | @(IHr ???? (λx. pre' (p1 x))) |
---|
268 | #p' @IHl |
---|
269 | #p'' cases oa |
---|
270 | [ @S |
---|
271 | | #a cases (decidable_eq_pos p'' (pre' one)) |
---|
272 | [ #E destruct |
---|
273 | >(lookup_opt_insert_hit ?? (pre (pre' one))) |
---|
274 | >(lookup_opt_insert_hit ?? (pre' one)) |
---|
275 | % |
---|
276 | | #NE >(lookup_opt_insert_miss ??? (pre (pre' one))) |
---|
277 | [ >(lookup_opt_insert_miss ??? (pre' one)) // |
---|
278 | | % #E @(absurd … (PRE … E) NE) |
---|
279 | ] |
---|
280 | ] |
---|
281 | ] |
---|
282 | ] qed. |
---|
283 | |
---|
284 | (* Link the domain of a map (used in the result about fold) to the original |
---|
285 | map. *) |
---|
286 | |
---|
287 | lemma domain_of_pm_present : ∀A,m,p. |
---|
288 | lookup_opt A p m ≠ None ? ↔ lookup_opt unit p (domain_of_pm A m) ≠ None ?. |
---|
289 | |
---|
290 | #A #m whd in match (domain_of_pm ??); |
---|
291 | elim m |
---|
292 | [ #p normalize /3/ |
---|
293 | | #oa #l #r #IHl #IHr |
---|
294 | whd in match (fold ???? (pm_leaf unit)); |
---|
295 | * |
---|
296 | [ change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?))); |
---|
297 | >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ] |
---|
298 | change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?))); |
---|
299 | >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ] |
---|
300 | cases oa |
---|
301 | [ normalize /3/ |
---|
302 | | #a change with (insert unit one ??) in ⊢ (??(?(??(???%)?))); |
---|
303 | >(lookup_opt_insert_hit ?? one) normalize |
---|
304 | % #_ % #E destruct |
---|
305 | ] |
---|
306 | | #p >(pm_fold_eq ??????? (pm_leaf unit)) |
---|
307 | [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ] |
---|
308 | @IHr |
---|
309 | | >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ] |
---|
310 | cases oa |
---|
311 | [ % |
---|
312 | | #a >(lookup_opt_insert_miss ?? (p1 p)) [2: % #E destruct ] |
---|
313 | % |
---|
314 | ] |
---|
315 | | #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p1 y)) |
---|
316 | [ #E destruct |
---|
317 | >(lookup_opt_insert_hit ?? (p1 y)) |
---|
318 | >(lookup_opt_insert_hit ?? (p1 y)) |
---|
319 | % |
---|
320 | | #NE >(lookup_opt_insert_miss ?? x … NE) |
---|
321 | >(lookup_opt_insert_miss ?? x … NE) |
---|
322 | @S |
---|
323 | ] |
---|
324 | ] |
---|
325 | | #p |
---|
326 | >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ] |
---|
327 | >(pm_fold_eq ??????? (pm_leaf unit)) |
---|
328 | [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ] |
---|
329 | @IHl |
---|
330 | | cases oa |
---|
331 | [ % |
---|
332 | | #a >(lookup_opt_insert_miss ?? (p0 p)) [2: % #E destruct ] |
---|
333 | % |
---|
334 | ] |
---|
335 | | #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p0 y)) |
---|
336 | [ #E destruct |
---|
337 | >(lookup_opt_insert_hit ?? (p0 y)) |
---|
338 | >(lookup_opt_insert_hit ?? (p0 y)) |
---|
339 | % |
---|
340 | | #NE >(lookup_opt_insert_miss ?? x … NE) |
---|
341 | >(lookup_opt_insert_miss ?? x … NE) |
---|
342 | @S |
---|
343 | ] |
---|
344 | ] |
---|
345 | ] |
---|
346 | ] qed. |
---|
347 | |
---|
348 | |
---|
349 | lemma update_fail : ∀A,b,a,t. |
---|
350 | update A b a t = None ? → |
---|
351 | lookup_opt A b t = None ?. |
---|
352 | #A #b #a elim b |
---|
353 | [ * [ // | * // #x #l #r normalize #E destruct ] |
---|
354 | | #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?); |
---|
355 | cases (update A b' a r) in U ⊢ %; |
---|
356 | [ // | normalize #t #E destruct ] |
---|
357 | ] |
---|
358 | | #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?); |
---|
359 | cases (update A b' a l) in U ⊢ %; |
---|
360 | [ // | normalize #t #E destruct ] |
---|
361 | ] |
---|
362 | ] qed. |
---|
363 | |
---|
364 | lemma update_lookup_opt_same : ∀A,b,a,t,t'. |
---|
365 | update A b a t = Some ? t' → |
---|
366 | lookup_opt A b t' = Some ? a. |
---|
367 | #A #b #a elim b |
---|
368 | [ * [ #t' normalize #E destruct |
---|
369 | | * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?); |
---|
370 | #E destruct // |
---|
371 | ] |
---|
372 | | #b' #IH * |
---|
373 | [ #t' normalize #E destruct |
---|
374 | | #x #l #r #t' whd in ⊢ (??%? → ??%?); |
---|
375 | lapply (IH r) |
---|
376 | cases (update A b' a r) |
---|
377 | [ #_ normalize #E destruct |
---|
378 | | #r' #H normalize #E destruct @H @refl |
---|
379 | ] |
---|
380 | ] |
---|
381 | | #b' #IH * |
---|
382 | [ #t' normalize #E destruct |
---|
383 | | #x #l #r #t' whd in ⊢ (??%? → ??%?); |
---|
384 | lapply (IH l) |
---|
385 | cases (update A b' a l) |
---|
386 | [ #_ normalize #E destruct |
---|
387 | | #r' #H normalize #E destruct @H @refl |
---|
388 | ] |
---|
389 | ] |
---|
390 | ] qed. |
---|
391 | |
---|
392 | lemma update_lookup_opt_other : ∀A,b,a,t,t'. |
---|
393 | update A b a t = Some ? t' → |
---|
394 | ∀b'. b ≠ b' → |
---|
395 | lookup_opt A b' t = lookup_opt A b' t'. |
---|
396 | #A #b #a elim b |
---|
397 | [ * [ #t' normalize #E destruct |
---|
398 | | * [2: #x] #l #r #t' normalize #E destruct |
---|
399 | * [ * #H elim (H (refl …)) ] |
---|
400 | #tl #NE normalize // |
---|
401 | ] |
---|
402 | | #b' #IH * |
---|
403 | [ #t' normalize #E destruct |
---|
404 | | #x #l #r #t' normalize |
---|
405 | lapply (IH r) |
---|
406 | cases (update A b' a r) |
---|
407 | [ #_ normalize #E destruct |
---|
408 | | #t'' #H normalize #E destruct * // #b'' #NE @H /2/ |
---|
409 | ] |
---|
410 | ] |
---|
411 | | #b' #IH * |
---|
412 | [ #t' normalize #E destruct |
---|
413 | | #x #l #r #t' normalize |
---|
414 | lapply (IH l) |
---|
415 | cases (update A b' a l) |
---|
416 | [ #_ normalize #E destruct |
---|
417 | | #t'' #H normalize #E destruct * // #b'' #NE @H /2/ |
---|
418 | ] |
---|
419 | ] |
---|
420 | ] qed. |
---|
421 | |
---|
422 | include "utilities/option.ma". |
---|
423 | |
---|
424 | let rec map_opt A B (f : A → option B) (b : positive_map A) on b : positive_map B ≝ |
---|
425 | match b with |
---|
426 | [ pm_leaf ⇒ pm_leaf ? |
---|
427 | | pm_node a l r ⇒ pm_node ? (!x ← a ; f x) |
---|
428 | (map_opt ?? f l) |
---|
429 | (map_opt ?? f r) |
---|
430 | ]. |
---|
431 | |
---|
432 | definition map ≝ λA,B,f.map_opt A B (λx. Some ? (f x)). |
---|
433 | |
---|
434 | lemma lookup_opt_map : ∀A,B,f,b,p. |
---|
435 | lookup_opt … p (map_opt A B f b) = ! x ← lookup_opt … p b ; f x. |
---|
436 | #A#B#f#b elim b [//] |
---|
437 | #a #l #r #Hil #Hir * [//] |
---|
438 | #p |
---|
439 | whd in ⊢ (??(???%)(????%?)); |
---|
440 | whd in ⊢ (??%?); // |
---|
441 | qed. |
---|
442 | |
---|
443 | lemma map_opt_id_eq_ext : ∀A,m,f.(∀x.f x = Some ? x) → map_opt A A f m = m. |
---|
444 | #A #m #f #Hf elim m [//] |
---|
445 | * [2:#x] #l #r #Hil #Hir normalize [>Hf] // |
---|
446 | qed. |
---|
447 | |
---|
448 | lemma map_opt_id : ∀A,m.map_opt A A (λx. Some ? x) m = m. |
---|
449 | #A #m @map_opt_id_eq_ext // |
---|
450 | qed. |
---|
451 | |
---|
452 | let rec merge A B C (choice : option A → option B → option C) |
---|
453 | (a : positive_map A) (b : positive_map B) on a : positive_map C ≝ |
---|
454 | match a with |
---|
455 | [ pm_leaf ⇒ map_opt ?? (λx.choice (None ?) (Some ? x)) b |
---|
456 | | pm_node o l r ⇒ |
---|
457 | match b with |
---|
458 | [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a |
---|
459 | | pm_node o' l' r' ⇒ |
---|
460 | pm_node ? (choice o o') |
---|
461 | (merge … choice l l') |
---|
462 | (merge … choice r r') |
---|
463 | ] |
---|
464 | ]. |
---|
465 | |
---|
466 | lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p. |
---|
467 | choice (None ?) (None ?) = None ? → |
---|
468 | lookup_opt … p (merge A B C choice a b) = |
---|
469 | choice (lookup_opt … p a) (lookup_opt … p b). |
---|
470 | #A#B#C#choice#a elim a |
---|
471 | [ normalize #b |
---|
472 | | #o#l#r#Hil#Hir * [2: #o'#l'#r' * normalize /2 by /] |
---|
473 | ] |
---|
474 | #p#choice_good >lookup_opt_map |
---|
475 | elim (lookup_opt ???) |
---|
476 | normalize // |
---|
477 | qed. |
---|
478 | |
---|
479 | let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝ |
---|
480 | match b with |
---|
481 | [ pm_leaf ⇒ 0 |
---|
482 | | pm_node a l r ⇒ |
---|
483 | (match a with |
---|
484 | [ Some _ ⇒ 1 |
---|
485 | | None ⇒ 0 |
---|
486 | ]) + domain_size A l + domain_size A r |
---|
487 | ]. |
---|
488 | |
---|
489 | (* just to load notation for 'norm (list.ma's notation overrides core's 'card)*) |
---|
490 | include "basics/lists/list.ma". |
---|
491 | interpretation "positive map size" 'norm p = (domain_size ? p). |
---|
492 | |
---|
493 | lemma map_opt_size : ∀A,B,f,b.|map_opt A B f b| ≤ |b|. |
---|
494 | #A#B#f#b elim b [//] |
---|
495 | *[2:#x]#l#r#Hil#Hir normalize |
---|
496 | [elim (f ?) normalize [@(transitive_le ? ? ? ? (le_n_Sn ?)) | #y @le_S_S ] ] |
---|
497 | @le_plus assumption |
---|
498 | qed. |
---|
499 | |
---|
500 | lemma map_size : ∀A,B,f,b.|map A B f b| = |b|. |
---|
501 | #A#B#f#b elim b [//] |
---|
502 | *[2:#x]#l#r#Hil#Hir normalize |
---|
503 | >Hil >Hir @refl |
---|
504 | qed. |
---|
505 | |
---|
506 | lemma lookup_opt_O_lt_size : ∀A,m,p. lookup_opt A p m ≠ None ? → 0 < |m|. |
---|
507 | #A#m elim m |
---|
508 | [#p normalize #F elim (absurd ? (refl ??) F) |
---|
509 | |* [2: #x] #l #r #Hil #Hir * normalize |
---|
510 | [1,2,3: // |
---|
511 | |4: #F elim (absurd ? (refl ??) F)] |
---|
512 | #p #H [@(transitive_le … (Hir ? H)) | @(transitive_le … (Hil ? H))] // |
---|
513 | qed. |
---|
514 | |
---|
515 | lemma insert_size : ∀A,p,a,m. |insert A p a m| = |
---|
516 | (match lookup_opt … p m with [Some _ ⇒ 0 | None ⇒ 1]) + |m|. |
---|
517 | #A#p elim p |
---|
518 | [ #a * [2: * [2: #x] #l #r] normalize // |
---|
519 | |*: #p #Hi #a * [2,4: * [2,4: #x] #l #r] normalize >Hi // |
---|
520 | ] qed. |
---|
521 | |
---|
522 | (* Testing all of the entries with a boolean predicate, where the predicate |
---|
523 | is given a proof that the entry is in the map. *) |
---|
524 | |
---|
525 | let rec pm_all_aux (A:Type[0]) (m,t:positive_map A) (pre:Pos → Pos) on t : (∀p. lookup_opt A (pre p) m = lookup_opt A p t) → (∀p,a.lookup_opt A p m = Some A a → bool) → bool ≝ |
---|
526 | match t return λt. (∀p. lookup_opt A (pre p) m = lookup_opt A p t) → (∀p,a.lookup_opt A p m = Some A a → bool) → bool with |
---|
527 | [ pm_leaf ⇒ λ_.λ_. true |
---|
528 | | pm_node a l r ⇒ λH,f. |
---|
529 | pm_all_aux A m l (λx. pre (p0 x)) ? f ∧ |
---|
530 | ((match a return λa. (∀p. ? = lookup_opt A p (pm_node ? a ??)) → ? with [ None ⇒ λ_. true | Some a' ⇒ λH. f (pre one) a' ? ]) H) ∧ |
---|
531 | pm_all_aux A m r (λx. pre (p1 x)) ? f |
---|
532 | ]. |
---|
533 | [ >H % |
---|
534 | | #p >H % |
---|
535 | | #p >H % |
---|
536 | ] qed. |
---|
537 | |
---|
538 | definition pm_all : ∀A. ∀m:positive_map A. (∀p,a. lookup_opt A p m = Some A a → bool) → bool ≝ |
---|
539 | λA,m,f. pm_all_aux A m m (λx.x) (λp. refl ??) f. |
---|
540 | |
---|
541 | (* Proof irrelevance doesn't seem to apply to arbitrary variables, but we can |
---|
542 | use the function graph to show that it's fine. *) |
---|
543 | |
---|
544 | inductive pm_all_pred_graph : ∀A,m,p,a,L. ∀f:∀p:Pos.∀a:A.lookup_opt A p m=Some A a→bool. bool → Prop ≝ |
---|
545 | | pmallpg : ∀A,m,p,a,L. ∀f:∀p:Pos.∀a:A.lookup_opt A p m=Some A a→bool. pm_all_pred_graph A m p a L f (f p a L). |
---|
546 | |
---|
547 | lemma pm_all_pred_irr : ∀A,m,p,a,L,L'. |
---|
548 | ∀f:∀p:Pos.∀a:A.lookup_opt A p m=Some A a→bool. |
---|
549 | f p a L = f p a L'. |
---|
550 | #A #m #p #a #L #L' #f |
---|
551 | cut (pm_all_pred_graph A m p a L f (f p a L)) [ % ] |
---|
552 | cases (f p a L) #H cut (pm_all_pred_graph A m p a L' f ?) [2,5: @H | 1,4: skip] |
---|
553 | * // |
---|
554 | qed. |
---|
555 | |
---|
556 | lemma pm_all_aux_ok_aux : ∀A,m,t,pre,H,f,a,L. |
---|
557 | pm_all_aux A m t pre H f → |
---|
558 | lookup_opt A one t = Some A a → |
---|
559 | f (pre one) a L. |
---|
560 | #A #m * |
---|
561 | [ #pre #H #f #a #L #H #L' normalize in L'; destruct |
---|
562 | | * [ #l #r #pre #H #f #a #L #H' #L' normalize in L'; destruct |
---|
563 | | #a' #l #r #pre #H #f #a #L #AUX #L' normalize in L'; destruct |
---|
564 | cases (andb_Prop_true … AUX) #AUX' cases (andb_Prop_true … AUX') |
---|
565 | #_ #HERE #_ whd in HERE:(?%); @eq_true_to_b <HERE @pm_all_pred_irr |
---|
566 | ] |
---|
567 | ] qed. |
---|
568 | |
---|
569 | lemma pm_all_aux_ok : ∀A,m,t,pre,H,f. |
---|
570 | bool_to_Prop (pm_all_aux A m t pre H f) ↔ (∀p,a,H. f (pre p) a H). |
---|
571 | #A #m #t #pre #H #f % |
---|
572 | [ #H' #p generalize in match pre in H H' ⊢ %; -pre generalize in match t; elim p |
---|
573 | [ #t #pre #H #H' #a #L lapply (refl ? (Some A a)) <L in ⊢ (??%? → ?); >H @pm_all_aux_ok_aux // |
---|
574 | | #q #IH * [ #pre #H #H' #a #L @⊥ >H in L; normalize #E destruct |
---|
575 | | #x #l #r #pre #H #H' #a #L @(IH r) |
---|
576 | [ #x >H % | cases (andb_Prop_true … H') #_ // ] |
---|
577 | ] |
---|
578 | | #q #IH * [ #pre #H #H' #a #L @⊥ >H in L; normalize #E destruct |
---|
579 | | #x #l #r #pre #H #H' #a #L @(IH l) |
---|
580 | [ #x >H % | cases (andb_Prop_true … H') #H'' cases (andb_Prop_true … H'') // ] |
---|
581 | ] |
---|
582 | ] |
---|
583 | | #H' generalize in match pre in H H' ⊢ %; -pre elim t |
---|
584 | [ // |
---|
585 | | * [2:#x] #l #r #IHl #IHr #pre #H #H' @andb_Prop |
---|
586 | [ 1,3: @andb_Prop |
---|
587 | [ 1,3: @IHl // |
---|
588 | | @(H' one x) |
---|
589 | | % |
---|
590 | ] |
---|
591 | | 2,4: @IHr // |
---|
592 | ] |
---|
593 | ] |
---|
594 | ] qed. |
---|
595 | |
---|
596 | lemma pm_all_ok : ∀A,m,f. |
---|
597 | bool_to_Prop (pm_all A m f) ↔ (∀p,a,H. f p a H). |
---|
598 | #A #m #f @pm_all_aux_ok |
---|
599 | qed. |
---|
600 | |
---|
601 | |
---|
602 | (* Attempt to choose an entry in the map, and if successful return the entry |
---|
603 | and the map without it. *) |
---|
604 | |
---|
605 | let rec pm_choose (A:Type[0]) (t:positive_map A) on t : option (Pos × A × (positive_map A)) ≝ |
---|
606 | match t with |
---|
607 | [ pm_leaf ⇒ None ? |
---|
608 | | pm_node a l r ⇒ |
---|
609 | match pm_choose A l with |
---|
610 | [ None ⇒ |
---|
611 | match pm_choose A r with |
---|
612 | [ None ⇒ |
---|
613 | match a with |
---|
614 | [ None ⇒ None ? |
---|
615 | | Some a ⇒ Some ? 〈〈one, a〉, pm_leaf A〉 |
---|
616 | ] |
---|
617 | | Some x ⇒ Some ? 〈〈p1 (\fst (\fst x)), \snd (\fst x)〉, pm_node A a l (\snd x)〉 |
---|
618 | ] |
---|
619 | | Some x ⇒ Some ? 〈〈p0 (\fst (\fst x)), \snd (\fst x)〉, pm_node A a (\snd x) r〉 |
---|
620 | ] |
---|
621 | ]. |
---|
622 | |
---|
623 | lemma pm_choose_empty : ∀A,t. |
---|
624 | pm_choose A t = None ? ↔ ∀p. lookup_opt A p t = None A. |
---|
625 | #A #t elim t |
---|
626 | [ % // |
---|
627 | | * |
---|
628 | [ #l #r * #IHl #IHl' * #IHr #IHr' % |
---|
629 | [ #C * |
---|
630 | [ % |
---|
631 | | #p whd in C:(??%?) ⊢ (??%?); |
---|
632 | @IHr cases (pm_choose A r) in C ⊢ %; |
---|
633 | [ // |
---|
634 | | #x normalize cases (pm_choose A l) [2: #y] normalize #E destruct |
---|
635 | ] |
---|
636 | | #p whd in C:(??%?) ⊢ (??%?); |
---|
637 | @IHl cases (pm_choose A l) in C ⊢ %; |
---|
638 | [ // |
---|
639 | | #x normalize #E destruct |
---|
640 | ] |
---|
641 | ] |
---|
642 | | #L whd in ⊢ (??%?); >IHl' [ normalize >IHr' [ % | #p @(L (p1 p)) ] | #p @(L (p0 p)) ] |
---|
643 | ] |
---|
644 | | #a #l #r #IHl #IHr % |
---|
645 | [ normalize cases (pm_choose A l) [2: normalize #x #E destruct ] |
---|
646 | normalize cases (pm_choose A r) [2: #x] normalize #E destruct |
---|
647 | | #L lapply (L one) normalize #E destruct |
---|
648 | ] |
---|
649 | ] |
---|
650 | ] qed. |
---|
651 | |
---|
652 | lemma pm_choose_empty_card : ∀A,t. |
---|
653 | pm_choose A t = None ? ↔ |t| = 0. |
---|
654 | #A #t elim t |
---|
655 | [ /2/ |
---|
656 | | * [ #l #r * #IHl #IHl' * #IHr #IHr' % |
---|
657 | [ normalize lapply IHl cases (pm_choose A l) [2: #x #_ #E normalize in E; destruct ] |
---|
658 | normalize lapply IHr cases (pm_choose A r) [2: #x #_ #_ #E normalize in E; destruct ] |
---|
659 | #H1 #H2 #_ >(H1 (refl ??)) >(H2 (refl ??)) % |
---|
660 | | normalize #CARD >IHl' [ >IHr' ] /2 by refl, le_n_O_to_eq/ |
---|
661 | ] |
---|
662 | | #a #l #r #_ #_ % normalize |
---|
663 | [ cases (pm_choose A l) [ cases (pm_choose A r) [ | #x ] | #x ] |
---|
664 | #E normalize in E; destruct |
---|
665 | | #E destruct |
---|
666 | ] |
---|
667 | ] |
---|
668 | ] qed. |
---|
669 | |
---|
670 | lemma pm_choose_some : ∀A,t,p,a,t'. |
---|
671 | pm_choose A t = Some ? 〈〈p,a〉,t'〉 → |
---|
672 | lookup_opt A p t = Some A a ∧ |
---|
673 | lookup_opt A p t' = None A ∧ |
---|
674 | (∀q. p = q ∨ lookup_opt A q t = lookup_opt A q t') ∧ |
---|
675 | |t| = S (|t'|). |
---|
676 | #A #t elim t |
---|
677 | [ #p #a #t' normalize #E destruct |
---|
678 | | #ao #l #r #IHl #IHr * |
---|
679 | [ #a #t' normalize |
---|
680 | lapply (pm_choose_empty_card A l) |
---|
681 | lapply (pm_choose_empty A l) |
---|
682 | cases (pm_choose A l) normalize [2: #x #_ #_ #E destruct ] * #EMPl #EMPl' * #CARDl #CARDl' |
---|
683 | lapply (pm_choose_empty_card A r) |
---|
684 | lapply (pm_choose_empty A r) |
---|
685 | cases (pm_choose A r) normalize [2: #x #_ #_ #E destruct ] * #EMPr #EMPr' * #CARDr #CARDr' |
---|
686 | cases ao normalize [2:#x] #E destruct |
---|
687 | % [ % /2/ * /2/ #q %2 whd in ⊢ (??%%); /2/ | >CARDl >CARDr // ] |
---|
688 | | #p #a #t' normalize |
---|
689 | lapply (pm_choose_empty_card A l) |
---|
690 | lapply (pm_choose_empty A l) |
---|
691 | cases (pm_choose A l) normalize [2: #x #_ #_ #E destruct ] * #EMPl #EMPl' * #CARDl #CARDl' |
---|
692 | lapply (IHr p) |
---|
693 | cases (pm_choose A r) normalize [ #_ cases ao [2:#a'] normalize #E destruct ] |
---|
694 | * * #p' #a' #t'' #IH #E destruct |
---|
695 | cases (IH ?? (refl ??)) * * #L1 #L2 #L3 #CARD |
---|
696 | % [ % [ % [ // | @L2 ]| * /2/ #q cases (L3 q) /2/ #L4 %2 @L4 ] | cases ao normalize >CARD // ] |
---|
697 | | #p #a #t' normalize |
---|
698 | lapply (IHl p) |
---|
699 | cases (pm_choose A l) normalize |
---|
700 | [ #_ cases (pm_choose A r) normalize [ cases ao [2:#a'] normalize #E destruct |
---|
701 | | #x #E destruct ] |
---|
702 | | * * #p' #a' #t'' #IH #E destruct |
---|
703 | cases (IH ?? (refl ??)) * * #L1 #L2 #L3 #CARD |
---|
704 | % [ % [ % [ // | @L2 ]| * /2/ #q cases (L3 q) /2/ #L4 %2 @L4 ] | cases ao normalize >CARD // ] |
---|
705 | ] |
---|
706 | ] |
---|
707 | ] qed. |
---|
708 | |
---|
709 | (* Try to remove an element, return updated map if successful *) |
---|
710 | |
---|
711 | let rec pm_try_remove (A:Type[0]) (b:Pos) (t:positive_map A) on b : option (A × (positive_map A)) ≝ |
---|
712 | match b with |
---|
713 | [ one ⇒ |
---|
714 | match t with |
---|
715 | [ pm_leaf ⇒ None ? |
---|
716 | | pm_node x l r ⇒ option_map ?? (λx. 〈x, pm_node A (None ?) l r〉) x |
---|
717 | ] |
---|
718 | | p0 tl ⇒ |
---|
719 | match t with |
---|
720 | [ pm_leaf ⇒ None ? |
---|
721 | | pm_node x l r ⇒ option_map ?? (λxl. 〈\fst xl, pm_node A x (\snd xl) r〉) (pm_try_remove A tl l) |
---|
722 | ] |
---|
723 | | p1 tl ⇒ |
---|
724 | match t with |
---|
725 | [ pm_leaf ⇒ None ? |
---|
726 | | pm_node x l r ⇒ option_map ?? (λxr. 〈\fst xr, pm_node A x l (\snd xr)〉) (pm_try_remove A tl r) |
---|
727 | ] |
---|
728 | ]. |
---|
729 | |
---|
730 | lemma pm_try_remove_none : ∀A,b,t. |
---|
731 | pm_try_remove A b t = None ? ↔ lookup_opt A b t = None ?. |
---|
732 | #A #b elim b |
---|
733 | [ * [ /2/ | * [ /2/ | #a #l #r % normalize #E destruct ] ] |
---|
734 | | #p #IH * [ /2/ | #x #l #r % normalize cases (IH r) cases (pm_try_remove A p r) |
---|
735 | [ normalize #H #X @H | * #a #t' #_ normalize #_ #X destruct |
---|
736 | | normalize // | * #a #t' normalize #A #B #C lapply (B C) #E destruct |
---|
737 | ] ] |
---|
738 | | #p #IH * [ /2/ | #x #l #r % normalize cases (IH l) cases (pm_try_remove A p l) |
---|
739 | [ normalize #H #X @H | * #a #t' #_ normalize #_ #X destruct |
---|
740 | | normalize // | * #a #t' normalize #A #B #C lapply (B C) #E destruct |
---|
741 | ] ] |
---|
742 | ] qed. |
---|
743 | |
---|
744 | lemma pm_try_remove_some : ∀A,p,t,a,t'. |
---|
745 | pm_try_remove A p t = Some ? 〈a,t'〉 → |
---|
746 | lookup_opt A p t = Some A a ∧ |
---|
747 | lookup_opt A p t' = None A ∧ |
---|
748 | (∀q. p = q ∨ lookup_opt A q t = lookup_opt A q t') ∧ |
---|
749 | |t| = S (|t'|). |
---|
750 | #A #p elim p |
---|
751 | [ * [ #a #t' #E normalize in E; destruct |
---|
752 | | * [ #l #r #a #t' #E normalize in E; destruct |
---|
753 | | #a' #l #r #a #t' #E normalize in E; destruct % [ % [ % // | * /2/ ]| // ] |
---|
754 | ] |
---|
755 | ] |
---|
756 | | #p' #IH * |
---|
757 | [ #a #t' #E normalize in E; destruct |
---|
758 | | #x #l #r #a #t' whd in ⊢ (??%? → ?); |
---|
759 | lapply (IH r) cases (pm_try_remove A p' r) [ #_ #E normalize in E; destruct ] |
---|
760 | * #a' #r' #H #E whd in E:(??%?); destruct |
---|
761 | cases (H a r' (refl ??)) * * #L1 #L2 #L3 #CARD |
---|
762 | @conj try @conj try @conj |
---|
763 | [ @L1 | @L2 | * /2/ #q cases (L3 q) [ /2/ | #E %2 @E ] | cases x normalize >CARD // ] |
---|
764 | ] |
---|
765 | | #p' #IH * |
---|
766 | [ #a #t' #E normalize in E; destruct |
---|
767 | | #x #l #r #a #t' whd in ⊢ (??%? → ?); |
---|
768 | lapply (IH l) cases (pm_try_remove A p' l) [ #_ #E normalize in E; destruct ] |
---|
769 | * #a' #l' #H #E whd in E:(??%?); destruct |
---|
770 | cases (H a l' (refl ??)) * * #L1 #L2 #L3 #CARD |
---|
771 | @conj try @conj try @conj |
---|
772 | [ @L1 | @L2 | * /2/ #q cases (L3 q) [ /2/ | #E %2 @E ] | cases x normalize >CARD // ] |
---|
773 | ] |
---|
774 | ] qed. |
---|
775 | |
---|
776 | lemma pm_try_remove_some' : ∀A,p,t,a. |
---|
777 | lookup_opt A p t = Some A a → |
---|
778 | ∃t'. pm_try_remove A p t = Some ? 〈a,t'〉. |
---|
779 | #A #p elim p |
---|
780 | [ * [ #a #L normalize in L; destruct |
---|
781 | | #q #l #r #a #L normalize in L; destruct % [2: % | skip ] |
---|
782 | ] |
---|
783 | | #q #IH * |
---|
784 | [ #a #L normalize in L; destruct |
---|
785 | | #x #l #r #a #L cases (IH r a L) #r' #R |
---|
786 | % [2: whd in ⊢ (??%?); >R in ⊢ (??%?); % | skip ] |
---|
787 | ] |
---|
788 | | #q #IH * |
---|
789 | [ #a #L normalize in L; destruct |
---|
790 | | #x #l #r #a #L cases (IH l a L) #l' #R |
---|
791 | % [2: whd in ⊢ (??%?); >R in ⊢ (??%?); % | skip ] |
---|
792 | ] |
---|
793 | ] qed. |
---|
794 | |
---|
795 | (* An "informative" dependently typed fold *) |
---|
796 | |
---|
797 | let rec pm_fold_inf_aux |
---|
798 | (A, B: Type[0]) |
---|
799 | (t: positive_map A) |
---|
800 | (f: ∀p:Pos. ∀a:A. lookup_opt … p t = Some A a → B → B) |
---|
801 | (t': positive_map A) |
---|
802 | (pre: Pos → Pos) |
---|
803 | (b: B) on t': (∀p. lookup_opt … p t' = lookup_opt … (pre p) t) → B ≝ |
---|
804 | match t' return λt'. (∀p. lookup_opt A p t' = lookup_opt A (pre p) t) → B with |
---|
805 | [ pm_leaf ⇒ λ_. b |
---|
806 | | pm_node a l r ⇒ λH. |
---|
807 | let b ≝ match a return λa. lookup_opt A one (pm_node A a ??) = ? → B with [ None ⇒ λ_.b | Some a ⇒ λH. f (pre one) a ? b ] (H one) in |
---|
808 | let b ≝ pm_fold_inf_aux A B t f l (λx. pre (p0 x)) b ? in |
---|
809 | pm_fold_inf_aux A B t f r (λx. pre (p1 x)) b ? |
---|
810 | ]. |
---|
811 | [ #p @(H (p1 p)) | #p @(H (p0 p)) | <H % ] |
---|
812 | qed. |
---|
813 | |
---|
814 | definition pm_fold_inf : ∀A, B: Type[0]. ∀t: positive_map A. |
---|
815 | ∀f: (∀p:Pos. ∀a:A. lookup_opt … p t = Some A a → B → B). B → B ≝ |
---|
816 | λA,B,t,f,b. pm_fold_inf_aux A B t f t (λx.x) b (λp. refl ??). |
---|
817 | |
---|
818 | (* Find an entry in the map matching the given predicate *) |
---|
819 | |
---|
820 | let rec pm_find_aux (pre: Pos → Pos) (A:Type[0]) (t: positive_map A) (p:Pos → A → bool) on t : option (Pos × A) ≝ |
---|
821 | match t with |
---|
822 | [ pm_leaf ⇒ None ? |
---|
823 | | pm_node a l r ⇒ |
---|
824 | let x ≝ match a with |
---|
825 | [ Some a ⇒ if p (pre one) a then Some ? 〈pre one, a〉 else None ? |
---|
826 | | None ⇒ None ? |
---|
827 | ] in |
---|
828 | match x with |
---|
829 | [ Some x ⇒ Some ? x |
---|
830 | | None ⇒ |
---|
831 | match pm_find_aux (λx. pre (p0 x)) A l p with |
---|
832 | [ None ⇒ pm_find_aux (λx. pre (p1 x)) A r p |
---|
833 | | Some y ⇒ Some ? y |
---|
834 | ] |
---|
835 | ] |
---|
836 | ]. |
---|
837 | |
---|
838 | definition pm_find : ∀A:Type[0]. positive_map A → (Pos → A → bool) → option (Pos × A) ≝ |
---|
839 | pm_find_aux (λx.x). |
---|
840 | |
---|
841 | lemma pm_find_aux_pre : ∀A,t,pre,p,q,a. |
---|
842 | pm_find_aux pre A t p = Some ? 〈q,a〉 → |
---|
843 | ∃q'. q = pre q'. |
---|
844 | #A #t elim t |
---|
845 | [ normalize #pre #p #q #a #E destruct |
---|
846 | | * [2:#a] #l #r #IHl #IHr #pre #p #q #a' normalize |
---|
847 | [ cases (p (pre one) a) normalize [ #E destruct /2/ ] ] |
---|
848 | lapply (IHl (λx. pre (p0 x)) p) |
---|
849 | cases (pm_find_aux ?? l ?) |
---|
850 | [ 1,3: #_ normalize |
---|
851 | lapply (IHr (λx. pre (p1 x)) p) |
---|
852 | cases (pm_find_aux ?? r ?) |
---|
853 | [ 1,3: #_ #E destruct |
---|
854 | | *: * #q' #a'' #H #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/ |
---|
855 | ] |
---|
856 | | *: * #q' #a'' #H normalize #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/ |
---|
857 | ] |
---|
858 | ] qed. |
---|
859 | |
---|
860 | (* XXX: Hmm... destruct doesn't work properly with this, not sure why *) |
---|
861 | lemma option_pair_f_eq : ∀A,B:Type[0].∀a,a',b,b'. ∀f:A → A. |
---|
862 | (∀a,a'. f a = f a' → a = a') → |
---|
863 | Some (A×B) 〈f a,b〉 = Some ? 〈f a',b'〉 → |
---|
864 | a = a' ∧ b = b'. |
---|
865 | #A #B #a #a' #b #b' #f #EXT #E |
---|
866 | cut (f a = f a') [ destruct (E) destruct (e0) @e2 (* WTF? *) ] |
---|
867 | #E' >(EXT … E') in E ⊢ %; #E destruct /2/ |
---|
868 | qed. |
---|
869 | |
---|
870 | lemma pm_find_lookup : ∀A,p,q,a,t. |
---|
871 | pm_find A t p = Some ? 〈q,a〉 → |
---|
872 | lookup_opt A q t = Some ? a. |
---|
873 | #A #p #q #a normalize #t |
---|
874 | change with ((λx.x) q) in match q in ⊢ (% → ?); |
---|
875 | cut (∀y,z:Pos. (λx.x) y = (λx.x) z → y = z) // |
---|
876 | generalize in match q; -q generalize in match (λx.x); |
---|
877 | elim t |
---|
878 | [ #pre #q #_ normalize #E destruct |
---|
879 | | * [2:#a'] #l #r #IHl #IHr #pre #q #PRE |
---|
880 | normalize [ cases (p (pre one) a') normalize [ #E cases (option_pair_f_eq … pre PRE E) #E1 #E2 destruct normalize % ] ] |
---|
881 | lapply (IHl (λx.pre (p0 x))) |
---|
882 | lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p) |
---|
883 | cases (pm_find_aux ?? l ?) |
---|
884 | [ 1,3: #_ #_ normalize |
---|
885 | lapply (IHr (λx.pre (p1 x))) |
---|
886 | lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p) |
---|
887 | cases (pm_find_aux ?? r ?) |
---|
888 | [ 1,3: #_ #_ #E destruct |
---|
889 | | *: * #q' #a' #H1 #H2 #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct |
---|
890 | whd in ⊢ (??%?); @H2 // |
---|
891 | #y #z #E lapply (PRE … E) #E' destruct // |
---|
892 | ] |
---|
893 | | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct |
---|
894 | whd in ⊢ (??%?); @H2 // |
---|
895 | #y #z #E lapply (PRE … E) #E' destruct // |
---|
896 | ] |
---|
897 | ] qed. |
---|
898 | |
---|
899 | lemma pm_find_aux_none : ∀A,t,pre,p,q,a. |
---|
900 | pm_find_aux pre A t p = None ? → |
---|
901 | lookup_opt A q t = Some ? a → |
---|
902 | ¬ p (pre q) a. |
---|
903 | #A #t elim t |
---|
904 | [ #pre #p #q #a #_ normalize #E destruct |
---|
905 | | #oa #l #r #IHl #IHr #pre #p * |
---|
906 | [ #a cases oa |
---|
907 | [ #_ normalize #E destruct |
---|
908 | | #a' #F whd in F:(??%?); whd in F:(??match % with [_⇒?|_⇒?]?); |
---|
909 | #E normalize in E; destruct |
---|
910 | cases (p (pre one) a) in F ⊢ %; // |
---|
911 | normalize #E destruct |
---|
912 | ] |
---|
913 | | #q #a #F #L @(IHr (λx. pre (p1 x)) p q a ? L) |
---|
914 | whd in F:(??%?); cases oa in F; |
---|
915 | [2: #a' normalize cases (p (pre one) a') [ normalize #E destruct ] ] |
---|
916 | normalize cases (pm_find_aux ?? l p) normalize // |
---|
917 | #x #E destruct |
---|
918 | | #q #a #F #L @(IHl (λx. pre (p0 x)) p q a ? L) |
---|
919 | whd in F:(??%?); cases oa in F; |
---|
920 | [2: #a' normalize cases (p (pre one) a') [ normalize #E destruct ] ] |
---|
921 | normalize cases (pm_find_aux ?? l p) normalize // |
---|
922 | ] |
---|
923 | ] qed. |
---|
924 | |
---|
925 | lemma pm_find_none : ∀A,t,p,q,a. |
---|
926 | pm_find A t p = None ? → |
---|
927 | lookup_opt A q t = Some ? a → |
---|
928 | ¬ p q a. |
---|
929 | #A #t |
---|
930 | @(pm_find_aux_none A t (λx.x)) |
---|
931 | qed. |
---|
932 | |
---|
933 | lemma pm_find_predicate : ∀A,t,p,q,a. |
---|
934 | pm_find A t p = Some ? 〈q,a〉 → |
---|
935 | p q a. |
---|
936 | #A #t #p normalize #q |
---|
937 | change with ((λx.x) q) in match q; generalize in match q; -q generalize in match (λx.x); |
---|
938 | elim t |
---|
939 | [ normalize #pre #q #a #E destruct |
---|
940 | | * [2:#a'] #l #r #IHl #IHr #pre #q #a normalize |
---|
941 | [ lapply (refl ? (p (pre one) a')) cases (p (pre one) a') in ⊢ (???% → %); |
---|
942 | [ #E normalize #E' |
---|
943 | cut (pre one = pre q) [ destruct (E') destruct (e0) @e2 (* XXX ! *) ] |
---|
944 | #E'' <E'' in E' ⊢ %; #E' destruct >E % |
---|
945 | | #_ normalize |
---|
946 | ] |
---|
947 | ] |
---|
948 | lapply (IHl (λx.pre (p0 x))) |
---|
949 | lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p) |
---|
950 | cases (pm_find_aux ?? l ?) |
---|
951 | [ 1,3: #_ #_ normalize |
---|
952 | lapply (IHr (λx.pre (p1 x))) |
---|
953 | lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p) |
---|
954 | cases (pm_find_aux ?? r ?) |
---|
955 | [ 1,3: #_ #_ #E destruct |
---|
956 | | *: * #q' #a' #H1 #H2 #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E % |
---|
957 | ] |
---|
958 | | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E % |
---|
959 | ] |
---|
960 | ] qed. |
---|