Hash table with separate chaining

14 fully proved

Hash Table

StructureHash table with separate chaining#✓fully proved

For a key type \(\alpha\), a value type \(\beta\) and a hash function \(h : \alpha \to \mathbb{N}\), a hash table with hash function \(h\) consists of a positive number \(m\) of buckets and, for each bucket index \(i < m\), a chain stored at bucket \(i\): an association list of key–value pairs whose keys are pairwise distinct. The structure itself does not require keys to lie in their hash-selected bucket.

No expected constant-time bound is claimed because the model supplies neither a probability distribution nor a probabilistic assumption about the hash function.

public structure HashTable (α : Type u) (β : Type v) (hash : α → Nat) where
  /-- The positive number of chains in the table. -/
  bucketCount : Nat
  /-- The table has at least one chain. -/
  bucketCount_pos : 0 < bucketCount
  /-- The canonical association list stored at each bucket. -/
  buckets : Fin bucketCount → AList (fun _ : α => β)

Used by 11

Used byFinite map represented by a hash table · Insertion commutes with the abstraction · Empty hash table · Insertion into a hash table · Hash table lookup · Lookup agrees with the abstraction · Hash table lookup after insertion · Insertion does not affect other keys · Valid hash table · The empty hash table is valid · Insertion preserves validity of a hash table

DefinitionEmpty hash table#✓fully proved

For a hash function \(h\) and a positive integer \(m\), the empty hash table with hash function \(h\) has \(m\) buckets, each holding the empty chain.

public def empty {α : Type u} {β : Type v} (hash : α → Nat)
    (bucketCount : Nat) (bucketCount_pos : 0 < bucketCount) : HashTable α β hash where
  bucketCount := bucketCount
  bucketCount_pos := bucketCount_pos
  buckets := fun _ => ∅

Uses 1 · Used by 3

Statement usesHash table with separate chaining

Used byThe empty hash table represents the empty map · Lookup in the empty hash table · The empty hash table is valid

DefinitionHash table lookup#✓fully proved

For a hash table with hash function \(h\) and \(m\) buckets, looking up a key \(k\) searches only the bucket with index \(h(k) \bmod m\): the result is the value bound to \(k\) in that bucket's association list, or nothing if \(k\) has no binding there.

public def lookup {α : Type u} {β : Type v} {hash : α → Nat} [DecidableEq α]
    (key : α) (table : HashTable α β hash) : Option β :=
  AList.lookup key (table.buckets
    ⟨hash key % table.bucketCount, Nat.mod_lt _ table.bucketCount_pos⟩)

Uses 1 · Used by 5

Statement usesHash table with separate chaining

Used byInsertion commutes with the abstraction · Lookup agrees with the abstraction · Lookup in the empty hash table · Hash table lookup after insertion · Insertion does not affect other keys

DefinitionInsertion into a hash table#✓fully proved

Inserting a key \(k\) with value \(v\) into a hash table with \(m\) buckets and hash function \(h\) keeps the bucket count and every bucket other than bucket \(h(k) \bmod m\), and replaces the chain at bucket \(h(k) \bmod m\) by that chain with \(k\) bound to \(v\): any earlier binding of \(k\) in that chain is removed and the binding of \(k\) to \(v\) is added.

public def insert {α : Type u} {β : Type v} {hash : α → Nat} [DecidableEq α]
    (key : α) (value : β) (table : HashTable α β hash) : HashTable α β hash where
  bucketCount := table.bucketCount
  bucketCount_pos := table.bucketCount_pos
  buckets := Function.update table.buckets
    ⟨hash key % table.bucketCount, Nat.mod_lt _ table.bucketCount_pos⟩
    (AList.insert key value (table.buckets
      ⟨hash key % table.bucketCount, Nat.mod_lt _ table.bucketCount_pos⟩))

Uses 1 · Used by 4

Statement usesHash table with separate chaining

Used byInsertion commutes with the abstraction · Hash table lookup after insertion · Insertion does not affect other keys · Insertion preserves validity of a hash table

DefinitionValid hash table#✓fully proved

A hash table with hash function \(h\) and \(m\) buckets is valid when every binding lies in its hash-selected bucket: for every bucket index \(i < m\) and every key \(k\), if \(k\) has a binding in bucket \(i\), then \(h(k) \bmod m = i\).

Keys within a single bucket are distinct automatically, since each bucket is an association list.

public def Valid {α : Type u} {β : Type v} {hash : α → Nat} [DecidableEq α]
    (table : HashTable α β hash) : Prop :=
  ∀ (index : Fin table.bucketCount) (key : α),
    (AList.lookup key (table.buckets index)).isSome →
      (⟨hash key % table.bucketCount, Nat.mod_lt _ table.bucketCount_pos⟩ :
        Fin table.bucketCount) = index

Uses 1 · Used by 4

Statement usesHash table with separate chaining

Used byInsertion commutes with the abstraction · Lookup agrees with the abstraction · The empty hash table is valid · Insertion preserves validity of a hash table

DefinitionFinite map represented by a hash table#✓fully proved

The finite map represented by a hash table with \(m\) buckets is built from the list of all bindings of buckets \(0, 1, \dots, m - 1\), concatenated in this order: it binds exactly the keys occurring in this list, and binds each such key to the value of its first binding in the list.

public def abstraction {α : Type u} {β : Type v} {hash : α → Nat} [DecidableEq α]
    (table : HashTable α β hash) : Finmap (fun _ : α => β) :=
  ((List.finRange table.bucketCount).flatMap fun index =>
    (table.buckets index).entries).toFinmap

