Documentation

Mathlib.Data.Fin.VecNotation

Matrix and vector notation #

This file defines notation for vectors and matrices. Given a b c d : α, the notation allows us to write ![a, b, c, d] : Fin 4 → α. Nesting vectors gives coefficients of a matrix, so ![![a, b], ![c, d]] : Fin 2 → Fin 2 → α. In later files we introduce !![a, b; c, d] as notation for Matrix.of ![![a, b], ![c, d]].

Main definitions #

Implementation notes #

The simp lemmas require that one of the arguments is of the form vecCons _ _. This ensures simp works with entries only when (some) entries are already given. In other words, this notation will only appear in the output of simp if it already appears in the input.

Notations #

The main new notation is ![a, b], which gets expanded to vecCons a (vecCons b vecEmpty).

Examples #

Examples of usage can be found in the test/matrix.lean file.

def Matrix.vecEmpty {α : Type u} :
Fin 0α

![] is the vector with no entries.

Equations
  • ![] = Fin.elim0'
Instances For
    def Matrix.vecCons {α : Type u} {n : } (h : α) (t : Fin nα) :
    Fin (Nat.succ n)α

    vecCons h t prepends an entry h to a vector t.

    The inverse functions are vecHead and vecTail. The notation ![a, b, ...] expands to vecCons a (vecCons b ...).

    Equations
    Instances For

      Construct a vector Fin n → α using Matrix.vecEmpty and Matrix.vecCons.

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

        Unexpander for the ![x, y, ...] notation.

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

          Unexpander for the ![] notation.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def Matrix.vecHead {α : Type u} {n : } (v : Fin (Nat.succ n)α) :
            α

            vecHead v gives the first entry of the vector v

            Equations
            Instances For
              def Matrix.vecTail {α : Type u} {n : } (v : Fin (Nat.succ n)α) :
              Fin nα

              vecTail v gives a vector consisting of all entries of v except the first

              Equations
              Instances For
                instance PiFin.hasRepr {α : Type u} {n : } [Repr α] :
                Repr (Fin nα)

                Use ![...] notation for displaying a vector Fin n → α, for example:

                #eval ![1, 2] + ![3, 4] -- ![4, 6]
                
                Equations
                • One or more equations did not get rendered due to their size.
                theorem Matrix.empty_eq {α : Type u} (v : Fin 0α) :
                v = ![]
                @[simp]
                theorem Matrix.head_fin_const {α : Type u} {n : } (a : α) :
                (Matrix.vecHead fun x => a) = a
                @[simp]
                theorem Matrix.cons_val_zero {α : Type u} {m : } (x : α) (u : Fin mα) :
                theorem Matrix.cons_val_zero' {α : Type u} {m : } (h : 0 < Nat.succ m) (x : α) (u : Fin mα) :
                Matrix.vecCons x u { val := 0, isLt := h } = x
                @[simp]
                theorem Matrix.cons_val_succ {α : Type u} {m : } (x : α) (u : Fin mα) (i : Fin m) :
                @[simp]
                theorem Matrix.cons_val_succ' {α : Type u} {m : } {i : } (h : Nat.succ i < Nat.succ m) (x : α) (u : Fin mα) :
                Matrix.vecCons x u { val := Nat.succ i, isLt := h } = u { val := i, isLt := (_ : i < m) }
                @[simp]
                theorem Matrix.head_cons {α : Type u} {m : } (x : α) (u : Fin mα) :
                @[simp]
                theorem Matrix.tail_cons {α : Type u} {m : } (x : α) (u : Fin mα) :
                @[simp]
                theorem Matrix.empty_val' {α : Type u} {n' : Type u_4} (j : n') :
                (fun i => ![]) = ![]
                @[simp]
                theorem Matrix.cons_head_tail {α : Type u} {m : } (u : Fin (Nat.succ m)α) :
                @[simp]
                theorem Matrix.range_cons {α : Type u} {n : } (x : α) (u : Fin nα) :
                @[simp]
                theorem Matrix.range_empty {α : Type u} (u : Fin 0α) :
                theorem Matrix.range_cons_empty {α : Type u} (x : α) (u : Fin 0α) :
                theorem Matrix.range_cons_cons_empty {α : Type u} (x : α) (y : α) (u : Fin 0α) :
                @[simp]
                theorem Matrix.vecCons_const {α : Type u} {n : } (a : α) :
                (Matrix.vecCons a fun x => a) = fun x => a
                theorem Matrix.vec_single_eq_const {α : Type u} (a : α) :
                ![a] = fun x => a
                @[simp]
                theorem Matrix.cons_val_one {α : Type u} {m : } (x : α) (u : Fin (Nat.succ m)α) :

                ![a, b, ...] 1 is equal to b.

                The simplifier needs a special lemma for length ≥ 2, in addition to cons_val_succ, because 1 : Fin 1 = 0 : Fin 1.

                @[simp]
                theorem Matrix.cons_val_two {α : Type u} {m : } (x : α) (u : Fin (Nat.succ (Nat.succ m))α) :
                @[simp]
                theorem Matrix.cons_val_fin_one {α : Type u} (x : α) (u : Fin 0α) (i : Fin 1) :
                theorem Matrix.cons_fin_one {α : Type u} (x : α) (u : Fin 0α) :
                Matrix.vecCons x u = fun x => x
                instance PiFin.toExpr {α : Type u} [Lean.ToLevel.{u}] [Lean.ToExpr α] (n : ) :
                Lean.ToExpr (Fin nα)

                bit0 and bit1 indices #

                The following definitions and simp lemmas are used to allow numeral-indexed element of a vector given with matrix notation to be extracted by simp in Lean 3 (even when the numeral is larger than the number of elements in the vector, which is taken modulo that number of elements by virtue of the semantics of bit0 and bit1 and of addition on Fin n).

                def Matrix.vecAppend {m : } {n : } {α : Type u_4} {o : } (ho : o = m + n) (u : Fin mα) (v : Fin nα) :
                Fin oα

                vecAppend ho u v appends two vectors of lengths m and n to produce one of length o = m + n. This is a variant of Fin.append with an additional ho argument, which provides control of definitional equality for the vector length.

                This turns out to be helpful when providing simp lemmas to reduce ![a, b, c] n, and also means that vecAppend ho u v 0 is valid. Fin.append u v 0 is not valid in this case because there is no Zero (Fin (m + n)) instance.

                Equations
                Instances For
                  theorem Matrix.vecAppend_eq_ite {m : } {n : } {α : Type u_4} {o : } (ho : o = m + n) (u : Fin mα) (v : Fin nα) :
                  Matrix.vecAppend ho u v = fun i => if h : i < m then u { val := i, isLt := h } else v { val := i - m, isLt := (_ : i - m < n) }
                  @[simp]
                  theorem Matrix.vecAppend_apply_zero {m : } {n : } {α : Type u_4} {o : } (ho : o + 1 = m + 1 + n) (u : Fin (m + 1)α) (v : Fin nα) :
                  Matrix.vecAppend ho u v 0 = u 0
                  @[simp]
                  theorem Matrix.empty_vecAppend {α : Type u} {n : } (v : Fin nα) :
                  Matrix.vecAppend (_ : n = 0 + n) ![] v = v
                  @[simp]
                  theorem Matrix.cons_vecAppend {α : Type u} {m : } {n : } {o : } (ho : o + 1 = m + 1 + n) (x : α) (u : Fin mα) (v : Fin nα) :
                  def Matrix.vecAlt0 {α : Type u} {m : } {n : } (hm : m = n + n) (v : Fin mα) (k : Fin n) :
                  α

                  vecAlt0 v gives a vector with half the length of v, with only alternate elements (even-numbered).

                  Equations
                  Instances For
                    def Matrix.vecAlt1 {α : Type u} {m : } {n : } (hm : m = n + n) (v : Fin mα) (k : Fin n) :
                    α

                    vecAlt1 v gives a vector with half the length of v, with only alternate elements (odd-numbered).

                    Equations
                    Instances For
                      theorem Matrix.vecAlt0_vecAppend {α : Type u} {n : } (v : Fin nα) :
                      Matrix.vecAlt0 (_ : n + n = n + n) (Matrix.vecAppend (_ : n + n = n + n) v v) = v bit0
                      theorem Matrix.vecAlt1_vecAppend {α : Type u} {n : } (v : Fin (n + 1)α) :
                      Matrix.vecAlt1 (_ : n + 1 + (n + 1) = n + 1 + (n + 1)) (Matrix.vecAppend (_ : n + 1 + (n + 1) = n + 1 + (n + 1)) v v) = v bit1
                      @[simp]
                      theorem Matrix.vecHead_vecAlt0 {α : Type u} {m : } {n : } (hm : m + 2 = n + 1 + (n + 1)) (v : Fin (m + 2)α) :
                      @[simp]
                      theorem Matrix.vecHead_vecAlt1 {α : Type u} {m : } {n : } (hm : m + 2 = n + 1 + (n + 1)) (v : Fin (m + 2)α) :
                      @[simp]
                      theorem Matrix.cons_vec_bit0_eq_alt0 {α : Type u} {n : } (x : α) (u : Fin nα) (i : Fin (n + 1)) :
                      @[simp]
                      theorem Matrix.cons_vec_bit1_eq_alt1 {α : Type u} {n : } (x : α) (u : Fin nα) (i : Fin (n + 1)) :
                      @[simp]
                      theorem Matrix.cons_vecAlt0 {α : Type u} {m : } {n : } (h : m + 1 + 1 = n + 1 + (n + 1)) (x : α) (y : α) (u : Fin mα) :
                      @[simp]
                      theorem Matrix.empty_vecAlt0 (α : Type u_4) {h : 0 = 0 + 0} :
                      Matrix.vecAlt0 h ![] = ![]
                      @[simp]
                      theorem Matrix.cons_vecAlt1 {α : Type u} {m : } {n : } (h : m + 1 + 1 = n + 1 + (n + 1)) (x : α) (y : α) (u : Fin mα) :
                      @[simp]
                      theorem Matrix.empty_vecAlt1 (α : Type u_4) {h : 0 = 0 + 0} :
                      Matrix.vecAlt1 h ![] = ![]
                      @[simp]
                      theorem Matrix.smul_empty {α : Type u} {M : Type u_4} [SMul M α] (x : M) (v : Fin 0α) :
                      x v = ![]
                      @[simp]
                      theorem Matrix.smul_cons {α : Type u} {n : } {M : Type u_4} [SMul M α] (x : M) (y : α) (v : Fin nα) :
                      @[simp]
                      theorem Matrix.empty_add_empty {α : Type u} [Add α] (v : Fin 0α) (w : Fin 0α) :
                      v + w = ![]
                      @[simp]
                      theorem Matrix.cons_add {α : Type u} {n : } [Add α] (x : α) (v : Fin nα) (w : Fin (Nat.succ n)α) :
                      @[simp]
                      theorem Matrix.add_cons {α : Type u} {n : } [Add α] (v : Fin (Nat.succ n)α) (y : α) (w : Fin nα) :
                      theorem Matrix.cons_add_cons {α : Type u} {n : } [Add α] (x : α) (v : Fin nα) (y : α) (w : Fin nα) :
                      @[simp]
                      theorem Matrix.head_add {α : Type u} {n : } [Add α] (a : Fin (Nat.succ n)α) (b : Fin (Nat.succ n)α) :
                      @[simp]
                      theorem Matrix.tail_add {α : Type u} {n : } [Add α] (a : Fin (Nat.succ n)α) (b : Fin (Nat.succ n)α) :
                      @[simp]
                      theorem Matrix.empty_sub_empty {α : Type u} [Sub α] (v : Fin 0α) (w : Fin 0α) :
                      v - w = ![]
                      @[simp]
                      theorem Matrix.cons_sub {α : Type u} {n : } [Sub α] (x : α) (v : Fin nα) (w : Fin (Nat.succ n)α) :
                      @[simp]
                      theorem Matrix.sub_cons {α : Type u} {n : } [Sub α] (v : Fin (Nat.succ n)α) (y : α) (w : Fin nα) :
                      theorem Matrix.cons_sub_cons {α : Type u} {n : } [Sub α] (x : α) (v : Fin nα) (y : α) (w : Fin nα) :
                      @[simp]
                      theorem Matrix.head_sub {α : Type u} {n : } [Sub α] (a : Fin (Nat.succ n)α) (b : Fin (Nat.succ n)α) :
                      @[simp]
                      theorem Matrix.tail_sub {α : Type u} {n : } [Sub α] (a : Fin (Nat.succ n)α) (b : Fin (Nat.succ n)α) :
                      @[simp]
                      theorem Matrix.zero_empty {α : Type u} [Zero α] :
                      0 = ![]
                      @[simp]
                      theorem Matrix.cons_zero_zero {α : Type u} {n : } [Zero α] :
                      @[simp]
                      theorem Matrix.head_zero {α : Type u} {n : } [Zero α] :
                      @[simp]
                      theorem Matrix.tail_zero {α : Type u} {n : } [Zero α] :
                      @[simp]
                      theorem Matrix.cons_eq_zero_iff {α : Type u} {n : } [Zero α] {v : Fin nα} {x : α} :
                      Matrix.vecCons x v = 0 x = 0 v = 0
                      theorem Matrix.cons_nonzero_iff {α : Type u} {n : } [Zero α] {v : Fin nα} {x : α} :
                      @[simp]
                      theorem Matrix.neg_empty {α : Type u} [Neg α] (v : Fin 0α) :
                      -v = ![]
                      @[simp]
                      theorem Matrix.neg_cons {α : Type u} {n : } [Neg α] (x : α) (v : Fin nα) :
                      @[simp]
                      theorem Matrix.head_neg {α : Type u} {n : } [Neg α] (a : Fin (Nat.succ n)α) :
                      @[simp]
                      theorem Matrix.tail_neg {α : Type u} {n : } [Neg α] (a : Fin (Nat.succ n)α) :