source: src/common/PositiveMap.ma @ 2428

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

Tidy away generic results about folds on positive/identifier maps.

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