Mathlib.Data.Vector.Basic

List.Vector.term_::ᵥ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
infixr:67 " ::ᵥ " => Vector.cons

Vector cons notation `::ᵥ`

Informal description

The infix notation `::ᵥ` is introduced as a shorthand for `Vector.cons`, with right associativity and precedence level 67.

List.Vector.instInhabited instance

[Inhabited α] : Inhabited (Vector α n)

Full source

instance [Inhabited α] : Inhabited (Vector α n) :=
  ⟨ofFn default⟩

Inhabitedness of List-Based Vectors

Informal description

For any inhabited type $\alpha$ and natural number $n$, the type of list-based vectors $\text{Vector}\,\alpha\,n$ is also inhabited.

List.Vector.toList_injective theorem

: Function.Injective (@toList α n)

Full source

theorem toList_injective : Function.Injective (@toList α n) :=
  Subtype.val_injective

Injectivity of the Underlying List Function for Vectors

Informal description

The function `toList` that maps a vector of type `List.Vector α n` to its underlying list is injective. That is, for any two vectors $v, w : \text{List.Vector } \alpha \text{ } n$, if $\text{toList}(v) = \text{toList}(w)$, then $v = w$.

List.Vector.ext theorem

: ∀ {v w : Vector α n} (_ : ∀ m : Fin n, Vector.get v m = Vector.get w m), v = w

Full source

/-- Two `v w : Vector α n` are equal iff they are equal at every single index. -/
@[ext]
theorem ext : ∀ {v w : Vector α n} (_ : ∀ m : Fin n, Vector.get v m = Vector.get w m), v = w
  | ⟨v, hv⟩, ⟨w, hw⟩, h =>
    Subtype.eq (List.ext_get (by rw [hv, hw]) fun m hm _ => h ⟨m, hv ▸ hm⟩)

Extensionality of List-Based Vectors

Informal description

Two vectors $v$ and $w$ of type `List.Vector α n` (lists of length $n$ with elements in $\alpha$) are equal if and only if their elements are equal at every index $m$ in the finite set $\{0, \dots, n-1\}$.

List.Vector.zero_subsingleton instance

: Subsingleton (Vector α 0)

Full source

/-- The empty `Vector` is a `Subsingleton`. -/
instance zero_subsingleton : Subsingleton (Vector α 0) :=
  ⟨fun _ _ => Vector.ext fun m => Fin.elim0 m⟩

The Empty Vector is a Subsingleton

Informal description

For any type $\alpha$, the type of vectors of length $0$ (i.e., the empty vector) is a subsingleton, meaning there is at most one element of type `Vector α 0`.

List.Vector.cons_val theorem

(a : α) : ∀ v : Vector α n, (a ::ᵥ v).val = a :: v.val

Full source

@[simp]
theorem cons_val (a : α) : ∀ v : Vector α n, (a ::ᵥ v).val = a :: v.val
  | ⟨_, _⟩ => rfl

Underlying List of Cons Vector Equals Cons of Element and Original List

Informal description

For any element $a$ of type $\alpha$ and any vector $v$ of length $n$ over $\alpha$, the underlying list of the vector $a ::ᵥ v$ is equal to the list $a :: v.\text{val}$, where $v.\text{val}$ denotes the underlying list of $v$.

List.Vector.ne_cons_iff theorem

