mathlib3 documentation

data.hash_map

Hash maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

hash_map: constructed with mk_hash_map.

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) (n : ℕ+) :

Type (max u v)

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

Equations

bucket_array α β n = array ↑n (list (Σ (a : α), β a))

Instances for bucket_array

bucket_array.inhabited

def hash_map.mk_idx (n : ℕ+) (i : ℕ) :

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

Equations

hash_map.mk_idx n i = ⟨i % ↑n, _⟩

@[protected, instance]

def bucket_array.inhabited {α : Type u} {β : α → Type v} {n : ℕ+} :

inhabited (bucket_array α β n)

Equations

bucket_array.inhabited = {default := mk_array ↑n list.nil}

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

list (Σ (a : α), β a)

Read the bucket corresponding to an element

Equations

bucket_array.read hash_fn data a = let bidx : fin ↑n := hash_map.mk_idx n (hash_fn a) in array.read data bidx

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

bucket_array α β n

Write the bucket corresponding to an element

Equations

bucket_array.write hash_fn data a l = let bidx : fin ↑n := hash_map.mk_idx n (hash_fn a) in array.write data bidx l

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

bucket_array α β n

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

Equations

bucket_array.modify hash_fn data a f = let bidx : fin ↑n := hash_map.mk_idx n (hash_fn a) in array.write data bidx (f (array.read data bidx))

def bucket_array.as_list {α : Type u} {β : α → Type v} {n : ℕ+} (data : bucket_array α β n) :

list (Σ (a : α), β a)

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

Equations

data.as_list = (array.to_list data).join

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} (d : δ) (f : δ → Π (a : α), β a → δ) :

δ

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

Equations

data.foldl d f = array.foldl data d (λ (b : list (Σ (a : α), β a)) (d : δ), list.foldl (λ (r : δ) (a : Σ (a : α), β a), f r a.fst a.snd) d b)

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 : α) (b : β a) :

bucket_array α β n

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

Equations

hash_map.reinsert_aux hash_fn data a b = bucket_array.modify hash_fn data a (λ (l : list (Σ (a : α), β a)), ⟨a, b⟩ :: l)

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

bucket_array.as_list (mk_array ↑n list.nil) = list.nil

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

hash_map.find_aux a (⟨a', b⟩ :: t) = dite (a' = a) (λ (h : a' = a), option.some (h.rec_on b)) (λ (h : ¬a' = a), hash_map.find_aux a t)
hash_map.find_aux a list.nil = option.none

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

(list.map sigma.fst l).nodup → (hash_map.find_aux a l = option.some b ↔ ⟨a, b⟩ ∈ l)

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

Returns tt if the bucket l contains the key a

Equations

hash_map.contains_aux a l = (hash_map.find_aux a l).is_some

theorem hash_map.contains_aux_iff {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l : list (Σ (a : α), β a)} (nd : (list.map sigma.fst l).nodup) :

↥(hash_map.contains_aux a l) ↔ a ∈ list.map sigma.fst l

def hash_map.replace_aux {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) :

list (Σ (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

hash_map.replace_aux a b (⟨a', b'⟩ :: t) = ite (a' = a) (⟨a, b⟩ :: t) (⟨a', b'⟩ :: hash_map.replace_aux a b t)
hash_map.replace_aux a b list.nil = list.nil

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

list (Σ (a : α), β a) → list (Σ (a : α), β a)

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

Equations

hash_map.erase_aux a (⟨a', b'⟩ :: t) = ite (a' = a) t (⟨a', b'⟩ :: hash_map.erase_aux a t)
hash_map.erase_aux a list.nil = list.nil

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

Prop

len : bkts.as_list.length = sz
idx : ∀ {i : fin ↑n} {a : Σ (a : α), β a}, a ∈ array.read bkts i → hash_map.mk_idx n (hash_fn a.fst) = i
nodup : ∀ (i : fin ↑n), (list.map sigma.fst (array.read bkts i)).nodup

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} (hl : ⟨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} (hl : ⟨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 : ℕ} (v : 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 : ℕ+) :

hash_map.valid hash_fn (mk_array ↑n list.nil) 0

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) = option.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 : α) :

↥(hash_map.contains_aux a (bucket_array.read hash_fn bkts a)) ↔ a ∈ list.map sigma.fst bkts.as_list

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)) (hl : array.read bkts bidx = u ++ v1 ++ w) (hfl : f (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 ∈ v2 → hash_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 : ℕ} (v : hash_map.valid hash_fn bkts sz) :

v1.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) (Hc : ↥(hash_map.contains_aux a (bucket_array.read hash_fn bkts a))) (v : hash_map.valid hash_fn bkts sz) :

hash_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) (Hnc : ¬↥(hash_map.contains_aux a (bucket_array.read hash_fn bkts a))) (v : hash_map.valid hash_fn bkts sz) :

hash_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 : α) (Hc : ↥(hash_map.contains_aux a (bucket_array.read hash_fn bkts a))) (v : hash_map.valid hash_fn bkts sz) :

hash_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)

