Init.Data.List.OfFn

List.ofFn definition

{n} (f : Fin n → α) : List α

Full source

/--
Creates a list by applying `f` to each potential index in order, starting at `0`.

Examples:
 * `List.ofFn (n := 3) toString = ["0", "1", "2"]`
 * `List.ofFn (fun i => #["red", "green", "blue"].get i.val i.isLt) = ["red", "green", "blue"]`
-/
def ofFn {n} (f : Fin n → α) : List α := Fin.foldr n (f · :: ·) []

List from function on finite indices

Informal description

Given a natural number $n$ and a function $f : \text{Fin } n \to \alpha$, the function $\text{List.ofFn}$ constructs a list of length $n$ by applying $f$ to each index $i$ in $\text{Fin } n$ (i.e., $0 \leq i < n$) in order from $0$ to $n-1$. For example: - $\text{List.ofFn } (\text{fun } i \Rightarrow \text{toString } i) \text{ with } n = 3$ produces the list $["0", "1", "2"]$. - $\text{List.ofFn } (\text{fun } i \Rightarrow \text{["red", "green", "blue"].get } i)$ produces the list $["red", "green", "blue"]$.

List.length_ofFn theorem

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

Full source

@[simp]
theorem length_ofFn {f : Fin n → α} : (ofFn f).length = n := by
  simp only [ofFn]
  induction n with
  | zero => simp
  | succ n ih => simp [Fin.foldr_succ, ih]

Length of List Constructed from Function on Finite Indices Equals $n$

Informal description

For any natural number $n$ and any function $f : \text{Fin } n \to \alpha$, the length of the list constructed by $\text{List.ofFn } f$ is equal to $n$.

List.getElem_ofFn theorem

{f : Fin n → α} (h : i < (ofFn f).length) : (ofFn f)[i] = f ⟨i, by simp_all⟩

Full source

@[simp]
protected theorem getElem_ofFn {f : Fin n → α} (h : i < (ofFn f).length) :
    (ofFn f)[i] = f ⟨i, by simp_all⟩ := by
  simp only [ofFn]
  induction n generalizing i with
  | zero => simp at h
  | succ n ih =>
    match i with
    | 0 => simp [Fin.foldr_succ]
    | i+1 =>
      simp only [Fin.foldr_succ]
      apply ih
      simp_all

Element Access in List Constructed from Function on Finite Indices

Informal description

For any natural number $n$, function $f : \text{Fin } n \to \alpha$, and index $i$ such that $i < \text{length}(\text{List.ofFn } f)$, the $i$-th element of the list $\text{List.ofFn } f$ is equal to $f$ evaluated at the index $\langle i, h \rangle$, where $h$ is a proof that $i < n$.

List.getElem?_ofFn theorem

