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 → α→ fin 2 → α→ α
.
In later files we introduce !![a, b; c, d]
as notation for matrix.of ![![a, b], ![c, d]]
.
Main definitions #
vec_empty
is the empty vector (or0
byn
matrix)![]
vec_cons
prepends an entry to a vector, so![a, b]
isvec_cons a (vec_cons b vec_empty)
Implementation notes #
The simp
lemmas require that one of the arguments is of the form vec_cons _ _
.
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 vec_cons a (vec_cons b vec_empty)
.
Examples #
Examples of usage can be found in the test/matrix.lean
file.
Construct a vector Fin n → α→ α
using Matrix.vecEmpty
and Matrix.vecCons
.
Equations
- One or more equations did not get rendered due to their size.
vecHead v
gives the first entry of the vector v
Equations
- Matrix.vecHead v = v 0
![a, b, ...] 1
is equal to b
.
The simplifier needs a special lemma for length ≥ 2≥ 2
, in addition to
cons_val_succ
, because 1 : fin 1 = 0 : fin 1
.
Numeral (bit0
and bit1
) indices #
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 bit0
and bit1
and of
addition on fin n
).
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 ∘ ↑(RelIso.toRelEmbedding (Fin.cast ho)).toEmbedding