Documentation

Mathlib.Data.List.Defs

Definitions on lists #

This file contains various definitions on lists. It does not contain proofs about these definitions, those are contained in other files in Data.List

Equations
    def List.getI {α : Type u_1} [Inhabited α] (l : List α) (n : ) :
    α

    "Inhabited" get function: returns default instead of none in the case that the index is out of bounds.

    Equations
      Instances For
        def List.headI {α : Type u_1} [Inhabited α] :
        List αα

        The head of a list, or the default element of the type is the list is nil.

        Equations
          Instances For
            @[simp]
            theorem List.headI_nil {α : Type u_1} [Inhabited α] :
            @[simp]
            theorem List.headI_cons {α : Type u_1} [Inhabited α] {h : α} {t : List α} :
            (h :: t).headI = h
            def List.getLastI {α : Type u_1} [Inhabited α] :
            List αα

            The last element of a list, with the default if list empty

            Equations
              Instances For
                def List.takeI {α : Type u_1} [Inhabited α] (n : ) (l : List α) :
                List α

                "Inhabited" take function: Take n elements from a list l. If l has less than n elements, append n - length l elements default.

                Equations
                  Instances For
                    def List.findM {α : Type u} {m : Type u → Type v} [Alternative m] (tac : αm PUnit) :
                    List αm α

                    findM tac l returns the first element of l on which tac succeeds, and fails otherwise.

                    Equations
                      Instances For
                        def List.findM?' {m : Type u → Type v} [Monad m] {α : Type u} (p : αm (ULift Bool)) :
                        List αm (Option α)

                        findM? p l returns the first element a of l for which p a returns true. findM? short-circuits, so p is not necessarily run on every a in l. This is a monadic version of List.find.

                        Equations
                          Instances For
                            def List.orM {m : TypeType v} [Monad m] :
                            List (m Bool)m Bool

                            orM xs runs the actions in xs, returning true if any of them returns true. orM short-circuits, so if an action returns true, later actions are not run.

                            Equations
                              Instances For
                                def List.andM {m : TypeType v} [Monad m] :
                                List (m Bool)m Bool

                                andM xs runs the actions in xs, returning true if all of them return true. andM short-circuits, so if an action returns false, later actions are not run.

                                Equations
                                  Instances For
                                    def List.foldlIdxM {m : Type v → Type w} [Monad m] {α : Type u_7} {β : Type v} (f : βαm β) (b : β) (as : List α) :
                                    m β

                                    Monadic variant of foldlIdx.

                                    Equations
                                      Instances For
                                        def List.foldrIdxM {m : Type v → Type w} [Monad m] {α : Type u_7} {β : Type v} (f : αβm β) (b : β) (as : List α) :
                                        m β

                                        Monadic variant of foldrIdx.

                                        Equations
                                          Instances For
                                            def List.mapIdxMAux' {m : Type v → Type w} [Monad m] {α : Type u_7} (f : αm PUnit) :
                                            List αm PUnit

                                            Auxiliary definition for mapIdxM'.

                                            Equations
                                              Instances For
                                                def List.mapIdxM' {m : Type v → Type w} [Monad m] {α : Type u_7} (f : αm PUnit) (as : List α) :

                                                A variant of mapIdxM specialised to applicative actions which return Unit.

                                                Equations
                                                  Instances For
                                                    def List.Forall {α : Type u_1} (p : αProp) :
                                                    List αProp

                                                    l.Forall p is equivalent to ∀ a ∈ l, p a, but unfolds directly to a conjunction, i.e. List.Forall p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2.

                                                    Equations
                                                      Instances For
                                                        def List.permutationsAux2 {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) :
                                                        List α(List αβ)List α × List β

                                                        An auxiliary function for defining permutations. permutationsAux2 t ts r ys f is equal to (ys ++ ts, (insert_left ys t ts).map f ++ r), where insert_left ys t ts (not explicitly defined) is the list of lists of the form insert_nth n t (ys ++ ts) for 0 ≤ n < length ys.

                                                        permutations_aux2 10 [4, 5, 6] [] [1, 2, 3] id =
                                                          ([1, 2, 3, 4, 5, 6],
                                                           [[10, 1, 2, 3, 4, 5, 6],
                                                            [1, 10, 2, 3, 4, 5, 6],
                                                            [1, 2, 10, 3, 4, 5, 6]]) 
                                                        
                                                        Equations
                                                          Instances For
                                                            @[irreducible]
                                                            def List.permutationsAux.rec {α : Type u_1} {C : List αList αSort v} (H0 : (is : List α) → C [] is) (H1 : (t : α) → (ts is : List α) → C ts (t :: is)C is []C (t :: ts) is) (l₁ l₂ : List α) :
                                                            C l₁ l₂

                                                            A recursor for pairs of lists. To have C l₁ l₂ for all l₁, l₂, it suffices to have it for l₂ = [] and to be able to pour the elements of l₁ into l₂.

                                                            Equations
                                                              Instances For
                                                                def List.permutationsAux {α : Type u_1} :
                                                                List αList αList (List α)

                                                                An auxiliary function for defining permutations. permutationsAux ts is is the set of all permutations of is ++ ts that do not fix ts.

                                                                Equations
                                                                  Instances For
                                                                    def List.permutations {α : Type u_1} (l : List α) :
                                                                    List (List α)

                                                                    List of all permutations of l.

                                                                    permutations [1, 2, 3] = [[1, 2, 3], [2, 1, 3], [3, 2, 1], [2, 3, 1], [3, 1, 2], [1, 3, 2]]

                                                                    Equations
                                                                      Instances For
                                                                        def List.permutations'Aux {α : Type u_1} (t : α) :
                                                                        List αList (List α)

                                                                        permutations'Aux t ts inserts t into every position in ts, including the last. This function is intended for use in specifications, so it is simpler than permutationsAux2, which plays roughly the same role in permutations.

                                                                        Note that (permutationsAux2 t [] [] ts id).2 is similar to this function, but skips the last position:

                                                                        permutations'Aux 10 [1, 2, 3] =
                                                                          [[10, 1, 2, 3], [1, 10, 2, 3], [1, 2, 10, 3], [1, 2, 3, 10]]
                                                                        (permutationsAux2 10 [] [] [1, 2, 3] id).2 =
                                                                          [[10, 1, 2, 3], [1, 10, 2, 3], [1, 2, 10, 3]] 
                                                                        
                                                                        Equations
                                                                          Instances For
                                                                            def List.permutations' {α : Type u_1} :
                                                                            List αList (List α)

                                                                            List of all permutations of l. This version of permutations is less efficient but has simpler definitional equations. The permutations are in a different order, but are equal up to permutation, as shown by List.permutations_perm_permutations'.

                                                                             permutations [1, 2, 3] =
                                                                               [[1, 2, 3], [2, 1, 3], [2, 3, 1],
                                                                                [1, 3, 2], [3, 1, 2], [3, 2, 1]] 
                                                                            
                                                                            Equations
                                                                              Instances For
                                                                                def List.extractp {α : Type u_1} (p : αProp) [DecidablePred p] :
                                                                                List αOption α × List α

                                                                                extractp p l returns a pair of an element a of l satisfying the predicate p, and l, with a removed. If there is no such element a it returns (none, l).

                                                                                Equations
                                                                                  Instances For
                                                                                    instance List.instSProd {α : Type u_1} {β : Type u_2} :
                                                                                    SProd (List α) (List β) (List (α × β))

                                                                                    Notation for calculating the product of a List

                                                                                    Equations
                                                                                      instance List.decidableChain {α : Type u_1} {R : ααProp} [DecidableRel R] (a : α) (l : List α) :
                                                                                      Equations
                                                                                        instance List.decidableChain' {α : Type u_1} {R : ααProp} [DecidableRel R] (l : List α) :
                                                                                        Equations
                                                                                          def List.dedup {α : Type u_1} [DecidableEq α] :
                                                                                          List αList α

                                                                                          dedup l removes duplicates from l (taking only the last occurrence). Defined as pwFilter (≠).

                                                                                          dedup [1, 0, 2, 2, 1] = [0, 2, 1]

                                                                                          Equations
                                                                                            Instances For
                                                                                              def List.destutter' {α : Type u_1} (R : ααProp) [DecidableRel R] :
                                                                                              αList αList α

                                                                                              Greedily create a sublist of a :: l such that, for every two adjacent elements a, b, R a b holds. Mostly used with ≠; for example, destutter' (≠) 1 [2, 2, 1, 1] = [1, 2, 1], destutter' (≠) 1, [2, 3, 3] = [1, 2, 3], destutter' (<) 1 [2, 5, 2, 3, 4, 9] = [1, 2, 5, 9].

                                                                                              Equations
                                                                                                Instances For
                                                                                                  def List.destutter {α : Type u_1} (R : ααProp) [DecidableRel R] :
                                                                                                  List αList α

                                                                                                  Greedily create a sublist of l such that, for every two adjacent elements a, b ∈ l, R a b holds. Mostly used with ≠; for example, destutter (≠) [1, 2, 2, 1, 1] = [1, 2, 1], destutter (≠) [1, 2, 3, 3] = [1, 2, 3], destutter (<) [1, 2, 5, 2, 3, 4, 9] = [1, 2, 5, 9].

                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      def List.chooseX {α : Type u_1} (p : αProp) [DecidablePred p] (l : List α) :
                                                                                                      ( (a : α), a l p a) → { a : α // a l p a }

                                                                                                      Given a decidable predicate p and a proof of existence of a ∈ l such that p a, choose the first element with this property. This version returns both a and proofs of a ∈ l and p a.

                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          def List.choose {α : Type u_1} (p : αProp) [DecidablePred p] (l : List α) (hp : (a : α), a l p a) :
                                                                                                          α

                                                                                                          Given a decidable predicate p and a proof of existence of a ∈ l such that p a, choose the first element with this property. This version returns a : α, and properties are given by choose_mem and choose_property.

                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              def List.mapDiagM' {m : TypeType u_7} [Monad m] {α : Type u_8} (f : ααm Unit) :
                                                                                                              List αm Unit

                                                                                                              mapDiagM' f l calls f on all elements in the upper triangular part of l × l. That is, for each e ∈ l, it will run f e e and then f e e' for each e' that appears after e in l.

                                                                                                              Example: suppose l = [1, 2, 3]. mapDiagM' f l will evaluate, in this order, f 1 1, f 1 2, f 1 3, f 2 2, f 2 3, f 3 3.

                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  def List.map₂Left' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αOption βγ) :
                                                                                                                  List αList βList γ × List β

                                                                                                                  Left-biased version of List.map₂. map₂Left' f as bs applies f to each pair of elements aᵢ ∈ as and bᵢ ∈ bs. If bs is shorter than as, f is applied to none for the remaining aᵢ. Returns the results of the f applications and the remaining bs.

                                                                                                                  map₂Left' prod.mk [1, 2] ['a'] = ([(1, some 'a'), (2, none)], [])
                                                                                                                  
                                                                                                                  map₂Left' prod.mk [1] ['a', 'b'] = ([(1, some 'a')], ['b'])
                                                                                                                  
                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      def List.map₂Right' {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option αβγ) (as : List α) (bs : List β) :
                                                                                                                      List γ × List α

                                                                                                                      Right-biased version of List.map₂. map₂Right' f as bs applies f to each pair of elements aᵢ ∈ as and bᵢ ∈ bs. If as is shorter than bs, f is applied to none for the remaining bᵢ. Returns the results of the f applications and the remaining as.

                                                                                                                      map₂Right' prod.mk [1] ['a', 'b'] = ([(some 1, 'a'), (none, 'b')], [])
                                                                                                                      
                                                                                                                      map₂Right' prod.mk [1, 2] ['a'] = ([(some 1, 'a')], [2])
                                                                                                                      
                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          def List.map₂Left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αOption βγ) :
                                                                                                                          List αList βList γ

                                                                                                                          Left-biased version of List.map₂. map₂Left f as bs applies f to each pair aᵢ ∈ as and bᵢ ∈ bs. If bs is shorter than as, f is applied to none for the remaining aᵢ.

                                                                                                                          map₂Left Prod.mk [1, 2] ['a'] = [(1, some 'a'), (2, none)]
                                                                                                                          
                                                                                                                          map₂Left Prod.mk [1] ['a', 'b'] = [(1, some 'a')]
                                                                                                                          
                                                                                                                          map₂Left f as bs = (map₂Left' f as bs).fst
                                                                                                                          
                                                                                                                          Equations
                                                                                                                            Instances For
                                                                                                                              def List.map₂Right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option αβγ) (as : List α) (bs : List β) :
                                                                                                                              List γ

                                                                                                                              Right-biased version of List.map₂. map₂Right f as bs applies f to each pair aᵢ ∈ as and bᵢ ∈ bs. If as is shorter than bs, f is applied to none for the remaining bᵢ.

                                                                                                                              map₂Right Prod.mk [1, 2] ['a'] = [(some 1, 'a')]
                                                                                                                              
                                                                                                                              map₂Right Prod.mk [1] ['a', 'b'] = [(some 1, 'a'), (none, 'b')]
                                                                                                                              
                                                                                                                              map₂Right f as bs = (map₂Right' f as bs).fst
                                                                                                                              
                                                                                                                              Equations
                                                                                                                                Instances For
                                                                                                                                  def List.mapAsyncChunked {α : Type u_7} {β : Type u_8} (f : αβ) (xs : List α) (chunk_size : := 1024) :
                                                                                                                                  List β

                                                                                                                                  Asynchronous version of List.map.

                                                                                                                                  Equations
                                                                                                                                    Instances For

                                                                                                                                      We add some n-ary versions of List.zipWith for functions with more than two arguments. These can also be written in terms of List.zip or List.zipWith. For example, zipWith3 f xs ys zs could also be written as zipWith id (zipWith f xs ys) zs or as (zip xs <| zip ys zs).map <| fun ⟨x, y, z⟩ ↦ f x y z.

                                                                                                                                      def List.zipWith3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : αβγδ) :
                                                                                                                                      List αList βList γList δ

                                                                                                                                      Ternary version of List.zipWith.

                                                                                                                                      Equations
                                                                                                                                        Instances For
                                                                                                                                          def List.zipWith4 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} (f : αβγδε) :
                                                                                                                                          List αList βList γList δList ε

                                                                                                                                          Quaternary version of list.zipWith.

                                                                                                                                          Equations
                                                                                                                                            Instances For
                                                                                                                                              def List.zipWith5 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (f : αβγδεζ) :
                                                                                                                                              List αList βList γList δList εList ζ

                                                                                                                                              Quinary version of list.zipWith.

                                                                                                                                              Equations
                                                                                                                                                Instances For
                                                                                                                                                  def List.replaceIf {α : Type u_1} :
                                                                                                                                                  List αList BoolList αList α

                                                                                                                                                  Given a starting list old, a list of booleans and a replacement list new, read the items in old in succession and either replace them with the next element of new or not, according as to whether the corresponding boolean is true or false.

                                                                                                                                                  Equations
                                                                                                                                                    Instances For
                                                                                                                                                      def List.iterate {α : Type u_1} (f : αα) (a : α) (n : ) :
                                                                                                                                                      List α

                                                                                                                                                      iterate f a n is [a, f a, ..., f^[n - 1] a].

                                                                                                                                                      Equations
                                                                                                                                                        Instances For
                                                                                                                                                          @[inline]
                                                                                                                                                          def List.iterateTR {α : Type u_1} (f : αα) (a : α) (n : ) :
                                                                                                                                                          List α

                                                                                                                                                          Tail-recursive version of List.iterate.

                                                                                                                                                          Equations
                                                                                                                                                            Instances For
                                                                                                                                                              @[specialize #[]]
                                                                                                                                                              def List.iterateTR.loop {α : Type u_1} (f : αα) (a : α) (n : ) (l : List α) :
                                                                                                                                                              List α

                                                                                                                                                              iterateTR.loop f a n l := iterate f a n ++ reverse l.

                                                                                                                                                              Equations
                                                                                                                                                                Instances For
                                                                                                                                                                  theorem List.iterateTR_loop_eq {α : Type u_1} (f : αα) (a : α) (n : ) (l : List α) :
                                                                                                                                                                  def List.mapAccumr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αγγ × β) :
                                                                                                                                                                  List αγγ × List β

                                                                                                                                                                  Runs a function over a list returning the intermediate results and a final result.

                                                                                                                                                                  Equations
                                                                                                                                                                    Instances For
                                                                                                                                                                      @[simp]
                                                                                                                                                                      theorem List.length_mapAccumr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αγγ × β) (x : List α) (s : γ) :

                                                                                                                                                                      Length of the list obtained by mapAccumr.

                                                                                                                                                                      def List.mapAccumr₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : αβγγ × δ) :
                                                                                                                                                                      List αList βγγ × List δ

                                                                                                                                                                      Runs a function over two lists returning the intermediate results and a final result.

                                                                                                                                                                      Equations
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[simp]
                                                                                                                                                                          theorem List.length_mapAccumr₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : αβγγ × δ) (x : List α) (y : List β) (c : γ) :

                                                                                                                                                                          Length of a list obtained using mapAccumr₂.