Extensional hash maps

This module develops the type Std.ExtHashMap of extensional hash maps. Dependent hash maps are defined in Std.Data.ExtDHashMap.

Lemmas about the operations on Std.ExtHashMap are available in the module Std.Data.ExtHashMap.Lemmas.

structure Std.ExtHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] : Type (max u v)

Hash maps.

This is a simple separate-chaining hash table. The data of the hash map consists of a cached size and an array of buckets, where each bucket is a linked list of key-value pais. The number of buckets is always a power of two. The hash map doubles its size upon inserting an element such that the number of elements is more than 75% of the number of buckets.

The hash table is backed by an Array. Users should make sure that the hash map is used linearly to avoid expensive copies.

The hash map uses == (provided by the BEq typeclass) to compare keys and hash (provided by the Hashable typeclass) to hash them. To ensure that the operations behave as expected, == should be an equivalence relation and a == b should imply hash a = hash b (see also the EquivBEq and LawfulHashable typeclasses). Both of these conditions are automatic if the BEq instance is lawful, i.e., if a == b implies a = b.

In contrast to regular hash maps, Std.ExtHashMap offers several extensionality lemmas and therefore has more lemmas about equality of hash maps. This however also makes it lose the ability to iterate freely over hash maps.

These hash maps contain a bundled well-formedness invariant, which means that they cannot be used in nested inductive types. For these use cases, Std.HashMap.Raw and Std.HashMap.Raw.WF unbundle the invariant from the hash map. When in doubt, prefer HashMap or ExtHashMap over HashMap.Raw.

Dependent hash maps, in which keys may occur in their values' types, are available as Std.ExtDHashMap in the module Std.Data.ExtDHashMap.

• inner : ExtDHashMap α fun (x : α) => β

  Internal implementation detail of the hash map

@[inline]

def Std.ExtHashMap.emptyWithCapacity {α : Type u} {β : Type v} [BEq α] [Hashable α] (capacity : Nat := 8) : ExtHashMap α β

Creates a new empty hash map. The optional parameter capacity can be supplied to presize the map so that it can hold the given number of mappings without reallocating. It is also possible to use the empty collection notations ∅ and {} to create an empty hash map with the default capacity.

Equations

• Std.ExtHashMap.emptyWithCapacity capacity = { inner := Std.ExtDHashMap.emptyWithCapacity capacity }

instance Std.ExtHashMap.instEmptyCollection {α : Type u} {β : Type v} [BEq α] [Hashable α] : EmptyCollection (ExtHashMap α β)

Equations

• Std.ExtHashMap.instEmptyCollection = { emptyCollection := Std.ExtHashMap.emptyWithCapacity }

instance Std.ExtHashMap.instInhabited {α : Type u} {β : Type v} [BEq α] [Hashable α] : Inhabited (ExtHashMap α β)

Equations

• Std.ExtHashMap.instInhabited = { default := ∅ }

@[inline]

def Std.ExtHashMap.insert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (m : ExtHashMap α β) (a : α) (b : β) : ExtHashMap α β

Inserts the given mapping into the map. If there is already a mapping for the given key, then both key and value will be replaced.

Note: this replacement behavior is true for HashMap, DHashMap, HashMap.Raw and DHashMap.Raw. The insert function on HashSet and HashSet.Raw behaves differently: it will return the set unchanged if a matching key is already present.

Equations

• m.insert a b = { inner := m.inner.insert a b }

instance Std.ExtHashMap.instSingletonProdOfEquivBEqOfLawfulHashable {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] : Singleton (α × β) (ExtHashMap α β)

Equations

• Std.ExtHashMap.instSingletonProdOfEquivBEqOfLawfulHashable = { singleton := fun (x : α × β) => match x with | (a, b) => ∅.insert a b }

instance Std.ExtHashMap.instInsertProdOfEquivBEqOfLawfulHashable {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] : Insert (α × β) (ExtHashMap α β)

Equations

• Std.ExtHashMap.instInsertProdOfEquivBEqOfLawfulHashable = { insert := fun (x : α × β) (x_1 : Std.ExtHashMap α β) => match x, x_1 with | (a, b), s => s.insert a b }

instance Std.ExtHashMap.instLawfulSingletonProd {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] : LawfulSingleton (α × β) (ExtHashMap α β)

@[inline]

def Std.ExtHashMap.insertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (m : ExtHashMap α β) (a : α) (b : β) : ExtHashMap α β

If there is no mapping for the given key, inserts the given mapping into the map. Otherwise, returns the map unaltered.

Equations

• m.insertIfNew a b = { inner := m.inner.insertIfNew a b }

@[inline]

