Mathlib.Data.List.OfFn

List.get_ofFn theorem

{n} (f : Fin n → α) (i) : get (ofFn f) i = f (Fin.cast (by simp) i)

Full source

theorem get_ofFn {n} (f : Fin n → α) (i) : get (ofFn f) i = f (Fin.cast (by simp) i) := by
  simp; congr

Element Access in List Generated from Function on Finite Indices

Informal description

For any function $f : \text{Fin } n \to \alpha$ and any index $i$, the $i$-th element of the list $\text{ofFn } f$ is equal to $f$ evaluated at the index obtained by casting $i$ via $\text{Fin.cast}$ (which is justified by the simplification `by simp`). In other words, if we convert a function $f$ defined on $\text{Fin } n$ to a list of length $n$ using $\text{ofFn}$, then accessing the $i$-th element of this list via $\text{get}$ gives the same result as applying $f$ to the appropriately cast index $i$.

List.map_ofFn theorem

{β : Type*} {n : ℕ} (f : Fin n → α) (g : α → β) : map g (ofFn f) = ofFn (g ∘ f)

Full source

@[simp]
theorem map_ofFn {β : Type*} {n : ℕ} (f : Fin n → α) (g : α → β) :
    map g (ofFn f) = ofFn (g ∘ f) :=
  ext_get (by simp) fun i h h' => by simp

Map Commutes with List Construction from Function

Informal description

For any function $f \colon \operatorname{Fin} n \to \alpha$ and any function $g \colon \alpha \to \beta$, the list obtained by applying $g$ to each element of the list generated from $f$ via $\operatorname{List.ofFn}$ is equal to the list generated from the composition $g \circ f$ via $\operatorname{List.ofFn}$. In other words, $\operatorname{map}\, g (\operatorname{ofFn}\, f) = \operatorname{ofFn}\, (g \circ f)$.

List.ofFn_congr theorem

{m n : ℕ} (h : m = n) (f : Fin m → α) : ofFn f = ofFn fun i : Fin n => f (Fin.cast h.symm i)

Full source

@[congr]
theorem ofFn_congr {m n : ℕ} (h : m = n) (f : Fin m → α) :
    ofFn f = ofFn fun i : Fin n => f (Fin.cast h.symm i) := by
  subst h
  simp_rw [Fin.cast_refl, id]

Congruence of List Construction from Function under Equality of Indices

Informal description

For any natural numbers $m$ and $n$ such that $m = n$, and for any function $f : \text{Fin}(m) \to \alpha$, the list constructed from $f$ via `List.ofFn` is equal to the list constructed from the function $\lambda i : \text{Fin}(n), f(\text{cast}(h^{-1}, i))$, where $\text{cast}(h^{-1}, \cdot)$ adjusts the index $i$ from $\text{Fin}(n)$ to $\text{Fin}(m)$ using the equality $h : m = n$.

List.ofFn_succ' theorem

{n} (f : Fin (succ n) → α) : ofFn f = (ofFn fun i => f (Fin.castSucc i)).concat (f (Fin.last _))

Full source

theorem ofFn_succ' {n} (f : Fin (succ n) → α) :
    ofFn f = (ofFn fun i => f (Fin.castSucc i)).concat (f (Fin.last _)) := by
  induction' n with n IH
  · rw [ofFn_zero, concat_nil, ofFn_succ, ofFn_zero]
    rfl
  · rw [ofFn_succ, IH, ofFn_succ, concat_cons, Fin.castSucc_zero]
    congr

Decomposition of `ofFn` for successor indices

Informal description

For any natural number $n$ and any function $f : \text{Fin}(n+1) \to \alpha$, the list obtained from $f$ via `List.ofFn` is equal to the concatenation of the list obtained from the restriction of $f$ to $\text{Fin}(n)$ (via `Fin.castSucc`) with the singleton list containing $f(\text{last } n)$. In symbols: $$\text{ofFn } f = (\text{ofFn } (f \circ \text{castSucc})).\text{concat}(f(\text{last } n))$$

