Tail recursive implementations for List definitions.

Many of the proofs require theorems about Array, so these are in a separate file to minimize imports.

If you import Init.Data.List.Basic but do not import this file, then at runtime you will get non-tail recursive versions of the following definitions.

Basic List operations.

The following operations are already tail-recursive, and do not need @[csimp] replacements: get, foldl, beq, isEqv, reverse, elem (and hence contains), drop, dropWhile, partition, isPrefixOf, isPrefixOf?, find?, findSome?, lookup, any (and hence or), all (and hence and) , range, eraseDups, eraseReps, span, splitBy.

The following operations are still missing @[csimp] replacements: concat, zipWithAll.

The following operations are not recursive to begin with (or are defined in terms of recursive primitives): isEmpty, isSuffixOf, isSuffixOf?, rotateLeft, rotateRight, insert, zip, enum, min?, max?, and removeAll.

The following operations were already given @[csimp] replacements in Init/Data/List/Basic.lean: length, map, filter, replicate, leftPad, unzip, range', iota, intersperse.

The following operations are given @[csimp] replacements below: set, filterMap, foldr, append, bind, join, take, takeWhile, dropLast, replace, modify, insertIdx, erase, eraseIdx, zipWith, enumFrom, and intercalate.

set

@[inline]

def List.setTR {α : Type u_1} (l : List α) (n : Nat) (a : α) : List α

Replaces the value at (zero-based) index n in l with a. If the index is out of bounds, then the list is returned unmodified.

This is a tail-recursive version of List.set that's used at runtime.

Examples:

• ["water", "coffee", "soda", "juice"].set 1 "tea" = ["water", "tea", "soda", "juice"]
• ["water", "coffee", "soda", "juice"].set 4 "tea" = ["water", "coffee", "soda", "juice"]

Equations

• l.setTR n a = List.setTR.go l a l n #[]

def List.setTR.go {α : Type u_1} (l : List α) (a : α) : List α → Nat → Array α → List α

Auxiliary for setTR: setTR.go l a xs n acc = acc.toList ++ set xs a, unless n ≥ l.length in which case it returns l

Equations

• List.setTR.go l a [] x✝¹ x✝ = l
• List.setTR.go l a (head :: xs) 0 x✝ = x✝.toListAppend (a :: xs)
• List.setTR.go l a (x_3 :: xs) n.succ x✝ = List.setTR.go l a xs n (x✝.push x_3)

@[csimp]

theorem List.set_eq_setTR : @set = @setTR

theorem List.set_eq_setTR.go (α : Type u_1) (l : List α) (a : α) (acc : Array α) (xs : List α) (i : Nat) : l = acc.toList ++ xs → setTR.go l a xs i acc = acc.toList ++ xs.set i a

filterMap

@[inline]

def List.filterMapTR {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) : List β

Applies a function that returns an Option to each element of a list, collecting the non-none values.

O(|l|). This is a tail-recursive version of List.filterMap, used at runtime.

Example:

#eval [1, 2, 5, 2, 7, 7].filterMapTR fun x =>
  if x > 2 then some (2 * x) else none

[10, 14, 14]

Equations

• List.filterMapTR f l = List.filterMapTR.go f l #[]

