Operations using indexes

mapIdx

@[inline]

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

Given a list as = [a₀, a₁, ...] function f : Fin 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 : Fin 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))

mapFinIdx

@[simp]

theorem List.mapFinIdx_nil {α : Type u_1} {β : Type u_2} {f : Fin 0 → α → β} : [].mapFinIdx f = []

@[simp]

theorem List.length_mapFinIdx_go {α✝ : Type u_1} {as : List α✝} {α✝¹ : Type u_2} {f : Fin 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 : Fin 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 : Fin 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 : Fin 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 : Fin 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 : Fin 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 : Fin (l.length + 1) → α → β} : (a :: l).mapFinIdx f = f 0 a :: l.mapFinIdx fun (i : Fin l.length) => f i.succ

theorem List.mapFinIdx_append {α : Type u_1} {β : Type u_2} {K L : List α} {f : Fin (K ++ L).length → α → β} : (K ++ L).mapFinIdx f = (K.mapFinIdx fun (i : Fin K.length) => f (Fin.castLE ⋯ i)) ++ L.mapFinIdx fun (i : Fin L.length) => f (Fin.cast ⋯ (Fin.natAdd K.length i))

@[simp]

theorem List.mapFinIdx_concat {α : Type u_1} {β : Type u_2} {l : List α} {e : α} {f : Fin (l ++ [e]).length → α → β} : (l ++ [e]).mapFinIdx f = (l.mapFinIdx fun (i : Fin l.length) => f (Fin.castLE ⋯ i)) ++ [f ⟨l.length, ⋯⟩ e]

theorem List.mapFinIdx_singleton {α : Type u_1} {β : Type u_2} {a : α} {f : Fin 1 → α → β} : [a].mapFinIdx f = [f ⟨0, ⋯⟩ a]

theorem List.mapFinIdx_eq_enum_map {α : Type u_1} {β : Type u_2} {l : List α} {f : Fin l.length → α → β} : l.mapFinIdx f = map (fun (x : { x : Nat × α // x ∈ l.enum }) => match x with | ⟨(i, x), m⟩ => f ⟨i, ⋯⟩ x) l.enum.attach

@[simp]

theorem List.mapFinIdx_eq_nil_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : Fin l.length → α → β} : l.mapFinIdx f = [] ↔ l = []

theorem List.mapFinIdx_ne_nil_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : Fin l.length → α → β} : l.mapFinIdx f ≠ [] ↔ l ≠ []

theorem List.exists_of_mem_mapFinIdx {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : Fin l.length → α → β} (h : b ∈ l.mapFinIdx f) : ∃ (i : Fin l.length), f i l[i] = b

@[simp]

theorem List.mem_mapFinIdx {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : Fin l.length → α → β} : b ∈ l.mapFinIdx f ↔ ∃ (i : Fin l.length), f i l[i] = b

theorem List.mapFinIdx_eq_cons_iff {α : Type u_1} {β : Type u_2} {l₂ : List β} {l : List α} {b : β} {f : Fin l.length → α → β} : l.mapFinIdx f = b :: l₂ ↔ ∃ (a : α), ∃ (l₁ : List α), ∃ (h : l = a :: l₁), f ⟨0, ⋯⟩ a = b ∧ (l₁.mapFinIdx fun (i : Fin l₁.length) => f (Fin.cast ⋯ i.succ)) = l₂

theorem List.mapFinIdx_eq_cons_iff' {α : Type u_1} {β : Type u_2} {l₂ : List β} {l : List α} {b : β} {f : Fin 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 : Fin t.length) => f (Fin.cast ⋯ i.succ)) l.tail?.attach = some l₂

theorem List.mapFinIdx_eq_iff {α : Type u_1} {β : Type u_2} {l' : List β} {l : List α} {f : Fin l.length → α → β} : l.mapFinIdx f = l' ↔ ∃ (h : l'.length = l.length), ∀ (i : Nat) (h_1 : i < l.length), l'[i] = f ⟨i, h_1⟩ l[i]

theorem List.mapFinIdx_eq_mapFinIdx_iff {α : Type u_1} {β : Type u_2} {l : List α} {f g : Fin l.length → α → β} : l.mapFinIdx f = l.mapFinIdx g ↔ ∀ (i : Fin l.length), f i l[i] = g i l[i]

@[simp]

theorem List.mapFinIdx_mapFinIdx {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {f : Fin l.length → α → β} {g : Fin (l.mapFinIdx f).length → β → γ} : (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx fun (i : Fin l.length) => g (Fin.cast ⋯ i) ∘ f i

theorem List.mapFinIdx_eq_replicate_iff {α : Type u_1} {β : Type u_2} {l : List α} {f : Fin l.length → α → β} {b : β} : l.mapFinIdx f = replicate l.length b ↔ ∀ (i : Fin l.length), f i l[i] = b

@[simp]

theorem List.mapFinIdx_reverse {α : Type u_1} {β : Type u_2} {l : List α} {f : Fin l.reverse.length → α → β} : l.reverse.mapFinIdx f = (l.mapFinIdx fun (i : Fin l.length) => f ⟨l.length - 1 - ↑i, ⋯⟩).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 : Fin l.length → α → β} {g : Nat → α → β} (h : ∀ (i : Fin l.length), f i l[i] = 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 : Fin l.length) => f ↑i

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

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

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_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