List.ofFn_add theorem

 {m n} (f : Fin (m + n) → α) :
  List.ofFn f = (List.ofFn fun i => f (Fin.castAdd n i)) ++ List.ofFn fun j => f (Fin.natAdd m j)

Full source

/-- Note this matches the convention of `List.ofFn_succ'`, putting the `Fin m` elements first. -/
theorem ofFn_add {m n} (f : Fin (m + n) → α) :
    List.ofFn f =
      (List.ofFn fun i => f (Fin.castAdd n i)) ++ List.ofFn fun j => f (Fin.natAdd m j) := by
  induction' n with n IH
  · rw [ofFn_zero, append_nil, Fin.castAdd_zero, Fin.cast_refl]
    rfl
  · rw [ofFn_succ', ofFn_succ', IH, append_concat]
    rfl

Decomposition of `ofFn` for Sum Indices: $\text{ofFn } f = \text{ofFn } (f \circ \text{castAdd } n) +\!\!+ \text{ofFn } (f \circ \text{natAdd } m)$

Informal description

For any natural numbers $m$ and $n$, and any function $f : \text{Fin}(m+n) \to \alpha$, the list obtained from $f$ via `List.ofFn` is equal to the concatenation of two lists: 1. The list obtained from the function $\lambda i, f(\text{castAdd } n \ i)$ (which maps $\text{Fin}(m)$ to $\text{Fin}(m+n)$ by adding $n$ to the index) 2. The list obtained from the function $\lambda j, f(\text{natAdd } m \ j)$ (which maps $\text{Fin}(n)$ to $\text{Fin}(m+n)$ by offsetting the index by $m$) In symbols: $$\text{ofFn } f = (\text{ofFn } (f \circ \text{castAdd } n)) +\!\!+ (\text{ofFn } (f \circ \text{natAdd } m))$$

List.ofFn_fin_append theorem

{m n} (a : Fin m → α) (b : Fin n → α) : List.ofFn (Fin.append a b) = List.ofFn a ++ List.ofFn b

Full source

@[simp]
theorem ofFn_fin_append {m n} (a : Fin m → α) (b : Fin n → α) :
    List.ofFn (Fin.append a b) = List.ofFn a ++ List.ofFn b := by
  simp_rw [ofFn_add, Fin.append_left, Fin.append_right]

List Construction Preserves Tuple Concatenation: $\text{ofFn}\, (\text{append}\, a\, b) = \text{ofFn}\, a +\!\!+ \text{ofFn}\, b$

Informal description

For any natural numbers $m$ and $n$, and any functions $a : \text{Fin}\, m \to \alpha$ and $b : \text{Fin}\, n \to \alpha$, the list obtained from the concatenated function $\text{Fin.append}\, a\, b$ is equal to the concatenation of the lists obtained from $a$ and $b$ individually. In symbols: $$\text{ofFn}\, (\text{append}\, a\, b) = (\text{ofFn}\, a) +\!\!+ (\text{ofFn}\, b)$$

List.ofFn_mul theorem

 {m n} (f : Fin (m * n) → α) :
  List.ofFn f =
    List.flatten
      (List.ofFn fun i : Fin m =>
        List.ofFn fun j : Fin n =>
          f
            ⟨i * n + j,
              calc
                ↑i * n + j < (i + 1) * n := (Nat.add_lt_add_left j.prop _).trans_eq (by rw [Nat.add_mul, Nat.one_mul])
                _ ≤ _ := Nat.mul_le_mul_right _ i.prop⟩)

Full source

