source: src/common/PositiveMap.ma @ 2599

Last change on this file since 2599 was 2599, checked in by tranquil, 7 years ago
  • map_opt and map on positive maps are now clean (erase empty subtrees)
  • minor changes to blocks
File size: 32.0 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 pm_set (A:Type[0]) (b:Pos) (a:option 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 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
46definition insert : ∀A:Type[0]. Pos → A → positive_map A → positive_map A ≝
47λA,p,a. pm_set A p (Some ? a).
48
49let rec update (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : option (positive_map A) ≝
50match 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
68lemma 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
83lemma 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
98lemma 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 %
106qed.
107
108lemma 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
131lemma 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
154let rec fold (A, B: Type[0]) (f: Pos → A → B → B)
155 (t: positive_map A) (b: B) on t: B ≝
156match 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
164definition 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
169lemma 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
189lemma 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
215lemma 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/
218qed.
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
224lemma 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
230whd 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
238lemma 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
254lemma 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
259cut (∀p. lookup_opt unit (pre p) (pm_leaf unit) = lookup_opt unit p (pm_leaf unit)) [ // ]
260generalize in match (pm_leaf unit) in ⊢ ((? → ??%?) → ? → ? → ??%?);
261generalize in match (pm_leaf unit);
262elim 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
287lemma 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 ??);
291elim 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
349lemma 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
364lemma 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
392lemma 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
422include "utilities/option.ma".
423
424definition is_none : ∀A.option A → bool ≝ λA,o.match o with [ None ⇒ true | _ ⇒ false ].
425definition is_pm_leaf : ∀A.positive_map A → bool ≝ λA,m.match m with [ pm_leaf ⇒ true | _ ⇒ false ].
426
427let rec map_opt A B (f : A → option B) (b : positive_map A) on b : positive_map B ≝
428match b with
429[ pm_leaf ⇒ pm_leaf ?
430| pm_node a l r ⇒
431  let a' ≝ !x ← a ; f x in
432  let l' ≝ map_opt ?? f l in
433  let r' ≝ map_opt ?? f r in
434  if is_none … a' ∧ is_pm_leaf … l' ∧ is_pm_leaf … r' then
435    pm_leaf ?
436  else
437    pm_node ? a' l' r'
438].
439
440definition map ≝ λA,B,f.map_opt A B (λx. Some ? (f x)).
441
442lemma andb_false_r : ∀b.(b∧false)=false. *% qed.
443
444lemma lookup_opt_map : ∀A,B,f,b,p.
445  lookup_opt … p (map_opt A B f b) = ! x ← lookup_opt … p b ; f x.
446#A#B#f#b elim b [//]
447#a #l #r #IHl #IHr * [2,3: #p ]
448whd in match (map_opt ????); whd in match (lookup_opt ???) in ⊢ (???%);
449[3: cases (! x ← a ; f x) [2: #x] try % cases (?∧?) % ]
450inversion (map_opt ??? l)
451[2,4: #lo #ll #lr #_ #_ >andb_false_r normalize nodelta #EQl <EQl
452  whd in ⊢ (??%?); // ]
453#EQl
454inversion (map_opt ??? r)
455[2,4: #ro #rl #rr #_ #_ >andb_false_r normalize nodelta #EQr <EQr <EQl
456  whd in ⊢ (??%?); // ]
457#EQr
458[ <IHr >EQr | <IHl >EQl ] cases (?∧?) %
459qed.
460
461(*
462lemma map_opt_id_eq_ext : ∀A,m,f.(∀x.f x = Some ? x) → map_opt A A f m = m.
463#A #m #f #Hf elim m [//]
464* [2:#x] #l #r #Hil #Hir normalize [>Hf] //
465qed.
466
467lemma map_opt_id : ∀A,m.map_opt A A (λx. Some ? x) m = m.
468#A #m @map_opt_id_eq_ext //
469qed.
470*)
471
472let rec merge A B C (choice : option A → option B → option C)
473  (a : positive_map A) (b : positive_map B) on a : positive_map C ≝
474match a with
475[ pm_leaf ⇒ map_opt ?? (λx.choice (None ?) (Some ? x)) b
476| pm_node o l r ⇒
477  match b with
478  [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a
479  | pm_node o' l' r' ⇒
480    let o'' ≝ choice o o' in
481    let l'' ≝ merge … choice l l' in
482    let r'' ≝ merge … choice r r' in
483    if is_none … o'' ∧ is_pm_leaf … l'' ∧ is_pm_leaf … r'' then
484      pm_leaf ?
485    else
486      pm_node ? o'' l'' r''
487  ]
488].
489
490lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p.
491  choice (None ?) (None ?) = None ? →
492  lookup_opt … p (merge A B C choice a b) =
493    choice (lookup_opt … p a) (lookup_opt … p b).
494 #A#B#C#choice#a elim a -a
495[ #b
496| #o#l#r#Hil#Hir * [2: #o'#l'#r' * [2,3: #x] normalize cases(choice o o') normalize /2 by /
497  [3: cases (merge A B C choice l l') normalize /2 by / cases(merge A B C choice r r')
498      normalize /2 by /
499  |*: #H [<Hir|<Hil] /2 by / cases(merge A B C choice l l') normalize /2 by /
500      cases (merge A B C choice r r') normalize /2 by /
501  ]
502]]
503#p #choice_good >lookup_opt_map
504elim (lookup_opt ???)
505normalize //
506qed.
507
508let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝
509match b with
510[ pm_leaf ⇒ 0
511| pm_node a l r ⇒
512  (match a with
513   [ Some _ ⇒ 1
514   | None ⇒ 0
515   ]) + domain_size A l + domain_size A r
516].
517
518interpretation "positive map size" 'card p = (domain_size ? p).
519
520(*
521lemma map_opt_size : ∀A,B,f,b.|map_opt A B f b| ≤ |b|.
522#A#B#f#b elim b [//]
523*[2:#x]#l#r#Hil#Hir normalize
524[elim (f ?) normalize [@(transitive_le ? ? ? ? (le_n_Sn ?)) | #y @le_S_S ] ]
525@le_plus assumption
526qed.
527*)
528
529lemma map_size : ∀A,B,f,b.|map A B f b| = |b|.
530#A#B#f#b elim b [//]
531*[2:#x]#l#r#Hil#Hir
532[ normalize >Hil >Hir @refl ]
533whd in match (map ????);
534inversion (map_opt ??? l)
535[2: #lo #ll #lr #_ #_ >andb_false_r normalize nodelta #EQl <EQl
536  whd in ⊢ (??%?); normalize nodelta >Hil >Hir % ]
537#EQl
538inversion (map_opt ??? r)
539[2,4: #ro #rl #rr #_ #_ >andb_false_r normalize nodelta #EQr <EQr <EQl
540  whd in ⊢ (??%?); normalize nodelta >Hil >Hir % ]
541#EQr normalize nodelta normalize
542<Hil <Hir whd in match map; normalize nodelta >EQl >EQr %
543qed.
544
545lemma lookup_opt_O_lt_size : ∀A,m,p. lookup_opt A p m ≠ None ? → 0 < |m|.
546#A#m elim m
547[#p normalize #F elim (absurd ? (refl ??) F)
548|* [2: #x]  #l #r #Hil #Hir * normalize
549  [1,2,3: //
550  |4:  #F elim (absurd ? (refl ??) F)]
551  #p #H [@(transitive_le … (Hir ? H)) | @(transitive_le … (Hil ? H))] //
552qed.
553
554lemma insert_size : ∀A,p,a,m. |insert A p a m| =
555  (match lookup_opt … p m with [Some _ ⇒ 0 | None ⇒ 1]) + |m|.
556#A#p elim p
557[ #a * [2: * [2: #x] #l #r] normalize //
558|*: #p #Hi #a * [2,4: * [2,4: #x] #l #r] normalize >Hi //
559] qed.
560
561(* Testing all of the entries with a boolean predicate, where the predicate
562   is given a proof that the entry is in the map. *)
563
564let 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 ≝
565match 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
566[ pm_leaf ⇒ λ_.λ_. true
567| pm_node a l r ⇒ λH,f.
568    pm_all_aux A m l (λx. pre (p0 x)) ? f ∧
569    ((match a return λa. (∀p. ? = lookup_opt A p (pm_node ? a ??)) → ? with [ None ⇒ λ_. true | Some a' ⇒ λH. f (pre one) a' ? ]) H) ∧
570    pm_all_aux A m r (λx. pre (p1 x)) ? f
571].
572[ >H %
573| #p >H %
574| #p >H %
575] qed.
576
577definition pm_all : ∀A. ∀m:positive_map A. (∀p,a. lookup_opt A p m = Some A a → bool) → bool ≝
578λA,m,f. pm_all_aux A m m (λx.x) (λp. refl ??) f.
579
580(* Proof irrelevance doesn't seem to apply to arbitrary variables, but we can
581   use the function graph to show that it's fine. *)
582   
583inductive 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 ≝
584| 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).
585
586lemma pm_all_pred_irr : ∀A,m,p,a,L,L'.
587 ∀f:∀p:Pos.∀a:A.lookup_opt A p m=Some A a→bool.
588 f p a L = f p a L'.
589#A #m #p #a #L #L' #f
590cut (pm_all_pred_graph A m p a L f (f p a L)) [ % ]
591cases (f p a L) #H cut (pm_all_pred_graph A m p a L' f ?) [2,5: @H | 1,4: skip]
592* //
593qed.
594
595lemma pm_all_aux_ok_aux : ∀A,m,t,pre,H,f,a,L.
596  pm_all_aux A m t pre H f →
597  lookup_opt A one t = Some A a →
598  f (pre one) a L.
599#A #m *
600[ #pre #H #f #a #L #H #L' normalize in L'; destruct
601| * [ #l #r #pre #H #f #a #L #H' #L' normalize in L'; destruct
602    | #a' #l #r #pre #H #f #a #L #AUX #L' normalize in L'; destruct
603      cases (andb_Prop_true … AUX) #AUX' cases (andb_Prop_true … AUX')
604      #_ #HERE #_ whd in HERE:(?%); @eq_true_to_b <HERE @pm_all_pred_irr
605    ]
606] qed.
607
608lemma pm_all_aux_ok : ∀A,m,t,pre,H,f.
609  bool_to_Prop (pm_all_aux A m t pre H f) ↔ (∀p,a,H. f (pre p) a H).
610#A #m #t #pre #H #f %
611[ #H' #p generalize in match pre in H H' ⊢ %; -pre generalize in match t; elim p
612  [ #t #pre #H #H' #a #L lapply (refl ? (Some A a)) <L in ⊢ (??%? → ?); >H @pm_all_aux_ok_aux //
613  | #q #IH * [ #pre #H #H' #a #L @⊥ >H in L; normalize #E destruct
614             | #x #l #r #pre #H #H' #a #L @(IH r)
615               [ #x >H % | cases (andb_Prop_true … H') #_ // ]
616             ]
617  | #q #IH * [ #pre #H #H' #a #L @⊥ >H in L; normalize #E destruct
618             | #x #l #r #pre #H #H' #a #L @(IH l)
619               [ #x >H % | cases (andb_Prop_true … H') #H'' cases (andb_Prop_true … H'') // ]
620             ]
621  ]
622| #H' generalize in match pre in H H' ⊢ %; -pre elim t
623  [ //
624  | * [2:#x] #l #r #IHl #IHr #pre #H #H' @andb_Prop
625    [ 1,3: @andb_Prop
626      [ 1,3: @IHl //
627      | @(H' one x)
628      | %
629      ]
630    | 2,4: @IHr //
631    ]
632  ]
633] qed.
634
635lemma pm_all_ok : ∀A,m,f.
636  bool_to_Prop (pm_all A m f) ↔ (∀p,a,H. f p a H).
637#A #m #f @pm_all_aux_ok
638qed.
639
640
641(* Attempt to choose an entry in the map, and if successful return the entry
642   and the map without it. *)
643
644let rec pm_choose (A:Type[0]) (t:positive_map A) on t : option (Pos × A × (positive_map A)) ≝
645match t with
646[ pm_leaf ⇒ None ?
647| pm_node a l r ⇒
648  match pm_choose A l with
649  [ None ⇒
650    match pm_choose A r with
651    [ None ⇒
652      match a with
653      [ None ⇒ None ?
654      | Some a ⇒ Some ? 〈〈one, a〉, pm_leaf A〉
655      ]
656    | Some x ⇒ Some ? 〈〈p1 (\fst (\fst x)), \snd (\fst x)〉, pm_node A a l (\snd x)〉
657    ]
658  | Some x ⇒ Some ? 〈〈p0 (\fst (\fst x)), \snd (\fst x)〉, pm_node A a (\snd x) r〉
659  ]
660].
661
662lemma pm_choose_empty : ∀A,t.
663  pm_choose A t = None ? ↔ ∀p. lookup_opt A p t = None A.
664#A #t elim t
665[ % //
666| *
667  [ #l #r * #IHl #IHl' * #IHr #IHr' %
668    [ #C *
669      [ %
670      | #p whd in C:(??%?) ⊢ (??%?);
671        @IHr cases (pm_choose A r) in C ⊢ %;
672        [ //
673        | #x normalize cases (pm_choose A l) [2: #y] normalize #E destruct
674        ]
675      | #p whd in C:(??%?) ⊢ (??%?);
676        @IHl cases (pm_choose A l) in C ⊢ %;
677        [ //
678        | #x normalize #E destruct
679        ]
680      ]
681    | #L whd in ⊢ (??%?); >IHl' [ normalize >IHr' [ % | #p @(L (p1 p)) ] | #p @(L (p0 p)) ]
682    ]
683  | #a #l #r #IHl #IHr %
684    [ normalize cases (pm_choose A l) [2: normalize #x #E destruct ]
685      normalize cases (pm_choose A r) [2: #x] normalize #E destruct
686    | #L lapply (L one) normalize #E destruct
687    ]
688  ]
689] qed.
690
691lemma pm_choose_empty_card : ∀A,t.
692  pm_choose A t = None ? ↔ |t| = 0.
693#A #t elim t
694[ /2/
695| * [ #l #r * #IHl #IHl' * #IHr #IHr' %
696      [ normalize lapply IHl cases (pm_choose A l) [2: #x #_ #E normalize in E; destruct ]
697        normalize lapply IHr cases (pm_choose A r) [2: #x #_ #_ #E normalize in E; destruct ]
698        #H1 #H2 #_ >(H1 (refl ??)) >(H2 (refl ??)) %
699      | normalize #CARD >IHl' [ >IHr' ] /2 by refl, le_n_O_to_eq/
700      ]
701    | #a #l #r #_ #_ % normalize
702      [ cases (pm_choose A l) [ cases (pm_choose A r) [ | #x ] | #x ]
703        #E normalize in E; destruct
704      | #E destruct
705      ]
706    ]
707] qed.
708
709lemma pm_choose_some : ∀A,t,p,a,t'.
710  pm_choose A t = Some ? 〈〈p,a〉,t'〉 →
711  lookup_opt A p t = Some A a ∧
712  lookup_opt A p t' = None A ∧
713  (∀q. p = q ∨ lookup_opt A q t = lookup_opt A q t') ∧
714  |t| = S (|t'|).
715#A #t elim t
716[ #p #a #t' normalize #E destruct
717| #ao #l #r #IHl #IHr *
718  [ #a #t' normalize
719    lapply (pm_choose_empty_card A l)
720    lapply (pm_choose_empty A l)
721    cases (pm_choose A l) normalize [2: #x #_ #_ #E destruct ] * #EMPl #EMPl' * #CARDl #CARDl'
722    lapply (pm_choose_empty_card A r)
723    lapply (pm_choose_empty A r)
724    cases (pm_choose A r) normalize [2: #x #_ #_ #E destruct ] * #EMPr #EMPr' * #CARDr #CARDr'
725    cases ao normalize [2:#x] #E destruct
726    % [ % /2/ * /2/ #q %2 whd in ⊢ (??%%); /2/ | >CARDl >CARDr // ]
727  | #p #a #t' normalize
728    lapply (pm_choose_empty_card A l)
729    lapply (pm_choose_empty A l)
730    cases (pm_choose A l) normalize [2: #x #_ #_ #E destruct ] * #EMPl #EMPl' * #CARDl #CARDl'
731    lapply (IHr p)
732    cases (pm_choose A r) normalize [ #_ cases ao [2:#a'] normalize #E destruct ]
733    * * #p' #a' #t'' #IH #E destruct
734    cases (IH ?? (refl ??)) * * #L1 #L2 #L3 #CARD
735    % [ % [ % [ // | @L2 ]| * /2/ #q cases (L3 q) /2/ #L4 %2 @L4 ] | cases ao normalize >CARD // ]
736  | #p #a #t' normalize
737    lapply (IHl p)
738    cases (pm_choose A l) normalize
739    [ #_ cases (pm_choose A r) normalize [ cases ao [2:#a'] normalize #E destruct
740      | #x #E destruct ]
741    |  * * #p' #a' #t'' #IH #E destruct
742      cases (IH ?? (refl ??)) * * #L1 #L2 #L3 #CARD
743      % [ % [ % [ // | @L2 ]| * /2/ #q cases (L3 q) /2/ #L4 %2 @L4 ] | cases ao normalize >CARD // ]
744    ]
745  ]
746] qed.
747
748(* Try to remove an element, return updated map if successful *)
749
750let rec pm_try_remove (A:Type[0]) (b:Pos) (t:positive_map A) on b : option (A × (positive_map A)) ≝
751match b with
752[ one ⇒
753    match t with
754    [ pm_leaf ⇒ None ?
755    | pm_node x l r ⇒ option_map ?? (λx. 〈x, pm_node A (None ?) l r〉) x
756    ]
757| p0 tl ⇒
758    match t with
759    [ pm_leaf ⇒ None ?
760    | pm_node x l r ⇒ option_map ?? (λxl. 〈\fst xl, pm_node A x (\snd xl) r〉) (pm_try_remove A tl l)
761    ]
762| p1 tl ⇒
763    match t with
764    [ pm_leaf ⇒ None ?
765    | pm_node x l r ⇒ option_map ?? (λxr. 〈\fst xr, pm_node A x l (\snd xr)〉) (pm_try_remove A tl r)
766    ]
767].
768
769lemma pm_try_remove_none : ∀A,b,t.
770  pm_try_remove A b t = None ? ↔ lookup_opt A b t = None ?.
771#A #b elim b
772[ * [ /2/ | * [ /2/ | #a #l #r % normalize #E destruct ] ]
773| #p #IH * [ /2/ | #x #l #r % normalize cases (IH r) cases (pm_try_remove A p r)
774  [ normalize #H #X @H | * #a #t' #_ normalize #_ #X destruct
775  | normalize // | * #a #t' normalize #A #B #C lapply (B C) #E destruct
776  ] ]
777| #p #IH * [ /2/ | #x #l #r % normalize cases (IH l) cases (pm_try_remove A p l)
778  [ normalize #H #X @H | * #a #t' #_ normalize #_ #X destruct
779  | normalize // | * #a #t' normalize #A #B #C lapply (B C) #E destruct
780  ] ]
781] qed.
782
783lemma pm_try_remove_some : ∀A,p,t,a,t'.
784  pm_try_remove A p t = Some ? 〈a,t'〉 →
785  lookup_opt A p t = Some A a ∧
786  lookup_opt A p t' = None A ∧
787  (∀q. p = q ∨ lookup_opt A q t = lookup_opt A q t') ∧
788  |t| = S (|t'|).
789#A #p elim p
790[ * [ #a #t' #E normalize in E; destruct
791    | * [ #l #r #a #t' #E normalize in E; destruct
792        | #a' #l #r #a #t' #E normalize in E; destruct % [ % [ % // | * /2/ ]| // ]
793        ]
794    ]
795| #p' #IH *
796  [ #a #t' #E normalize in E; destruct
797  | #x #l #r #a #t' whd in ⊢ (??%? → ?);
798    lapply (IH r) cases (pm_try_remove A p' r) [ #_ #E normalize in E; destruct ]
799    * #a' #r' #H #E whd in E:(??%?); destruct
800    cases (H a r' (refl ??)) * * #L1 #L2 #L3 #CARD
801    @conj try @conj try @conj
802    [ @L1 | @L2 | * /2/ #q cases (L3 q) [ /2/ | #E %2 @E ] | cases x normalize >CARD // ]
803  ]
804| #p' #IH *
805  [ #a #t' #E normalize in E; destruct
806  | #x #l #r #a #t' whd in ⊢ (??%? → ?);
807    lapply (IH l) cases (pm_try_remove A p' l) [ #_ #E normalize in E; destruct ]
808    * #a' #l' #H #E whd in E:(??%?); destruct
809    cases (H a l' (refl ??)) * * #L1 #L2 #L3 #CARD
810    @conj try @conj try @conj
811    [ @L1 | @L2 | * /2/ #q cases (L3 q) [ /2/ | #E %2 @E ] | cases x normalize >CARD // ]
812  ]
813] qed.
814
815lemma pm_try_remove_some' : ∀A,p,t,a.
816  lookup_opt A p t = Some A a →
817  ∃t'. pm_try_remove A p t = Some ? 〈a,t'〉.
818#A #p elim p
819[ * [ #a #L normalize in L; destruct
820    | #q #l #r #a #L normalize in L; destruct % [2: % | skip ]
821    ]
822| #q #IH *
823  [ #a #L normalize in L; destruct
824  | #x #l #r #a #L cases (IH r a L) #r' #R
825    % [2: whd in ⊢ (??%?); >R in ⊢ (??%?); % | skip ]
826  ]
827| #q #IH *
828  [ #a #L normalize in L; destruct
829  | #x #l #r #a #L cases (IH l a L) #l' #R
830    % [2: whd in ⊢ (??%?); >R in ⊢ (??%?); % | skip ]
831  ]
832] qed.
833
834(* An "informative" dependently typed fold *)
835
836let rec pm_fold_inf_aux
837 (A, B: Type[0])
838 (t: positive_map A)
839 (f: ∀p:Pos. ∀a:A. lookup_opt … p t = Some A a → B → B)
840 (t': positive_map A)
841 (pre: Pos → Pos)
842 (b: B) on t': (∀p. lookup_opt … p t' = lookup_opt … (pre p) t) → B ≝
843match t' return λt'. (∀p. lookup_opt A p t' = lookup_opt A (pre p) t) → B with
844[ pm_leaf ⇒ λ_. b
845| pm_node a l r ⇒ λH.
846    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
847    let b ≝ pm_fold_inf_aux A B t f l (λx. pre (p0 x)) b ? in
848            pm_fold_inf_aux A B t f r (λx. pre (p1 x)) b ?
849].
850[ #p @(H (p1 p)) | #p @(H (p0 p)) | <H % ]
851qed.
852
853definition pm_fold_inf : ∀A, B: Type[0]. ∀t: positive_map A.
854 ∀f: (∀p:Pos. ∀a:A. lookup_opt … p t = Some A a → B → B). B → B ≝
855  λA,B,t,f,b. pm_fold_inf_aux A B t f t (λx.x) b (λp. refl ??).
856
857(* Find an entry in the map matching the given predicate *)
858
859let rec pm_find_aux (pre: Pos → Pos) (A:Type[0]) (t: positive_map A) (p:Pos → A → bool) on t : option (Pos × A) ≝
860match t with
861[ pm_leaf ⇒ None ?
862| pm_node a l r ⇒
863  let x ≝ match a with
864  [ Some a ⇒ if p (pre one) a then Some ? 〈pre one, a〉 else None ?
865  | None ⇒ None ?
866  ] in
867  match x with
868  [ Some x ⇒ Some ? x
869  | None ⇒
870    match pm_find_aux (λx. pre (p0 x)) A l p with
871    [ None ⇒ pm_find_aux (λx. pre (p1 x)) A r p
872    | Some y ⇒ Some ? y
873    ]
874  ]
875].
876
877definition pm_find : ∀A:Type[0]. positive_map A → (Pos → A → bool) → option (Pos × A) ≝
878  pm_find_aux (λx.x).
879
880lemma pm_find_aux_pre : ∀A,t,pre,p,q,a.
881  pm_find_aux pre A t p = Some ? 〈q,a〉 →
882  ∃q'. q = pre q'.
883#A #t elim t
884[ normalize #pre #p #q #a #E destruct
885| * [2:#a] #l #r #IHl #IHr #pre #p #q #a' normalize
886  [ cases (p (pre one) a) normalize [ #E destruct /2/ ] ]
887  lapply (IHl (λx. pre (p0 x)) p)
888  cases (pm_find_aux ?? l ?)
889  [ 1,3: #_ normalize
890    lapply (IHr (λx. pre (p1 x)) p)
891    cases (pm_find_aux ?? r ?)
892    [ 1,3: #_ #E destruct
893    | *: * #q' #a'' #H #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/
894    ]
895  | *: * #q' #a'' #H normalize #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/
896  ]
897] qed.
898
899(* XXX: Hmm... destruct doesn't work properly with this, not sure why *)
900lemma option_pair_f_eq : ∀A,B:Type[0].∀a,a',b,b'. ∀f:A → A.
901  (∀a,a'. f a = f a' → a = a') →
902  Some (A×B) 〈f a,b〉 = Some ? 〈f a',b'〉 →
903  a = a' ∧ b = b'.
904#A #B #a #a' #b #b' #f #EXT #E
905cut (f a = f a') [ destruct (E) destruct (e0) @e2 (* WTF? *) ]
906#E' >(EXT … E') in E ⊢ %; #E destruct /2/
907qed.
908
909lemma pm_find_lookup : ∀A,p,q,a,t.
910  pm_find A t p = Some ? 〈q,a〉 →
911  lookup_opt A q t = Some ? a.
912#A #p #q #a normalize #t
913change with ((λx.x) q) in match q in ⊢ (% → ?);
914cut (∀y,z:Pos. (λx.x) y = (λx.x) z → y = z) //
915generalize in match q; -q generalize in match (λx.x);
916elim t
917[ #pre #q #_  normalize #E destruct
918| * [2:#a'] #l #r #IHl #IHr #pre #q #PRE
919  normalize [ cases (p (pre one) a') normalize [ #E cases (option_pair_f_eq … pre PRE E) #E1 #E2 destruct normalize % ] ]
920  lapply (IHl (λx.pre (p0 x)))
921  lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p)
922  cases (pm_find_aux ?? l ?)
923  [ 1,3: #_ #_ normalize
924    lapply (IHr (λx.pre (p1 x)))
925    lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p)
926    cases (pm_find_aux ?? r ?)
927    [ 1,3: #_ #_ #E destruct
928    | *: * #q' #a' #H1 #H2 #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct
929         whd in ⊢ (??%?); @H2 //
930         #y #z #E lapply (PRE … E) #E' destruct //
931    ]
932  | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct
933         whd in ⊢ (??%?); @H2 //
934         #y #z #E lapply (PRE … E) #E' destruct //
935  ]
936] qed.
937
938lemma pm_find_aux_none : ∀A,t,pre,p,q,a.
939  pm_find_aux pre A t p = None ? →
940  lookup_opt A q t = Some ? a →
941  ¬ p (pre q) a.
942#A #t elim t
943[ #pre #p #q #a #_ normalize #E destruct
944| #oa #l #r #IHl #IHr #pre #p *
945  [ #a cases oa
946    [ #_ normalize #E destruct
947    | #a' #F whd in F:(??%?); whd in F:(??match % with [_⇒?|_⇒?]?);
948      #E normalize in E; destruct
949      cases (p (pre one) a) in F ⊢ %; //
950      normalize #E destruct
951    ]
952  | #q #a #F #L @(IHr (λx. pre (p1 x)) p q a ? L)
953    whd in F:(??%?); cases oa in F;
954    [2: #a' normalize cases (p (pre one) a') [ normalize #E destruct ] ]
955    normalize cases (pm_find_aux ?? l p) normalize //
956    #x #E destruct
957  | #q #a #F #L @(IHl (λx. pre (p0 x)) p q a ? L)
958    whd in F:(??%?); cases oa in F;
959    [2: #a' normalize cases (p (pre one) a') [ normalize #E destruct ] ]
960    normalize cases (pm_find_aux ?? l p) normalize //
961  ]
962] qed.
963
964lemma pm_find_none : ∀A,t,p,q,a.
965  pm_find A t p = None ? →
966  lookup_opt A q t = Some ? a →
967  ¬ p q a.
968#A #t
969@(pm_find_aux_none A t (λx.x))
970qed.
971
972lemma pm_find_predicate : ∀A,t,p,q,a.
973  pm_find A t p = Some ? 〈q,a〉 →
974  p q a.
975#A #t #p normalize #q
976change with ((λx.x) q) in match q; generalize in match q; -q generalize in match (λx.x);
977elim t
978[ normalize #pre #q #a #E destruct
979| * [2:#a'] #l #r #IHl #IHr #pre #q #a normalize
980  [ lapply (refl ? (p (pre one) a')) cases (p (pre one) a') in ⊢ (???% → %);
981    [ #E normalize #E'
982      cut (pre one = pre q) [ destruct (E') destruct (e0) @e2 (* XXX ! *) ]
983      #E'' <E'' in E' ⊢ %; #E' destruct >E %
984    | #_ normalize
985    ]
986  ]
987  lapply (IHl (λx.pre (p0 x)))
988  lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p)
989  cases (pm_find_aux ?? l ?)
990  [ 1,3: #_ #_ normalize
991    lapply (IHr (λx.pre (p1 x)))
992    lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p)
993    cases (pm_find_aux ?? r ?)
994    [ 1,3: #_ #_ #E destruct
995    | *: * #q' #a' #H1 #H2 #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E %
996    ]
997  | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E %
998  ]
999] qed.
Note: See TracBrowser for help on using the repository browser.