Documentation

Batteries.Data.PairingHeap

A Heap is the nodes of the pairing heap. Each node have two pointers: child going to the first child of this node, and sibling goes to the next sibling of this tree. So it actually encodes a forest where each node has children node.child, node.child.sibling, node.child.sibling.sibling, etc.

Each edge in this forest denotes a le a b relation that has been checked, so the root is smaller than everything else under it.

Instances For
    Equations
    • Batteries.PairingHeapImp.instReprHeap = { reprPrec := Batteries.PairingHeapImp.reprHeap✝ }

    O(n). The number of elements in the heap.

    Equations
    Instances For

      A node containing a single element a.

      Equations
      Instances For

        O(1). Is the heap empty?

        Equations
        • Batteries.PairingHeapImp.Heap.nil.isEmpty = true
        • x.isEmpty = false
        Instances For
          @[specialize #[]]

          O(1). Merge two heaps. Ignore siblings.

          Equations
          • One or more equations did not get rendered due to their size.
          • Batteries.PairingHeapImp.Heap.merge le Batteries.PairingHeapImp.Heap.nil Batteries.PairingHeapImp.Heap.nil = Batteries.PairingHeapImp.Heap.nil
          Instances For
            @[specialize #[]]

            Auxiliary for Heap.deleteMin: merge the forest in pairs.

            Equations
            Instances For
              @[inline]

              O(1). Get the smallest element in the heap, including the passed in value a.

              Equations
              Instances For
                @[inline]

                O(1). Get the smallest element in the heap, if it has an element.

                Equations
                Instances For
                  @[inline]

                  Amortized O(log n). Find and remove the the minimum element from the heap.

                  Equations
                  Instances For
                    @[inline]

                    Amortized O(log n). Get the tail of the pairing heap after removing the minimum element.

                    Equations
                    Instances For
                      @[inline]

                      Amortized O(log n). Remove the minimum element of the heap.

                      Equations
                      Instances For

                        A predicate says there is no more than one tree.

                        Instances For
                          Equations
                          • Batteries.PairingHeapImp.instDecidableNoSibling = isTrue
                          • Batteries.PairingHeapImp.instDecidableNoSibling = isTrue
                          • Batteries.PairingHeapImp.instDecidableNoSibling = isFalse
                          theorem Batteries.PairingHeapImp.Heap.size_merge_node {α : Type u_1} (le : ααBool) (a₁ : α) (c₁ : Batteries.PairingHeapImp.Heap α) (s₁ : Batteries.PairingHeapImp.Heap α) (a₂ : α) (c₂ : Batteries.PairingHeapImp.Heap α) (s₂ : Batteries.PairingHeapImp.Heap α) :
                          (Batteries.PairingHeapImp.Heap.merge le (Batteries.PairingHeapImp.Heap.node a₁ c₁ s₁) (Batteries.PairingHeapImp.Heap.node a₂ c₂ s₂)).size = c₁.size + c₂.size + 2
                          theorem Batteries.PairingHeapImp.Heap.size_merge {α : Type u_1} (le : ααBool) {s₁ : Batteries.PairingHeapImp.Heap α} {s₂ : Batteries.PairingHeapImp.Heap α} (h₁ : s₁.NoSibling) (h₂ : s₂.NoSibling) :
                          (Batteries.PairingHeapImp.Heap.merge le s₁ s₂).size = s₁.size + s₂.size
                          @[irreducible]
                          theorem Batteries.PairingHeapImp.Heap.size_deleteMin {α : Type u_1} {le : ααBool} {a : α} {s' : Batteries.PairingHeapImp.Heap α} {s : Batteries.PairingHeapImp.Heap α} (h : s.NoSibling) (eq : Batteries.PairingHeapImp.Heap.deleteMin le s = some (a, s')) :
                          s.size = s'.size + 1
                          theorem Batteries.PairingHeapImp.Heap.size_tail? {α : Type u_1} {le : ααBool} {s' : Batteries.PairingHeapImp.Heap α} {s : Batteries.PairingHeapImp.Heap α} (h : s.NoSibling) :
                          Batteries.PairingHeapImp.Heap.tail? le s = some s's.size = s'.size + 1
                          theorem Batteries.PairingHeapImp.Heap.size_tail {α : Type u_1} (le : ααBool) {s : Batteries.PairingHeapImp.Heap α} (h : s.NoSibling) :
                          theorem Batteries.PairingHeapImp.Heap.size_deleteMin_lt {α : Type u_1} {le : ααBool} {a : α} {s' : Batteries.PairingHeapImp.Heap α} {s : Batteries.PairingHeapImp.Heap α} (eq : Batteries.PairingHeapImp.Heap.deleteMin le s = some (a, s')) :
                          s'.size < s.size
                          @[irreducible, specialize #[]]
                          def Batteries.PairingHeapImp.Heap.foldM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (le : ααBool) (s : Batteries.PairingHeapImp.Heap α) (init : β) (f : βαm β) :
                          m β

                          O(n log n). Monadic fold over the elements of a heap in increasing order, by repeatedly pulling the minimum element out of the heap.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[inline]
                            def Batteries.PairingHeapImp.Heap.fold {α : Type u_1} {β : Type u_2} (le : ααBool) (s : Batteries.PairingHeapImp.Heap α) (init : β) (f : βαβ) :
                            β

                            O(n log n). Fold over the elements of a heap in increasing order, by repeatedly pulling the minimum element out of the heap.

                            Equations
                            Instances For
                              @[inline]
                              def Batteries.PairingHeapImp.Heap.toArray {α : Type u_1} (le : ααBool) (s : Batteries.PairingHeapImp.Heap α) :

                              O(n log n). Convert the heap to an array in increasing order.

                              Equations
                              Instances For
                                @[inline]
                                def Batteries.PairingHeapImp.Heap.toList {α : Type u_1} (le : ααBool) (s : Batteries.PairingHeapImp.Heap α) :
                                List α

                                O(n log n). Convert the heap to a list in increasing order.

                                Equations
                                Instances For
                                  @[specialize #[]]
                                  def Batteries.PairingHeapImp.Heap.foldTreeM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (nil : β) (join : αββm β) :

                                  O(n). Fold a monadic function over the tree structure to accumulate a value.

                                  Equations
                                  Instances For
                                    @[inline]
                                    def Batteries.PairingHeapImp.Heap.foldTree {β : Type u_1} {α : Type u_2} (nil : β) (join : αβββ) (s : Batteries.PairingHeapImp.Heap α) :
                                    β

                                    O(n). Fold a function over the tree structure to accumulate a value.

                                    Equations
                                    Instances For

                                      O(n). Convert the heap to a list in arbitrary order.

                                      Equations
                                      Instances For

                                        O(n). Convert the heap to an array in arbitrary order.

                                        Equations
                                        Instances For
                                          def Batteries.PairingHeapImp.Heap.NodeWF {α : Type u_1} (le : ααBool) (a : α) :

                                          The well formedness predicate for a heap node. It asserts that:

                                          • If a is added at the top to make the forest into a tree, the resulting tree is a le-min-heap (if le is well-behaved)
                                          Equations
                                          Instances For
                                            inductive Batteries.PairingHeapImp.Heap.WF {α : Type u_1} (le : ααBool) :

                                            The well formedness predicate for a pairing heap. It asserts that:

                                            • There is no more than one tree.
                                            • It is a le-min-heap (if le is well-behaved)
                                            Instances For
                                              def Batteries.PairingHeap (α : Type u) (le : ααBool) :
                                              Type (max 0 u)

                                              A pairing heap is a data structure which supports the following primary operations:

                                              The first two operations are known as a "priority queue", so this could be called a "mergeable priority queue". The standard choice for a priority queue is a binary heap, which supports insert and deleteMin in O(log n), but merge is O(n). With a PairingHeap, insert and merge are O(1), deleteMin is amortized O(log n).

                                              Note that deleteMin may be O(n) in a single operation. So if you need an efficient persistent priority queue, you should use other data structures with better worst-case time.

                                              Equations
                                              Instances For
                                                @[inline]
                                                def Batteries.mkPairingHeap (α : Type u) (le : ααBool) :

                                                O(1). Make a new empty pairing heap.

                                                Equations
                                                Instances For
                                                  @[inline]
                                                  def Batteries.PairingHeap.empty {α : Type u} {le : ααBool} :

                                                  O(1). Make a new empty pairing heap.

                                                  Equations
                                                  Instances For
                                                    instance Batteries.PairingHeap.instInhabited {α : Type u} {le : ααBool} :
                                                    Equations
                                                    • Batteries.PairingHeap.instInhabited = { default := Batteries.PairingHeap.empty }
                                                    @[inline]
                                                    def Batteries.PairingHeap.isEmpty {α : Type u} {le : ααBool} (b : Batteries.PairingHeap α le) :

                                                    O(1). Is the heap empty?

                                                    Equations
                                                    • b.isEmpty = b.val.isEmpty
                                                    Instances For
                                                      @[inline]
                                                      def Batteries.PairingHeap.size {α : Type u} {le : ααBool} (b : Batteries.PairingHeap α le) :

                                                      O(n). The number of elements in the heap.

                                                      Equations
                                                      • b.size = b.val.size
                                                      Instances For
                                                        @[inline]
                                                        def Batteries.PairingHeap.singleton {α : Type u} {le : ααBool} (a : α) :

                                                        O(1). Make a new heap containing a.

                                                        Equations
                                                        Instances For
                                                          @[inline]
                                                          def Batteries.PairingHeap.merge {α : Type u} {le : ααBool} :

                                                          O(1). Merge the contents of two heaps.

                                                          Equations
                                                          Instances For
                                                            @[inline]
                                                            def Batteries.PairingHeap.insert {α : Type u} {le : ααBool} (a : α) (h : Batteries.PairingHeap α le) :

                                                            O(1). Add element a to the given heap h.

                                                            Equations
                                                            Instances For
                                                              def Batteries.PairingHeap.ofList {α : Type u} (le : ααBool) (as : List α) :

                                                              O(n log n). Construct a heap from a list by inserting all the elements.

                                                              Equations
                                                              Instances For
                                                                def Batteries.PairingHeap.ofArray {α : Type u} (le : ααBool) (as : Array α) :

                                                                O(n log n). Construct a heap from a list by inserting all the elements.

                                                                Equations
                                                                Instances For
                                                                  @[inline]
                                                                  def Batteries.PairingHeap.deleteMin {α : Type u} {le : ααBool} (b : Batteries.PairingHeap α le) :

                                                                  Amortized O(log n). Remove and return the minimum element from the heap.

                                                                  Equations
                                                                  Instances For
                                                                    @[inline]
                                                                    def Batteries.PairingHeap.head? {α : Type u} {le : ααBool} (b : Batteries.PairingHeap α le) :

                                                                    O(1). Returns the smallest element in the heap, or none if the heap is empty.

                                                                    Equations
                                                                    • b.head? = b.val.head?
                                                                    Instances For
                                                                      @[inline]
                                                                      def Batteries.PairingHeap.head! {α : Type u} {le : ααBool} [Inhabited α] (b : Batteries.PairingHeap α le) :
                                                                      α

                                                                      O(1). Returns the smallest element in the heap, or panics if the heap is empty.

                                                                      Equations
                                                                      • b.head! = b.head?.get!
                                                                      Instances For
                                                                        @[inline]
                                                                        def Batteries.PairingHeap.headI {α : Type u} {le : ααBool} [Inhabited α] (b : Batteries.PairingHeap α le) :
                                                                        α

                                                                        O(1). Returns the smallest element in the heap, or default if the heap is empty.

                                                                        Equations
                                                                        • b.headI = b.head?.getD default
                                                                        Instances For
                                                                          @[inline]
                                                                          def Batteries.PairingHeap.tail? {α : Type u} {le : ααBool} (b : Batteries.PairingHeap α le) :

                                                                          Amortized O(log n). Removes the smallest element from the heap, or none if the heap is empty.

                                                                          Equations
                                                                          Instances For
                                                                            @[inline]
                                                                            def Batteries.PairingHeap.tail {α : Type u} {le : ααBool} (b : Batteries.PairingHeap α le) :

                                                                            Amortized O(log n). Removes the smallest element from the heap, if possible.

                                                                            Equations
                                                                            Instances For
                                                                              @[inline]
                                                                              def Batteries.PairingHeap.toList {α : Type u} {le : ααBool} (b : Batteries.PairingHeap α le) :
                                                                              List α

                                                                              O(n log n). Convert the heap to a list in increasing order.

                                                                              Equations
                                                                              Instances For
                                                                                @[inline]
                                                                                def Batteries.PairingHeap.toArray {α : Type u} {le : ααBool} (b : Batteries.PairingHeap α le) :

                                                                                O(n log n). Convert the heap to an array in increasing order.

                                                                                Equations
                                                                                Instances For
                                                                                  @[inline]
                                                                                  def Batteries.PairingHeap.toListUnordered {α : Type u} {le : ααBool} (b : Batteries.PairingHeap α le) :
                                                                                  List α

                                                                                  O(n). Convert the heap to a list in arbitrary order.

                                                                                  Equations
                                                                                  • b.toListUnordered = b.val.toListUnordered
                                                                                  Instances For
                                                                                    @[inline]
                                                                                    def Batteries.PairingHeap.toArrayUnordered {α : Type u} {le : ααBool} (b : Batteries.PairingHeap α le) :

                                                                                    O(n). Convert the heap to an array in arbitrary order.

                                                                                    Equations
                                                                                    • b.toArrayUnordered = b.val.toArrayUnordered
                                                                                    Instances For