Matrix and vector notation #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
vec_emptyis the empty vector (or
vec_consprepends an entry to a vector, so
vec_cons a (vec_cons b vec_empty)
Implementation notes #
simp lemmas require that one of the arguments is of the form
vec_cons _ _.
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.
The main new notation is
![a, b], which gets expanded to
vec_cons a (vec_cons b vec_empty).
Examples of usage can be found in the
![...] notation for displaying a vector
fin n → α, for example:
#eval ![1, 2] + ![3, 4] -- ![4, 6]
The following definitions and
simp lemmas are to allow any
numeral-indexed element of a vector given with matrix notation to
be extracted by
simp (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
bit1 and of
vec_append ho u v appends two vectors of lengths
n to produce
one of length
o = m + n. This is a variant of
fin.append with an additional
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
vec_append ho u v 0 is valid.
fin.append u v 0 is not valid in this case because there is
has_zero (fin (m + n)) instance.