Mathlib.Data.Fin.VecNotation

Matrix.vecEmpty definition

: Fin 0 → α

Full source

/-- `![]` is the vector with no entries. -/
def vecEmpty : Fin 0 → α :=
  Fin.elim0

Empty vector

Informal description

The empty vector `![]` is the function from the canonical type with 0 elements to any type $\alpha$, which has no entries since the domain is empty.

Matrix.vecCons definition

{n : ℕ} (h : α) (t : Fin n → α) : Fin n.succ → α

Full source

/-- `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 ...)`.
-/
def vecCons {n : ℕ} (h : α) (t : Fin n → α) : Fin n.succ → α :=
  Fin.cons h t

Vector cons operation

Informal description

Given a natural number `n`, an element `h` of type `α`, and a vector `t : Fin n → α`, the function `vecCons` constructs a new vector of length `n + 1` by prepending `h` to `t`. Specifically, the resulting vector is defined as `Fin.cons h t`, which maps `0` to `h` and `i.succ` to `t i` for `i : Fin n`.

Matrix.vecNotation definition

: Lean.ParserDescr✝

Full source

/-- `![...]` 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.
-/
syntax (name := vecNotation) "![" term,* "]" : term

Vector notation `![...]`

Informal description

The notation `![a₁, a₂, ..., aₙ]` constructs a vector (a function `Fin n → α`) by successively prepending elements to an empty vector using `vecCons`. For example, `![a, b, c]` represents the vector `vecCons a (vecCons b (vecCons c vecEmpty))` of type `Fin 3 → α`.

Matrix.vecConsUnexpander definition

: Lean.PrettyPrinter.Unexpander

Full source

