Documentation

Batteries.Data.Vector.Basic

Vectors #

Vector α n is an array with a statically fixed size n. It combines the benefits of Lean's special support for Arrays that offer O(1) accesses and in-place mutations for arrays with no more than one reference, with static guarantees about the size of the underlying array.

structure Batteries.Vector (α : Type u) (n : Nat) :

Vector α n is an Array α whose size is statically fixed to n

  • toArray : Array α

    Internally, a vector is stored as an array for fast access

  • size_eq : self.toArray.size = n

    size_eq fixes the size of toArray statically

Instances For
    theorem Batteries.Vector.size_eq {α : Type u} {n : Nat} (self : Batteries.Vector α n) :
    self.toArray.size = n

    size_eq fixes the size of toArray statically

    instance Batteries.instReprVector :
    {α : Type u_1} → {n : Nat} → [inst : Repr α] → Repr (Batteries.Vector α n)
    Equations
    • Batteries.instReprVector = { reprPrec := Batteries.reprVector✝ }
    instance Batteries.instDecidableEqVector :
    {α : Type u_1} → {n : Nat} → [inst : DecidableEq α] → DecidableEq (Batteries.Vector α n)
    Equations
    • Batteries.instDecidableEqVector = Batteries.decEqVector✝

    Syntax for Vector α n

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Batteries.Vector.elimAsArray {α : Type u_1} {motive : {n : Nat} → Batteries.Vector α nSort u} (mk : (a : Array α) → motive { toArray := a, size_eq := }) {n : Nat} (v : Batteries.Vector α n) :
      motive v

      Custom eliminator for Vector α n through Array α

      Equations
      Instances For
        def Batteries.Vector.elimAsList {α : Type u_1} {motive : {n : Nat} → Batteries.Vector α nSort u} (mk : (a : List α) → motive { toArray := { toList := a }, size_eq := }) {n : Nat} (v : Batteries.Vector α n) :
        motive v

        Custom eliminator for Vector α n through List α

        Equations
        Instances For
          def Batteries.Vector.size {α : Type u_1} {n : Nat} :

          Vector.size gives the size of a vector.

          Equations
          • x.size = n
          Instances For

            Vector.empty produces an empty vector

            Equations
            • Batteries.Vector.empty = { toArray := #[], size_eq := }
            Instances For
              def Batteries.Vector.mkEmpty {α : Type u_1} (capacity : Nat) :

              Make an empty vector with pre-allocated capacity

              Equations
              Instances For
                def Batteries.Vector.mkVector {α : Type u_1} (n : Nat) (v : α) :

                Makes a vector of size n with all cells containing v

                Equations
                Instances For
                  def Batteries.Vector.singleton {α : Type u_1} (v : α) :

                  Returns a vector of size 1 with a single element v

                  Equations
                  Instances For

                    The Inhabited instance for Vector α n with [Inhabited α] produces a vector of size n with all its elements equal to the default element of type α

                    Equations
                    def Batteries.Vector.toList {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) :
                    List α

                    The list obtained from a vector.

                    Equations
                    • v.toList = v.toArray.toList
                    Instances For
                      def Batteries.Vector.get {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Fin n) :
                      α

                      nth element of a vector, indexed by a Fin type.

                      Equations
                      Instances For
                        def Batteries.Vector.uget {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : USize) (h : i.toNat < n) :
                        α

                        Vector lookup function that takes an index i of type USize

                        Equations
                        • v.uget i h = v.toArray.uget i
                        Instances For
                          instance Batteries.Vector.instGetElemNatLt {α : Type u_1} {n : Nat} :
                          GetElem (Batteries.Vector α n) Nat α fun (x : Batteries.Vector α n) (i : Nat) => i < n

                          Vector α n instance for the GetElem typeclass.

                          Equations
                          • Batteries.Vector.instGetElemNatLt = { getElem := fun (x : Batteries.Vector α n) (i : Nat) (h : i < n) => x.get i, h }
                          def Batteries.Vector.getD {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (v₀ : α) :
                          α

                          getD v i v₀ gets the iᵗʰ element of v if valid. Otherwise it returns v₀ by default

                          Equations
                          • v.getD i v₀ = v.toArray.getD i v₀
                          Instances For
                            @[reducible, inline]
                            abbrev Batteries.Vector.back! {α : Type u_1} {n : Nat} [Inhabited α] (v : Batteries.Vector α n) :
                            α

                            v.back! v gets the last element of the vector. panics if v is empty.

                            Equations
                            • v.back! = v[n - 1]!
                            Instances For
                              @[reducible, inline]
                              abbrev Batteries.Vector.back? {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) :

                              v.back? gets the last element x of the array as some x if it exists. Else the vector is empty and it returns none

                              Equations
                              • v.back? = v[n - 1]?
                              Instances For
                                @[reducible, inline]
                                abbrev Batteries.Vector.back {α : Type u_1} {n : Nat} (v : Batteries.Vector α (n + 1)) :
                                α

                                Abbreviation for the last element of a non-empty Vector.

                                Equations
                                • v.back = v[n]
                                Instances For
                                  @[reducible, inline]
                                  abbrev Batteries.Vector.head {α : Type u_1} {n : Nat} (v : Batteries.Vector α (n + 1)) :
                                  α

                                  Vector.head produces the head of a vector

                                  Equations
                                  • v.head = v[0]
                                  Instances For
                                    def Batteries.Vector.push {α : Type u_1} {n : Nat} (x : α) (v : Batteries.Vector α n) :

                                    push v x pushes x to the end of vector v in O(1) time

                                    Equations
                                    Instances For
                                      def Batteries.Vector.pop {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) :

                                      pop v returns the vector with the last element removed

                                      Equations
                                      • v.pop = { toArray := v.toArray.pop, size_eq := }
                                      Instances For
                                        def Batteries.Vector.set {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Fin n) (x : α) :

                                        Sets an element in a vector using a Fin index.

                                        This will perform the update destructively provided that a has a reference count of 1 when called.

                                        Equations
                                        • v.set i x = { toArray := v.toArray.set (Fin.cast i) x, size_eq := }
                                        Instances For
                                          def Batteries.Vector.setN {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (x : α) (h : autoParam (i < n) _auto✝) :

                                          setN v i h x sets an element in a vector using a Nat index which is provably valid. By default a proof by get_elem_tactic is provided.

                                          This will perform the update destructively provided that a has a reference count of 1 when called.

                                          Equations
                                          • v.setN i x h = v.set i, h x
                                          Instances For
                                            def Batteries.Vector.setD {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (x : α) :

                                            Sets an element in a vector, or do nothing if the index is out of bounds.

                                            This will perform the update destructively provided that a has a reference count of 1 when called.

                                            Equations
                                            • v.setD i x = { toArray := v.toArray.setD i x, size_eq := }
                                            Instances For
                                              def Batteries.Vector.set! {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (x : α) :

                                              Sets an element in an array, or panic if the index is out of bounds.

                                              This will perform the update destructively provided that a has a reference count of 1 when called.

                                              Equations
                                              • v.set! i x = { toArray := v.toArray.set! i x, size_eq := }
                                              Instances For
                                                def Batteries.Vector.append {α : Type u_1} {n : Nat} {m : Nat} :

                                                Appends a vector to another.

                                                Equations
                                                • { toArray := a₁, size_eq := size_eq }.append { toArray := a₂, size_eq := size_eq_1 } = { toArray := a₁ ++ a₂, size_eq := }
                                                Instances For
                                                  Equations
                                                  • Batteries.Vector.instHAppendHAddNat = { hAppend := Batteries.Vector.append }
                                                  def Batteries.Vector.cast {α : Type u_1} {n : Nat} {m : Nat} (h : n = m) :

                                                  Creates a vector from another with a provably equal length.

                                                  Equations
                                                  Instances For
                                                    def Batteries.Vector.extract {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (start : Nat) (stop : Nat) :
                                                    Batteries.Vector α (min stop n - start)

                                                    extract v start halt Returns the slice of v from indices start to stop (exclusive). If start is greater or equal to stop, the result is empty. If stop is greater than the size of v, the size is used instead.

                                                    Equations
                                                    • v.extract start stop = { toArray := v.toArray.extract start stop, size_eq := }
                                                    Instances For
                                                      def Batteries.Vector.map {α : Type u_1} {β : Type u_2} {n : Nat} (f : αβ) (v : Batteries.Vector α n) :

                                                      Maps a vector under a function.

                                                      Equations
                                                      Instances For
                                                        def Batteries.Vector.zipWith {α : Type u_1} {n : Nat} {β : Type u_2} {φ : Type u_3} (a : Batteries.Vector α n) (b : Batteries.Vector β n) (f : αβφ) :

                                                        Maps two vectors under a curried function of two variables.

                                                        Equations
                                                        • { toArray := a, size_eq := h₁ }.zipWith { toArray := b, size_eq := h₂ } x = { toArray := a.zipWith b x, size_eq := }
                                                        Instances For
                                                          def Batteries.Vector.ofFn {n : Nat} {α : Type u_1} (f : Fin nα) :

                                                          Returns a vector of length n from a function on Fin n.

                                                          Equations
                                                          Instances For
                                                            def Batteries.Vector.swap {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Fin n) (j : Fin n) :

                                                            Swaps two entries in a Vector.

                                                            This will perform the update destructively provided that v has a reference count of 1 when called.

                                                            Equations
                                                            • v.swap i j = { toArray := v.toArray.swap (Fin.cast i) (Fin.cast j), size_eq := }
                                                            Instances For
                                                              def Batteries.Vector.swapN {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (j : Nat) (hi : autoParam (i < n) _auto✝) (hj : autoParam (j < n) _auto✝) :

                                                              swapN v i j hi hj swaps two Nat indexed entries in a Vector α n. Uses get_elem_tactic to supply proofs hi and hj respectively that the indices i and j are in range.

                                                              This will perform the update destructively provided that v has a reference count of 1 when called.

                                                              Equations
                                                              • v.swapN i j hi hj = v.swap i, hi j, hj
                                                              Instances For
                                                                def Batteries.Vector.swap! {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (j : Nat) :

                                                                Swaps two entries in a Vector α n, or panics if either index is out of bounds.

                                                                This will perform the update destructively provided that v has a reference count of 1 when called.

                                                                Equations
                                                                • v.swap! i j = { toArray := v.toArray.swap! i j, size_eq := }
                                                                Instances For
                                                                  def Batteries.Vector.swapAt {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Fin n) (x : α) :

                                                                  Swaps the entry with index i : Fin n in the vector for a new entry. The old entry is returned with the modified vector.

                                                                  Equations
                                                                  • v.swapAt i x = ((v.toArray.swapAt (Fin.cast i) x).fst, { toArray := (v.toArray.swapAt (Fin.cast i) x).snd, size_eq := })
                                                                  Instances For
                                                                    def Batteries.Vector.swapAtN {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (x : α) (h : autoParam (i < n) _auto✝) :

                                                                    Swaps the entry with index i : Nat in the vector for a new entry x. The old entry is returned alongwith the modified vector.

                                                                    Automatically generates a proof of i < n with get_elem_tactic where feasible.

                                                                    Equations
                                                                    • v.swapAtN i x h = v.swapAt i, h x
                                                                    Instances For
                                                                      @[inline]
                                                                      def Batteries.Vector.swapAt! {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (x : α) :

                                                                      swapAt! v i x swaps out the entry at index i : Nat in the vector for x, if the index is valid. Otherwise it panics The old entry is returned with the modified vector.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For

                                                                        range n returns the vector #v[0,1,2,...,n-1].

                                                                        Equations
                                                                        Instances For
                                                                          def Batteries.Vector.shrink {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (m : Nat) :

                                                                          shrink v m shrinks the vector to the first m elements if m < n. Returns v unchanged if m ≥ n.

                                                                          Equations
                                                                          • v.shrink m = { toArray := v.toArray.shrink m, size_eq := }
                                                                          Instances For
                                                                            def Batteries.Vector.drop {α : Type u_1} {n : Nat} (i : Nat) (v : Batteries.Vector α n) :

                                                                            Drops the first (up to) i elements from a vector of length n. If m ≥ n, the return value is empty.

                                                                            Equations
                                                                            Instances For
                                                                              def Batteries.Vector.take {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (m : Nat) :

                                                                              Takes the first (up to) i elements from a vector of length n.

                                                                              Equations
                                                                              Instances For
                                                                                @[inline]
                                                                                def Batteries.Vector.isEqv {α : Type u_1} {n : Nat} (a : Batteries.Vector α n) (b : Batteries.Vector α n) (p : ααBool) :

                                                                                isEqv takes a given boolean property p. It returns true if and only if p a[i] b[i] holds true for all valid indices i.

                                                                                Equations
                                                                                • a.isEqv b p = a.toArray.isEqvAux b.toArray p 0
                                                                                Instances For
                                                                                  instance Batteries.Vector.instBEq {α : Type u_1} {n : Nat} [BEq α] :
                                                                                  Equations
                                                                                  • Batteries.Vector.instBEq = { beq := fun (a b : Batteries.Vector α n) => a.isEqv b BEq.beq }
                                                                                  def Batteries.Vector.reverse {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) :

                                                                                  reverse v reverses the vector v.

                                                                                  Equations
                                                                                  • v.reverse = { toArray := v.toArray.reverse, size_eq := }
                                                                                  Instances For
                                                                                    def Batteries.Vector.feraseIdx {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Fin n) :

                                                                                    O(|v| - i). feraseIdx v i removes the element at position i in vector v.

                                                                                    Equations
                                                                                    • v.feraseIdx i = { toArray := v.toArray.feraseIdx (Fin.cast i), size_eq := }
                                                                                    Instances For
                                                                                      @[inline]
                                                                                      def Batteries.Vector.tail {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) :

                                                                                      Vector.tail produces the tail of the vector v.

                                                                                      Equations
                                                                                      • v_2.tail = v_2
                                                                                      • v_2.tail = v_2.feraseIdx 0
                                                                                      Instances For
                                                                                        @[inline]
                                                                                        def Batteries.Vector.eraseIdx! {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) :

                                                                                        O(|v| - i). eraseIdx! v i removes the element at position i from vector v of length n. Panics if i is not less than n.

                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For
                                                                                          @[reducible, inline]
                                                                                          abbrev Batteries.Vector.eraseIdxN {α : Type u_1} {n : Nat} (v : Batteries.Vector α n) (i : Nat) (h : autoParam (i < n) _auto✝) :

                                                                                          eraseIdxN v i h removes the element at position i from a vector of length n. h : i < n has a default argument by get_elem_tactic which tries to supply a proof that the index is valid.

                                                                                          This function takes worst case O(n) time because it has to backshift all elements at positions greater than i.

                                                                                          Equations
                                                                                          • v.eraseIdxN i h = v.feraseIdx i, h
                                                                                          Instances For
                                                                                            def Batteries.Vector.indexOf? {α : Type u_1} {n : Nat} [BEq α] (v : Batteries.Vector α n) (x : α) :

                                                                                            If x is an element of vector v at index j, then indexOf? v x returns some j. Otherwise it returns none.

                                                                                            Equations
                                                                                            • v.indexOf? x = match v.toArray.indexOf? x with | some res => some (Fin.cast res) | none => none
                                                                                            Instances For
                                                                                              def Batteries.Vector.isPrefixOf {α : Type u_1} {m : Nat} {n : Nat} [BEq α] (as : Batteries.Vector α m) (bs : Batteries.Vector α n) :

                                                                                              isPrefixOf as bs returns true iff vector as is a prefix of vectorbs

                                                                                              Equations
                                                                                              • as.isPrefixOf bs = as.toArray.isPrefixOf bs.toArray
                                                                                              Instances For
                                                                                                def Batteries.Vector.allDiff {α : Type u_1} {n : Nat} [BEq α] (as : Batteries.Vector α n) :

                                                                                                allDiff as i returns true when all elements of v are distinct from each other`

                                                                                                Equations
                                                                                                • as.allDiff = as.toArray.allDiff
                                                                                                Instances For