## Operations using indexes #

source
@[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 #[] ⋯

Instances For

source
@[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 ⋯)) ⋯

Instances For

source
@[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 #[]

Instances For

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

Instances For

source
@[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 #[] ⋯

Instances For

source
@[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) ⋯

Instances For

source
@[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 #[]

Instances For

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

Instances For

### mapFinIdx #

source
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 ⋯
source
@[simp]
theorem List.mapFinIdx_nil {α : Type u_1} {β : Type u_2} {f : (i : Nat) → α → i < 0 → β} :
[].mapFinIdx f = []
source
@[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
source
@[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
source
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] ⋯
source
@[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] ⋯
source
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] ⋯
source
@[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 ⋯)
source
@[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 ⋯
source
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 ⋯
source
@[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 ⋯]
source
theorem List.mapFinIdx_singleton {α : Type u_1} {β : Type u_2} {a : α} {f : (i : Nat) → α → i < 1 → β} :
[a].mapFinIdx f = [f 0 a mapFinIdx_singleton._proof_1]
source
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
source
@[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 = []
source
theorem List.mapFinIdx_ne_nil_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : Nat) → α → i < l.length → β} :
l.mapFinIdx f ≠ [] ↔ l ≠ []
source
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
source
@[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
source
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₂
source
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₂
source
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
source
@[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
source
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₂
source
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
source
@[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) ⋯
source
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
source
@[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 #

source
@[simp]
theorem List.mapIdx_nil {α : Type u_1} {β : Type u_2} {f : Nat → α → β} :
mapIdx f [] = []
source
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
source
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
source
@[simp]
theorem List.length_mapIdx {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {l : List α} :
(mapIdx f l).length = l.length
source
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]?
source
@[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]?
source
@[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]
source
@[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
source
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
source
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
source
@[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
source
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
source
@[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]
source
theorem List.mapIdx_singleton {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {a : α} :
mapIdx f [a] = [f 0 a]
source
@[simp]
theorem List.mapIdx_eq_nil_iff {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {l : List α} :
mapIdx f l = [] ↔ l = []
source
theorem List.mapIdx_ne_nil_iff {α : Type u_1} {α✝ : Type u_2} {f : Nat → α → α✝} {l : List α} :
mapIdx f l ≠ [] ↔ l ≠ []
source
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
source
@[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
source
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₂
source
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₂
source
@[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
source
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]?
source
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₂
source
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]
source
@[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)
source
@[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 ⋯)
source
@[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?
source
@[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 ⋯)
source
@[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?
source
@[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
source
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
source
@[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