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 α

Tail recursive version of List.set.

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 β

Tail recursive version of filterMap.

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 α) : β

Tail recursive version of List.foldr.

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 β

Tail recursive version of List.flatMap.

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 α

Tail recursive version of List.flatten.

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 α

Tail recursive version of List.take.

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 α

Tail recursive version of List.takeWhile.

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 α

Tail recursive version of dropLast.

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 α

Tail recursive version of List.replace.

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} (f : α → α) (n : Nat) (l : List α) : List α

Tail-recursive version of modify.

Equations

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

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

Auxiliary for modifyTR: modifyTR.go f l n acc = acc.toList ++ modify f n 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 ++ modify f i l

@[csimp]

theorem List.modify_eq_modifyTR : @modify = @modifyTR

insertIdx

@[inline]

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

Tail-recursive version of insertIdx.

Equations

• List.insertIdxTR n a l = 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 ++ insertIdx i a l

@[csimp]

theorem List.insertIdx_eq_insertIdxTR : @insertIdx = @insertIdxTR

erase

@[inline]

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

Tail recursive version of List.erase.

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 α

Tail-recursive version of eraseP.

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 α

Tail recursive version of List.eraseIdx.

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 γ

Tail recursive version of List.zipWith.

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)

Tail recursive version of List.zipIdx.

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 α) : List (List α) → List α

Tail recursive version of List.intercalate.

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