source: src/common/PositiveMap.ma @ 2548

Last change on this file since 2548 was 2541, checked in by tranquil, 7 years ago

adapted size notation to last matita lib update (01/12/2012)
that removed 'norm interpretation
Beware: will not work without updating matita's lib

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