Operations using indexes

mapIdx

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

@[simp]

theorem List.mapIdx_nil {α : Type u_1} {β : Type u_2} {f : Nat → α → β} : List.mapIdx f [] = []

theorem List.mapIdx_go_append {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {l₁ : List α} {l₂ : List α} {arr : Array β} : List.mapIdx.go f (l₁ ++ l₂) arr = List.mapIdx.go f l₂ (List.mapIdx.go f l₁ arr).toArray

theorem List.mapIdx_go_length {β : Type u_1} : ∀ {α : Type u_2} {f : Nat → α → β} {l : List α} {arr : Array β}, (List.mapIdx.go f l arr).length = l.length + arr.size

@[simp]

theorem List.mapIdx_concat {α : Type u_1} : ∀ {α_1 : Type u_2} {f : Nat → α → α_1} {l : List α} {e : α}, List.mapIdx f (l ++ [e]) = List.mapIdx f l ++ [f l.length e]

@[simp]

theorem List.mapIdx_singleton {α : Type u_1} : ∀ {α_1 : Type u_2} {f : Nat → α → α_1} {a : α}, List.mapIdx f [a] = [f 0 a]

theorem List.length_mapIdx_go {α : Type u_1} {β : Type u_2} {f : Nat → α → β} {l : List α} {arr : Array β} : (List.mapIdx.go f l arr).length = l.length + arr.size

@[simp]

theorem List.length_mapIdx {α : Type u_1} : ∀ {α_1 : Type u_2} {f : Nat → α → α_1} {l : List α}, (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} : (List.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} : ∀ {α_1 : Type u_2} {f : Nat → α → α_1} {l : List α} {i : Nat}, (List.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 < (List.mapIdx f l).length} : (List.mapIdx f l)[i] = f i l[i]

theorem List.mapIdx_eq_enum_map {α : Type u_1} : ∀ {α_1 : Type u_2} {f : Nat → α → α_1} {l : List α}, List.mapIdx f l = List.map (Function.uncurry f) l.enum

@[simp]

theorem List.mapIdx_cons {α : Type u_1} : ∀ {α_1 : Type u_2} {f : Nat → α → α_1} {l : List α} {a : α}, List.mapIdx f (a :: l) = f 0 a :: List.mapIdx (fun (i : Nat) => f (i + 1)) l

theorem List.mapIdx_append {α : Type u_1} : ∀ {α_1 : Type u_2} {f : Nat → α → α_1} {K L : List α}, List.mapIdx f (K ++ L) = List.mapIdx f K ++ List.mapIdx (fun (i : Nat) => f (i + K.length)) L

@[simp]

theorem List.mapIdx_eq_nil_iff {α : Type u_1} : ∀ {α_1 : Type u_2} {f : Nat → α → α_1} {l : List α}, List.mapIdx f l = [] ↔ l = []

theorem List.mapIdx_ne_nil_iff {α : Type u_1} : ∀ {α_1 : Type u_2} {f : Nat → α → α_1} {l : List α}, List.mapIdx f l ≠ [] ↔ l ≠ []

theorem List.exists_of_mem_mapIdx {β : Type u_1} {α : Type u_2} {f : Nat → α → β} {b : β} {l : List α} (h : b ∈ List.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 ∈ List.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 : β} : List.mapIdx f l = b :: l₂ ↔ ∃ (a : α), ∃ (l₁ : List α), l = a :: l₁ ∧ f 0 a = b ∧ List.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 : β} : List.mapIdx f l = b :: l₂ ↔ Option.map (f 0) l.head? = some b ∧ Option.map (List.mapIdx fun (i : Nat) => f (i + 1)) l.tail? = some l₂

theorem List.mapIdx_eq_iff {α : Type u_1} : ∀ {α_1 : Type u_2} {f : Nat → α → α_1} {l' : List α_1} {l : List α}, List.mapIdx f l = l' ↔ ∀ (i : Nat), l'[i]? = Option.map (f i) l[i]?

theorem List.mapIdx_eq_mapIdx_iff {α : Type u_1} : ∀ {α_1 : Type u_2} {f g : Nat → α → α_1} {l : List α}, List.mapIdx f l = List.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} : ∀ {α_1 : Type u_2} {f : Nat → α → α_1} {l : List α} {i : Nat} {a : α}, List.mapIdx f (l.set i a) = (List.mapIdx f l).set i (f i a)

@[simp]

theorem List.head_mapIdx {α : Type u_1} {β : Type u_2} {l : List α} {f : Nat → α → β} {w : List.mapIdx f l ≠ []} : (List.mapIdx f l).head w = f 0 (l.head ⋯)

@[simp]

theorem List.head?_mapIdx {α : Type u_1} {β : Type u_2} {l : List α} {f : Nat → α → β} : (List.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 : List.mapIdx f l ≠ []} : (List.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 → α → β} : (List.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 → β → γ} : List.mapIdx g (List.mapIdx f l) = List.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 : β} : List.mapIdx f l = List.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 → α → β} : List.mapIdx f l.reverse = (List.mapIdx (fun (i : Nat) => f (l.length - 1 - i)) l).reverse