Uses 1 · Used by 3

Statement usesHash table with separate chaining

Used byThe empty hash table represents the empty map · Insertion commutes with the abstraction · Lookup agrees with the abstraction

TheoremThe empty hash table is valid#✓fully proved

For every hash function \(h\) and every positive bucket count \(m\), the empty hash table with hash function \(h\) and \(m\) buckets is valid.

public theorem valid_empty {α : Type u} {β : Type v} (hash : α → Nat) [DecidableEq α]
    (bucketCount : Nat) (bucketCount_pos : 0 < bucketCount) :
    Valid (empty hash bucketCount bucketCount_pos : HashTable α β hash)

Uses 3

Statement usesValid hash table · Empty hash table

Proof usesHash table with separate chaining

TheoremLookup in the empty hash table#✓fully proved

For every hash function \(h\), every positive bucket count \(m\) and every key \(k\), looking up \(k\) in the empty hash table with hash function \(h\) and \(m\) buckets finds no value.

@[simp]
public theorem lookup_empty {α : Type u} {β : Type v} (hash : α → Nat) [DecidableEq α]
    (bucketCount : Nat) (bucketCount_pos : 0 < bucketCount) (key : α) :
    lookup key (empty hash bucketCount bucketCount_pos : HashTable α β hash) = none

Uses 2

Statement usesEmpty hash table · Hash table lookup

TheoremThe empty hash table represents the empty map#✓fully proved

For every hash function \(h\) and every positive bucket count \(m\), the finite map represented by the empty hash table with hash function \(h\) and \(m\) buckets is the empty finite map.

@[simp]
public theorem abstraction_empty {α : Type u} {β : Type v} (hash : α → Nat) [DecidableEq α]
    (bucketCount : Nat) (bucketCount_pos : 0 < bucketCount) :
    abstraction (empty hash bucketCount bucketCount_pos : HashTable α β hash) = ∅

Uses 2

Statement usesFinite map represented by a hash table · Empty hash table

TheoremHash table lookup after insertion#✓fully proved

For every hash table \(T\), every key \(k\) and every value \(v\), looking up \(k\) in the table obtained by inserting \(k\) with value \(v\) into \(T\) returns \(v\).

public theorem lookup_insert {α : Type u} {β : Type v} {hash : α → Nat} [DecidableEq α]
    (key : α) (value : β) (table : HashTable α β hash) :
    lookup key (insert key value table) = some value

Uses 3 · Used by 1

Statement usesHash table with separate chaining · Insertion into a hash table · Hash table lookup

Used byInsertion commutes with the abstraction

TheoremInsertion does not affect other keys#✓fully proved

For every hash table \(T\), all keys \(k \ne k'\) and every value \(v\), looking up \(k'\) in the table obtained by inserting \(k\) with value \(v\) into \(T\) gives the same result as looking up \(k'\) in \(T\), also when \(k\) and \(k'\) lie in the same bucket.

public theorem lookup_insert_of_ne {α : Type u} {β : Type v} {hash : α → Nat}
    [DecidableEq α] (key other : α) (value : β) (table : HashTable α β hash)
    (different : other ≠ key) :
    lookup other (insert key value table) = lookup other table

Uses 3 · Used by 1

Statement usesHash table with separate chaining · Insertion into a hash table · Hash table lookup

Used byInsertion commutes with the abstraction

TheoremInsertion preserves validity of a hash table#✓fully proved

If a hash table is valid, then the table obtained from it by inserting a key \(k\) with value \(v\) (adding a new binding for \(k\), or replacing the existing one) is again valid.

public theorem valid_insert {α : Type u} {β : Type v} {hash : α → Nat} [DecidableEq α]
    (key : α) (value : β) (table : HashTable α β hash) (valid : Valid table) :
    Valid (insert key value table)

Uses 3 · Used by 1

Statement usesHash table with separate chaining · Valid hash table · Insertion into a hash table

Used byInsertion commutes with the abstraction

TheoremLookup agrees with the abstraction#✓fully proved

For every valid hash table \(T\) and every key \(k\), looking up \(k\) in the finite map represented by \(T\) gives the same result as looking up \(k\) in \(T\).

public theorem lookup_abstraction {α : Type u} {β : Type v} {hash : α → Nat}
    [DecidableEq α] (key : α) (table : HashTable α β hash) (valid : Valid table) :
    Finmap.lookup key (abstraction table) = lookup key table

Uses 4 · Used by 1

Statement usesHash table with separate chaining · Valid hash table · Finite map represented by a hash table · Hash table lookup

Used byInsertion commutes with the abstraction

TheoremInsertion commutes with the abstraction#✓fully proved

For every valid hash table \(T\), every key \(k\) and every value \(v\), the finite map represented by the table obtained by inserting \(k\) with value \(v\) into \(T\) equals the finite map represented by \(T\) with \(k\) bound to \(v\), replacing any earlier binding of \(k\).

public theorem abstraction_insert {α : Type u} {β : Type v} {hash : α → Nat}
    [DecidableEq α] (key : α) (value : β) (table : HashTable α β hash)
    (valid : Valid table) :
    abstraction (insert key value table) = Finmap.insert key value (abstraction table)

Uses 9

Statement usesHash table with separate chaining · Valid hash table · Finite map represented by a hash table · Insertion into a hash table

Proof usesHash table lookup · Lookup agrees with the abstraction · Hash table lookup after insertion · Insertion does not affect other keys · Insertion preserves validity of a hash table

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.