Documentation

Init.Data.List.Impl

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
    Instances For
      def List.setTR.go {α : Type u_1} (l : List α) (a : α) :
      List αNatArray α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
        Instances For
          @[csimp]
          theorem List.set_eq_setTR.go (α : Type u_1) (l : List α) (a : α) (acc : Array α) (xs : List α) (i : Nat) :
          l = acc.toList ++ xssetTR.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
            Instances For
              @[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
                Instances For
                  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
                    Instances For

                      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:

                      Equations
                        Instances For
                          @[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
                            Instances For
                              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
                                Instances For

                                  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
                                    Instances For
                                      @[specialize #[]]
                                      def List.takeTR.go {α : Type u_1} (l : List α) :
                                      List αNatArray α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
                                        Instances For

                                          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:

                                          Equations
                                            Instances For
                                              @[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
                                                Instances For

                                                  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:

                                                  Equations
                                                    Instances For

                                                      Finding elements #

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

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

                                                      Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem List.find?_singleton {α : Type u_1} {p : αBool} {a : α} :
                                                          @[simp]
                                                          theorem List.find?_append {α : Type u_1} {p : αBool} {xs ys : List α} :
                                                          find? p (xs ++ ys) = (find? p xs).or (find? p ys)
                                                          @[simp]
                                                          theorem List.findRev?_eq_find?_reverse {α : Type u_1} {l : List α} {p : αBool} :
                                                          def List.findSomeRev?TR {α : Type u_1} {β : Type u_2} (f : αOption β) (l : List α) :

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

                                                          Equations
                                                            Instances For
                                                              @[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)
                                                              @[simp]
                                                              theorem List.findSomeRev?_eq_findSome?_reverse {α : Type u_1} {β : Type u_2} {l : List α} {f : αOption β} :

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

                                                                      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
                                                                        Instances For
                                                                          def List.modifyTR.go {α : Type u_1} (f : αα) :
                                                                          List αNatArray αList α

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

                                                                          Equations
                                                                            Instances For
                                                                              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

                                                                              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
                                                                                Instances For
                                                                                  def List.insertIdxTR.go {α : Type u_1} (a : α) :
                                                                                  NatList αArray αList α

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

                                                                                  Equations
                                                                                    Instances For
                                                                                      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

                                                                                      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
                                                                                        Instances For
                                                                                          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
                                                                                            Instances For
                                                                                              @[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
                                                                                                Instances For
                                                                                                  @[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
                                                                                                    Instances For
                                                                                                      theorem List.eraseP_eq_erasePTR.go (α : Type u_1) (p : αBool) (l : List α) (acc : Array α) (xs : List α) :
                                                                                                      l = acc.toList ++ xserasePTR.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:

                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          def List.eraseIdxTR.go {α : Type u_1} (l : List α) :
                                                                                                          List αNatArray α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
                                                                                                            Instances For

                                                                                                              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
                                                                                                                Instances For
                                                                                                                  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
                                                                                                                    Instances For
                                                                                                                      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
                                                                                                                        Instances For
                                                                                                                          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
                                                                                                                            Instances For
                                                                                                                              @[csimp, deprecated List.zipIdx_eq_zipIdxTR (since := "2025-01-21")]
                                                                                                                              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:

                                                                                                                              Equations
                                                                                                                                Instances For
                                                                                                                                  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
                                                                                                                                    Instances For
                                                                                                                                      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