Documentation

Init.Data.List.MapIdx

Operations using indexes #

@[inline]
def List.mapFinIdx {α : Type u_1} {β : Type u_2} (as : List α) (f : (i : Nat) → αi < as.lengthβ) :
List β

Applies a function to each element of the list along with the index at which that element is found, returning the list of results. In addition to the index, the function is also provided with a proof that the index is valid.

List.mapIdx is a variant that does not provide the function with evidence that the index is valid.

Equations
    Instances For
      @[specialize #[]]
      def List.mapFinIdx.go {α : Type u_1} {β : Type u_2} (as : List α) (f : (i : Nat) → αi < as.lengthβ) (bs : List α) (acc : Array β) :
      bs.length + acc.size = as.lengthList β

      Auxiliary for mapFinIdx: mapFinIdx.go [a₀, a₁, ...] acc = acc.toList ++ [f 0 a₀ ⋯, f 1 a₁ ⋯, ...]

      Equations
        Instances For
          @[inline]
          def List.mapIdx {α : Type u_1} {β : Type u_2} (f : Natαβ) (as : List α) :
          List β

          Applies a function to each element of the list along with the index at which that element is found, returning the list of results.

          List.mapFinIdx is a variant that additionally provides the function with a proof that the index is valid.

          Equations
            Instances For
              @[specialize #[]]
              def List.mapIdx.go {α : Type u_1} {β : Type u_2} (f : Natαβ) :
              List αArray βList β

              Auxiliary for mapIdx: mapIdx.go [a₀, a₁, ...] acc = acc.toList ++ [f acc.size a₀, f (acc.size + 1) a₁, ...]

              Equations
                Instances For
                  @[inline]
                  def List.mapFinIdxM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (as : List α) (f : (i : Nat) → αi < as.lengthm β) :
                  m (List β)

                  Applies a monadic function to each element of the list along with the index at which that element is found, returning the list of results. In addition to the index, the function is also provided with a proof that the index is valid.

                  List.mapIdxM is a variant that does not provide the function with evidence that the index is valid.

                  Equations
                    Instances For
                      @[specialize #[]]
                      def List.mapFinIdxM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (as : List α) (f : (i : Nat) → αi < as.lengthm β) (bs : List α) (acc : Array β) :
                      bs.length + acc.size = as.lengthm (List β)

                      Auxiliary for mapFinIdxM: mapFinIdxM.go [a₀, a₁, ...] acc = acc.toList ++ [f 0 a₀ ⋯, f 1 a₁ ⋯, ...]

                      Equations
                        Instances For
                          @[inline]
                          def List.mapIdxM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : Natαm β) (as : List α) :
                          m (List β)

                          Applies a monadic function to each element of the list along with the index at which that element is found, returning the list of results.

                          List.mapFinIdxM is a variant that additionally provides the function with a proof that the index is valid.

                          Equations
                            Instances For
                              @[specialize #[]]
                              def List.mapIdxM.go {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : Natαm β) :
                              List αArray βm (List β)

                              Auxiliary for mapIdxM: mapIdxM.go [a₀, a₁, ...] acc = acc.toList ++ [f acc.size a₀, f (acc.size + 1) a₁, ...]

                              Equations
                                Instances For

                                  mapFinIdx #

                                  theorem List.mapFinIdx_congr {α : Type u_1} {β : Type u_2} {xs ys : List α} (w : xs = ys) (f : (i : Nat) → αi < xs.lengthβ) :
                                  xs.mapFinIdx f = ys.mapFinIdx fun (i : Nat) (a : α) (h : i < ys.length) => f i a
                                  @[simp]
                                  theorem List.mapFinIdx_nil {α : Type u_1} {β : Type u_2} {f : (i : Nat) → αi < 0β} :
                                  @[simp]
                                  theorem List.length_mapFinIdx_go {α✝ : Type u_1} {as : List α✝} {α✝¹ : Type u_2} {f : (i : Nat) → α✝i < as.lengthα✝¹} {bs : List α✝} {acc : Array α✝¹} {h : bs.length + acc.size = as.length} :
                                  (mapFinIdx.go as f bs acc h).length = as.length
                                  @[simp]
                                  theorem List.length_mapFinIdx {α : Type u_1} {β : Type u_2} {as : List α} {f : (i : Nat) → αi < as.lengthβ} :
                                  theorem List.getElem_mapFinIdx_go {α : Type u_1} {β : Type u_2} {bs : List α} {acc : Array β} {as : List α} {f : (i : Nat) → αi < as.lengthβ} {i : Nat} {h : bs.length + acc.size = as.length} {w : i < (mapFinIdx.go as f bs acc h).length} :
                                  (mapFinIdx.go as f bs acc h)[i] = if w' : i < acc.size then acc[i] else f i bs[i - acc.size]
                                  @[simp]
                                  theorem List.getElem_mapFinIdx {α : Type u_1} {β : Type u_2} {as : List α} {f : (i : Nat) → αi < as.lengthβ} {i : Nat} {h : i < (as.mapFinIdx f).length} :
                                  (as.mapFinIdx f)[i] = f i as[i]
                                  theorem List.mapFinIdx_eq_ofFn {α : Type u_1} {β : Type u_2} {as : List α} {f : (i : Nat) → αi < as.lengthβ} :
                                  as.mapFinIdx f = ofFn fun (i : Fin as.length) => f (↑i) as[i]
                                  @[simp]
                                  theorem List.getElem?_mapFinIdx {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : Nat) → αi < l.lengthβ} {i : Nat} :
                                  (l.mapFinIdx f)[i]? = l[i]?.pbind fun (x : α) (m : l[i]? = some x) => some (f i x )
                                  @[simp]
                                  theorem List.mapFinIdx_cons {α : Type u_1} {β : Type u_2} {l : List α} {a : α} {f : (i : Nat) → αi < l.length + 1β} :
                                  (a :: l).mapFinIdx f = f 0 a :: l.mapFinIdx fun (i : Nat) (a : α) (h : i < l.length) => f (i + 1) a
                                  theorem List.mapFinIdx_append {α : Type u_1} {β : Type u_2} {xs ys : List α} {f : (i : Nat) → αi < (xs ++ ys).lengthβ} :
                                  (xs ++ ys).mapFinIdx f = (xs.mapFinIdx fun (i : Nat) (a : α) (h : i < xs.length) => f i a ) ++ ys.mapFinIdx fun (i : Nat) (a : α) (h : i < ys.length) => f (i + xs.length) a
                                  @[simp]
                                  theorem List.mapFinIdx_concat {α : Type u_1} {β : Type u_2} {l : List α} {e : α} {f : (i : Nat) → αi < (l ++ [e]).lengthβ} :
                                  (l ++ [e]).mapFinIdx f = (l.mapFinIdx fun (i : Nat) (a : α) (h : i < l.length) => f i a ) ++ [f l.length e ]
                                  theorem List.mapFinIdx_singleton {α : Type u_1} {β : Type u_2} {a : α} {f : (i : Nat) → αi < 1β} :
                                  [a].mapFinIdx f = [f 0 a ]
                                  theorem List.mapFinIdx_eq_zipIdx_map {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : Nat) → αi < l.lengthβ} :
                                  l.mapFinIdx f = map (fun (x : { x : α × Nat // x l.zipIdx }) => match x with | (x, i), m => f i x ) l.zipIdx.attach
                                  @[reducible, inline, deprecated List.mapFinIdx_eq_zipIdx_map (since := "2025-01-21")]
                                  abbrev List.mapFinIdx_eq_zipWithIndex_map {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : Nat) → αi < l.lengthβ} :
                                  l.mapFinIdx f = map (fun (x : { x : α × Nat // x l.zipIdx }) => match x with | (x, i), m => f i x ) l.zipIdx.attach
                                  Equations
                                    Instances For
                                      @[simp]
                                      theorem List.mapFinIdx_eq_nil_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : Nat) → αi < l.lengthβ} :
                                      theorem List.mapFinIdx_ne_nil_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : Nat) → αi < l.lengthβ} :
                                      theorem List.exists_of_mem_mapFinIdx {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : (i : Nat) → αi < l.lengthβ} (h : b l.mapFinIdx f) :
                                      (i : Nat), (h : i < l.length), f i l[i] h = b
                                      @[simp]
                                      theorem List.mem_mapFinIdx {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : (i : Nat) → αi < l.lengthβ} :
                                      b l.mapFinIdx f (i : Nat), (h : i < l.length), f i l[i] h = b
                                      theorem List.mapFinIdx_eq_cons_iff {α : Type u_1} {β : Type u_2} {l₂ : List β} {l : List α} {b : β} {f : (i : Nat) → αi < l.lengthβ} :
                                      l.mapFinIdx f = b :: l₂ (a : α), (l₁ : List α), (w : l = a :: l₁), f 0 a = b (l₁.mapFinIdx fun (i : Nat) (a_1 : α) (h : i < l₁.length) => f (i + 1) a_1 ) = l₂
                                      theorem List.mapFinIdx_eq_cons_iff' {α : Type u_1} {β : Type u_2} {l₂ : List β} {l : List α} {b : β} {f : (i : Nat) → αi < l.lengthβ} :
                                      l.mapFinIdx f = b :: l₂ (l.head?.pbind fun (x : α) (m : l.head? = some x) => some (f 0 x )) = some b Option.map (fun (x : { x : List α // l.tail? = some x }) => match x with | t, m => t.mapFinIdx fun (i : Nat) (a : α) (h : i < t.length) => f (i + 1) a ) l.tail?.attach = some l₂
                                      theorem List.mapFinIdx_eq_iff {α : Type u_1} {β : Type u_2} {l' : List β} {l : List α} {f : (i : Nat) → αi < l.lengthβ} :
                                      l.mapFinIdx f = l' (h : l'.length = l.length), ∀ (i : Nat) (h_1 : i < l.length), l'[i] = f i l[i] h_1
                                      @[simp]
                                      theorem List.mapFinIdx_eq_singleton_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : Nat) → αi < l.lengthβ} {b : β} :
                                      l.mapFinIdx f = [b] (a : α), (w : l = [a]), f 0 a = b
                                      theorem List.mapFinIdx_eq_append_iff {α : Type u_1} {β : Type u_2} {l₁ l₂ : List β} {l : List α} {f : (i : Nat) → αi < l.lengthβ} :
                                      l.mapFinIdx f = l₁ ++ l₂ (l₁' : List α), (l₂' : List α), (w : l = l₁' ++ l₂'), (l₁'.mapFinIdx fun (i : Nat) (a : α) (h : i < l₁'.length) => f i a ) = l₁ (l₂'.mapFinIdx fun (i : Nat) (a : α) (h : i < l₂'.length) => f (i + l₁'.length) a ) = l₂
                                      theorem List.mapFinIdx_eq_mapFinIdx_iff {α : Type u_1} {β : Type u_2} {l : List α} {f g : (i : Nat) → αi < l.lengthβ} :
                                      l.mapFinIdx f = l.mapFinIdx g ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i] h
                                      @[simp]
                                      theorem List.mapFinIdx_mapFinIdx {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {f : (i : Nat) → αi < l.lengthβ} {g : (i : Nat) → βi < (l.mapFinIdx f).lengthγ} :
                                      (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx fun (i : Nat) (a : α) (h : i < l.length) => g i (f i a h)
                                      theorem List.mapFinIdx_eq_replicate_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : Nat) → αi < l.lengthβ} {b : β} :
                                      l.mapFinIdx f = replicate l.length b ∀ (i : Nat) (h : i < l.length), f i l[i] h = b
                                      @[simp]
                                      theorem List.mapFinIdx_reverse {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : Nat) → αi < l.reverse.lengthβ} :
                                      l.reverse.mapFinIdx f = (l.mapFinIdx fun (i : Nat) (a : α) (h : i < l.length) => f (l.length - 1 - i) a ).reverse

                                      mapIdx #

                                      @[simp]
                                      theorem List.mapIdx_nil {α : Type u_1} {β : Type u_2} {f : Natαβ} :
                                      theorem List.mapIdx_go_length {β : Type u_1} {α✝ : Type u_2} {f : Natα✝β} {l : List α✝} {acc : Array β} :
                                      (mapIdx.go f l acc).length = l.length + acc.size
                                      theorem List.length_mapIdx_go {α : Type u_1} {β : Type u_2} {f : Natαβ} {l : List α} {acc : Array β} :
                                      (mapIdx.go f l acc).length = l.length + acc.size
                                      @[simp]
                                      theorem List.length_mapIdx {α : Type u_1} {α✝ : Type u_2} {f : Natαα✝} {l : List α} :
                                      theorem List.getElem?_mapIdx_go {α : Type u_1} {β : Type u_2} {f : Natαβ} {l : List α} {acc : Array β} {i : Nat} :
                                      (mapIdx.go f l acc)[i]? = if h : i < acc.size then some acc[i] else Option.map (f i) l[i - acc.size]?
                                      @[simp]
                                      theorem List.getElem?_mapIdx {α : Type u_1} {α✝ : Type u_2} {f : Natαα✝} {l : List α} {i : Nat} :
                                      (mapIdx f l)[i]? = Option.map (f i) l[i]?
                                      @[simp]
                                      theorem List.getElem_mapIdx {α : Type u_1} {β : Type u_2} {l : List α} {f : Natαβ} {i : Nat} {h : i < (mapIdx f l).length} :
                                      (mapIdx f l)[i] = f i l[i]
                                      @[simp]
                                      theorem List.mapFinIdx_eq_mapIdx {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : Nat) → αi < l.lengthβ} {g : Natαβ} (h : ∀ (i : Nat) (h : i < l.length), f i l[i] h = g i l[i]) :
                                      theorem List.mapIdx_eq_mapFinIdx {α : Type u_1} {β : Type u_2} {l : List α} {f : Natαβ} :
                                      mapIdx f l = l.mapFinIdx fun (i : Nat) (a : α) (x : i < l.length) => f i a
                                      theorem List.mapIdx_eq_zipIdx_map {α : Type u_1} {β : Type u_2} {l : List α} {f : Natαβ} :
                                      mapIdx f l = map (fun (x : α × Nat) => match x with | (a, i) => f i a) l.zipIdx
                                      @[reducible, inline, deprecated List.mapIdx_eq_zipIdx_map (since := "2025-01-21")]
                                      abbrev List.mapIdx_eq_enum_map {α : Type u_1} {β : Type u_2} {l : List α} {f : Natαβ} :
                                      mapIdx f l = map (fun (x : α × Nat) => match x with | (a, i) => f i a) l.zipIdx
                                      Equations
                                        Instances For
                                          @[simp]
                                          theorem List.mapIdx_cons {α : Type u_1} {α✝ : Type u_2} {f : Natαα✝} {l : List α} {a : α} :
                                          mapIdx f (a :: l) = f 0 a :: mapIdx (fun (i : Nat) => f (i + 1)) l
                                          theorem List.mapIdx_append {α : Type u_1} {α✝ : Type u_2} {f : Natαα✝} {xs ys : List α} :
                                          mapIdx f (xs ++ ys) = mapIdx f xs ++ mapIdx (fun (i : Nat) => f (i + xs.length)) ys
                                          @[simp]
                                          theorem List.mapIdx_concat {α : Type u_1} {α✝ : Type u_2} {f : Natαα✝} {l : List α} {e : α} :
                                          mapIdx f (l ++ [e]) = mapIdx f l ++ [f l.length e]
                                          theorem List.mapIdx_singleton {α : Type u_1} {α✝ : Type u_2} {f : Natαα✝} {a : α} :
                                          mapIdx f [a] = [f 0 a]
                                          @[simp]
                                          theorem List.mapIdx_eq_nil_iff {α : Type u_1} {α✝ : Type u_2} {f : Natαα✝} {l : List α} :
                                          mapIdx f l = [] l = []
                                          theorem List.mapIdx_ne_nil_iff {α : Type u_1} {α✝ : Type u_2} {f : Natαα✝} {l : List α} :
                                          theorem List.exists_of_mem_mapIdx {β : Type u_1} {α : Type u_2} {f : Natαβ} {b : β} {l : List α} (h : b mapIdx f l) :
                                          (i : Nat), (h : i < l.length), f i l[i] = b
                                          @[simp]
                                          theorem List.mem_mapIdx {β : Type u_1} {α : Type u_2} {f : Natαβ} {b : β} {l : List α} :
                                          b mapIdx f l (i : Nat), (h : i < l.length), f i l[i] = b
                                          theorem List.mapIdx_eq_cons_iff {α : Type u_1} {β : Type u_2} {f : Natαβ} {l₂ : List β} {l : List α} {b : β} :
                                          mapIdx f l = b :: l₂ (a : α), (l₁ : List α), l = a :: l₁ f 0 a = b mapIdx (fun (i : Nat) => f (i + 1)) l₁ = l₂
                                          theorem List.mapIdx_eq_cons_iff' {α : Type u_1} {β : Type u_2} {f : Natαβ} {l₂ : List β} {l : List α} {b : β} :
                                          mapIdx f l = b :: l₂ Option.map (f 0) l.head? = some b Option.map (mapIdx fun (i : Nat) => f (i + 1)) l.tail? = some l₂
                                          @[simp]
                                          theorem List.mapIdx_eq_singleton_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : Natαβ} {b : β} :
                                          mapIdx f l = [b] (a : α), l = [a] f 0 a = b
                                          theorem List.mapIdx_eq_iff {α : Type u_1} {α✝ : Type u_2} {f : Natαα✝} {l' : List α✝} {l : List α} :
                                          mapIdx f l = l' ∀ (i : Nat), l'[i]? = Option.map (f i) l[i]?
                                          theorem List.mapIdx_eq_append_iff {α : Type u_1} {α✝ : Type u_2} {f : Natαα✝} {l₁ l₂ : List α✝} {l : List α} :
                                          mapIdx f l = l₁ ++ l₂ (l₁' : List α), (l₂' : List α), l = l₁' ++ l₂' mapIdx f l₁' = l₁ mapIdx (fun (i : Nat) => f (i + l₁'.length)) l₂' = l₂
                                          theorem List.mapIdx_eq_mapIdx_iff {α : Type u_1} {α✝ : Type u_2} {f g : Natαα✝} {l : List α} :
                                          mapIdx f l = mapIdx g l ∀ (i : Nat) (h : i < l.length), f i l[i] = g i l[i]
                                          @[simp]
                                          theorem List.mapIdx_set {α : Type u_1} {α✝ : Type u_2} {f : Natαα✝} {l : List α} {i : Nat} {a : α} :
                                          mapIdx f (l.set i a) = (mapIdx f l).set i (f i a)
                                          @[simp]
                                          theorem List.head_mapIdx {α : Type u_1} {β : Type u_2} {l : List α} {f : Natαβ} {w : mapIdx f l []} :
                                          (mapIdx f l).head w = f 0 (l.head )
                                          @[simp]
                                          theorem List.head?_mapIdx {α : Type u_1} {β : Type u_2} {l : List α} {f : Natαβ} :
                                          (mapIdx f l).head? = Option.map (f 0) l.head?
                                          @[simp]
                                          theorem List.getLast_mapIdx {α : Type u_1} {β : Type u_2} {l : List α} {f : Natαβ} {h : mapIdx f l []} :
                                          (mapIdx f l).getLast h = f (l.length - 1) (l.getLast )
                                          @[simp]
                                          theorem List.getLast?_mapIdx {α : Type u_1} {β : Type u_2} {l : List α} {f : Natαβ} :
                                          @[simp]
                                          theorem List.mapIdx_mapIdx {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {f : Natαβ} {g : Natβγ} :
                                          mapIdx g (mapIdx f l) = mapIdx (fun (i : Nat) => g i f i) l
                                          theorem List.mapIdx_eq_replicate_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : Natαβ} {b : β} :
                                          mapIdx f l = replicate l.length b ∀ (i : Nat) (h : i < l.length), f i l[i] = b
                                          @[simp]
                                          theorem List.mapIdx_reverse {α : Type u_1} {β : Type u_2} {l : List α} {f : Natαβ} :
                                          mapIdx f l.reverse = (mapIdx (fun (i : Nat) => f (l.length - 1 - i)) l).reverse