source: src/common/Identifiers.ma @ 2418

Last change on this file since 2418 was 2418, checked in by campbell, 8 years ago

Add a checking function for the uniqueness of cost labels in RTLabs
programs.

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