source: src/common/PositiveMap.ma @ 2486

Last change on this file since 2486 was 2453, checked in by tranquil, 7 years ago

come changes in monad notation to

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