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