Tail recursive implementations for List definitions.

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

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, groupBy.

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, minimum?, maximum?, and removeAll.

The following operations are given @[csimp] replacements below: length, set, map, filter, filterMap, foldr, append, bind, join, replicate, take, takeWhile, dropLast, replace, erase, eraseIdx, zipWith, unzip, iota, enumFrom, intersperse, and intercalate.

length

theorem List.length_add_eq_lengthTRAux {α : Type u_1} (as : List α) (n : Nat) : as.length + n = as.lengthTRAux n

@[csimp]

theorem List.length_eq_lengthTR : @List.length = @List.lengthTR

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 : @List.set = @List.setTR

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

map

@[inline]

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

Tail-recursive version of List.map.

Equations

• List.mapTR f as = List.mapTR.loop f as []

@[specialize #[]]

def List.mapTR.loop {α : Type u_1} {β : Type u_2} (f : α → β) : List α → List β → List β

Equations

• List.mapTR.loop f [] x = x.reverse
• List.mapTR.loop f (a :: as) x = List.mapTR.loop f as (f a :: x)

theorem List.mapTR_loop_eq {α : Type u_1} {β : Type u_2} (f : α → β) (as : List α) (bs : List β) : List.mapTR.loop f as bs = bs.reverse ++ List.map f as

@[csimp]

theorem List.map_eq_mapTR : @List.map = @List.mapTR

filter

@[inline]

def List.filterTR {α : Type u_1} (p : α → Bool) (as : List α) : List α

Tail-recursive version of List.filter.

Equations

• List.filterTR p as = List.filterTR.loop p as []

@[specialize #[]]

def List.filterTR.loop {α : Type u_1} (p : α → Bool) : List α → List α → List α

Equations

• List.filterTR.loop p [] x = x.reverse
• List.filterTR.loop p (a :: as) x = match p a with | true => List.filterTR.loop p as (a :: x) | false => List.filterTR.loop p as x

theorem List.filterTR_loop_eq {α : Type u_1} (p : α → Bool) (as : List α) (bs : List α) : List.filterTR.loop p as bs = bs.reverse ++ List.filter p as

@[csimp]

theorem List.filter_eq_filterTR : @List.filter = @List.filterTR

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 : @List.filterMap = @List.filterMapTR

theorem List.filterMap_eq_filterMapTR.go (α : Type u_2) (β : Type u_1) (f : α → Option β) (as : List α) (acc : Array β) : List.filterMapTR.go f as acc = acc.data ++ List.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 (List.toArray l)

@[csimp]

theorem List.foldr_eq_foldrTR : @List.foldr = @List.foldrTR

bind

@[inline]

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

Tail recursive version of List.bind.

Equations

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

@[specialize #[]]

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

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

Equations

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

@[csimp]

theorem List.bind_eq_bindTR : @List.bind = @List.bindTR

theorem List.bind_eq_bindTR.go (α : Type u_2) (β : Type u_1) (f : α → List β) (as : List α) (acc : Array β) : List.bindTR.go f as acc = acc.data ++ as.bind f

join

@[inline]

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

Tail recursive version of List.join.

Equations

• l.joinTR = l.bindTR id

@[csimp]

theorem List.join_eq_joinTR : @List.join = @List.joinTR

replicate

def List.replicateTR {α : Type u} (n : Nat) (a : α) : List α

Tail-recursive version of List.replicate.

Equations

• List.replicateTR n a = List.replicateTR.loop a n []

def List.replicateTR.loop {α : Type u} (a : α) : Nat → List α → List α

Equations

• List.replicateTR.loop a 0 x = x
• List.replicateTR.loop a n.succ x = List.replicateTR.loop a n (a :: x)

theorem List.replicateTR_loop_replicate_eq {α : Type u_1} (a : α) (m : Nat) (n : Nat) : List.replicateTR.loop a n (List.replicate m a) = List.replicate (n + m) a

theorem List.replicateTR_loop_eq : ∀ {α : Type u_1} {a : α} {acc : List α} (n : Nat), List.replicateTR.loop a n acc = List.replicate n a ++ acc

@[csimp]

theorem List.replicate_eq_replicateTR : @List.replicate = @List.replicateTR

Additional functions

leftpad

@[inline]

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

Optimized version of leftpad.

Equations

• List.leftpadTR n a l = List.replicateTR.loop a (n - l.length) l

@[csimp]

theorem List.leftpad_eq_leftpadTR : @List.leftpad = @List.leftpadTR

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 : @List.take = @List.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 : @List.takeWhile = @List.takeWhileTR

dropLast

@[inline]

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

Tail recursive version of dropLast.

Equations

• l.dropLastTR = (List.toArray l).pop.toList

@[csimp]

theorem List.dropLast_eq_dropLastTR : @List.dropLast = @List.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 : @List.replace = @List.replaceTR

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 = @List.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 : @List.eraseP = @List.erasePTR

theorem List.eraseP_eq_erasePTR.go (α : Type u_1) (p : α → Bool) (l : List α) (acc : Array α) (xs : List α) : l = acc.data ++ xs → List.erasePTR.go p l xs acc = acc.data ++ List.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 : @List.eraseIdx = @List.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 : @List.zipWith = @List.zipWithTR

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

unzip

def List.unzipTR {α : Type u_1} {β : Type u_2} (l : List (α × β)) : List α × List β

Tail recursive version of List.unzip.

Equations

• l.unzipTR = List.foldr (fun (x : α × β) (x_1 : List α × List β) => match x with | (a, b) => match x_1 with | (al, bl) => (a :: al, b :: bl)) ([], []) l

@[csimp]

theorem List.unzip_eq_unzipTR : @List.unzip = @List.unzipTR

Ranges and enumeration

range'

@[inline]

def List.range'TR (s : Nat) (n : Nat) (step : optParam Nat 1) : List Nat

Optimized version of range'.

Equations

• List.range'TR s n step = List.range'TR.go step n (s + step * n) []

def List.range'TR.go (step : optParam Nat 1) : Nat → Nat → List Nat → List Nat

Auxiliary for range'TR: range'TR.go n e = [e-n, ..., e-1] ++ acc.

Equations

• List.range'TR.go step 0 x✝ x = x
• List.range'TR.go step n.succ x✝ x = List.range'TR.go step n (x✝ - step) ((x✝ - step) :: x)

@[csimp]

theorem List.range'_eq_range'TR : @List.range' = @List.range'TR

theorem List.range'_eq_range'TR.go (step : optParam Nat 1) (s : Nat) (n : Nat) (m : Nat) : List.range'TR.go step n (s + step * n) (List.range' (s + step * n) m step) = List.range' s (n + m) step

iota

def List.iotaTR (n : Nat) : List Nat

Tail-recursive version of List.iota.

Equations

• List.iotaTR n = List.iotaTR.go n []

def List.iotaTR.go : Nat → List Nat → List Nat

Equations

• List.iotaTR.go 0 x = x.reverse
• List.iotaTR.go n.succ x = List.iotaTR.go n (n.succ :: x)

@[csimp]

theorem List.iota_eq_iotaTR : List.iota = List.iotaTR

enumFrom

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]

theorem List.enumFrom_eq_enumFromTR : @List.enumFrom = @List.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); List.foldr f (n + l.length, []) l = (n, List.enumFrom n l)

Other list operations

intersperse

def List.intersperseTR {α : Type u_1} (sep : α) : List α → List α

Tail recursive version of List.intersperse.

Equations

• List.intersperseTR sep x = match x with | [] => [] | [x] => [x] | x :: y :: xs => x :: sep :: y :: List.foldr (fun (a : α) (r : List α) => sep :: a :: r) [] xs

@[csimp]

theorem List.intersperse_eq_intersperseTR : @List.intersperse = @List.intersperseTR

intercalate

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

Tail recursive version of List.intercalate.

Equations

• sep.intercalateTR x = match x with | [] => [] | [x] => x | x :: xs => List.intercalateTR.go (List.toArray sep) x 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 : @List.intercalate = @List.intercalateTR

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