Mathlib.Data.List.Iterate

List.length_iterate theorem

(f : α → α) (a : α) (n : ℕ) : length (iterate f a n) = n

Full source

@[simp]
theorem length_iterate (f : α → α) (a : α) (n : ℕ) : length (iterate f a n) = n := by
  induction n generalizing a <;> simp [*]

Length of Iterated Function Application List Equals Iteration Count

Informal description

For any function $f : \alpha \to \alpha$, initial value $a \in \alpha$, and natural number $n$, the length of the list obtained by iterating $f$ starting from $a$ $n$ times is equal to $n$. That is, $\text{length}(\text{iterate}\,f\,a\,n) = n$.

List.iterate_eq_nil theorem

{f : α → α} {a : α} {n : ℕ} : iterate f a n = [] ↔ n = 0

Full source

@[simp]
theorem iterate_eq_nil {f : α → α} {a : α} {n : ℕ} : iterateiterate f a n = [] ↔ n = 0 := by
  rw [← length_eq_zero_iff, length_iterate]

Empty Iteration List iff Zero Iterations

Informal description

For any function $f : \alpha \to \alpha$, initial value $a \in \alpha$, and natural number $n$, the list obtained by iterating $f$ starting from $a$ $n$ times is empty if and only if $n = 0$. That is, $\text{iterate}\,f\,a\,n = [] \leftrightarrow n = 0$.

List.getElem?_iterate theorem

(f : α → α) (a : α) : ∀ (n i : ℕ), i < n → (iterate f a n)[i]? = f^[i] a

Full source

theorem getElem?_iterate (f : α → α) (a : α) :
    ∀ (n i : ℕ), i < n → (iterate f a n)[i]? = f^[i] a
  | n + 1, 0    , _ => by simp
  | n + 1, i + 1, h => by simp [getElem?_iterate f (f a) n i (by simpa using h)]

Element Access in Iterated Function List Equals Function Iterate

Informal description

For any function $f : \alpha \to \alpha$, initial value $a \in \alpha$, and natural numbers $n$ and $i$ such that $i < n$, the $i$-th element (if it exists) of the list obtained by iterating $f$ starting from $a$ $n$ times is equal to the $i$-th iterate of $f$ applied to $a$. That is, $(\text{iterate}\,f\,a\,n)[i]? = f^{[i]}(a)$.

List.getElem_iterate theorem

(f : α → α) (a : α) (n : ℕ) (i : Nat) (h : i < (iterate f a n).length) : (iterate f a n)[i] = f^[i] a

Full source

@[simp]
theorem getElem_iterate (f : α → α) (a : α) (n : ℕ) (i : Nat) (h : i < (iterate f a n).length) :
    (iterate f a n)[i] = f^[i] a :=
  (getElem_eq_iff _).2 <| getElem?_iterate _ _ _ _ <| by rwa [length_iterate] at h

Element Access in Iterated List Equals Function Iterate

Informal description

For any function $f : \alpha \to \alpha$, initial value $a \in \alpha$, natural number $n$, and index $i$ such that $i$ is less than the length of the list $\text{iterate}\,f\,a\,n$, the $i$-th element of this list equals the $i$-th iterate of $f$ applied to $a$. That is, $(\text{iterate}\,f\,a\,n)[i] = f^{[i]}(a)$.

List.mem_iterate theorem

{f : α → α} {a : α} {n : ℕ} {b : α} : b ∈ iterate f a n ↔ ∃ m < n, b = f^[m] a

Full source

@[simp]
theorem mem_iterate {f : α → α} {a : α} {n : ℕ} {b : α} :
    b ∈ iterate f a nb ∈ iterate f a n ↔ ∃ m < n, b = f^[m] a := by
  simp [List.mem_iff_get, Fin.exists_iff, eq_comm (b := b)]

Membership in Iterated Function List Equals Existence of Iterate Index

Informal description

For any function $f : \alpha \to \alpha$, initial value $a \in \alpha$, natural number $n$, and element $b \in \alpha$, the element $b$ is in the list $\text{iterate}\,f\,a\,n$ if and only if there exists a natural number $m < n$ such that $b = f^{[m]}(a)$, where $f^{[m]}$ denotes the $m$-th iterate of $f$.

List.range_map_iterate theorem

(n : ℕ) (f : α → α) (a : α) : (List.range n).map (f^[·] a) = List.iterate f a n

Full source

@[simp]
theorem range_map_iterate (n : ℕ) (f : α → α) (a : α) :
    (List.range n).map (f^[·] a) = List.iterate f a n := by
  apply List.ext_getElem <;> simp

Range Map of Function Iterates Equals Iterated List

Informal description

For any natural number $n$, function $f : \alpha \to \alpha$, and initial value $a \in \alpha$, the list obtained by mapping the function $\lambda m, f^{[m]}(a)$ (the $m$-th iterate of $f$ applied to $a$) over the range $[0, \dots, n-1]$ is equal to the list $\text{iterate}\,f\,a\,n$. That is, $$ \text{map}\,(\lambda m, f^{[m]}(a))\,(\text{range}\,n) = \text{iterate}\,f\,a\,n. $$

List.iterate_add theorem

(f : α → α) (a : α) (m n : ℕ) : iterate f a (m + n) = iterate f a m ++ iterate f (f^[m] a) n

Full source

theorem iterate_add (f : α → α) (a : α) (m n : ℕ) :
    iterate f a (m + n) = iterate f a m ++ iterate f (f^[m] a) n := by
  induction m generalizing a with
  | zero => simp
  | succ n ih => rw [iterate, add_right_comm, iterate, ih, Nat.iterate, cons_append]

Additivity of Function Iteration Lists

Informal description

For any function $f : \alpha \to \alpha$, initial value $a \in \alpha$, and natural numbers $m, n$, the list obtained by iterating $f$ on $a$ for $m + n$ steps is equal to the concatenation of: 1. The list obtained by iterating $f$ on $a$ for $m$ steps, and 2. The list obtained by iterating $f$ on $f^m(a)$ for $n$ steps. In symbols: $\text{iterate}\,f\,a\,(m + n) = \text{iterate}\,f\,a\,m +\!\!\!+\,\text{iterate}\,f\,(f^m(a))\,n$.

List.take_iterate theorem

(f : α → α) (a : α) (m n : ℕ) : take m (iterate f a n) = iterate f a (min m n)

Full source

theorem take_iterate (f : α → α) (a : α) (m n : ℕ) :
    take m (iterate f a n) = iterate f a (min m n) := by
  rw [← range_map_iterate, ← range_map_iterate, ← map_take, take_range]

Taking Prefix of Iterated List Equals Iterated List of Minimum Length

Informal description

For any function $f : \alpha \to \alpha$, initial value $a \in \alpha$, and natural numbers $m, n$, taking the first $m$ elements of the iterated list $\text{iterate}\,f\,a\,n$ is equal to the iterated list $\text{iterate}\,f\,a\,(\min(m, n))$. That is, $$ \text{take}\,m\,(\text{iterate}\,f\,a\,n) = \text{iterate}\,f\,a\,(\min(m, n)). $$