/-- This breaks a list of `m*n` items into `m` groups each containing `n` elements. -/
theorem ofFn_mul {m n} (f : Fin (m * n) → α) :
    List.ofFn f = List.flatten (List.ofFn fun i : Fin m => List.ofFn fun j : Fin n => f ⟨i * n + j,
    calc
      ↑i * n + j < (i + 1) * n :=
        (Nat.add_lt_add_left j.prop _).trans_eq (by rw [Nat.add_mul, Nat.one_mul])
      _ ≤ _ := Nat.mul_le_mul_right _ i.prop⟩) := by
  induction' m with m IH
  · simp [ofFn_zero, Nat.zero_mul, ofFn_zero, flatten]
  · simp_rw [ofFn_succ', succ_mul]
    simp [flatten_concat, ofFn_add, IH]
    rfl

Decomposition of `ofFn` for Product Indices: $\text{ofFn } f$ as Flattened Matrix

Informal description

For any natural numbers $m$ and $n$, and any function $f : \text{Fin}(m \times n) \to \alpha$, the list obtained from $f$ via `List.ofFn` is equal to the flattened list of lists constructed by grouping the elements of $f$ into $m$ groups of $n$ elements each. Specifically, for each index $i \in \text{Fin}(m)$, the inner list is constructed by applying $f$ to the indices $\langle i \times n + j \rangle$ where $j \in \text{Fin}(n)$. In symbols: $$\text{ofFn } f = \text{flatten} \left( \text{ofFn} \left( \lambda i : \text{Fin}(m), \text{ofFn} \left( \lambda j : \text{Fin}(n), f \langle i \times n + j \rangle \right) \right) \right)$$

List.ofFn_mul' theorem

 {m n} (f : Fin (m * n) → α) :
  List.ofFn f =
    List.flatten
      (List.ofFn fun i : Fin n =>
        List.ofFn fun j : Fin m =>
          f
            ⟨m * i + j,
              calc
                m * i + j < m * (i + 1) := (Nat.add_lt_add_left j.prop _).trans_eq (by rw [Nat.mul_add, Nat.mul_one])
                _ ≤ _ := Nat.mul_le_mul_left _ i.prop⟩)

Full source

/-- This breaks a list of `m*n` items into `n` groups each containing `m` elements. -/
theorem ofFn_mul' {m n} (f : Fin (m * n) → α) :
    List.ofFn f = List.flatten (List.ofFn fun i : Fin n => List.ofFn fun j : Fin m => f ⟨m * i + j,
    calc
      m * i + j < m * (i + 1) :=
        (Nat.add_lt_add_left j.prop _).trans_eq (by rw [Nat.mul_add, Nat.mul_one])
      _ ≤ _ := Nat.mul_le_mul_left _ i.prop⟩) := by simp_rw [m.mul_comm, ofFn_mul, Fin.cast_mk]

Decomposition of $\text{ofFn } f$ into $n$ groups of $m$ elements each

Informal description

For any natural numbers $m$ and $n$, and any function $f : \text{Fin}(m \times n) \to \alpha$, the list obtained from $f$ via `List.ofFn` is equal to the flattened list of lists constructed by grouping the elements of $f$ into $n$ groups each containing $m$ elements. Specifically, for each index $i \in \text{Fin}(n)$, the inner list is constructed by applying $f$ to the indices $\langle m \times i + j \rangle$ where $j \in \text{Fin}(m)$. In symbols: $$\text{ofFn } f = \text{flatten} \left( \text{ofFn} \left( \lambda i : \text{Fin}(n), \text{ofFn} \left( \lambda j : \text{Fin}(m), f \langle m \times i + j \rangle \right) \right) \right)$$

List.ofFn_get theorem

: ∀ l : List α, (ofFn (get l)) = l

Full source

@[simp]
theorem ofFn_get : ∀ l : List α, (ofFn (get l)) = l
  | [] => by rw [ofFn_zero]
  | a :: l => by
    rw [ofFn_succ]
    congr
    exact ofFn_get l

Reconstruction of List from Indexed Elements via `ofFn`

Informal description

For any list $l$ of elements of type $\alpha$, the list constructed by applying `List.ofFn` to the function that retrieves elements of $l$ by their indices is equal to $l$ itself. In other words, $\text{ofFn}(\text{get}(l)) = l$.

List.ofFn_getElem theorem

: ∀ l : List α, (ofFn (fun i : Fin l.length => l[(i : Nat)])) = l

Full source

@[simp]
theorem ofFn_getElem : ∀ l : List α, (ofFn (fun i : Fin l.length => l[(i : Nat)])) = l
  | [] => by rw [ofFn_zero]
  | a :: l => by
    rw [ofFn_succ]
    congr
    exact ofFn_get l

List Reconstruction from Indexed Access via `ofFn`

Informal description

For any list $l$ of elements of type $\alpha$, the list constructed by applying `List.ofFn` to the function that retrieves elements of $l$ by their indices (viewed as natural numbers) is equal to $l$ itself. In other words, $\text{ofFn}(\lambda (i : \text{Fin } l.\text{length}), l[i]) = l$.

List.ofFn_getElem_eq_map theorem

{β : Type*} (l : List α) (f : α → β) : ofFn (fun i : Fin l.length => f <| l[(i : Nat)]) = l.map f

Full source

@[simp]
theorem ofFn_getElem_eq_map {β : Type*} (l : List α) (f : α → β) :
    ofFn (fun i : Fin l.length => f <| l[(i : Nat)]) = l.map f := by
  rw [← Function.comp_def, ← map_ofFn, ofFn_getElem]

Equivalence of List Construction via Indexing and Mapping

Informal description

For any list $l$ of elements of type $\alpha$ and any function $f \colon \alpha \to \beta$, the list constructed by applying $f$ to each element of $l$ via indexing (using `Fin l.length`) is equal to the list obtained by mapping $f$ over $l$. In other words, $\text{ofFn}(\lambda (i : \text{Fin } l.\text{length}), f(l[i])) = \text{map}\, f\, l$.

List.mem_ofFn' theorem

{n} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ a ∈ Set.range f

Full source

theorem mem_ofFn' {n} (f : Fin n → α) (a : α) : a ∈ ofFn fa ∈ ofFn f ↔ a ∈ Set.range f := by
  simp only [mem_iff_get, Set.mem_range, get_ofFn]
  exact ⟨fun ⟨i, hi⟩ => ⟨Fin.cast (by simp) i, hi⟩, fun ⟨i, hi⟩ => ⟨Fin.cast (by simp) i, hi⟩⟩

Membership in List from Function Equivales Membership in Function's Range

Informal description

For any function $f : \text{Fin } n \to \alpha$ and any element $a \in \alpha$, the element $a$ appears in the list $\text{ofFn } f$ if and only if $a$ is in the range of $f$, i.e., $a \in \text{range } f$.

List.forall_mem_ofFn_iff theorem

{n : ℕ} {f : Fin n → α} {P : α → Prop} : (∀ i ∈ ofFn f, P i) ↔ ∀ j : Fin n, P (f j)

Full source

theorem forall_mem_ofFn_iff {n : ℕ} {f : Fin n → α} {P : α → Prop} :
    (∀ i ∈ ofFn f, P i) ↔ ∀ j : Fin n, P (f j) := by simp

Universal Quantification over List from Function vs. Function Domain

Informal description

For any natural number $n$, function $f \colon \mathrm{Fin}\,n \to \alpha$, and predicate $P \colon \alpha \to \mathrm{Prop}$, the following are equivalent: 1. For every element $i$ in the list $\mathrm{ofFn}\,f$, the proposition $P(i)$ holds. 2. For every index $j \in \mathrm{Fin}\,n$, the proposition $P(f(j))$ holds.

List.ofFn_const theorem

: ∀ (n : ℕ) (c : α), (ofFn fun _ : Fin n => c) = replicate n c

Full source

@[simp]
theorem ofFn_const : ∀ (n : ℕ) (c : α), (ofFn fun _ : Fin n => c) = replicate n c
  | 0, c => by rw [ofFn_zero, replicate_zero]
  | n+1, c => by rw [replicate, ← ofFn_const n]; simp

Constant Function Generates Replicated List

Informal description

For any natural number $n$ and any element $c$ of type $\alpha$, the list constructed from the constant function $\lambda \_, c$ on $\text{Fin } n$ is equal to the list obtained by replicating $c$ $n$ times. In other words, $\text{ofFn} (\lambda \_, c) = \text{replicate } n c$.

List.ofFn_fin_repeat theorem

{m} (a : Fin m → α) (n : ℕ) : List.ofFn (Fin.repeat n a) = (List.replicate n (List.ofFn a)).flatten

Full source

@[simp]
theorem ofFn_fin_repeat {m} (a : Fin m → α) (n : ℕ) :
    List.ofFn (Fin.repeat n a) = (List.replicate n (List.ofFn a)).flatten := by
  simp_rw [ofFn_mul, ← ofFn_const, Fin.repeat, Fin.modNat, Nat.add_comm,
    Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt (Fin.is_lt _)]

List from Repeated Tuple Equals Flattened Replicated List

Informal description

For any natural number $m$, function $a \colon \mathrm{Fin}\,m \to \alpha$, and natural number $n$, the list generated from the repeated tuple $\mathrm{Fin.repeat}\,n\,a$ is equal to the flattened list obtained by replicating the list $\mathrm{List.ofFn}\,a$ exactly $n$ times. In symbols: $$\mathrm{List.ofFn}\,(\mathrm{Fin.repeat}\,n\,a) = \mathrm{flatten}\,(\mathrm{replicate}\,n\,(\mathrm{List.ofFn}\,a))$$

List.pairwise_ofFn theorem

{R : α → α → Prop} {n} {f : Fin n → α} : (ofFn f).Pairwise R ↔ ∀ ⦃i j⦄, i < j → R (f i) (f j)

Full source

@[simp]
theorem pairwise_ofFn {R : α → α → Prop} {n} {f : Fin n → α} :
    (ofFn f).Pairwise R ↔ ∀ ⦃i j⦄, i < j → R (f i) (f j) := by
  simp only [pairwise_iff_getElem, length_ofFn, List.getElem_ofFn,
    (Fin.rightInverse_cast length_ofFn).surjective.forall, Fin.forall_iff, Fin.cast_mk,
    Fin.mk_lt_mk, forall_comm (α := (_ : Prop)) (β := ℕ)]

Pairwise Relation on List Generated from Function via `ofFn`

Informal description

For any binary relation $R$ on a type $\alpha$, any natural number $n$, and any function $f : \text{Fin } n \to \alpha$, the list $\text{ofFn } f$ is pairwise related by $R$ if and only if for all indices $i, j$ in $\text{Fin } n$ with $i < j$, the relation $R(f(i), f(j))$ holds.

List.getLast_ofFn_succ theorem

{n : ℕ} (f : Fin n.succ → α) : (ofFn f).getLast (mt ofFn_eq_nil_iff.1 (Nat.succ_ne_zero _)) = f (Fin.last _)

Full source

lemma getLast_ofFn_succ {n : ℕ} (f : Fin n.succ → α) :
    (ofFn f).getLast (mt ofFn_eq_nil_iff.1 (Nat.succ_ne_zero _)) = f (Fin.last _) :=
  getLast_ofFn _

Last Element of List Generated from Function on $\text{Fin}(n+1)$

Informal description

For any natural number $n$ and any function $f : \text{Fin}(n+1) \to \alpha$, the last element of the list obtained from $f$ via `List.ofFn` is equal to $f$ evaluated at the last element of $\text{Fin}(n+1)$. That is, if $L = \text{List.ofFn}(f)$, then $\text{List.getLast}(L) = f(\text{Fin.last}(n))$.

List.ofFn_cons theorem

{n} (a : α) (f : Fin n → α) : ofFn (Fin.cons a f) = a :: ofFn f

Full source

lemma ofFn_cons {n} (a : α) (f : Fin n → α) : ofFn (Fin.cons a f) = a :: ofFn f := by
  rw [ofFn_succ]
  rfl

List Construction via `ofFn` Preserves Prepend Operation

Informal description

For any natural number $n$, element $a : \alpha$, and function $f : \text{Fin } n \to \alpha$, the list constructed from the function $\text{Fin.cons } a \ f$ (which prepends $a$ to $f$) is equal to the list obtained by prepending $a$ to the list constructed from $f$. That is, $\text{ofFn}(\text{Fin.cons } a \ f) = a :: \text{ofFn } f$.

List.find?_ofFn_eq_some theorem

 {n} {f : Fin n → α} {p : α → Bool} {b : α} :
  (ofFn f).find? p = some b ↔ p b = true ∧ ∃ i, f i = b ∧ ∀ j < i, ¬(p (f j) = true)

Full source

lemma find?_ofFn_eq_some {n} {f : Fin n → α} {p : α → Bool} {b : α} :
    (ofFn f).find? p = some b ↔ p b = true ∧ ∃ i, f i = b ∧ ∀ j < i, ¬(p (f j) = true) := by
  rw [find?_eq_some_iff_getElem]
  exact ⟨fun ⟨hpb, i, hi, hfb, h⟩ ↦
      ⟨hpb, ⟨⟨i, length_ofFn (f := f) ▸ hi⟩, by simpa using hfb, fun j hj ↦ by simpa using h j hj⟩⟩,
    fun ⟨hpb, i, hfb, h⟩ ↦
      ⟨hpb, ⟨i, (length_ofFn (f := f)).symm ▸ i.isLt, by simpa using hfb,
        fun j hj ↦ by simpa using h ⟨j, by omega⟩ (by simpa using hj)⟩⟩⟩

Characterization of `find?` on Lists Generated from Functions

Informal description

For a function $f \colon \mathrm{Fin}\,n \to \alpha$ and a predicate $p \colon \alpha \to \mathrm{Bool}$, the `find?` operation on the list `ofFn f` returns `some b` if and only if: 1. The predicate $p$ holds for $b$ (i.e., $p(b) = \mathtt{true}$), and 2. There exists an index $i \in \mathrm{Fin}\,n$ such that $f(i) = b$ and for all indices $j < i$, the predicate $p$ does not hold for $f(j)$ (i.e., $p(f(j)) \neq \mathtt{true}$).

List.find?_ofFn_eq_some_of_injective theorem

 {n} {f : Fin n → α} {p : α → Bool} {i : Fin n} (h : Function.Injective f) :
  (ofFn f).find? p = some (f i) ↔ p (f i) = true ∧ ∀ j < i, ¬(p (f j) = true)

Full source

lemma find?_ofFn_eq_some_of_injective {n} {f : Fin n → α} {p : α → Bool} {i : Fin n}
    (h : Function.Injective f) :
    (ofFn f).find? p = some (f i) ↔ p (f i) = true ∧ ∀ j < i, ¬(p (f j) = true) := by
  simp only [find?_ofFn_eq_some, h.eq_iff, Bool.not_eq_true, exists_eq_left]

Characterization of `find?` on Injective Function-Generated Lists

Informal description

Let $f \colon \mathrm{Fin}\,n \to \alpha$ be an injective function, $p \colon \alpha \to \mathrm{Bool}$ a predicate, and $i \in \mathrm{Fin}\,n$ an index. Then the `find?` operation on the list `ofFn f` returns `some (f i)` if and only if: 1. The predicate $p$ holds for $f(i)$ (i.e., $p(f(i)) = \mathtt{true}$), and 2. For all indices $j < i$, the predicate $p$ does not hold for $f(j)$ (i.e., $p(f(j)) \neq \mathtt{true}$).

List.equivSigmaTuple definition

: List α ≃ Σ n, Fin n → α

Full source

/-- Lists are equivalent to the sigma type of tuples of a given length. -/
@[simps]
def equivSigmaTuple : ListList α ≃ Σn, Fin n → α where
  toFun l := ⟨l.length, l.get⟩
  invFun f := List.ofFn f.2
  left_inv := List.ofFn_get
  right_inv := fun ⟨_, f⟩ =>
    Fin.sigma_eq_of_eq_comp_cast length_ofFn <| funext fun i => get_ofFn f i

Equivalence between lists and functions on finite types

Informal description

The equivalence between lists of elements of type $\alpha$ and pairs $(n, f)$, where $n$ is a natural number and $f \colon \mathrm{Fin}\,n \to \alpha$ is a function from the canonical type with $n$ elements to $\alpha$. The forward map sends a list $l$ to the pair $(|l|, \mathrm{get}(l))$, where $|l|$ is the length of $l$ and $\mathrm{get}(l)$ is the function that retrieves the $i$-th element of $l$ for $i \in \mathrm{Fin}\,|l|$. The inverse map constructs a list from a function $f \colon \mathrm{Fin}\,n \to \alpha$ by applying $f$ to all elements of $\mathrm{Fin}\,n$.

List.ofFnRec definition

{C : List α → Sort*} (h : ∀ (n) (f : Fin n → α), C (List.ofFn f)) (l : List α) : C l

Full source

/-- A recursor for lists that expands a list into a function mapping to its elements.

This can be used with `induction l using List.ofFnRec`. -/
@[elab_as_elim]
def ofFnRec {C : List α → Sort*} (h : ∀ (n) (f : Fin n → α), C (List.ofFn f)) (l : List α) : C l :=
  cast (congr_arg C l.ofFn_get) <|
    h l.length l.get

Recursor for lists via functions on finite types

Informal description

Given a type family `C` depending on lists of type `α` and a function `h` that for any natural number `n` and any function `f : Fin n → α` produces an element of `C (List.ofFn f)`, the recursor `List.ofFnRec` constructs an element of `C l` for any list `l`. Here, `List.ofFn f` is the list obtained by applying `f` to all elements of `Fin n`.

List.ofFnRec_ofFn theorem

 {C : List α → Sort*} (h : ∀ (n) (f : Fin n → α), C (List.ofFn f)) {n : ℕ} (f : Fin n → α) :
  @ofFnRec _ C h (List.ofFn f) = h _ f

Full source

@[simp]
theorem ofFnRec_ofFn {C : List α → Sort*} (h : ∀ (n) (f : Fin n → α), C (List.ofFn f)) {n : ℕ}
    (f : Fin n → α) : @ofFnRec _ C h (List.ofFn f) = h _ f :=
  equivSigmaTuple.rightInverse_symm.cast_eq (fun s => h s.1 s.2) ⟨n, f⟩

Recursor Computation for Lists Constructed from Finite Functions

Informal description

For any type family $C$ depending on lists of type $\alpha$, and any function $h$ that for every natural number $n$ and function $f \colon \mathrm{Fin}\,n \to \alpha$ produces an element of $C(\mathrm{List.ofFn}\,f)$, we have that applying the recursor $\mathrm{ofFnRec}$ to the list $\mathrm{List.ofFn}\,f$ yields the same result as directly applying $h$ to $n$ and $f$. In other words, for any $n \in \mathbb{N}$ and $f \colon \mathrm{Fin}\,n \to \alpha$, the following equality holds: \[ \mathrm{ofFnRec}\,h\,(\mathrm{List.ofFn}\,f) = h\,n\,f \]

List.exists_iff_exists_tuple theorem

{P : List α → Prop} : (∃ l : List α, P l) ↔ ∃ (n : _) (f : Fin n → α), P (List.ofFn f)

Full source

theorem exists_iff_exists_tuple {P : List α → Prop} :
    (∃ l : List α, P l) ↔ ∃ (n : _) (f : Fin n → α), P (List.ofFn f) :=
  equivSigmaTuple.symm.surjective.exists.trans Sigma.exists

Existence of Lists via Functions on Finite Types

Informal description

For any predicate $P$ on lists of type $\alpha$, there exists a list $l$ satisfying $P(l)$ if and only if there exists a natural number $n$ and a function $f \colon \mathrm{Fin}\,n \to \alpha$ such that $P$ holds for the list generated by applying $f$ to all elements of $\mathrm{Fin}\,n$.

List.forall_iff_forall_tuple theorem

{P : List α → Prop} : (∀ l : List α, P l) ↔ ∀ (n) (f : Fin n → α), P (List.ofFn f)

Full source

theorem forall_iff_forall_tuple {P : List α → Prop} :
    (∀ l : List α, P l) ↔ ∀ (n) (f : Fin n → α), P (List.ofFn f) :=
  equivSigmaTuple.symm.surjective.forall.trans Sigma.forall

Universal Quantification over Lists vs. Functions on Finite Types

Informal description

For any predicate $P$ on lists of elements of type $\alpha$, the universal quantification $\forall l \in \text{List}\,\alpha, P(l)$ holds if and only if for every natural number $n$ and every function $f \colon \text{Fin}\,n \to \alpha$, the predicate $P(\text{ofFn}\,f)$ holds, where $\text{ofFn}\,f$ is the list obtained by applying $f$ to all elements of $\text{Fin}\,n$.

List.ofFn_inj' theorem

{m n : ℕ} {f : Fin m → α} {g : Fin n → α} : ofFn f = ofFn g ↔ (⟨m, f⟩ : Σ n, Fin n → α) = ⟨n, g⟩

Full source

/-- `Fin.sigma_eq_iff_eq_comp_cast` may be useful to work with the RHS of this expression. -/
theorem ofFn_inj' {m n : ℕ} {f : Fin m → α} {g : Fin n → α} :
    ofFnofFn f = ofFn g ↔ (⟨m, f⟩ : Σn, Fin n → α) = ⟨n, g⟩ :=
  Iff.symm <| equivSigmaTuple.symm.injective.eq_iff.symm

Equality of Generated Lists via Functions on Finite Types

Informal description

For any natural numbers $m, n$ and functions $f \colon \mathrm{Fin}\,m \to \alpha$, $g \colon \mathrm{Fin}\,n \to \alpha$, the lists generated by $f$ and $g$ are equal if and only if the pairs $(m, f)$ and $(n, g)$ are equal in the sigma type $\Sigma n, \mathrm{Fin}\,n \to \alpha$. In other words, $\mathrm{ofFn}\,f = \mathrm{ofFn}\,g$ if and only if $m = n$ and $f = g$.

List.ofFn_injective theorem

{n : ℕ} : Function.Injective (ofFn : (Fin n → α) → List α)

Full source

/-- Note we can only state this when the two functions are indexed by defeq `n`. -/
theorem ofFn_injective {n : ℕ} : Function.Injective (ofFn : (Fin n → α) → List α) := fun f g h =>
  eq_of_heq <| by rw [ofFn_inj'] at h; cases h; rfl

Injectivity of List Construction from Finite Functions

Informal description

For any natural number $n$, the function $\mathrm{ofFn} \colon (\mathrm{Fin}\,n \to \alpha) \to \mathrm{List}\,\alpha$ is injective. That is, for any two functions $f, g \colon \mathrm{Fin}\,n \to \alpha$, if $\mathrm{ofFn}\,f = \mathrm{ofFn}\,g$, then $f = g$.

List.ofFn_inj theorem

{n : ℕ} {f g : Fin n → α} : ofFn f = ofFn g ↔ f = g

Full source

/-- A special case of `List.ofFn_inj` for when the two functions are indexed by defeq `n`. -/
@[simp]
theorem ofFn_inj {n : ℕ} {f g : Fin n → α} : ofFnofFn f = ofFn g ↔ f = g :=
  ofFn_injective.eq_iff

Equality of Lists Constructed from Functions on $\mathrm{Fin}\,n$

Informal description

For any natural number $n$ and functions $f, g \colon \mathrm{Fin}\,n \to \alpha$, the lists constructed from $f$ and $g$ are equal if and only if $f = g$. That is, $\mathrm{ofFn}\,f = \mathrm{ofFn}\,g \leftrightarrow f = g$.

Main Statements