Operations using indexes

@[inline]

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

Given a list as = [a₀, a₁, ...] and a function f : (i : Nat) → α → (h : i < as.length) → β, returns the list [f 0 a₀ ⋯, f 1 a₁ ⋯, ...].

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 β

Given a function f : Nat → α → β and as : List α, as = [a₀, a₁, ...], returns the list [f 0 a₀, f 1 a₁, ...].

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 β)

Given a list as = [a₀, a₁, ...] and a monadic function f : (i : Nat) → α → (h : i < as.length) → m β, returns the list [f 0 a₀ ⋯, f 1 a₁ ⋯, ...].

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 β)

Given a monadic function f : Nat → α → m β and as : List α, as = [a₀, a₁, ...], returns the list [f 0 a₀, f 1 a₁, ...].

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} {K L : List α} {f : (i : Nat) → α → i < (K ++ L).length → β} : (K ++ L).mapFinIdx f = (K.mapFinIdx fun (i : Nat) (a : α) (h : i < K.length) => f i a ⋯) ++ L.mapFinIdx fun (i : Nat) (a : α) (h : i < L.length) => f (i + K.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 α✝} {arr : Array β} : (mapIdx.go f l arr).length = l.length + arr.size

theorem List.length_mapIdx_go {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {l : List α} {arr : Array β} : (mapIdx.go f l arr).length = l.length + arr.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 α} {arr : Array β} {i : Nat} : (mapIdx.go f l arr)[i]? = if h : i < arr.size then some arr[i] else Option.map (f i) l[i - arr.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 → α → α✝} {K L : List α} : mapIdx f (K ++ L) = mapIdx f K ++ mapIdx (fun (i : Nat) => f (i + K.length)) L

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