Init.Data.List.FinRange

List.finRange definition

(n : Nat) : List (Fin n)

Full source

/--
Lists all elements of `Fin n` in order, starting at `0`.

Examples:
 * `List.finRange 0 = ([] : List (Fin 0))`
 * `List.finRange 2 = ([0, 1] : List (Fin 2))`
-/
def finRange (n : Nat) : List (Fin n) := ofFn fun i => i

List of all elements in `Fin n` in order

Informal description

The function `List.finRange` takes a natural number `n` and returns a list containing all elements of the type `Fin n` in ascending order, starting from `0`. For example: - `List.finRange 0` returns the empty list `[]`. - `List.finRange 2` returns the list `[0, 1]`.

List.length_finRange theorem

{n : Nat} : (List.finRange n).length = n

Full source

@[simp] theorem length_finRange {n : Nat} : (List.finRange n).length = n := by
  simp [List.finRange]

Length of `finRange n` is $n$

Informal description

For any natural number $n$, the length of the list `finRange n` (which contains all elements of `Fin n` in ascending order) is equal to $n$.

List.getElem_finRange theorem

{i : Nat} (h : i < (List.finRange n).length) : (finRange n)[i] = Fin.cast length_finRange ⟨i, h⟩

Full source

@[simp] theorem getElem_finRange {i : Nat} (h : i < (List.finRange n).length) :
    (finRange n)[i] = Fin.cast length_finRange ⟨i, h⟩ := by
  simp [List.finRange]

Indexing in `finRange` Preserves Value via Casting

Informal description

For any natural number $i$ such that $i < \text{length}(\text{finRange } n)$, the $i$-th element of the list $\text{finRange } n$ is equal to the natural number $i$ cast as an element of $\text{Fin } n$ via the equality $\text{length}(\text{finRange } n) = n$.

List.finRange_zero theorem

: finRange 0 = []

Full source

@[simp] theorem finRange_zero : finRange 0 = [] := by simp [finRange, ofFn]

Empty Finite Range Yields Empty List

Informal description

For the empty finite set `Fin 0`, the list `finRange 0` is equal to the empty list `[]`.

List.finRange_succ theorem

{n} : finRange (n + 1) = 0 :: (finRange n).map Fin.succ

Full source

theorem finRange_succ {n} : finRange (n+1) = 0 :: (finRange n).map Fin.succ := by
  apply List.ext_getElem; simp; intro i; cases i <;> simp

Recursive Construction of $\text{finRange}(n + 1)$ via Successor Mapping

Informal description

For any natural number $n$, the list $\text{finRange}(n + 1)$ containing all elements of $\text{Fin}(n + 1)$ in ascending order is equal to the list obtained by prepending $0$ to the list $\text{finRange}(n)$ where each element is mapped via the successor function $\text{Fin.succ}$.

List.finRange_succ_last theorem

{n} : finRange (n + 1) = (finRange n).map Fin.castSucc ++ [Fin.last n]

Full source

theorem finRange_succ_last {n} :
    finRange (n+1) = (finRange n).map Fin.castSucc ++ [Fin.last n] := by
  apply List.ext_getElem
  · simp
  · intros
    simp only [List.finRange, List.getElem_ofFn, getElem_append, length_map, length_ofFn,
      getElem_map, Fin.castSucc_mk, getElem_singleton]
    split
    · rfl
    · next h => exact Fin.eq_last_of_not_lt h

Recursive construction of $\text{finRange}(n+1)$ via casting and last element

Informal description

For any natural number $n$, the list $\text{finRange}(n + 1)$ containing all elements of $\text{Fin}(n + 1)$ in ascending order is equal to the concatenation of the list $\text{finRange}(n)$ with each element cast via $\text{Fin.castSucc}$ and the singleton list containing $\text{Fin.last}\ n$.

List.finRange_reverse theorem

{n} : (finRange n).reverse = (finRange n).map Fin.rev

Full source

theorem finRange_reverse {n} : (finRange n).reverse = (finRange n).map Fin.rev := by
  induction n with
  | zero => simp
  | succ n ih =>
    conv => lhs; rw [finRange_succ_last]
    conv => rhs; rw [finRange_succ]
    rw [reverse_append, reverse_cons, reverse_nil, nil_append, singleton_append, ← map_reverse,
      map_cons, ih, map_map, map_map]
    congr; funext
    simp [Fin.rev_succ]

Reversed Finite Range Equals Mapped Reversal: $(\text{finRange}(n))^{\text{rev}} = \text{map Fin.rev} (\text{finRange}(n))$

Informal description

For any natural number $n$, the reverse of the list $\text{finRange}(n)$ (which contains all elements of $\text{Fin}(n)$ in ascending order) is equal to the list obtained by applying the reversal function $\text{Fin.rev}$ to each element of $\text{finRange}(n)$. That is, $$ (\text{finRange}(n))^{\text{rev}} = \text{map Fin.rev} (\text{finRange}(n)). $$