{f : Fin n → α} : (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none

Full source

@[simp]
protected theorem getElem?_ofFn {f : Fin n → α} : (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none :=
  if h : i < (ofFn f).length
  then by
    rw [getElem?_eq_getElem h, List.getElem_ofFn]
    · simp only [length_ofFn] at h; simp [h]
  else by
    rw [dif_neg] <;>
    simpa using h

Optional Indexing of List Constructed from Finite Function

Informal description

For any natural number $n$ and function $f : \text{Fin } n \to \alpha$, the optional indexing operation on the list $\text{List.ofFn } f$ at index $i$ satisfies: \[ (\text{List.ofFn } f)[i]? = \begin{cases} \text{some } (f \langle i, h \rangle) & \text{if } i < n \text{ (with proof } h \text{)} \\ \text{none} & \text{otherwise} \end{cases} \]

List.ofFn_zero theorem

{f : Fin 0 → α} : ofFn f = []

Full source

/-- `ofFn` on an empty domain is the empty list. -/
@[simp]
theorem ofFn_zero {f : Fin 0 → α} : ofFn f = [] :=
  ext_get (by simp) (fun i hi₁ hi₂ => by contradiction)

Empty List Construction from Zero-Domain Function

Informal description

For any function $f : \text{Fin } 0 \to \alpha$, the list constructed by applying $f$ to all indices in $\text{Fin } 0$ is the empty list, i.e., $\text{List.ofFn } f = []$.

List.ofFn_succ theorem

{n} {f : Fin (n + 1) → α} : ofFn f = f 0 :: ofFn fun i => f i.succ

Full source

@[simp]
theorem ofFn_succ {n} {f : Fin (n + 1) → α} : ofFn f = f 0 :: ofFn fun i => f i.succ :=
  ext_get (by simp) (fun i hi₁ hi₂ => by
    cases i
    · simp
    · simp)

Recursive Construction of List from Function on Successor Indices: $\text{List.ofFn } f = f(0) :: \text{List.ofFn } (i \mapsto f(i+1))$

Informal description

For any natural number $n$ and function $f : \text{Fin}(n+1) \to \alpha$, the list constructed from $f$ via $\text{List.ofFn}$ is equal to the list whose head is $f(0)$ and whose tail is the list constructed from the function $i \mapsto f(i+1)$ on $\text{Fin}(n)$.

List.ofFn_eq_nil_iff theorem

{f : Fin n → α} : ofFn f = [] ↔ n = 0

Full source

@[simp]
theorem ofFn_eq_nil_iff {f : Fin n → α} : ofFnofFn f = [] ↔ n = 0 := by
  cases n <;> simp only [ofFn_zero, ofFn_succ, eq_self_iff_true, Nat.succ_ne_zero, reduceCtorEq]

Empty List from Function iff Domain is Zero: $\text{List.ofFn } f = [] \leftrightarrow n = 0$

Informal description

For any function $f : \text{Fin } n \to \alpha$, the list $\text{List.ofFn } f$ is empty if and only if $n = 0$.

List.mem_ofFn theorem

{n} {f : Fin n → α} {a : α} : a ∈ ofFn f ↔ ∃ i, f i = a

Full source

@[simp 500]
theorem mem_ofFn {n} {f : Fin n → α} {a : α} : a ∈ ofFn fa ∈ ofFn f ↔ ∃ i, f i = a := by
  constructor
  · intro w
    obtain ⟨i, h, rfl⟩ := getElem_of_mem w
    exact ⟨⟨i, by simpa using h⟩, by simp⟩
  · rintro ⟨i, rfl⟩
    apply mem_of_getElem (i := i) <;> simp

Membership in List from Function: $a \in \text{List.ofFn } f \leftrightarrow \exists i, f(i) = a$

Informal description

For any natural number $n$, function $f : \text{Fin } n \to \alpha$, and element $a \in \alpha$, the element $a$ is in the list $\text{List.ofFn } f$ if and only if there exists an index $i \in \text{Fin } n$ such that $f(i) = a$.

List.head_ofFn theorem

{n} {f : Fin n → α} (h : ofFn f ≠ []) : (ofFn f).head h = f ⟨0, Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)⟩

Full source

theorem head_ofFn {n} {f : Fin n → α} (h : ofFnofFn f ≠ []) :
    (ofFn f).head h = f ⟨0, Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)⟩ := by
  rw [← getElem_zero (length_ofFn ▸ Nat.pos_of_ne_zero (mt ofFn_eq_nil_iff.2 h)),
    List.getElem_ofFn]

Head of List from Function Equals Function at Zero Index

Informal description

For any natural number $n$ and function $f : \text{Fin } n \to \alpha$, if the list $\text{List.ofFn } f$ is non-empty, then its head element is equal to $f$ evaluated at the index $\langle 0, h \rangle$, where $h$ is a proof that $0 < n$.

List.getLast_ofFn theorem

 {n} {f : Fin n → α} (h : ofFn f ≠ []) : (ofFn f).getLast h = f ⟨n - 1, Nat.sub_one_lt (mt ofFn_eq_nil_iff.2 h)⟩

Full source

theorem getLast_ofFn {n} {f : Fin n → α} (h : ofFnofFn f ≠ []) :
    (ofFn f).getLast h = f ⟨n - 1, Nat.sub_one_lt (mt ofFn_eq_nil_iff.2 h)⟩ := by
  simp [getLast_eq_getElem, length_ofFn, List.getElem_ofFn]

Last Element of List from Function: $\text{getLast}(\text{List.ofFn } f) = f(n - 1)$ for Non-Empty Lists

Informal description

For any natural number $n$ and function $f : \text{Fin } n \to \alpha$, if the list $\text{List.ofFn } f$ is non-empty, then its last element is equal to $f$ evaluated at the index $\langle n - 1, h \rangle$, where $h$ is a proof that $n - 1 < n$ (which holds since $n \neq 0$ by the non-emptiness condition).