hash_fn : α → ℕ
size : ℕ
nbuckets : ℕ+
buckets : bucket_array α β self.nbuckets
is_valid : hash_map.valid self.hash_fn self.buckets self.size

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

Instances for hash_map

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

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

Equations

mk_hash_map hash_fn nbuckets = let n : ℕ := 8 := ite (nbuckets = 0) 8 nbuckets, nz : n > 0 := _ in {hash_fn := hash_fn, size := 0, nbuckets := ⟨n, nz⟩, buckets := mk_array n list.nil, is_valid := _}

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

m.find a = hash_map.find_aux a (bucket_array.read m.hash_fn m.buckets a)

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

Return tt if the key exists in the map

Equations

m.contains a = (m.find a).is_some

@[protected, instance]

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

has_mem α (hash_map α β)

Equations

hash_map.has_mem = {mem := λ (a : α) (m : hash_map α β), ↥(m.contains a)}

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

δ

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

Equations

m.fold d f = m.buckets.foldl d f

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

list (Σ (a : α), β a)

The list of key-value pairs in the map

Equations

m.entries = m.buckets.as_list

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

The list of keys in the map

Equations

m.keys = list.map sigma.fst m.entries

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

m.find a = option.some b ↔ ⟨a, b⟩ ∈ m.entries

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

↥(m.contains a) ↔ a ∈ m.keys

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

(mk_hash_map hash_fn n).entries = list.nil

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

(mk_hash_map hash_fn n).keys = list.nil

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

(mk_hash_map hash_fn n).find a = option.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 : ℕ} (v : hash_map.valid hash_fn bkts sz) :

hash_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 : α) (b : β a) :

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

Equations

{hash_fn := hash_fn, size := size, nbuckets := n, buckets := buckets, is_valid := v}.insert a b = let bkt : list (Σ (a : α), β a) := bucket_array.read hash_fn buckets a in dite ↥(hash_map.contains_aux a bkt) (λ (hc : ↥(hash_map.contains_aux a bkt)), {hash_fn := hash_fn, size := size, nbuckets := n, buckets := bucket_array.modify hash_fn buckets a (hash_map.replace_aux a b), is_valid := _}) (λ (hc : ¬↥(hash_map.contains_aux a bkt)), let size' : ℕ := size + 1, buckets' : bucket_array α β n := bucket_array.modify hash_fn buckets a (λ (l : list (Σ (a : α), β a)), ⟨a, b⟩ :: l), valid' : hash_map.valid hash_fn (hash_map.reinsert_aux hash_fn buckets a b) (size + 1) := _ in ite (size' ≤ ↑n) {hash_fn := hash_fn, size := size', nbuckets := n, buckets := buckets', is_valid := valid'} (let n' : ℕ+ := ⟨↑n * 2, _⟩, buckets'' : bucket_array α β n' := buckets'.foldl (mk_array ↑n' list.nil) (hash_map.reinsert_aux hash_fn) in {hash_fn := hash_fn, size := size', nbuckets := n', buckets := buckets'', is_valid := _}))

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 = option.some b

theorem hash_map.find_insert_ne {α : Type u} {β : α → Type v} [decidable_eq α] (m : hash_map α β) (a a' : α) (b : β a) (h : 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'), option.some (h.rec_on b)) (λ (h : ¬a = a'), m.find a')

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

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

Equations

hash_map.insert_all l m = list.foldl (λ (m : hash_map α β) (_x : Σ (a : α), β a), hash_map.insert_all._match_1 m _x) m l
hash_map.insert_all._match_1 m ⟨a, b⟩ = m.insert a b

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

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

Equations

hash_map.of_list l hash_fn = hash_map.insert_all l (mk_hash_map hash_fn (2 * l.length))

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

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

Equations

m.erase a = hash_map.erase._match_1 m a m
hash_map.erase._match_1 m a {hash_fn := hash_fn, size := size, nbuckets := n, buckets := buckets, is_valid := v} = dite ↥(hash_map.contains_aux a (bucket_array.read hash_fn buckets a)) (λ (hc : ↥(hash_map.contains_aux a (bucket_array.read hash_fn buckets a))), {hash_fn := hash_fn, size := size - 1, nbuckets := n, buckets := bucket_array.modify hash_fn buckets a (hash_map.erase_aux a), is_valid := _}) (λ (hc : ¬↥(hash_map.contains_aux a (bucket_array.read hash_fn buckets a))), m)

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 = option.none

theorem hash_map.find_erase_ne {α : Type u} {β : α → Type v} [decidable_eq α] (m : hash_map α β) (a a' : α) (h : 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') option.none (m.find a')

@[protected, instance]

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

has_to_string (hash_map α β)

Equations

hash_map.has_to_string = {to_string := to_string (λ (a : α), _inst_3 a)}

@[protected, instance]

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

has_to_format (hash_map α β)

@[protected, instance]

def hash_map.inhabited {β : ℕ → Type u_1} :

inhabited (hash_map ℕ β)

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

Equations

hash_map.inhabited = {default := (mk_hash_map id)}