def Std.ExtHashMap.containsThenInsert {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (m : ExtHashMap α β) (a : α) (b : β) : Bool × ExtHashMap α β

Checks whether a key is present in a map, and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling contains followed by insert.

Equations

• m.containsThenInsert a b = match m.inner.containsThenInsert a b with | (replaced, r) => (replaced, { inner := r })

@[inline]

def Std.ExtHashMap.containsThenInsertIfNew {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (m : ExtHashMap α β) (a : α) (b : β) : Bool × ExtHashMap α β

Checks whether a key is present in a map and inserts a value for the key if it was not found.

If the returned Bool is true, then the returned map is unaltered. If the Bool is false, then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling contains followed by insertIfNew.

Equations

• m.containsThenInsertIfNew a b = match m.inner.containsThenInsertIfNew a b with | (replaced, r) => (replaced, { inner := r })

@[inline]

def Std.ExtHashMap.getThenInsertIfNew? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (m : ExtHashMap α β) (a : α) (b : β) : Option β × ExtHashMap α β

Checks whether a key is present in a map, returning the associate value, and inserts a value for the key if it was not found.

If the returned value is some v, then the returned map is unaltered. If it is none, then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling get? followed by insertIfNew.

Equations

• m.getThenInsertIfNew? a b = match Std.ExtDHashMap.Const.getThenInsertIfNew? m.inner a b with | (previous, r) => (previous, { inner := r })

@[inline]

def Std.ExtHashMap.get? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (m : ExtHashMap α β) (a : α) : Option β

The notation m[a]? is preferred over calling this function directly.

Tries to retrieve the mapping for the given key, returning none if no such mapping is present.

Equations

• m.get? a = Std.ExtDHashMap.Const.get? m.inner a

@[inline]

def Std.ExtHashMap.contains {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (m : ExtHashMap α β) (a : α) : Bool

Returns true if there is a mapping for the given key. There is also a Prop-valued version of this: a ∈ m is equivalent to m.contains a = true.

Observe that this is different behavior than for lists: for lists, ∈ uses = and contains uses == for comparisons, while for hash maps, both use ==.

Equations

• m.contains a = m.inner.contains a

instance Std.ExtHashMap.instMembershipOfEquivBEqOfLawfulHashable {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] : Membership α (ExtHashMap α β)

Equations

• Std.ExtHashMap.instMembershipOfEquivBEqOfLawfulHashable = { mem := fun (m : Std.ExtHashMap α β) (a : α) => a ∈ m.inner }

instance Std.ExtHashMap.instDecidableMem {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : ExtHashMap α β} {a : α} : Decidable (a ∈ m)

Equations

• Std.ExtHashMap.instDecidableMem = inferInstanceAs (Decidable (a ∈ m.inner))

@[inline]

def Std.ExtHashMap.get {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (m : ExtHashMap α β) (a : α) (h : a ∈ m) : β

The notation m[a] or m[a]'h is preferred over calling this function directly.

Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of a ∈ m.

Equations

• m.get a h = Std.ExtDHashMap.Const.get m.inner a h

@[inline]

def Std.ExtHashMap.getD {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (m : ExtHashMap α β) (a : α) (fallback : β) : β

Tries to retrieve the mapping for the given key, returning fallback if no such mapping is present.

Equations

• m.getD a fallback = Std.ExtDHashMap.Const.getD m.inner a fallback

@[inline]

def Std.ExtHashMap.get! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] [Inhabited β] (m : ExtHashMap α β) (a : α) : β

The notation m[a]! is preferred over calling this function directly.

Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Equations

• m.get! a = Std.ExtDHashMap.Const.get! m.inner a

instance Std.ExtHashMap.instGetElem?Mem {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] : GetElem? (ExtHashMap α β) α β fun (m : ExtHashMap α β) (a : α) => a ∈ m

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.ExtHashMap.getKey? {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (m : ExtHashMap α β) (a : α) : Option α

Checks if a mapping for the given key exists and returns the key if it does, otherwise none. The result in the some case is guaranteed to be pointer equal to the key in the map.

Equations

• m.getKey? a = m.inner.getKey? a

@[inline]

def Std.ExtHashMap.getKey {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (m : ExtHashMap α β) (a : α) (h : a ∈ m) : α

Retrieves the key from the mapping that matches a. Ensures that such a mapping exists by requiring a proof of a ∈ m. The result is guaranteed to be pointer equal to the key in the map.

Equations

• m.getKey a h = m.inner.getKey a h

@[inline]

def Std.ExtHashMap.getKeyD {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (m : ExtHashMap α β) (a fallback : α) : α

Checks if a mapping for the given key exists and returns the key if it does, otherwise fallback. If a mapping exists the result is guaranteed to be pointer equal to the key in the map.

Equations

• m.getKeyD a fallback = m.inner.getKeyD a fallback

@[inline]

def Std.ExtHashMap.getKey! {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] [Inhabited α] (m : ExtHashMap α β) (a : α) : α

Checks if a mapping for the given key exists and returns the key if it does, otherwise panics. If no panic occurs the result is guaranteed to be pointer equal to the key in the map.

Equations

• m.getKey! a = m.inner.getKey! a

@[inline]

def Std.ExtHashMap.erase {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (m : ExtHashMap α β) (a : α) : ExtHashMap α β

Removes the mapping for the given key if it exists.

Equations

• m.erase a = { inner := m.inner.erase a }

@[inline]

def Std.ExtHashMap.size {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (m : ExtHashMap α β) : Nat

The number of mappings present in the hash map

Equations

• m.size = m.inner.size

@[inline]

def Std.ExtHashMap.isEmpty {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (m : ExtHashMap α β) : Bool

Returns true if the hash map contains no mappings.

Note that if your BEq instance is not reflexive or your Hashable instance is not lawful, then it is possible that this function returns false even though is not possible to get anything out of the hash map.

Equations

• m.isEmpty = m.inner.isEmpty

@[inline]

def Std.ExtHashMap.ofList {α : Type u} {β : Type v} [BEq α] [Hashable α] (l : List (α × β)) : ExtHashMap α β

Creates a hash map from a list of mappings. If the same key appears multiple times, the last occurrence takes precedence.

Equations

• Std.ExtHashMap.ofList l = { inner := Std.ExtDHashMap.Const.ofList l }

@[inline]

def Std.ExtHashMap.unitOfList {α : Type u} [BEq α] [Hashable α] (l : List α) : ExtHashMap α Unit

Creates a hash map from a list of keys, associating the value () with each key.

This is mainly useful to implement HashSet.ofList, so if you are considering using this, HashSet or HashSet.Raw might be a better fit for you.

Equations

• Std.ExtHashMap.unitOfList l = { inner := Std.ExtDHashMap.Const.unitOfList l }

@[inline]

def Std.ExtHashMap.filter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (f : α → β → Bool) (m : ExtHashMap α β) : ExtHashMap α β

Removes all mappings of the hash map for which the given function returns false.

Equations

• Std.ExtHashMap.filter f m = { inner := Std.ExtDHashMap.filter f m.inner }

@[inline]

def Std.ExtHashMap.map {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (f : α → β → γ) (m : ExtHashMap α β) : ExtHashMap α γ

Updates the values of the hash map by applying the given function to all mappings.

Equations

• Std.ExtHashMap.map f m = { inner := Std.ExtDHashMap.map f m.inner }

@[inline]

def Std.ExtHashMap.filterMap {α : Type u} {β : Type v} {γ : Type w} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (f : α → β → Option γ) (m : ExtHashMap α β) : ExtHashMap α γ

Updates the values of the hash map by applying the given function to all mappings, keeping only those mappings where the function returns some value.

Equations

• Std.ExtHashMap.filterMap f m = { inner := Std.ExtDHashMap.filterMap f m.inner }

@[inline]

def Std.ExtHashMap.modify {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (m : ExtHashMap α β) (a : α) (f : β → β) : ExtHashMap α β

Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.

Equations

• m.modify a f = { inner := Std.ExtDHashMap.Const.modify m.inner a f }

@[inline]

def Std.ExtHashMap.alter {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] (m : ExtHashMap α β) (a : α) (f : Option β → Option β) : ExtHashMap α β

Modifies in place the value associated with a given key, allowing creating new values and deleting values via an Option valued replacement function.

This function ensures that the value is used linearly.

Equations

• m.alter a f = { inner := Std.ExtDHashMap.Const.alter m.inner a f }

@[inline]

def Std.ExtHashMap.insertMany {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {ρ : Type w} [ForIn Id ρ (α × β)] (m : ExtHashMap α β) (l : ρ) : ExtHashMap α β

Inserts multiple mappings into the hash map by iterating over the given collection and calling insert. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for HashMap, DHashMap, HashMap.Raw and DHashMap.Raw. The insertMany function on HashSet and HashSet.Raw behaves differently: it will prefer the first appearance.

Equations

• m.insertMany l = { inner := Std.ExtDHashMap.Const.insertMany m.inner l }

@[inline]

def Std.ExtHashMap.insertManyIfNewUnit {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] {ρ : Type w} [ForIn Id ρ α] (m : ExtHashMap α Unit) (l : ρ) : ExtHashMap α Unit

Inserts multiple keys with the value () into the hash map by iterating over the given collection and calling insertIfNew. If the same key appears multiple times, the first occurrence takes precedence.

This is mainly useful to implement HashSet.insertMany, so if you are considering using this, HashSet or HashSet.Raw might be a better fit for you.

Equations

• m.insertManyIfNewUnit l = { inner := Std.ExtDHashMap.Const.insertManyIfNewUnit m.inner l }

@[inline]

def Std.ExtHashMap.unitOfArray {α : Type u} [BEq α] [Hashable α] (l : Array α) : ExtHashMap α Unit

Creates a hash map from an array of keys, associating the value () with each key.

This is mainly useful to implement HashSet.ofArray, so if you are considering using this, HashSet or HashSet.Raw might be a better fit for you.

Equations

• Std.ExtHashMap.unitOfArray l = { inner := Std.ExtDHashMap.Const.unitOfArray l }