source: src/common/PositiveMap.ma @ 1971

Last change on this file since 1971 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 7.7 KB
Line 
1include "basics/types.ma".
2include "utilities/binary/positive.ma".
3
4inductive positive_map (A:Type[0]) : Type[0] ≝
5| pm_leaf : positive_map A
6| pm_node : option A → positive_map A → positive_map A → positive_map A.
7
8let rec lookup_opt (A:Type[0]) (b:Pos) (t:positive_map A) on t : option A ≝
9match t with
10[ pm_leaf ⇒ None ?
11| pm_node a l r ⇒
12    match b with
13    [ one ⇒ a
14    | p0 tl ⇒ lookup_opt A tl l
15    | p1 tl ⇒ lookup_opt A tl r
16    ]
17].
18
19definition lookup: ∀A:Type[0].Pos → positive_map A → A → A ≝ 
20 λA.λb.λt.λx.
21 match lookup_opt A b t with
22 [ None ⇒ x
23 | Some r ⇒ r
24 ].
25
26let rec insert (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : positive_map A ≝
27match b with
28[ one ⇒
29    match t with
30    [ pm_leaf ⇒ pm_node A (Some ? a) (pm_leaf A) (pm_leaf A)
31    | pm_node _ l r ⇒ pm_node A (Some ? a) l r
32    ]
33| p0 tl ⇒
34    match t with
35    [ pm_leaf ⇒ pm_node A (None ?) (insert A tl a (pm_leaf A)) (pm_leaf A)
36    | pm_node x l r ⇒ pm_node A x (insert A tl a l) r
37    ]
38| p1 tl ⇒
39    match t with
40    [ pm_leaf ⇒ pm_node A (None ?) (pm_leaf A) (insert A tl a (pm_leaf A))
41    | pm_node x l r ⇒ pm_node A x l (insert A tl a r)
42    ]
43].
44
45let rec update (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : option (positive_map A) ≝
46match b with
47[ one ⇒
48    match t with
49    [ pm_leaf ⇒ None ?
50    | pm_node x l r ⇒ option_map ?? (λ_. pm_node A (Some ? a) l r) x
51    ]
52| p0 tl ⇒
53    match t with
54    [ pm_leaf ⇒ None ?
55    | pm_node x l r ⇒ option_map ?? (λl. pm_node A x l r) (update A tl a l)
56    ]
57| p1 tl ⇒
58    match t with
59    [ pm_leaf ⇒ None ?
60    | pm_node x l r ⇒ option_map ?? (λr. pm_node A x l r) (update A tl a r)
61    ]
62].
63
64lemma lookup_opt_insert_hit :
65 ∀A:Type[0].∀v:A.∀b:Pos.∀t:positive_map A.
66  lookup_opt … b (insert … b v t) = Some A v.
67#A #v #b elim b
68[ * //
69| #tl #IH *
70  [ whd in ⊢ (??%%); @IH
71  | #x #l #r @IH
72  ]
73| #tl #IH *
74  [ whd in ⊢ (??%%); @IH
75  | #x #l #r @IH
76  ]
77] qed.
78
79axiom lookup_insert_hit:
80  ∀a: Type[0].
81  ∀v: a.
82  ∀b: Pos.
83  ∀t: positive_map a.
84  ∀d: a.
85    lookup … b (insert … b v t) d = v.
86
87lemma lookup_opt_insert_miss:
88 ∀A:Type[0].∀v:A.∀b,c:Pos.∀t:positive_map A.
89  b ≠ c → lookup_opt … b (insert … c v t) = lookup_opt … b t.
90#A #v #b elim b
91[ * [ #t * #H elim (H (refl …))
92    | *: #c' #t #NE cases t //
93    ]
94| #b' #IH *
95  [ * [ #NE @refl | #x #l #r #NE @refl ]
96  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
97          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
98          ]
99  | #c' * //
100  ]
101| #b' #IH *
102  [ * [ #NE @refl | #x #l #r #NE @refl ]
103  | #c' * //
104  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
105          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
106          ]
107  ]
108] qed.
109
110let rec fold (A, B: Type[0]) (f: Pos → A → B → B)
111 (t: positive_map A) (b: B) on t: B ≝
112match t with
113[ pm_leaf ⇒ b
114| pm_node a l r ⇒
115    let b ≝ match a with [ None ⇒ b | Some a ⇒ f one a b ] in
116    let b ≝ fold A B (λx.f (p0 x)) l b in
117            fold A B (λx.f (p1 x)) r b
118].   
119
120lemma update_fail : ∀A,b,a,t.
121  update A b a t = None ? →
122  lookup_opt A b t = None ?.
123#A #b #a elim b
124[ * [ // | * // #x #l #r normalize #E destruct ]
125| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
126                   cases (update A b' a r) in U ⊢ %;
127                   [ // | normalize #t #E destruct ]
128            ]
129| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
130                   cases (update A b' a l) in U ⊢ %;
131                   [ // | normalize #t #E destruct ]
132            ]
133] qed.
134
135lemma update_lookup_opt_same : ∀A,b,a,t,t'.
136  update A b a t = Some ? t' →
137  lookup_opt A b t' = Some ? a.
138#A #b #a elim b
139[ * [ #t' normalize #E destruct
140    | * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?);
141      #E destruct //
142    ]
143| #b' #IH *
144  [ #t' normalize #E destruct
145  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
146    lapply (IH r)
147    cases (update A b' a r)
148    [ #_ normalize #E destruct
149    | #r' #H normalize #E destruct @H @refl
150    ]
151  ]
152| #b' #IH *
153  [ #t' normalize #E destruct
154  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
155    lapply (IH l)
156    cases (update A b' a l)
157    [ #_ normalize #E destruct
158    | #r' #H normalize #E destruct @H @refl
159    ]
160  ]
161] qed.
162
163lemma update_lookup_opt_other : ∀A,b,a,t,t'.
164  update A b a t = Some ? t' →
165  ∀b'. b ≠ b' →
166  lookup_opt A b' t = lookup_opt A b' t'.
167#A #b #a elim b
168[ * [ #t' normalize #E destruct
169    | * [2: #x] #l #r #t' normalize #E destruct
170      * [ * #H elim (H (refl …)) ]
171      #tl #NE normalize //
172    ]
173| #b' #IH *
174  [ #t' normalize #E destruct
175  | #x #l #r #t' normalize
176    lapply (IH r)
177    cases (update A b' a r)
178    [ #_ normalize #E destruct
179    | #t'' #H normalize #E destruct * // #b'' #NE @H /2/
180    ]
181  ]
182| #b' #IH *
183  [ #t' normalize #E destruct
184  | #x #l #r #t' normalize
185    lapply (IH l)
186    cases (update A b' a l)
187    [ #_ normalize #E destruct
188    | #t'' #H normalize #E destruct * // #b'' #NE @H /2/
189    ]
190  ]
191] qed.
192
193include "utilities/option.ma".
194
195let rec map_opt A B (f : A → option B) (b : positive_map A) on b : positive_map B ≝
196match b with
197[ pm_leaf ⇒ pm_leaf ?
198| pm_node a l r ⇒ pm_node ? (a »= f)
199    (map_opt ?? f l)
200    (map_opt ?? f r)
201].
202
203definition map ≝ λA,B,f.map_opt A B (λx. Some ? (f x)).
204
205lemma lookup_opt_map : ∀A,B,f,b,p.
206  lookup_opt … p (map_opt A B f b) = ! x ← lookup_opt … p b ; f x.
207#A#B#f#b elim b [//]
208#a #l #r #Hil #Hir * [//]
209#p
210whd in ⊢ (??(???%)(????%?));
211whd in ⊢ (??%?); //
212qed.
213
214lemma map_opt_id_eq_ext : ∀A,m,f.(∀x.f x = Some ? x) → map_opt A A f m = m.
215#A #m #f #Hf elim m [//]
216* [2:#x] #l #r #Hil #Hir normalize [>Hf] //
217qed.
218
219lemma map_opt_id : ∀A,m.map_opt A A (λx. Some ? x) m = m.
220#A #m @map_opt_id_eq_ext //
221qed.
222
223let rec merge A B C (choice : option A → option B → option C)
224  (a : positive_map A) (b : positive_map B) on a : positive_map C ≝
225match a with
226[ pm_leaf ⇒ map_opt ?? (λx.choice (None ?) (Some ? x)) b
227| pm_node o l r ⇒
228  match b with
229  [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a
230  | pm_node o' l' r' ⇒
231    pm_node ? (choice o o')
232      (merge … choice l l')
233      (merge … choice r r')
234  ]
235].
236
237lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p.
238  choice (None ?) (None ?) = None ? →
239  lookup_opt … p (merge A B C choice a b) =
240    choice (lookup_opt … p a) (lookup_opt … p b).
241 #A#B#C#choice#a elim a
242[ normalize #b
243| #o#l#r#Hil#Hir * [2: #o'#l'#r' * normalize /2 by /]
244]
245#p#choice_good >lookup_opt_map
246elim (lookup_opt ???)
247normalize //
248qed.
249
250let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝
251match b with
252[ pm_leaf ⇒ 0
253| pm_node a l r ⇒
254  (match a with
255   [ Some _ ⇒ 1
256   | None ⇒ 0
257   ]) + domain_size A l + domain_size A r
258].
259
260(* just to load notation for 'norm (list.ma's notation overrides core's 'card)*)
261include "basics/lists/list.ma".
262interpretation "positive map size" 'norm p = (domain_size ? p).
263
264lemma map_opt_size : ∀A,B,f,b.|map_opt A B f b| ≤ |b|.
265#A#B#f#b elim b [//]
266*[2:#x]#l#r#Hil#Hir normalize
267[elim (f ?) normalize [@(transitive_le ? ? ? ? (le_n_Sn ?)) | #y @le_S_S ] ]
268@le_plus assumption
269qed.
270
271lemma map_size : ∀A,B,f,b.|map A B f b| = |b|.
272#A#B#f#b elim b [//]
273*[2:#x]#l#r#Hil#Hir normalize
274>Hil >Hir @refl
275qed.
276
277lemma lookup_opt_O_lt_size : ∀A,m,p. lookup_opt A p m ≠ None ? → 0 < |m|.
278#A#m elim m
279[#p normalize #F elim (absurd ? (refl ??) F)
280|* [2: #x]  #l #r #Hil #Hir * normalize
281  [1,2,3: //
282  |4:  #F elim (absurd ? (refl ??) F)]
283  #p #H [@(transitive_le … (Hir ? H)) | @(transitive_le … (Hil ? H))] //
284qed.
285
286lemma insert_size : ∀A,p,a,m. |insert A p a m| =
287  (match lookup_opt … p m with [Some _ ⇒ 0 | None ⇒ 1]) + |m|.
288#A#p elim p
289[ #a * [2: * [2: #x] #l #r] normalize //
290|*: #p #Hi #a * [2,4: * [2,4: #x] #l #r] normalize >Hi //
291] qed.
Note: See TracBrowser for help on using the repository browser.