mathlib documentation

data.hash_map

Hash maps

Defines a hash map data structure, representing a finite key-value map with a value type that may depend on the key type. The structure requires a nat-valued hash function to associate keys to buckets.

Main definitions

Implementation details

A hash map with key type α and (dependent) value type β : α → Type* consists of an array of buckets, which are lists containing key/value pairs for that bucket. The hash function is taken modulo n to assign keys to their respective bucket. Because of this, some care should be put into the hash function to ensure it evenly distributes keys.

The bucket array is an array. These have special VM support for in-place modification if there is only ever one reference to them. If one takes special care to never keep references to old versions of a hash map alive after updating it, then the hash map will be modified in-place. In this documentation, when we say a hash map is modified in-place, we are assuming the API is being used in this manner.

When inserting (hash_map.insert), if the number of stored pairs (the size) is going to exceed the number of buckets, then a new hash map is first created with double the number of buckets and everything in the old hash map is reinserted along with the new key/value pair. Otherwise, the bucket array is modified in-place. The amortized running time of inserting $$n$$ elements into a hash map is $$O(n)$$.

When removing (hash_map.erase), the hash map is modified in-place. The implementation does not reduce the number of buckets in the hash map if the size gets too low.

Tags

hash map

def bucket_array (α : Type u) :
(α → Type v)ℕ+Type (max u v)

bucket_array α β is the underlying data type for hash_map α β, an array of linked lists of key-value pairs.

Equations
def hash_map.mk_idx (n : ℕ+) :
fin n

Make a hash_map index from a nat hash value and a (positive) buffer size

Equations
@[instance]
def bucket_array.inhabited {α : Type u} {β : α → Type v} {n : ℕ+} :

Equations
def bucket_array.read {α : Type u} {β : α → Type v} (hash_fn : α → ) {n : ℕ+} :
bucket_array α β nα → list (Σ (a : α), β a)

Read the bucket corresponding to an element

Equations
def bucket_array.write {α : Type u} {β : α → Type v} (hash_fn : α → ) {n : ℕ+} :
bucket_array α β nα → list (Σ (a : α), β a)bucket_array α β n

Write the bucket corresponding to an element

Equations
def bucket_array.modify {α : Type u} {β : α → Type v} (hash_fn : α → ) {n : ℕ+} :
bucket_array α β nα → (list (Σ (a : α), β a)list (Σ (a : α), β a))bucket_array α β n

Modify (read, apply f, and write) the bucket corresponding to an element

Equations
def bucket_array.as_list {α : Type u} {β : α → Type v} {n : ℕ+} :
bucket_array α β nlist (Σ (a : α), β a)

The list of all key-value pairs in the bucket list

Equations
theorem bucket_array.mem_as_list {α : Type u} {β : α → Type v} {n : ℕ+} (data : bucket_array α β n) {a : Σ (a : α), β a} :
a data.as_list ∃ (i : fin n), a array.read data i

def bucket_array.foldl {α : Type u} {β : α → Type v} {n : ℕ+} (data : bucket_array α β n) {δ : Type w} :
δ → (δ → Π (a : α), β a → δ) → δ

Fold a function f over the key-value pairs in the bucket list

Equations
theorem bucket_array.foldl_eq {α : Type u} {β : α → Type v} {n : ℕ+} (data : bucket_array α β n) {δ : Type w} (d : δ) (f : δ → Π (a : α), β a → δ) :
data.foldl d f = list.foldl (λ (r : δ) (a : Σ (a : α), β a), f r a.fst a.snd) d data.as_list

def hash_map.reinsert_aux {α : Type u} {β : α → Type v} (hash_fn : α → ) {n : ℕ+} (data : bucket_array α β n) (a : α) :
β abucket_array α β n

Insert the pair ⟨a, b⟩ into the correct location in the bucket array (without checking for duplication)

Equations
theorem hash_map.mk_as_list {α : Type u} {β : α → Type v} (n : ℕ+) :