@[specialize #[]]

def List.filterMapTR.go {α : Type u_1} {β : Type u_2} (f : α → Option β) : List α → Array β → List β

Auxiliary for filterMap: filterMap.go f l = acc.toList ++ filterMap f l

Equations

• List.filterMapTR.go f [] x✝ = x✝.toList
• List.filterMapTR.go f (a :: as) x✝ = match f a with | none => List.filterMapTR.go f as x✝ | some b => List.filterMapTR.go f as (x✝.push b)

@[csimp]

theorem List.filterMap_eq_filterMapTR : @filterMap = @filterMapTR

theorem List.filterMap_eq_filterMapTR.go (α : Type u_2) (β : Type u_1) (f : α → Option β) (as : List α) (acc : Array β) : filterMapTR.go f as acc = acc.toList ++ filterMap f as

foldr

@[specialize #[]]

def List.foldrTR {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (l : List α) : β

Folds a function over a list from the right, accumulating a value starting with init. The accumulated value is combined with the each element of the list in reverse order, using f.

O(|l|). This is the tail-recursive replacement for List.foldr in runtime code.

Examples:

• [a, b, c].foldrTR f init = f a (f b (f c init))
• [1, 2, 3].foldrTR (toString · ++ ·) "" = "123"
• [1, 2, 3].foldrTR (s!"({·} {·})") "!" = "(1 (2 (3 !)))"

Equations

• List.foldrTR f init l = Array.foldr f init l.toArray

@[csimp]

theorem List.foldr_eq_foldrTR : @foldr = @foldrTR

flatMap

@[inline]

def List.flatMapTR {α : Type u_1} {β : Type u_2} (f : α → List β) (as : List α) : List β

Applies a function that returns a list to each element of a list, and concatenates the resulting lists.

This is the tail-recursive version of List.flatMap that's used at runtime.

Examples:

• [2, 3, 2].flatMapTR List.range = [0, 1, 0, 1, 2, 0, 1]
• ["red", "blue"].flatMapTR String.toList = ['r', 'e', 'd', 'b', 'l', 'u', 'e']

Equations

• List.flatMapTR f as = List.flatMapTR.go f as #[]

@[specialize #[]]

def List.flatMapTR.go {α : Type u_1} {β : Type u_2} (f : α → List β) : List α → Array β → List β

Auxiliary for flatMap: flatMap.go f as = acc.toList ++ bind f as

Equations

• List.flatMapTR.go f [] x✝ = x✝.toList
• List.flatMapTR.go f (a :: as) x✝ = List.flatMapTR.go f as (x✝ ++ f a)

@[csimp]

theorem List.flatMap_eq_flatMapTR : @flatMap = @flatMapTR

theorem List.flatMap_eq_flatMapTR.go (α : Type u_2) (β : Type u_1) (f : α → List β) (as : List α) (acc : Array β) : flatMapTR.go f as acc = acc.toList ++ flatMap f as

flatten

@[inline]

def List.flattenTR {α : Type u_1} (l : List (List α)) : List α

Concatenates a list of lists into a single list, preserving the order of the elements.

O(|flatten L|). This is a tail-recursive version of List.flatten, used in runtime code.

Examples:

• [["a"], ["b", "c"]].flattenTR = ["a", "b", "c"]
• [["a"], [], ["b", "c"], ["d", "e", "f"]].flattenTR = ["a", "b", "c", "d", "e", "f"]

Equations

• l.flattenTR = List.flatMapTR id l

@[csimp]

theorem List.flatten_eq_flattenTR : @flatten = @flattenTR

Sublists

take

@[inline]

def List.takeTR {α : Type u_1} (n : Nat) (l : List α) : List α

Extracts the first n elements of xs, or the whole list if n is greater than xs.length.

O(min n |xs|). This is a tail-recursive version of List.take, used at runtime.

Examples:

• [a, b, c, d, e].takeTR 0 = []
• [a, b, c, d, e].takeTR 3 = [a, b, c]
• [a, b, c, d, e].takeTR 6 = [a, b, c, d, e]

Equations

• List.takeTR n l = List.takeTR.go l l n #[]

@[specialize #[]]

def List.takeTR.go {α : Type u_1} (l : List α) : List α → Nat → Array α → List α

Auxiliary for take: take.go l xs n acc = acc.toList ++ take n xs, unless n ≥ xs.length in which case it returns l.

Equations

• List.takeTR.go l [] x✝¹ x✝ = l
• List.takeTR.go l (head :: xs) 0 x✝ = x✝.toList
• List.takeTR.go l (x_3 :: xs) n.succ x✝ = List.takeTR.go l xs n (x✝.push x_3)

@[csimp]

theorem List.take_eq_takeTR : @take = @takeTR

takeWhile

@[inline]

def List.takeWhileTR {α : Type u_1} (p : α → Bool) (l : List α) : List α

Returns the longest initial segment of xs for which p returns true.

O(|xs|). This is a tail-recursive version of List.take, used at runtime.

Examples:

• [7, 6, 4, 8].takeWhileTR (· > 5) = [7, 6]
• [7, 6, 6, 5].takeWhileTR (· > 5) = [7, 6, 6]
• [7, 6, 6, 8].takeWhileTR (· > 5) = [7, 6, 6, 8]

Equations

• List.takeWhileTR p l = List.takeWhileTR.go p l l #[]

@[specialize #[]]

def List.takeWhileTR.go {α : Type u_1} (p : α → Bool) (l : List α) : List α → Array α → List α

Auxiliary for takeWhile: takeWhile.go p l xs acc = acc.toList ++ takeWhile p xs, unless no element satisfying p is found in xs in which case it returns l.

Equations

• List.takeWhileTR.go p l [] x✝ = l
• List.takeWhileTR.go p l (a :: as) x✝ = bif p a then List.takeWhileTR.go p l as (x✝.push a) else x✝.toList

@[csimp]

theorem List.takeWhile_eq_takeWhileTR : @takeWhile = @takeWhileTR

dropLast

@[inline]

def List.dropLastTR {α : Type u_1} (l : List α) : List α

Removes the last element of the list, if one exists.

This is a tail-recursive version of List.dropLast, used at runtime.

Examples:

• [].dropLastTR = []
• ["tea"].dropLastTR = []
• ["tea", "coffee", "juice"].dropLastTR = ["tea", "coffee"]

Equations

• l.dropLastTR = l.toArray.pop.toList

@[csimp]

theorem List.dropLast_eq_dropLastTR : @dropLast = @dropLastTR

Manipulating elements

replace

@[inline]

def List.replaceTR {α : Type u_1} [BEq α] (l : List α) (b c : α) : List α

Replaces the first element of the list l that is equal to a with b. If no element is equal to a, then the list is returned unchanged.

O(|l|). This is a tail-recursive version of List.replace that's used in runtime code.

Examples:

• [1, 4, 2, 3, 3, 7].replaceTR 3 6 = [1, 4, 2, 6, 3, 7]
• [1, 4, 2, 3, 3, 7].replaceTR 5 6 = [1, 4, 2, 3, 3, 7]

Equations

• l.replaceTR b c = List.replaceTR.go l b c l #[]

@[specialize #[]]

def List.replaceTR.go {α : Type u_1} [BEq α] (l : List α) (b c : α) : List α → Array α → List α

Auxiliary for replace: replace.go l b c xs acc = acc.toList ++ replace xs b c, unless b is not found in xs in which case it returns l.

Equations

• List.replaceTR.go l b c [] x✝ = l
• List.replaceTR.go l b c (a :: as) x✝ = bif b == a then x✝.toListAppend (c :: as) else List.replaceTR.go l b c as (x✝.push a)

@[csimp]

theorem List.replace_eq_replaceTR : @replace = @replaceTR

modify

def List.modifyTR {α : Type u_1} (l : List α) (i : Nat) (f : α → α) : List α

Replaces the element at the given index, if it exists, with the result of applying f to it.

This is a tail-recursive version of List.modify.

Examples:

• [1, 2, 3].modifyTR 0 (· * 10) = [10, 2, 3]
• [1, 2, 3].modifyTR 2 (· * 10) = [1, 2, 30]
• [1, 2, 3].modifyTR 3 (· * 10) = [1, 2, 3]

Equations

• l.modifyTR i f = List.modifyTR.go f l i #[]

def List.modifyTR.go {α : Type u_1} (f : α → α) : List α → Nat → Array α → List α

Auxiliary for modifyTR: modifyTR.go f l i acc = acc.toList ++ modify f i l.

Equations

• List.modifyTR.go f [] x✝¹ x✝ = x✝.toList
• List.modifyTR.go f (head :: xs) 0 x✝ = x✝.toListAppend (f head :: xs)
• List.modifyTR.go f (x_3 :: xs) n.succ x✝ = List.modifyTR.go f xs n (x✝.push x_3)

theorem List.modifyTR_go_eq {α✝ : Type u_1} {f : α✝ → α✝} {acc : Array α✝} (l : List α✝) (i : Nat) : modifyTR.go f l i acc = acc.toList ++ l.modify i f

@[csimp]

theorem List.modify_eq_modifyTR : @modify = @modifyTR

insertIdx

@[inline]

def List.insertIdxTR {α : Type u_1} (l : List α) (n : Nat) (a : α) : List α

Inserts an element into a list at the specified index. If the index is greater than the length of the list, then the list is returned unmodified.

In other words, the new element is inserted into the list l after the first i elements of l.

This is a tail-recursive version of List.insertIdx, used at runtime.

Examples:

• ["tues", "thur", "sat"].insertIdxTR 1 "wed" = ["tues", "wed", "thur", "sat"]
• ["tues", "thur", "sat"].insertIdxTR 2 "wed" = ["tues", "thur", "wed", "sat"]
• ["tues", "thur", "sat"].insertIdxTR 3 "wed" = ["tues", "thur", "sat", "wed"]
• ["tues", "thur", "sat"].insertIdxTR 4 "wed" = ["tues", "thur", "sat"]

Equations

• l.insertIdxTR n a = List.insertIdxTR.go a n l #[]

def List.insertIdxTR.go {α : Type u_1} (a : α) : Nat → List α → Array α → List α

Auxiliary for insertIdxTR: insertIdxTR.go a n l acc = acc.toList ++ insertIdx n a l.

Equations

• List.insertIdxTR.go a 0 x✝¹ x✝ = x✝.toListAppend (a :: x✝¹)
• List.insertIdxTR.go a x✝¹ [] x✝ = x✝.toList
• List.insertIdxTR.go a n.succ (a_1 :: l) x✝ = List.insertIdxTR.go a n l (x✝.push a_1)

theorem List.insertIdxTR_go_eq {α✝ : Type u_1} {a : α✝} {acc : Array α✝} (i : Nat) (l : List α✝) : insertIdxTR.go a i l acc = acc.toList ++ l.insertIdx i a

@[csimp]

theorem List.insertIdx_eq_insertIdxTR : @insertIdx = @insertIdxTR

erase

@[inline]

def List.eraseTR {α : Type u_1} [BEq α] (l : List α) (a : α) : List α

Removes the first occurrence of a from l. If a does not occur in l, the list is returned unmodified.

O(|l|).

This is a tail-recursive version of List.erase, used in runtime code.

Examples:

• [1, 5, 3, 2, 5].eraseTR 5 = [1, 3, 2, 5]
• [1, 5, 3, 2, 5].eraseTR 6 = [1, 5, 3, 2, 5]

Equations

• l.eraseTR a = List.eraseTR.go l a l #[]

def List.eraseTR.go {α : Type u_1} [BEq α] (l : List α) (a : α) : List α → Array α → List α

Auxiliary for eraseTR: eraseTR.go l a xs acc = acc.toList ++ erase xs a, unless a is not present in which case it returns l

Equations

• List.eraseTR.go l a [] x✝ = l
• List.eraseTR.go l a (a_1 :: as) x✝ = bif a_1 == a then x✝.toListAppend as else List.eraseTR.go l a as (x✝.push a_1)

@[csimp]

theorem List.erase_eq_eraseTR : @List.erase = @eraseTR

@[inline]

def List.erasePTR {α : Type u_1} (p : α → Bool) (l : List α) : List α

Removes the first element of a list for which p returns true. If no element satisfies p, then the list is returned unchanged.

This is a tail-recursive version of eraseP, used at runtime.

Examples:

• [2, 1, 2, 1, 3, 4].erasePTR (· < 2) = [2, 2, 1, 3, 4]
• [2, 1, 2, 1, 3, 4].erasePTR (· > 2) = [2, 1, 2, 1, 4]
• [2, 1, 2, 1, 3, 4].erasePTR (· > 8) = [2, 1, 2, 1, 3, 4]

Equations

• List.erasePTR p l = List.erasePTR.go p l l #[]

@[specialize #[]]

def List.erasePTR.go {α : Type u_1} (p : α → Bool) (l : List α) : List α → Array α → List α

Auxiliary for erasePTR: erasePTR.go p l xs acc = acc.toList ++ eraseP p xs, unless xs does not contain any elements satisfying p, where it returns l.

Equations

• List.erasePTR.go p l [] x✝ = l
• List.erasePTR.go p l (a :: as) x✝ = bif p a then x✝.toListAppend as else List.erasePTR.go p l as (x✝.push a)

@[csimp]

theorem List.eraseP_eq_erasePTR : @eraseP = @erasePTR

theorem List.eraseP_eq_erasePTR.go (α : Type u_1) (p : α → Bool) (l : List α) (acc : Array α) (xs : List α) : l = acc.toList ++ xs → erasePTR.go p l xs acc = acc.toList ++ eraseP p xs

eraseIdx

@[inline]

def List.eraseIdxTR {α : Type u_1} (l : List α) (n : Nat) : List α

Removes the element at the specified index. If the index is out of bounds, the list is returned unmodified.

O(i).

This is a tail-recursive version of List.eraseIdx, used at runtime.

Examples:

• [0, 1, 2, 3, 4].eraseIdxTR 0 = [1, 2, 3, 4]
• [0, 1, 2, 3, 4].eraseIdxTR 1 = [0, 2, 3, 4]
• [0, 1, 2, 3, 4].eraseIdxTR 5 = [0, 1, 2, 3, 4]

Equations

• l.eraseIdxTR n = List.eraseIdxTR.go l l n #[]

def List.eraseIdxTR.go {α : Type u_1} (l : List α) : List α → Nat → Array α → List α

Auxiliary for eraseIdxTR: eraseIdxTR.go l n xs acc = acc.toList ++ eraseIdx xs a, unless a is not present in which case it returns l

Equations

• List.eraseIdxTR.go l [] x✝¹ x✝ = l
• List.eraseIdxTR.go l (head :: xs) 0 x✝ = x✝.toListAppend xs
• List.eraseIdxTR.go l (x_3 :: xs) n.succ x✝ = List.eraseIdxTR.go l xs n (x✝.push x_3)

@[csimp]

theorem List.eraseIdx_eq_eraseIdxTR : @eraseIdx = @eraseIdxTR

Zippers

zipWith

@[inline]

def List.zipWithTR {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (as : List α) (bs : List β) : List γ

Applies a function to the corresponding elements of two lists, stopping at the end of the shorter list.

O(min |xs| |ys|). This is a tail-recursive version of List.zipWith that's used at runtime.

Examples:

• [1, 2].zipWithTR (· + ·) [5, 6] = [6, 8]
• [1, 2, 3].zipWithTR (· + ·) [5, 6, 10] = [6, 8, 13]
• [].zipWithTR (· + ·) [5, 6] = []
• [x₁, x₂, x₃].zipWithTR f [y₁, y₂, y₃, y₄] = [f x₁ y₁, f x₂ y₂, f x₃ y₃]

Equations

• List.zipWithTR f as bs = List.zipWithTR.go f as bs #[]

def List.zipWithTR.go {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) : List α → List β → Array γ → List γ

Auxiliary for zipWith: zipWith.go f as bs acc = acc.toList ++ zipWith f as bs

Equations

• List.zipWithTR.go f (a :: as) (b :: bs) x✝ = List.zipWithTR.go f as bs (x✝.push (f a b))
• List.zipWithTR.go f x✝² x✝¹ x✝ = x✝.toList

@[csimp]

theorem List.zipWith_eq_zipWithTR : @zipWith = @zipWithTR

theorem List.zipWith_eq_zipWithTR.go (α : Type u_3) (β : Type u_2) (γ : Type u_1) (f : α → β → γ) (as : List α) (bs : List β) (acc : Array γ) : zipWithTR.go f as bs acc = acc.toList ++ zipWith f as bs

Ranges and enumeration

zipIdx

def List.zipIdxTR {α : Type u_1} (l : List α) (n : Nat := 0) : List (α × Nat)

Pairs each element of a list with its index, optionally starting from an index other than 0.

O(|l|). This is a tail-recursive version of List.zipIdx that's used at runtime.

Examples:

• [a, b, c].zipIdxTR = [(a, 0), (b, 1), (c, 2)]
• [a, b, c].zipIdxTR 5 = [(a, 5), (b, 6), (c, 7)]

Equations

• One or more equations did not get rendered due to their size.

@[csimp]

theorem List.zipIdx_eq_zipIdxTR : @zipIdx = @zipIdxTR

theorem List.zipIdx_eq_zipIdxTR.go (α : Type u_1) (l : List α) (i : Nat) : let f := fun (a : α) (x : Nat × List (α × Nat)) => match x with | (n, acc) => (n - 1, (a, n - 1) :: acc); foldr f (i + l.length, []) l = (i, l.zipIdx i)

enumFrom

@[deprecated List.zipIdxTR (since := "2025-01-21")]

def List.enumFromTR {α : Type u_1} (n : Nat) (l : List α) : List (Nat × α)

Tail recursive version of List.enumFrom.

Equations

• One or more equations did not get rendered due to their size.

@[csimp, deprecated List.zipIdx_eq_zipIdxTR (since := "2025-01-21")]

theorem List.enumFrom_eq_enumFromTR : @enumFrom = @enumFromTR

theorem List.enumFrom_eq_enumFromTR.go (α : Type u_1) (l : List α) (n : Nat) : let f := fun (a : α) (x : Nat × List (Nat × α)) => match x with | (n, acc) => (n - 1, (n - 1, a) :: acc); foldr f (n + l.length, []) l = (n, enumFrom n l)

Other list operations

intercalate

def List.intercalateTR {α : Type u_1} (sep : List α) (xs : List (List α)) : List α

Alternates the lists in xs with the separator sep.

This is a tail-recursive version of List.intercalate used at runtime.

Examples:

• List.intercalateTR sep [] = []
• List.intercalateTR sep [a] = a
• List.intercalateTR sep [a, b] = a ++ sep ++ b
• List.intercalateTR sep [a, b, c] = a ++ sep ++ b ++ sep ++ c

Equations

• sep.intercalateTR [] = []
• sep.intercalateTR [x_1] = x_1
• sep.intercalateTR (x_1 :: xs) = List.intercalateTR.go sep.toArray x_1 xs #[]

def List.intercalateTR.go {α : Type u_1} (sep : Array α) : List α → List (List α) → Array α → List α

Auxiliary for intercalateTR: intercalateTR.go sep x xs acc = acc.toList ++ intercalate sep.toList (x::xs)

Equations

• List.intercalateTR.go sep x✝¹ [] x✝ = x✝.toListAppend x✝¹
• List.intercalateTR.go sep x✝¹ (y :: xs) x✝ = List.intercalateTR.go sep y xs (x✝ ++ x✝¹ ++ sep)

@[csimp]

theorem List.intercalate_eq_intercalateTR : @intercalate = @intercalateTR

theorem List.intercalate_eq_intercalateTR.go (α : Type u_1) (sep : List α) {acc : Array α} {x : List α} (xs : List (List α)) : intercalateTR.go sep.toArray x xs acc = acc.toList ++ (intersperse sep (x :: xs)).flatten