# 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 #

- `vecEmpty` is the empty vector (or `0` by `n` matrix) `![]`
- `vecCons` prepends an entry to a vector, so `![a, b]` is `vecCons a (vecCons b vecEmpty)`

## 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.

## Notation #

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 `MathlibTest/matrix.lean` file.

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

`![]` is the vector with no entries.

Equations

- ![] = Fin.elim0

Instances For

source
def Matrix.vecCons {α : Type u} {n : ℕ} (h : α) (t : Fin n → α) :
Fin n.succ → α

`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

- Matrix.vecCons h t = Fin.cons h t

Instances For

source
def Matrix.vecNotation :
Lean.ParserDescr

`![...]` notation is used to construct a vector `Fin n → α` using `Matrix.vecEmpty` and `Matrix.vecCons`.

For instance, `![a, b, c] : Fin 3` is syntax for `vecCons a (vecCons b (vecCons c vecEmpty))`.

Note that this should not be used as syntax for `Matrix` as it generates a term with the wrong type. The `!![a, b; c, d]` syntax (provided by `Matrix.matrixNotation`) should be used instead.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Matrix.vecConsUnexpander :
Lean.PrettyPrinter.Unexpander

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Matrix.vecEmptyUnexpander :
Lean.PrettyPrinter.Unexpander

Unexpander for the `![]` notation.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Matrix.vecHead {α : Type u} {n : ℕ} (v : Fin n.succ → α) :
α

`vecHead v` gives the first entry of the vector `v`

Equations

- Matrix.vecHead v = v 0

Instances For

source
def Matrix.vecTail {α : Type u} {n : ℕ} (v : Fin n.succ → α) :
Fin n → α

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

Equations

- Matrix.vecTail v = v ∘ Fin.succ

Instances For

source
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.

source
theorem Matrix.empty_eq {α : Type u} (v : Fin 0 → α) :
v = ![]
source
@[simp]
theorem Matrix.head_fin_const {α : Type u} {n : ℕ} (a : α) :
(vecHead fun (x : Fin (n + 1)) => a) = a
source
@[simp]
theorem Matrix.cons_val_zero {α : Type u} {m : ℕ} (x : α) (u : Fin m → α) :
vecCons x u 0 = x
source
theorem Matrix.cons_val_zero' {α : Type u} {m : ℕ} (h : 0 < m.succ) (x : α) (u : Fin m → α) :
vecCons x u ⟨0, h⟩ = x
source
@[simp]
theorem Matrix.cons_val_succ {α : Type u} {m : ℕ} (x : α) (u : Fin m → α) (i : Fin m) :
vecCons x u i.succ = u i
source
@[simp]
theorem Matrix.cons_val_succ' {α : Type u} {m i : ℕ} (h : i.succ < m.succ) (x : α) (u : Fin m → α) :
vecCons x u ⟨i.succ, h⟩ = u ⟨i, ⋯⟩
source
partial def Matrix.matchVecConsPrefix (n : Q(ℕ)) (e : Lean.Expr) :
Lean.MetaM (List Lean.Expr × Q(ℕ) × Lean.Expr)

Parses a chain of `Matrix.vecCons` calls into elements, leaving everything else in the tail.

`let ⟨xs, tailn, tail⟩ ← matchVecConsPrefix n e` decomposes `e : Fin n → _` in the form `vecCons x₀ <| ... <| vecCons xₙ <| tail` where `tail : Fin tailn → _`.

source
def Matrix.cons_val :
Lean.Meta.Simp.DSimproc

A simproc that handles terms of the form `Matrix.vecCons a f i` where `i` is a numeric literal.

In practice, this is most effective at handling `![a, b, c] i`-style terms.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Matrix.head_cons {α : Type u} {m : ℕ} (x : α) (u : Fin m → α) :
vecHead (vecCons x u) = x
source
@[simp]
theorem Matrix.tail_cons {α : Type u} {m : ℕ} (x : α) (u : Fin m → α) :
vecTail (vecCons x u) = u
source
theorem Matrix.empty_val' {α : Type u} {n' : Type u_1} (j : n') :
(fun (i : Fin 0) => ![] i j) = ![]
source
@[simp]
theorem Matrix.cons_head_tail {α : Type u} {m : ℕ} (u : Fin m.succ → α) :
vecCons (vecHead u) (vecTail u) = u
source
@[simp]
theorem Matrix.range_cons {α : Type u} {n : ℕ} (x : α) (u : Fin n → α) :
Set.range (vecCons x u) = {x} ∪ Set.range u
source
@[simp]
theorem Matrix.range_empty {α : Type u} (u : Fin 0 → α) :
Set.range u = ∅
source
theorem Matrix.range_cons_empty {α : Type u} (x : α) (u : Fin 0 → α) :
Set.range (vecCons x u) = {x}
source
theorem Matrix.range_cons_cons_empty {α : Type u} (x y : α) (u : Fin 0 → α) :
Set.range (vecCons x (vecCons y u)) = {x, y}
source
theorem Matrix.vecCons_const {α : Type u} {n : ℕ} (a : α) :
(vecCons a fun (x : Fin n) => a) = fun (x : Fin n.succ) => a
source
theorem Matrix.vec_single_eq_const {α : Type u} (a : α) :
![a] = fun (x : Fin (Nat.succ 0)) => a
source
@[simp]
theorem Matrix.cons_val_one {α : Type u} {m : ℕ} (x : α) (u : Fin m.succ → α) :
vecCons x u 1 = u 0

`![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`.

source
theorem Matrix.cons_val_two {α : Type u} {m : ℕ} (x : α) (u : Fin m.succ.succ → α) :
vecCons x u 2 = vecHead (vecTail u)
source
theorem Matrix.cons_val_three {α : Type u} {m : ℕ} (x : α) (u : Fin m.succ.succ.succ → α) :
vecCons x u 3 = vecHead (vecTail (vecTail u))
source
theorem Matrix.cons_val_four {α : Type u} {m : ℕ} (x : α) (u : Fin m.succ.succ.succ.succ → α) :
vecCons x u 4 = vecHead (vecTail (vecTail (vecTail u)))
source
@[simp]
theorem Matrix.cons_val_fin_one {α : Type u} (x : α) (u : Fin 0 → α) (i : Fin 1) :
vecCons x u i = x
source
theorem Matrix.cons_fin_one {α : Type u} (x : α) (u : Fin 0 → α) :
vecCons x u = fun (x_1 : Fin (Nat.succ 0)) => x
source
@[simp]
theorem Matrix.vecCons_inj {α : Type u} {n : ℕ} {x y : α} {u v : Fin n → α} :
vecCons x u = vecCons y v ↔ x = y ∧ u = v
source
def PiFin.mkLiteralQ {u : Lean.Level} {α : Q(Type u)} {n : ℕ} (elems : Fin n → Q(«$α»)) :
Q(Fin «$n» → «$α»)

`mkVecLiteralQ ![x, y, z]` produces the term `q(![$x, $y, $z])`.

Equations

- PiFin.mkLiteralQ elems = PiFin.mkLiteralQ.loop elems 0 q(![])

Instances For

source
@[irreducible]
def PiFin.mkLiteralQ.loop {u : Lean.Level} {α : Q(Type u)} {n : ℕ} (elems : Fin n → Q(«$α»)) (i : ℕ) (rest : Q(Fin «$i» → «$α»)) :
Q(Fin «$n» → «$α»)

The core logic of `loop` is that `loop 0 ![] = ![a 0, a 1, a 2] = loop 1 ![a 2]`, where recursion starts from the end. In this example, on the right-hand side, the variable `rest := 1` tracks the length of the current generated notation `![a 2]`, and the last used index is `n - rest` (`= 3 - 1 = 2`).

Equations

- PiFin.mkLiteralQ.loop elems i rest = if h : i < n then PiFin.mkLiteralQ.loop elems (i + 1) (have a := elems ⟨i, h⟩.rev; q(Matrix.vecCons «$a» «$rest»)) else rest

Instances For

source
instance PiFin.toExpr {α : Type u} [Lean.ToLevel] [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`).