def hash_map.find_aux {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :
list (Σ (a : α), β a)option (β a)

Search a bucket for a key a and return the value

Equations
theorem hash_map.find_aux_iff {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l : list (Σ (a : α), β a)} :

def hash_map.contains_aux {α : Type u} {β : α → Type v} [decidable_eq α] :
α → list (Σ (a : α), β a)bool

Returns tt if the bucket l contains the key a

Equations
theorem hash_map.contains_aux_iff {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l : list (Σ (a : α), β a)} :

def hash_map.replace_aux {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :
β alist (Σ (a : α), β a)list (Σ (a : α), β a)

Modify a bucket to replace a value in the list. Leaves the list unchanged if the key is not found.

Equations
def hash_map.erase_aux {α : Type u} {β : α → Type v} [decidable_eq α] :
α → list (Σ (a : α), β a)list (Σ (a : α), β a)

Modify a bucket to remove a key, if it exists.

Equations
structure hash_map.valid {α : Type u} {β : α → Type v} (hash_fn : α → ) [decidable_eq α] {n : ℕ+} :
bucket_array α β n → Prop

The predicate valid bkts sz means that bkts satisfies the hash_map invariants: There are exactly sz elements in it, every pair is in the bucket determined by its key and the hash function, and no key appears multiple times in the list.

theorem hash_map.valid.idx_enum {α : Type u} {β : α → Type v} (hash_fn : α → ) [decidable_eq α] {n : ℕ+} {bkts : bucket_array α β n} {sz : } (v : hash_map.valid hash_fn bkts sz) {i : } {l : list (Σ (a : α), β a)} (he : (i, l) (array.to_list bkts).enum) {a : α} {b : β a} :
a, b⟩ l(∃ (h : i < n), hash_map.mk_idx n (hash_fn a) = i, h⟩)

theorem hash_map.valid.idx_enum_1 {α : Type u} {β : α → Type v} (hash_fn : α → ) [decidable_eq α] {n : ℕ+} {bkts : bucket_array α β n} {sz : } (v : hash_map.valid hash_fn bkts sz) {i : } {l : list (Σ (a : α), β a)} (he : (i, l) (array.to_list bkts).enum) {a : α} {b : β a} :
a, b⟩ l(hash_map.mk_idx n (hash_fn a)).val = i

theorem hash_map.valid.as_list_nodup {α : Type u} {β : α → Type v} (hash_fn : α → ) [decidable_eq α] {n : ℕ+} {bkts : bucket_array α β n} {sz : } :
hash_map.valid hash_fn bkts sz(list.map sigma.fst bkts.as_list).nodup

theorem hash_map.mk_valid {α : Type u} {β : α → Type v} (hash_fn : α → ) [decidable_eq α] (n : ℕ+) :

theorem hash_map.valid.find_aux_iff {α : Type u} {β : α → Type v} (hash_fn : α → ) [decidable_eq α] {n : ℕ+} {bkts : bucket_array α β n} {sz : } (v : hash_map.valid hash_fn bkts sz) {a : α} {b : β a} :
hash_map.find_aux a (bucket_array.read hash_fn bkts a) = some b a, b⟩ bkts.as_list

theorem hash_map.valid.contains_aux_iff {α : Type u} {β : α → Type v} (hash_fn : α → ) [decidable_eq α] {n : ℕ+} {bkts : bucket_array α β n} {sz : } (v : hash_map.valid hash_fn bkts sz) (a : α) :

theorem hash_map.append_of_modify {α : Type u} {β : α → Type v} [decidable_eq α] {n : ℕ+} {bkts : bucket_array α β n} {bidx : fin n} {f : list (Σ (a : α), β a)list (Σ (a : α), β a)} (u v1 v2 w : list (Σ (a : α), β a)) :
array.read bkts bidx = u ++ v1 ++ wf (array.read bkts bidx) = u ++ v2 ++ w(∃ (u' w' : list (Σ (a : α), β a)), bkts.as_list = u' ++ v1 ++ w' bkts'.as_list = u' ++ v2 ++ w')

theorem hash_map.valid.modify {α : Type u} {β : α → Type v} (hash_fn : α → ) [decidable_eq α] {n : ℕ+} {bkts : bucket_array α β n} {bidx : fin n} {f : list (Σ (a : α), β a)list (Σ (a : α), β a)} (u v1 v2 w : list (Σ (a : α), β a)) (hl : array.read bkts bidx = u ++ v1 ++ w) (hfl : f (array.read bkts bidx) = u ++ v2 ++ w) (hvnd : (list.map sigma.fst v2).nodup) (hal : ∀ (a : Σ (a : α), β a), a v2hash_map.mk_idx n (hash_fn a.fst) = bidx) (djuv : (list.map sigma.fst u).disjoint (list.map sigma.fst v2)) (djwv : (list.map sigma.fst w).disjoint (list.map sigma.fst v2)) {sz : } :
hash_map.valid hash_fn bkts szv1.length sz + v2.length hash_map.valid hash_fn bkts' (sz + v2.length - v1.length)

theorem hash_map.valid.replace_aux {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) (l : list (Σ (a : α), β a)) :
a list.map sigma.fst l(∃ (u w : list (Σ (a : α), β a)) (b' : β a), l = u ++ [a, b'⟩] ++ w hash_map.replace_aux a b l = u ++ [a, b⟩] ++ w)

theorem hash_map.valid.replace {α : Type u} {β : α → Type v} (hash_fn : α → ) [decidable_eq α] {n : ℕ+} {bkts : bucket_array α β n} {sz : } (a : α) (b : β a) :
(hash_map.contains_aux a (bucket_array.read hash_fn bkts a))hash_map.valid hash_fn bkts szhash_map.valid hash_fn (bucket_array.modify hash_fn bkts a (hash_map.replace_aux a b)) sz

theorem hash_map.valid.insert {α : Type u} {β : α → Type v} (hash_fn : α → ) [decidable_eq α] {n : ℕ+} {bkts : bucket_array α β n} {sz : } (a : α) (b : β a) :
¬(hash_map.contains_aux a (bucket_array.read hash_fn bkts a))hash_map.valid hash_fn bkts szhash_map.valid hash_fn (hash_map.reinsert_aux hash_fn bkts a b) (sz + 1)

theorem hash_map.valid.erase_aux {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (l : list (Σ (a : α), β a)) :
a list.map sigma.fst l(∃ (u w : list (Σ (a : α), β a)) (b : β a), l = u ++ [a, b⟩] ++ w hash_map.erase_aux a l = u ++ list.nil ++ w)

theorem hash_map.valid.erase {α : Type u} {β : α → Type v} (hash_fn : α → ) [decidable_eq α] {n : ℕ+} {bkts : bucket_array α β n} {sz : } (a : α) :
(hash_map.contains_aux a (bucket_array.read hash_fn bkts a))hash_map.valid hash_fn bkts szhash_map.valid hash_fn (bucket_array.modify hash_fn bkts a (hash_map.erase_aux a)) (sz - 1)

structure hash_map (α : Type u) [decidable_eq α] :
(α → Type v)Type (max u v)

A hash map data structure, representing a finite key-value map with key type α and value type β (which may depend on α).

def mk_hash_map {α : Type u} [decidable_eq α] {β : α → Type v} :
(α → )( := 8)hash_map α β

Construct an empty hash map with buffer size nbuckets (default 8).

Equations
def hash_map.find {α : Type u} {β : α → Type v} [decidable_eq α] (m : hash_map α β) (a : α) :
option (β a)

Return the value corresponding to a key, or none if not found

Equations
def hash_map.contains {α : Type u} {β : α → Type v} [decidable_eq α] :
hash_map α βα → bool

Return tt if the key exists in the map

Equations
@[instance]
def hash_map.has_mem {α : Type u} {β : α → Type v} [decidable_eq α] :
has_mem α (hash_map α β)

Equations
def hash_map.fold {α : Type u} {β : α → Type v} [decidable_eq α] {δ : Type w} :
hash_map α βδ → (δ → Π (a : α), β a → δ) → δ

Fold a function over the key-value pairs in the map

Equations
def hash_map.entries {α : Type u} {β : α → Type v} [decidable_eq α] :
hash_map α βlist (Σ (a : α), β a)

The list of key-value pairs in the map

Equations
def hash_map.keys {α : Type u} {β : α → Type v} [decidable_eq α] :
hash_map α βlist α

The list of keys in the map

Equations
theorem hash_map.find_iff {α : Type u} {β : α → Type v} [decidable_eq α] (m : hash_map α β) (a : α) (b : β a) :
m.find a = some b a, b⟩ m.entries

theorem hash_map.contains_iff {α : Type u} {β : α → Type v} [decidable_eq α] (m : hash_map α β) (a : α) :

theorem hash_map.entries_empty {α : Type u} {β : α → Type v} [decidable_eq α] (hash_fn : α → ) (n : := 8) :

theorem hash_map.keys_empty {α : Type u} {β : α → Type v} [decidable_eq α] (hash_fn : α → ) (n : := 8) :

theorem hash_map.find_empty {α : Type u} {β : α → Type v} [decidable_eq α] (hash_fn : α → ) (n : := 8) (a : α) :
(mk_hash_map hash_fn n).find a = none

theorem hash_map.not_contains_empty {α : Type u} {β : α → Type v} [decidable_eq α] (hash_fn : α → ) (n : := 8) (a : α) :
¬((mk_hash_map hash_fn n).contains a)

theorem hash_map.insert_lemma {α : Type u} {β : α → Type v} [decidable_eq α] (hash_fn : α → ) {n n' : ℕ+} {bkts : bucket_array α β n} {sz : } :
hash_map.valid hash_fn bkts szhash_map.valid hash_fn (bkts.foldl (mk_array n' list.nil) (hash_map.reinsert_aux hash_fn)) sz

def hash_map.insert {α : Type u} {β : α → Type v} [decidable_eq α] (m : hash_map α β) (a : α) :
β ahash_map α β

Insert a key-value pair into the map. (Modifies m in-place when applicable)

Equations
theorem hash_map.mem_insert {α : Type u} {β : α → Type v} [decidable_eq α] (m : hash_map α β) (a : α) (b : β a) (a' : α) (b' : β a') :
a', b'⟩ (m.insert a b).entries ite (a = a') (b == b') (a', b'⟩ m.entries)

theorem hash_map.find_insert_eq {α : Type u} {β : α → Type v} [decidable_eq α] (m : hash_map α β) (a : α) (b : β a) :
(m.insert a b).find a = some b

theorem hash_map.find_insert_ne {α : Type u} {β : α → Type v} [decidable_eq α] (m : hash_map α β) (a a' : α) (b : β a) :
a a'(m.insert a b).find a' = m.find a'

theorem hash_map.find_insert {α : Type u} {β : α → Type v} [decidable_eq α] (m : hash_map α β) (a' a : α) (b : β a) :
(m.insert a b).find a' = dite (a = a') (λ (h : a = a'), some (h.rec_on b)) (λ (h : ¬a = a'), m.find a')

def hash_map.insert_all {α : Type u} {β : α → Type v} [decidable_eq α] :
list (Σ (a : α), β a)hash_map α βhash_map α β

Insert a list of key-value pairs into the map. (Modifies m in-place when applicable)

Equations
def hash_map.of_list {α : Type u} {β : α → Type v} [decidable_eq α] :
list (Σ (a : α), β a)(α → )hash_map α β

Construct a hash map from a list of key-value pairs.

Equations
def hash_map.erase {α : Type u} {β : α → Type v} [decidable_eq α] :
hash_map α βα → hash_map α β

Remove a key from the map. (Modifies m in-place when applicable)

Equations
theorem hash_map.mem_erase {α : Type u} {β : α → Type v} [decidable_eq α] (m : hash_map α β) (a a' : α) (b' : β a') :
a', b'⟩ (m.erase a).entries a a' a', b'⟩ m.entries

theorem hash_map.find_erase_eq {α : Type u} {β : α → Type v} [decidable_eq α] (m : hash_map α β) (a : α) :
(m.erase a).find a = none

theorem hash_map.find_erase_ne {α : Type u} {β : α → Type v} [decidable_eq α] (m : hash_map α β) (a a' : α) :
a a'(m.erase a).find a' = m.find a'

theorem hash_map.find_erase {α : Type u} {β : α → Type v} [decidable_eq α] (m : hash_map α β) (a' a : α) :
(m.erase a).find a' = ite (a = a') none (m.find a')

@[instance]
def hash_map.has_to_string {α : Type u} {β : α → Type v} [decidable_eq α] [has_to_string α] [Π (a : α), has_to_string (β a)] :

Equations
@[instance]
meta def hash_map.has_to_format {α : Type u} {β : α → Type v} [decidable_eq α] [has_to_format α] [Π (a : α), has_to_format (β a)] :

@[instance]
def hash_map.inhabited {β : Type u_1} :

hash_map with key type nat and value type that may vary.

Equations