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

• as.mapFinIdx f = List.mapFinIdx.go as f as #[] ⋯

@[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.length → List β

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

Equations

• List.mapFinIdx.go as f [] x x_1 = x.toList
• List.mapFinIdx.go as f (a :: as_1) x x_1 = List.mapFinIdx.go as f as_1 (x.push (f x.size a ⋯)) ⋯

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

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

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

• List.mapIdx.go f [] x✝ = x✝.toList
• List.mapIdx.go f (a :: as) x✝ = List.mapIdx.go f as (x✝.push (f x✝.size a))

@[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.length → m β) : 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

• as.mapFinIdxM f = List.mapFinIdxM.go as f as #[] ⋯

@[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.length → m β) (bs : List α) (acc : Array β) : bs.length + acc.size = as.length → m (List β)

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

Equations

• List.mapFinIdxM.go as f [] x x_1 = pure x.toList
• List.mapFinIdxM.go as f (a :: as_1) x x_1 = do let __do_lift ← f x.size a ⋯ List.mapFinIdxM.go as f as_1 (x.push __do_lift) ⋯

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

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

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

• List.mapIdxM.go f [] x✝ = pure x✝.toList
• List.mapIdxM.go f (a :: as) x✝ = do let __do_lift ← f x✝.size a List.mapIdxM.go f as (x✝.push __do_lift)

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 → β} : [].mapFinIdx f = []

@[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 → β} : (as.mapFinIdx f).length = 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 : x ∈ l[i]?) => 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

• @List.mapFinIdx_eq_zipWithIndex_map = @List.mapFinIdx_eq_zipIdx_map

@[simp]

theorem List.mapFinIdx_eq_nil_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : Nat) → α → i < l.length → β} : l.mapFinIdx f = [] ↔ l = []

theorem List.mapFinIdx_ne_nil_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : Nat) → α → i < l.length → β} : l.mapFinIdx f ≠ [] ↔ l ≠ []

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 : x ∈ l.head?) => some (f 0 x ⋯)) = some b ∧ Option.map (fun (x : { x : List α // x ∈ l.tail? }) => 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 → α → β} : mapIdx f [] = []

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 α} : (mapIdx f l).length = l.length

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]) : l.mapFinIdx f = mapIdx g l

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

• @List.mapIdx_eq_enum_map = @List.mapIdx_eq_zipIdx_map

@[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 α} : mapIdx f l ≠ [] ↔ l ≠ []

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 → α → β} : (mapIdx f l).getLast? = Option.map (f (l.length - 1)) l.getLast?

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