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 #[]

@[csimp]

theorem List.set_eq_setTR : @set = @setTR

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

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 #[]

@[csimp]

theorem List.flatMap_eq_flatMapTR : @flatMap = @flatMapTR

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 #[]

@[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 #[]

@[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

Finding elements

def List.findRev?TR {α : Type u_1} (p : α → Bool) (l : List α) : Option α

Tail recursive implementation of findRev?. This is only used at runtime.

Equations

• List.findRev?TR p l = List.find? p l.reverse

@[simp]

theorem List.find?_singleton {α : Type u_1} {p : α → Bool} {a : α} : find? p [a] = if p a = true then some a else none

@[simp]

theorem List.find?_append {α : Type u_1} {p : α → Bool} {xs ys : List α} : find? p (xs ++ ys) = (find? p xs).or (find? p ys)

@[csimp]

theorem List.findRev?_eq_findRev?TR : @findRev? = @findRev?TR

@[simp]

theorem List.findRev?_eq_find?_reverse {α : Type u_1} {l : List α} {p : α → Bool} : findRev? p l = find? p l.reverse

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

Tail recursive implementation of finSomedRev?. This is only used at runtime.

Equations

• List.findSomeRev?TR f l = List.findSome? f l.reverse

@[simp]

theorem List.findSome?_singleton {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} {a : α} : findSome? f [a] = f a

@[simp]

theorem List.findSome?_append {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} {xs ys : List α} : findSome? f (xs ++ ys) = (findSome? f xs).or (findSome? f ys)

@[csimp]

theorem List.findSomeRev?_eq_findSomeRev?TR : @findSomeRev? = @findSomeRev?TR

@[simp]

theorem List.findSomeRev?_eq_findSome?_reverse {α : Type u_1} {β : Type u_2} {l : List α} {f : α → Option β} : findSomeRev? f l = findSome? f l.reverse

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 #[]

@[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 #[]

@[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 #[]

@[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 #[]

@[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 #[]

@[csimp]

theorem List.eraseP_eq_erasePTR : @eraseP = @erasePTR

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 #[]

@[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 #[]

@[csimp]

theorem List.zipWith_eq_zipWithTR : @zipWith = @zipWithTR

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

enumFrom

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 #[]

@[csimp]

theorem List.intercalate_eq_intercalateTR : @intercalate = @intercalateTR