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 insert (A:Type[0]) (b:Pos) (a: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 (Some ? a) (pm_leaf A) (pm_leaf A) |
---|
32 | | pm_node _ l r ⇒ pm_node A (Some ? a) l r |
---|
33 | ] |
---|
34 | | p0 tl ⇒ |
---|
35 | match t with |
---|
36 | [ pm_leaf ⇒ pm_node A (None ?) (insert A tl a (pm_leaf A)) (pm_leaf A) |
---|
37 | | pm_node x l r ⇒ pm_node A x (insert A tl a l) r |
---|
38 | ] |
---|
39 | | p1 tl ⇒ |
---|
40 | match t with |
---|
41 | [ pm_leaf ⇒ pm_node A (None ?) (pm_leaf A) (insert A tl a (pm_leaf A)) |
---|
42 | | pm_node x l r ⇒ pm_node A x l (insert A tl a r) |
---|
43 | ] |
---|
44 | ]. |
---|
45 | |
---|
46 | let rec update (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : option (positive_map A) ≝ |
---|
47 | match b with |
---|
48 | [ one ⇒ |
---|
49 | match t with |
---|
50 | [ pm_leaf ⇒ None ? |
---|
51 | | pm_node x l r ⇒ option_map ?? (λ_. pm_node A (Some ? a) l r) x |
---|
52 | ] |
---|
53 | | p0 tl ⇒ |
---|
54 | match t with |
---|
55 | [ pm_leaf ⇒ None ? |
---|
56 | | pm_node x l r ⇒ option_map ?? (λl. pm_node A x l r) (update A tl a l) |
---|
57 | ] |
---|
58 | | p1 tl ⇒ |
---|
59 | match t with |
---|
60 | [ pm_leaf ⇒ None ? |
---|
61 | | pm_node x l r ⇒ option_map ?? (λr. pm_node A x l r) (update A tl a r) |
---|
62 | ] |
---|
63 | ]. |
---|
64 | |
---|
65 | lemma lookup_opt_insert_hit : |
---|
66 | ∀A:Type[0].∀v:A.∀b:Pos.∀t:positive_map A. |
---|
67 | lookup_opt … b (insert … b v t) = Some A v. |
---|
68 | #A #v #b elim b |
---|
69 | [ * // |
---|
70 | | #tl #IH * |
---|
71 | [ whd in ⊢ (??%%); @IH |
---|
72 | | #x #l #r @IH |
---|
73 | ] |
---|
74 | | #tl #IH * |
---|
75 | [ whd in ⊢ (??%%); @IH |
---|
76 | | #x #l #r @IH |
---|
77 | ] |
---|
78 | ] qed. |
---|
79 | |
---|
80 | lemma lookup_insert_hit: |
---|
81 | ∀a: Type[0]. |
---|
82 | ∀v: a. |
---|
83 | ∀b: Pos. |
---|
84 | ∀t: positive_map a. |
---|
85 | ∀d: a. |
---|
86 | lookup … b (insert … b v t) d = v. |
---|
87 | #A #v #b #t #d whd in ⊢ (??%?); >lookup_opt_insert_hit % |
---|
88 | qed. |
---|
89 | |
---|
90 | lemma lookup_opt_insert_miss: |
---|
91 | ∀A:Type[0].∀v:A.∀b,c:Pos.∀t:positive_map A. |
---|
92 | b ≠ c → lookup_opt … b (insert … c v t) = lookup_opt … b t. |
---|
93 | #A #v #b elim b |
---|
94 | [ * [ #t * #H elim (H (refl …)) |
---|
95 | | *: #c' #t #NE cases t // |
---|
96 | ] |
---|
97 | | #b' #IH * |
---|
98 | [ * [ #NE @refl | #x #l #r #NE @refl ] |
---|
99 | | #c' * [ #NE whd in ⊢ (??%%); @IH /2/ |
---|
100 | | #x #l #r #NE whd in ⊢ (??%%); @IH /2/ |
---|
101 | ] |
---|
102 | | #c' * // |
---|
103 | ] |
---|
104 | | #b' #IH * |
---|
105 | [ * [ #NE @refl | #x #l #r #NE @refl ] |
---|
106 | | #c' * // |
---|
107 | | #c' * [ #NE whd in ⊢ (??%%); @IH /2/ |
---|
108 | | #x #l #r #NE whd in ⊢ (??%%); @IH /2/ |
---|
109 | ] |
---|
110 | ] |
---|
111 | ] qed. |
---|
112 | |
---|
113 | let rec fold (A, B: Type[0]) (f: Pos → A → B → B) |
---|
114 | (t: positive_map A) (b: B) on t: B ≝ |
---|
115 | match t with |
---|
116 | [ pm_leaf ⇒ b |
---|
117 | | pm_node a l r ⇒ |
---|
118 | let b ≝ match a with [ None ⇒ b | Some a ⇒ f one a b ] in |
---|
119 | let b ≝ fold A B (λx.f (p0 x)) l b in |
---|
120 | fold A B (λx.f (p1 x)) r b |
---|
121 | ]. |
---|
122 | |
---|
123 | lemma update_fail : ∀A,b,a,t. |
---|
124 | update A b a t = None ? → |
---|
125 | lookup_opt A b t = None ?. |
---|
126 | #A #b #a elim b |
---|
127 | [ * [ // | * // #x #l #r normalize #E destruct ] |
---|
128 | | #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?); |
---|
129 | cases (update A b' a r) in U ⊢ %; |
---|
130 | [ // | normalize #t #E destruct ] |
---|
131 | ] |
---|
132 | | #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?); |
---|
133 | cases (update A b' a l) in U ⊢ %; |
---|
134 | [ // | normalize #t #E destruct ] |
---|
135 | ] |
---|
136 | ] qed. |
---|
137 | |
---|
138 | lemma update_lookup_opt_same : ∀A,b,a,t,t'. |
---|
139 | update A b a t = Some ? t' → |
---|
140 | lookup_opt A b t' = Some ? a. |
---|
141 | #A #b #a elim b |
---|
142 | [ * [ #t' normalize #E destruct |
---|
143 | | * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?); |
---|
144 | #E destruct // |
---|
145 | ] |
---|
146 | | #b' #IH * |
---|
147 | [ #t' normalize #E destruct |
---|
148 | | #x #l #r #t' whd in ⊢ (??%? → ??%?); |
---|
149 | lapply (IH r) |
---|
150 | cases (update A b' a r) |
---|
151 | [ #_ normalize #E destruct |
---|
152 | | #r' #H normalize #E destruct @H @refl |
---|
153 | ] |
---|
154 | ] |
---|
155 | | #b' #IH * |
---|
156 | [ #t' normalize #E destruct |
---|
157 | | #x #l #r #t' whd in ⊢ (??%? → ??%?); |
---|
158 | lapply (IH l) |
---|
159 | cases (update A b' a l) |
---|
160 | [ #_ normalize #E destruct |
---|
161 | | #r' #H normalize #E destruct @H @refl |
---|
162 | ] |
---|
163 | ] |
---|
164 | ] qed. |
---|
165 | |
---|
166 | lemma update_lookup_opt_other : ∀A,b,a,t,t'. |
---|
167 | update A b a t = Some ? t' → |
---|
168 | ∀b'. b ≠ b' → |
---|
169 | lookup_opt A b' t = lookup_opt A b' t'. |
---|
170 | #A #b #a elim b |
---|
171 | [ * [ #t' normalize #E destruct |
---|
172 | | * [2: #x] #l #r #t' normalize #E destruct |
---|
173 | * [ * #H elim (H (refl …)) ] |
---|
174 | #tl #NE normalize // |
---|
175 | ] |
---|
176 | | #b' #IH * |
---|
177 | [ #t' normalize #E destruct |
---|
178 | | #x #l #r #t' normalize |
---|
179 | lapply (IH r) |
---|
180 | cases (update A b' a r) |
---|
181 | [ #_ normalize #E destruct |
---|
182 | | #t'' #H normalize #E destruct * // #b'' #NE @H /2/ |
---|
183 | ] |
---|
184 | ] |
---|
185 | | #b' #IH * |
---|
186 | [ #t' normalize #E destruct |
---|
187 | | #x #l #r #t' normalize |
---|
188 | lapply (IH l) |
---|
189 | cases (update A b' a l) |
---|
190 | [ #_ normalize #E destruct |
---|
191 | | #t'' #H normalize #E destruct * // #b'' #NE @H /2/ |
---|
192 | ] |
---|
193 | ] |
---|
194 | ] qed. |
---|
195 | |
---|
196 | include "utilities/option.ma". |
---|
197 | |
---|
198 | let rec map_opt A B (f : A → option B) (b : positive_map A) on b : positive_map B ≝ |
---|
199 | match b with |
---|
200 | [ pm_leaf ⇒ pm_leaf ? |
---|
201 | | pm_node a l r ⇒ pm_node ? (a »= f) |
---|
202 | (map_opt ?? f l) |
---|
203 | (map_opt ?? f r) |
---|
204 | ]. |
---|
205 | |
---|
206 | definition map ≝ λA,B,f.map_opt A B (λx. Some ? (f x)). |
---|
207 | |
---|
208 | lemma lookup_opt_map : ∀A,B,f,b,p. |
---|
209 | lookup_opt … p (map_opt A B f b) = ! x ← lookup_opt … p b ; f x. |
---|
210 | #A#B#f#b elim b [//] |
---|
211 | #a #l #r #Hil #Hir * [//] |
---|
212 | #p |
---|
213 | whd in ⊢ (??(???%)(????%?)); |
---|
214 | whd in ⊢ (??%?); // |
---|
215 | qed. |
---|
216 | |
---|
217 | lemma map_opt_id_eq_ext : ∀A,m,f.(∀x.f x = Some ? x) → map_opt A A f m = m. |
---|
218 | #A #m #f #Hf elim m [//] |
---|
219 | * [2:#x] #l #r #Hil #Hir normalize [>Hf] // |
---|
220 | qed. |
---|
221 | |
---|
222 | lemma map_opt_id : ∀A,m.map_opt A A (λx. Some ? x) m = m. |
---|
223 | #A #m @map_opt_id_eq_ext // |
---|
224 | qed. |
---|
225 | |
---|
226 | let rec merge A B C (choice : option A → option B → option C) |
---|
227 | (a : positive_map A) (b : positive_map B) on a : positive_map C ≝ |
---|
228 | match a with |
---|
229 | [ pm_leaf ⇒ map_opt ?? (λx.choice (None ?) (Some ? x)) b |
---|
230 | | pm_node o l r ⇒ |
---|
231 | match b with |
---|
232 | [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a |
---|
233 | | pm_node o' l' r' ⇒ |
---|
234 | pm_node ? (choice o o') |
---|
235 | (merge … choice l l') |
---|
236 | (merge … choice r r') |
---|
237 | ] |
---|
238 | ]. |
---|
239 | |
---|
240 | lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p. |
---|
241 | choice (None ?) (None ?) = None ? → |
---|
242 | lookup_opt … p (merge A B C choice a b) = |
---|
243 | choice (lookup_opt … p a) (lookup_opt … p b). |
---|
244 | #A#B#C#choice#a elim a |
---|
245 | [ normalize #b |
---|
246 | | #o#l#r#Hil#Hir * [2: #o'#l'#r' * normalize /2 by /] |
---|
247 | ] |
---|
248 | #p#choice_good >lookup_opt_map |
---|
249 | elim (lookup_opt ???) |
---|
250 | normalize // |
---|
251 | qed. |
---|
252 | |
---|
253 | let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝ |
---|
254 | match b with |
---|
255 | [ pm_leaf ⇒ 0 |
---|
256 | | pm_node a l r ⇒ |
---|
257 | (match a with |
---|
258 | [ Some _ ⇒ 1 |
---|
259 | | None ⇒ 0 |
---|
260 | ]) + domain_size A l + domain_size A r |
---|
261 | ]. |
---|
262 | |
---|
263 | (* just to load notation for 'norm (list.ma's notation overrides core's 'card)*) |
---|
264 | include "basics/lists/list.ma". |
---|
265 | interpretation "positive map size" 'norm p = (domain_size ? p). |
---|
266 | |
---|
267 | lemma map_opt_size : ∀A,B,f,b.|map_opt A B f b| ≤ |b|. |
---|
268 | #A#B#f#b elim b [//] |
---|
269 | *[2:#x]#l#r#Hil#Hir normalize |
---|
270 | [elim (f ?) normalize [@(transitive_le ? ? ? ? (le_n_Sn ?)) | #y @le_S_S ] ] |
---|
271 | @le_plus assumption |
---|
272 | qed. |
---|
273 | |
---|
274 | lemma map_size : ∀A,B,f,b.|map A B f b| = |b|. |
---|
275 | #A#B#f#b elim b [//] |
---|
276 | *[2:#x]#l#r#Hil#Hir normalize |
---|
277 | >Hil >Hir @refl |
---|
278 | qed. |
---|
279 | |
---|
280 | lemma lookup_opt_O_lt_size : ∀A,m,p. lookup_opt A p m ≠ None ? → 0 < |m|. |
---|
281 | #A#m elim m |
---|
282 | [#p normalize #F elim (absurd ? (refl ??) F) |
---|
283 | |* [2: #x] #l #r #Hil #Hir * normalize |
---|
284 | [1,2,3: // |
---|
285 | |4: #F elim (absurd ? (refl ??) F)] |
---|
286 | #p #H [@(transitive_le … (Hir ? H)) | @(transitive_le … (Hil ? H))] // |
---|
287 | qed. |
---|
288 | |
---|
289 | lemma insert_size : ∀A,p,a,m. |insert A p a m| = |
---|
290 | (match lookup_opt … p m with [Some _ ⇒ 0 | None ⇒ 1]) + |m|. |
---|
291 | #A#p elim p |
---|
292 | [ #a * [2: * [2: #x] #l #r] normalize // |
---|
293 | |*: #p #Hi #a * [2,4: * [2,4: #x] #l #r] normalize >Hi // |
---|
294 | ] qed. |
---|
295 | |
---|
296 | (* Testing all of the entries with a boolean predicate, where the predicate |
---|
297 | is given a proof that the entry is in the map. *) |
---|
298 | |
---|
299 | 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 ≝ |
---|
300 | 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 |
---|
301 | [ pm_leaf ⇒ λ_.λ_. true |
---|
302 | | pm_node a l r ⇒ λH,f. |
---|
303 | pm_all_aux A m l (λx. pre (p0 x)) ? f ∧ |
---|
304 | ((match a return λa. (∀p. ? = lookup_opt A p (pm_node ? a ??)) → ? with [ None ⇒ λ_. true | Some a' ⇒ λH. f (pre one) a' ? ]) H) ∧ |
---|
305 | pm_all_aux A m r (λx. pre (p1 x)) ? f |
---|
306 | ]. |
---|
307 | [ >H % |
---|
308 | | #p >H % |
---|
309 | | #p >H % |
---|
310 | ] qed. |
---|
311 | |
---|
312 | definition pm_all : ∀A. ∀m:positive_map A. (∀p,a. lookup_opt A p m = Some A a → bool) → bool ≝ |
---|
313 | λA,m,f. pm_all_aux A m m (λx.x) (λp. refl ??) f. |
---|
314 | |
---|
315 | (* Proof irrelevance doesn't seem to apply to arbitrary variables, but we can |
---|
316 | use the function graph to show that it's fine. *) |
---|
317 | |
---|
318 | 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 ≝ |
---|
319 | | 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). |
---|
320 | |
---|
321 | lemma pm_all_pred_irr : ∀A,m,p,a,L,L'. |
---|
322 | ∀f:∀p:Pos.∀a:A.lookup_opt A p m=Some A a→bool. |
---|
323 | f p a L = f p a L'. |
---|
324 | #A #m #p #a #L #L' #f |
---|
325 | cut (pm_all_pred_graph A m p a L f (f p a L)) [ % ] |
---|
326 | cases (f p a L) #H cut (pm_all_pred_graph A m p a L' f ?) [2,5: @H | 1,4: skip] |
---|
327 | * // |
---|
328 | qed. |
---|
329 | |
---|
330 | lemma pm_all_aux_ok_aux : ∀A,m,t,pre,H,f,a,L. |
---|
331 | pm_all_aux A m t pre H f → |
---|
332 | lookup_opt A one t = Some A a → |
---|
333 | f (pre one) a L. |
---|
334 | #A #m * |
---|
335 | [ #pre #H #f #a #L #H #L' normalize in L'; destruct |
---|
336 | | * [ #l #r #pre #H #f #a #L #H' #L' normalize in L'; destruct |
---|
337 | | #a' #l #r #pre #H #f #a #L #AUX #L' normalize in L'; destruct |
---|
338 | cases (andb_Prop_true … AUX) #AUX' cases (andb_Prop_true … AUX') |
---|
339 | #_ #HERE #_ whd in HERE:(?%); @eq_true_to_b <HERE @pm_all_pred_irr |
---|
340 | ] |
---|
341 | ] qed. |
---|
342 | |
---|
343 | lemma pm_all_aux_ok : ∀A,m,t,pre,H,f. |
---|
344 | bool_to_Prop (pm_all_aux A m t pre H f) ↔ (∀p,a,H. f (pre p) a H). |
---|
345 | #A #m #t #pre #H #f % |
---|
346 | [ #H' #p generalize in match pre in H H' ⊢ %; -pre generalize in match t; elim p |
---|
347 | [ #t #pre #H #H' #a #L lapply (refl ? (Some A a)) <L in ⊢ (??%? → ?); >H @pm_all_aux_ok_aux // |
---|
348 | | #q #IH * [ #pre #H #H' #a #L @⊥ >H in L; normalize #E destruct |
---|
349 | | #x #l #r #pre #H #H' #a #L @(IH r) |
---|
350 | [ #x >H % | cases (andb_Prop_true … H') #_ // ] |
---|
351 | ] |
---|
352 | | #q #IH * [ #pre #H #H' #a #L @⊥ >H in L; normalize #E destruct |
---|
353 | | #x #l #r #pre #H #H' #a #L @(IH l) |
---|
354 | [ #x >H % | cases (andb_Prop_true … H') #H'' cases (andb_Prop_true … H'') // ] |
---|
355 | ] |
---|
356 | ] |
---|
357 | | #H' generalize in match pre in H H' ⊢ %; -pre elim t |
---|
358 | [ // |
---|
359 | | * [2:#x] #l #r #IHl #IHr #pre #H #H' @andb_Prop |
---|
360 | [ 1,3: @andb_Prop |
---|
361 | [ 1,3: @IHl // |
---|
362 | | @(H' one x) |
---|
363 | | % |
---|
364 | ] |
---|
365 | | 2,4: @IHr // |
---|
366 | ] |
---|
367 | ] |
---|
368 | ] qed. |
---|
369 | |
---|
370 | lemma pm_all_ok : ∀A,m,f. |
---|
371 | bool_to_Prop (pm_all A m f) ↔ (∀p,a,H. f p a H). |
---|
372 | #A #m #f @pm_all_aux_ok |
---|
373 | qed. |
---|
374 | |
---|
375 | |
---|
376 | (* Attempt to choose an entry in the map, and if successful return the entry |
---|
377 | and the map without it. *) |
---|
378 | |
---|
379 | let rec pm_choose (A:Type[0]) (t:positive_map A) on t : option (Pos × A × (positive_map A)) ≝ |
---|
380 | match t with |
---|
381 | [ pm_leaf ⇒ None ? |
---|
382 | | pm_node a l r ⇒ |
---|
383 | match pm_choose A l with |
---|
384 | [ None ⇒ |
---|
385 | match pm_choose A r with |
---|
386 | [ None ⇒ |
---|
387 | match a with |
---|
388 | [ None ⇒ None ? |
---|
389 | | Some a ⇒ Some ? 〈〈one, a〉, pm_leaf A〉 |
---|
390 | ] |
---|
391 | | Some x ⇒ Some ? 〈〈p1 (\fst (\fst x)), \snd (\fst x)〉, pm_node A a l (\snd x)〉 |
---|
392 | ] |
---|
393 | | Some x ⇒ Some ? 〈〈p0 (\fst (\fst x)), \snd (\fst x)〉, pm_node A a (\snd x) r〉 |
---|
394 | ] |
---|
395 | ]. |
---|
396 | |
---|
397 | lemma pm_choose_empty : ∀A,t. |
---|
398 | pm_choose A t = None ? ↔ ∀p. lookup_opt A p t = None A. |
---|
399 | #A #t elim t |
---|
400 | [ % // |
---|
401 | | * |
---|
402 | [ #l #r * #IHl #IHl' * #IHr #IHr' % |
---|
403 | [ #C * |
---|
404 | [ % |
---|
405 | | #p whd in C:(??%?) ⊢ (??%?); |
---|
406 | @IHr cases (pm_choose A r) in C ⊢ %; |
---|
407 | [ // |
---|
408 | | #x normalize cases (pm_choose A l) [2: #y] normalize #E destruct |
---|
409 | ] |
---|
410 | | #p whd in C:(??%?) ⊢ (??%?); |
---|
411 | @IHl cases (pm_choose A l) in C ⊢ %; |
---|
412 | [ // |
---|
413 | | #x normalize #E destruct |
---|
414 | ] |
---|
415 | ] |
---|
416 | | #L whd in ⊢ (??%?); >IHl' [ normalize >IHr' [ % | #p @(L (p1 p)) ] | #p @(L (p0 p)) ] |
---|
417 | ] |
---|
418 | | #a #l #r #IHl #IHr % |
---|
419 | [ normalize cases (pm_choose A l) [2: normalize #x #E destruct ] |
---|
420 | normalize cases (pm_choose A r) [2: #x] normalize #E destruct |
---|
421 | | #L lapply (L one) normalize #E destruct |
---|
422 | ] |
---|
423 | ] |
---|
424 | ] qed. |
---|
425 | |
---|
426 | lemma pm_choose_empty_card : ∀A,t. |
---|
427 | pm_choose A t = None ? ↔ |t| = 0. |
---|
428 | #A #t elim t |
---|
429 | [ /2/ |
---|
430 | | * [ #l #r * #IHl #IHl' * #IHr #IHr' % |
---|
431 | [ normalize lapply IHl cases (pm_choose A l) [2: #x #_ #E normalize in E; destruct ] |
---|
432 | normalize lapply IHr cases (pm_choose A r) [2: #x #_ #_ #E normalize in E; destruct ] |
---|
433 | #H1 #H2 #_ >(H1 (refl ??)) >(H2 (refl ??)) % |
---|
434 | | normalize #CARD >IHl' [ >IHr' ] /2 by refl, le_n_O_to_eq/ |
---|
435 | ] |
---|
436 | | #a #l #r #_ #_ % normalize |
---|
437 | [ cases (pm_choose A l) [ cases (pm_choose A r) [ | #x ] | #x ] |
---|
438 | #E normalize in E; destruct |
---|
439 | | #E destruct |
---|
440 | ] |
---|
441 | ] |
---|
442 | ] qed. |
---|
443 | |
---|
444 | lemma pm_choose_some : ∀A,t,p,a,t'. |
---|
445 | pm_choose A t = Some ? 〈〈p,a〉,t'〉 → |
---|
446 | lookup_opt A p t = Some A a ∧ |
---|
447 | lookup_opt A p t' = None A ∧ |
---|
448 | (∀q. p = q ∨ lookup_opt A q t = lookup_opt A q t') ∧ |
---|
449 | |t| = S (|t'|). |
---|
450 | #A #t elim t |
---|
451 | [ #p #a #t' normalize #E destruct |
---|
452 | | #ao #l #r #IHl #IHr * |
---|
453 | [ #a #t' normalize |
---|
454 | lapply (pm_choose_empty_card A l) |
---|
455 | lapply (pm_choose_empty A l) |
---|
456 | cases (pm_choose A l) normalize [2: #x #_ #_ #E destruct ] * #EMPl #EMPl' * #CARDl #CARDl' |
---|
457 | lapply (pm_choose_empty_card A r) |
---|
458 | lapply (pm_choose_empty A r) |
---|
459 | cases (pm_choose A r) normalize [2: #x #_ #_ #E destruct ] * #EMPr #EMPr' * #CARDr #CARDr' |
---|
460 | cases ao normalize [2:#x] #E destruct |
---|
461 | % [ % /2/ * /2/ #q %2 whd in ⊢ (??%%); /2/ | >CARDl >CARDr // ] |
---|
462 | | #p #a #t' normalize |
---|
463 | lapply (pm_choose_empty_card A l) |
---|
464 | lapply (pm_choose_empty A l) |
---|
465 | cases (pm_choose A l) normalize [2: #x #_ #_ #E destruct ] * #EMPl #EMPl' * #CARDl #CARDl' |
---|
466 | lapply (IHr p) |
---|
467 | cases (pm_choose A r) normalize [ #_ cases ao [2:#a'] normalize #E destruct ] |
---|
468 | * * #p' #a' #t'' #IH #E destruct |
---|
469 | cases (IH ?? (refl ??)) * * #L1 #L2 #L3 #CARD |
---|
470 | % [ % [ % [ // | @L2 ]| * /2/ #q cases (L3 q) /2/ #L4 %2 @L4 ] | cases ao normalize >CARD // ] |
---|
471 | | #p #a #t' normalize |
---|
472 | lapply (IHl p) |
---|
473 | cases (pm_choose A l) normalize |
---|
474 | [ #_ cases (pm_choose A r) normalize [ cases ao [2:#a'] normalize #E destruct |
---|
475 | | #x #E destruct ] |
---|
476 | | * * #p' #a' #t'' #IH #E destruct |
---|
477 | cases (IH ?? (refl ??)) * * #L1 #L2 #L3 #CARD |
---|
478 | % [ % [ % [ // | @L2 ]| * /2/ #q cases (L3 q) /2/ #L4 %2 @L4 ] | cases ao normalize >CARD // ] |
---|
479 | ] |
---|
480 | ] |
---|
481 | ] qed. |
---|
482 | |
---|
483 | (* Try to remove an element, return updated map if successful *) |
---|
484 | |
---|
485 | let rec pm_try_remove (A:Type[0]) (b:Pos) (t:positive_map A) on b : option (A × (positive_map A)) ≝ |
---|
486 | match b with |
---|
487 | [ one ⇒ |
---|
488 | match t with |
---|
489 | [ pm_leaf ⇒ None ? |
---|
490 | | pm_node x l r ⇒ option_map ?? (λx. 〈x, pm_node A (None ?) l r〉) x |
---|
491 | ] |
---|
492 | | p0 tl ⇒ |
---|
493 | match t with |
---|
494 | [ pm_leaf ⇒ None ? |
---|
495 | | pm_node x l r ⇒ option_map ?? (λxl. 〈\fst xl, pm_node A x (\snd xl) r〉) (pm_try_remove A tl l) |
---|
496 | ] |
---|
497 | | p1 tl ⇒ |
---|
498 | match t with |
---|
499 | [ pm_leaf ⇒ None ? |
---|
500 | | pm_node x l r ⇒ option_map ?? (λxr. 〈\fst xr, pm_node A x l (\snd xr)〉) (pm_try_remove A tl r) |
---|
501 | ] |
---|
502 | ]. |
---|
503 | |
---|
504 | lemma pm_try_remove_none : ∀A,b,t. |
---|
505 | pm_try_remove A b t = None ? ↔ lookup_opt A b t = None ?. |
---|
506 | #A #b elim b |
---|
507 | [ * [ /2/ | * [ /2/ | #a #l #r % normalize #E destruct ] ] |
---|
508 | | #p #IH * [ /2/ | #x #l #r % normalize cases (IH r) cases (pm_try_remove A p r) |
---|
509 | [ normalize #H #X @H | * #a #t' #_ normalize #_ #X destruct |
---|
510 | | normalize // | * #a #t' normalize #A #B #C lapply (B C) #E destruct |
---|
511 | ] ] |
---|
512 | | #p #IH * [ /2/ | #x #l #r % normalize cases (IH l) cases (pm_try_remove A p l) |
---|
513 | [ normalize #H #X @H | * #a #t' #_ normalize #_ #X destruct |
---|
514 | | normalize // | * #a #t' normalize #A #B #C lapply (B C) #E destruct |
---|
515 | ] ] |
---|
516 | ] qed. |
---|
517 | |
---|
518 | lemma pm_try_remove_some : ∀A,p,t,a,t'. |
---|
519 | pm_try_remove A p t = Some ? 〈a,t'〉 → |
---|
520 | lookup_opt A p t = Some A a ∧ |
---|
521 | lookup_opt A p t' = None A ∧ |
---|
522 | (∀q. p = q ∨ lookup_opt A q t = lookup_opt A q t') ∧ |
---|
523 | |t| = S (|t'|). |
---|
524 | #A #p elim p |
---|
525 | [ * [ #a #t' #E normalize in E; destruct |
---|
526 | | * [ #l #r #a #t' #E normalize in E; destruct |
---|
527 | | #a' #l #r #a #t' #E normalize in E; destruct % [ % [ % // | * /2/ ]| // ] |
---|
528 | ] |
---|
529 | ] |
---|
530 | | #p' #IH * |
---|
531 | [ #a #t' #E normalize in E; destruct |
---|
532 | | #x #l #r #a #t' whd in ⊢ (??%? → ?); |
---|
533 | lapply (IH r) cases (pm_try_remove A p' r) [ #_ #E normalize in E; destruct ] |
---|
534 | * #a' #r' #H #E whd in E:(??%?); destruct |
---|
535 | cases (H a r' (refl ??)) * * #L1 #L2 #L3 #CARD |
---|
536 | @conj try @conj try @conj |
---|
537 | [ @L1 | @L2 | * /2/ #q cases (L3 q) [ /2/ | #E %2 @E ] | cases x normalize >CARD // ] |
---|
538 | ] |
---|
539 | | #p' #IH * |
---|
540 | [ #a #t' #E normalize in E; destruct |
---|
541 | | #x #l #r #a #t' whd in ⊢ (??%? → ?); |
---|
542 | lapply (IH l) cases (pm_try_remove A p' l) [ #_ #E normalize in E; destruct ] |
---|
543 | * #a' #l' #H #E whd in E:(??%?); destruct |
---|
544 | cases (H a l' (refl ??)) * * #L1 #L2 #L3 #CARD |
---|
545 | @conj try @conj try @conj |
---|
546 | [ @L1 | @L2 | * /2/ #q cases (L3 q) [ /2/ | #E %2 @E ] | cases x normalize >CARD // ] |
---|
547 | ] |
---|
548 | ] qed. |
---|
549 | |
---|
550 | lemma pm_try_remove_some' : ∀A,p,t,a. |
---|
551 | lookup_opt A p t = Some A a → |
---|
552 | ∃t'. pm_try_remove A p t = Some ? 〈a,t'〉. |
---|
553 | #A #p elim p |
---|
554 | [ * [ #a #L normalize in L; destruct |
---|
555 | | #q #l #r #a #L normalize in L; destruct % [2: % | skip ] |
---|
556 | ] |
---|
557 | | #q #IH * |
---|
558 | [ #a #L normalize in L; destruct |
---|
559 | | #x #l #r #a #L cases (IH r a L) #r' #R |
---|
560 | % [2: whd in ⊢ (??%?); >R in ⊢ (??%?); % | skip ] |
---|
561 | ] |
---|
562 | | #q #IH * |
---|
563 | [ #a #L normalize in L; destruct |
---|
564 | | #x #l #r #a #L cases (IH l a L) #l' #R |
---|
565 | % [2: whd in ⊢ (??%?); >R in ⊢ (??%?); % | skip ] |
---|
566 | ] |
---|
567 | ] qed. |
---|
568 | |
---|
569 | |
---|