1 | include "basics/types.ma". |
---|
2 | include "ASM/String.ma". |
---|
3 | include "utilities/binary/positive.ma". |
---|
4 | include "utilities/lists.ma". |
---|
5 | include "utilities/extralib.ma". |
---|
6 | include "common/Errors.ma". |
---|
7 | |
---|
8 | (* identifiers and their generators are tagged to differentiate them, and to |
---|
9 | provide extra type checking. *) |
---|
10 | |
---|
11 | (* in common/PreIdentifiers.ma, via Errors.ma. |
---|
12 | inductive identifier (tag:String) : Type[0] ≝ |
---|
13 | an_identifier : Pos → identifier tag. |
---|
14 | *) |
---|
15 | |
---|
16 | record universe (tag:String) : Type[0] ≝ |
---|
17 | { |
---|
18 | next_identifier : Pos |
---|
19 | }. |
---|
20 | |
---|
21 | definition new_universe : ∀tag:String. universe tag ≝ |
---|
22 | λtag. mk_universe tag one. |
---|
23 | |
---|
24 | let rec fresh (tag:String) (u:universe tag) on u : identifier tag × (universe tag) ≝ |
---|
25 | let id ≝ next_identifier ? u in |
---|
26 | 〈an_identifier tag id, mk_universe tag (succ id)〉. |
---|
27 | |
---|
28 | |
---|
29 | let rec fresh_for_univ tag (id:identifier tag) (u:universe tag) on id : Prop ≝ |
---|
30 | match id with [ an_identifier p ⇒ p < next_identifier … u ]. |
---|
31 | |
---|
32 | |
---|
33 | lemma fresh_is_fresh : ∀tag,id,u,u'. |
---|
34 | 〈id,u〉 = fresh tag u' → |
---|
35 | fresh_for_univ tag id u. |
---|
36 | #tag * #id * #u * #u' #E whd in E:(???%); destruct // |
---|
37 | qed. |
---|
38 | |
---|
39 | lemma fresh_remains_fresh : ∀tag,id,id',u,u'. |
---|
40 | fresh_for_univ tag id u → |
---|
41 | 〈id',u'〉 = fresh tag u → |
---|
42 | fresh_for_univ tag id u'. |
---|
43 | #tag * #id * #id' * #u * #u' normalize #H #E destruct /2 by le_S/ |
---|
44 | qed. |
---|
45 | |
---|
46 | lemma fresh_distinct : ∀tag,id,id',u,u'. |
---|
47 | fresh_for_univ tag id u → |
---|
48 | 〈id',u'〉 = fresh tag u → |
---|
49 | id ≠ id'. |
---|
50 | #tag * #id * #id' * #u * #u' normalize #H #E destruct % #E' destruct /2 by absurd/ |
---|
51 | qed. |
---|
52 | |
---|
53 | |
---|
54 | let rec env_fresh_for_univ tag A (env:list (identifier tag × A)) (u:universe tag) on u : Prop ≝ |
---|
55 | All ? (λida. fresh_for_univ tag (\fst ida) u) env. |
---|
56 | |
---|
57 | lemma fresh_env_extend : ∀tag,A,env,u,u',id,a. |
---|
58 | env_fresh_for_univ tag A env u → |
---|
59 | 〈id,u'〉 = fresh tag u → |
---|
60 | env_fresh_for_univ tag A (〈id,a〉::env) u'. |
---|
61 | #tag #A #env * #u * #u' #id #a |
---|
62 | #H #E whd % [ @(fresh_is_fresh … E) | @(All_mp … H) * #id #a #H' /2 by fresh_remains_fresh/ ] |
---|
63 | qed. |
---|
64 | |
---|
65 | definition eq_identifier : ∀t. identifier t → identifier t → bool ≝ |
---|
66 | λt,l,r. |
---|
67 | match l with |
---|
68 | [ an_identifier l' ⇒ |
---|
69 | match r with |
---|
70 | [ an_identifier r' ⇒ |
---|
71 | eqb l' r' |
---|
72 | ] |
---|
73 | ]. |
---|
74 | |
---|
75 | lemma eq_identifier_elim : ∀P:bool → Type[0]. ∀t,x,y. |
---|
76 | (x = y → P true) → (x ≠ y → P false) → |
---|
77 | P (eq_identifier t x y). |
---|
78 | #P #t * #x * #y #T #F |
---|
79 | change with (P (eqb ??)) |
---|
80 | @(eqb_elim x y P) [ /2 by / | * #H @F % #E destruct /2 by / ] |
---|
81 | qed. |
---|
82 | |
---|
83 | lemma eq_identifier_eq: |
---|
84 | ∀tag: String. |
---|
85 | ∀l. |
---|
86 | ∀r. |
---|
87 | eq_identifier tag l r = true → l = r. |
---|
88 | #tag #l #r cases l cases r |
---|
89 | #pos_l #pos_r |
---|
90 | cases pos_l cases pos_r |
---|
91 | [1: |
---|
92 | #_ % |
---|
93 | |2,3,4,7: |
---|
94 | #p1_l normalize in ⊢ (% → ?); |
---|
95 | #absurd destruct(absurd) |
---|
96 | |5,9: |
---|
97 | #p1_l #p1_r normalize in ⊢ (% → ?); |
---|
98 | #relevant lapply (eqb_true_to_eq … relevant) #EQ >EQ % |
---|
99 | |*: |
---|
100 | #p_l #p_r normalize in ⊢ (% → ?); |
---|
101 | #absurd destruct(absurd) |
---|
102 | ] |
---|
103 | qed. |
---|
104 | |
---|
105 | axiom neq_identifier_neq: |
---|
106 | ∀tag: String. |
---|
107 | ∀l, r: identifier tag. |
---|
108 | eq_identifier tag l r = false → (l = r → False). |
---|
109 | |
---|
110 | include "basics/deqsets.ma". |
---|
111 | definition Deq_identifier : String → DeqSet ≝ λtag. |
---|
112 | mk_DeqSet (identifier tag) (eq_identifier tag) ?. |
---|
113 | #x#y @eq_identifier_elim /2 by conj/ * #H % [#ABS destruct(ABS) | #G elim (H G)] |
---|
114 | qed. |
---|
115 | |
---|
116 | unification hint 0 ≔ tag; D ≟ Deq_identifier tag |
---|
117 | (*-----------------------------------------------------*)⊢ |
---|
118 | identifier tag ≡ carr D. |
---|
119 | |
---|
120 | definition word_of_identifier ≝ |
---|
121 | λt. |
---|
122 | λl: identifier t. |
---|
123 | match l with |
---|
124 | [ an_identifier l' ⇒ l' |
---|
125 | ]. |
---|
126 | |
---|
127 | lemma eq_identifier_refl : ∀tag,id. eq_identifier tag id id = true. |
---|
128 | #tag * #id whd in ⊢ (??%?); >eqb_n_n @refl |
---|
129 | qed. |
---|
130 | |
---|
131 | axiom eq_identifier_sym: |
---|
132 | ∀tag: String. |
---|
133 | ∀l : identifier tag. |
---|
134 | ∀r : identifier tag. |
---|
135 | eq_identifier tag l r = eq_identifier tag r l. |
---|
136 | |
---|
137 | lemma eq_identifier_false : ∀tag,x,y. x≠y → eq_identifier tag x y = false. |
---|
138 | #tag * #x * #y #NE normalize @not_eq_to_eqb_false /2 by not_to_not/ |
---|
139 | qed. |
---|
140 | |
---|
141 | definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y). |
---|
142 | #tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %); |
---|
143 | #E [ % | %2 ] |
---|
144 | lapply E @eqb_elim |
---|
145 | [ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2 by absurd/ ] |
---|
146 | qed. |
---|
147 | |
---|
148 | definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝ |
---|
149 | λtag,n. an_identifier tag (succ_pos_of_nat n). |
---|
150 | |
---|
151 | |
---|
152 | (* States that all identifiers in an environment are distinct from one another. *) |
---|
153 | let rec distinct_env tag (A:Type[0]) (l:list (identifier tag × A)) on l : Prop ≝ |
---|
154 | match l with |
---|
155 | [ nil ⇒ True |
---|
156 | | cons hd tl ⇒ All ? (λia. \fst hd ≠ \fst ia) tl ∧ |
---|
157 | distinct_env tag A tl |
---|
158 | ]. |
---|
159 | |
---|
160 | lemma distinct_env_append_l : ∀tag,A,l,r. distinct_env tag A (l@r) → distinct_env tag A l. |
---|
161 | #tag #A #l elim l |
---|
162 | [ // |
---|
163 | | * #id #a #tl #IH #r * #H1 #H2 % /2 by All_append_l/ |
---|
164 | ] qed. |
---|
165 | |
---|
166 | lemma distinct_env_append_r : ∀tag,A,l,r. distinct_env tag A (l@r) → distinct_env tag A r. |
---|
167 | #tag #A #l elim l |
---|
168 | [ // |
---|
169 | | * #id #a #tl #IH #r * #H1 #H2 /2 by / |
---|
170 | ] qed. |
---|
171 | |
---|
172 | (* check_distinct_env is quadratic - we could pay more attention when building maps to make sure that |
---|
173 | the original environment was distinct. *) |
---|
174 | |
---|
175 | axiom DuplicateVariable : String. |
---|
176 | |
---|
177 | let rec check_member_env tag (A:Type[0]) (id:identifier tag) (l:list (identifier tag × A)) on l : res (All ? (λia. id ≠ \fst ia) l) ≝ |
---|
178 | match l return λl.res (All ?? l) with |
---|
179 | [ nil ⇒ OK ? I |
---|
180 | | cons hd tl ⇒ |
---|
181 | match identifier_eq tag id (\fst hd) with |
---|
182 | [ inl _ ⇒ Error ? [MSG DuplicateVariable; CTX ? id] |
---|
183 | | inr NE ⇒ |
---|
184 | do Htl ← check_member_env tag A id tl; |
---|
185 | OK ? (conj ?? NE Htl) |
---|
186 | ] |
---|
187 | ]. |
---|
188 | |
---|
189 | let rec check_distinct_env tag (A:Type[0]) (l:list (identifier tag × A)) on l : res (distinct_env tag A l) ≝ |
---|
190 | match l return λl.res (distinct_env tag A l) with |
---|
191 | [ nil ⇒ OK ? I |
---|
192 | | cons hd tl ⇒ |
---|
193 | do Hhd ← check_member_env tag A (\fst hd) tl; |
---|
194 | do Htl ← check_distinct_env tag A tl; |
---|
195 | OK ? (conj ?? Hhd Htl) |
---|
196 | ]. |
---|
197 | |
---|
198 | |
---|
199 | |
---|
200 | |
---|
201 | (* Maps from identifiers to arbitrary types. *) |
---|
202 | |
---|
203 | include "common/PositiveMap.ma". |
---|
204 | |
---|
205 | inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝ |
---|
206 | an_id_map : positive_map A → identifier_map tag A. |
---|
207 | |
---|
208 | definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝ |
---|
209 | λtag,A. an_id_map tag A (pm_leaf A). |
---|
210 | |
---|
211 | let rec lookup tag A (m:identifier_map tag A) (l:identifier tag) on m : option A ≝ |
---|
212 | lookup_opt A (match l with [ an_identifier l' ⇒ l' ]) |
---|
213 | (match m with [ an_id_map m' ⇒ m' ]). |
---|
214 | |
---|
215 | definition lookup_def ≝ |
---|
216 | λtag,A,m,l,d. match lookup tag A m l with [ None ⇒ d | Some x ⇒ x]. |
---|
217 | |
---|
218 | definition member ≝ |
---|
219 | λtag,A.λm:identifier_map tag A.λl:identifier tag. |
---|
220 | match lookup tag A m l with [ None ⇒ false | _ ⇒ true ]. |
---|
221 | |
---|
222 | interpretation "identifier map membership" 'mem a b = (member ?? b a). |
---|
223 | |
---|
224 | definition lookup_safe : ∀tag,A.∀m : identifier_map tag A.∀i.i∈m → A ≝ |
---|
225 | λtag,A,m,i. |
---|
226 | match lookup … m i return λx.match x in option return λ_.bool with [ _ ⇒ ?] → ? with |
---|
227 | [ Some x ⇒ λ_.x |
---|
228 | | None ⇒ λprf.⊥ |
---|
229 | ]. @prf qed. |
---|
230 | |
---|
231 | lemma lookup_eq_safe : ∀tag,A,m,i,prf.lookup tag A m i = Some ? (lookup_safe tag A m i prf). |
---|
232 | #tag #A #m #i whd in match (i∈m); |
---|
233 | whd in match lookup_safe; normalize nodelta |
---|
234 | cases (lookup ????) normalize nodelta [*] // qed. |
---|
235 | |
---|
236 | (* Always adds the identifier to the map. *) |
---|
237 | let rec add tag A (m:identifier_map tag A) (l:identifier tag) (a:A) on m : identifier_map tag A ≝ |
---|
238 | an_id_map tag A (insert A (match l with [ an_identifier l' ⇒ l' ]) a |
---|
239 | (match m with [ an_id_map m' ⇒ m' ])). |
---|
240 | |
---|
241 | lemma lookup_add_hit : ∀tag,A,m,i,a. |
---|
242 | lookup tag A (add tag A m i a) i = Some ? a. |
---|
243 | #tag #A * #m * #i #a |
---|
244 | @lookup_opt_insert_hit |
---|
245 | qed. |
---|
246 | |
---|
247 | lemma lookup_def_add_hit : ∀tag,A,m,i,a,d. |
---|
248 | lookup_def tag A (add tag A m i a) i d = a. |
---|
249 | #tag #A * #m * #i #a #d |
---|
250 | @lookup_insert_hit |
---|
251 | qed. |
---|
252 | |
---|
253 | lemma lookup_add_miss : ∀tag,A,m,i,j,a. |
---|
254 | i ≠ j → |
---|
255 | lookup tag A (add tag A m j a) i = lookup tag A m i. |
---|
256 | #tag #A * #m * #i * #j #a #H |
---|
257 | @lookup_opt_insert_miss /2 by not_to_not/ |
---|
258 | qed. |
---|
259 | |
---|
260 | axiom lookup_def_add_miss : ∀tag,A,m,i,j,a,d. |
---|
261 | i ≠ j → |
---|
262 | lookup_def tag A (add tag A m j a) i d = lookup_def tag A m i d. |
---|
263 | |
---|
264 | lemma lookup_add_oblivious : ∀tag,A,m,i,j,a. |
---|
265 | (lookup tag A m i ≠ None ?) → |
---|
266 | lookup tag A (add tag A m j a) i ≠ None ?. |
---|
267 | #tag #A #m #i #j #a #H |
---|
268 | cases (identifier_eq ? i j) |
---|
269 | [ #E >E >lookup_add_hit % #N destruct |
---|
270 | | #NE >lookup_add_miss // |
---|
271 | ] qed. |
---|
272 | |
---|
273 | lemma lookup_add_cases : ∀tag,A,m,i,j,a,v. |
---|
274 | lookup tag A (add tag A m i a) j = Some ? v → |
---|
275 | (i=j ∧ v = a) ∨ lookup tag A m j = Some ? v. |
---|
276 | #tag #A #m #i #j #a #v |
---|
277 | cases (identifier_eq ? i j) |
---|
278 | [ #E >E >lookup_add_hit #H %1 destruct % // |
---|
279 | | #NE >lookup_add_miss /2 by or_intror, sym_not_eq/ |
---|
280 | ] qed. |
---|
281 | |
---|
282 | (* Extract every identifier, value pair from the map. *) |
---|
283 | definition elements : ∀tag,A. identifier_map tag A → list (identifier tag × A) ≝ |
---|
284 | λtag,A,m. |
---|
285 | fold ?? (λl,a,el. 〈an_identifier tag l, a〉::el) |
---|
286 | (match m with [ an_id_map m' ⇒ m' ]) [ ]. |
---|
287 | |
---|
288 | (* Test a predicate on all of the entries in a map. The predicate is given a |
---|
289 | proof that the entry appears in the map. *) |
---|
290 | |
---|
291 | definition idmap_all : ∀tag,A. ∀m:identifier_map tag A. (∀id,a. lookup tag A m id = Some A a → bool) → bool ≝ |
---|
292 | λtag,A,m,f. pm_all A (match m with [ an_id_map m' ⇒ m' ]) |
---|
293 | (λp,a,H. f (an_identifier tag p) a ?). |
---|
294 | cases m in H ⊢ %; #m' normalize // |
---|
295 | qed. |
---|
296 | |
---|
297 | inductive idmap_pred_graph : ∀tag,A,m,id,a,L. ∀f:(∀id,a. lookup tag A m id = Some A a → bool). bool → Prop ≝ |
---|
298 | | idmappg : ∀tag,A,m,id,a,L,f. idmap_pred_graph tag A m id a L f (f id a L). |
---|
299 | |
---|
300 | lemma idmap_pred_irr : ∀tag,A,m,id,a,L,L'. ∀f:(∀id,a. lookup tag A m id = Some A a → bool). |
---|
301 | f id a L = f id a L'. |
---|
302 | #tag #A #m #id #a #L #L' #f |
---|
303 | cut (idmap_pred_graph tag A m id a L f (f id a L)) [ % ] |
---|
304 | cases (f id a L) #H |
---|
305 | cut (idmap_pred_graph tag A m id a L' f ?) [ 2,5: @H | 1,4: skip ] * // |
---|
306 | qed. |
---|
307 | |
---|
308 | lemma idmap_all_ok : ∀tag,A,m,f. |
---|
309 | bool_to_Prop (idmap_all tag A m f) ↔ (∀id,a,H. f id a H). |
---|
310 | #tag #A * #m #f |
---|
311 | whd in match (idmap_all ????); @(iff_trans … (pm_all_ok …)) % |
---|
312 | [ #H * #id #a #PR lapply (H id a PR) #X @eq_true_to_b <X @idmap_pred_irr |
---|
313 | | #H #p #a #PR @H |
---|
314 | ] qed. |
---|
315 | |
---|
316 | |
---|
317 | axiom MissingId : String. |
---|
318 | |
---|
319 | (* Only updates an existing entry; fails with an error otherwise. *) |
---|
320 | definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝ |
---|
321 | λtag,A,m,l,a. |
---|
322 | match update A (match l with [ an_identifier l' ⇒ l' ]) a |
---|
323 | (match m with [ an_id_map m' ⇒ m' ]) with |
---|
324 | [ None ⇒ Error ? ([MSG MissingId; CTX tag l]) (* missing identifier *) |
---|
325 | | Some m' ⇒ OK ? (an_id_map tag A m') |
---|
326 | ]. |
---|
327 | |
---|
328 | definition foldi: |
---|
329 | ∀A, B: Type[0]. |
---|
330 | ∀tag: String. |
---|
331 | (identifier tag -> A -> B -> B) -> identifier_map tag A -> B -> B ≝ |
---|
332 | λA,B,tag,f,m,b. |
---|
333 | match m with |
---|
334 | [ an_id_map m' ⇒ fold A B (λbv. f (an_identifier ? bv)) m' b ]. |
---|
335 | |
---|
336 | (* An informative, dependently-typed, fold. *) |
---|
337 | |
---|
338 | definition fold_inf: |
---|
339 | ∀A, B: Type[0]. |
---|
340 | ∀tag: String. |
---|
341 | ∀m:identifier_map tag A. |
---|
342 | (∀id:identifier tag. ∀a:A. lookup … m id = Some A a → B → B) → B → B ≝ |
---|
343 | λA,B,tag,m. |
---|
344 | match m return λm. (∀id:identifier tag. ∀a:A. lookup … m id = Some A a → B → B) → B → B with |
---|
345 | [ an_id_map m' ⇒ λf,b. pm_fold_inf A B m' (λbv,a,H. f (an_identifier ? bv) a H) b ]. |
---|
346 | |
---|
347 | (* Find one element of a map that satisfies a predicate *) |
---|
348 | definition find : ∀tag,A. identifier_map tag A → (identifier tag → A → bool) → |
---|
349 | option (identifier tag × A) ≝ |
---|
350 | λtag,A,m,p. |
---|
351 | match m with [ an_id_map m' ⇒ |
---|
352 | option_map … (λx. 〈an_identifier tag (\fst x), \snd x〉) |
---|
353 | (pm_find … m' (λid. p (an_identifier tag id))) ]. |
---|
354 | |
---|
355 | lemma find_lookup : ∀tag,A,m,p,id,a. |
---|
356 | find tag A m p = Some ? 〈id,a〉 → |
---|
357 | lookup … m id = Some ? a. |
---|
358 | #tag #A * #m #p * #id #a #FIND |
---|
359 | @(pm_find_lookup A (λid. p (an_identifier tag id)) id a m) |
---|
360 | whd in FIND:(??%?); cases (pm_find ???) in FIND ⊢ %; |
---|
361 | [ normalize #E destruct |
---|
362 | | * #id' #a' normalize #E destruct % |
---|
363 | ] qed. |
---|
364 | |
---|
365 | lemma find_predicate : ∀tag,A,m,p,id,a. |
---|
366 | find tag A m p = Some ? 〈id,a〉 → |
---|
367 | p id a. |
---|
368 | #tag #A * #m #p * #id #a #FIND whd in FIND:(??%?); |
---|
369 | @(pm_find_predicate A m (λid. p (an_identifier tag id)) id a) |
---|
370 | cases (pm_find ???) in FIND ⊢ %; |
---|
371 | [ normalize #E destruct |
---|
372 | | * #id' #a' normalize #E destruct % |
---|
373 | ] qed. |
---|
374 | |
---|
375 | (* A predicate that an identifier is in a map, and a failure-avoiding lookup |
---|
376 | and update using it. *) |
---|
377 | |
---|
378 | definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝ |
---|
379 | λtag,A,m,i. lookup … m i ≠ None ?. |
---|
380 | |
---|
381 | lemma member_present : ∀tag,A,m,id. |
---|
382 | member tag A m id = true → present tag A m id. |
---|
383 | #tag #A * #m #id normalize cases (lookup_opt A ??) normalize |
---|
384 | [ #E destruct |
---|
385 | | #x #E % #E' destruct |
---|
386 | ] qed. |
---|
387 | |
---|
388 | lemma present_member : ∀tag,A,m,id. |
---|
389 | present tag A m id → member tag A m id. |
---|
390 | #tag #A #m #id whd in ⊢ (% → ?%); cases (lookup ????) // * #H cases (H (refl ??)) |
---|
391 | qed. |
---|
392 | |
---|
393 | definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝ |
---|
394 | λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ]. |
---|
395 | cases H #H' cases (H' (refl ??)) qed. |
---|
396 | |
---|
397 | lemma lookup_lookup_present : ∀tag,A,m,id,p. |
---|
398 | lookup tag A m id = Some ? (lookup_present tag A m id p). |
---|
399 | #tag #A #m #id #p |
---|
400 | whd in p ⊢ (???(??%)); |
---|
401 | cases (lookup tag A m id) in p ⊢ %; |
---|
402 | [ * #H @⊥ @H @refl |
---|
403 | | #a #H @refl |
---|
404 | ] qed. |
---|
405 | |
---|
406 | lemma lookup_is_present : ∀tag,T,m,id,t. |
---|
407 | lookup tag T m id = Some T t → |
---|
408 | present ?? m id. |
---|
409 | #tag #T #m #id #t #L normalize >L % #E destruct |
---|
410 | qed. |
---|
411 | |
---|
412 | lemma lookup_present_eq : ∀tag,T,m,id,t. |
---|
413 | lookup tag T m id = Some T t → |
---|
414 | ∀H. lookup_present tag T m id H = t. |
---|
415 | #tag #T #m #id #t #L #H |
---|
416 | lapply (lookup_lookup_present … H) >L #E destruct % |
---|
417 | qed. |
---|
418 | |
---|
419 | |
---|
420 | definition update_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A → identifier_map tag A ≝ |
---|
421 | λtag,A,m,l,p,a. |
---|
422 | let l' ≝ match l with [ an_identifier l' ⇒ l' ] in |
---|
423 | let m' ≝ match m with [ an_id_map m' ⇒ m' ] in |
---|
424 | let u' ≝ update A l' a m' in |
---|
425 | match u' return λx. update ???? = x → ? with |
---|
426 | [ None ⇒ λE.⊥ |
---|
427 | | Some m' ⇒ λ_. an_id_map tag A m' |
---|
428 | ] (refl ? u'). |
---|
429 | cases l in p E; cases m; -l' -m' #m' #l' |
---|
430 | whd in ⊢ (% → ?); |
---|
431 | whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?); |
---|
432 | #NL #U cases NL #H @H @(update_fail … U) |
---|
433 | qed. |
---|
434 | |
---|
435 | lemma update_still_present : ∀tag,A,m,id,a,id'. |
---|
436 | ∀H:present tag A m id. |
---|
437 | ∀H':present tag A m id'. |
---|
438 | present tag A (update_present tag A m id' H' a) id. |
---|
439 | #tag #A * #m * #id #a * #id' #H #H' |
---|
440 | whd whd in ⊢ (?(??(???(%??????)?)?)); normalize nodelta |
---|
441 | cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id')) |
---|
442 | [ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); >(update_lookup_opt_same ????? U) |
---|
443 | % #E' destruct |
---|
444 | | #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); whd in ⊢ (?(??(??%%)?)); |
---|
445 | <(update_lookup_opt_other ????? U id) [ @H | % #E cases NE >E #H @H @refl ] |
---|
446 | ] qed. |
---|
447 | |
---|
448 | lemma lookup_present_add_hit: |
---|
449 | ∀tag, A, map, k, v, k_pres. |
---|
450 | lookup_present tag A (add … map k v) k k_pres = v. |
---|
451 | #tag #a #map #k #v #k_pres |
---|
452 | lapply (lookup_lookup_present … (add … map k v) … k_pres) |
---|
453 | >lookup_add_hit #Some_assm destruct(Some_assm) |
---|
454 | <e0 % |
---|
455 | qed. |
---|
456 | |
---|
457 | lemma lookup_present_add_miss: |
---|
458 | ∀tag, A, map, k, k', v, k_pres', k_pres''. |
---|
459 | k' ≠ k → |
---|
460 | lookup_present tag A (add … map k v) k' k_pres' = lookup_present tag A map k' k_pres''. |
---|
461 | #tag #A #map #k #k' #v #k_pres' #k_pres'' #neq_assm |
---|
462 | lapply (lookup_lookup_present … (add … map k v) ? k_pres') |
---|
463 | >lookup_add_miss try assumption |
---|
464 | #Some_assm |
---|
465 | lapply (lookup_lookup_present … map k') >Some_assm #Some_assm' |
---|
466 | lapply (Some_assm' k_pres'') #Some_assm'' destruct assumption |
---|
467 | qed. |
---|
468 | |
---|
469 | lemma present_add_present: |
---|
470 | ∀tag, a, map, k, k', v. |
---|
471 | k' ≠ k → |
---|
472 | present tag a (add tag a map k v) k' → |
---|
473 | present tag a map k'. |
---|
474 | #tag #a #map #k #k' #v #neq_hyp #present_hyp |
---|
475 | whd in match present; normalize nodelta |
---|
476 | whd in match present in present_hyp; normalize nodelta in present_hyp; |
---|
477 | cases (not_None_to_Some a … present_hyp) #v' #Some_eq_hyp |
---|
478 | lapply (lookup_add_cases tag ?????? Some_eq_hyp) * |
---|
479 | [1: |
---|
480 | * #k_eq_hyp @⊥ /2/ |
---|
481 | |2: |
---|
482 | #Some_eq_hyp' /2/ |
---|
483 | ] |
---|
484 | qed. |
---|
485 | |
---|
486 | lemma present_add_hit: |
---|
487 | ∀tag, a, map, k, v. |
---|
488 | present tag a (add tag a map k v) k. |
---|
489 | #tag #a #map #k #v |
---|
490 | whd >lookup_add_hit |
---|
491 | % #absurd destruct |
---|
492 | qed. |
---|
493 | |
---|
494 | lemma present_add_miss: |
---|
495 | ∀tag, a, map, k, k', v. |
---|
496 | k' ≠ k → present tag a map k' → present tag a (add tag a map k v) k'. |
---|
497 | #tag #a #map #k #k' #v #neq_assm #present_assm |
---|
498 | whd >lookup_add_miss assumption |
---|
499 | qed. |
---|
500 | |
---|
501 | |
---|
502 | let rec fresh_for_map tag A (id:identifier tag) (m:identifier_map tag A) on id : Prop ≝ |
---|
503 | lookup … m id = None A. |
---|
504 | |
---|
505 | lemma fresh_for_empty_map : ∀tag,A,id. |
---|
506 | fresh_for_map tag A id (empty_map tag A). |
---|
507 | #tag #A * #id // |
---|
508 | qed. |
---|
509 | |
---|
510 | definition fresh_map_for_univ ≝ |
---|
511 | λtag,A. λm:identifier_map tag A. λu:universe tag. |
---|
512 | ∀id. present tag A m id → fresh_for_univ tag id u. |
---|
513 | |
---|
514 | lemma fresh_fresh_for_map : ∀tag,A,m,id,u,u'. |
---|
515 | fresh_map_for_univ tag A m u → |
---|
516 | 〈id,u'〉 = fresh tag u → |
---|
517 | fresh_for_map tag A id m. |
---|
518 | #tag #A * #m * #id * #u * #u' whd in ⊢ (% → ???% → %); |
---|
519 | #FMU #E destruct lapply (FMU (an_identifier tag u)) whd in ⊢ ((% → %) → ?); |
---|
520 | generalize in ⊢ ((?(??%?) → ?) → ??%?); * |
---|
521 | [ // | #a #H @False_ind lapply (H ?) /2 by absurd/ % #E destruct |
---|
522 | qed. |
---|
523 | |
---|
524 | lemma fresh_map_preserved : ∀tag,A,m,u,u',id. |
---|
525 | fresh_map_for_univ tag A m u → |
---|
526 | 〈id,u'〉 = fresh tag u → |
---|
527 | fresh_map_for_univ tag A m u'. |
---|
528 | #tag #A #m #u * #u' #id whd in ⊢ (% → ? → %); #H #E |
---|
529 | #id' #PR @(fresh_remains_fresh … E) @H // |
---|
530 | qed. |
---|
531 | |
---|
532 | lemma fresh_map_add : ∀tag,A,m,u,id,a. |
---|
533 | fresh_map_for_univ tag A m u → |
---|
534 | fresh_for_univ tag id u → |
---|
535 | fresh_map_for_univ tag A (add tag A m id a) u. |
---|
536 | #tag #A * #m #u #id #a #Hm #Hi |
---|
537 | #id' #PR cases (identifier_eq tag id' id) |
---|
538 | [ #E >E @Hi |
---|
539 | | #NE @Hm whd in PR; |
---|
540 | change with (add tag A (an_id_map tag A m) id a) in PR:(?(??(???%?)?)); |
---|
541 | >lookup_add_miss in PR; // |
---|
542 | ] qed. |
---|
543 | |
---|
544 | lemma present_not_fresh : ∀tag,A,m,id,id'. |
---|
545 | present tag A m id → |
---|
546 | fresh_for_map tag A id' m → |
---|
547 | id ≠ id'. |
---|
548 | #tag #A #m #id * #id' whd in ⊢ (% → % → ?); |
---|
549 | * #NE #E % #E' destruct @(NE E) |
---|
550 | qed. |
---|
551 | |
---|
552 | lemma fresh_for_map_add : ∀tag,A,id,m,id',a. |
---|
553 | id ≠ id' → |
---|
554 | fresh_for_map tag A id m → |
---|
555 | fresh_for_map tag A id (add tag A m id' a). |
---|
556 | #tag #A * #id #m #id' #a #NE #F |
---|
557 | whd >lookup_add_miss // |
---|
558 | qed. |
---|
559 | |
---|
560 | (* Extending the domain of a map (without necessarily preserving contents). *) |
---|
561 | |
---|
562 | definition extends_domain : ∀tag,A. identifier_map tag A → identifier_map tag A → Prop ≝ |
---|
563 | λtag,A,m1,m2. ∀l. present ?? m1 l → present ?? m2 l. |
---|
564 | |
---|
565 | lemma extends_dom_trans : ∀tag,A,m1,m2,m3. |
---|
566 | extends_domain tag A m1 m2 → extends_domain tag A m2 m3 → extends_domain tag A m1 m3. |
---|
567 | #tag #A #m1 #m2 #m3 #H1 #H2 #l #P1 @H2 @H1 @P1 qed. |
---|
568 | |
---|
569 | |
---|
570 | (* Sets *) |
---|
571 | |
---|
572 | definition identifier_set ≝ λtag.identifier_map tag unit. |
---|
573 | |
---|
574 | definition empty_set : ∀tag.identifier_set tag ≝ λtag.empty_map …. |
---|
575 | |
---|
576 | |
---|
577 | definition add_set : ∀tag.identifier_set tag → identifier tag → identifier_set tag ≝ |
---|
578 | λtag,s,i.add … s i it. |
---|
579 | |
---|
580 | definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝ |
---|
581 | λtag,i. add_set tag (empty_set tag) i. |
---|
582 | |
---|
583 | let rec union_set (tag:String) A B (s:identifier_map tag A) (s':identifier_map tag B) on s : identifier_set tag ≝ |
---|
584 | an_id_map tag unit (merge … (λo,o'.match o with [Some _ ⇒ Some ? it | None ⇒ !_ o'; return it]) |
---|
585 | (match s with [ an_id_map s0 ⇒ s0 ]) |
---|
586 | (match s' with [ an_id_map s1 ⇒ s1 ])). |
---|
587 | |
---|
588 | |
---|
589 | (* set minus is generalised to maps *) |
---|
590 | let rec minus_set (tag:String) A B (s:identifier_map tag A) (s':identifier_map tag B) on s : identifier_map tag A ≝ |
---|
591 | an_id_map tag A (merge A B A (λo,o'.match o' with [None ⇒ o | Some _ ⇒ None ?]) |
---|
592 | (match s with [ an_id_map s0 ⇒ s0 ]) |
---|
593 | (match s' with [ an_id_map s1 ⇒ s1 ])). |
---|
594 | |
---|
595 | notation "a ∖ b" left associative with precedence 55 for @{'setminus $a $b}. |
---|
596 | |
---|
597 | interpretation "identifier set union" 'union a b = (union_set ??? a b). |
---|
598 | notation "∅" non associative with precedence 90 for @{ 'empty }. |
---|
599 | interpretation "empty identifier set" 'empty = (empty_set ?). |
---|
600 | interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a). |
---|
601 | interpretation "identifier map difference" 'setminus a b = (minus_set ??? a b). |
---|
602 | |
---|
603 | definition IdentifierSet : String → Setoid ≝ λtag. |
---|
604 | mk_Setoid (identifier_set tag) (λs,s'.∀i.i ∈ s = (i ∈ s')) ???. |
---|
605 | // qed. |
---|
606 | |
---|
607 | unification hint 0 ≔ tag; |
---|
608 | S ≟ IdentifierSet tag |
---|
609 | (*-----------------------------*)⊢ |
---|
610 | identifier_set tag ≡ std_supp S. |
---|
611 | unification hint 0 ≔ tag; |
---|
612 | S ≟ IdentifierSet tag |
---|
613 | (*-----------------------------*)⊢ |
---|
614 | identifier_map tag unit ≡ std_supp S. |
---|
615 | |
---|
616 | lemma mem_set_add : ∀tag,A.∀i,j : identifier tag.∀s,x. |
---|
617 | i ∈ add ? A s j x = (eq_identifier ? i j ∨ i ∈ s). |
---|
618 | #tag #A *#i *#j *#s #x normalize |
---|
619 | @(eqb_elim i j) |
---|
620 | [#EQ destruct |
---|
621 | >(lookup_opt_insert_hit A x j) |
---|
622 | |#NEQ >(lookup_opt_insert_miss … s NEQ) |
---|
623 | ] elim (lookup_opt A j s) normalize // qed. |
---|
624 | |
---|
625 | lemma mem_set_add_id : ∀tag,A,i,s,x.bool_to_Prop (i ∈ add tag A s i x). |
---|
626 | #tag #A #i #s #x >mem_set_add |
---|
627 | @eq_identifier_elim [#_ %| #ABS elim (absurd … (refl ? i) ABS)] qed. |
---|
628 | |
---|
629 | lemma in_map_domain : ∀tag,A.∀m : identifier_map tag A.∀i. |
---|
630 | if i ∈ m then (∃s.lookup … m i = Some ? s) else (lookup … m i = None ?). |
---|
631 | #tag #A * #m * #i normalize |
---|
632 | elim (lookup_opt A i m) normalize |
---|
633 | [ % | #x %{x} % ] |
---|
634 | qed. |
---|
635 | |
---|
636 | lemma union_empty_l : ∀tag.∀s:identifier_set tag. ∅ ∪ s = s. |
---|
637 | #tag * normalize #m >map_opt_id_eq_ext // * % |
---|
638 | qed. |
---|
639 | |
---|
640 | lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s. |
---|
641 | #tag * * [//] *[2: *] #l#r normalize |
---|
642 | >map_opt_id_eq_ext [1,3: >map_opt_id_eq_ext [2,4: *] |*: *] // |
---|
643 | qed. |
---|
644 | |
---|
645 | lemma minus_empty_l : ∀tag,A.∀s:identifier_map tag A. ∅ ∖ s ≅ ∅. |
---|
646 | #tag #A * * [//] *[2:#x]#l#r * * normalize [1,4://] |
---|
647 | #p >lookup_opt_map elim (lookup_opt ???) normalize // |
---|
648 | qed. |
---|
649 | |
---|
650 | lemma minus_empty_r : ∀tag,A.∀s:identifier_map tag A. s ∖ ∅ = s. |
---|
651 | #tag #A * * [//] *[2:#x]#l#r normalize |
---|
652 | >map_opt_id >map_opt_id // |
---|
653 | qed. |
---|
654 | |
---|
655 | lemma mem_set_union : ∀tag.∀i : identifier tag.∀s,s' : identifier_set tag. |
---|
656 | i ∈ (s ∪ s') = (i ∈ s ∨ i ∈ s'). |
---|
657 | #tag * #i * #s * #s' normalize |
---|
658 | >lookup_opt_merge [2: @refl] |
---|
659 | elim (lookup_opt ???) |
---|
660 | elim (lookup_opt ???) |
---|
661 | normalize // qed. |
---|
662 | |
---|
663 | lemma mem_set_minus : ∀tag,A,B.∀i : identifier tag.∀s : identifier_map tag A. |
---|
664 | ∀s' : identifier_map tag B. |
---|
665 | i ∈ (s ∖ s') = (i ∈ s ∧ ¬ i ∈ s'). |
---|
666 | #tag #A #B * #i * #s * #s' normalize |
---|
667 | >lookup_opt_merge [2: @refl] |
---|
668 | elim (lookup_opt ???) |
---|
669 | elim (lookup_opt ???) |
---|
670 | normalize // qed. |
---|
671 | |
---|
672 | lemma set_eq_ext_node : ∀tag.∀o,o',l,l',r,r'. |
---|
673 | an_id_map tag ? (pm_node ? o l r) ≅ an_id_map … (pm_node ? o' l' r') → |
---|
674 | o = o' ∧ an_id_map tag ? l ≅ an_id_map … l' ∧ an_id_map tag ? r ≅ an_id_map … r'. |
---|
675 | #tag#o#o'#l#l'#r#r'#H |
---|
676 | %[ |
---|
677 | %[ lapply (H (an_identifier ? one)) |
---|
678 | elim o [2: *] elim o' [2,4: *] normalize // #EQ destruct |
---|
679 | | *#p lapply (H (an_identifier ? (p0 p))) normalize // |
---|
680 | ]| *#p lapply (H (an_identifier ? (p1 p))) normalize // |
---|
681 | ] |
---|
682 | qed. |
---|
683 | |
---|
684 | lemma set_eq_ext_leaf : ∀tag,A.∀o,l,r. |
---|
685 | (∀i.i∈an_id_map tag A (pm_node ? o l r) = false) → |
---|
686 | o = None ? ∧ (∀i.i∈an_id_map tag ? l = false) ∧ (∀i.i∈an_id_map tag ? r = false). |
---|
687 | #tag#A#o#l#r#H |
---|
688 | %[ |
---|
689 | %[ lapply (H (an_identifier ? one)) |
---|
690 | elim o [2: #a] normalize // #EQ destruct |
---|
691 | | *#p lapply (H (an_identifier ? (p0 p))) normalize // |
---|
692 | ]| *#p lapply (H (an_identifier ? (p1 p))) normalize // |
---|
693 | ] |
---|
694 | qed. |
---|
695 | |
---|
696 | |
---|
697 | definition id_map_size : ∀tag : String.∀A. identifier_map tag A → ℕ ≝ |
---|
698 | λtag,A,s.match s with [an_id_map p ⇒ |p|]. |
---|
699 | |
---|
700 | interpretation "identifier map domain size" 'norm s = (id_map_size ?? s). |
---|
701 | |
---|
702 | lemma set_eq_ext_empty_to_card : ∀tag,A.∀s : identifier_map tag A. (∀i.i∈s = false) → |s| = 0. |
---|
703 | #tag#A * #s elim s [//] |
---|
704 | #o#l#r normalize in ⊢((?→%)→(?→%)→?); #Hil #Hir #H |
---|
705 | elim (set_eq_ext_leaf … H) * #EQ destruct #Hl #Hr normalize |
---|
706 | >(Hil Hl) >(Hir Hr) // qed. |
---|
707 | |
---|
708 | lemma set_eq_ext_to_card : ∀tag.∀s,s' : identifier_set tag. s ≅ s' → |s| = |s'|. |
---|
709 | #tag *#s elim s |
---|
710 | [** [//] #o#l#r #H |
---|
711 | >(set_eq_ext_empty_to_card … (std_symm … H)) // |
---|
712 | | #o#l#r normalize in ⊢((?→?→??%?)→(?→?→??%?)→?); |
---|
713 | #Hil #Hir ** |
---|
714 | [#H @(set_eq_ext_empty_to_card … H)] |
---|
715 | #o'#l'#r' #H elim (set_eq_ext_node … H) * #EQ destruct(EQ) #Hl #Hr |
---|
716 | normalize >(Hil ? Hl) >(Hir ? Hr) // |
---|
717 | ] qed. |
---|
718 | |
---|
719 | lemma add_size: ∀tag,A,s,i,x. |
---|
720 | |add tag A s i x| = (if i ∈ s then 0 else 1) + |s|. |
---|
721 | #tag #A *#s *#i #x |
---|
722 | lapply (insert_size ? i x s) |
---|
723 | lapply (refl ? (lookup_opt ? i s)) |
---|
724 | generalize in ⊢ (???%→?); * [2: #x'] |
---|
725 | normalize #EQ >EQ normalize // |
---|
726 | qed. |
---|
727 | |
---|
728 | lemma mem_set_O_lt_card : ∀tag,A.∀i.∀s : identifier_map tag A. i ∈ s → |s| > 0. |
---|
729 | #tag #A * #i * #s normalize #H |
---|
730 | @(lookup_opt_O_lt_size … i) |
---|
731 | % #EQ >EQ in H; normalize * |
---|
732 | qed. |
---|
733 | |
---|
734 | (* NB: no control on values if applied to maps *) |
---|
735 | definition set_subset ≝ λtag,A,B.λs : identifier_map tag A. |
---|
736 | λs' : identifier_map tag B. ∀i.i ∈ s → (bool_to_Prop (i ∈ s')). |
---|
737 | |
---|
738 | interpretation "identifier set subset" 'subseteq s s' = (set_subset ??? s s'). |
---|
739 | |
---|
740 | lemma add_subset : |
---|
741 | ∀tag,A,B.∀i : identifier tag.∀x.∀s : identifier_map ? A.∀s' : identifier_map ? B. |
---|
742 | i ∈ s' → s ⊆ s' → add … s i x ⊆ s'. |
---|
743 | #tag#A#B#i#x#s#s' #H #G #j |
---|
744 | >mem_set_add |
---|
745 | @eq_identifier_elim #H' [* >H' @H | #js @(G ? js)] |
---|
746 | qed. |
---|
747 | |
---|
748 | definition set_forall : ∀tag,A.(identifier tag → Prop) → |
---|
749 | identifier_map tag A → Prop ≝ λtag,A,P,m.∀i. i ∈ m → P i. |
---|
750 | |
---|
751 | lemma set_forall_add : ∀tag,P,m,i.set_forall tag ? P m → P i → |
---|
752 | set_forall tag ? P (add_set ? m i). |
---|
753 | #tag#P#m#i#Pm#Pi#j |
---|
754 | >mem_set_add |
---|
755 | @eq_identifier_elim |
---|
756 | [#EQ destruct(EQ) #_ @Pi |
---|
757 | |#_ @Pm |
---|
758 | ] |
---|
759 | qed. |
---|
760 | |
---|
761 | include "utilities/proper.ma". |
---|
762 | |
---|
763 | lemma minus_subset : ∀tag,A,B.minus_set tag A B ⊨ set_subset … ++> set_subset … -+> set_subset …. |
---|
764 | #tag#A#B#s#s' #H #s'' #s''' #G #i |
---|
765 | >mem_set_minus >mem_set_minus |
---|
766 | #H' elim (andb_Prop_true … H') -H' #is #nis'' |
---|
767 | >(H … is) |
---|
768 | elim (true_or_false_Prop (i∈s''')) |
---|
769 | [ #is''' >(G … is''') in nis''; * |
---|
770 | | #nis''' >nis''' % |
---|
771 | ] |
---|
772 | qed. |
---|
773 | |
---|
774 | lemma subset_node : ∀tag,A,B.∀o,o',l,l',r,r'. |
---|
775 | an_id_map tag A (pm_node ? o l r) ⊆ an_id_map tag B (pm_node ? o' l' r') → |
---|
776 | opt_All ? (λ_.o' ≠ None ?) o ∧ an_id_map tag ? l ⊆ an_id_map tag ? l' ∧ |
---|
777 | an_id_map tag ? r ⊆ an_id_map tag ? r'. |
---|
778 | #tag#A#B#o#o'#l#l'#r#r'#H |
---|
779 | %[% |
---|
780 | [ lapply (H (an_identifier ? (one))) elim o [2: #a] elim o' [2:#b] |
---|
781 | normalize // [#_ % #ABS destruct(ABS) | #G lapply (G I) *] |
---|
782 | | *#p lapply (H (an_identifier ? (p0 p))) |
---|
783 | ] |
---|
784 | | *#p lapply (H (an_identifier ? (p1 p))) |
---|
785 | ] #H @H |
---|
786 | qed. |
---|
787 | |
---|
788 | lemma subset_leaf : ∀tag,A.∀o,l,r. |
---|
789 | an_id_map tag A (pm_node ? o l r) ⊆ ∅ → |
---|
790 | o = None ? ∧ (∀i.i∈an_id_map tag ? l = false) ∧ (∀i.i∈an_id_map tag ? r = false). |
---|
791 | #tag#A#o#l#r#H |
---|
792 | %[ |
---|
793 | %[ lapply (H (an_identifier ? one)) |
---|
794 | elim o [2: #a] normalize // #EQ lapply(EQ I) * |
---|
795 | | *#p lapply (H (an_identifier ? (p0 p))) |
---|
796 | ] |
---|
797 | | *#p lapply (H (an_identifier ? (p1 p))) |
---|
798 | ] normalize elim (lookup_opt ? p ?) normalize |
---|
799 | // #a #H lapply (H I) * |
---|
800 | qed. |
---|
801 | |
---|
802 | lemma subset_card : ∀tag,A,B.∀s : identifier_map tag A.∀s' : identifier_map tag B. |
---|
803 | s ⊆ s' → |s| ≤ |s'|. |
---|
804 | #tag #A #B *#s elim s |
---|
805 | [ // |
---|
806 | | #o#l#r #Hil #Hir ** |
---|
807 | [ #H elim (subset_leaf … H) * #EQ >EQ #Hl #Hr |
---|
808 | lapply (set_eq_ext_empty_to_card … Hl) |
---|
809 | lapply (set_eq_ext_empty_to_card … Hr) |
---|
810 | normalize // |
---|
811 | | #o' #l' #r' #H elim (subset_node … H) * |
---|
812 | elim o [2: #a] elim o' [2,4: #a'] |
---|
813 | [3: #G normalize in G; elim(absurd ? (refl ??) G) |
---|
814 | |*: #_ #Hl #Hr lapply (Hil ? Hl) lapply (Hir ? Hr) |
---|
815 | normalize #H1 #H2 |
---|
816 | [@le_S_S | @(transitive_le … (|l'|+|r'|)) [2: / by /]] |
---|
817 | @le_plus assumption |
---|
818 | ] |
---|
819 | ] |
---|
820 | ] |
---|
821 | qed. |
---|
822 | |
---|
823 | lemma mem_set_empty : ∀tag,A.∀i: identifier tag. i∈empty_map tag A = false. |
---|
824 | #tag #A * #i normalize % |
---|
825 | qed. |
---|
826 | |
---|
827 | lemma mem_set_singl_to_eq : ∀tag.∀i,j : identifier tag.i∈{(j)} → i = j. |
---|
828 | #tag |
---|
829 | #i #j >mem_set_add >mem_set_empty |
---|
830 | #H elim (orb_true_l … H) -H |
---|
831 | [@eq_identifier_elim [//] #_] #EQ destruct |
---|
832 | qed. |
---|
833 | |
---|
834 | lemma subset_add_set : ∀tag,i,s.s ⊆ add_set tag s i. |
---|
835 | #tag#i#s#j #H >mem_set_add >H |
---|
836 | >commutative_orb % |
---|
837 | qed. |
---|
838 | |
---|
839 | lemma add_set_monotonic : ∀tag,i,s,s'.s ⊆ s' → add_set tag s i ⊆ add_set tag s' i. |
---|
840 | #tag#i#s#s' #H #j >mem_set_add >mem_set_add |
---|
841 | @orb_elim elim (eq_identifier ???) |
---|
842 | whd lapply (H j) /2 by / |
---|
843 | qed. |
---|
844 | |
---|
845 | lemma transitive_subset : ∀tag,A.transitive ? (set_subset tag A A). |
---|
846 | #tag#A#s#s'#s''#H#G#i #is |
---|
847 | @(G … (H … is)) |
---|
848 | qed. |
---|
849 | |
---|
850 | definition set_from_list : ∀tag.list (identifier tag) → identifier_map tag unit ≝ |
---|
851 | λtag.foldl … (add_set ?) ∅. |
---|
852 | |
---|
853 | coercion id_set_from_list : ∀tag.∀l : list (identifier tag).identifier_map tag unit ≝ |
---|
854 | set_from_list on _l : list (identifier ?) to identifier_map ? unit. |
---|
855 | |
---|
856 | lemma mem_map_domain : ∀tag,A.∀m : identifier_map tag A.∀i. |
---|
857 | i∈m → lookup … m i ≠ None ?. |
---|
858 | #tag#A * #m #i |
---|
859 | whd in match (i∈?); |
---|
860 | elim (lookup ????) normalize [2: #x] |
---|
861 | * % #EQ destruct(EQ) |
---|
862 | qed. |
---|
863 | |
---|
864 | |
---|
865 | |
---|
866 | lemma mem_list_as_set : ∀tag.∀l : list (identifier tag). |
---|
867 | ∀i.i ∈ l → In ? l i. |
---|
868 | #tag #l @(list_elim_left … l) |
---|
869 | [ #i * |
---|
870 | | #t #h #Hi #i |
---|
871 | whd in ⊢ (?(???%?)→?); |
---|
872 | >foldl_append |
---|
873 | whd in ⊢ (?(???%?)→?); |
---|
874 | >mem_set_add |
---|
875 | @eq_identifier_elim |
---|
876 | [ #EQi destruct(EQi) |
---|
877 | #_ @Exists_append_r % % |
---|
878 | | #_ #H @Exists_append_l @Hi assumption |
---|
879 | ] |
---|
880 | ] |
---|
881 | qed. |
---|
882 | |
---|
883 | lemma list_as_set_mem : ∀tag.∀l : list (identifier tag). |
---|
884 | ∀i.In ? l i → i ∈ l. |
---|
885 | #tag #l @(list_elim_left … l) |
---|
886 | [ #i * |
---|
887 | | #t #h #Hi #i #H |
---|
888 | whd in ⊢ (?(???%?)); |
---|
889 | >foldl_append |
---|
890 | whd in ⊢ (?(???%?)); |
---|
891 | elim (Exists_append … H) -H |
---|
892 | [ #H >mem_set_add |
---|
893 | @eq_identifier_elim [//] #_ normalize |
---|
894 | @Hi @H |
---|
895 | | * [2: *] #EQi destruct(EQi) >mem_set_add_id % |
---|
896 | ] |
---|
897 | ] |
---|
898 | qed. |
---|
899 | |
---|
900 | lemma list_as_set_All : ∀tag,P.∀ l : list (identifier tag). |
---|
901 | (∀i.i ∈ l → P i) → All ? P l. |
---|
902 | #tag #P #l @(list_elim_left … l) |
---|
903 | [ #_ % |
---|
904 | | #x #l' #Hi |
---|
905 | whd in match (set_from_list … (l'@[x])); |
---|
906 | >foldl_append |
---|
907 | #H @All_append |
---|
908 | [ @Hi #i #G @H |
---|
909 | whd in ⊢ (?(???%?)); |
---|
910 | >mem_set_add @orb_Prop_r @G |
---|
911 | | % [2: %] |
---|
912 | @H |
---|
913 | whd in ⊢ (?(???%?)); |
---|
914 | @mem_set_add_id |
---|
915 | ] |
---|
916 | ] |
---|
917 | qed. |
---|
918 | |
---|
919 | lemma All_list_as_set : ∀tag,P.∀ l : list (identifier tag). |
---|
920 | All ? P l → ∀i.i ∈ l → P i. |
---|
921 | #tag #P #l @(list_elim_left … l) |
---|
922 | [ * #i * |
---|
923 | | #x #l' #Hi #H |
---|
924 | lapply (All_append_l … H) |
---|
925 | lapply (All_append_r … H) |
---|
926 | * #Px * #Pl' #i |
---|
927 | whd in match (set_from_list … (l'@[x])); |
---|
928 | >foldl_append |
---|
929 | >mem_set_add |
---|
930 | @eq_identifier_elim |
---|
931 | [ #EQx >EQx #_ @Px |
---|
932 | | #_ whd in match (?∨?); @Hi @Pl' |
---|
933 | ] |
---|
934 | ] |
---|
935 | qed. |
---|
936 | |
---|
937 | lemma map_mem_prop : |
---|
938 | ∀tag,A.∀m : identifier_map tag A.∀i. |
---|
939 | lookup ?? m i ≠ None ? → i ∈ m. |
---|
940 | #p #globals #m #i |
---|
941 | lapply (in_map_domain … m i) |
---|
942 | cases (i∈m) |
---|
943 | [ * #x #_ #_ % |
---|
944 | | #EQ >EQ * #ABS @ABS % |
---|
945 | ] qed. |
---|
946 | |
---|
947 | |
---|
948 | (* Attempt to choose an entry in the map/set, and if successful return the entry |
---|
949 | and the map/set without it. *) |
---|
950 | |
---|
951 | definition choose : ∀tag,A. identifier_map tag A → option (identifier tag × A × (identifier_map tag A)) ≝ |
---|
952 | λtag,A,m. |
---|
953 | match pm_choose A (match m with [ an_id_map m' ⇒ m' ]) with |
---|
954 | [ None ⇒ None ? |
---|
955 | | Some x ⇒ Some ? 〈〈an_identifier tag (\fst (\fst x)), \snd (\fst x)〉, an_id_map tag A (\snd x)〉 |
---|
956 | ]. |
---|
957 | |
---|
958 | lemma choose_empty : ∀tag,A,m. |
---|
959 | choose tag A m = None ? ↔ ∀id. lookup tag A m id = None ?. |
---|
960 | #tag #A * #m lapply (pm_choose_empty A m) * #H1 #H2 % |
---|
961 | [ normalize #C * @H1 cases (pm_choose A m) in C ⊢ %; [ // | normalize #x #E destruct ] |
---|
962 | | normalize #L lapply (pm_choose_empty A m) cases (pm_choose A m) |
---|
963 | [ * #H1 #H2 normalize // | #x * #_ #H lapply (H ?) [ #p @(L (an_identifier ? p)) | #E destruct ] ] |
---|
964 | ] qed. |
---|
965 | |
---|
966 | lemma choose_some : ∀tag,A,m,id,a,m'. |
---|
967 | choose tag A m = Some ? 〈〈id,a〉,m'〉 → |
---|
968 | lookup tag A m id = Some A a ∧ |
---|
969 | lookup tag A m' id = None A ∧ |
---|
970 | (∀id'. id = id' ∨ lookup tag A m id' = lookup tag A m' id'). |
---|
971 | #tag #A * #m * #id #a * #m' #C |
---|
972 | lapply (pm_choose_some A m id a m' ?) |
---|
973 | [ whd in C:(??%?); cases (pm_choose A m) in C ⊢ %; normalize [ #E destruct | * * #x #y #z #E destruct % ] ] |
---|
974 | * * * #L1 #L2 #L3 #_ |
---|
975 | % [ % [ @L1 | @L2 ] | * #id' cases (L3 id') [ /2/ | #L4 %2 @L4 ] ] |
---|
976 | qed. |
---|
977 | |
---|
978 | lemma choose_some_subset : ∀tag,A,m,id,a,m'. |
---|
979 | choose tag A m = Some ? 〈〈id,a〉,m'〉 → |
---|
980 | m' ⊆ m. |
---|
981 | #tag #A #m #id #a #m' #C |
---|
982 | cases (choose_some … m' C) * #L1 #L2 #L3 |
---|
983 | #id' whd in ⊢ (?% → ?%); |
---|
984 | cases (L3 id') |
---|
985 | [ #E destruct >L2 * |
---|
986 | | #L4 >L4 // |
---|
987 | ] qed. |
---|
988 | |
---|
989 | lemma choose_some_card : ∀tag,A,m,id,a,m'. |
---|
990 | choose tag A m = Some ? 〈〈id,a〉,m'〉 → |
---|
991 | |m| = S (|m'|). |
---|
992 | #tag #A * #m * #id #a * #m' #C |
---|
993 | lapply (pm_choose_some A m id a m' ?) |
---|
994 | [ whd in C:(??%?); cases (pm_choose A m) in C ⊢ %; normalize [ #E destruct | * * #x #y #z #E destruct % ] ] |
---|
995 | * #_ #H @H |
---|
996 | qed. |
---|
997 | |
---|
998 | (* Remove an element from a map/set, returning the element and a new map/set. *) |
---|
999 | |
---|
1000 | definition try_remove : ∀tag,A. identifier_map tag A → identifier tag → option (A × (identifier_map tag A)) ≝ |
---|
1001 | λtag,A,m,id. |
---|
1002 | match pm_try_remove A (match id with [ an_identifier id' ⇒ id']) (match m with [ an_id_map m' ⇒ m' ]) with |
---|
1003 | [ None ⇒ None ? |
---|
1004 | | Some x ⇒ Some ? 〈\fst x, an_id_map tag A (\snd x)〉 |
---|
1005 | ]. |
---|
1006 | |
---|
1007 | lemma try_remove_empty : ∀tag,A,m,id. |
---|
1008 | try_remove tag A m id = None ? ↔ lookup tag A m id = None ?. |
---|
1009 | #tag #A * #m * #id lapply (pm_try_remove_none A id m) * #H1 #H2 % |
---|
1010 | [ normalize #C @H1 cases (pm_try_remove A id m) in C ⊢ %; [ // | normalize #x #E destruct ] |
---|
1011 | | normalize #L >H2 // |
---|
1012 | ] qed. |
---|
1013 | |
---|
1014 | lemma try_remove_some : ∀tag,A,m,id,a,m'. |
---|
1015 | try_remove tag A m id = Some ? 〈a,m'〉 → |
---|
1016 | lookup tag A m id = Some A a ∧ |
---|
1017 | lookup tag A m' id = None A ∧ |
---|
1018 | (∀id'. id = id' ∨ lookup tag A m id' = lookup tag A m' id'). |
---|
1019 | #tag #A * #m * #id #a * #m' #C |
---|
1020 | lapply (pm_try_remove_some A id m a m' ?) |
---|
1021 | [ whd in C:(??%?); cases (pm_try_remove A id m) in C ⊢ %; normalize [ #E destruct | * #x #y #E destruct % ] ] |
---|
1022 | * * * #L1 #L2 #L3 #_ |
---|
1023 | % [ % [ @L1 | @L2 ] | * #id' cases (L3 id') [ /2/ | #L4 %2 @L4 ] ] |
---|
1024 | qed. |
---|
1025 | |
---|
1026 | lemma try_remove_some_card : ∀tag,A,m,id,a,m'. |
---|
1027 | try_remove tag A m id = Some ? 〈a,m'〉 → |
---|
1028 | |m| = S (|m'|). |
---|
1029 | #tag #A * #m * #id #a * #m' #C |
---|
1030 | lapply (pm_try_remove_some A id m a m' ?) |
---|
1031 | [ whd in C:(??%?); cases (pm_try_remove A id m) in C ⊢ %; normalize [ #E destruct | * #x #y #E destruct % ] ] |
---|
1032 | * #_ #H @H |
---|
1033 | qed. |
---|
1034 | |
---|
1035 | lemma try_remove_this : ∀tag,A,m,id,a. |
---|
1036 | lookup tag A m id = Some A a → |
---|
1037 | ∃m'. try_remove tag A m id = Some ? 〈a,m'〉. |
---|
1038 | #tag #A * #m * #id #a #L |
---|
1039 | cases (pm_try_remove_some' A id m a L) |
---|
1040 | #m' #R %{(an_id_map tag A m')} whd in ⊢ (??%?); >R % |
---|
1041 | qed. |
---|
1042 | |
---|
1043 | (* Link a map with the set consisting of its domain. *) |
---|
1044 | |
---|
1045 | definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝ |
---|
1046 | λtag,A,m. an_id_map tag unit (map … (λ_. it) (match m with [ an_id_map m' ⇒ m'])). |
---|
1047 | |
---|
1048 | lemma id_set_of_map_subset : ∀tag,A,m. |
---|
1049 | id_set_of_map tag A m ⊆ m. |
---|
1050 | #tag #A * #m * #id normalize |
---|
1051 | >lookup_opt_map normalize cases (lookup_opt ???) // |
---|
1052 | qed. |
---|
1053 | |
---|
1054 | lemma id_set_of_map_present : ∀tag,A,m,id. |
---|
1055 | present tag A m id ↔ present tag unit (id_set_of_map … m) id. |
---|
1056 | #tag #A * #m * #id % |
---|
1057 | normalize @not_to_not |
---|
1058 | >lookup_opt_map cases (lookup_opt ???) normalize // |
---|
1059 | #a #E destruct |
---|
1060 | qed. |
---|
1061 | |
---|
1062 | lemma id_set_of_map_card : ∀tag,A,m. |
---|
1063 | |m| = |id_set_of_map tag A m|. |
---|
1064 | #tag #A * #m whd in ⊢ (??%%); >map_size // |
---|
1065 | qed. |
---|
1066 | |
---|
1067 | |
---|
1068 | (* Transforming a list into a set. *) |
---|
1069 | |
---|
1070 | definition set_of_list : ∀tag. list (identifier tag) → identifier_set tag ≝ |
---|
1071 | λtag,l. foldl ?? (λs,id. add_set tag s id) ∅ l. |
---|
1072 | |
---|
1073 | lemma fold_add_set_monotone : ∀tag,l,s,id. |
---|
1074 | present tag unit s id → |
---|
1075 | present tag unit (foldl ?? (λs,id. add_set tag s id) s l) id. |
---|
1076 | #tag #l elim l |
---|
1077 | [ // |
---|
1078 | | #h #t #IH #s #id #PR |
---|
1079 | whd in ⊢ (???%?); @IH |
---|
1080 | @lookup_add_oblivious |
---|
1081 | @PR |
---|
1082 | ] qed. |
---|
1083 | |
---|
1084 | lemma in_set_of_list : ∀tag,l,id. |
---|
1085 | Exists ? (λid'. id' = id) l → |
---|
1086 | present ?? (set_of_list tag l) id. |
---|
1087 | #tag #l #id whd in match (set_of_list ??); generalize in match ∅; elim l |
---|
1088 | [ #s * |
---|
1089 | | #id' #tl #IH #s * |
---|
1090 | [ #E whd in ⊢ (???%?); destruct |
---|
1091 | @fold_add_set_monotone // |
---|
1092 | | @IH |
---|
1093 | ] |
---|
1094 | ] qed. |
---|
1095 | |
---|
1096 | lemma in_set_of_list' : ∀tag,l,id. |
---|
1097 | present ?? (set_of_list tag l) id → |
---|
1098 | Exists ? (λid'. id = id') l. |
---|
1099 | #tag #l #id whd in match (set_of_list ??); |
---|
1100 | cut (¬present ?? ∅ id) [ /3/ ] |
---|
1101 | generalize in match ∅; |
---|
1102 | elim l |
---|
1103 | [ #s #F #T @⊥ @(absurd … T F) |
---|
1104 | | #id' #tl #IH #s #F #PR whd in PR:(???%?); |
---|
1105 | cases (identifier_eq … id id') |
---|
1106 | [ #E destruct /2/ |
---|
1107 | | #NE %2 @(IH … PR) |
---|
1108 | @(not_to_not … F) /2/ |
---|
1109 | ] |
---|
1110 | ] qed. |
---|
1111 | |
---|
1112 | |
---|
1113 | |
---|