source: src/common/PositiveMap.ma @ 2415

Last change on this file since 2415 was 2415, checked in by campbell, 7 years ago

Add the ability to map blocks to symbols in preparation for stack space.

File size: 22.3 KB
Line 
1include "basics/types.ma".
2include "utilities/binary/positive.ma".
3include "ASM/Util.ma". (* bool_to_Prop *)
4
5inductive 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
9let rec lookup_opt (A:Type[0]) (b:Pos) (t:positive_map A) on t : option A ≝
10match 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
20definition 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
27let rec insert (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : positive_map A ≝
28match 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
46let rec update (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : option (positive_map A) ≝
47match 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
65lemma 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
80lemma 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 %
88qed.
89
90lemma 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
113let rec fold (A, B: Type[0]) (f: Pos → A → B → B)
114 (t: positive_map A) (b: B) on t: B ≝
115match 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
123lemma 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
138lemma 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
166lemma 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
196include "utilities/option.ma".
197
198let rec map_opt A B (f : A → option B) (b : positive_map A) on b : positive_map B ≝
199match 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
206definition map ≝ λA,B,f.map_opt A B (λx. Some ? (f x)).
207
208lemma 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
213whd in ⊢ (??(???%)(????%?));
214whd in ⊢ (??%?); //
215qed.
216
217lemma 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] //
220qed.
221
222lemma map_opt_id : ∀A,m.map_opt A A (λx. Some ? x) m = m.
223#A #m @map_opt_id_eq_ext //
224qed.
225
226let 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 ≝
228match 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
240lemma 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
249elim (lookup_opt ???)
250normalize //
251qed.
252
253let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝
254match 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)*)
264include "basics/lists/list.ma".
265interpretation "positive map size" 'norm p = (domain_size ? p).
266
267lemma 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
272qed.
273
274lemma 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
278qed.
279
280lemma 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))] //
287qed.
288
289lemma 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
299let 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 ≝
300match 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
312definition 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   
318inductive 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
321lemma 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
325cut (pm_all_pred_graph A m p a L f (f p a L)) [ % ]
326cases (f p a L) #H cut (pm_all_pred_graph A m p a L' f ?) [2,5: @H | 1,4: skip]
327* //
328qed.
329
330lemma 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
343lemma 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
370lemma 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
373qed.
374
375
376(* Attempt to choose an entry in the map, and if successful return the entry
377   and the map without it. *)
378
379let rec pm_choose (A:Type[0]) (t:positive_map A) on t : option (Pos × A × (positive_map A)) ≝
380match 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
397lemma 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
426lemma 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
444lemma 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
485let rec pm_try_remove (A:Type[0]) (b:Pos) (t:positive_map A) on b : option (A × (positive_map A)) ≝
486match 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
504lemma 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
518lemma 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
550lemma 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(* An "informative" dependently typed fold *)
570
571let rec pm_fold_inf_aux
572 (A, B: Type[0])
573 (t: positive_map A)
574 (f: ∀p:Pos. ∀a:A. lookup_opt … p t = Some A a → B → B)
575 (t': positive_map A)
576 (pre: Pos → Pos)
577 (b: B) on t': (∀p. lookup_opt … p t' = lookup_opt … (pre p) t) → B ≝
578match t' return λt'. (∀p. lookup_opt A p t' = lookup_opt A (pre p) t) → B with
579[ pm_leaf ⇒ λ_. b
580| pm_node a l r ⇒ λH.
581    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
582    let b ≝ pm_fold_inf_aux A B t f l (λx. pre (p0 x)) b ? in
583            pm_fold_inf_aux A B t f r (λx. pre (p1 x)) b ?
584].
585[ #p @(H (p1 p)) | #p @(H (p0 p)) | <H % ]
586qed.
587
588definition pm_fold_inf : ∀A, B: Type[0]. ∀t: positive_map A.
589 ∀f: (∀p:Pos. ∀a:A. lookup_opt … p t = Some A a → B → B). B → B ≝
590  λA,B,t,f,b. pm_fold_inf_aux A B t f t (λx.x) b (λp. refl ??).
591
592(* Find an entry in the map matching the given predicate *)
593
594let rec pm_find_aux (pre: Pos → Pos) (A:Type[0]) (t: positive_map A) (p:Pos → A → bool) on t : option (Pos × A) ≝
595match t with
596[ pm_leaf ⇒ None ?
597| pm_node a l r ⇒
598  let x ≝ match a with
599  [ Some a ⇒ if p (pre one) a then Some ? 〈pre one, a〉 else None ?
600  | None ⇒ None ?
601  ] in
602  match x with
603  [ Some x ⇒ Some ? x
604  | None ⇒
605    match pm_find_aux (λx. pre (p0 x)) A l p with
606    [ None ⇒ pm_find_aux (λx. pre (p1 x)) A r p
607    | Some y ⇒ Some ? y
608    ]
609  ]
610].
611
612definition pm_find : ∀A:Type[0]. positive_map A → (Pos → A → bool) → option (Pos × A) ≝
613  pm_find_aux (λx.x).
614
615lemma pm_find_aux_pre : ∀A,t,pre,p,q,a.
616  pm_find_aux pre A t p = Some ? 〈q,a〉 →
617  ∃q'. q = pre q'.
618#A #t elim t
619[ normalize #pre #p #q #a #E destruct
620| * [2:#a] #l #r #IHl #IHr #pre #p #q #a' normalize
621  [ cases (p (pre one) a) normalize [ #E destruct /2/ ] ]
622  lapply (IHl (λx. pre (p0 x)) p)
623  cases (pm_find_aux ?? l ?)
624  [ 1,3: #_ normalize
625    lapply (IHr (λx. pre (p1 x)) p)
626    cases (pm_find_aux ?? r ?)
627    [ 1,3: #_ #E destruct
628    | *: * #q' #a'' #H #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/
629    ]
630  | *: * #q' #a'' #H normalize #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/
631  ]
632] qed.
633
634(* XXX: Hmm... destruct doesn't work properly with this, not sure why *)
635lemma option_pair_f_eq : ∀A,B:Type[0].∀a,a',b,b'. ∀f:A → A.
636  (∀a,a'. f a = f a' → a = a') →
637  Some (A×B) 〈f a,b〉 = Some ? 〈f a',b'〉 →
638  a = a' ∧ b = b'.
639#A #B #a #a' #b #b' #f #EXT #E
640cut (f a = f a') [ destruct (E) destruct (e0) @e2 (* WTF? *) ]
641#E' >(EXT … E') in E ⊢ %; #E destruct /2/
642qed.
643
644lemma pm_find_lookup : ∀A,p,q,a,t.
645  pm_find A t p = Some ? 〈q,a〉 →
646  lookup_opt A q t = Some ? a.
647#A #p #q #a normalize #t
648change with ((λx.x) q) in match q in ⊢ (% → ?);
649cut (∀y,z:Pos. (λx.x) y = (λx.x) z → y = z) //
650generalize in match q; -q generalize in match (λx.x);
651elim t
652[ #pre #q #_  normalize #E destruct
653| * [2:#a'] #l #r #IHl #IHr #pre #q #PRE
654  normalize [ cases (p (pre one) a') normalize [ #E cases (option_pair_f_eq … pre PRE E) #E1 #E2 destruct normalize % ] ]
655  lapply (IHl (λx.pre (p0 x)))
656  lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p)
657  cases (pm_find_aux ?? l ?)
658  [ 1,3: #_ #_ normalize
659    lapply (IHr (λx.pre (p1 x)))
660    lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p)
661    cases (pm_find_aux ?? r ?)
662    [ 1,3: #_ #_ #E destruct
663    | *: * #q' #a' #H1 #H2 #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct
664         whd in ⊢ (??%?); @H2 //
665         #y #z #E lapply (PRE … E) #E' destruct //
666    ]
667  | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct
668         whd in ⊢ (??%?); @H2 //
669         #y #z #E lapply (PRE … E) #E' destruct //
670  ]
671] qed.
672
673lemma pm_find_predicate : ∀A,t,p,q,a.
674  pm_find A t p = Some ? 〈q,a〉 →
675  p q a.
676#A #t #p normalize #q
677change with ((λx.x) q) in match q; generalize in match q; -q generalize in match (λx.x);
678elim t
679[ normalize #pre #q #a #E destruct
680| * [2:#a'] #l #r #IHl #IHr #pre #q #a normalize
681  [ lapply (refl ? (p (pre one) a')) cases (p (pre one) a') in ⊢ (???% → %);
682    [ #E normalize #E'
683      cut (pre one = pre q) [ destruct (E') destruct (e0) @e2 (* XXX ! *) ]
684      #E'' <E'' in E' ⊢ %; #E' destruct >E %
685    | #_ normalize
686    ]
687  ]
688  lapply (IHl (λx.pre (p0 x)))
689  lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p)
690  cases (pm_find_aux ?? l ?)
691  [ 1,3: #_ #_ normalize
692    lapply (IHr (λx.pre (p1 x)))
693    lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p)
694    cases (pm_find_aux ?? r ?)
695    [ 1,3: #_ #_ #E destruct
696    | *: * #q' #a' #H1 #H2 #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E %
697    ]
698  | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E %
699  ]
700] qed.
Note: See TracBrowser for help on using the repository browser.