source
def Matrix.vecAppend {m n : ℕ} {α : Type u_1} {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

- Matrix.vecAppend ho u v = Fin.append u v ∘ Fin.cast ho

Instances For

source
theorem Matrix.vecAppend_eq_ite {m n : ℕ} {α : Type u_1} {o : ℕ} (ho : o = m + n) (u : Fin m → α) (v : Fin n → α) :
vecAppend ho u v = fun (i : Fin o) => if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩
source
@[simp]
theorem Matrix.vecAppend_apply_zero {m n : ℕ} {α : Type u_1} {o : ℕ} (ho : o + 1 = m + 1 + n) (u : Fin (m + 1) → α) (v : Fin n → α) :
vecAppend ho u v 0 = u 0
source
@[simp]
theorem Matrix.empty_vecAppend {α : Type u} {n : ℕ} (v : Fin n → α) :
vecAppend ⋯ ![] v = v
source
@[simp]
theorem Matrix.vecAppend_empty {α : Type u} {n : ℕ} (v : Fin n → α) :
vecAppend ⋯ v ![] = v
source
@[simp]
theorem Matrix.cons_vecAppend {α : Type u} {m n o : ℕ} (ho : o + 1 = m + 1 + n) (x : α) (u : Fin m → α) (v : Fin n → α) :
vecAppend ho (vecCons x u) v = vecCons x (vecAppend ⋯ u v)
source
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

- Matrix.vecAlt0 hm v k = v ⟨↑k + ↑k, ⋯⟩

Instances For

source
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

- Matrix.vecAlt1 hm v k = v ⟨↑k + ↑k + 1, ⋯⟩

Instances For

source
theorem Matrix.vecAlt0_vecAppend {α : Type u} {n : ℕ} (v : Fin n → α) :
vecAlt0 ⋯ (vecAppend ⋯ v v) = v ∘ fun (n_1 : Fin n) => n_1 + n_1
source
theorem Matrix.vecAlt1_vecAppend {α : Type u} {n : ℕ} (v : Fin (n + 1) → α) :
vecAlt1 ⋯ (vecAppend ⋯ v v) = v ∘ fun (n_1 : Fin (n + 1)) => n_1 + n_1 + 1
source
@[simp]
theorem Matrix.vecHead_vecAlt0 {α : Type u} {m n : ℕ} (hm : m + 2 = n + 1 + (n + 1)) (v : Fin (m + 2) → α) :
vecHead (vecAlt0 hm v) = v 0
source
@[simp]
theorem Matrix.vecHead_vecAlt1 {α : Type u} {m n : ℕ} (hm : m + 2 = n + 1 + (n + 1)) (v : Fin (m + 2) → α) :
vecHead (vecAlt1 hm v) = v 1
source
theorem Matrix.cons_vec_bit0_eq_alt0 {α : Type u} {n : ℕ} (x : α) (u : Fin n → α) (i : Fin (n + 1)) :
vecCons x u (i + i) = vecAlt0 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i
source
theorem Matrix.cons_vec_bit1_eq_alt1 {α : Type u} {n : ℕ} (x : α) (u : Fin n → α) (i : Fin (n + 1)) :
vecCons x u (i + i + 1) = vecAlt1 ⋯ (vecAppend ⋯ (vecCons x u) (vecCons x u)) i
source
@[simp]
theorem Matrix.cons_vecAlt0 {α : Type u} {m n : ℕ} (h : m + 1 + 1 = n + 1 + (n + 1)) (x y : α) (u : Fin m → α) :
vecAlt0 h (vecCons x (vecCons y u)) = vecCons x (vecAlt0 ⋯ u)
source
@[simp]
theorem Matrix.empty_vecAlt0 (α : Type u_1) {h : 0 = 0 + 0} :
vecAlt0 h ![] = ![]
source
@[simp]
theorem Matrix.cons_vecAlt1 {α : Type u} {m n : ℕ} (h : m + 1 + 1 = n + 1 + (n + 1)) (x y : α) (u : Fin m → α) :
vecAlt1 h (vecCons x (vecCons y u)) = vecCons y (vecAlt1 ⋯ u)
source
@[simp]
theorem Matrix.empty_vecAlt1 (α : Type u_1) {h : 0 = 0 + 0} :
vecAlt1 h ![] = ![]
source
theorem Matrix.const_fin1_eq {α : Type u} (x : α) :
(fun (x_1 : Fin 1) => x) = ![x]