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/PositiveMap.ma

    r1601 r1882  
    191191] qed.
    192192
    193 let rec merge (A: Type[0]) (b: positive_map A) (c:positive_map A) on b: positive_map A ≝
    194 match b with
    195 [ pm_leaf ⇒ c
     193include "utilities/option.ma".
     194
     195let rec map_opt A B (f : A → option B) (b : positive_map A) on b : positive_map B ≝
     196match b with
     197[ pm_leaf ⇒ pm_leaf ?
     198| pm_node a l r ⇒ pm_node ? (a »= f)
     199    (map_opt ?? f l)
     200    (map_opt ?? f r)
     201].
     202
     203definition map ≝ λA,B,f.map_opt A B (λx. Some ? (f x)).
     204
     205lemma lookup_opt_map : ∀A,B,f,b,p.
     206  lookup_opt … p (map_opt A B f b) = ! x ← lookup_opt … p b ; f x.
     207#A#B#f#b elim b [//]
     208#a #l #r #Hil #Hir * [//]
     209#p
     210whd in ⊢ (??(???%)(????%?));
     211whd in ⊢ (??%?); //
     212qed.
     213
     214lemma map_opt_id_eq_ext : ∀A,m,f.(∀x.f x = Some ? x) → map_opt A A f m = m.
     215#A #m #f #Hf elim m [//]
     216* [2:#x] #l #r #Hil #Hir normalize [>Hf] //
     217qed.
     218
     219lemma map_opt_id : ∀A,m.map_opt A A (λx. Some ? x) m = m.
     220#A #m @map_opt_id_eq_ext //
     221qed.
     222
     223let rec merge A B C (choice : option A → option B → option C)
     224  (a : positive_map A) (b : positive_map B) on a : positive_map C ≝
     225match a with
     226[ pm_leaf ⇒ map_opt ?? (λx.choice (None ?) (Some ? x)) b
     227| pm_node o l r ⇒
     228  match b with
     229  [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a
     230  | pm_node o' l' r' ⇒
     231    pm_node ? (choice o o')
     232      (merge … choice l l')
     233      (merge … choice r r')
     234  ]
     235].
     236
     237lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p.
     238  choice (None ?) (None ?) = None ? →
     239  lookup_opt … p (merge A B C choice a b) =
     240    choice (lookup_opt … p a) (lookup_opt … p b).
     241 #A#B#C#choice#a elim a
     242[ normalize #b
     243| #o#l#r#Hil#Hir * [2: #o'#l'#r' * normalize /2 by /]
     244]
     245#p#choice_good >lookup_opt_map
     246elim (lookup_opt ???)
     247normalize //
     248qed.
     249
     250let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝
     251match b with
     252[ pm_leaf ⇒ 0
    196253| pm_node a l r ⇒
    197   match c with
    198   [ pm_leaf ⇒ pm_node A a l r
    199   | pm_node a' l' r' ⇒ pm_node A a' (merge A l l') (merge A r r')
    200   ]
    201 ].
    202 
     254  (match a with
     255   [ Some _ ⇒ 1
     256   | None ⇒ 0
     257   ]) + domain_size A l + domain_size A r
     258].
     259
     260(* just to load notation for 'norm (list.ma's notation overrides core's 'card)*)
     261include "basics/lists/list.ma".
     262interpretation "positive map size" 'norm p = (domain_size ? p).
     263
     264lemma map_opt_size : ∀A,B,f,b.|map_opt A B f b| ≤ |b|.
     265#A#B#f#b elim b [//]
     266*[2:#x]#l#r#Hil#Hir normalize
     267[elim (f ?) normalize [@(transitive_le ? ? ? ? (le_n_Sn ?)) | #y @le_S_S ] ]
     268@le_plus assumption
     269qed.
     270
     271lemma map_size : ∀A,B,f,b.|map A B f b| = |b|.
     272#A#B#f#b elim b [//]
     273*[2:#x]#l#r#Hil#Hir normalize
     274>Hil >Hir @refl
     275qed.
     276
     277lemma lookup_opt_O_lt_size : ∀A,m,p. lookup_opt A p m ≠ None ? → 0 < |m|.
     278#A#m elim m
     279[#p normalize #F elim (absurd ? (refl ??) F)
     280|* [2: #x]  #l #r #Hil #Hir * normalize
     281  [1,2,3: //
     282  |4:  #F elim (absurd ? (refl ??) F)]
     283  #p #H [@(transitive_le … (Hir ? H)) | @(transitive_le … (Hil ? H))] //
     284qed.
     285
     286lemma insert_size : ∀A,p,a,m. |insert A p a m| =
     287  (match lookup_opt … p m with [Some _ ⇒ 0 | None ⇒ 1]) + |m|.
     288#A#p elim p
     289[ #a * [2: * [2: #x] #l #r] normalize //
     290|*: #p #Hi #a * [2,4: * [2,4: #x] #l #r] normalize >Hi //
     291] qed.
Note: See TracChangeset for help on using the changeset viewer.