English
IterateTR is a tail-recursive variant of iterate, defined as iterateTR f a n = loop a n [] where loop(a,0,l) = reverse l and loop(a,n+1,l) = loop(f(a), n, a::l). In particular, iterateTR is equivalent to iterate up to equality of functions on lists.
Русский
IterateTR — хвостовая рекурсия для iterate: iterateTR f a n = loop a n [], где loop(a,0,l) = reverse l и loop(a,n+1,l) = loop(f(a), n, a::l). Таким образом, iterateTR эквивалентен iterate как функции.
LaTeX
$$$$\operatorname{iterateTR}(f,a,n) = \text{loop } a\ n\, []\quad\text{with}\quad \text{loop}(a,0,l)=\operatorname{reverse}(l),\ \text{loop}(a,n+1,l)=\text{loop}(f(a),n,a\mathbin{::}l).$$$$
Lean4
/-- Tail-recursive version of `List.iterate`. -/
@[inline]
def iterateTR (f : α → α) (a : α) (n : ℕ) : List α :=
loop a n []
where/-- `iterateTR.loop f a n l := iterate f a n ++ reverse l`. -/
@[simp, specialize] loop (a : α) (n : ℕ) (l : List α) : List α :=
match n with
| 0 => reverse l
| n + 1 => loop (f a) n (a :: l)
