source: src/common/PositiveMap.ma @ 2755

Last change on this file since 2755 was 2673, checked in by tranquil, 7 years ago

corrected some compilation errors (that might depend on some matita update)

File size: 32.0 KB
Line 
1include "basics/types.ma".
2include "utilities/binary/positive.ma".
3include "ASM/Util.ma". (* bool_to_Prop *)
4include "utilities/option.ma".
5
6inductive positive_map (A:Type[0]) : Type[0] ≝
7| pm_leaf : positive_map A
8| pm_node : option A → positive_map A → positive_map A → positive_map A.
9
10let rec lookup_opt (A:Type[0]) (b:Pos) (t:positive_map A) on t : option A ≝
11match t with
12[ pm_leaf ⇒ None ?
13| pm_node a l r ⇒
14    match b with
15    [ one ⇒ a
16    | p0 tl ⇒ lookup_opt A tl l
17    | p1 tl ⇒ lookup_opt A tl r
18    ]
19].
20
21definition lookup: ∀A:Type[0].Pos → positive_map A → A → A ≝ 
22 λA.λb.λt.λx.
23 match lookup_opt A b t with
24 [ None ⇒ x
25 | Some r ⇒ r
26 ].
27
28let rec pm_set (A:Type[0]) (b:Pos) (a:option A) (t:positive_map A) on b : positive_map A ≝
29match b with
30[ one ⇒
31    match t with
32    [ pm_leaf ⇒ pm_node A a (pm_leaf A) (pm_leaf A)
33    | pm_node _ l r ⇒ pm_node A a l r
34    ]
35| p0 tl ⇒
36    match t with
37    [ pm_leaf ⇒ pm_node A (None ?) (pm_set A tl a (pm_leaf A)) (pm_leaf A)
38    | pm_node x l r ⇒ pm_node A x (pm_set A tl a l) r
39    ]
40| p1 tl ⇒
41    match t with
42    [ pm_leaf ⇒ pm_node A (None ?) (pm_leaf A) (pm_set A tl a (pm_leaf A))
43    | pm_node x l r ⇒ pm_node A x l (pm_set A tl a r)
44    ]
45].
46
47definition insert : ∀A:Type[0]. Pos → A → positive_map A → positive_map A ≝
48λA,p,a. pm_set A p (Some ? a).
49
50let rec update (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : option (positive_map A) ≝
51match b with
52[ one ⇒
53    match t with
54    [ pm_leaf ⇒ None ?
55    | pm_node x l r ⇒ option_map ?? (λ_. pm_node A (Some ? a) l r) x
56    ]
57| p0 tl ⇒
58    match t with
59    [ pm_leaf ⇒ None ?
60    | pm_node x l r ⇒ option_map ?? (λl. pm_node A x l r) (update A tl a l)
61    ]
62| p1 tl ⇒
63    match t with
64    [ pm_leaf ⇒ None ?
65    | pm_node x l r ⇒ option_map ?? (λr. pm_node A x l r) (update A tl a r)
66    ]
67].
68
69lemma lookup_opt_pm_set_hit :
70 ∀A:Type[0].∀v:option A.∀b:Pos.∀t:positive_map A.
71  lookup_opt … b (pm_set … b v t) = v.
72#A #v #b elim b
73[ * //
74| #tl #IH *
75  [ whd in ⊢ (??%%); @IH
76  | #x #l #r @IH
77  ]
78| #tl #IH *
79  [ whd in ⊢ (??%%); @IH
80  | #x #l #r @IH
81  ]
82] qed.
83
84lemma lookup_opt_insert_hit :
85 ∀A:Type[0].∀v:A.∀b:Pos.∀t:positive_map A.
86  lookup_opt … b (insert … b v t) = Some A v.
87#A #v #b elim b
88[ * //
89| #tl #IH *
90  [ whd in ⊢ (??%%); @IH
91  | #x #l #r @IH
92  ]
93| #tl #IH *
94  [ whd in ⊢ (??%%); @IH
95  | #x #l #r @IH
96  ]
97] qed.
98
99lemma lookup_insert_hit:
100  ∀a: Type[0].
101  ∀v: a.
102  ∀b: Pos.
103  ∀t: positive_map a.
104  ∀d: a.
105    lookup … b (insert … b v t) d = v.
106#A #v #b #t #d whd in ⊢ (??%?); >lookup_opt_insert_hit %
107qed.
108
109lemma lookup_opt_pm_set_miss:
110 ∀A:Type[0].∀v:option A.∀b,c:Pos.∀t:positive_map A.
111  b ≠ c → lookup_opt … b (pm_set … c v t) = lookup_opt … b t.
112#A #v #b elim b
113[ * [ #t * #H elim (H (refl …))
114    | *: #c' #t #NE cases t //
115    ]
116| #b' #IH *
117  [ * [ #NE @refl | #x #l #r #NE @refl ]
118  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
119          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
120          ]
121  | #c' * //
122  ]
123| #b' #IH *
124  [ * [ #NE @refl | #x #l #r #NE @refl ]
125  | #c' * //
126  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
127          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
128          ]
129  ]
130] qed.
131
132lemma lookup_opt_insert_miss:
133 ∀A:Type[0].∀v:A.∀b,c:Pos.∀t:positive_map A.
134  b ≠ c → lookup_opt … b (insert … c v t) = lookup_opt … b t.
135#A #v #b elim b
136[ * [ #t * #H elim (H (refl …))
137    | *: #c' #t #NE cases t //
138    ]
139| #b' #IH *
140  [ * [ #NE @refl | #x #l #r #NE @refl ]
141  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
142          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
143          ]
144  | #c' * //
145  ]
146| #b' #IH *
147  [ * [ #NE @refl | #x #l #r #NE @refl ]
148  | #c' * //
149  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
150          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
151          ]
152  ]
153] qed.
154
155let rec fold (A, B: Type[0]) (f: Pos → A → B → B)
156 (t: positive_map A) (b: B) on t: B ≝
157match t with
158[ pm_leaf ⇒ b
159| pm_node a l r ⇒
160    let b ≝ match a with [ None ⇒ b | Some a ⇒ f one a b ] in
161    let b ≝ fold A B (λx.f (p0 x)) l b in
162            fold A B (λx.f (p1 x)) r b
163].   
164
165definition domain_of_pm : ∀A. positive_map A → positive_map unit ≝
166λA,t. fold A (positive_map unit) (λp,a,b. insert unit p it b) t (pm_leaf unit).
167
168(* Build some results about fold using domain_of_pm. *)
169
170lemma pm_fold_ignore_adding_junk : ∀A. ∀m. ∀f,g:Pos → Pos. ∀s.
171  (∀p,q. f p ≠ g q) →
172  ∀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.
173#A #m elim m
174[ normalize //
175| #oa #l #r #IHl #IHr
176  #f #g #s #not_g #p
177  normalize
178  >IHr
179  [ >IHl
180    [ cases oa
181      [ normalize %
182      | #a normalize >(lookup_opt_insert_miss ?? (f p)) [ % | @not_g ]
183      ]
184    | #x #y % #E cases (not_g x (p0 y)) #H @H @E
185    ]
186  | #x #y % #E cases (not_g x (p1 y)) #H @H @E
187  ]
188] qed.
189
190lemma pm_fold_ind_gen : ∀A,B,m,f,b.
191  ∀pre:Pos→Pos. (∀x,y.pre x = pre y → x = y) → ∀ps. (∀p. lookup_opt ? (pre p) ps = None ?) →
192  ∀P:B → positive_map unit → Prop.
193  P b ps →
194  (∀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)) →
195  P (fold A B (λx. f (pre x)) m b) (fold ?? (λp,a,b. insert unit (pre p) it b) m ps).
196#A #B #m elim m
197[ //
198| #oa #l #r #IHl #IHr
199  #f #b #pre #PRE #ps #PS #P #emp #step whd in ⊢ (?%%);
200  @IHr
201  [ #x #y #E lapply (PRE … E) #E' destruct //
202  | #p change with ((λx. pre (p1 x)) p) in match (pre (p1 p)); >pm_fold_ignore_adding_junk
203    [ cases oa [ @PS | #a >(lookup_opt_insert_miss ?? (pre (p1 p))) [ @PS | % #E lapply (PRE … E) #E' destruct ] ]
204    | #p #q % #E lapply (PRE … E) #E' destruct
205    ]
206  | @IHl
207    [ #x #y #E lapply (PRE … E) #E' destruct //
208    | #p cases oa [ @PS | #a >(lookup_opt_insert_miss ?? (pre (p0 p))) [ @PS | % #E lapply (PRE … E) #E' destruct ] ]
209    | cases oa in step ⊢ %; [ #_ @emp | #a #step normalize @step [ @PS | % | @emp ] ]
210    | #p #ps' #a #b' @step
211    ]
212  | #p #ps' #a #b' @step
213  ]
214] qed.
215
216lemma pm_fold_ext : ∀A,B,m,f,b.
217  fold A B f m b = fold A B (λx:Pos. f x) m b.
218#A #B #m elim m /4/
219qed.
220
221(* Main result about folds.  (Rather than producing a result about just the
222   domain of m we could use the whole mapping, but we'd need a function to
223   canonicalise maps because their representation can contain some junk.) *)
224
225lemma pm_fold_ind : ∀A,B,f,m,b. ∀P:B → positive_map unit → Prop.
226  P b (pm_leaf unit) →
227  (∀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)) →
228  P (fold A B f m b) (domain_of_pm A m).
229#A #B #f #m #b #P #emp #step
230>pm_fold_ext
231whd in ⊢ (??%);
232@(pm_fold_ind_gen A B m f b (λx.x) ? (pm_leaf unit) ???)
233[ //
234| //
235| @emp
236| @step
237] qed.
238
239lemma pm_fold_eq : ∀A,B,b,f.
240  (∀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)) →
241  ∀p,s1,s2.
242  lookup_opt B p s1 = lookup_opt B p s2 →
243  lookup_opt B p (fold A (positive_map B) f b s1) = lookup_opt B p (fold A (positive_map B) f b s2).
244#A #B #b elim b
245[ #f #H #p #s1 #s2 #H @H
246| #oa #l #r #IHl #IHr #f #H #p #s1 #s2 #H'
247  whd in match (fold ???? s1);
248  whd in match (fold ???? s2);
249  @IHr [ #q #k #a #s1' #s2' #H'' @H @H'' ]
250  @IHl [ #q #k #a #s1' #s2' #H'' @H @H'' ]
251  cases oa [ @H' | #a @H @H' ]
252] qed.
253
254
255lemma pm_fold_ignore_prefix : ∀A. ∀m. ∀pre:Pos → Pos. (∀x,y. pre x = pre y → x = y) →
256  ∀p. ∀pre'.
257      lookup_opt unit (pre p) (fold A ? (λx,a,b. insert unit (pre (pre' x)) it b) m (pm_leaf ?)) =
258      lookup_opt unit p (fold A ? (λx,a,b. insert unit (pre' x) it b) m (pm_leaf ?)).
259#A #m #pre #PRE
260cut (∀p. lookup_opt unit (pre p) (pm_leaf unit) = lookup_opt unit p (pm_leaf unit)) [ // ]
261generalize in match (pm_leaf unit) in ⊢ ((? → ??%?) → ? → ? → ??%?);
262generalize in match (pm_leaf unit);
263elim m
264[ #s1 #s2 #S #p #pre' @S
265| #oa #l #r #IHl #IHr
266  #s1 #s2 #S #p #pre'
267  whd in ⊢ (??(???%)(???%));
268  @(IHr ???? (λx. pre' (p1 x)))
269  #p' @IHl
270  #p'' cases oa
271  [ @S
272  | #a cases (decidable_eq_pos p'' (pre' one))
273    [ #E destruct
274      >(lookup_opt_insert_hit ?? (pre (pre' one)))
275      >(lookup_opt_insert_hit ?? (pre' one))
276      %
277    | #NE >(lookup_opt_insert_miss ??? (pre (pre' one)))
278      [ >(lookup_opt_insert_miss ??? (pre' one)) //
279      | % #E @(absurd … (PRE … E) NE)
280      ]
281    ]
282  ]
283] qed.
284
285(* Link the domain of a map (used in the result about fold) to the original
286   map. *)
287
288lemma domain_of_pm_present : ∀A,m,p.
289  lookup_opt A p m ≠ None ? ↔ lookup_opt unit p (domain_of_pm A m) ≠ None ?.
290
291#A #m whd in match (domain_of_pm ??);
292elim m
293[ #p normalize /3/
294| #oa #l #r #IHl #IHr
295  whd in match (fold ???? (pm_leaf unit));
296  *
297  [ change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?)));
298    >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ]
299    change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?)));
300    >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ]
301    cases oa
302    [ normalize /3/
303    | #a change with (insert unit one ??) in ⊢ (??(?(??(???%)?)));
304      >(lookup_opt_insert_hit ?? one) normalize
305      % #_ % #E destruct
306    ]
307  | #p >(pm_fold_eq ??????? (pm_leaf unit))
308    [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ]
309      @IHr
310    | >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ]
311      cases oa
312      [ %
313      | #a >(lookup_opt_insert_miss ?? (p1 p)) [2: % #E destruct ]
314        %
315      ]
316    | #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p1 y))
317      [ #E destruct
318        >(lookup_opt_insert_hit ?? (p1 y))
319        >(lookup_opt_insert_hit ?? (p1 y))
320        %
321      | #NE >(lookup_opt_insert_miss ?? x … NE)
322        >(lookup_opt_insert_miss ?? x … NE)
323        @S
324      ]
325    ] 
326  | #p
327    >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ]
328    >(pm_fold_eq ??????? (pm_leaf unit))
329    [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ]
330      @IHl
331    | cases oa
332      [ %
333      | #a >(lookup_opt_insert_miss ?? (p0 p)) [2: % #E destruct ]
334        %
335      ]
336    | #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p0 y))
337      [ #E destruct
338        >(lookup_opt_insert_hit ?? (p0 y))
339        >(lookup_opt_insert_hit ?? (p0 y))
340        %
341      | #NE >(lookup_opt_insert_miss ?? x … NE)
342        >(lookup_opt_insert_miss ?? x … NE)
343        @S
344      ]
345    ]
346  ]
347] qed.
348
349
350lemma update_fail : ∀A,b,a,t.
351  update A b a t = None ? →
352  lookup_opt A b t = None ?.
353#A #b #a elim b
354[ * [ // | * // #x #l #r normalize #E destruct ]
355| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
356                   cases (update A b' a r) in U ⊢ %;
357                   [ // | normalize #t #E destruct ]
358            ]
359| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
360                   cases (update A b' a l) in U ⊢ %;
361                   [ // | normalize #t #E destruct ]
362            ]
363] qed.
364
365lemma update_lookup_opt_same : ∀A,b,a,t,t'.
366  update A b a t = Some ? t' →
367  lookup_opt A b t' = Some ? a.
368#A #b #a elim b
369[ * [ #t' normalize #E destruct
370    | * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?);
371      #E destruct //
372    ]
373| #b' #IH *
374  [ #t' normalize #E destruct
375  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
376    lapply (IH r)
377    cases (update A b' a r)
378    [ #_ normalize #E destruct
379    | #r' #H normalize #E destruct @H @refl
380    ]
381  ]
382| #b' #IH *
383  [ #t' normalize #E destruct
384  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
385    lapply (IH l)
386    cases (update A b' a l)
387    [ #_ normalize #E destruct
388    | #r' #H normalize #E destruct @H @refl
389    ]
390  ]
391] qed.
392
393lemma update_lookup_opt_other : ∀A,b,a,t,t'.
394  update A b a t = Some ? t' →
395  ∀b'. b ≠ b' →
396  lookup_opt A b' t = lookup_opt A b' t'.
397#A #b #a elim b
398[ * [ #t' normalize #E destruct
399    | * [2: #x] #l #r #t' normalize #E destruct
400      * [ * #H elim (H (refl …)) ]
401      #tl #NE normalize //
402    ]
403| #b' #IH *
404  [ #t' normalize #E destruct
405  | #x #l #r #t' normalize
406    lapply (IH r)
407    cases (update A b' a r)
408    [ #_ normalize #E destruct
409    | #t'' #H normalize #E destruct * // #b'' #NE @H /2/
410    ]
411  ]
412| #b' #IH *
413  [ #t' normalize #E destruct
414  | #x #l #r #t' normalize
415    lapply (IH l)
416    cases (update A b' a l)
417    [ #_ normalize #E destruct
418    | #t'' #H normalize #E destruct * // #b'' #NE @H /2/
419    ]
420  ]
421] qed.
422
423definition is_none : ∀A.option A → bool ≝ λA,o.match o with [ None ⇒ true | _ ⇒ false ].
424definition is_pm_leaf : ∀A.positive_map A → bool ≝ λA,m.match m with [ pm_leaf ⇒ true | _ ⇒ false ].
425
426let rec map_opt A B (f : A → option B) (b : positive_map A) on b : positive_map B ≝
427match b with
428[ pm_leaf ⇒ pm_leaf ?
429| pm_node a l r ⇒
430  let a' ≝ !x ← a ; f x in
431  let l' ≝ map_opt ?? f l in
432  let r' ≝ map_opt ?? f r in
433  if is_none … a' ∧ is_pm_leaf … l' ∧ is_pm_leaf … r' then
434    pm_leaf ?
435  else
436    pm_node ? a' l' r'
437].
438
439definition map ≝ λA,B,f.map_opt A B (λx. Some ? (f x)).
440
441lemma andb_false_r : ∀b.(b∧false)=false. *% qed.
442
443lemma lookup_opt_map : ∀A,B,f,b,p.
444  lookup_opt … p (map_opt A B f b) = ! x ← lookup_opt … p b ; f x.
445#A#B#f#b elim b [//]
446#a #l #r #IHl #IHr * [2,3: #p ]
447whd in match (map_opt ????); whd in match (lookup_opt ???) in ⊢ (???%);
448[3: cases (! x ← a ; f x) [2: #x] try % cases (?∧?) % ]
449inversion (map_opt ??? l)
450[2,4: #lo #ll #lr #_ #_ >andb_false_r normalize nodelta #EQl <EQl
451  whd in ⊢ (??%?); // ]
452#EQl
453inversion (map_opt ??? r)
454[2,4: #ro #rl #rr #_ #_ >andb_false_r normalize nodelta #EQr <EQr <EQl
455  whd in ⊢ (??%?); // ]
456#EQr
457[ <IHr >EQr | <IHl >EQl ] cases (?∧?) %
458qed.
459
460(*
461lemma map_opt_id_eq_ext : ∀A,m,f.(∀x.f x = Some ? x) → map_opt A A f m = m.
462#A #m #f #Hf elim m [//]
463* [2:#x] #l #r #Hil #Hir normalize [>Hf] //
464qed.
465
466lemma map_opt_id : ∀A,m.map_opt A A (λx. Some ? x) m = m.
467#A #m @map_opt_id_eq_ext //
468qed.
469*)
470
471let rec merge A B C (choice : option A → option B → option C)
472  (a : positive_map A) (b : positive_map B) on a : positive_map C ≝
473match a with
474[ pm_leaf ⇒ map_opt ?? (λx.choice (None ?) (Some ? x)) b
475| pm_node o l r ⇒
476  match b with
477  [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a
478  | pm_node o' l' r' ⇒
479    let o'' ≝ choice o o' in
480    let l'' ≝ merge … choice l l' in
481    let r'' ≝ merge … choice r r' in
482    if is_none … o'' ∧ is_pm_leaf … l'' ∧ is_pm_leaf … r'' then
483      pm_leaf ?
484    else
485      pm_node ? o'' l'' r''
486  ]
487].
488
489lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p.
490  choice (None ?) (None ?) = None ? →
491  lookup_opt … p (merge A B C choice a b) =
492    choice (lookup_opt … p a) (lookup_opt … p b).
493 #A#B#C#choice#a elim a -a
494[ #b
495| #o#l#r#Hil#Hir * [2: #o'#l'#r' * [2,3: #x] normalize cases(choice o o') normalize /2 by /
496  [3: cases (merge A B C choice l l') normalize /2 by / cases(merge A B C choice r r')
497      normalize /2 by /
498  |*: #H [<Hir|<Hil] /2 by / cases(merge A B C choice l l') normalize /2 by /
499      cases (merge A B C choice r r') normalize /2 by /
500  ]
501]]
502#p #choice_good >lookup_opt_map
503elim (lookup_opt ???)
504normalize //
505qed.
506
507let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝
508match b with
509[ pm_leaf ⇒ 0
510| pm_node a l r ⇒
511  (match a with
512   [ Some _ ⇒ 1
513   | None ⇒ 0
514   ]) + domain_size A l + domain_size A r
515].
516
517interpretation "positive map size" 'card p = (domain_size ? p).
518
519(*
520lemma map_opt_size : ∀A,B,f,b.|map_opt A B f b| ≤ |b|.
521#A#B#f#b elim b [//]
522*[2:#x]#l#r#Hil#Hir normalize
523[elim (f ?) normalize [@(transitive_le ? ? ? ? (le_n_Sn ?)) | #y @le_S_S ] ]
524@le_plus assumption
525qed.
526*)
527
528lemma map_size : ∀A,B,f,b.|map A B f b| = |b|.
529#A#B#f#b elim b [//]
530*[2:#x]#l#r#Hil#Hir
531[ normalize >Hil >Hir @refl ]
532whd in match (map ????);
533inversion (map_opt ??? l)
534[2: #lo #ll #lr #_ #_ >andb_false_r normalize nodelta #EQl <EQl
535  whd in ⊢ (??%?); normalize nodelta >Hil >Hir % ]
536#EQl
537inversion (map_opt ??? r)
538[2,4: #ro #rl #rr #_ #_ >andb_false_r normalize nodelta #EQr <EQr <EQl
539  whd in ⊢ (??%?); normalize nodelta >Hil >Hir % ]
540#EQr normalize nodelta normalize
541<Hil <Hir whd in match map; normalize nodelta >EQl >EQr %
542qed.
543
544lemma lookup_opt_O_lt_size : ∀A,m,p. lookup_opt A p m ≠ None ? → 0 < |m|.
545#A#m elim m
546[#p normalize #F elim (absurd ? (refl ??) F)
547|* [2: #x]  #l #r #Hil #Hir * normalize
548  [1,2,3: //
549  |4:  #F elim (absurd ? (refl ??) F)]
550  #p #H [@(transitive_le … (Hir ? H)) | @(transitive_le … (Hil ? H))] //
551qed.
552
553lemma insert_size : ∀A,p,a,m. |insert A p a m| =
554  (match lookup_opt … p m with [Some _ ⇒ 0 | None ⇒ 1]) + |m|.
555#A#p elim p
556[ #a * [2: * [2: #x] #l #r] normalize //
557|*: #p #Hi #a * [2,4: * [2,4: #x] #l #r] normalize >Hi //
558] qed.
559
560(* Testing all of the entries with a boolean predicate, where the predicate
561   is given a proof that the entry is in the map. *)
562
563let 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 ≝
564match 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
565[ pm_leaf ⇒ λ_.λ_. true
566| pm_node a l r ⇒ λH,f.
567    pm_all_aux A m l (λx. pre (p0 x)) ? f ∧
568    ((match a return λa. (∀p. ? = lookup_opt A p (pm_node ? a ??)) → ? with [ None ⇒ λ_. true | Some a' ⇒ λH. f (pre one) a' ? ]) H) ∧
569    pm_all_aux A m r (λx. pre (p1 x)) ? f
570].
571[ >H %
572| #p >H %
573| #p >H %
574] qed.
575
576definition pm_all : ∀A. ∀m:positive_map A. (∀p,a. lookup_opt A p m = Some A a → bool) → bool ≝
577λA,m,f. pm_all_aux A m m (λx.x) (λp. refl ??) f.
578
579(* Proof irrelevance doesn't seem to apply to arbitrary variables, but we can
580   use the function graph to show that it's fine. *)
581   
582inductive 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 ≝
583| 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).
584
585lemma pm_all_pred_irr : ∀A,m,p,a,L,L'.
586 ∀f:∀p:Pos.∀a:A.lookup_opt A p m=Some A a→bool.
587 f p a L = f p a L'.
588#A #m #p #a #L #L' #f
589cut (pm_all_pred_graph A m p a L f (f p a L)) [ % ]
590cases (f p a L) #H cut (pm_all_pred_graph A m p a L' f ?) [2,5: @H | 1,4: skip]
591* //
592qed.
593
594lemma pm_all_aux_ok_aux : ∀A,m,t,pre,H,f,a,L.
595  pm_all_aux A m t pre H f →
596  lookup_opt A one t = Some A a →
597  f (pre one) a L.
598#A #m *
599[ #pre #H #f #a #L #H #L' normalize in L'; destruct
600| * [ #l #r #pre #H #f #a #L #H' #L' normalize in L'; destruct
601    | #a' #l #r #pre #H #f #a #L #AUX #L' normalize in L'; destruct
602      cases (andb_Prop_true … AUX) #AUX' cases (andb_Prop_true … AUX')
603      #_ #HERE #_ whd in HERE:(?%); @eq_true_to_b <HERE @pm_all_pred_irr
604    ]
605] qed.
606
607lemma pm_all_aux_ok : ∀A,m,t,pre,H,f.
608  bool_to_Prop (pm_all_aux A m t pre H f) ↔ (∀p,a,H. f (pre p) a H).
609#A #m #t #pre #H #f %
610[ #H' #p generalize in match pre in H H' ⊢ %; -pre generalize in match t; elim p
611  [ #t #pre #H #H' #a #L lapply (refl ? (Some A a)) <L in ⊢ (??%? → ?); >H @pm_all_aux_ok_aux //
612  | #q #IH * [ #pre #H #H' #a #L @⊥ >H in L; normalize #E destruct
613             | #x #l #r #pre #H #H' #a #L @(IH r)
614               [ #x >H % | cases (andb_Prop_true … H') #_ // ]
615             ]
616  | #q #IH * [ #pre #H #H' #a #L @⊥ >H in L; normalize #E destruct
617             | #x #l #r #pre #H #H' #a #L @(IH l)
618               [ #x >H % | cases (andb_Prop_true … H') #H'' cases (andb_Prop_true … H'') // ]
619             ]
620  ]
621| #H' generalize in match pre in H H' ⊢ %; -pre elim t
622  [ //
623  | * [2:#x] #l #r #IHl #IHr #pre #H #H' @andb_Prop
624    [ 1,3: @andb_Prop
625      [ 1,3: @IHl //
626      | @(H' one x)
627      | %
628      ]
629    | 2,4: @IHr //
630    ]
631  ]
632] qed.
633
634lemma pm_all_ok : ∀A,m,f.
635  bool_to_Prop (pm_all A m f) ↔ (∀p,a,H. f p a H).
636#A #m #f @pm_all_aux_ok
637qed.
638
639
640(* Attempt to choose an entry in the map, and if successful return the entry
641   and the map without it. *)
642
643let rec pm_choose (A:Type[0]) (t:positive_map A) on t : option (Pos × A × (positive_map A)) ≝
644match t with
645[ pm_leaf ⇒ None ?
646| pm_node a l r ⇒
647  match pm_choose A l with
648  [ None ⇒
649    match pm_choose A r with
650    [ None ⇒
651      match a with
652      [ None ⇒ None ?
653      | Some a ⇒ Some ? 〈〈one, a〉, pm_leaf A〉
654      ]
655    | Some x ⇒ Some ? 〈〈p1 (\fst (\fst x)), \snd (\fst x)〉, pm_node A a l (\snd x)〉
656    ]
657  | Some x ⇒ Some ? 〈〈p0 (\fst (\fst x)), \snd (\fst x)〉, pm_node A a (\snd x) r〉
658  ]
659].
660
661lemma pm_choose_empty : ∀A,t.
662  pm_choose A t = None ? ↔ ∀p. lookup_opt A p t = None A.
663#A #t elim t
664[ % //
665| *
666  [ #l #r * #IHl #IHl' * #IHr #IHr' %
667    [ #C *
668      [ %
669      | #p whd in C:(??%?) ⊢ (??%?);
670        @IHr cases (pm_choose A r) in C ⊢ %;
671        [ //
672        | #x normalize cases (pm_choose A l) [2: #y] normalize #E destruct
673        ]
674      | #p whd in C:(??%?) ⊢ (??%?);
675        @IHl cases (pm_choose A l) in C ⊢ %;
676        [ //
677        | #x normalize #E destruct
678        ]
679      ]
680    | #L whd in ⊢ (??%?); >IHl' [ normalize >IHr' [ % | #p @(L (p1 p)) ] | #p @(L (p0 p)) ]
681    ]
682  | #a #l #r #IHl #IHr %
683    [ normalize cases (pm_choose A l) [2: normalize #x #E destruct ]
684      normalize cases (pm_choose A r) [2: #x] normalize #E destruct
685    | #L lapply (L one) normalize #E destruct
686    ]
687  ]
688] qed.
689
690lemma pm_choose_empty_card : ∀A,t.
691  pm_choose A t = None ? ↔ |t| = 0.
692#A #t elim t
693[ /2/
694| * [ #l #r * #IHl #IHl' * #IHr #IHr' %
695      [ normalize lapply IHl cases (pm_choose A l) [2: #x #_ #E normalize in E; destruct ]
696        normalize lapply IHr cases (pm_choose A r) [2: #x #_ #_ #E normalize in E; destruct ]
697        #H1 #H2 #_ >(H1 (refl ??)) >(H2 (refl ??)) %
698      | normalize #CARD >IHl' [ >IHr' ] /2 by refl, le_n_O_to_eq/
699      ]
700    | #a #l #r #_ #_ % normalize
701      [ cases (pm_choose A l) [ cases (pm_choose A r) [ | #x ] | #x ]
702        #E normalize in E; destruct
703      | #E destruct
704      ]
705    ]
706] qed.
707
708lemma pm_choose_some : ∀A,t,p,a,t'.
709  pm_choose A t = Some ? 〈〈p,a〉,t'〉 →
710  lookup_opt A p t = Some A a ∧
711  lookup_opt A p t' = None A ∧
712  (∀q. p = q ∨ lookup_opt A q t = lookup_opt A q t') ∧
713  |t| = S (|t'|).
714#A #t elim t
715[ #p #a #t' normalize #E destruct
716| #ao #l #r #IHl #IHr *
717  [ #a #t' normalize
718    lapply (pm_choose_empty_card A l)
719    lapply (pm_choose_empty A l)
720    cases (pm_choose A l) normalize [2: #x #_ #_ #E destruct ] * #EMPl #EMPl' * #CARDl #CARDl'
721    lapply (pm_choose_empty_card A r)
722    lapply (pm_choose_empty A r)
723    cases (pm_choose A r) normalize [2: #x #_ #_ #E destruct ] * #EMPr #EMPr' * #CARDr #CARDr'
724    cases ao normalize [2:#x] #E destruct
725    % [ % /2/ * /2/ #q %2 whd in ⊢ (??%%); /2/ | >CARDl >CARDr // ]
726  | #p #a #t' normalize
727    lapply (pm_choose_empty_card A l)
728    lapply (pm_choose_empty A l)
729    cases (pm_choose A l) normalize [2: #x #_ #_ #E destruct ] * #EMPl #EMPl' * #CARDl #CARDl'
730    lapply (IHr p)
731    cases (pm_choose A r) normalize [ #_ cases ao [2:#a'] normalize #E destruct ]
732    * * #p' #a' #t'' #IH #E destruct
733    cases (IH ?? (refl ??)) * * #L1 #L2 #L3 #CARD
734    % [ % [ % [ // | @L2 ]| * /2/ #q cases (L3 q) /2/ #L4 %2 @L4 ] | cases ao normalize >CARD // ]
735  | #p #a #t' normalize
736    lapply (IHl p)
737    cases (pm_choose A l) normalize
738    [ #_ cases (pm_choose A r) normalize [ cases ao [2:#a'] normalize #E destruct
739      | #x #E destruct ]
740    |  * * #p' #a' #t'' #IH #E destruct
741      cases (IH ?? (refl ??)) * * #L1 #L2 #L3 #CARD
742      % [ % [ % [ // | @L2 ]| * /2/ #q cases (L3 q) /2/ #L4 %2 @L4 ] | cases ao normalize >CARD // ]
743    ]
744  ]
745] qed.
746
747(* Try to remove an element, return updated map if successful *)
748
749let rec pm_try_remove (A:Type[0]) (b:Pos) (t:positive_map A) on b : option (A × (positive_map A)) ≝
750match b with
751[ one ⇒
752    match t with
753    [ pm_leaf ⇒ None ?
754    | pm_node x l r ⇒ option_map ?? (λx. 〈x, pm_node A (None ?) l r〉) x
755    ]
756| p0 tl ⇒
757    match t with
758    [ pm_leaf ⇒ None ?
759    | pm_node x l r ⇒ option_map ?? (λxl. 〈\fst xl, pm_node A x (\snd xl) r〉) (pm_try_remove A tl l)
760    ]
761| p1 tl ⇒
762    match t with
763    [ pm_leaf ⇒ None ?
764    | pm_node x l r ⇒ option_map ?? (λxr. 〈\fst xr, pm_node A x l (\snd xr)〉) (pm_try_remove A tl r)
765    ]
766].
767
768lemma pm_try_remove_none : ∀A,b,t.
769  pm_try_remove A b t = None ? ↔ lookup_opt A b t = None ?.
770#A #b elim b
771[ * [ /2/ | * [ /2/ | #a #l #r % normalize #E destruct ] ]
772| #p #IH * [ /2/ | #x #l #r % normalize cases (IH r) cases (pm_try_remove A p r)
773  [ normalize #H #X @H | * #a #t' #_ normalize #_ #X destruct
774  | normalize // | * #a #t' normalize #A #B #C lapply (B C) #E destruct
775  ] ]
776| #p #IH * [ /2/ | #x #l #r % normalize cases (IH l) cases (pm_try_remove A p l)
777  [ normalize #H #X @H | * #a #t' #_ normalize #_ #X destruct
778  | normalize // | * #a #t' normalize #A #B #C lapply (B C) #E destruct
779  ] ]
780] qed.
781
782lemma pm_try_remove_some : ∀A,p,t,a,t'.
783  pm_try_remove A p t = Some ? 〈a,t'〉 →
784  lookup_opt A p t = Some A a ∧
785  lookup_opt A p t' = None A ∧
786  (∀q. p = q ∨ lookup_opt A q t = lookup_opt A q t') ∧
787  |t| = S (|t'|).
788#A #p elim p
789[ * [ #a #t' #E normalize in E; destruct
790    | * [ #l #r #a #t' #E normalize in E; destruct
791        | #a' #l #r #a #t' #E normalize in E; destruct % [ % [ % // | * /2/ ]| // ]
792        ]
793    ]
794| #p' #IH *
795  [ #a #t' #E normalize in E; destruct
796  | #x #l #r #a #t' whd in ⊢ (??%? → ?);
797    lapply (IH r) cases (pm_try_remove A p' r) [ #_ #E normalize in E; destruct ]
798    * #a' #r' #H #E whd in E:(??%?); destruct
799    cases (H a r' (refl ??)) * * #L1 #L2 #L3 #CARD
800    @conj try @conj try @conj
801    [ @L1 | @L2 | * /2/ #q cases (L3 q) [ /2/ | #E %2 @E ] | cases x normalize >CARD // ]
802  ]
803| #p' #IH *
804  [ #a #t' #E normalize in E; destruct
805  | #x #l #r #a #t' whd in ⊢ (??%? → ?);
806    lapply (IH l) cases (pm_try_remove A p' l) [ #_ #E normalize in E; destruct ]
807    * #a' #l' #H #E whd in E:(??%?); destruct
808    cases (H a l' (refl ??)) * * #L1 #L2 #L3 #CARD
809    @conj try @conj try @conj
810    [ @L1 | @L2 | * /2/ #q cases (L3 q) [ /2/ | #E %2 @E ] | cases x normalize >CARD // ]
811  ]
812] qed.
813
814lemma pm_try_remove_some' : ∀A,p,t,a.
815  lookup_opt A p t = Some A a →
816  ∃t'. pm_try_remove A p t = Some ? 〈a,t'〉.
817#A #p elim p
818[ * [ #a #L normalize in L; destruct
819    | #q #l #r #a #L normalize in L; destruct % [2: % | skip ]
820    ]
821| #q #IH *
822  [ #a #L normalize in L; destruct
823  | #x #l #r #a #L cases (IH r a L) #r' #R
824    % [2: whd in ⊢ (??%?); >R in ⊢ (??%?); % | skip ]
825  ]
826| #q #IH *
827  [ #a #L normalize in L; destruct
828  | #x #l #r #a #L cases (IH l a L) #l' #R
829    % [2: whd in ⊢ (??%?); >R in ⊢ (??%?); % | skip ]
830  ]
831] qed.
832
833(* An "informative" dependently typed fold *)
834
835let rec pm_fold_inf_aux
836 (A, B: Type[0])
837 (t: positive_map A)
838 (f: ∀p:Pos. ∀a:A. lookup_opt … p t = Some A a → B → B)
839 (t': positive_map A)
840 (pre: Pos → Pos)
841 (b: B) on t': (∀p. lookup_opt … p t' = lookup_opt … (pre p) t) → B ≝
842match t' return λt'. (∀p. lookup_opt A p t' = lookup_opt A (pre p) t) → B with
843[ pm_leaf ⇒ λ_. b
844| pm_node a l r ⇒ λH.
845    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
846    let b ≝ pm_fold_inf_aux A B t f l (λx. pre (p0 x)) b ? in
847            pm_fold_inf_aux A B t f r (λx. pre (p1 x)) b ?
848].
849[ #p @(H (p1 p)) | #p @(H (p0 p)) | <H % ]
850qed.
851
852definition pm_fold_inf : ∀A, B: Type[0]. ∀t: positive_map A.
853 ∀f: (∀p:Pos. ∀a:A. lookup_opt … p t = Some A a → B → B). B → B ≝
854  λA,B,t,f,b. pm_fold_inf_aux A B t f t (λx.x) b (λp. refl ??).
855
856(* Find an entry in the map matching the given predicate *)
857
858let rec pm_find_aux (pre: Pos → Pos) (A:Type[0]) (t: positive_map A) (p:Pos → A → bool) on t : option (Pos × A) ≝
859match t with
860[ pm_leaf ⇒ None ?
861| pm_node a l r ⇒
862  let x ≝ match a with
863  [ Some a ⇒ if p (pre one) a then Some ? 〈pre one, a〉 else None ?
864  | None ⇒ None ?
865  ] in
866  match x with
867  [ Some x ⇒ Some ? x
868  | None ⇒
869    match pm_find_aux (λx. pre (p0 x)) A l p with
870    [ None ⇒ pm_find_aux (λx. pre (p1 x)) A r p
871    | Some y ⇒ Some ? y
872    ]
873  ]
874].
875
876definition pm_find : ∀A:Type[0]. positive_map A → (Pos → A → bool) → option (Pos × A) ≝
877  pm_find_aux (λx.x).
878
879lemma pm_find_aux_pre : ∀A,t,pre,p,q,a.
880  pm_find_aux pre A t p = Some ? 〈q,a〉 →
881  ∃q'. q = pre q'.
882#A #t elim t
883[ normalize #pre #p #q #a #E destruct
884| * [2:#a] #l #r #IHl #IHr #pre #p #q #a' normalize
885  [ cases (p (pre one) a) normalize [ #E destruct /2/ ] ]
886  lapply (IHl (λx. pre (p0 x)) p)
887  cases (pm_find_aux ?? l ?)
888  [ 1,3: #_ normalize
889    lapply (IHr (λx. pre (p1 x)) p)
890    cases (pm_find_aux ?? r ?)
891    [ 1,3: #_ #E destruct
892    | *: * #q' #a'' #H #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/
893    ]
894  | *: * #q' #a'' #H normalize #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/
895  ]
896] qed.
897
898(* XXX: Hmm... destruct doesn't work properly with this, not sure why *)
899lemma option_pair_f_eq : ∀A,B:Type[0].∀a,a',b,b'. ∀f:A → A.
900  (∀a,a'. f a = f a' → a = a') →
901  Some (A×B) 〈f a,b〉 = Some ? 〈f a',b'〉 →
902  a = a' ∧ b = b'.
903#A #B #a #a' #b #b' #f #EXT #E
904cut (f a = f a') [ destruct (E) destruct (e0) @e2 (* WTF? *) ]
905#E' >(EXT … E') in E ⊢ %; #E destruct /2/
906qed.
907
908lemma pm_find_lookup : ∀A,p,q,a,t.
909  pm_find A t p = Some ? 〈q,a〉 →
910  lookup_opt A q t = Some ? a.
911#A #p #q #a normalize #t
912change with ((λx.x) q) in match q in ⊢ (% → ?);
913cut (∀y,z:Pos. (λx.x) y = (λx.x) z → y = z) //
914generalize in match q; -q generalize in match (λx.x);
915elim t
916[ #pre #q #_  normalize #E destruct
917| * [2:#a'] #l #r #IHl #IHr #pre #q #PRE
918  normalize [ cases (p (pre one) a') normalize [ #E cases (option_pair_f_eq … pre PRE E) #E1 #E2 destruct normalize % ] ]
919  lapply (IHl (λx.pre (p0 x)))
920  lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p)
921  cases (pm_find_aux ?? l ?)
922  [ 1,3: #_ #_ normalize
923    lapply (IHr (λx.pre (p1 x)))
924    lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p)
925    cases (pm_find_aux ?? r ?)
926    [ 1,3: #_ #_ #E destruct
927    | *: * #q' #a' #H1 #H2 #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct
928         whd in ⊢ (??%?); @H2 //
929         #y #z #E lapply (PRE … E) #E' destruct //
930    ]
931  | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct
932         whd in ⊢ (??%?); @H2 //
933         #y #z #E lapply (PRE … E) #E' destruct //
934  ]
935] qed.
936
937lemma pm_find_aux_none : ∀A,t,pre,p,q,a.
938  pm_find_aux pre A t p = None ? →
939  lookup_opt A q t = Some ? a →
940  ¬ p (pre q) a.
941#A #t elim t
942[ #pre #p #q #a #_ normalize #E destruct
943| #oa #l #r #IHl #IHr #pre #p *
944  [ #a cases oa
945    [ #_ normalize #E destruct
946    | #a' #F whd in F:(??%?); whd in F:(??match % with [_⇒?|_⇒?]?);
947      #E normalize in E; destruct
948      cases (p (pre one) a) in F ⊢ %; //
949      normalize #E destruct
950    ]
951  | #q #a #F #L @(IHr (λx. pre (p1 x)) p q a ? L)
952    whd in F:(??%?); cases oa in F;
953    [2: #a' normalize cases (p (pre one) a') [ normalize #E destruct ] ]
954    normalize cases (pm_find_aux ?? l p) normalize //
955    #x #E destruct
956  | #q #a #F #L @(IHl (λx. pre (p0 x)) p q a ? L)
957    whd in F:(??%?); cases oa in F;
958    [2: #a' normalize cases (p (pre one) a') [ normalize #E destruct ] ]
959    normalize cases (pm_find_aux ?? l p) normalize //
960  ]
961] qed.
962
963lemma pm_find_none : ∀A,t,p,q,a.
964  pm_find A t p = None ? →
965  lookup_opt A q t = Some ? a →
966  ¬ p q a.
967#A #t
968@(pm_find_aux_none A t (λx.x))
969qed.
970
971lemma pm_find_predicate : ∀A,t,p,q,a.
972  pm_find A t p = Some ? 〈q,a〉 →
973  p q a.
974#A #t #p normalize #q
975change with ((λx.x) q) in match q; generalize in match q; -q generalize in match (λx.x);
976elim t
977[ normalize #pre #q #a #E destruct
978| * [2:#a'] #l #r #IHl #IHr #pre #q #a normalize
979  [ lapply (refl ? (p (pre one) a')) cases (p (pre one) a') in ⊢ (???% → %);
980    [ #E normalize #E'
981      cut (pre one = pre q) [ destruct (E') destruct (e0) @e2 (* XXX ! *) ]
982      #E'' <E'' in E' ⊢ %; #E' destruct >E %
983    | #_ normalize
984    ]
985  ]
986  lapply (IHl (λx.pre (p0 x)))
987  lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p)
988  cases (pm_find_aux ?? l ?)
989  [ 1,3: #_ #_ normalize
990    lapply (IHr (λx.pre (p1 x)))
991    lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p)
992    cases (pm_find_aux ?? r ?)
993    [ 1,3: #_ #_ #E destruct
994    | *: * #q' #a' #H1 #H2 #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E %
995    ]
996  | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E %
997  ]
998] qed.
Note: See TracBrowser for help on using the repository browser.