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