Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (8 years ago)
Author:
tranquil
Message:

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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r1635 r1882  
    33include "utilities/binary/positive.ma".
    44include "utilities/lists.ma".
     5include "utilities/extralib.ma".
    56include "common/Errors.ma".
    67
     
    370371(* Sets *)
    371372
    372 inductive identifier_set (tag:String) : Type[0] ≝
    373   an_id_set : positive_map unit → identifier_set tag.
    374 
    375 definition empty_set : ∀tag:String. identifier_set tag ≝
    376 λtag. an_id_set tag (pm_leaf unit).
    377 
    378 let rec add_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : identifier_set tag ≝
    379   an_id_set tag (insert unit (match i with [ an_identifier i' ⇒ i' ])
    380                           it (match s with [ an_id_set s' ⇒ s' ])).
     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.
    381380
    382381definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
    383382λtag,i. add_set tag (empty_set tag) i.
    384383
    385 let rec mem_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : bool ≝
    386   match lookup_opt ? (match i with [ an_identifier i' ⇒ i' ])
    387                      (match s with [ an_id_set s' ⇒ s' ]) with
     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
    388387  [ None ⇒ false
    389388  | Some _ ⇒ true
    390389  ].
    391 
    392 let rec union_set (tag:String) (s:identifier_set tag) (s':identifier_set tag) on s : identifier_set tag ≝
    393   an_id_set tag (merge unit (match s with [ an_id_set s0 ⇒ s0 ])
    394                             (match s' with [ an_id_set s1 ⇒ s1 ])).
    395 
    396 interpretation "identifier set union" 'union a b = (union_set ? a b).
     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).
    397406notation "∅" non associative with precedence 90 for @{ 'empty }.
    398407interpretation "empty identifier set" 'empty = (empty_set ?).
    399408interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a).
    400 interpretation "identifier set membership" 'mem a b = (mem_set ? b 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.
    401444
    402445lemma union_empty_l : ∀tag.∀s:identifier_set tag. ∅ ∪ s = s.
    403 #tag * //
     446#tag * normalize #m >map_opt_id_eq_ext // * %
    404447qed.
    405448
    406449lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s.
    407 #tag * * // qed.
    408 
     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 TracChangeset for help on using the changeset viewer.