Documentation

Std.Data.HashSet.Basic

Hash sets #

This module develops the type Std.Data.HashSet of dependent hash sets.

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

See the module Std.Data.HashSet.Raw for a variant of this type which is safe to use in nested inductive types.

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

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.

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.Data.HashSet.Raw and Std.Data.HashSet.Raw.WF unbundle the invariant from the hash set. When in doubt, prefer HashSet over HashSet.Raw.

Instances For
    @[inline]
    def Std.HashSet.empty {α : Type u} [BEq α] [Hashable α] (capacity : optParam Nat 8) :

    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
    Instances For
      Equations
      • Std.HashSet.instEmptyCollection = { emptyCollection := Std.HashSet.empty }
      Equations
      • Std.HashSet.instInhabited = { default := }
      @[inline]
      def Std.HashSet.insert {α : Type u} :
      {x : BEq α} → {x_1 : Hashable α} → Std.HashSet ααStd.HashSet α

      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.

      Equations
      • m.insert a = { inner := m.inner.insertIfNew a () }
      Instances For
        instance Std.HashSet.instSingleton {α : Type u} :
        {x : BEq α} → {x_1 : Hashable α} → Singleton α (Std.HashSet α)
        Equations
        • Std.HashSet.instSingleton = { singleton := fun (a : α) => Std.HashSet.empty.insert a }
        instance Std.HashSet.instInsert {α : Type u} :
        {x : BEq α} → {x_1 : Hashable α} → Insert α (Std.HashSet α)
        Equations
        • Std.HashSet.instInsert = { insert := fun (a : α) (s : Std.HashSet α) => s.insert a }
        @[inline]
        def Std.HashSet.containsThenInsert {α : Type u} :
        {x : BEq α} → {x_1 : Hashable α} → Std.HashSet ααBool × Std.HashSet α

        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 })
        Instances For
          @[inline]
          def Std.HashSet.contains {α : Type u} :
          {x : BEq α} → {x_1 : Hashable α} → Std.HashSet αα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
          Instances For
            instance Std.HashSet.instMembership {α : Type u} [BEq α] [Hashable α] :
            Equations
            • Std.HashSet.instMembership = { mem := fun (m : Std.HashSet α) (a : α) => a m.inner }
            instance Std.HashSet.instDecidableMem {α : Type u} [BEq α] [Hashable α] {m : Std.HashSet α} {a : α} :
            Equations
            @[inline]
            def Std.HashSet.erase {α : Type u} :
            {x : BEq α} → {x_1 : Hashable α} → Std.HashSet ααStd.HashSet α

            Removes the element if it exists.

            Equations
            • m.erase a = { inner := m.inner.erase a }
            Instances For
              @[inline]
              def Std.HashSet.size {α : Type u} :
              {x : BEq α} → {x_1 : Hashable α} → Std.HashSet αNat

              The number of elements present in the set

              Equations
              • m.size = m.inner.size
              Instances For
                @[inline]
                def Std.HashSet.get? {α : Type u} :
                {x : BEq α} → {x_1 : Hashable α} → Std.HashSet αα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
                Instances For
                  @[inline]
                  def Std.HashSet.get {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet α) (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
                  Instances For
                    @[inline]
                    def Std.HashSet.getD {α : Type u} [BEq α] [Hashable α] (m : Std.HashSet α) (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
                    Instances For
                      @[inline]
                      def Std.HashSet.get! {α : Type u} [BEq α] [Hashable α] [Inhabited α] (m : Std.HashSet α) (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
                      Instances For
                        @[inline]
                        def Std.HashSet.isEmpty {α : Type u} :
                        {x : BEq α} → {x_1 : Hashable α} → Std.HashSet α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
                        Instances For

                          We currently do not provide lemmas for the functions below.

                          @[inline]
                          def Std.HashSet.filter {α : Type u} :
                          {x : BEq α} → {x_1 : Hashable α} → (αBool)Std.HashSet αStd.HashSet α

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

                          Equations
                          Instances For
                            @[inline]
                            def Std.HashSet.partition {α : Type u} :
                            {x : BEq α} → {x_1 : Hashable α} → (αBool)Std.HashSet αStd.HashSet α × Std.HashSet α

                            Partition a hashset into two hashsets based on a predicate.

                            Equations
                            Instances For
                              @[inline]
                              def Std.HashSet.foldM {α : Type u} :
                              {x : BEq α} → {x_1 : Hashable α} → {m : Type v → Type v} → [inst : Monad m] → {β : Type v} → (βαm β)βStd.HashSet αm β

                              Monadically computes a value by folding the given function over the elements in the hash set in some order.

                              Equations
                              Instances For
                                @[inline]
                                def Std.HashSet.fold {α : Type u} :
                                {x : BEq α} → {x_1 : Hashable α} → {β : Type v} → (βαβ)βStd.HashSet αβ

                                Folds the given function over the elements of the hash set in some order.

                                Equations
                                Instances For
                                  @[inline]
                                  def Std.HashSet.forM {α : Type u} :
                                  {x : BEq α} → {x_1 : Hashable α} → {m : Type v → Type v} → [inst : Monad m] → (αm PUnit)Std.HashSet αm PUnit

                                  Carries out a monadic action on each element in the hash set in some order.

                                  Equations
                                  Instances For
                                    @[inline]
                                    def Std.HashSet.forIn {α : Type u} :
                                    {x : BEq α} → {x_1 : Hashable α} → {m : Type v → Type v} → [inst : Monad m] → {β : Type v} → (αβm (ForInStep β))βStd.HashSet αm β

                                    Support for the for loop construct in do blocks.

                                    Equations
                                    Instances For
                                      instance Std.HashSet.instForM {α : Type u} [BEq α] [Hashable α] {m : Type v → Type v} :
                                      ForM m (Std.HashSet α) α
                                      Equations
                                      instance Std.HashSet.instForIn {α : Type u} [BEq α] [Hashable α] {m : Type v → Type v} :
                                      ForIn m (Std.HashSet α) α
                                      Equations
                                      @[inline]
                                      def Std.HashSet.all {α : Type u} :
                                      {x : BEq α} → {x_1 : Hashable α} → Std.HashSet α(αBool)Bool

                                      Check if all elements satisfy the predicate, short-circuiting if a predicate fails.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[inline]
                                        def Std.HashSet.any {α : Type u} :
                                        {x : BEq α} → {x_1 : Hashable α} → Std.HashSet α(αBool)Bool

                                        Check if any element satisfies the predicate, short-circuiting if a predicate succeeds.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[inline]
                                          def Std.HashSet.toList {α : Type u} :
                                          {x : BEq α} → {x_1 : Hashable α} → Std.HashSet αList α

                                          Transforms the hash set into a list of elements in some order.

                                          Equations
                                          • m.toList = m.inner.keys
                                          Instances For
                                            @[inline]
                                            def Std.HashSet.toArray {α : Type u} :
                                            {x : BEq α} → {x_1 : Hashable α} → Std.HashSet αArray α

                                            Transforms the hash set into an array of elements in some order.

                                            Equations
                                            • m.toArray = m.inner.keysArray
                                            Instances For
                                              @[inline]
                                              def Std.HashSet.insertMany {α : Type u} :
                                              {x : BEq α} → {x_1 : Hashable α} → {ρ : Type v} → [inst : ForIn Id ρ α] → Std.HashSet αρStd.HashSet α

                                              Inserts multiple elements into the hash set. 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
                                              • m.insertMany l = { inner := m.inner.insertManyUnit l }
                                              Instances For
                                                @[inline]
                                                def Std.HashSet.ofList {α : Type u} [BEq α] [Hashable α] (l : List α) :

                                                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
                                                Instances For
                                                  @[inline]
                                                  def Std.HashSet.ofArray {α : Type u} [BEq α] [Hashable α] (l : Array α) :

                                                  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
                                                  Instances For
                                                    @[inline]
                                                    def Std.HashSet.union {α : Type u} [BEq α] [Hashable α] (m₁ : Std.HashSet α) (m₂ : Std.HashSet α) :

                                                    Computes the union of the given hash sets, by traversing m₂ and inserting its elements into m₁.

                                                    Equations
                                                    Instances For
                                                      instance Std.HashSet.instUnion {α : Type u} [BEq α] [Hashable α] :
                                                      Equations
                                                      • Std.HashSet.instUnion = { union := Std.HashSet.union }
                                                      def Std.HashSet.Internal.numBuckets {α : Type u} :
                                                      {x : BEq α} → {x_1 : Hashable α} → Std.HashSet αNat

                                                      Returns the number of buckets in the internal representation of the hash set. This function may be useful for things like monitoring system health, but it should be considered an internal implementation detail.

                                                      Equations
                                                      Instances For
                                                        instance Std.HashSet.instRepr {α : Type u} [BEq α] [Hashable α] [Repr α] :
                                                        Equations