source: src/common/Identifiers.ma @ 1882

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

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

File size: 23.4 KB
Line 
1include "basics/types.ma".
2include "ASM/String.ma".
3include "utilities/binary/positive.ma".
4include "utilities/lists.ma".
5include "utilities/extralib.ma".
6include "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.
12inductive identifier (tag:String) : Type[0] ≝
13  an_identifier : Pos → identifier tag.
14*)
15
16record universe (tag:String) : Type[0] ≝
17{
18  next_identifier : Pos
19}.
20
21definition new_universe : ∀tag:String. universe tag ≝
22  λtag. mk_universe tag one.
23
24let 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
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'.
43#tag * #id * #id' * #u * #u' normalize #H #E destruct /2 by le_S/
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'.
50#tag * #id * #id' * #u * #u' normalize #H #E destruct % #E' destruct /2 by absurd/
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
62#H #E whd % [ @(fresh_is_fresh … E) | @(All_mp … H) * #id #a #H' /2 by fresh_remains_fresh/ ]
63qed.
64
65definition 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
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
79change with (P (eqb ??))
80@(eqb_elim x y P) [ /2 by / | * #H @F % #E destruct /2 by / ]
81qed.
82   
83definition word_of_identifier ≝
84  λt.
85  λl: identifier t.
86  match l with   
87  [ an_identifier l' ⇒ l'
88  ].
89
90lemma eq_identifier_refl : ∀tag,id. eq_identifier tag id id = true.
91#tag * #id whd in ⊢ (??%?); >eqb_n_n @refl
92qed.
93
94axiom eq_identifier_sym:
95  ∀tag: String.
96  ∀l  : identifier tag.
97  ∀r  : identifier tag.
98    eq_identifier tag l r = eq_identifier tag r l.
99
100lemma eq_identifier_false : ∀tag,x,y. x≠y → eq_identifier tag x y = false.
101#tag * #x * #y #NE normalize @not_eq_to_eqb_false /2 by not_to_not/
102qed.
103
104definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
105#tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %);
106#E [ % | %2 ]
107lapply E @eqb_elim
108[ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2 by absurd/ ]
109qed.
110
111definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
112  λtag,n. an_identifier tag (succ_pos_of_nat  n).
113
114
115(* States that all identifiers in an environment are distinct from one another. *)
116let rec distinct_env tag (A:Type[0]) (l:list (identifier tag × A)) on l : Prop ≝
117match l with
118[ nil ⇒ True
119| cons hd tl ⇒ All ? (λia. \fst hd ≠ \fst ia) tl ∧
120               distinct_env tag A tl
121].
122
123lemma distinct_env_append_l : ∀tag,A,l,r. distinct_env tag A (l@r) → distinct_env tag A l.
124#tag #A #l elim l
125[ //
126| * #id #a #tl #IH #r * #H1 #H2 % /2 by All_append_l/
127] qed.
128
129lemma distinct_env_append_r : ∀tag,A,l,r. distinct_env tag A (l@r) → distinct_env tag A r.
130#tag #A #l elim l
131[ //
132| * #id #a #tl #IH #r * #H1 #H2 /2 by /
133] qed.
134
135(* check_distinct_env is quadratic - we could pay more attention when building maps to make sure that
136   the original environment was distinct. *)
137
138axiom DuplicateVariable : String.
139
140let 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) ≝
141match l return λl.res (All ?? l) with
142[ nil ⇒ OK ? I
143| cons hd tl ⇒
144    match identifier_eq tag id (\fst hd) with
145    [ inl _ ⇒ Error ? [MSG DuplicateVariable; CTX ? id]
146    | inr NE ⇒
147        do Htl ← check_member_env tag A id tl;
148        OK ? (conj ?? NE Htl)
149    ]
150].
151
152let rec check_distinct_env tag (A:Type[0]) (l:list (identifier tag × A)) on l : res (distinct_env tag A l) ≝
153match l return λl.res (distinct_env tag A l) with
154[ nil ⇒ OK ? I
155| cons hd tl ⇒
156    do Hhd ← check_member_env tag A (\fst hd) tl;
157    do Htl ← check_distinct_env tag A tl;
158    OK ? (conj ?? Hhd Htl)
159].
160
161
162
163
164(* Maps from identifiers to arbitrary types. *)
165
166include "common/PositiveMap.ma".
167
168inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝
169  an_id_map : positive_map A → identifier_map tag A.
170 
171definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
172  λtag,A. an_id_map tag A (pm_leaf A).
173
174let rec lookup tag A (m:identifier_map tag A) (l:identifier tag) on m : option A ≝
175  lookup_opt A (match l with [ an_identifier l' ⇒ l' ])
176               (match m with [ an_id_map m' ⇒ m' ]).
177
178definition lookup_def ≝
179λtag,A,m,l,d. match lookup tag A m l with [ None ⇒ d | Some x ⇒ x].
180
181let rec member tag A (m:identifier_map tag A) (l:identifier tag) on m : bool ≝
182  match lookup tag A m l with [ None ⇒ false | _ ⇒ true ].
183
184(* Always adds the identifier to the map. *)
185let rec add tag A (m:identifier_map tag A) (l:identifier tag) (a:A) on m : identifier_map tag A ≝
186  an_id_map tag A (insert A (match l with [ an_identifier l' ⇒ l' ]) a
187                            (match m with [ an_id_map m' ⇒ m' ])).
188
189lemma lookup_add_hit : ∀tag,A,m,i,a.
190  lookup tag A (add tag A m i a) i = Some ? a.
191#tag #A * #m * #i #a
192@lookup_opt_insert_hit
193qed.
194
195lemma lookup_def_add_hit : ∀tag,A,m,i,a,d.
196  lookup_def tag A (add tag A m i a) i d = a.
197#tag #A * #m * #i #a #d
198@lookup_insert_hit
199qed.
200
201lemma lookup_add_miss : ∀tag,A,m,i,j,a.
202  i ≠ j →
203  lookup tag A (add tag A m j a) i = lookup tag A m i.
204#tag #A * #m * #i * #j #a #H
205@lookup_opt_insert_miss /2 by not_to_not/
206qed.
207
208axiom lookup_def_add_miss : ∀tag,A,m,i,j,a,d.
209  i ≠ j →
210  lookup_def tag A (add tag A m j a) i d = lookup_def tag A m i d.
211
212lemma lookup_add_oblivious : ∀tag,A,m,i,j,a.
213  (lookup tag A m i ≠ None ?) →
214  lookup tag A (add tag A m j a) i ≠ None ?.
215#tag #A #m #i #j #a #H
216cases (identifier_eq ? i j)
217[ #E >E >lookup_add_hit % #N destruct
218| #NE >lookup_add_miss //
219] qed.
220
221lemma lookup_add_cases : ∀tag,A,m,i,j,a,v.
222  lookup tag A (add tag A m i a) j = Some ? v →
223  (i=j ∧ v = a) ∨ lookup tag A m j = Some ? v.
224#tag #A #m #i #j #a #v
225cases (identifier_eq ? i j)
226[ #E >E >lookup_add_hit #H %1 destruct % //
227| #NE >lookup_add_miss /2 by or_intror, sym_not_eq/
228] qed.
229
230(* Extract every identifier, value pair from the map. *)
231definition elements : ∀tag,A. identifier_map tag A → list (identifier tag × A) ≝
232λtag,A,m.
233  fold ?? (λl,a,el. 〈an_identifier tag l, a〉::el)
234          (match m with [ an_id_map m' ⇒ m' ]) [ ].
235
236axiom MissingId : String.
237
238(* Only updates an existing entry; fails with an error otherwise. *)
239definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
240λtag,A,m,l,a.
241  match update A (match l with [ an_identifier l' ⇒ l' ]) a
242                 (match m with [ an_id_map m' ⇒ m' ]) with
243  [ None ⇒ Error ? ([MSG MissingId; CTX tag l]) (* missing identifier *)
244  | Some m' ⇒ OK ? (an_id_map tag A m')
245  ].
246
247definition foldi:
248  ∀A, B: Type[0].
249  ∀tag: String.
250  (identifier tag -> A -> B -> B) -> identifier_map tag A -> B -> B ≝
251λA,B,tag,f,m,b.
252  match m with
253  [ an_id_map m' ⇒ fold A B (λbv. f (an_identifier ? bv)) m' b ].
254
255(* A predicate that an identifier is in a map, and a failure-avoiding lookup
256   and update using it. *)
257
258definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
259λtag,A,m,i. lookup … m i ≠ None ?.
260
261lemma member_present : ∀tag,A,m,id.
262  member tag A m id = true → present tag A m id.
263#tag #A * #m #id normalize cases (lookup_opt A ??) normalize
264[ #E destruct
265| #x #E % #E' destruct
266] qed.
267
268include "ASM/Util.ma".
269
270definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝
271λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ].
272cases H #H'  cases (H' (refl ??)) qed.
273
274lemma lookup_lookup_present : ∀tag,A,m,id,p.
275  lookup tag A m id = Some ? (lookup_present tag A m id p).
276#tag #A #m #id #p
277whd in p ⊢ (???(??%));
278cases (lookup tag A m id) in p ⊢ %;
279[ * #H @⊥ @H @refl
280| #a #H @refl
281] qed.
282
283definition update_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A → identifier_map tag A ≝
284λtag,A,m,l,p,a.
285  let l' ≝ match l with [ an_identifier l' ⇒ l' ] in
286  let m' ≝ match m with [ an_id_map m' ⇒ m' ] in
287  let u' ≝ update A l' a m' in
288  match u' return λx. update ???? = x → ? with
289  [ None ⇒ λE.⊥
290  | Some m' ⇒ λ_. an_id_map tag A m'
291  ] (refl ? u').
292cases l in p E; cases m; -l' -m' #m' #l'
293whd in ⊢ (% → ?);
294 whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?);
295#NL #U cases NL #H @H @(update_fail … U)
296qed.
297
298lemma update_still_present : ∀tag,A,m,id,a,id'.
299  ∀H:present tag A m id.
300  ∀H':present tag A m id'.
301  present tag A (update_present tag A m id' H' a) id.
302#tag #A * #m * #id #a * #id' #H #H'
303whd whd in ⊢ (?(??(???(%??????)?)?)); normalize nodelta
304cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id'))
305[ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); >(update_lookup_opt_same ????? U)
306  % #E' destruct
307| #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); whd in ⊢ (?(??(??%%)?));
308  <(update_lookup_opt_other ????? U id) [ @H | % #E cases NE >E #H @H @refl ]
309] qed.
310
311
312let rec fresh_for_map tag A (id:identifier tag) (m:identifier_map tag A) on id : Prop ≝
313  lookup … m id = None A.
314
315lemma fresh_for_empty_map : ∀tag,A,id.
316  fresh_for_map tag A id (empty_map tag A).
317#tag #A * #id //
318qed.
319
320definition fresh_map_for_univ ≝
321λtag,A. λm:identifier_map tag A. λu:universe tag.
322  ∀id. present tag A m id → fresh_for_univ tag id u.
323
324lemma fresh_fresh_for_map : ∀tag,A,m,id,u,u'.
325  fresh_map_for_univ tag A m u →
326  〈id,u'〉 = fresh tag u →
327  fresh_for_map tag A id m.
328#tag #A * #m * #id * #u * #u' whd in ⊢ (% → ???% → %);
329#FMU #E destruct lapply (FMU (an_identifier tag u)) whd in ⊢ ((% → %) → ?);
330generalize in ⊢ ((?(??%?) → ?) → ??%?); *
331[ // | #a #H @False_ind lapply (H ?) /2 by absurd/ % #E destruct
332qed.
333
334lemma fresh_map_preserved : ∀tag,A,m,u,u',id.
335  fresh_map_for_univ tag A m u →
336  〈id,u'〉 = fresh tag u →
337  fresh_map_for_univ tag A m u'.
338#tag #A #m #u * #u' #id whd in ⊢ (% → ? → %); #H #E
339#id' #PR @(fresh_remains_fresh … E) @H //
340qed.
341
342lemma fresh_map_add : ∀tag,A,m,u,id,a.
343  fresh_map_for_univ tag A m u →
344  fresh_for_univ tag id u →
345  fresh_map_for_univ tag A (add tag A m id a) u.
346#tag #A * #m #u #id #a #Hm #Hi
347#id' #PR cases (identifier_eq tag id' id)
348[ #E >E @Hi
349| #NE @Hm whd in PR;
350  change with (add tag A (an_id_map tag A m) id a) in PR:(?(??(???%?)?));
351  >lookup_add_miss in PR; //
352] qed.
353
354lemma present_not_fresh : ∀tag,A,m,id,id'.
355  present tag A m id →
356  fresh_for_map tag A id' m →
357  id ≠ id'.
358#tag #A #m #id * #id' whd in ⊢ (% → % → ?);
359* #NE #E % #E' destruct @(NE E)
360qed.
361
362lemma fresh_for_map_add : ∀tag,A,id,m,id',a.
363  id ≠ id' →
364  fresh_for_map tag A id m →
365  fresh_for_map tag A id (add tag A m id' a).
366#tag #A * #id #m #id' #a #NE #F
367whd >lookup_add_miss //
368qed.
369
370
371(* Sets *)
372
373definition identifier_set ≝ λtag.identifier_map tag unit.
374
375definition empty_set : ∀tag.identifier_set tag ≝ λtag.empty_map ….
376
377
378definition add_set : ∀tag.identifier_set tag → identifier tag → identifier_set tag ≝
379  λtag,s,i.add … s i it.
380
381definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
382λtag,i. add_set tag (empty_set tag) i.
383
384(* mem set is generalised to all maps *)
385let rec mem_set (tag:String) A (s:identifier_map tag A) (i:identifier tag) on s : bool ≝
386  match lookup … s i with
387  [ None ⇒ false
388  | Some _ ⇒ true
389  ].
390 
391let rec union_set (tag:String) A B (s:identifier_map tag A) (s':identifier_map tag B) on s : identifier_set tag ≝
392  an_id_map tag unit (merge … (λo,o'.match o with [Some _ ⇒ Some ? it | None ⇒ !_ o'; return it])
393    (match s with [ an_id_map s0 ⇒ s0 ])
394    (match s' with [ an_id_map s1 ⇒ s1 ])).
395
396
397(* set minus is generalised to maps *)
398let rec minus_set (tag:String) A B (s:identifier_map tag A) (s':identifier_map tag B) on s : identifier_map tag A ≝
399  an_id_map tag A (merge A B A (λo,o'.match o' with [None ⇒ o | Some _ ⇒ None ?])
400    (match s with [ an_id_map s0 ⇒ s0 ])
401    (match s' with [ an_id_map s1 ⇒ s1 ])).
402
403notation "a ∖ b" left associative with precedence 50 for @{'setminus $a $b}.
404
405interpretation "identifier set union" 'union a b = (union_set ??? a b).
406notation "∅" non associative with precedence 90 for @{ 'empty }.
407interpretation "empty identifier set" 'empty = (empty_set ?).
408interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a).
409interpretation "identifier set membership" 'mem a b = (mem_set ?? b a).
410interpretation "identifier map difference" 'setminus a b = (minus_set ??? a b).
411
412definition IdentifierSet : String → Setoid ≝ λtag.
413  mk_Setoid (identifier_set tag) (λs,s'.∀i.i ∈ s = (i ∈ s')) ???.
414  // qed.
415
416unification hint 0 ≔ tag;
417S ≟ IdentifierSet tag
418(*-----------------------------*)⊢
419identifier_set tag ≡ std_supp S.
420unification hint 0 ≔ tag;
421S ≟ IdentifierSet tag
422(*-----------------------------*)⊢
423identifier_map tag unit ≡ std_supp S.
424
425lemma mem_set_add : ∀tag,A.∀i,j : identifier tag.∀s,x.
426  i ∈ add ? A s j x = (eq_identifier ? i j ∨ i ∈ s).
427#tag #A *#i *#j *#s #x normalize
428@(eqb_elim i j)
429[#EQ destruct
430  >(lookup_opt_insert_hit A x j)
431|#NEQ >(lookup_opt_insert_miss … s NEQ)
432] elim (lookup_opt  A j s) normalize // qed.
433
434lemma mem_set_add_id : ∀tag,A,i,s,x.bool_to_Prop (i ∈ add tag A s i x).
435#tag #A #i #s #x >mem_set_add
436@eq_identifier_elim [#_ %| #ABS elim (absurd … (refl ? i) ABS)] qed.
437
438lemma in_map_domain : ∀tag,A.∀m : identifier_map tag A.∀i.
439  if i ∈ m then (∃s.lookup … m i = Some ? s) else (lookup … m i = None ?).
440#tag #A * #m * #i normalize
441elim (lookup_opt A i m) normalize
442[ % | #x %{x} % ]
443qed.
444
445lemma union_empty_l : ∀tag.∀s:identifier_set tag. ∅ ∪ s = s.
446#tag * normalize #m >map_opt_id_eq_ext // * %
447qed.
448
449lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s.
450#tag * * [//] *[2: *] #l#r normalize
451>map_opt_id_eq_ext [1,3: >map_opt_id_eq_ext [2,4: *] |*: *] //
452qed.
453
454lemma minus_empty_l : ∀tag,A.∀s:identifier_map tag A. ∅ ∖ s ≅ ∅.
455#tag #A * * [//] *[2:#x]#l#r * * normalize [1,4://]
456#p >lookup_opt_map elim (lookup_opt ???) normalize //
457qed.
458
459lemma minus_empty_r : ∀tag,A.∀s:identifier_map tag A. s ∖ ∅ = s.
460#tag #A * * [//] *[2:#x]#l#r normalize
461>map_opt_id >map_opt_id //
462qed.
463
464lemma mem_set_union : ∀tag.∀i : identifier tag.∀s,s' : identifier_set tag.
465  i ∈ (s ∪ s') = (i ∈ s ∨ i ∈ s').
466#tag * #i * #s * #s' normalize
467>lookup_opt_merge [2: @refl]
468elim (lookup_opt ???)
469elim (lookup_opt ???)
470normalize // qed.
471
472lemma mem_set_minus : ∀tag,A,B.∀i : identifier tag.∀s : identifier_map tag A.
473  ∀s' : identifier_map tag B.
474  i ∈ (s ∖ s') = (i ∈ s ∧ ¬ i ∈ s').
475#tag #A #B * #i * #s * #s' normalize
476>lookup_opt_merge [2: @refl]
477elim (lookup_opt ???)
478elim (lookup_opt ???)
479normalize // qed.
480
481lemma set_eq_ext_node : ∀tag.∀o,o',l,l',r,r'.
482  an_id_map tag ? (pm_node ? o l r) ≅ an_id_map … (pm_node ? o' l' r') →
483    o = o' ∧ an_id_map tag ? l ≅ an_id_map … l' ∧ an_id_map tag ? r ≅ an_id_map … r'.
484#tag#o#o'#l#l'#r#r'#H
485%[
486%[ lapply (H (an_identifier ? one))
487   elim o [2: *] elim o' [2,4: *] normalize // #EQ destruct
488 | *#p lapply (H (an_identifier ? (p0 p))) normalize //
489]| *#p lapply (H (an_identifier ? (p1 p))) normalize //
490]
491qed.
492
493lemma set_eq_ext_leaf : ∀tag,A.∀o,l,r.
494  (∀i.i∈an_id_map tag A (pm_node ? o l r) = false) →
495    o = None ? ∧ (∀i.i∈an_id_map tag ? l = false) ∧ (∀i.i∈an_id_map tag ? r = false).
496#tag#A#o#l#r#H
497%[
498%[ lapply (H (an_identifier ? one))
499   elim o [2: #a] normalize // #EQ destruct
500 | *#p lapply (H (an_identifier ? (p0 p))) normalize //
501]| *#p lapply (H (an_identifier ? (p1 p))) normalize //
502]
503qed.
504
505
506definition id_map_size : ∀tag : String.∀A. identifier_map tag A → ℕ ≝
507  λtag,A,s.match s with [an_id_map p ⇒ |p|].
508
509interpretation "identifier map domain size" 'norm s = (id_map_size ?? s).
510
511lemma set_eq_ext_empty_to_card : ∀tag,A.∀s : identifier_map tag A. (∀i.i∈s = false) → |s| = 0.
512#tag#A * #s elim s [//]
513#o#l#r normalize in ⊢((?→%)→(?→%)→?); #Hil #Hir #H
514elim (set_eq_ext_leaf … H) * #EQ destruct #Hl #Hr normalize
515>(Hil Hl) >(Hir Hr) // qed.
516
517lemma set_eq_ext_to_card : ∀tag.∀s,s' : identifier_set tag. s ≅ s' → |s| = |s'|.
518#tag *#s elim s
519[** [//] #o#l#r #H
520  >(set_eq_ext_empty_to_card … (std_symm … H)) //
521| #o#l#r normalize in ⊢((?→?→??%?)→(?→?→??%?)→?);
522  #Hil #Hir **
523  [#H @(set_eq_ext_empty_to_card … H)]
524  #o'#l'#r' #H elim (set_eq_ext_node … H) * #EQ destruct(EQ) #Hl #Hr
525  normalize >(Hil ? Hl) >(Hir ? Hr) //
526] qed.
527
528lemma add_size: ∀tag,A,s,i,x.
529  |add tag A s i x| = (if i ∈ s then 0 else 1) + |s|.
530#tag #A *#s *#i #x
531lapply (insert_size ? i x s)
532lapply (refl ? (lookup_opt ? i s))
533generalize in ⊢ (???%→?); * [2: #x']
534normalize #EQ >EQ normalize //
535qed.
536
537lemma mem_set_O_lt_card : ∀tag,A.∀i.∀s : identifier_map tag A. i ∈ s → |s| > 0.
538#tag #A * #i * #s normalize #H
539@(lookup_opt_O_lt_size … i)
540% #EQ >EQ in H; normalize *
541qed.
542
543(* NB: no control on values if applied to maps *)
544definition set_subset ≝ λtag,A,B.λs : identifier_map tag A.
545  λs' : identifier_map tag B. ∀i.i ∈ s → (bool_to_Prop (i ∈ s')).
546
547interpretation "identifier set subset" 'subseteq s s' = (set_subset ??? s s').
548
549lemma add_subset :
550  ∀tag,A,B.∀i : identifier tag.∀x.∀s : identifier_map ? A.∀s' : identifier_map ? B.
551    i ∈ s' → s ⊆ s' → add … s i x ⊆ s'.
552#tag#A#B#i#x#s#s' #H #G #j
553>mem_set_add
554@eq_identifier_elim #H' [* >H' @H | #js @(G ? js)]
555qed.
556
557definition set_forall : ∀tag,A.(identifier tag → Prop) →
558  identifier_map tag A → Prop ≝ λtag,A,P,m.∀i. i ∈ m → P i.
559 
560lemma set_forall_add : ∀tag,P,m,i.set_forall tag ? P m → P i →
561  set_forall tag ? P (add_set ? m i).
562#tag#P#m#i#Pm#Pi#j
563>mem_set_add
564@eq_identifier_elim
565[#EQ destruct(EQ) #_ @Pi
566|#_ @Pm
567]
568qed.
569
570include "utilities/proper.ma".
571
572lemma minus_subset : ∀tag,A,B.minus_set tag A B ⊨ set_subset … ++> set_subset … -+> set_subset ….
573#tag#A#B#s#s' #H #s'' #s''' #G #i
574>mem_set_minus >mem_set_minus
575#H' elim (andb_Prop_true … H') -H' #is #nis''
576>(H … is)
577elim (true_or_false_Prop (i∈s'''))
578[ #is''' >(G … is''') in nis''; *
579| #nis''' >nis''' %
580]
581qed.
582
583lemma subset_node : ∀tag,A,B.∀o,o',l,l',r,r'.
584  an_id_map tag A (pm_node ? o l r) ⊆ an_id_map tag B (pm_node ? o' l' r') →
585    opt_All ? (λ_.o' ≠ None ?) o ∧ an_id_map tag ? l ⊆ an_id_map tag  ? l' ∧
586      an_id_map tag ? r ⊆ an_id_map tag ? r'.
587#tag#A#B#o#o'#l#l'#r#r'#H
588%[%
589  [ lapply (H (an_identifier ? (one))) elim o [2: #a] elim o' [2:#b]
590    normalize // [#_ % #ABS destruct(ABS) | #G lapply (G I) *]
591  | *#p lapply (H (an_identifier ? (p0 p)))
592  ]
593 | *#p lapply (H (an_identifier ? (p1 p)))
594] #H @H
595qed.
596
597lemma subset_leaf : ∀tag,A.∀o,l,r.
598  an_id_map tag A (pm_node ? o l r) ⊆ ∅ →
599    o = None ? ∧ (∀i.i∈an_id_map tag ? l = false) ∧ (∀i.i∈an_id_map tag ? r = false).
600#tag#A#o#l#r#H
601%[
602%[ lapply (H (an_identifier ? one))
603   elim o [2: #a] normalize // #EQ lapply(EQ I) *
604 | *#p lapply (H (an_identifier ? (p0 p)))
605 ]
606|  *#p lapply (H (an_identifier ? (p1 p)))
607] normalize elim (lookup_opt ? p ?) normalize
608// #a #H lapply (H I) *
609qed.
610
611lemma subset_card : ∀tag,A,B.∀s : identifier_map tag A.∀s' : identifier_map tag B.
612  s ⊆ s' → |s| ≤ |s'|.
613#tag #A #B *#s elim s
614[ //
615| #o#l#r #Hil #Hir **
616  [ #H elim (subset_leaf … H) * #EQ >EQ #Hl #Hr
617    lapply (set_eq_ext_empty_to_card … Hl)
618    lapply (set_eq_ext_empty_to_card … Hr)
619    normalize //
620  | #o' #l' #r' #H elim (subset_node … H) *
621    elim o [2: #a] elim o' [2,4: #a']
622    [3: #G normalize in G; elim(absurd ? (refl ??) G)
623    |*: #_ #Hl #Hr lapply (Hil ? Hl) lapply (Hir ? Hr)
624      normalize #H1 #H2
625      [@le_S_S | @(transitive_le … (|l'|+|r'|)) [2: / by /]]
626      @le_plus assumption
627    ]
628  ]
629]
630qed.
631
632lemma mem_set_empty : ∀tag.∀i: identifier tag. i∈∅ = false.
633#tag * #i normalize %
634qed.
635
636lemma mem_set_singl_to_eq : ∀tag.∀i,j : identifier tag.i∈{(j)} → i = j.
637#tag
638#i #j >mem_set_add >mem_set_empty
639#H elim (orb_true_l … H) -H
640[@eq_identifier_elim [//] #_] #EQ destruct
641qed.
642
643lemma subset_add_set : ∀tag,i,s.s ⊆ add_set tag s i.
644#tag#i#s#j #H >mem_set_add >H
645>commutative_orb %
646qed.
647
648lemma add_set_monotonic : ∀tag,i,s,s'.s ⊆ s' → add_set tag s i ⊆ add_set tag s' i.
649#tag#i#s#s' #H #j >mem_set_add >mem_set_add
650@orb_elim elim (eq_identifier ???)
651whd lapply (H j) /2 by /
652qed.
653
654lemma transitive_subset : ∀tag,A.transitive ? (set_subset tag A A).
655#tag#A#s#s'#s''#H#G#i #is
656@(G … (H … is))
657qed.
658
659definition set_from_list : ∀tag.list (identifier tag) → identifier_map tag unit ≝
660  λtag.foldl … (add_set ?) ∅.
661
662coercion id_set_from_list : ∀tag.∀l : list (identifier tag).identifier_map tag unit ≝
663  set_from_list on _l : list (identifier ?) to identifier_map ? unit.
664
665lemma mem_map_domain : ∀tag,A.∀m : identifier_map tag A.∀i.
666i∈m → lookup … m i ≠ None ?.
667#tag#A * #m #i
668whd in match (i∈?);
669elim (lookup ????) normalize [2: #x]
670* % #EQ destruct(EQ)
671qed.
672
673
674
675lemma mem_list_as_set : ∀tag.∀l : list (identifier tag).
676  ∀i.i ∈ l → In ? l i.
677#tag #l @(list_elim_left … l)
678[ #i *
679| #t #h #Hi  #i
680  whd in ⊢ (?(???%?)→?);
681  >foldl_append
682  whd in ⊢ (?(???%?)→?);
683  >mem_set_add
684  @eq_identifier_elim
685  [ #EQi destruct(EQi)
686    #_ @Exists_append_r % %
687  | #_ #H @Exists_append_l @Hi assumption
688  ]
689]
690qed.
691
692lemma list_as_set_mem : ∀tag.∀l : list (identifier tag).
693  ∀i.In ? l i → i ∈ l.
694#tag #l @(list_elim_left … l)
695[ #i *
696| #t #h #Hi #i #H
697  whd in ⊢ (?(???%?));
698  >foldl_append
699  whd in ⊢ (?(???%?));
700  elim (Exists_append … H) -H
701  [ #H >mem_set_add
702    @eq_identifier_elim [//] #_ normalize
703    @Hi @H
704  | * [2: *] #EQi destruct(EQi) >mem_set_add_id %
705  ]
706]
707qed.
708
709lemma list_as_set_All : ∀tag,P.∀ l : list (identifier tag).
710  (∀i.i ∈ l → P i) → All ? P l.
711#tag #P #l @(list_elim_left … l)
712[ #_ %
713| #x #l' #Hi
714  whd in match (l'@[x] : identifier_map tag unit);
715  >foldl_append
716  #H @All_append
717  [ @Hi #i #G @H
718    whd in ⊢ (?(???%?));
719    >mem_set_add @orb_Prop_r @G
720  | % [2: %]
721    @H
722    whd in ⊢ (?(???%?));
723    @mem_set_add_id
724  ]
725]
726qed.
727
728lemma All_list_as_set : ∀tag,P.∀ l : list (identifier tag).
729  All ? P l → ∀i.i ∈ l → P i.
730#tag #P #l @(list_elim_left … l)
731[ * #i *
732| #x #l' #Hi #H
733  lapply (All_append_l … H)
734  lapply (All_append_r … H)
735  * #Px * #Pl' #i
736  whd in match (l'@[x] : identifier_map ??);
737  >foldl_append
738  >mem_set_add
739  @eq_identifier_elim
740  [ #EQx >EQx #_ @Px
741  | #_ whd in match (?∨?); @Hi @Pl'
742  ]
743]
744qed. 
745
746
747
Note: See TracBrowser for help on using the repository browser.