(a : α) (v : Vector α n.succ) (v' : Vector α n) : v ≠ a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v'

Full source

theorem ne_cons_iff (a : α) (v : Vector α n.succ) (v' : Vector α n) :
    v ≠ a ::ᵥ v'v ≠ a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v' := by rw [Ne, eq_cons_iff a v v', not_and_or]

Characterization of Vector Inequality via Head and Tail

Informal description

For any element $a$ of type $\alpha$, a vector $v$ of length $n+1$ over $\alpha$, and a vector $v'$ of length $n$ over $\alpha$, the vector $v$ is not equal to the concatenation $a :: v'$ if and only if either the head of $v$ is not equal to $a$ or the tail of $v$ is not equal to $v'$. In other words, $v \neq a :: v' \leftrightarrow \text{head}(v) \neq a \lor \text{tail}(v) \neq v'$.

List.Vector.exists_eq_cons theorem

(v : Vector α n.succ) : ∃ (a : α) (as : Vector α n), v = a ::ᵥ as

Full source

theorem exists_eq_cons (v : Vector α n.succ) : ∃ (a : α) (as : Vector α n), v = a ::ᵥ as :=
  ⟨v.head, v.tail, (eq_cons_iff v.head v v.tail).2 ⟨rfl, rfl⟩⟩

Decomposition of Non-Empty Vector into Head and Tail

Informal description

For any vector $v$ of length $n+1$ over a type $\alpha$, there exists an element $a \in \alpha$ and a vector $v'$ of length $n$ such that $v$ can be expressed as the concatenation $a :: v'$.

List.Vector.toList_ofFn theorem

: ∀ {n} (f : Fin n → α), toList (ofFn f) = List.ofFn f

Full source

@[simp]
theorem toList_ofFn : ∀ {n} (f : Fin n → α), toList (ofFn f) = List.ofFn f
  | 0, f => by rw [ofFn, List.ofFn_zero, toList, nil]
  | n + 1, f => by rw [ofFn, List.ofFn_succ, toList_cons, toList_ofFn]

List Conversion of Vector Construction from Function: $\text{toList}(\text{ofFn}(f)) = \text{List.ofFn}(f)$

Informal description

For any natural number $n$ and any function $f \colon \mathrm{Fin}\,n \to \alpha$, the underlying list of the vector constructed from $f$ via `ofFn` is equal to the list constructed from $f$ via `List.ofFn$. In symbols: $\text{toList}(\text{ofFn}(f)) = \text{List.ofFn}(f)$.

List.Vector.mk_toList theorem

: ∀ (v : Vector α n) (h), (⟨toList v, h⟩ : Vector α n) = v

Full source

@[simp]
theorem mk_toList : ∀ (v : Vector α n) (h), (⟨toList v, h⟩ : Vector α n) = v
  | ⟨_, _⟩, _ => rfl

Reconstruction of Vector from Underlying List Preserves Identity

Informal description

For any vector $v$ of type `List.Vector α n` and any proof $h$ that the length of the underlying list `toList v` is equal to $n$, the vector constructed from `toList v` with the proof $h$ is equal to $v$ itself.

List.Vector.length_val theorem

(v : Vector α n) : v.val.length = n

Full source

@[simp] theorem length_val (v : Vector α n) : v.val.length = n := v.2

Length of Underlying List in Fixed-Length Vector

Informal description

For any vector $v$ of type `List.Vector α n` (a list-based vector with elements of type $\alpha$ and fixed length $n$), the length of the underlying list $v.\text{val}$ is equal to $n$.

List.Vector.pmap_cons theorem

 {p : α → Prop} (f : (a : α) → p a → β) (a : α) (v : Vector α n) (hp : ∀ x ∈ (cons a v).toList, p x) :
  (cons a v).pmap f hp =
    cons
      (f a
        (by
          simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp
          exact hp.1))
      (v.pmap f
        (by
          simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp
          exact hp.2))

Full source

@[simp]
theorem pmap_cons {p : α → Prop} (f : (a : α) → p a → β) (a : α) (v : Vector α n)
    (hp : ∀ x ∈ (cons a v).toList, p x) :
    (cons a v).pmap f hp = cons (f a (by
      simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp
      exact hp.1))
      (v.pmap f (by
        simp only [Nat.succ_eq_add_one, toList_cons, List.mem_cons, forall_eq_or_imp] at hp
        exact hp.2)) := rfl

Partial Mapping of Cons Vector: $\text{pmap}\, f\, (\text{cons}(a, v))\, h = \text{cons}(f\, a\, h_1)\, (\text{pmap}\, f\, v\, h_2)$

Informal description

Let $\alpha$ and $\beta$ be types, $p : \alpha \to \text{Prop}$ be a predicate, $f : (a : \alpha) \to p(a) \to \beta$ be a function, $a \in \alpha$ be an element, and $v \in \text{Vector } \alpha n$ be a vector of length $n$. If every element in the vector $\text{cons}(a, v)$ satisfies $p$, then the partial mapping of $\text{cons}(a, v)$ under $f$ is equal to the vector obtained by prepending $f(a)$ (with proof that $p(a)$ holds) to the partial mapping of $v$ under $f$. More formally: \[ \text{pmap}\, f\, (\text{cons}(a, v))\, h = \text{cons}(f\, a\, h_1)\, (\text{pmap}\, f\, v\, h_2) \] where $h$ is the proof that all elements in $\text{cons}(a, v)$ satisfy $p$, $h_1$ is the proof that $a$ satisfies $p$, and $h_2$ is the proof that all elements in $v$ satisfy $p$.

List.Vector.pmap_cons' theorem

 {p : α → Prop} (f : (a : α) → p a → β) (a : α) (v : Vector α n) (ha : p a) (hp : ∀ x ∈ v.toList, p x) :
  cons (f a ha) (v.pmap f hp) = (cons a v).pmap f (by simpa [ha])

Full source

/-- Opposite direction of `Vector.pmap_cons` -/
theorem pmap_cons' {p : α → Prop} (f : (a : α) → p a → β) (a : α) (v : Vector α n)
    (ha : p a) (hp : ∀ x ∈ v.toList, p x) :
    cons (f a ha) (v.pmap f hp) = (cons a v).pmap f (by simpa [ha]) := rfl

Partial Mapping of Cons Vector: $\text{cons}(f\, a\, ha)\, (\text{pmap}\, f\, v\, hp) = \text{pmap}\, f\, (\text{cons}(a, v))\, h$

Informal description

Let $\alpha$ and $\beta$ be types, $p : \alpha \to \text{Prop}$ be a predicate, and $f : (a : \alpha) \to p(a) \to \beta$ be a function. For any element $a \in \alpha$ satisfying $p(a)$ and any vector $v \in \text{Vector } \alpha n$ where all elements satisfy $p$, the vector obtained by prepending $f(a)$ (with proof $ha$) to the partial mapping of $v$ under $f$ is equal to the partial mapping of $\text{cons}(a, v)$ under $f$. In symbols: \[ \text{cons}(f\, a\, ha)\, (\text{pmap}\, f\, v\, hp) = \text{pmap}\, f\, (\text{cons}(a, v))\, h \] where $h$ is the proof that all elements in $\text{cons}(a, v)$ satisfy $p$ (which follows from $ha$ and $hp$).

List.Vector.toList_map theorem

{β : Type*} (v : Vector α n) (f : α → β) : (v.map f).toList = v.toList.map f

Full source

@[simp]
theorem toList_map {β : Type*} (v : Vector α n) (f : α → β) :
    (v.map f).toList = v.toList.map f := by cases v; rfl

Mapping Commutes with Underlying List Construction

Informal description

For any vector $\mathbf{v} \in \text{Vector} \alpha n$ and any function $f : \alpha \to \beta$, the underlying list of the mapped vector $\mathbf{v}.map(f)$ is equal to the mapped underlying list of $\mathbf{v}$, i.e., $(\mathbf{v}.map(f)).toList = \mathbf{v}.toList.map(f)$.

List.Vector.head_map theorem

{β : Type*} (v : Vector α (n + 1)) (f : α → β) : (v.map f).head = f v.head

Full source

@[simp]
theorem head_map {β : Type*} (v : Vector α (n + 1)) (f : α → β) : (v.map f).head = f v.head := by
  obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
  rw [h, map_cons, head_cons, head_cons]

Head Preservation under Vector Mapping: $(v.map(f)).head = f(v.head)$

Informal description

For any vector $v$ of length $n+1$ over a type $\alpha$ and any function $f : \alpha \to \beta$, the head of the mapped vector $v.map(f)$ is equal to $f$ applied to the head of $v$, i.e., $(v.map(f)).head = f(v.head)$.

List.Vector.tail_map theorem

{β : Type*} (v : Vector α (n + 1)) (f : α → β) : (v.map f).tail = v.tail.map f

Full source

@[simp]
theorem tail_map {β : Type*} (v : Vector α (n + 1)) (f : α → β) :
    (v.map f).tail = v.tail.map f := by
  obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
  rw [h, map_cons, tail_cons, tail_cons]

Tail-Map Commutation for Vectors: $(v.map(f)).tail = (v.tail).map(f)$

Informal description

For any vector $v$ of length $n+1$ over a type $\alpha$ and any function $f : \alpha \to \beta$, the tail of the mapped vector $v.map(f)$ is equal to the mapped tail of $v$, i.e., $(v.map(f)).tail = (v.tail).map(f)$.

List.Vector.getElem_map theorem

{β : Type*} (v : Vector α n) (f : α → β) {i : ℕ} (hi : i < n) : (v.map f)[i] = f v[i]

Full source

@[simp]
theorem getElem_map {β : Type*} (v : Vector α n) (f : α → β) {i : ℕ} (hi : i < n) :
    (v.map f)[i] = f v[i] := by
  simp only [getElem_def, toList_map, List.getElem_map]

Element-wise Mapping of Vectors: $(\mathbf{v}.map(f))[i] = f(\mathbf{v}[i])$

Informal description

For any vector $\mathbf{v} \in \text{Vector} \alpha n$, any function $f \colon \alpha \to \beta$, and any index $i \in \mathbb{N}$ with $i < n$, the $i$-th element of the mapped vector $\mathbf{v}.map(f)$ is equal to $f$ applied to the $i$-th element of $\mathbf{v}$, i.e., $(\mathbf{v}.map(f))[i] = f(\mathbf{v}[i])$.

List.Vector.toList_pmap theorem

 {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α n) (hp : ∀ x ∈ v.toList, p x) :
  (v.pmap f hp).toList = v.toList.pmap f hp

Full source

@[simp]
theorem toList_pmap {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α n)
    (hp : ∀ x ∈ v.toList, p x) :
    (v.pmap f hp).toList = v.toList.pmap f hp := by cases v; rfl

Underlying List Preserves Partial Mapping: $\text{toList}(\text{pmap}(f, \mathbf{v}, hp)) = \text{toList}(\mathbf{v}).\text{pmap}(f, hp)$

Informal description

For any predicate $p$ on elements of type $\alpha$, any function $f \colon (a \colon \alpha) \to p(a) \to \beta$, and any vector $\mathbf{v} \in \text{Vector } \alpha n$ where all elements satisfy $p$, the underlying list of the partially mapped vector $\text{pmap}(f, \mathbf{v}, hp)$ is equal to the partial mapping of the underlying list of $\mathbf{v}$ with $f$ and $hp$. In other words, if $\mathbf{v}$ is a vector of length $n$ with $\forall x \in \text{toList}(\mathbf{v}), p(x)$, then: $$ \text{toList}(\text{pmap}(f, \mathbf{v}, hp)) = \text{toList}(\mathbf{v}).\text{pmap}(f, hp) $$

List.Vector.head_pmap theorem

 {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α (n + 1)) (hp : ∀ x ∈ v.toList, p x) :
  (v.pmap f hp).head =
    f v.head (hp _ <| by rw [← cons_head_tail v, toList_cons, head_cons, List.mem_cons]; exact .inl rfl)

Full source

@[simp]
theorem head_pmap {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α (n + 1))
    (hp : ∀ x ∈ v.toList, p x) :
    (v.pmap f hp).head = f v.head (hp _ <| by
      rw [← cons_head_tail v, toList_cons, head_cons, List.mem_cons]; exact .inl rfl) := by
  obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
  simp_rw [h, pmap_cons, head_cons]

Head of Partially Mapped Vector Equals Function Applied to Head

Informal description

For any predicate $p$ on elements of type $\alpha$, any function $f \colon (a \colon \alpha) \to p(a) \to \beta$, and any vector $v$ of length $n+1$ over $\alpha$ where all elements satisfy $p$, the head of the partially mapped vector $\text{pmap}(f, v, hp)$ is equal to $f$ applied to the head of $v$ and the proof that it satisfies $p$. More precisely, if $v$ is a vector of length $n+1$ with $\forall x \in \text{toList}(v), p(x)$, then: $$ \text{head}(\text{pmap}(f, v, hp)) = f(\text{head}(v), \text{proof that } \text{head}(v) \text{ satisfies } p) $$

List.Vector.tail_pmap theorem

 {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α (n + 1)) (hp : ∀ x ∈ v.toList, p x) :
  (v.pmap f hp).tail =
    v.tail.pmap f (fun x hx ↦ hp _ <| by rw [← cons_head_tail v, toList_cons, List.mem_cons]; exact .inr hx)

Full source

@[simp]
theorem tail_pmap {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α (n + 1))
    (hp : ∀ x ∈ v.toList, p x) :
    (v.pmap f hp).tail = v.tail.pmap f (fun x hx ↦ hp _ <| by
      rw [← cons_head_tail v, toList_cons, List.mem_cons]; exact .inr hx) := by
  obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v
  simp_rw [h, pmap_cons, tail_cons]

Tail of Partially Mapped Vector Equals Partial Mapping of Tail

Informal description

For any predicate $p$ on elements of type $\alpha$, any function $f \colon (a \colon \alpha) \to p(a) \to \beta$, and any vector $v$ of length $n+1$ over $\alpha$ where all elements satisfy $p$, the tail of the partially mapped vector $\text{pmap}(f, v, hp)$ is equal to the partial mapping of the tail of $v$ with $f$ and the proof that its elements satisfy $p$. More precisely, if $v$ is a vector of length $n+1$ with $\forall x \in \text{toList}(v), p(x)$, then: $$ \text{tail}(\text{pmap}(f, v, hp)) = \text{pmap}(f, \text{tail}(v), \text{proof that tail elements satisfy } p) $$

List.Vector.getElem_pmap theorem

 {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α n) (hp : ∀ x ∈ v.toList, p x) {i : ℕ} (hi : i < n) :
  (v.pmap f hp)[i] = f v[i] (hp _ (by simp [getElem_def, List.getElem_mem]))

Full source

@[simp]
theorem getElem_pmap {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α n)
    (hp : ∀ x ∈ v.toList, p x) {i : ℕ} (hi : i < n) :
    (v.pmap f hp)[i] = f v[i] (hp _ (by simp [getElem_def, List.getElem_mem])) := by
  simp only [getElem_def, toList_pmap, List.getElem_pmap]

Element-wise Partial Mapping of Vectors: $(\text{pmap}(f, v, hp))_i = f(v_i, \text{proof})$

Informal description

For any predicate $p$ on elements of type $\alpha$, any function $f \colon (a \colon \alpha) \to p(a) \to \beta$, and any vector $v$ of length $n$ over $\alpha$ where all elements satisfy $p$, the $i$-th element of the partially mapped vector $\text{pmap}(f, v, hp)$ (for $i < n$) is equal to $f$ applied to the $i$-th element of $v$ and the proof that it satisfies $p$. In other words, if $v$ is a vector of length $n$ with $\forall x \in \text{toList}(v), p(x)$, then for any index $i < n$: $$ (\text{pmap}(f, v, hp))[i] = f(v[i], \text{proof that } v[i] \text{ satisfies } p) $$

List.Vector.get_eq_get_toList theorem

(v : Vector α n) (i : Fin n) : v.get i = v.toList.get (Fin.cast v.toList_length.symm i)

Full source

theorem get_eq_get_toList (v : Vector α n) (i : Fin n) :
    v.get i = v.toList.get (Fin.cast v.toList_length.symm i) :=
  rfl

Equality of Vector and List Element Access: $v_i = (\text{toList}(v))_i$

Informal description

For any vector $v$ of type `List.Vector α n` and any index $i$ of type `Fin n`, the $i$-th element of $v$ is equal to the $i$-th element of the underlying list of $v$, where the index is cast using the length equality $|\text{toList}(v)| = n$.

List.Vector.get_replicate theorem

(a : α) (i : Fin n) : (Vector.replicate n a).get i = a

Full source

@[simp]
theorem get_replicate (a : α) (i : Fin n) : (Vector.replicate n a).get i = a := by
  apply List.getElem_replicate

Element Access in Replicated Vector: $(a \text{ replicated } n \text{ times})_i = a$

Informal description

For any element $a$ of type $\alpha$ and any index $i$ in the finite type $\text{Fin}\,n$, the $i$-th element of the vector obtained by replicating $a$ $n$ times is equal to $a$.

List.Vector.get_map theorem

{β : Type*} (v : Vector α n) (f : α → β) (i : Fin n) : (v.map f).get i = f (v.get i)

Full source

@[simp]
theorem get_map {β : Type*} (v : Vector α n) (f : α → β) (i : Fin n) :
    (v.map f).get i = f (v.get i) := by
  cases v; simp [Vector.map, get_eq_get_toList]

Element-wise Mapping of Vectors: $(\text{map}(f, \mathbf{v}))_i = f(v_i)$

Informal description

For any vector $\mathbf{v} \in \text{Vector} \alpha n$, any function $f : \alpha \to \beta$, and any index $i \in \text{Fin}\,n$, the $i$-th element of the mapped vector $\text{map}(f, \mathbf{v})$ is equal to $f$ applied to the $i$-th element of $\mathbf{v}$, i.e., \[ (\text{map}(f, \mathbf{v}))_i = f(v_i). \]

List.Vector.map₂_nil theorem

(f : α → β → γ) : Vector.map₂ f nil nil = nil

Full source

@[simp]
theorem map₂_nil (f : α → β → γ) : Vector.map₂ f nil nil = nil :=
  rfl

Pairwise Mapping Preserves Empty Vectors: $\text{map}_2(f, \text{nil}, \text{nil}) = \text{nil}$

Informal description

For any function $f : \alpha \to \beta \to \gamma$, the pairwise mapping of two empty vectors of type $\alpha$ and $\beta$ results in an empty vector of type $\gamma$, i.e., $\text{map}_2(f, \text{nil}, \text{nil}) = \text{nil}$.

List.Vector.map₂_cons theorem

 (hd₁ : α) (tl₁ : Vector α n) (hd₂ : β) (tl₂ : Vector β n) (f : α → β → γ) :
  Vector.map₂ f (hd₁ ::ᵥ tl₁) (hd₂ ::ᵥ tl₂) = f hd₁ hd₂ ::ᵥ (Vector.map₂ f tl₁ tl₂)

Full source

@[simp]
theorem map₂_cons (hd₁ : α) (tl₁ : Vector α n) (hd₂ : β) (tl₂ : Vector β n) (f : α → β → γ) :
    Vector.map₂ f (hd₁ ::ᵥ tl₁) (hd₂ ::ᵥ tl₂) = f hd₁ hd₂ ::ᵥ (Vector.map₂ f tl₁ tl₂) :=
  rfl

Pairwise Mapping Preserves Vector Cons: $\text{map}_2(f, h_1 :: \mathbf{v}_1, h_2 :: \mathbf{v}_2) = f(h_1, h_2) :: \text{map}_2(f, \mathbf{v}_1, \mathbf{v}_2)$

Informal description

For any function $f : \alpha \to \beta \to \gamma$, elements $h_1 : \alpha$ and $h_2 : \beta$, and vectors $\mathbf{v}_1 : \text{Vector } \alpha n$ and $\mathbf{v}_2 : \text{Vector } \beta n$, the pairwise mapping of the cons-constructed vectors satisfies: \[ \text{map}_2(f, h_1 :: \mathbf{v}_1, h_2 :: \mathbf{v}_2) = f(h_1, h_2) :: \text{map}_2(f, \mathbf{v}_1, \mathbf{v}_2), \] where $::$ denotes the vector cons operation.

List.Vector.get_ofFn theorem

{n} (f : Fin n → α) (i) : get (ofFn f) i = f i

Full source

@[simp]
theorem get_ofFn {n} (f : Fin n → α) (i) : get (ofFn f) i = f i := by
  conv_rhs => erw [← List.get_ofFn f ⟨i, by simp⟩]
  simp only [get_eq_get_toList]
  congr <;> simp [Fin.heq_ext_iff]

Element Access in Vector Construction: $\text{get}(\text{ofFn}(f), i) = f(i)$

Informal description

For any natural number $n$, function $f \colon \mathrm{Fin}\,n \to \alpha$, and index $i \in \mathrm{Fin}\,n$, the $i$-th element of the vector constructed from $f$ via `ofFn` is equal to $f(i)$. In symbols: $\text{get}(\text{ofFn}(f), i) = f(i)$.

List.Vector.ofFn_get theorem

(v : Vector α n) : ofFn (get v) = v

Full source

@[simp]
theorem ofFn_get (v : Vector α n) : ofFn (get v) = v := by
  rcases v with ⟨l, rfl⟩
  apply toList_injective
  dsimp
  simpa only [toList_ofFn] using List.ofFn_get _

Vector Reconstruction from Element Access: $\text{ofFn}(\text{get}\,v) = v$

Informal description

For any vector $v$ of type $\text{Vector}\,\alpha\,n$, the vector constructed from the element-access function $\text{get}\,v$ is equal to $v$ itself. In symbols: $\text{ofFn}(\text{get}\,v) = v$.

Equiv.vectorEquivFin definition

(α : Type*) (n : ℕ) : Vector α n ≃ (Fin n → α)

Full source

/-- The natural equivalence between length-`n` vectors and functions from `Fin n`. -/
def _root_.Equiv.vectorEquivFin (α : Type*) (n : ℕ) : VectorVector α n ≃ (Fin n → α) :=
  ⟨Vector.get, Vector.ofFn, Vector.ofFn_get, fun f => funext <| Vector.get_ofFn f⟩

Equivalence between vectors and functions on finite indices

Informal description

The natural equivalence between the type of vectors of length $n$ over $\alpha$ and the type of functions from $\mathrm{Fin}\,n$ to $\alpha$. Specifically: - The forward direction maps a vector $v$ to the function $i \mapsto v_i$ (the $i$-th element of $v$). - The backward direction constructs a vector from a function $f \colon \mathrm{Fin}\,n \to \alpha$ by setting each element $v_i = f(i)$. - The equivalence is witnessed by the fact that these operations are mutual inverses: constructing a vector from its element-access function returns the original vector, and accessing elements of a vector constructed from a function $f$ recovers $f$. Symbolically, this is expressed as $\text{Vector}\,\alpha\,n \simeq (\mathrm{Fin}\,n \to \alpha)$.

List.Vector.get_tail theorem

(x : Vector α n) (i) : x.tail.get i = x.get ⟨i.1 + 1, by omega⟩

Full source

theorem get_tail (x : Vector α n) (i) : x.tail.get i = x.get ⟨i.1 + 1, by omega⟩ := by
  obtain ⟨i, ih⟩ := i; dsimp
  rcases x with ⟨_ | _, h⟩ <;> try rfl
  rw [List.length] at h
  rw [← h] at ih
  contradiction

Tail Element Correspondence in List-Based Vectors

Informal description

For any vector $x$ of type `List.Vector α n` and any index $i$ of type `Fin (n-1)`, the $i$-th element of the tail of $x$ is equal to the $(i+1)$-th element of $x$. Symbolically: If $x : \text{Vector}\,\alpha\,n$ and $i : \text{Fin}\,(n-1)$, then $\text{get}\,(\text{tail}\,x)\,i = \text{get}\,x\,(i+1)$.

List.Vector.get_tail_succ theorem

: ∀ (v : Vector α n.succ) (i : Fin n), get (tail v) i = get v i.succ

Full source

@[simp]
theorem get_tail_succ : ∀ (v : Vector α n.succ) (i : Fin n), get (tail v) i = get v i.succ
  | ⟨a :: l, e⟩, ⟨i, h⟩ => by simp [get_eq_get_toList]; rfl

Tail Element Correspondence in Vectors: $\text{get}\,(\text{tail}\,v)\,i = \text{get}\,v\,(i+1)$

Informal description

For any vector $v$ of length $n+1$ (where $n$ is a natural number) and any index $i$ of type $\text{Fin}\,n$, the $i$-th element of the tail of $v$ is equal to the $(i+1)$-th element of $v$. Symbolically: If $v : \text{Vector}\,\alpha\,(n+1)$ and $i : \text{Fin}\,n$, then $\text{get}\,(\text{tail}\,v)\,i = \text{get}\,v\,(i+1)$.

List.Vector.tail_val theorem

: ∀ v : Vector α n.succ, v.tail.val = v.val.tail

Full source

@[simp]
theorem tail_val : ∀ v : Vector α n.succ, v.tail.val = v.val.tail
  | ⟨_ :: _, _⟩ => rfl

Tail-List Commutativity for Vectors

Informal description

For any vector $v$ of length $n+1$ (where $n$ is a natural number), the underlying list of the tail of $v$ is equal to the tail of the underlying list of $v$. In other words, if $v$ is represented as a list, then removing the first element of $v$ (to get `v.tail`) is equivalent to first converting $v$ to a list and then removing its first element. Symbolically: If $v : \text{Vector}\,\alpha\,(n+1)$, then $\text{val}(\text{tail}(v)) = \text{tail}(\text{val}(v))$, where $\text{val}$ extracts the underlying list of a vector, and $\text{tail}$ removes the first element of a list or vector.

List.Vector.tail_nil theorem

: (@nil α).tail = nil

Full source

/-- The `tail` of a `nil` vector is `nil`. -/
@[simp]
theorem tail_nil : (@nil α).tail = nil :=
  rfl

Tail of Empty Vector is Empty

Informal description

The tail of the empty vector of type $\alpha$ is itself the empty vector, i.e., $\text{tail}(\text{nil}) = \text{nil}$.

List.Vector.singleton_tail theorem

: ∀ (v : Vector α 1), v.tail = Vector.nil

Full source

/-- The `tail` of a vector made up of one element is `nil`. -/
@[simp]
theorem singleton_tail : ∀ (v : Vector α 1), v.tail = Vector.nil
  | ⟨[_], _⟩ => rfl

Tail of a Singleton Vector is Empty

Informal description

For any vector $v$ of length $1$ over a type $\alpha$, the tail of $v$ is the empty vector of length $0$.

List.Vector.tail_ofFn theorem

{n : ℕ} (f : Fin n.succ → α) : tail (ofFn f) = ofFn fun i => f i.succ

Full source

@[simp]
theorem tail_ofFn {n : ℕ} (f : Fin n.succ → α) : tail (ofFn f) = ofFn fun i => f i.succ :=
  (ofFn_get _).symm.trans <| by
    congr
    funext i
    rw [get_tail, get_ofFn]
    rfl

Tail of Vector Construction from Function: $\text{tail}(\text{ofFn}(f)) = \text{ofFn}(i \mapsto f(i+1))$

Informal description

For any natural number $n$ and any function $f \colon \mathrm{Fin}\,(n+1) \to \alpha$, the tail of the vector constructed from $f$ via `ofFn` is equal to the vector constructed from the function $i \mapsto f(i+1)$. Symbolically: $\text{tail}(\text{ofFn}(f)) = \text{ofFn}(i \mapsto f(i+1))$.

List.Vector.toList_empty theorem

(v : Vector α 0) : v.toList = []

Full source

@[simp]
theorem toList_empty (v : Vector α 0) : v.toList = [] :=
  List.length_eq_zero_iff.mp v.2

Empty Vector Yields Empty List

Informal description

For any vector $v$ of type `List.Vector α 0` (a list-based vector of length 0), the underlying list is empty, i.e., $v.\text{toList} = []$.

List.Vector.toList_singleton theorem

(v : Vector α 1) : v.toList = [v.head]

Full source

/-- The list that makes up a `Vector` made up of a single element,
retrieved via `toList`, is equal to the list of that single element. -/
@[simp]
theorem toList_singleton (v : Vector α 1) : v.toList = [v.head] := by
  rw [← v.cons_head_tail]
  simp only [toList_cons, toList_nil, head_cons, eq_self_iff_true, and_self_iff, singleton_tail]

Singleton Vector's List Representation Equals List of Its Head

Informal description

For any vector $v$ of length $1$ over a type $\alpha$, the underlying list representation of $v$ is equal to the singleton list containing the head element of $v$, i.e., $\text{toList}(v) = [\text{head}(v)]$.

List.Vector.empty_toList_eq_ff theorem

(v : Vector α (n + 1)) : v.toList.isEmpty = false

Full source

@[simp]
theorem empty_toList_eq_ff (v : Vector α (n + 1)) : v.toList.isEmpty = false :=
  match v with
  | ⟨_ :: _, _⟩ => rfl

Non-Empty Underlying List for Non-Zero Length Vector

Informal description

For any vector $v$ of type `List.Vector α (n + 1)` (a list-based vector of length $n + 1$), the underlying list is non-empty, i.e., $v.\text{toList}.\text{isEmpty} = \text{false}$.

List.Vector.not_empty_toList theorem

(v : Vector α (n + 1)) : ¬v.toList.isEmpty

Full source

theorem not_empty_toList (v : Vector α (n + 1)) : ¬v.toList.isEmpty := by
  simp only [empty_toList_eq_ff, Bool.coe_sort_false, not_false_iff]

Non-Empty Underlying List for Non-Zero Length Vector

Informal description

For any vector $v$ of type `List.Vector α (n + 1)` (a list-based vector of length $n + 1$), the underlying list $v.\text{toList}$ is non-empty.

List.Vector.map_id theorem

{n : ℕ} (v : Vector α n) : Vector.map id v = v

Full source

/-- Mapping under `id` does not change a vector. -/
@[simp]
theorem map_id {n : ℕ} (v : Vector α n) : Vector.map id v = v :=
  Vector.eq _ _ (by simp only [List.map_id, Vector.toList_map])

Identity Mapping Preserves Vector

Informal description

For any natural number $n$ and any vector $\mathbf{v} \in \text{Vector} \alpha n$, mapping the identity function over $\mathbf{v}$ yields $\mathbf{v}$ itself, i.e., $\text{map}(\text{id}, \mathbf{v}) = \mathbf{v}$.

List.Vector.nodup_iff_injective_get theorem

{v : Vector α n} : v.toList.Nodup ↔ Function.Injective v.get

Full source

theorem nodup_iff_injective_get {v : Vector α n} : v.toList.Nodup ↔ Function.Injective v.get := by
  obtain ⟨l, hl⟩ := v
  subst hl
  exact List.nodup_iff_injective_get

Equivalence of List Duplicate-Freeness and Injectivity of Vector Element Access

Informal description

For a vector $v$ of type `List.Vector α n` (a list of elements of type $\alpha$ with fixed length $n$), the underlying list $v.\text{toList}$ has no duplicate elements if and only if the element access function $v.\text{get}$ is injective. In other words, the list $v.\text{toList}$ is duplicate-free precisely when the function that retrieves elements from $v$ via their index is injective (i.e., distinct indices correspond to distinct elements).

List.Vector.head?_toList theorem

: ∀ v : Vector α n.succ, (toList v).head? = some (head v)

Full source

theorem head?_toList : ∀ v : Vector α n.succ, (toList v).head? = some (head v)
  | ⟨_ :: _, _⟩ => rfl

Head Option of List Representation Equals Some of Vector Head

Informal description

For any non-empty vector $v$ of type $\text{Vector}\,\alpha\,(n+1)$, the first element of the underlying list $\text{toList}\,v$ is equal to $\text{some}\,(\text{head}\,v)$. In other words, the head option of the list representation of $v$ is the head of $v$ wrapped in a $\text{some}$ constructor.

List.Vector.reverse definition

(v : Vector α n) : Vector α n

Full source

/-- Reverse a vector. -/
def reverse (v : Vector α n) : Vector α n :=
  ⟨v.toList.reverse, by simp⟩

Reversed vector

Informal description

The function reverses the order of elements in a vector $ v $ of type `List.Vector α n`, returning a new vector of the same length $ n $ with the elements in reverse order. The underlying list of the reversed vector is the reverse of the original vector's underlying list.

List.Vector.toList_reverse theorem

{v : Vector α n} : v.reverse.toList = v.toList.reverse

Full source

/-- The `List` of a vector after a `reverse`, retrieved by `toList` is equal
to the `List.reverse` after retrieving a vector's `toList`. -/
theorem toList_reverse {v : Vector α n} : v.reverse.toList = v.toList.reverse :=
  rfl

Reversed Vector's List Equals List's Reverse

Informal description

For any vector $v$ of type `List.Vector α n`, the underlying list of the reversed vector $v.\text{reverse}$ is equal to the reversed list of the underlying list of $v$, i.e., $v.\text{reverse}.\text{toList} = v.\text{toList}.\text{reverse}$.

List.Vector.reverse_reverse theorem

{v : Vector α n} : v.reverse.reverse = v

Full source

@[simp]
theorem reverse_reverse {v : Vector α n} : v.reverse.reverse = v := by
  cases v
  simp [Vector.reverse]

Double Reversal of Vector Yields Original Vector

Informal description

For any vector $v$ of type `List.Vector α n`, reversing the vector twice yields the original vector, i.e., $\text{reverse}(\text{reverse}(v)) = v$.

List.Vector.get_zero theorem

: ∀ v : Vector α n.succ, get v 0 = head v

Full source

@[simp]
theorem get_zero : ∀ v : Vector α n.succ, get v 0 = head v
  | ⟨_ :: _, _⟩ => rfl

First Element Equals Head in Non-Empty Vectors

Informal description

For any vector $v$ of type $\text{Vector}\,\alpha\,(n+1)$, the element at index $0$ is equal to the head of $v$, i.e., $\text{get}\,v\,0 = \text{head}\,v$.

List.Vector.head_ofFn theorem

{n : ℕ} (f : Fin n.succ → α) : head (ofFn f) = f 0

Full source

@[simp]
theorem head_ofFn {n : ℕ} (f : Fin n.succ → α) : head (ofFn f) = f 0 := by
  rw [← get_zero, get_ofFn]

Head of Vector from Function Equals Function at Zero

Informal description

For any natural number $n$ and any function $f \colon \mathrm{Fin}\,(n+1) \to \alpha$, the head of the vector constructed from $f$ via `ofFn` is equal to $f(0)$. In symbols: $\text{head}(\text{ofFn}(f)) = f(0)$.

List.Vector.get_cons_zero theorem

(a : α) (v : Vector α n) : get (a ::ᵥ v) 0 = a

Full source

theorem get_cons_zero (a : α) (v : Vector α n) : get (a ::ᵥ v) 0 = a := by simp [get_zero]

First Element of Prepended Vector Equals Prepended Element

Informal description

For any element $a$ of type $\alpha$ and any vector $v$ of length $n$ over $\alpha$, the first element (at index $0$) of the vector obtained by prepending $a$ to $v$ is equal to $a$, i.e., $\text{get}(a ::ᵥ v, 0) = a$.

List.Vector.get_cons_nil theorem

: ∀ {ix : Fin 1} (x : α), get (x ::ᵥ nil) ix = x

Full source

/-- Accessing the nth element of a vector made up
of one element `x : α` is `x` itself. -/
@[simp]
theorem get_cons_nil : ∀ {ix : Fin 1} (x : α), get (x ::ᵥ nil) ix = x
  | ⟨0, _⟩, _ => rfl

Accessing Any Element of a Singleton Vector Yields the Element

Informal description

For any index $i$ of type $\text{Fin }1$ (the finite type with one element) and any element $x$ of type $\alpha$, accessing the $i$-th element of the vector formed by prepending $x$ to the empty vector (denoted $x ::ᵥ \text{nil}$) yields $x$.

List.Vector.get_cons_succ theorem

(a : α) (v : Vector α n) (i : Fin n) : get (a ::ᵥ v) i.succ = get v i

Full source

@[simp]
theorem get_cons_succ (a : α) (v : Vector α n) (i : Fin n) : get (a ::ᵥ v) i.succ = get v i := by
  rw [← get_tail_succ, tail_cons]

Element Correspondence in Prepended Vector: $\text{get}(a ::ᵥ v, i+1) = \text{get}(v, i)$

Informal description

For any element $a$ of type $\alpha$, any vector $v$ of length $n$ over $\alpha$, and any index $i$ of type $\text{Fin}\,n$, the element at index $i+1$ of the vector obtained by prepending $a$ to $v$ is equal to the element at index $i$ of $v$. Symbolically: $\text{get}(a ::ᵥ v, i+1) = \text{get}(v, i)$.

List.Vector.last definition

(v : Vector α (n + 1)) : α

Full source

/-- The last element of a `Vector`, given that the vector is at least one element. -/
def last (v : Vector α (n + 1)) : α :=
  v.get (Fin.last n)

Last element of a vector

Informal description

For a vector $v$ of type `List.Vector α (n + 1)` (a list of elements of type $\alpha$ with fixed length $n + 1$), the function returns the last element of $v$, which is obtained by accessing the element at the last valid index of the vector.

List.Vector.last_def theorem

{v : Vector α (n + 1)} : v.last = v.get (Fin.last n)

Full source

/-- The last element of a `Vector`, given that the vector is at least one element. -/
theorem last_def {v : Vector α (n + 1)} : v.last = v.get (Fin.last n) :=
  rfl

Last Element of Vector Equals Element at Last Index

Informal description

For any vector $v$ of type `List.Vector α (n + 1)` (a list of elements of type $\alpha$ with fixed length $n + 1$), the last element of $v$ is equal to the element of $v$ at the last valid index (given by `Fin.last n`). That is, $v_{\text{last}} = v_{\text{get}}(\text{last}_n)$, where $\text{last}_n$ denotes the last index in a vector of length $n + 1$.

List.Vector.reverse_get_zero theorem

{v : Vector α (n + 1)} : v.reverse.head = v.last

Full source

/-- The `last` element of a vector is the `head` of the `reverse` vector. -/
theorem reverse_get_zero {v : Vector α (n + 1)} : v.reverse.head = v.last := by
  rw [← get_zero, last_def, get_eq_get_toList, get_eq_get_toList]
  simp_rw [toList_reverse]
  rw [List.get_eq_getElem, List.get_eq_getElem, ← Option.some_inj, Fin.cast, Fin.cast,
    ← List.getElem?_eq_getElem, ← List.getElem?_eq_getElem, List.getElem?_reverse]
  · congr
    simp
  · simp

Head of Reversed Vector Equals Last Element: $\text{head}(v^{\text{rev}}) = \text{last}(v)$

Informal description

For any vector $v$ of type `List.Vector α (n + 1)`, the head of the reversed vector $v^{\text{rev}}$ is equal to the last element of $v$, i.e., $\text{head}(v^{\text{rev}}) = \text{last}(v)$.

List.Vector.scanl definition

: Vector β (n + 1)

Full source

/-- Construct a `Vector β (n + 1)` from a `Vector α n` by scanning `f : β → α → β`
from the "left", that is, from 0 to `Fin.last n`, using `b : β` as the starting value.
-/
def scanl : Vector β (n + 1) :=
  ⟨List.scanl f b v.toList, by rw [List.length_scanl, toList_length]⟩

Left scan of a vector

Informal description

Given a function $f : \beta \to \alpha \to \beta$, an initial value $b : \beta$, and a vector $v$ of type `List.Vector α n`, the function constructs a new vector of type `List.Vector β (n + 1)` by applying $f$ cumulatively from left to right (starting with $b$) to the elements of $v$.

List.Vector.scanl_nil theorem

: scanl f b nil = b ::ᵥ nil

Full source

/-- Providing an empty vector to `scanl` gives the starting value `b : β`. -/
@[simp]
theorem scanl_nil : scanl f b nil = b ::ᵥ nil :=
  rfl

Left Scan of Empty Vector Yields Singleton

Informal description

For any function $f : \beta \to \alpha \to \beta$ and initial value $b : \beta$, the left scan operation applied to the empty vector `nil` results in a singleton vector containing just $b$, i.e., $\text{scanl}(f, b, \text{nil}) = b :: \text{nil}$.

List.Vector.scanl_cons theorem

(x : α) : scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v

Full source

/-- The recursive step of `scanl` splits a vector `x ::ᵥ v : Vector α (n + 1)`
into the provided starting value `b : β` and the recursed `scanl`
`f b x : β` as the starting value.

This lemma is the `cons` version of `scanl_get`.
-/
@[simp]
theorem scanl_cons (x : α) : scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v := by
  simp only [scanl, toList_cons, List.scanl]; dsimp
  simp only [cons]

Recursive Step of Left Scan for Vectors: $\text{scanl}\, f\, b\, (x ::ᵥ v) = b ::ᵥ \text{scanl}\, f\, (f\, b\, x)\, v$

Informal description

For any function $f : \beta \to \alpha \to \beta$, initial value $b : \beta$, element $x : \alpha$, and vector $v$ of type `Vector α n`, the left scan of the vector $x ::ᵥ v$ is given by: $$\text{scanl}\, f\, b\, (x ::ᵥ v) = b ::ᵥ \text{scanl}\, f\, (f\, b\, x)\, v.$$

List.Vector.scanl_val theorem

: ∀ {v : Vector α n}, (scanl f b v).val = List.scanl f b v.val

Full source

/-- The underlying `List` of a `Vector` after a `scanl` is the `List.scanl`
of the underlying `List` of the original `Vector`.
-/
@[simp]
theorem scanl_val : ∀ {v : Vector α n}, (scanl f b v).val = List.scanl f b v.val
  | _ => rfl

Underlying List of Vector Scan Equals List Scan of Underlying List

Informal description

For any function $f : \beta \to \alpha \to \beta$, initial value $b : \beta$, and vector $v$ of type `List.Vector α n`, the underlying list of the left scan of $v$ is equal to the left scan of the underlying list of $v$. That is, $$(\text{scanl}\, f\, b\, v).\text{val} = \text{List.scanl}\, f\, b\, (v.\text{val}).$$

List.Vector.toList_scanl theorem

: (scanl f b v).toList = List.scanl f b v.toList

Full source

/-- The `toList` of a `Vector` after a `scanl` is the `List.scanl`
of the `toList` of the original `Vector`.
-/
@[simp]
theorem toList_scanl : (scanl f b v).toList = List.scanl f b v.toList :=
  rfl

List Representation of Vector Scan: $\text{scanl}\, f\, b\, v$

Informal description

For any function $f : \beta \to \alpha \to \beta$, initial value $b : \beta$, and vector $v$ of type `List.Vector α n`, the underlying list of the left scan of $v$ is equal to the left scan of the underlying list of $v$. That is, $$(\text{scanl}\, f\, b\, v).\text{toList} = \text{List.scanl}\, f\, b\, (v.\text{toList}).$$

List.Vector.scanl_singleton theorem

(v : Vector α 1) : scanl f b v = b ::ᵥ f b v.head ::ᵥ nil

Full source

/-- The recursive step of `scanl` splits a vector made up of a single element
`x ::ᵥ nil : Vector α 1` into a `Vector` of the provided starting value `b : β`
and the mapped `f b x : β` as the last value.
-/
@[simp]
theorem scanl_singleton (v : Vector α 1) : scanl f b v = b ::ᵥ f b v.head ::ᵥ nil := by
  rw [← cons_head_tail v]
  simp only [scanl_cons, scanl_nil, head_cons, singleton_tail]

Left Scan of Singleton Vector: $\text{scanl}\, f\, b\, v = b ::ᵥ f\, b\, (\text{head}\, v) ::ᵥ \text{nil}$

Informal description

For any function $f : \beta \to \alpha \to \beta$, initial value $b : \beta$, and singleton vector $v$ of type `Vector α 1`, the left scan of $v$ is given by: $$\text{scanl}\, f\, b\, v = b ::ᵥ f\, b\, (\text{head}\, v) ::ᵥ \text{nil}.$$

List.Vector.scanl_head theorem

: (scanl f b v).head = b

Full source

/-- The first element of `scanl` of a vector `v : Vector α n`,
retrieved via `head`, is the starting value `b : β`.
-/
@[simp]
theorem scanl_head : (scanl f b v).head = b := by
  cases n
  · have : v = nil := by simp only [eq_iff_true_of_subsingleton]
    simp only [this, scanl_nil, head_cons]
  · rw [← cons_head_tail v]
    simp [← get_zero, get_eq_get_toList]

Head of Left Scan Equals Initial Value: $\text{head}(\text{scanl}\,f\,b\,v) = b$

Informal description

For any function $f : \beta \to \alpha \to \beta$, initial value $b : \beta$, and vector $v : \text{Vector}\,\alpha\,n$, the head of the left scan $\text{scanl}\,f\,b\,v$ is equal to $b$.

List.Vector.scanl_get theorem

(i : Fin n) : (scanl f b v).get i.succ = f ((scanl f b v).get (Fin.castSucc i)) (v.get i)

Full source

/-- For an index `i : Fin n`, the nth element of `scanl` of a
vector `v : Vector α n` at `i.succ`, is equal to the application
function `f : β → α → β` of the `castSucc i` element of
`scanl f b v` and `get v i`.

This lemma is the `get` version of `scanl_cons`.
-/
@[simp]
theorem scanl_get (i : Fin n) :
    (scanl f b v).get i.succ = f ((scanl f b v).get (Fin.castSucc i)) (v.get i) := by
  rcases n with - | n
  · exact i.elim0
  induction' n with n hn generalizing b
  · have i0 : i = 0 := Fin.eq_zero _
    simp [scanl_singleton, i0, get_zero]; simp [get_eq_get_toList, List.get]
  · rw [← cons_head_tail v, scanl_cons, get_cons_succ]
    refine Fin.cases ?_ ?_ i
    · simp only [get_zero, scanl_head, Fin.castSucc_zero, head_cons]
    · intro i'
      simp only [hn, Fin.castSucc_fin_succ, get_cons_succ]

Recursive relation for left scan elements: $(\text{scanl}\,f\,b\,v)_{i+1} = f((\text{scanl}\,f\,b\,v)_i, v_i)$

Informal description

For any function $f : \beta \to \alpha \to \beta$, initial value $b : \beta$, vector $v : \text{Vector}\,\alpha\,n$, and index $i : \text{Fin}\,n$, the $(i+1)$-th element of the left scan $\text{scanl}\,f\,b\,v$ is equal to $f$ applied to the $i$-th element of the scan and the $i$-th element of $v$. More precisely: $$(\text{scanl}\,f\,b\,v).\text{get}(i+1) = f\big((\text{scanl}\,f\,b\,v).\text{get}(i)\big)\,(v.\text{get}(i))$$

List.Vector.mOfFn definition

{m} [Monad m] {α : Type u} : ∀ {n}, (Fin n → m α) → m (Vector α n)

Full source

/-- Monadic analog of `Vector.ofFn`.
Given a monadic function on `Fin n`, return a `Vector α n` inside the monad. -/
def mOfFn {m} [Monad m] {α : Type u} : ∀ {n}, (Fin n → m α) → m (Vector α n)
  | 0, _ => pure nil
  | _ + 1, f => do
    let a ← f 0
    let v ← mOfFn fun i => f i.succ
    pure (a ::ᵥ v)

Monadic vector construction from finite function

Informal description

Given a monad `m`, a type `α`, and a natural number `n`, the function `mOfFn` takes a monadic function `f : Fin n → m α` and returns a monadic computation producing a vector `Vector α n`. For `n = 0`, it returns the empty vector `nil` inside the monad. For `n = k + 1`, it first computes the head element `a` by applying `f` to `0`, then recursively computes the tail vector `v` by applying `f` to the remaining indices, and finally combines them as `a ::ᵥ v` inside the monad.

List.Vector.mOfFn_pure theorem

{m} [Monad m] [LawfulMonad m] {α} : ∀ {n} (f : Fin n → α), (@mOfFn m _ _ _ fun i => pure (f i)) = pure (ofFn f)

Full source

theorem mOfFn_pure {m} [Monad m] [LawfulMonad m] {α} :
    ∀ {n} (f : Fin n → α), (@mOfFn m _ _ _ fun i => pure (f i)) = pure (ofFn f)
  | 0, _ => rfl
  | n + 1, f => by
    rw [mOfFn, @mOfFn_pure m _ _ _ n _, ofFn]
    simp

Monadic Vector Construction Preserves Pure Functions

Informal description

For any monad $m$ that is a lawful monad, any type $\alpha$, and any natural number $n$, given a function $f \colon \mathrm{Fin}\,n \to \alpha$, the monadic vector construction of the function $\lambda i \mapsto \mathrm{pure}(f(i))$ is equal to the pure vector constructed from $f$: \[ \mathrm{mOfFn}\, (\lambda i \mapsto \mathrm{pure}(f(i))) = \mathrm{pure}(\mathrm{ofFn}\, f) \]

List.Vector.mmap definition

{m} [Monad m] {α} {β : Type u} (f : α → m β) : ∀ {n}, Vector α n → m (Vector β n)

Full source

/-- Apply a monadic function to each component of a vector,
returning a vector inside the monad. -/
def mmap {m} [Monad m] {α} {β : Type u} (f : α → m β) : ∀ {n}, Vector α n → m (Vector β n)
  | 0, _ => pure nil
  | _ + 1, xs => do
    let h' ← f xs.head
    let t' ← mmap f xs.tail
    pure (h' ::ᵥ t')

Monadic map over vectors

Informal description

Given a monad `m`, a function `f : α → m β`, and a vector `v : Vector α n`, the function `mmap` applies `f` to each element of `v` and collects the results in the monad `m`, returning a vector `Vector β n` inside the monad. Specifically: - For the empty vector `nil`, it returns `pure nil`. - For a non-empty vector `a ::ᵥ v`, it applies `f` to the head `a`, recursively applies `mmap f` to the tail `v`, and combines the results as `h' ::ᵥ t'` inside the monad.

List.Vector.mmap_nil theorem

{m} [Monad m] {α β} (f : α → m β) : mmap f nil = pure nil

Full source

@[simp]
theorem mmap_nil {m} [Monad m] {α β} (f : α → m β) : mmap f nil = pure nil :=
  rfl

Monadic map preserves the empty vector

Informal description

For any monad $m$ and types $\alpha, \beta$, given a function $f : \alpha \to m \beta$, applying the monadic map operation to the empty vector yields the pure empty vector in the monad: \[ \text{mmap}\, f\, \text{nil} = \text{pure}\, \text{nil} \]

List.Vector.mmap_cons theorem

 {m} [Monad m] {α β} (f : α → m β) (a) :
  ∀ {n} (v : Vector α n),
    mmap f (a ::ᵥ v) = do
      let h' ← f a
      let t' ← mmap f v
      pure (h' ::ᵥ t')

Full source

@[simp]
theorem mmap_cons {m} [Monad m] {α β} (f : α → m β) (a) :
    ∀ {n} (v : Vector α n),
      mmap f (a ::ᵥ v) = do
        let h' ← f a
        let t' ← mmap f v
        pure (h' ::ᵥ t')
  | _, ⟨_, rfl⟩ => rfl

Monadic map distributes over vector cons

Informal description

Let $m$ be a monad, $\alpha$ and $\beta$ types, and $f : \alpha \to m \beta$ a function. For any element $a \in \alpha$ and vector $v$ of length $n$ over $\alpha$, the monadic map operation satisfies: \[ \text{mmap}\, f\, (a ::ᵥ v) = \text{do}\ \begin{cases} h' \leftarrow f\, a \\ t' \leftarrow \text{mmap}\, f\, v \\ \text{pure}\, (h' ::ᵥ t') \end{cases} \] where $::ᵥ$ denotes the vector cons operation.

List.Vector.inductionOn definition

 {C : ∀ {n : ℕ}, Vector α n → Sort*} {n : ℕ} (v : Vector α n) (nil : C nil)
  (cons : ∀ {n : ℕ} {x : α} {w : Vector α n}, C w → C (x ::ᵥ w)) : C v

Full source

/--
Define `C v` by induction on `v : Vector α n`.

This function has two arguments: `nil` handles the base case on `C nil`,
and `cons` defines the inductive step using `∀ x : α, C w → C (x ::ᵥ w)`.

It is used as the default induction principle for the `induction` tactic.
-/
@[elab_as_elim, induction_eliminator]
def inductionOn {C : ∀ {n : ℕ}, Vector α n → Sort*} {n : ℕ} (v : Vector α n)
    (nil : C nil) (cons : ∀ {n : ℕ} {x : α} {w : Vector α n}, C w → C (x ::ᵥ w)) : C v := by
  induction' n with n ih
  · rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
    exact nil
  · rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
    cases v_property
    exact cons (ih ⟨v, (add_left_inj 1).mp v_property⟩)

Induction principle for vectors

Informal description

Given a type $\alpha$ and a natural number $n$, let $C$ be a property depending on vectors of type $\alpha$ and length $n$. For any vector $v : \text{Vector } \alpha n$, the induction principle states that to prove $C(v)$, it suffices to: 1. Prove the base case $C(\text{nil})$ for the empty vector, and 2. For any $x : \alpha$ and any vector $w : \text{Vector } \alpha n$, show that $C(w)$ implies $C(x ::ᵥ w)$ (where $::ᵥ$ denotes vector cons operation). This provides a way to define functions or prove properties by induction on the structure of vectors.

List.Vector.inductionOn_nil theorem

 {C : ∀ {n : ℕ}, Vector α n → Sort*} (nil : C nil) (cons : ∀ {n : ℕ} {x : α} {w : Vector α n}, C w → C (x ::ᵥ w)) :
  Vector.nil.inductionOn nil cons = nil

Full source

@[simp]
theorem inductionOn_nil {C : ∀ {n : ℕ}, Vector α n → Sort*}
    (nil : C nil) (cons : ∀ {n : ℕ} {x : α} {w : Vector α n}, C w → C (x ::ᵥ w)) :
    Vector.nil.inductionOn nil cons = nil :=
  rfl

Base Case of Vector Induction Principle

Informal description

For any type family $C$ depending on vectors of any length, given a proof $\text{nil} : C(\text{nil})$ and an inductive step function $\text{cons}$ that constructs $C(x ::ᵥ w)$ from $C(w)$, applying the induction principle to the empty vector with these arguments yields $\text{nil}$. More formally: Given: - A type family $C$ depending on vectors of any length - A proof $\text{nil} : C(\text{nil})$ - A function $\text{cons}$ that for any $x : \alpha$ and $w : \text{Vector } \alpha n$, takes $C(w)$ to $C(x ::ᵥ w)$ Then: $$\text{nil.inductionOn}(\text{nil}, \text{cons}) = \text{nil}$$

List.Vector.inductionOn_cons theorem

 {C : ∀ {n : ℕ}, Vector α n → Sort*} {n : ℕ} (x : α) (v : Vector α n) (nil : C nil)
  (cons : ∀ {n : ℕ} {x : α} {w : Vector α n}, C w → C (x ::ᵥ w)) :
  (x ::ᵥ v).inductionOn nil cons = cons (v.inductionOn nil cons : C v)

Full source

@[simp]
theorem inductionOn_cons {C : ∀ {n : ℕ}, Vector α n → Sort*} {n : ℕ} (x : α) (v : Vector α n)
    (nil : C nil) (cons : ∀ {n : ℕ} {x : α} {w : Vector α n}, C w → C (x ::ᵥ w)) :
    (x ::ᵥ v).inductionOn nil cons = cons (v.inductionOn nil cons : C v) :=
  rfl

Induction Computation for Non-Empty Vectors

Informal description

For any type $\alpha$, natural number $n$, element $x : \alpha$, vector $v : \text{Vector } \alpha n$, property $C$ on vectors, base case proof $\text{nil} : C(\text{nil})$, and inductive step function $\text{cons}$ that constructs $C(x ::ᵥ w)$ from $C(w)$, the induction principle applied to the vector $x ::ᵥ v$ with these arguments equals $\text{cons}$ applied to the induction principle applied to $v$. More formally: Given: - A type family $C$ depending on vectors of any length - A vector $v : \text{Vector } \alpha n$ - A proof $\text{nil} : C(\text{nil})$ - A function $\text{cons}$ that for any $x' : \alpha$ and $w : \text{Vector } \alpha n'$, takes $C(w)$ to $C(x' ::ᵥ w)$ Then: $$(x ::ᵥ v).\text{inductionOn}(\text{nil}, \text{cons}) = \text{cons}(v.\text{inductionOn}(\text{nil}, \text{cons}))$$

List.Vector.inductionOn₂ definition

 {C : ∀ {n}, Vector α n → Vector β n → Sort*} (v : Vector α n) (w : Vector β n) (nil : C nil nil)
  (cons : ∀ {n a b} {x : Vector α n} {y}, C x y → C (a ::ᵥ x) (b ::ᵥ y)) : C v w

Full source

/-- Define `C v w` by induction on a pair of vectors `v : Vector α n` and `w : Vector β n`. -/
@[elab_as_elim]
def inductionOn₂ {C : ∀ {n}, Vector α n → Vector β n → Sort*}
    (v : Vector α n) (w : Vector β n)
    (nil : C nil nil) (cons : ∀ {n a b} {x : Vector α n} {y}, C x y → C (a ::ᵥ x) (b ::ᵥ y)) :
    C v w := by
  induction' n with n ih
  · rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
    rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
    exact nil
  · rcases v with ⟨_ | ⟨a, v⟩, v_property⟩
    cases v_property
    rcases w with ⟨_ | ⟨b, w⟩, w_property⟩
    cases w_property
    apply @cons n _ _ ⟨v, (add_left_inj 1).mp v_property⟩ ⟨w, (add_left_inj 1).mp w_property⟩
    apply ih

Double vector induction principle

Informal description

Given a type family $C$ depending on pairs of vectors of the same length, two vectors $v : \text{Vector} \alpha n$ and $w : \text{Vector} \beta n$, a base case $C(\text{nil}, \text{nil})$, and an inductive step that constructs $C(a ::ᵥ x, b ::ᵥ y)$ from $C(x, y)$, the function $\text{inductionOn}_2$ constructs an element of $C(v, w)$ by induction on the vectors.

List.Vector.inductionOn₃ definition

 {C : ∀ {n}, Vector α n → Vector β n → Vector γ n → Sort*} (u : Vector α n) (v : Vector β n) (w : Vector γ n)
  (nil : C nil nil nil) (cons : ∀ {n a b c} {x : Vector α n} {y z}, C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)) : C u v w

Full source

/-- Define `C u v w` by induction on a triplet of vectors
`u : Vector α n`, `v : Vector β n`, and `w : Vector γ b`. -/
@[elab_as_elim]
def inductionOn₃ {C : ∀ {n}, Vector α n → Vector β n → Vector γ n → Sort*}
    (u : Vector α n) (v : Vector β n) (w : Vector γ n) (nil : C nil nil nil)
    (cons : ∀ {n a b c} {x : Vector α n} {y z}, C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)) :
    C u v w := by
  induction' n with n ih
  · rcases u with ⟨_ | ⟨-, -⟩, - | -⟩
    rcases v with ⟨_ | ⟨-, -⟩, - | -⟩
    rcases w with ⟨_ | ⟨-, -⟩, - | -⟩
    exact nil
  · rcases u with ⟨_ | ⟨a, u⟩, u_property⟩
    cases u_property
    rcases v with ⟨_ | ⟨b, v⟩, v_property⟩
    cases v_property
    rcases w with ⟨_ | ⟨c, w⟩, w_property⟩
    cases w_property
    apply
      @cons n _ _ _ ⟨u, (add_left_inj 1).mp u_property⟩ ⟨v, (add_left_inj 1).mp v_property⟩
        ⟨w, (add_left_inj 1).mp w_property⟩
    apply ih

Triple vector induction principle

Informal description

Given a type family $C$ depending on triplets of vectors of the same length, three vectors $u : \text{Vector} \alpha n$, $v : \text{Vector} \beta n$, and $w : \text{Vector} \gamma n$, a base case $C(\text{nil}, \text{nil}, \text{nil})$, and an inductive step that constructs $C(a ::ᵥ x, b ::ᵥ y, c ::ᵥ z)$ from $C(x, y, z)$, the function $\text{inductionOn}_3$ constructs an element of $C(u, v, w)$ by induction on the vectors.

List.Vector.casesOn definition

 {motive : ∀ {n}, Vector α n → Sort*} (v : Vector α m) (nil : motive nil)
  (cons : ∀ {n}, (hd : α) → (tl : Vector α n) → motive (Vector.cons hd tl)) : motive v

Full source

/-- Define `motive v` by case-analysis on `v : Vector α n`. -/
def casesOn {motive : ∀ {n}, Vector α n → Sort*} (v : Vector α m)
    (nil : motive nil)
    (cons : ∀ {n}, (hd : α) → (tl : Vector α n) → motive (Vector.cons hd tl)) :
    motive v :=
  inductionOn (C := motive) v nil @fun _ hd tl _ => cons hd tl

Vector case analysis principle

Informal description

Given a type family `motive` depending on vectors of type $\alpha$ and length $n$, a vector $v : \text{Vector } \alpha m$, a base case `motive nil` for the empty vector, and a step function that constructs `motive (hd ::ᵥ tl)` from any element $hd : \alpha$ and vector $tl : \text{Vector } \alpha n$, the function `casesOn` constructs an element of `motive v` by case analysis on the vector.

List.Vector.casesOn₂ definition

 {motive : ∀ {n}, Vector α n → Vector β n → Sort*} (v₁ : Vector α m) (v₂ : Vector β m) (nil : motive nil nil)
  (cons : ∀ {n}, (x : α) → (y : β) → (xs : Vector α n) → (ys : Vector β n) → motive (x ::ᵥ xs) (y ::ᵥ ys)) :
  motive v₁ v₂

Full source

/-- Define `motive v₁ v₂` by case-analysis on `v₁ : Vector α n` and `v₂ : Vector β n`. -/
def casesOn₂ {motive : ∀ {n}, Vector α n → Vector β n → Sort*} (v₁ : Vector α m) (v₂ : Vector β m)
    (nil : motive nil nil)
    (cons : ∀ {n}, (x : α) → (y : β) → (xs : Vector α n) → (ys : Vector β n)
      → motive (x ::ᵥ xs) (y ::ᵥ ys)) :
    motive v₁ v₂ :=
  inductionOn₂ (C := motive) v₁ v₂ nil @fun _ x y xs ys _ => cons x y xs ys

Double vector case analysis principle

Informal description

Given a type family `motive` depending on pairs of vectors of the same length, two vectors `v₁ : Vector α m` and `v₂ : Vector β m`, a base case `motive nil nil`, and an inductive step that constructs `motive (x ::ᵥ xs) (y ::ᵥ ys)` for any elements `x : α`, `y : β` and vectors `xs`, `ys` of length `n`, the function `casesOn₂` constructs an element of `motive v₁ v₂` by case analysis on the vectors.

List.Vector.casesOn₃ definition

 {motive : ∀ {n}, Vector α n → Vector β n → Vector γ n → Sort*} (v₁ : Vector α m) (v₂ : Vector β m) (v₃ : Vector γ m)
  (nil : motive nil nil nil)
  (cons :
    ∀ {n},
      (x : α) →
        (y : β) →
          (z : γ) →
            (xs : Vector α n) → (ys : Vector β n) → (zs : Vector γ n) → motive (x ::ᵥ xs) (y ::ᵥ ys) (z ::ᵥ zs)) :
  motive v₁ v₂ v₃

Full source

/-- Define `motive v₁ v₂ v₃` by case-analysis on `v₁ : Vector α n`, `v₂ : Vector β n`, and
    `v₃ : Vector γ n`. -/
def casesOn₃ {motive : ∀ {n}, Vector α n → Vector β n → Vector γ n → Sort*} (v₁ : Vector α m)
    (v₂ : Vector β m) (v₃ : Vector γ m) (nil : motive nil nil nil)
    (cons : ∀ {n}, (x : α) → (y : β) → (z : γ) → (xs : Vector α n) → (ys : Vector β n)
      → (zs : Vector γ n) → motive (x ::ᵥ xs) (y ::ᵥ ys) (z ::ᵥ zs)) :
    motive v₁ v₂ v₃ :=
  inductionOn₃ (C := motive) v₁ v₂ v₃ nil @fun _ x y z xs ys zs _ => cons x y z xs ys zs

Triple vector case analysis principle

Informal description

Given a type family `motive` depending on triplets of vectors of the same length, three vectors `v₁ : Vector α m`, `v₂ : Vector β m`, and `v₃ : Vector γ m`, a base case `motive nil nil nil`, and an inductive step that constructs `motive (x ::ᵥ xs) (y ::ᵥ ys) (z ::ᵥ zs)` for any elements `x : α`, `y : β`, `z : γ` and vectors `xs`, `ys`, `zs` of length `n`, the function `casesOn₃` constructs an element of `motive v₁ v₂ v₃` by case analysis on the vectors.

List.Vector.toArray definition

: Vector α n → Array α

Full source

/-- Cast a vector to an array. -/
def toArray : Vector α n → Array α
  | ⟨xs, _⟩ => cast (by rfl) xs.toArray

Conversion from vector to array

Informal description

The function converts a vector (a list of elements of type $\alpha$ with fixed length $n$) into an array of elements of the same type.

List.Vector.insertIdx definition

(a : α) (i : Fin (n + 1)) (v : Vector α n) : Vector α (n + 1)

Full source

/-- `v.insertIdx a i` inserts `a` into the vector `v` at position `i`
(and shifting later components to the right). -/
def insertIdx (a : α) (i : Fin (n + 1)) (v : Vector α n) : Vector α (n + 1) :=
  ⟨v.1.insertIdx i a, by
    rw [List.length_insertIdx, v.2]
    split <;> omega⟩

Insert element into vector at specified index

Informal description

For a vector $ v $ of length $ n $ over a type $ \alpha $, an element $ a $ of type $ \alpha $, and an index $ i $ (where $ 0 \leq i \leq n $), the operation `insertIdx` inserts $ a $ into $ v $ at position $ i $, shifting all subsequent elements to the right, resulting in a new vector of length $ n + 1 $.

List.Vector.insertIdx_val theorem

{i : Fin (n + 1)} {v : Vector α n} : (v.insertIdx a i).val = v.val.insertIdx i.1 a

Full source

theorem insertIdx_val {i : Fin (n + 1)} {v : Vector α n} :
    (v.insertIdx a i).val = v.val.insertIdx i.1 a :=
  rfl

Underlying List Preservation under Element Insertion in Vectors

Informal description

For any vector $v$ of length $n$ over a type $\alpha$, any element $a$ of type $\alpha$, and any index $i$ (where $0 \leq i \leq n$), the underlying list of the vector obtained by inserting $a$ at index $i$ is equal to the list obtained by inserting $a$ at position $i$ in the underlying list of $v$. That is, $(v.\text{insertIdx}\ a\ i).\text{val} = v.\text{val}.\text{insertIdx}\ i\ a$.

List.Vector.eraseIdx_val theorem

{i : Fin n} : ∀ {v : Vector α n}, (eraseIdx i v).val = v.val.eraseIdx i

Full source

@[simp]
theorem eraseIdx_val {i : Fin n} : ∀ {v : Vector α n}, (eraseIdx i v).val = v.val.eraseIdx i
  | _ => rfl

Underlying List Preservation under Element Removal in Vectors

Informal description

For any vector $v$ of length $n$ over a type $\alpha$ and any index $i < n$, the underlying list of the vector obtained by removing the element at index $i$ is equal to the list obtained by removing the element at index $i$ from the underlying list of $v$. In other words, $(v \setminus i).\text{val} = v.\text{val} \setminus i$.

List.Vector.eraseIdx_insertIdx theorem

{v : Vector α n} {i : Fin (n + 1)} : eraseIdx i (insertIdx a i v) = v

Full source

theorem eraseIdx_insertIdx {v : Vector α n} {i : Fin (n + 1)} :
    eraseIdx i (insertIdx a i v) = v :=
  Subtype.eq (List.eraseIdx_insertIdx ..)

Insertion Followed by Deletion at Same Index Yields Original Vector

Informal description

For any vector $v$ of length $n$ over a type $\alpha$, any element $a$ of type $\alpha$, and any index $i$ (where $0 \leq i \leq n$), removing the element at index $i$ from the vector obtained by inserting $a$ at index $i$ into $v$ yields the original vector $v$. That is, $\text{eraseIdx}\ i\ (\text{insertIdx}\ a\ i\ v) = v$.

List.Vector.eraseIdx_insertIdx' theorem

 {v : Vector α (n + 1)} :
  ∀ {i : Fin (n + 1)} {j : Fin (n + 2)},
    eraseIdx (j.succAbove i) (insertIdx a j v) = insertIdx a (i.predAbove j) (eraseIdx i v)

Full source

/-- Erasing an element after inserting an element, at different indices. -/
theorem eraseIdx_insertIdx' {v : Vector α (n + 1)} :
    ∀ {i : Fin (n + 1)} {j : Fin (n + 2)},
      eraseIdx (j.succAbove i) (insertIdx a j v) = insertIdx a (i.predAbove j) (eraseIdx i v)
  | ⟨i, hi⟩, ⟨j, hj⟩ => by
    dsimp [insertIdx, eraseIdx, Fin.succAbove, Fin.predAbove]
    rw [Subtype.mk_eq_mk]
    simp only [Fin.lt_iff_val_lt_val]
    split_ifs with hij
    · rcases Nat.exists_eq_succ_of_ne_zero
        (Nat.pos_iff_ne_zero.1 (lt_of_le_of_lt (Nat.zero_le _) hij)) with ⟨j, rfl⟩
      rw [← List.insertIdx_eraseIdx_of_ge]
      · simp; rfl
      · simpa
      · simpa [Nat.lt_succ_iff] using hij
    · dsimp
      rw [← List.insertIdx_eraseIdx_of_le]
      · rfl
      · simpa
      · simpa [not_lt] using hij

Commutativity of Insertion and Deletion at Different Indices in Vectors

Informal description

For any vector $v$ of length $n+1$ over a type $\alpha$, any element $a$ of type $\alpha$, and any indices $i < n+1$ and $j < n+2$, the following equality holds: \[ \text{eraseIdx}\ (j.\text{succAbove}\ i)\ (\text{insertIdx}\ a\ j\ v) = \text{insertIdx}\ a\ (i.\text{predAbove}\ j)\ (\text{eraseIdx}\ i\ v) \] Here: - $\text{eraseIdx}\ i\ v$ removes the element at index $i$ from $v$, resulting in a vector of length $n$. - $\text{insertIdx}\ a\ j\ v$ inserts $a$ into $v$ at index $j$, resulting in a vector of length $n+2$. - $j.\text{succAbove}\ i$ embeds $i$ into $\text{Fin}(n+2)$ with a "hole" at $j$. - $i.\text{predAbove}\ j$ adjusts $j$ based on the relationship between $i$ and $j$.

List.Vector.insertIdx_comm theorem

 (a b : α) (i j : Fin (n + 1)) (h : i ≤ j) :
  ∀ v : Vector α n, (v.insertIdx a i).insertIdx b j.succ = (v.insertIdx b j).insertIdx a (Fin.castSucc i)

Full source

theorem insertIdx_comm (a b : α) (i j : Fin (n + 1)) (h : i ≤ j) :
    ∀ v : Vector α n,
      (v.insertIdx a i).insertIdx b j.succ = (v.insertIdx b j).insertIdx a (Fin.castSucc i)
  | ⟨l, hl⟩ => by
    refine Subtype.eq ?_
    simp only [insertIdx_val, Fin.val_succ, Fin.castSucc, Fin.coe_castAdd]
    apply List.insertIdx_comm
    · assumption
    · rw [hl]
      exact Nat.le_of_succ_le_succ j.2

Commutativity of Insertions in Vector at Different Indices

Informal description

For any vector $v$ of length $n$ over a type $\alpha$, any two elements $a, b \in \alpha$, and any two indices $i, j$ (where $0 \leq i \leq j \leq n$), inserting $a$ at index $i$ and then inserting $b$ at the successor of index $j$ is equivalent to first inserting $b$ at index $j$ and then inserting $a$ at the cast successor of index $i$. Symbolically: $(v.\text{insertIdx}(a, i)).\text{insertIdx}(b, j+1) = (v.\text{insertIdx}(b, j)).\text{insertIdx}(a, \text{castSucc}(i))$.

List.Vector.set definition

(v : Vector α n) (i : Fin n) (a : α) : Vector α n

Full source

/-- `set v n a` replaces the `n`th element of `v` with `a`. -/
def set (v : Vector α n) (i : Fin n) (a : α) : Vector α n :=
  ⟨v.1.set i.1 a, by simp⟩

Vector element replacement

Informal description

For a vector `v` of length `n` with elements of type `α`, an index `i` within the range `[0, n-1]`, and an element `a` of type `α`, the function `set` replaces the element at position `i` in `v` with `a`, returning a new vector of the same length.

List.Vector.toList_set theorem

(v : Vector α n) (i : Fin n) (a : α) : (v.set i a).toList = v.toList.set i a

Full source

@[simp]
theorem toList_set (v : Vector α n) (i : Fin n) (a : α) :
    (v.set i a).toList = v.toList.set i a :=
  rfl

Commutativity of Vector Element Setting with List Conversion

Informal description

For a vector $v$ of length $n$ with elements of type $\alpha$, an index $i$ within the range $[0, n-1]$, and an element $a$ of type $\alpha$, the underlying list of the vector obtained by setting the $i$-th element to $a$ is equal to the list obtained by setting the $i$-th element of $v$'s underlying list to $a$. In other words, the operation of setting an element in the vector commutes with converting the vector to a list. Symbolically: $\text{toList}(v.\text{set}(i, a)) = (\text{toList}(v)).\text{set}(i, a)$.

List.Vector.get_set_same theorem

(v : Vector α n) (i : Fin n) (a : α) : (v.set i a).get i = a

Full source

@[simp]
theorem get_set_same (v : Vector α n) (i : Fin n) (a : α) : (v.set i a).get i = a := by
  cases v; cases i; simp [Vector.set, get_eq_get_toList]

Vector Element Update at Index $i$ Yields $a$ at $i$

Informal description

For a vector $v$ of length $n$ with elements of type $\alpha$, an index $i$ in $\{0, \dots, n-1\}$, and an element $a$ of type $\alpha$, the $i$-th element of the vector obtained by setting the $i$-th element to $a$ is equal to $a$. Symbolically: $(v.\text{set}(i, a)).\text{get}(i) = a$.

List.Vector.get_set_of_ne theorem

{v : Vector α n} {i j : Fin n} (h : i ≠ j) (a : α) : (v.set i a).get j = v.get j

Full source

theorem get_set_of_ne {v : Vector α n} {i j : Fin n} (h : i ≠ j) (a : α) :
    (v.set i a).get j = v.get j := by
  cases v; cases i; cases j
  simp only [get_eq_get_toList, toList_set, toList_mk, Fin.cast_mk, List.get_eq_getElem]
  rw [List.getElem_set_of_ne]
  · simpa using h

Vector Element Update Preserves Other Elements: $(v[i \mapsto a])_j = v_j$ for $i \neq j$

Informal description

For a vector $v$ of length $n$ with elements of type $\alpha$, distinct indices $i$ and $j$ in $\{0, \dots, n-1\}$, and an element $a$ of type $\alpha$, the $j$-th element of the vector obtained by setting the $i$-th element to $a$ is equal to the original $j$-th element of $v$. Symbolically: $(v.\text{set}(i, a)).\text{get}(j) = v.\text{get}(j)$ when $i \neq j$.

List.Vector.get_set_eq_if theorem

{v : Vector α n} {i j : Fin n} (a : α) : (v.set i a).get j = if i = j then a else v.get j

Full source

theorem get_set_eq_if {v : Vector α n} {i j : Fin n} (a : α) :
    (v.set i a).get j = if i = j then a else v.get j := by
  split_ifs <;> (try simp [*]); rwa [get_set_of_ne]

Conditional Vector Element Update: $(v[i \mapsto a])_j = a$ if $i = j$, else $v_j$

Informal description

For a vector $v$ of length $n$ with elements of type $\alpha$, indices $i$ and $j$ in $\{0, \dots, n-1\}$, and an element $a$ of type $\alpha$, the $j$-th element of the vector obtained by setting the $i$-th element to $a$ is equal to $a$ if $i = j$, and is equal to the original $j$-th element of $v$ otherwise. Symbolically: $(v.\text{set}(i, a)).\text{get}(j) = \begin{cases} a & \text{if } i = j, \\ v.\text{get}(j) & \text{otherwise.} \end{cases}$

List.Vector.prod_set theorem

 [Monoid α] (v : Vector α n) (i : Fin n) (a : α) :
  (v.set i a).toList.prod = (v.take i).toList.prod * a * (v.drop (i + 1)).toList.prod

Full source

@[to_additive]
theorem prod_set [Monoid α] (v : Vector α n) (i : Fin n) (a : α) :
    (v.set i a).toList.prod = (v.take i).toList.prod * a * (v.drop (i + 1)).toList.prod := by
  refine (List.prod_set v.toList i a).trans ?_
  simp_all

Product of Vector After Replacement in Monoid: $\prod \text{set}(v, i, a) = (\prod \text{take}(i, v)) \cdot a \cdot (\prod \text{drop}(i+1, v))$

Informal description

Let $\alpha$ be a monoid, $v$ be a vector of length $n$ with elements in $\alpha$, $i$ be an index in $\{0, \dots, n-1\}$, and $a$ be an element of $\alpha$. Then the product of the elements in the vector obtained by replacing the $i$-th element of $v$ with $a$ is equal to the product of the elements in the prefix of $v$ up to index $i$, multiplied by $a$, and then multiplied by the product of the elements in the suffix of $v$ starting from index $i+1$. Symbolically: \[ \prod \left(\text{set}(v, i, a)\right) = \left(\prod \text{take}(i, v)\right) \cdot a \cdot \left(\prod \text{drop}(i+1, v)\right). \]

List.Vector.prod_set' theorem

[CommGroup α] (v : Vector α n) (i : Fin n) (a : α) : (v.set i a).toList.prod = v.toList.prod * (v.get i)⁻¹ * a

Full source

/-- Variant of `List.Vector.prod_set` that multiplies by the inverse of the replaced element -/
@[to_additive
  "Variant of `List.Vector.sum_set` that subtracts the inverse of the replaced element"]
theorem prod_set' [CommGroup α] (v : Vector α n) (i : Fin n) (a : α) :
    (v.set i a).toList.prod = v.toList.prod * (v.get i)⁻¹ * a := by
  refine (List.prod_set' v.toList i a).trans ?_
  simp [get_eq_get_toList, mul_assoc]

Product of Vector After Replacement in Commutative Group: $\prod \text{set}(v, i, a) = (\prod v) \cdot v_i^{-1} \cdot a$

Informal description

Let $\alpha$ be a commutative group, $v$ be a vector of length $n$ with elements in $\alpha$, $i$ be an index in $\{0, \dots, n-1\}$, and $a$ be an element of $\alpha$. Then the product of the elements in the vector obtained by replacing the $i$-th element of $v$ with $a$ is equal to the product of the original vector's elements multiplied by the inverse of the replaced element and the new element $a$, i.e., \[ \prod \left(\text{set}(v, i, a)\right) = \left(\prod v\right) \cdot (v_i)^{-1} \cdot a. \]

List.Vector.traverse definition

{α β : Type u} (f : α → F β) : Vector α n → F (Vector β n)

Full source

/-- Apply an applicative function to each component of a vector. -/
protected def traverse {α β : Type u} (f : α → F β) : Vector α n → F (Vector β n)
  | ⟨v, Hv⟩ => cast (by rw [Hv]) <| traverseAux f v

Applicative traversal of a vector

Informal description

Given an applicative functor `F`, a function `f : α → F β`, and a vector `v : Vector α n`, the function `traverse` applies `f` to each element of `v` and collects the results into a new vector `Vector β n` inside the applicative functor `F`.

List.Vector.traverse_def theorem

(f : α → F β) (x : α) : ∀ xs : Vector α n, (x ::ᵥ xs).traverse f = cons <$> f x <*> xs.traverse f

Full source

@[simp]
protected theorem traverse_def (f : α → F β) (x : α) :
    ∀ xs : Vector α n, (x ::ᵥ xs).traverse f = conscons <$> f xcons <$> f x <*> xs.traverse f := by
  rintro ⟨xs, rfl⟩; rfl

Traversal of Cons Vector in Applicative Functor: $(x ::ᵥ \text{xs}).\text{traverse} f = \text{cons} <$> f x <*> \text{xs.traverse} f$

Informal description

For any applicative functor $F$, function $f : \alpha \to F \beta$, element $x : \alpha$, and vector $\text{xs} : \text{Vector} \alpha n$, the traversal of the vector $x ::ᵥ \text{xs}$ with $f$ is equal to applying the vector cons operation inside the functor, where $f x$ provides the head and $\text{xs.traverse} f$ provides the tail.

List.Vector.id_traverse theorem

: ∀ x : Vector α n, x.traverse (pure : _ → Id _) = x

Full source

protected theorem id_traverse : ∀ x : Vector α n, x.traverse (pure : _ → Id _) = x := by
  rintro ⟨x, rfl⟩; dsimp [Vector.traverse, cast]
  induction' x with x xs IH; · rfl
  simp! [IH]; rfl

Identity Traversal Preserves Vector

Informal description

For any vector $x$ of length $n$ over type $\alpha$, traversing $x$ with the identity function (using the identity monad `Id`) returns $x$ unchanged.

List.Vector.comp_traverse theorem

 (f : β → F γ) (g : α → G β) (x : Vector α n) :
  Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) x = Comp.mk (Vector.traverse f <$> Vector.traverse g x)

Full source

@[nolint unusedArguments]
protected theorem comp_traverse (f : β → F γ) (g : α → G β) (x : Vector α n) :
    Vector.traverse (Comp.mkComp.mk ∘ Functor.map f ∘ g) x =
      Comp.mk (Vector.traverseVector.traverse f <$> Vector.traverse g x) := by
  induction' x with n x xs ih
  · simp! [cast, *, functor_norm]
    rfl
  · rw [Vector.traverse_def, ih]
    simp [functor_norm, Function.comp_def]

Composition Law for Vector Traversal: $\text{traverse}(f \circ g) = \text{Comp.mk} (\text{traverse} f <$> \text{traverse} g)$

Informal description

For any applicative functors $F$ and $G$, functions $f : \beta \to F \gamma$ and $g : \alpha \to G \beta$, and vector $x : \text{Vector} \alpha n$, the traversal of $x$ with the composition $\text{Comp.mk} \circ \text{Functor.map} f \circ g$ is equal to the composition of traversals: $$ \text{Vector.traverse} (\text{Comp.mk} \circ \text{Functor.map} f \circ g) \, x = \text{Comp.mk} (\text{Vector.traverse} f <$> \text{Vector.traverse} g \, x) $$ where $\text{Comp.mk}$ constructs a composition of functors and `<$>` is the applicative mapping operation.

List.Vector.traverse_eq_map_id theorem

{α β} (f : α → β) : ∀ x : Vector α n, x.traverse ((pure : _ → Id _) ∘ f) = (pure : _ → Id _) (map f x)

Full source

protected theorem traverse_eq_map_id {α β} (f : α → β) :
    ∀ x : Vector α n, x.traverse ((pure : _ → Id _) ∘ f) = (pure : _ → Id _) (map f x) := by
  rintro ⟨x, rfl⟩; simp!; induction x <;> simp! [*, functor_norm] <;> rfl

Traversal-Map Identity for Vectors

Informal description

For any function $f : \alpha \to \beta$ and any vector $x$ of length $n$ over $\alpha$, traversing $x$ with the composition of $f$ and the identity monad's `pure` is equivalent to applying `pure` to the result of mapping $f$ over $x$. In other words, the following equality holds for all $x \in \text{Vector} \alpha n$: $$ \text{traverse} (\text{pure} \circ f) \, x = \text{pure} (\text{map} \, f \, x) $$ where $\text{pure}$ is the identity monad's embedding and $\text{map}$ applies $f$ element-wise to the vector.

List.Vector.naturality theorem

{α β : Type u} (f : α → F β) (x : Vector α n) : η (x.traverse f) = x.traverse (@η _ ∘ f)

Full source

protected theorem naturality {α β : Type u} (f : α → F β) (x : Vector α n) :
    η (x.traverse f) = x.traverse (@η _ ∘ f) := by
  induction' x with n x xs ih
  · simp! [functor_norm, cast, η.preserves_pure]
  · rw [Vector.traverse_def, Vector.traverse_def, ← ih, η.preserves_seq, η.preserves_map]
    rfl

Naturality of Vector Traversal under Applicative Transformations

Informal description

Let $F$ and $G$ be applicative functors and $\eta : F \to G$ be an applicative transformation. For any function $f : \alpha \to F \beta$ and any vector $x$ of length $n$ over $\alpha$, the following diagram commutes: $$ \eta(x.\text{traverse} f) = x.\text{traverse} (\eta \circ f) $$ where $\text{traverse}$ denotes the applicative traversal operation on vectors.

List.Vector.instTraversableFlipNat instance

: Traversable.{u} (flip Vector n)

Full source

instance : Traversable.{u} (flip Vector n) where
  traverse := @Vector.traverse n
  map {α β} := @Vector.map.{u, u} α β n

Traversable Structure on Fixed-Length Vectors

Informal description

For any type $\alpha$ and natural number $n$, the type of vectors (lists of fixed length $n$) over $\alpha$ forms a traversable functor. This means that for any applicative functor $F$ and function $f : \alpha \to F \beta$, we can apply $f$ to each element of a vector $v : \text{Vector} \alpha n$ and collect the results into a new vector $\text{Vector} \beta n$ inside $F$.

List.Vector.instLawfulTraversableFlipNat instance

: LawfulTraversable.{u} (flip Vector n)

Full source

instance : LawfulTraversable.{u} (flip Vector n) where
  id_traverse := @Vector.id_traverse n
  comp_traverse := Vector.comp_traverse
  traverse_eq_map_id := @Vector.traverse_eq_map_id n
  naturality := Vector.naturality
  id_map := by intro _ x; cases x; simp! [(· <$> ·)]
  comp_map := by intro _ _ _ _ _ x; cases x; simp! [(· <$> ·)]
  map_const := rfl

Lawful Traversable Structure on Fixed-Length Vectors

Informal description

For any type $\alpha$ and natural number $n$, the traversable functor structure on the type of vectors (lists of fixed length $n$) over $\alpha$ is lawful. This means that the `traverse` operation satisfies the identity preservation law, composition law, and naturality conditions required for a lawful traversable functor.

List.Vector.replicate_succ theorem

(val : α) : replicate (n + 1) val = val ::ᵥ (replicate n val)

Full source

@[simp]
theorem replicate_succ (val : α) :
    replicate (n+1) val = val ::ᵥ (replicate n val) :=
  rfl

Recursive construction of replicated vector: $\text{replicate}(n+1, a) = a ::ᵥ \text{replicate}(n, a)$

Informal description

For any element $a$ of type $\alpha$ and natural number $n$, the vector formed by repeating $a$ $n+1$ times is equal to the vector obtained by prepending $a$ to the vector formed by repeating $a$ $n$ times. That is, $\text{replicate}(n+1, a) = a ::ᵥ \text{replicate}(n, a)$.

List.Vector.get_append_cons_zero theorem

: get (append (x ::ᵥ xs) ys) 0 = x

Full source

@[simp] lemma get_append_cons_zero : get (append (x ::ᵥ xs) ys) 0 = x := rfl

First element of concatenated vector with cons

Informal description

For any element $x$ of type $\alpha$, vector $xs$ of length $n$ over $\alpha$, and vector $ys$ of length $m$ over $\alpha$, the first element of the concatenation of the vector $x ::ᵥ xs$ with $ys$ is equal to $x$.

List.Vector.get_append_cons_succ theorem

{i : Fin (n + m)} {h} : get (append (x ::ᵥ xs) ys) ⟨i + 1, h⟩ = get (append xs ys) i

Full source

@[simp]
theorem get_append_cons_succ {i : Fin (n + m)} {h} :
    get (append (x ::ᵥ xs) ys) ⟨i+1, h⟩ = get (append xs ys) i :=
  rfl

Element Access in Concatenated Vector with Cons: $v_{i+1} = (xs \cdot ys)_i$

Informal description

For any element $x$ of type $\alpha$, vector $xs$ of length $n$ over $\alpha$, vector $ys$ of length $m$ over $\alpha$, and index $i$ of type $\text{Fin}(n + m)$ with proof $h$, the $(i+1)$-th element of the concatenation of the vector $x ::ᵥ xs$ with $ys$ is equal to the $i$-th element of the concatenation of $xs$ with $ys$. More formally, if $v = \text{append}(x ::ᵥ xs, ys)$, then $v_{i+1} = (\text{append}(xs, ys))_i$.

List.Vector.append_nil theorem

: append xs nil = xs

Full source

@[simp]
theorem append_nil : append xs nil = xs := by
  cases xs; simp [append]

Right Identity of Vector Concatenation with Empty Vector

Informal description

For any vector `xs` of length `n` over a type `α`, the concatenation of `xs` with the empty vector `nil` is equal to `xs` itself, i.e., $xs \cdot nil = xs$.

List.Vector.get_map₂ theorem

 (v₁ : Vector α n) (v₂ : Vector β n) (f : α → β → γ) (i : Fin n) : get (map₂ f v₁ v₂) i = f (get v₁ i) (get v₂ i)

Full source

@[simp]
theorem get_map₂ (v₁ : Vector α n) (v₂ : Vector β n) (f : α → β → γ) (i : Fin n) :
    get (map₂ f v₁ v₂) i = f (get v₁ i) (get v₂ i) := by
  clear * - v₁ v₂
  induction v₁, v₂ using inductionOn₂ with
  | nil =>
    exact Fin.elim0 i
  | cons ih =>
    rw [map₂_cons]
    cases i using Fin.cases
    · simp only [get_zero, head_cons]
    · simp only [get_cons_succ, ih]

Element-wise Evaluation of Pairwise Vector Mapping: $\text{map}_2(f, \mathbf{v}_1, \mathbf{v}_2)_i = f(\mathbf{v}_{1i}, \mathbf{v}_{2i})$

Informal description

For any vectors $\mathbf{v}_1 : \text{Vector}\,\alpha\,n$ and $\mathbf{v}_2 : \text{Vector}\,\beta\,n$, any function $f : \alpha \to \beta \to \gamma$, and any index $i : \text{Fin}\,n$, the $i$-th element of the pairwise mapped vector $\text{map}_2(f, \mathbf{v}_1, \mathbf{v}_2)$ is equal to $f$ applied to the $i$-th elements of $\mathbf{v}_1$ and $\mathbf{v}_2$, i.e., \[ \text{get}(\text{map}_2(f, \mathbf{v}_1, \mathbf{v}_2), i) = f(\text{get}(\mathbf{v}_1, i), \text{get}(\mathbf{v}_2, i)). \]

List.Vector.mapAccumr_cons theorem

 {f : α → σ → σ × β} :
  mapAccumr f (x ::ᵥ xs) s =
    let r := mapAccumr f xs s
    let q := f x r.1
    (q.1, q.2 ::ᵥ r.2)

Full source

@[simp]
theorem mapAccumr_cons {f : α → σ → σ × β} :
    mapAccumr f (x ::ᵥ xs) s
    = let r := mapAccumr f xs s
      let q := f x r.1
      (q.1, q.2 ::ᵥ r.2) :=
  rfl

Recursive decomposition of right-to-left vector accumulation

Informal description

Let $f : \alpha \to \sigma \to \sigma \times \beta$ be a function, and let $\mathbf{v} = x :: \mathbf{v}_s$ be a vector of length $n+1$ over type $\alpha$. Given an initial state $s : \sigma$, the right-to-left accumulation of $f$ over $\mathbf{v}$ satisfies: \[ \text{mapAccumr}\, f\, \mathbf{v}\, s = (q_1, q_2 :: \mathbf{u}) \] where: 1. $(r_1, \mathbf{u}) = \text{mapAccumr}\, f\, \mathbf{v}_s\, s$ is the result of processing the tail of the vector, 2. $(q_1, q_2) = f\, x\, r_1$ is the result of applying $f$ to the head $x$ with the intermediate state $r_1$.

List.Vector.mapAccumr₂_cons theorem

 {f : α → β → σ → σ × φ} :
  mapAccumr₂ f (x ::ᵥ xs) (y ::ᵥ ys) s =
    let r := mapAccumr₂ f xs ys s
    let q := f x y r.1
    (q.1, q.2 ::ᵥ r.2)

Full source

@[simp]
theorem mapAccumr₂_cons {f : α → β → σ → σ × φ} :
    mapAccumr₂ f (x ::ᵥ xs) (y ::ᵥ ys) s
    = let r := mapAccumr₂ f xs ys s
      let q := f x y r.1
      (q.1, q.2 ::ᵥ r.2) :=
  rfl

Recursive decomposition of right-to-left pairwise vector accumulation

Informal description

Let $f : \alpha \to \beta \to \sigma \to \sigma \times \phi$ be a function, and let $\mathbf{v} = x :: \mathbf{v}_s$ and $\mathbf{w} = y :: \mathbf{w}_s$ be two vectors of length $n+1$ over types $\alpha$ and $\beta$ respectively. Given an initial state $s : \sigma$, the right-to-left pairwise accumulation of $f$ over $\mathbf{v}$ and $\mathbf{w}$ satisfies: \[ \text{mapAccumr₂}\, f\, \mathbf{v}\, \mathbf{w}\, s = (q_1, q_2 :: \mathbf{u}) \] where: 1. $(r_1, \mathbf{u}) = \text{mapAccumr₂}\, f\, \mathbf{v}_s\, \mathbf{w}_s\, s$ is the result of processing the tails of the vectors, 2. $(q_1, q_2) = f\, x\, y\, r_1$ is the result of applying $f$ to the heads $x$ and $y$ with the intermediate state $r_1$.