source: src/common/Identifiers.ma @ 2768

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