Documentation

Mathlib.Data.Vector.Defs

The type List.Vector represents lists with fixed length.

TODO: The API of List.Vector is quite incomplete relative to Vector, and in particular does not use x[i] (that is GetElem notation) as the preferred accessor. Any combination of reducing the use of List.Vector in Mathlib, or modernising its API, would be welcome.

def List.Vector (α : Type u) (n : ) :

List.Vector α n is the type of lists of length n with elements of type α.

Note that there is also Vector α n in the root namespace, which is the type of arrays of length n with elements of type α.

Typically, if you are doing programming or verification, you will primarily use Vector α n, and if you are doing mathematics, you may want to use List.Vector α n instead.

Equations
    Instances For
      instance List.Vector.instDecidableEq {α : Type u_1} {n : } [DecidableEq α] :
      Equations
        @[match_pattern]
        def List.Vector.nil {α : Type u_1} :
        Vector α 0

        The empty vector with elements of type α

        Equations
          Instances For
            @[match_pattern]
            def List.Vector.cons {α : Type u_1} {n : } :
            αVector α nVector α n.succ

            If a : α and l : Vector α n, then cons a l, is the vector of length n + 1 whose first element is a and with l as the rest of the list.

            Equations
              Instances For
                @[reducible]
                def List.Vector.length {α : Type u_1} {n : } :
                Vector α n

                The length of a vector.

                Equations
                  Instances For
                    def List.Vector.head {α : Type u_1} {n : } :
                    Vector α n.succα

                    The first element of a vector with length at least 1.

                    Equations
                      Instances For
                        theorem List.Vector.head_cons {α : Type u_1} {n : } (a : α) (v : Vector α n) :
                        (cons a v).head = a

                        The head of a vector obtained by prepending is the element prepended.

                        def List.Vector.tail {α : Type u_1} {n : } :
                        Vector α nVector α (n - 1)

                        The tail of a vector, with an empty vector having empty tail.

                        Equations
                          Instances For
                            theorem List.Vector.tail_cons {α : Type u_1} {n : } (a : α) (v : Vector α n) :
                            (cons a v).tail = v

                            The tail of a vector obtained by prepending is the vector prepended. to

                            @[simp]
                            theorem List.Vector.cons_head_tail {α : Type u_1} {n : } (v : Vector α n.succ) :
                            cons v.head v.tail = v

                            Prepending the head of a vector to its tail gives the vector.

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

                            The list obtained from a vector.

                            Equations
                              Instances For
                                def List.Vector.get {α : Type u_1} {n : } (l : Vector α n) (i : Fin n) :
                                α

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

                                Equations
                                  Instances For
                                    def List.Vector.append {α : Type u_1} {n m : } :
                                    Vector α nVector α mVector α (n + m)

                                    Appending a vector to another.

                                    Equations
                                      Instances For
                                        def List.Vector.elim {α : Type u_5} {C : {n : } → Vector α nSort u} (H : (l : List α) → C l, ) {n : } (v : Vector α n) :
                                        C v

                                        Elimination rule for Vector.

                                        Equations
                                          Instances For
                                            def List.Vector.map {α : Type u_1} {β : Type u_2} {n : } (f : αβ) :
                                            Vector α nVector β n

                                            Map a vector under a function.

                                            Equations
                                              Instances For
                                                @[simp]
                                                theorem List.Vector.map_nil {α : Type u_1} {β : Type u_2} (f : αβ) :

                                                A nil vector maps to a nil vector.

                                                @[simp]
                                                theorem List.Vector.map_cons {α : Type u_1} {β : Type u_2} {n : } (f : αβ) (a : α) (v : Vector α n) :
                                                map f (cons a v) = cons (f a) (map f v)

                                                map is natural with respect to cons.

                                                def List.Vector.pmap {α : Type u_1} {β : Type u_2} {n : } {p : αProp} (f : (a : α) → p aβ) (v : Vector α n) :
                                                (∀ (x : α), x v.toListp x)Vector β n

                                                Map a vector under a partial function.

                                                Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem List.Vector.pmap_nil {α : Type u_1} {β : Type u_2} {p : αProp} (f : (a : α) → p aβ) (hp : ∀ (x : α), x nil.toListp x) :
                                                    pmap f nil hp = nil
                                                    def List.Vector.map₂ {α : Type u_1} {β : Type u_2} {φ : Type u_4} {n : } (f : αβφ) :
                                                    Vector α nVector β nVector φ n

                                                    Mapping two vectors under a curried function of two variables.

                                                    Equations
                                                      Instances For
                                                        def List.Vector.replicate {α : Type u_1} (n : ) (a : α) :
                                                        Vector α n

                                                        Vector obtained by repeating an element.

                                                        Equations
                                                          Instances For
                                                            def List.Vector.drop {α : Type u_1} {n : } (i : ) :
                                                            Vector α nVector α (n - i)

                                                            Drop i elements from a vector of length n; we can have i > n.

                                                            Equations
                                                              Instances For
                                                                def List.Vector.take {α : Type u_1} {n : } (i : ) :
                                                                Vector α nVector α (min i n)

                                                                Take i elements from a vector of length n; we can have i > n.

                                                                Equations
                                                                  Instances For
                                                                    def List.Vector.eraseIdx {α : Type u_1} {n : } (i : Fin n) :
                                                                    Vector α nVector α (n - 1)

                                                                    Remove the element at position i from a vector of length n.

                                                                    Equations
                                                                      Instances For
                                                                        def List.Vector.ofFn {α : Type u_1} {n : } :
                                                                        (Fin nα)Vector α n

                                                                        Vector of length n from a function on Fin n.

                                                                        Equations
                                                                          Instances For
                                                                            def List.Vector.congr {α : Type u_1} {n m : } (h : n = m) :
                                                                            Vector α nVector α m

                                                                            Create a vector from another with a provably equal length.

                                                                            Equations
                                                                              Instances For
                                                                                def List.Vector.mapAccumr {α : Type u_1} {β : Type u_2} {σ : Type u_3} {n : } (f : ασσ × β) :
                                                                                Vector α nσσ × Vector β n

                                                                                Runs a function over a vector returning the intermediate results and a final result.

                                                                                Equations
                                                                                  Instances For
                                                                                    def List.Vector.mapAccumr₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} {φ : Type u_4} {n : } (f : αβσσ × φ) :
                                                                                    Vector α nVector β nσσ × Vector φ n

                                                                                    Runs a function over a pair of vectors returning the intermediate results and a final result.

                                                                                    Equations
                                                                                      Instances For

                                                                                        Shift Primitives #

                                                                                        def List.Vector.shiftLeftFill {α : Type u_1} {n : } (v : Vector α n) (i : ) (fill : α) :
                                                                                        Vector α n

                                                                                        shiftLeftFill v i is the vector obtained by left-shifting v i times and padding with the fill argument. If v.length < i then this will return replicate n fill.

                                                                                        Equations
                                                                                          Instances For
                                                                                            def List.Vector.shiftRightFill {α : Type u_1} {n : } (v : Vector α n) (i : ) (fill : α) :
                                                                                            Vector α n

                                                                                            shiftRightFill v i is the vector obtained by right-shifting v i times and padding with the fill argument. If v.length < i then this will return replicate n fill.

                                                                                            Equations
                                                                                              Instances For

                                                                                                Basic Theorems #

                                                                                                theorem List.Vector.eq {α : Type u_1} {n : } (a1 a2 : Vector α n) :
                                                                                                a1.toList = a2.toLista1 = a2

                                                                                                Vector is determined by the underlying list.

                                                                                                theorem List.Vector.eq_nil {α : Type u_1} (v : Vector α 0) :
                                                                                                v = nil

                                                                                                A vector of length 0 is a nil vector.

                                                                                                @[simp]
                                                                                                theorem List.Vector.toList_mk {α : Type u_1} {n : } (v : List α) (P : v.length = n) :

                                                                                                Vector of length from a list v with witness that v has length n maps to v under toList.

                                                                                                @[simp]

                                                                                                A nil vector maps to a nil list.

                                                                                                @[simp]
                                                                                                theorem List.Vector.toList_length {α : Type u_1} {n : } (v : Vector α n) :

                                                                                                The length of the list to which a vector of length n maps is n.

                                                                                                @[simp]
                                                                                                theorem List.Vector.toList_cons {α : Type u_1} {n : } (a : α) (v : Vector α n) :
                                                                                                (cons a v).toList = a :: v.toList

                                                                                                toList of cons of a vector and an element is the cons of the list obtained by toList and the element

                                                                                                @[simp]
                                                                                                theorem List.Vector.toList_append {α : Type u_1} {n m : } (v : Vector α n) (w : Vector α m) :

                                                                                                Appending of vectors corresponds under toList to appending of lists.

                                                                                                @[simp]
                                                                                                theorem List.Vector.toList_drop {α : Type u_1} {n m : } (v : Vector α m) :

                                                                                                drop of vectors corresponds under toList to drop of lists.

                                                                                                @[simp]
                                                                                                theorem List.Vector.toList_take {α : Type u_1} {n m : } (v : Vector α m) :

                                                                                                take of vectors corresponds under toList to take of lists.

                                                                                                instance List.Vector.instGetElemNatLt {α : Type u_1} {n : } :
                                                                                                GetElem (Vector α n) α fun (x : Vector α n) (i : ) => i < n
                                                                                                Equations
                                                                                                  theorem List.Vector.getElem_def {α : Type u_1} {n : } (v : Vector α n) (i : ) {hi : i < n} :
                                                                                                  theorem List.Vector.toList_getElem {α : Type u_1} {n : } (v : Vector α n) (i : ) {hi : i < v.toList.length} :