Extensional hash sets

This module develops the type Std.ExtHashSet of extensional hash sets.

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

structure Std.ExtHashSet (α : Type u) [BEq α] [Hashable α] : Type u

Hash sets.

This is a simple separate-chaining hash table. The data of the hash set consists of a cached size and an array of buckets, where each bucket is a linked list of keys. The number of buckets is always a power of two. The hash set 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 set is used linearly to avoid expensive copies.

The hash set uses == (provided by the BEq typeclass) to compare elements 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 sets, Std.ExtHashSet 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 sets.

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

• inner : ExtHashMap α Unit

  Internal implementation detail of the hash set.

@[inline]

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

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

Equations

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

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

Equations

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

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

Equations

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

@[inline]

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

Inserts the given element into the set. If the hash set already contains an element that is equal (with regard to ==) to the given element, then the hash set is returned unchanged.

Note: this non-replacement behavior is true for ExtHashSet and ExtHashSet.Raw. The insert function on ExtHashMap, DExtHashMap, ExtHashMap.Raw and DExtHashMap.Raw behaves differently: it will overwrite an existing mapping.

Equations

• m.insert a = { inner := m.inner.insertIfNew a () }

instance Std.ExtHashSet.instSingletonOfEquivBEqOfLawfulHashable {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] : Singleton α (ExtHashSet α)

Equations

• Std.ExtHashSet.instSingletonOfEquivBEqOfLawfulHashable = { singleton := fun (a : α) => ∅.insert a }

instance Std.ExtHashSet.instInsertOfEquivBEqOfLawfulHashable {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} [EquivBEq α] [LawfulHashable α] : Insert α (ExtHashSet α)

Equations

• Std.ExtHashSet.instInsertOfEquivBEqOfLawfulHashable = { insert := fun (a : α) (s : Std.ExtHashSet α) => s.insert a }

@[inline]

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

Checks whether an element is present in a set and inserts the element if it was not found. If the hash set already contains an element that is equal (with regard to ==) to the given element, then the hash set is returned unchanged.

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

Equations

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

@[inline]

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

Returns true if the given key is present in the set. 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 use == for comparisons, while for hash sets, both use ==.

Equations

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

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

Equations

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

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

Equations

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

@[inline]

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

Removes the element if it exists.

Equations

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

@[inline]

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

The number of elements present in the set

Equations

• m.size = m.inner.size

@[inline]

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

Checks if given key is contained and returns the key if it is, otherwise none. The result in the some case is guaranteed to be pointer equal to the key in the set.

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

Checks if given key is contained and returns the key if it is, otherwise fallback. If they key is contained the result is guaranteed to be pointer equal to the key in the set.

Equations

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

@[inline]

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

Checks if given key is contained and returns the key if it is, otherwise panics. If no panic occurs the result is guaranteed to be pointer equal to the key in the set.

Equations

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

@[inline]

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

Returns true if the hash set contains no elements.

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 m.contains a = false for all a.

Equations

• m.isEmpty = m.inner.isEmpty

@[inline]

def Std.ExtHashSet.ofList {α : Type u} [BEq α] [Hashable α] (l : List α) : ExtHashSet α

Creates a hash set from a list of elements. Note that unlike repeatedly calling insert, if the collection contains multiple elements that are equal (with regard to ==), then the last element in the collection will be present in the returned hash set.

Equations

• Std.ExtHashSet.ofList l = { inner := Std.ExtHashMap.unitOfList l }

@[inline]

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

Removes all elements from the hash set for which the given function returns false.

Equations

• Std.ExtHashSet.filter f m = { inner := Std.ExtHashMap.filter (fun (a : α) (x : Unit) => f a) m.inner }

@[inline]

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

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

Note: this precedence behavior is true for ExtHashSet and ExtHashSet.Raw. The insertMany function on ExtHashMap, DExtHashMap, ExtHashMap.Raw and DExtHashMap.Raw behaves differently: it will prefer the last appearance.

Equations

• m.insertMany l = { inner := m.inner.insertManyIfNewUnit l }

@[inline]

def Std.ExtHashSet.ofArray {α : Type u} [BEq α] [Hashable α] (l : Array α) : ExtHashSet α

Creates a hash set from an array of elements. Note that unlike repeatedly calling insert, if the collection contains multiple elements that are equal (with regard to ==), then the last element in the collection will be present in the returned hash set.

Equations

• Std.ExtHashSet.ofArray l = { inner := Std.ExtHashMap.unitOfArray l }