Documentation

Mathlib.Data.BinaryHeap

structure BinaryHeap (α : Type u_1) (lt : ααBool) :
Type u_1

A max-heap data structure.

Instances For
    def BinaryHeap.heapifyDown {α : Type u_1} (lt : ααBool) (a : Array α) (i : Fin (Array.size a)) :
    { a' : Array α // Array.size a' = Array.size a }

    Core operation for binary heaps, expressed directly on arrays. Given an array which is a max-heap, push item i down to restore the max-heap property.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem BinaryHeap.size_heapifyDown {α : Type u_1} (lt : ααBool) (a : Array α) (i : Fin (Array.size a)) :
      def BinaryHeap.mkHeap {α : Type u_1} (lt : ααBool) (a : Array α) :
      { a' : Array α // Array.size a' = Array.size a }

      Core operation for binary heaps, expressed directly on arrays. Construct a heap from an unsorted array, by heapifying all the elements.

      Equations
      Instances For
        def BinaryHeap.mkHeap.loop {α : Type u_1} (lt : ααBool) (i : Nat) (a : Array α) :
        i Array.size a{ a' : Array α // Array.size a' = Array.size a }
        Equations
        • One or more equations did not get rendered due to their size.
        • BinaryHeap.mkHeap.loop lt 0 x x_1 = { val := x, property := }
        Instances For
          @[simp]
          theorem BinaryHeap.size_mkHeap {α : Type u_1} (lt : ααBool) (a : Array α) :
          def BinaryHeap.heapifyUp {α : Type u_1} (lt : ααBool) (a : Array α) (i : Fin (Array.size a)) :
          { a' : Array α // Array.size a' = Array.size a }

          Core operation for binary heaps, expressed directly on arrays. Given an array which is a max-heap, push item i up to restore the max-heap property.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem BinaryHeap.size_heapifyUp {α : Type u_1} (lt : ααBool) (a : Array α) (i : Fin (Array.size a)) :
            def BinaryHeap.empty {α : Type u_1} (lt : ααBool) :

            O(1). Build a new empty heap.

            Equations
            Instances For
              instance BinaryHeap.instInhabitedBinaryHeap {α : Type u_1} (lt : ααBool) :
              Equations
              instance BinaryHeap.instEmptyCollectionBinaryHeap {α : Type u_1} (lt : ααBool) :
              Equations
              def BinaryHeap.singleton {α : Type u_1} (lt : ααBool) (x : α) :

              O(1). Build a one-element heap.

              Equations
              Instances For
                def BinaryHeap.size {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) :

                O(1). Get the number of elements in a BinaryHeap.

                Equations
                Instances For
                  def BinaryHeap.get {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) (i : Fin (BinaryHeap.size self)) :
                  α

                  O(1). Get an element in the heap by index.

                  Equations
                  Instances For
                    def BinaryHeap.insert {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) (x : α) :

                    O(log n). Insert an element into a BinaryHeap, preserving the max-heap property.

                    Equations
                    Instances For
                      @[simp]
                      theorem BinaryHeap.size_insert {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) (x : α) :
                      def BinaryHeap.max {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) :

                      O(1). Get the maximum element in a BinaryHeap.

                      Equations
                      Instances For
                        def BinaryHeap.popMaxAux {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) :
                        { a' : BinaryHeap α lt // BinaryHeap.size a' = BinaryHeap.size self - 1 }

                        Auxiliary for popMax.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def BinaryHeap.popMax {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) :

                          O(log n). Remove the maximum element from a BinaryHeap. Call max first to actually retrieve the maximum element.

                          Equations
                          Instances For
                            @[simp]
                            theorem BinaryHeap.size_popMax {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) :
                            def BinaryHeap.extractMax {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) :

                            O(log n). Return and remove the maximum element from a BinaryHeap.

                            Equations
                            Instances For
                              theorem BinaryHeap.size_pos_of_max {α : Type u_1} {x : α} {lt : ααBool} {self : BinaryHeap α lt} (e : BinaryHeap.max self = some x) :
                              def BinaryHeap.insertExtractMax {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) (x : α) :
                              α × BinaryHeap α lt

                              O(log n). Equivalent to extractMax (self.insert x), except that extraction cannot fail.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def BinaryHeap.replaceMax {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) (x : α) :

                                O(log n). Equivalent to (self.max, self.popMax.insert x).

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  def BinaryHeap.decreaseKey {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) (i : Fin (BinaryHeap.size self)) (x : α) :

                                  O(log n). Replace the value at index i by x. Assumes that x ≤ self.get i.

                                  Equations
                                  Instances For
                                    def BinaryHeap.increaseKey {α : Type u_1} {lt : ααBool} (self : BinaryHeap α lt) (i : Fin (BinaryHeap.size self)) (x : α) :

                                    O(log n). Replace the value at index i by x. Assumes that self.get i ≤ x.

                                    Equations
                                    Instances For
                                      def Array.toBinaryHeap {α : Type u_1} (lt : ααBool) (a : Array α) :

                                      O(n). Convert an unsorted array to a BinaryHeap.

                                      Equations
                                      Instances For
                                        @[specialize #[]]
                                        def Array.heapSort {α : Type u_1} (a : Array α) (lt : ααBool) :

                                        O(n log n). Sort an array using a BinaryHeap.

                                        Equations
                                        Instances For
                                          def Array.heapSort.loop {α : Type u_1} (lt : ααBool) (a : BinaryHeap α fun (y x : α) => lt x y) (out : Array α) :
                                          Equations
                                          Instances For