source: src/common/Identifiers.ma @ 1949

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