/-- Unexpander for the `![x, y, ...]` notation. -/
@[app_unexpander vecCons]
def vecConsUnexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $term ![$term2, $terms,*]) => `(![$term, $term2, $terms,*])
  | `($_ $term ![$term2]) => `(![$term, $term2])
  | `($_ $term ![]) => `(![$term])
  | _ => throw ()

Vector notation unexpander

Informal description

The unexpander for the vector notation `![x, y, ...]` transforms expressions like `vecCons x ![y, ...]` back into the more readable vector notation `![x, y, ...]`. This ensures that the output of pretty-printing maintains the concise and familiar vector notation.

Matrix.vecEmptyUnexpander definition

: Lean.PrettyPrinter.Unexpander

Full source

/-- Unexpander for the `![]` notation. -/
@[app_unexpander vecEmpty]
def vecEmptyUnexpander : Lean.PrettyPrinter.Unexpander
  | `($_:ident) => `(![])
  | _ => throw ()

Empty vector notation unexpander

Informal description

The unexpander for the empty vector notation `![]`, which is used to represent the empty vector (or a $0 \times n$ matrix) in the matrix notation system.

Matrix.vecHead definition

{n : ℕ} (v : Fin n.succ → α) : α

Full source

/-- `vecHead v` gives the first entry of the vector `v` -/
def vecHead {n : ℕ} (v : Fin n.succ → α) : α :=
  v 0

First entry of a vector

Informal description

For a vector $ v $ of length $ n+1 $ (represented as a function $ v : \text{Fin}(n+1) \to \alpha $), the function returns the first entry $ v(0) $.

Matrix.vecTail definition

{n : ℕ} (v : Fin n.succ → α) : Fin n → α

Full source

/-- `vecTail v` gives a vector consisting of all entries of `v` except the first -/
def vecTail {n : ℕ} (v : Fin n.succ → α) : Fin n → α :=
  v ∘ Fin.succ

Tail of a vector

Informal description

For a vector $ v $ of length $ n+1 $ (represented as a function $ \text{Fin } (n+1) \to \alpha $), the function `vecTail` returns the vector consisting of all entries of $ v $ except the first, i.e., the vector $ (v_1, v_2, \ldots, v_n) $ where $ v = (v_0, v_1, \ldots, v_n) $.

PiFin.hasRepr instance

[Repr α] : Repr (Fin n → α)

Full source

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

```
#eval ![1, 2] + ![3, 4] -- ![4, 6]
```
-/
instance _root_.PiFin.hasRepr [Repr α] : Repr (Fin n → α) where
  reprPrec f _ :=
    Std.Format.bracket "![" (Std.Format.joinSep
      ((List.finRange n).map fun n => repr (f n)) ("," ++ Std.Format.line)) "]"

String Representation of Vectors

Informal description

For any type $\alpha$ with a string representation (via `Repr`), the type of vectors `Fin n → α` (functions from `Fin n` to $\alpha$) also has a string representation. This allows vectors to be displayed using the notation `![a₁, a₂, ..., aₙ]` where `a₁, a₂, ..., aₙ` are elements of $\alpha$.

Matrix.empty_eq theorem

(v : Fin 0 → α) : v = ![]

Full source

theorem empty_eq (v : Fin 0 → α) : v = ![] :=
  Subsingleton.elim _ _

Empty Vector Equality: $v = ![]$ for all zero-length vectors

Informal description

For any vector $v$ of length 0 (i.e., a function from $\text{Fin } 0$ to a type $\alpha$), $v$ is equal to the empty vector notation `![]`.

Matrix.head_fin_const theorem

(a : α) : (vecHead fun _ : Fin (n + 1) => a) = a

Full source

@[simp]
theorem head_fin_const (a : α) : (vecHead fun _ : Fin (n + 1) => a) = a :=
  rfl

First Entry of Constant Vector

Informal description

For any element $a$ of type $\alpha$ and any natural number $n$, the first entry of the constant vector of length $n+1$ with all entries equal to $a$ is $a$ itself.

Matrix.cons_val_zero theorem

(x : α) (u : Fin m → α) : vecCons x u 0 = x

Full source

@[simp]
theorem cons_val_zero (x : α) (u : Fin m → α) : vecCons x u 0 = x :=
  rfl

First Entry of Prepended Vector

Informal description

For any element $x$ of type $\alpha$ and any vector $u : \text{Fin } m \to \alpha$, the first entry (index $0$) of the vector obtained by prepending $x$ to $u$ is equal to $x$, i.e., $\text{vecCons } x\ u\ 0 = x$.

Matrix.cons_val_zero' theorem

(h : 0 < m.succ) (x : α) (u : Fin m → α) : vecCons x u ⟨0, h⟩ = x

Full source

theorem cons_val_zero' (h : 0 < m.succ) (x : α) (u : Fin m → α) : vecCons x u ⟨0, h⟩ = x :=
  rfl

First Entry of Prepended Vector

Informal description

For any natural number $m$, any element $x$ of type $\alpha$, and any vector $u : \text{Fin } m \to \alpha$, the first entry of the vector constructed by prepending $x$ to $u$ is equal to $x$. More precisely, if $h$ is a proof that $0 < m+1$, then $\text{vecCons } x\ u\ \langle 0, h \rangle = x$.

Matrix.cons_val_succ theorem

(x : α) (u : Fin m → α) (i : Fin m) : vecCons x u i.succ = u i

Full source

@[simp]
theorem cons_val_succ (x : α) (u : Fin m → α) (i : Fin m) : vecCons x u i.succ = u i := by
  simp [vecCons]

Successor Index Property of Prepended Vector

Informal description

For any element $x$ of type $\alpha$, any vector $u : \text{Fin } m \to \alpha$, and any index $i : \text{Fin } m$, the value of the vector $\text{vecCons } x\ u$ at the successor index $i.\text{succ}$ is equal to $u(i)$.

Matrix.cons_val_succ' theorem

 {i : ℕ} (h : i.succ < m.succ) (x : α) (u : Fin m → α) : vecCons x u ⟨i.succ, h⟩ = u ⟨i, Nat.lt_of_succ_lt_succ h⟩

Full source

@[simp]
theorem cons_val_succ' {i : ℕ} (h : i.succ < m.succ) (x : α) (u : Fin m → α) :
    vecCons x u ⟨i.succ, h⟩ = u ⟨i, Nat.lt_of_succ_lt_succ h⟩ := by
  simp only [vecCons, Fin.cons, Fin.cases_succ']

Successor index property of prepended vector (general form)

Informal description

For any natural number $i$ and proof $h$ that $i+1 < m+1$, given an element $x$ of type $\alpha$ and a vector $u : \text{Fin } m \to \alpha$, the value of the vector $\text{vecCons } x\ u$ at the index $\langle i+1, h \rangle$ is equal to $u$ evaluated at the index $\langle i, \text{Nat.lt\_of\_succ\_lt\_succ } h \rangle$.

Matrix.matchVecConsPrefix definition

(n : Q(Nat)) (e : Expr) : MetaM <| List Expr × Q(Nat) × Expr

Full source

/-- 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 → _`. -/
partial def matchVecConsPrefix (n : Q(Nat)) (e : Expr) : MetaM <| ListList Expr × Q(Nat) × Expr := do
  match_expr ← Meta.whnfR e with
  | Matrix.vecCons _ n x xs => do
    let (elems, n', tail) ← matchVecConsPrefix n xs
    return (x :: elems, n', tail)
  | _ =>
    return ([], n, e)

Decomposition of vector constructor chains

Informal description

The function `Matrix.matchVecConsPrefix` takes a natural number `n` and an expression `e` representing a vector (a function `Fin n → α`), and decomposes `e` into a list of elements constructed via `Matrix.vecCons` calls, leaving any remaining part of the vector in a tail expression. Specifically, if `e` is of the form `vecCons x₀ (vecCons x₁ (... (vecCons xₖ tail)))`, then the function returns the list `[x₀, x₁, ..., xₖ]`, the size `n'` of the remaining tail (if any), and the tail expression itself. If `e` does not start with `vecCons`, it returns an empty list, the original `n`, and `e` unchanged.

Matrix.cons_val definition

: Lean.Meta.Simp.DSimproc

Full source

/-- 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. -/
dsimproc cons_val (Matrix.vecCons _ _ _) := fun e => do
  let_expr Matrix.vecCons α en x xs' ei := ← Meta.whnfR e | return .continue
  let somesome i := ei.int? | return .continue
  let (xs, etailn, tail) ← matchVecConsPrefix en xs'
  let xs := x :: xs
  -- Determine if the tail is a numeral or only an offset.
  let (tailn, variadic, etailn) ← do
    let etailn_whnf : Q(ℕ) ← Meta.whnfD etailn
    if let Expr.lit (.natVal length) := etailn_whnf then
      pure (length, false, q(OfNat.ofNat $etailn_whnf))
    else if let .some ((base : Q(ℕ)), offset) ← (Meta.isOffset? etailn_whnf).run then
      let offset_e : Q(ℕ) := mkNatLit offset
      pure (offset, true, q($base + $offset))
    else
      pure (0, true, etailn)
  -- Wrap the index if possible, and abort if not
  let wrapped_i ←
    if variadic then
      -- can't wrap as we don't know the length
      unless 0 ≤ i ∧ i < xs.length + tailn do return .continue
      pure i.toNat
    else
      pure (i % (xs.length + tailn)).toNat
  if h : wrapped_i < xs.length then
    return .continue xs[wrapped_i]
  else
    -- Within the `tail`
    let _ ← synthInstanceQ q(NeZero $etailn)
    have i_lit : Q(ℕ) := mkRawNatLit (wrapped_i - xs.length)
    return .continue (.some <| .app tail q(OfNat.ofNat $i_lit : Fin $etailn))

Simplification procedure for vector element access

Informal description

A simplification procedure that handles terms of the form `Matrix.vecCons a f i` where `i` is a numeric literal. Specifically, it simplifies expressions like `![a, b, c] i` by extracting the `i`-th element from the vector constructed via `vecCons` calls. The procedure works by decomposing the vector into its constituent elements and then selecting the appropriate element based on the index `i`, wrapping around if necessary when the index exceeds the vector length.

Matrix.head_cons theorem

(x : α) (u : Fin m → α) : vecHead (vecCons x u) = x

Full source

@[simp]
theorem head_cons (x : α) (u : Fin m → α) : vecHead (vecCons x u) = x :=
  rfl

Head of Cons Vector Equals Prepended Element

Informal description

For any element $x$ of type $\alpha$ and any vector $u : \text{Fin}(m) \to \alpha$, the head of the vector constructed by prepending $x$ to $u$ is equal to $x$, i.e., $\text{vecHead}(\text{vecCons}(x, u)) = x$.

Matrix.tail_cons theorem

(x : α) (u : Fin m → α) : vecTail (vecCons x u) = u

Full source

@[simp]
theorem tail_cons (x : α) (u : Fin m → α) : vecTail (vecCons x u) = u := by
  ext
  simp [vecTail]

Tail of Prepended Vector Equals Original Vector

Informal description

For any element $x$ of type $\alpha$ and any vector $u : \text{Fin}(m) \to \alpha$, the tail of the vector constructed by prepending $x$ to $u$ is equal to $u$, i.e., $\text{vecTail}(\text{vecCons}(x, u)) = u$.

Matrix.empty_val' theorem

{n' : Type*} (j : n') : (fun i => (![] : Fin 0 → n' → α) i j) = ![]

Full source

theorem empty_val' {n' : Type*} (j : n') : (fun i => (![] : Fin 0 → n' → α) i j) = ![] :=
  empty_eq _

Empty Vector Evaluation: $f(i) = ![]$ for all $i$ in empty domain

Informal description

For any type `n'` and any element `j : n'`, the function `i ↦ (![] : Fin 0 → n' → α) i j` is equal to the empty vector `![]`.

Matrix.cons_head_tail theorem

(u : Fin m.succ → α) : vecCons (vecHead u) (vecTail u) = u

Full source

@[simp]
theorem cons_head_tail (u : Fin m.succ → α) : vecCons (vecHead u) (vecTail u) = u :=
  Fin.cons_self_tail _

Reconstruction of Vector from Head and Tail

Informal description

For any vector $u$ of length $m+1$ (represented as a function $u : \text{Fin}(m+1) \to \alpha$), prepending the first element $\text{vecHead}(u)$ to the tail of $u$ (obtained via $\text{vecTail}(u)$) reconstructs the original vector $u$. In other words, $\text{vecCons}(\text{vecHead}(u), \text{vecTail}(u)) = u$.

Matrix.range_cons theorem

(x : α) (u : Fin n → α) : Set.range (vecCons x u) = { x } ∪ Set.range u

Full source

@[simp]
theorem range_cons (x : α) (u : Fin n → α) : Set.range (vecCons x u) = {x}{x} ∪ Set.range u :=
  Set.ext fun y => by simp [Fin.exists_fin_succ, eq_comm]

Range of Prepended Vector is Union of Singleton and Original Range

Informal description

For any element $x$ of type $\alpha$ and any vector $u : \text{Fin } n \to \alpha$, the range of the vector $\text{vecCons } x\ u$ is equal to the union of the singleton set $\{x\}$ and the range of $u$.

Matrix.range_empty theorem

(u : Fin 0 → α) : Set.range u = ∅

Full source

@[simp]
theorem range_empty (u : Fin 0 → α) : Set.range u = ∅ :=
  Set.range_eq_empty _

Range of Function from Empty Finite Type is Empty

Informal description

For any function $u$ from the finite type $\text{Fin}\,0$ to a type $\alpha$, the range of $u$ is the empty set, i.e., $\text{range}\,u = \emptyset$.

Matrix.range_cons_empty theorem

(x : α) (u : Fin 0 → α) : Set.range (Matrix.vecCons x u) = { x }

Full source

theorem range_cons_empty (x : α) (u : Fin 0 → α) : Set.range (Matrix.vecCons x u) = {x} := by
  rw [range_cons, range_empty, Set.union_empty]

Range of Singleton Vector Construction from Empty Vector

Informal description

For any element $x$ of type $\alpha$ and any function $u : \text{Fin } 0 \to \alpha$, the range of the vector $\text{vecCons } x\ u$ is equal to the singleton set $\{x\}$.

Matrix.range_cons_cons_empty theorem

(x y : α) (u : Fin 0 → α) : Set.range (vecCons x <| vecCons y u) = { x, y }

Full source

theorem range_cons_cons_empty (x y : α) (u : Fin 0 → α) :
    Set.range (vecCons x <| vecCons y u) = {x, y} := by
  rw [range_cons, range_cons_empty, Set.singleton_union]

Range of Double-Prepended Vector from Empty Vector is $\{x, y\}$

Informal description

For any elements $x$ and $y$ of type $\alpha$ and any function $u : \text{Fin } 0 \to \alpha$, the range of the vector constructed by prepending $x$ to the vector obtained by prepending $y$ to $u$ is equal to the set $\{x, y\}$.

Matrix.vecCons_const theorem

(a : α) : (vecCons a fun _ : Fin n => a) = fun _ => a

Full source

theorem vecCons_const (a : α) : (vecCons a fun _ : Fin n => a) = fun _ => a :=
  funext <| Fin.forall_iff_succ.2 ⟨rfl, cons_val_succ _ _⟩

Constant Vector Construction via Prepending

Informal description

For any element $a$ of type $\alpha$ and any natural number $n$, the vector constructed by prepending $a$ to a constant vector (where every element is $a$) is equal to the constant function that maps every index to $a$. In other words, $\text{vecCons } a (\lambda \_, a) = \lambda \_, a$.

Matrix.vec_single_eq_const theorem

(a : α) : ![a] = fun _ => a

Full source

theorem vec_single_eq_const (a : α) : ![a] = fun _ => a :=
  let _ : Unique (Fin 1) := inferInstance
  funext <| Unique.forall_iff.2 rfl

Singleton Vector as Constant Function

Informal description

For any element $a$ of type $\alpha$, the singleton vector $![a]$ is equal to the constant function that maps every index to $a$.

Matrix.cons_val_one theorem

(x : α) (u : Fin m.succ → α) : vecCons x u 1 = u 0

Full source

/-- `![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 cons_val_one (x : α) (u : Fin m.succ → α) : vecCons x u 1 = u 0 :=
  rfl

First element of prepended vector equals head of original vector

Informal description

For any element $x$ of type $\alpha$ and any vector $u$ of length $m+1$ (represented as a function $u : \text{Fin}(m+1) \to \alpha$), the element at index $1$ of the vector obtained by prepending $x$ to $u$ is equal to the element at index $0$ of $u$. In other words, if we construct a new vector as $(x, u_0, u_1, \ldots)$, then its element at position $1$ equals $u_0$.

Matrix.cons_val_two theorem

(x : α) (u : Fin m.succ.succ → α) : vecCons x u 2 = vecHead (vecTail u)

Full source

theorem cons_val_two (x : α) (u : Fin m.succ.succ → α) : vecCons x u 2 = vecHead (vecTail u) := rfl

Second Element of Prepended Vector Equals Head of Tail

Informal description

For any element $x$ of type $\alpha$ and any vector $u$ of length $m+2$ (represented as a function $u : \text{Fin}(m+2) \to \alpha$), the second element of the vector obtained by prepending $x$ to $u$ is equal to the first element of the tail of $u$. In other words, if we construct a new vector as $(x, u_0, u_1, \ldots)$, then its second element (index 2) equals $u_0$.

Matrix.cons_val_three theorem

(x : α) (u : Fin m.succ.succ.succ → α) : vecCons x u 3 = vecHead (vecTail (vecTail u))

Full source

lemma cons_val_three (x : α) (u : Fin m.succ.succ.succ → α) :
    vecCons x u 3 = vecHead (vecTail (vecTail u)) :=
  rfl

Third Element of Prepended Vector Equals Head of Double Tail

Informal description

For any element $x$ of type $\alpha$ and any vector $u$ of length $m+3$ (represented as a function $u : \text{Fin}(m+3) \to \alpha$), the third element of the vector obtained by prepending $x$ to $u$ is equal to the first element of the tail of the tail of $u$. In other words, if we construct a new vector as $(x, u_0, u_1, u_2, \ldots)$, then its third element (index 3) equals $u_1$.

Matrix.cons_val_four theorem

(x : α) (u : Fin m.succ.succ.succ.succ → α) : vecCons x u 4 = vecHead (vecTail (vecTail (vecTail u)))

Full source

lemma cons_val_four (x : α) (u : Fin m.succ.succ.succ.succ → α) :
    vecCons x u 4 = vecHead (vecTail (vecTail (vecTail u))) :=
  rfl

Fourth Element of Prepended Vector Equals Head of Triple Tail

Informal description

For any element $x$ of type $\alpha$ and any vector $u$ of length $m+4$ (represented as a function $u : \text{Fin}(m+4) \to \alpha$), the fourth element of the vector obtained by prepending $x$ to $u$ is equal to the first element of the triple tail of $u$. In other words, if we construct a new vector as $(x, u_0, u_1, u_2, u_3, \ldots)$, then its fourth element (index 4) equals $u_2$.

Matrix.cons_val_fin_one theorem

(x : α) (u : Fin 0 → α) : ∀ (i : Fin 1), vecCons x u i = x

Full source

@[simp]
theorem cons_val_fin_one (x : α) (u : Fin 0 → α) : ∀ (i : Fin 1), vecCons x u i = x := by
  rw [Fin.forall_fin_one]
  rfl

Constant Property of Prepended Vector over Singleton Index Set

Informal description

For any element $x$ of type $\alpha$ and any empty vector $u : \text{Fin}(0) \to \alpha$, the vector obtained by prepending $x$ to $u$ is constant with value $x$ on all indices $i \in \text{Fin}(1)$. That is, $\text{vecCons}\ x\ u\ i = x$ for all $i \in \text{Fin}(1)$.

Matrix.cons_fin_one theorem

(x : α) (u : Fin 0 → α) : vecCons x u = fun _ => x

Full source

theorem cons_fin_one (x : α) (u : Fin 0 → α) : vecCons x u = fun _ => x :=
  funext (cons_val_fin_one x u)

Constant Function Property of Singleton Vector Construction

Informal description

For any element $x$ of type $\alpha$ and any empty vector $u : \text{Fin}(0) \to \alpha$, the vector obtained by prepending $x$ to $u$ is equal to the constant function that always returns $x$. That is, $\text{vecCons}\ x\ u = (\lambda \_. x)$.

PiFin.mkLiteralQ definition

{u : Level} {α : Q(Type u)} {n : ℕ} (elems : Fin n → Q($α)) : Q(Fin $n → $α)

Full source

/-- `mkVecLiteralQ ![x, y, z]` produces the term `q(![$x, $y, $z])`. -/
def _root_.PiFin.mkLiteralQ {u : Level} {α : Q(Type u)} {n : ℕ} (elems : Fin n → Q($α)) :
    Q(Fin $n → $α) :=
  loop 0 (Nat.zero_le _) q(vecEmpty)
where
  loop (i : ℕ) (hi : i ≤ n) (rest : Q(Fin $i → $α)) : let i' : Nat := i + 1; Q(Fin $(i') → $α) :=
    if h : i < n then
      loop (i + 1) h q(vecCons $(elems (Fin.rev ⟨i, h⟩)) $rest)
    else
      rest

Vector literal term constructor

Informal description

The function `mkVecLiteralQ` constructs a quoted term representing a vector literal `![x₁, x₂, ..., xₙ]` of type `Fin n → α` from given elements `x₁, x₂, ..., xₙ` (represented as quoted terms), where `n` is the length of the vector. The construction is done by iteratively prepending elements to an initially empty vector.

PiFin.toExpr instance

[ToLevel.{u}] [ToExpr α] (n : ℕ) : ToExpr (Fin n → α)

Full source

protected instance _root_.PiFin.toExpr [ToLevelToLevel.{u}] [ToExpr α] (n : ℕ) : ToExpr (Fin n → α) :=
  have lu := toLevel.{u}
  have eα : Q(Type $lu) := toTypeExpr α
  let toTypeExpr := q(Fin $n → $eα)
  { toTypeExpr, toExpr v := PiFin.mkLiteralQ fun i => show Q($eα) from toExpr (v i) }

Expression Construction for Vectors

Informal description

For any type $\alpha$ with a `ToExpr` instance and any natural number $n$, there is a `ToExpr` instance for the type of vectors `Fin n → α` (functions from `Fin n` to $\alpha$). This allows Lean to construct expressions representing vectors of length $n$ with elements of type $\alpha$.

Matrix.vecAppend definition

{α : Type*} {o : ℕ} (ho : o = m + n) (u : Fin m → α) (v : Fin n → α) : Fin o → α

Full source

/-- `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. -/
def vecAppend {α : Type*} {o : ℕ} (ho : o = m + n) (u : Fin m → α) (v : Fin n → α) : Fin o → α :=
  Fin.appendFin.append u v ∘ Fin.cast ho

Vector concatenation with length control

Informal description

Given a type $\alpha$, natural numbers $m$, $n$, and $o$ such that $o = m + n$, a vector $u$ of length $m$ (i.e., a function $u : \text{Fin}\, m \to \alpha$), and a vector $v$ of length $n$ (i.e., a function $v : \text{Fin}\, n \to \alpha$), the function $\text{vecAppend}\, ho\, u\, v$ constructs a new vector of length $o$ by concatenating $u$ and $v$. More precisely, for $i < o$, the $i$-th element of the resulting vector is $u\, i$ if $i < m$, and $v\, (i - m)$ otherwise. The argument $ho$ ensures that the length of the resulting vector is definitionally equal to $m + n$.

Matrix.vecAppend_eq_ite theorem

 {α : Type*} {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, by omega⟩

Full source

theorem vecAppend_eq_ite {α : Type*} {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, by omega⟩ := by
  ext i
  rw [vecAppend, Fin.append, Function.comp_apply, Fin.addCases]
  congr with hi
  simp only [eq_rec_constant]
  rfl

Characterization of Vector Concatenation via Conditional Expression

Informal description

Let $\alpha$ be a type, and let $m$, $n$, and $o$ be natural numbers such that $o = m + n$. Given vectors $u : \text{Fin}\, m \to \alpha$ and $v : \text{Fin}\, n \to \alpha$, the concatenated vector $\text{vecAppend}\, ho\, u\, v$ is equal to the function that maps each index $i : \text{Fin}\, o$ to $u\, \langle i, h \rangle$ if $i < m$ (where $h$ is a proof that $i < m$), and to $v\, \langle i - m, \text{by omega} \rangle$ otherwise.

Matrix.vecAppend_apply_zero theorem

{α : Type*} {o : ℕ} (ho : o + 1 = m + 1 + n) (u : Fin (m + 1) → α) (v : Fin n → α) : vecAppend ho u v 0 = u 0

Full source

@[simp]
theorem vecAppend_apply_zero {α : Type*} {o : ℕ} (ho : o + 1 = m + 1 + n) (u : Fin (m + 1) → α)
    (v : Fin n → α) : vecAppend ho u v 0 = u 0 :=
  dif_pos _

First Element of Concatenated Vector Equals First Element of First Vector

Informal description

Let $\alpha$ be a type, and let $m$, $n$, and $o$ be natural numbers such that $o + 1 = m + 1 + n$. Given a vector $u : \text{Fin}\, (m + 1) \to \alpha$ and a vector $v : \text{Fin}\, n \to \alpha$, the first element of the concatenated vector $\text{vecAppend}\, ho\, u\, v$ is equal to the first element of $u$, i.e., $(\text{vecAppend}\, ho\, u\, v)\, 0 = u\, 0$.

Matrix.empty_vecAppend theorem

(v : Fin n → α) : vecAppend n.zero_add.symm ![] v = v

Full source

@[simp]
theorem empty_vecAppend (v : Fin n → α) : vecAppend n.zero_add.symm ![] v = v := by
  ext
  simp [vecAppend_eq_ite]

Concatenation with Empty Vector Yields Original Vector

Informal description

For any vector $v$ of length $n$ (i.e., $v : \text{Fin}\, n \to \alpha$), concatenating the empty vector `![]` with $v$ using the length condition $n = 0 + n$ yields $v$ itself. That is, $\text{vecAppend}\, n.zero\_add.symm\, ![]\, v = v$.

Matrix.cons_vecAppend theorem

 (ho : o + 1 = m + 1 + n) (x : α) (u : Fin m → α) (v : Fin n → α) :
  vecAppend ho (vecCons x u) v = vecCons x (vecAppend (by omega) u v)

Full source

@[simp]
theorem cons_vecAppend (ho : o + 1 = m + 1 + n) (x : α) (u : Fin m → α) (v : Fin n → α) :
    vecAppend ho (vecCons x u) v = vecCons x (vecAppend (by omega) u v) := by
  ext i
  simp_rw [vecAppend_eq_ite]
  split_ifs with h
  · rcases i with ⟨⟨⟩ | i, hi⟩
    · simp
    · simp only [Nat.add_lt_add_iff_right, Fin.val_mk] at h
      simp [h]
  · rcases i with ⟨⟨⟩ | i, hi⟩
    · simp at h
    · rw [not_lt, Fin.val_mk, Nat.add_le_add_iff_right] at h
      simp [h, not_lt.2 h]

Concatenation-Prepend Commutativity for Vectors

Informal description

Given natural numbers $m$, $n$, and $o$ such that $o + 1 = m + 1 + n$, an element $x$ of type $\alpha$, a vector $u : \text{Fin}\, m \to \alpha$, and a vector $v : \text{Fin}\, n \to \alpha$, the concatenation of the vector $\text{vecCons}\, x\, u$ with $v$ is equal to the vector obtained by prepending $x$ to the concatenation of $u$ and $v$. More precisely, we have: $$\text{vecAppend}\, ho\, (\text{vecCons}\, x\, u)\, v = \text{vecCons}\, x\, (\text{vecAppend}\, (\text{by omega})\, u\, v)$$ where $\text{by omega}$ refers to the automatically generated proof that $o = m + n$.

Matrix.vecAlt0 definition

(hm : m = n + n) (v : Fin m → α) (k : Fin n) : α

Full source

/-- `vecAlt0 v` gives a vector with half the length of `v`, with
only alternate elements (even-numbered). -/
def vecAlt0 (hm : m = n + n) (v : Fin m → α) (k : Fin n) : α := v ⟨(k : ℕ) + k, by omega⟩

Even-indexed elements of a vector

Informal description

Given a natural number $n$ and a vector $v$ of length $m = 2n$ (i.e., $v \colon \text{Fin}\, m \to \alpha$), the function $\text{vecAlt0}$ returns a vector of length $n$ consisting of the even-indexed elements of $v$. Specifically, for each index $k \in \text{Fin}\, n$, the $k$-th element of $\text{vecAlt0}\, v$ is $v_{2k}$.

Matrix.vecAlt1 definition

(hm : m = n + n) (v : Fin m → α) (k : Fin n) : α

Full source

/-- `vecAlt1 v` gives a vector with half the length of `v`, with
only alternate elements (odd-numbered). -/
def vecAlt1 (hm : m = n + n) (v : Fin m → α) (k : Fin n) : α :=
  v ⟨(k : ℕ) + k + 1, hm.symm ▸ Nat.add_succ_lt_add k.2 k.2⟩

Odd-indexed elements of a vector

Informal description

Given a natural number `n` and a vector `v` of length `m = 2n`, the function `vecAlt1 v` returns a vector of length `n` consisting of the odd-indexed elements of `v` (i.e., elements at positions `1, 3, ..., 2n-1` when indexed starting from 0). More precisely, for each index `k` in the new vector, the element is taken from position `2k + 1` of the original vector `v`.

Matrix.vecAlt0_vecAppend theorem

(v : Fin n → α) : vecAlt0 rfl (vecAppend rfl v v) = v ∘ (fun n ↦ n + n)

Full source

theorem vecAlt0_vecAppend (v : Fin n → α) :
    vecAlt0 rfl (vecAppend rfl v v) = v ∘ (fun n ↦ n + n) := by
  ext i
  simp_rw [Function.comp, vecAlt0, vecAppend_eq_ite]
  split_ifs with h <;> congr
  · rw [Fin.val_mk] at h
    exact (Nat.mod_eq_of_lt h).symm
  · rw [Fin.val_mk, not_lt] at h
    simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_eq_sub_mod h]
    refine (Nat.mod_eq_of_lt ?_).symm
    omega

Even-indexed subvector of self-concatenation equals $v \circ (k \mapsto 2k)$

Informal description

For any vector $v \colon \text{Fin}\, n \to \alpha$, the even-indexed subvector of the concatenation of $v$ with itself is equal to the composition of $v$ with the function $k \mapsto 2k$. That is, $\text{vecAlt0}\, \text{rfl}\, (\text{vecAppend}\, \text{rfl}\, v\, v) = v \circ (k \mapsto 2k)$.

Matrix.vecAlt1_vecAppend theorem

(v : Fin (n + 1) → α) : vecAlt1 rfl (vecAppend rfl v v) = v ∘ (fun n ↦ (n + n) + 1)

Full source

theorem vecAlt1_vecAppend (v : Fin (n + 1) → α) :
    vecAlt1 rfl (vecAppend rfl v v) = v ∘ (fun n ↦ (n + n) + 1) := by
  ext i
  simp_rw [Function.comp, vecAlt1, vecAppend_eq_ite]
  cases n with
  | zero =>
    obtain ⟨i, hi⟩ := i
    simp only [Nat.zero_add, Nat.lt_one_iff] at hi; subst i; rfl
  | succ n =>
    split_ifs with h <;> congr
    · simp [Nat.mod_eq_of_lt, h]
    · rw [Fin.val_mk, not_lt] at h
      simp only [Fin.ext_iff, Fin.val_add, Fin.val_mk, Nat.mod_add_mod, Fin.val_one,
        Nat.mod_eq_sub_mod h, show 1 % (n + 2) = 1 from Nat.mod_eq_of_lt (by omega)]
      refine (Nat.mod_eq_of_lt ?_).symm
      omega

Odd-indexed Subvector of Self-Concatenation Equals Shifted Composition

Informal description

For any vector $v$ of length $n+1$ with entries in a type $\alpha$, the odd-indexed subvector of the concatenation of $v$ with itself is equal to the composition of $v$ with the function $k \mapsto 2k + 1$. That is, $\text{vecAlt1}\, \text{rfl}\, (\text{vecAppend}\, \text{rfl}\, v\, v) = v \circ (k \mapsto 2k + 1)$.

Matrix.vecHead_vecAlt0 theorem

(hm : m + 2 = n + 1 + (n + 1)) (v : Fin (m + 2) → α) : vecHead (vecAlt0 hm v) = v 0

Full source

@[simp]
theorem vecHead_vecAlt0 (hm : m + 2 = n + 1 + (n + 1)) (v : Fin (m + 2) → α) :
    vecHead (vecAlt0 hm v) = v 0 :=
  rfl

First Entry of Even-Indexed Subvector Equals Initial Entry

Informal description

Let $m$ and $n$ be natural numbers such that $m + 2 = n + 1 + (n + 1)$, and let $v$ be a vector of length $m + 2$ with entries in a type $\alpha$. Then the first entry of the vector obtained by taking the even-indexed elements of $v$ (via $\text{vecAlt0}$) is equal to $v(0)$.

Matrix.vecHead_vecAlt1 theorem

(hm : m + 2 = n + 1 + (n + 1)) (v : Fin (m + 2) → α) : vecHead (vecAlt1 hm v) = v 1

Full source

@[simp]
theorem vecHead_vecAlt1 (hm : m + 2 = n + 1 + (n + 1)) (v : Fin (m + 2) → α) :
    vecHead (vecAlt1 hm v) = v 1 := by simp [vecHead, vecAlt1]

First Entry of Odd-Indexed Subvector Equals Second Entry

Informal description

Let $m$ and $n$ be natural numbers such that $m + 2 = n + 1 + (n + 1)$, and let $v$ be a vector of length $m + 2$ with entries in a type $\alpha$. Then the first entry of the vector obtained by taking the odd-indexed elements of $v$ (via $\text{vecAlt1}$) is equal to $v(1)$.

Matrix.cons_vec_bit0_eq_alt0 theorem

 (x : α) (u : Fin n → α) (i : Fin (n + 1)) :
  vecCons x u (i + i) = vecAlt0 rfl (vecAppend rfl (vecCons x u) (vecCons x u)) i

Full source

theorem cons_vec_bit0_eq_alt0 (x : α) (u : Fin n → α) (i : Fin (n + 1)) :
    vecCons x u (i + i) = vecAlt0 rfl (vecAppend rfl (vecCons x u) (vecCons x u)) i := by
  rw [vecAlt0_vecAppend]; rfl

Even-indexed elements of prepended vector via concatenation: $(\text{vecCons}\, x\, u)(2i) = \text{vecAlt0}(\text{vecAppend}\, (\text{vecCons}\, x\, u)^2)_i$

Informal description

For any element $x$ of type $\alpha$, a vector $u \colon \text{Fin}\, n \to \alpha$, and an index $i \in \text{Fin}\, (n + 1)$, the $(2i)$-th element of the vector obtained by prepending $x$ to $u$ is equal to the $i$-th element of the even-indexed subvector of the concatenation of $\text{vecCons}\, x\, u$ with itself. In other words, $(\text{vecCons}\, x\, u)(2i) = \text{vecAlt0}\, \text{rfl}\, (\text{vecAppend}\, \text{rfl}\, (\text{vecCons}\, x\, u)\, (\text{vecCons}\, x\, u))\, i$.

Matrix.cons_vec_bit1_eq_alt1 theorem

 (x : α) (u : Fin n → α) (i : Fin (n + 1)) :
  vecCons x u ((i + i) + 1) = vecAlt1 rfl (vecAppend rfl (vecCons x u) (vecCons x u)) i

Full source

theorem cons_vec_bit1_eq_alt1 (x : α) (u : Fin n → α) (i : Fin (n + 1)) :
    vecCons x u ((i + i) + 1) = vecAlt1 rfl (vecAppend rfl (vecCons x u) (vecCons x u)) i := by
  rw [vecAlt1_vecAppend]; rfl

Odd-indexed elements of prepended vector via concatenation: $(\text{vecCons}\, x\, u)(2i + 1) = \text{vecAlt1}(\text{vecAppend}\, (\text{vecCons}\, x\, u)^2)_i$

Informal description

For any element $x$ of type $\alpha$, a vector $u \colon \text{Fin}\, n \to \alpha$, and an index $i \in \text{Fin}\, (n + 1)$, the $(2i + 1)$-th element of the vector obtained by prepending $x$ to $u$ is equal to the $i$-th element of the odd-indexed subvector of the concatenation of $\text{vecCons}\, x\, u$ with itself. In other words, $(\text{vecCons}\, x\, u)(2i + 1) = \text{vecAlt1}\, \text{rfl}\, (\text{vecAppend}\, \text{rfl}\, (\text{vecCons}\, x\, u)\, (\text{vecCons}\, x\, u))\, i$.

Matrix.cons_vecAlt0 theorem

 (h : m + 1 + 1 = n + 1 + (n + 1)) (x y : α) (u : Fin m → α) :
  vecAlt0 h (vecCons x (vecCons y u)) = vecCons x (vecAlt0 (by omega) u)

Full source

@[simp]
theorem cons_vecAlt0 (h : m + 1 + 1 = n + 1 + (n + 1)) (x y : α) (u : Fin m → α) :
    vecAlt0 h (vecCons x (vecCons y u)) = vecCons x (vecAlt0 (by omega) u) := by
  ext i
  simp_rw [vecAlt0]
  rcases i with ⟨⟨⟩ | i, hi⟩
  · rfl
  · simp only [← Nat.add_assoc, Nat.add_right_comm, cons_val_succ',
      cons_vecAppend, Nat.add_eq, vecAlt0]

Even-indexed elements of prepended vector: $\text{vecAlt0}(\text{vecCons } x (\text{vecCons } y\ u)) = \text{vecCons } x (\text{vecAlt0 } u)$

Informal description

For any natural numbers $m$ and $n$ satisfying $m + 2 = 2(n + 1)$, elements $x, y \in \alpha$, and vector $u : \text{Fin } m \to \alpha$, the even-indexed elements of the vector $\text{vecCons } x (\text{vecCons } y\ u)$ are equal to $\text{vecCons } x (\text{vecAlt0 } u)$, where $\text{vecAlt0}$ extracts the even-indexed elements. More precisely, when constructing a new vector by prepending $x$ and $y$ to $u$, the even-indexed elements of this new vector (positions 0, 2, ...) consist of $x$ followed by the even-indexed elements of $u$.

Matrix.empty_vecAlt0 theorem

(α) {h} : vecAlt0 h (![] : Fin 0 → α) = ![]

Full source

@[simp]
theorem empty_vecAlt0 (α) {h} : vecAlt0 h (![] : Fin 0 → α) = ![] := by
  simp [eq_iff_true_of_subsingleton]

Empty Vector Property for Even-Indexed Elements: $\text{vecAlt0}\, ![] = ![]$

Informal description

For any type $\alpha$ and any proof $h$ that $0 = 0 + 0$, applying the `vecAlt0` function to the empty vector `![]` results in another empty vector `![]$.

Matrix.cons_vecAlt1 theorem

 (h : m + 1 + 1 = n + 1 + (n + 1)) (x y : α) (u : Fin m → α) :
  vecAlt1 h (vecCons x (vecCons y u)) = vecCons y (vecAlt1 (by omega) u)

Full source

@[simp]
theorem cons_vecAlt1 (h : m + 1 + 1 = n + 1 + (n + 1)) (x y : α) (u : Fin m → α) :
    vecAlt1 h (vecCons x (vecCons y u)) = vecCons y (vecAlt1 (by omega) u) := by
  ext i
  simp_rw [vecAlt1]
  rcases i with ⟨⟨⟩ | i, hi⟩
  · rfl
  · simp [vecAlt1, Nat.add_right_comm, ← Nat.add_assoc]

Odd-indexed elements of prepended vector: $\text{vecAlt1}(\text{vecCons } x (\text{vecCons } y\ u)) = \text{vecCons } y (\text{vecAlt1 } u)$

Informal description

For any natural numbers $m$ and $n$ satisfying $m + 2 = 2(n + 1)$, elements $x, y \in \alpha$, and vector $u : \text{Fin } m \to \alpha$, the odd-indexed elements of the vector $\text{vecCons } x (\text{vecCons } y\ u)$ are equal to $\text{vecCons } y (\text{vecAlt1 } u)$, where $\text{vecAlt1}$ extracts the odd-indexed elements. More precisely, when constructing a new vector by prepending $x$ and $y$ to $u$, the odd-indexed elements of this new vector (positions 1, 3, ...) consist of $y$ followed by the odd-indexed elements of $u$.

Matrix.empty_vecAlt1 theorem

(α) {h} : vecAlt1 h (![] : Fin 0 → α) = ![]

Full source

@[simp]
theorem empty_vecAlt1 (α) {h} : vecAlt1 h (![] : Fin 0 → α) = ![] := by
  simp [eq_iff_true_of_subsingleton]

Empty Vector Yields Empty Vector under `vecAlt1`

Informal description

For any type $\alpha$ and any hypothesis $h$ (which is automatically satisfied when $m = 0$), the function `vecAlt1` applied to the empty vector `![]` of type `Fin 0 → α` yields the empty vector `![]`.

Matrix.const_fin1_eq theorem

(x : α) : (fun _ : Fin 1 => x) = ![x]

Full source

lemma const_fin1_eq (x : α) : (fun _ : Fin 1 => x) = ![x] :=
  (cons_fin_one x _).symm

Constant Function as Singleton Vector: $(\lambda \_, x) = [x]$ for $\text{Fin}(1)$

Informal description

For any element $x$ of type $\alpha$, the constant function that maps every element of $\text{Fin}(1)$ to $x$ is equal to the singleton vector $[x]$, i.e., $(\lambda \_ : \text{Fin}(1), x) = [x]$.

Mathlib.Data.Fin.VecNotation

Main definitions

Implementation notes

Notations

Examples