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.

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

set #

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

Tail recursive version of List.set.

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
      theorem List.set_eq_setTR.go (α : Type u_1) (l : List α) (a : α) (acc : Array α) (xs : List α) (n : Nat) :
      l = acc.data ++ xsList.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
      Instances For
        @[specialize #[]]
        def List.mapTR.loop {α : Type u_1} {β : Type u_2} (f : αβ) :
        List αList βList β
        Equations
        Instances For
          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

          filter #

          @[inline]
          def List.filterTR {α : Type u_1} (p : αBool) (as : List α) :
          List α

          Tail-recursive version of List.filter.

          Equations
          Instances For
            @[specialize #[]]
            def List.filterTR.loop {α : Type u_1} (p : αBool) :
            List αList αList α
            Equations
            Instances For
              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

              filterMap #

              @[inline]
              def List.filterMapTR {α : Type u_1} {β : Type u_2} (f : αOption β) (l : List α) :
              List β

              Tail recursive version of filterMap.

              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 β) :
                  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
                  Instances For

                    bind #

                    @[inline]
                    def List.bindTR {α : Type u_1} {β : Type u_2} (as : List α) (f : αList β) :
                    List β

                    Tail recursive version of List.bind.

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

                          replicate #

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

                          Tail-recursive version of List.replicate.

                          Equations
                          Instances For
                            def List.replicateTR.loop {α : Type u} (a : α) :
                            NatList αList α
                            Equations
                            Instances For
                              theorem List.replicateTR_loop_eq :
                              ∀ {α : Type u_1} {a : α} {acc : List α} (n : Nat), List.replicateTR.loop a n acc = List.replicate n a ++ acc

                              Sublists #

                              take #

                              @[inline]
                              def List.takeTR {α : Type u_1} (n : Nat) (l : List α) :
                              List α

                              Tail recursive version of List.take.

                              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 α

                                  Tail recursive version of List.takeWhile.

                                  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 α

                                      Tail recursive version of dropLast.

                                      Equations
                                      Instances For

                                        Manipulating elements #

                                        replace #

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

                                        Tail recursive version of List.replace.

                                        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

                                            erase #

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

                                            Tail recursive version of List.erase.

                                            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

                                                eraseIdx #

                                                @[inline]
                                                def List.eraseIdxTR {α : Type u_1} (l : List α) (n : Nat) :
                                                List α

                                                Tail recursive version of List.eraseIdx.

                                                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 γ

                                                    Tail recursive version of List.zipWith.

                                                    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 γ) :
                                                        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
                                                        Instances For

                                                          Ranges and enumeration #

                                                          iota #

                                                          def List.iotaTR (n : Nat) :

                                                          Tail-recursive version of List.iota.

                                                          Equations
                                                          Instances For
                                                            Equations
                                                            Instances For

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

                                                                  intercalate #

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

                                                                  Tail recursive version of List.intercalate.

                                                                  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 α)) :
                                                                      List.intercalateTR.go (List.toArray sep) x xs acc = acc.data ++ (List.intersperse sep (x :: xs)).join