Lemmas about List.*Idx functions.

Some specification lemmas for List.mapIdx, List.mapIdxM, List.foldlIdx and List.foldrIdx.

As of 2025-01-29, these are not used anywhere in Mathlib. Moreover, with List.enum and List.enumFrom being replaced by List.zipIdx in Lean's nightly-2025-01-29 release, they now use deprecated functions and theorems. Rather than updating this unused material, we are deprecating it. Anyone wanting to restore this material is welcome to do so, but will need to update uses of List.enum and List.enumFrom to use List.zipIdx instead. However, note that this material will later be implemented in the Lean standard library.

@[deprecated List.reverseRecOn (since := "2025-01-28")]

theorem List.list_reverse_induction {α : Type u} (p : List α → Prop) (base : p []) (ind : ∀ (l : List α) (e : α), p l → p (l ++ [e])) (l : List α) : p l

theorem List.mapIdx_append_one {α : Type u} {β : Type v} {f : ℕ → α → β} {l : List α} {e : α} : mapIdx f (l ++ [e]) = mapIdx f l ++ [f l.length e]

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

theorem List.map_enumFrom_eq_zipWith {α : Type u} {β : Type v} (l : List α) (n : ℕ) (f : ℕ → α → β) : map (Function.uncurry f) (enumFrom n l) = zipWith (fun (i : ℕ) => f (i + n)) (range l.length) l

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

theorem List.get_mapIdx {α : Type u} {β : Type v} (l : List α) (f : ℕ → α → β) (i : ℕ) (h : i < l.length) (h' : i < (mapIdx f l).length := ⋯) : (mapIdx f l).get ⟨i, h'⟩ = f i (l.get ⟨i, h⟩)

theorem List.mapIdx_eq_ofFn {α : Type u} {β : Type v} (l : List α) (f : ℕ → α → β) : mapIdx f l = ofFn fun (i : Fin l.length) => f (↑i) (l.get i)

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

def List.foldrIdxSpec {α : Type u} {β : Type v} (f : ℕ → α → β → β) (b : β) (as : List α) (start : ℕ) : β

Specification of foldrIdx.

Equations

• List.foldrIdxSpec f b as start = List.foldr (Function.uncurry f) b (List.enumFrom start as)

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

theorem List.foldrIdxSpec_cons {α : Type u} {β : Type v} (f : ℕ → α → β → β) (b : β) (a : α) (as : List α) (start : ℕ) : foldrIdxSpec f b (a :: as) start = f start a (foldrIdxSpec f b as (start + 1))

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

theorem List.foldrIdx_eq_foldrIdxSpec {α : Type u} {β : Type v} (f : ℕ → α → β → β) (b : β) (as : List α) (start : ℕ) : foldrIdx f b as start = foldrIdxSpec f b as start

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

theorem List.foldrIdx_eq_foldr_enum {α : Type u} {β : Type v} (f : ℕ → α → β → β) (b : β) (as : List α) : foldrIdx f b as = foldr (Function.uncurry f) b as.enum

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

theorem List.indexesValues_eq_filter_enum {α : Type u} (p : α → Prop) [DecidablePred p] (as : List α) : indexesValues (fun (b : α) => decide (p b)) as = filter ((fun (b : α) => decide (p b)) ∘ Prod.snd) as.enum

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

theorem List.findIdxs_eq_map_indexesValues {α : Type u} (p : α → Prop) [DecidablePred p] (as : List α) : findIdxs (fun (b : α) => decide (p b)) as = map Prod.fst (indexesValues (fun (b : α) => decide (p b)) as)

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

def List.foldlIdxSpec {α : Type u} {β : Type v} (f : ℕ → α → β → α) (a : α) (bs : List β) (start : ℕ) : α

Specification of foldlIdx.

Equations

• List.foldlIdxSpec f a bs start = List.foldl (fun (a : α) (p : ℕ × β) => f p.fst a p.snd) a (List.enumFrom start bs)

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

theorem List.foldlIdxSpec_cons {α : Type u} {β : Type v} (f : ℕ → α → β → α) (a : α) (b : β) (bs : List β) (start : ℕ) : foldlIdxSpec f a (b :: bs) start = foldlIdxSpec f (f start a b) bs (start + 1)

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

theorem List.foldlIdx_eq_foldlIdxSpec {α : Type u} {β : Type v} (f : ℕ → α → β → α) (a : α) (bs : List β) (start : ℕ) : foldlIdx f a bs start = foldlIdxSpec f a bs start

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

theorem List.foldlIdx_eq_foldl_enum {α : Type u} {β : Type v} (f : ℕ → α → β → α) (a : α) (bs : List β) : foldlIdx f a bs = foldl (fun (a : α) (p : ℕ × β) => f p.fst a p.snd) a bs.enum

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

theorem List.foldrIdxM_eq_foldrM_enum {α : Type u} {m : Type u → Type v} [Monad m] {β : Type u} (f : ℕ → α → β → m β) (b : β) (as : List α) [LawfulMonad m] : foldrIdxM f b as = foldrM (Function.uncurry f) b as.enum

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

theorem List.foldlIdxM_eq_foldlM_enum {α : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] {β : Type u} (f : ℕ → β → α → m β) (b : β) (as : List α) : foldlIdxM f b as = foldlM (fun (b : β) (p : ℕ × α) => f p.fst b p.snd) b as.enum

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

def List.mapIdxMAuxSpec {α : Type u} {m : Type u → Type v} [Monad m] {β : Type u} (f : ℕ → α → m β) (start : ℕ) (as : List α) : m (List β)

Specification of mapIdxMAux.

Equations

• List.mapIdxMAuxSpec f start as = List.traverse (Function.uncurry f) (List.enumFrom start as)

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

theorem List.mapIdxMAuxSpec_cons {α : Type u} {m : Type u → Type v} [Monad m] {β : Type u} (f : ℕ → α → m β) (start : ℕ) (a : α) (as : List α) : mapIdxMAuxSpec f start (a :: as) = cons <$> f start a <*> mapIdxMAuxSpec f (start + 1) as

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

theorem List.mapIdxMGo_eq_mapIdxMAuxSpec {α : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] {β : Type u} (f : ℕ → α → m β) (arr : Array β) (as : List α) : mapIdxM.go f as arr = (fun (x : List β) => arr.toList ++ x) <$> mapIdxMAuxSpec f arr.size as

@[deprecated "Deprecated without replacement." (since := "2025-01-29")]

theorem List.mapIdxM_eq_mmap_enum {α : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] {β : Type u} (f : ℕ → α → m β) (as : List α) : mapIdxM f as = List.traverse (Function.uncurry f) as.enum

theorem List.mapIdxMAux'_eq_mapIdxMGo {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type u_1} (f : ℕ → α → m PUnit.{u + 1}) (as : List α) (arr : Array PUnit.{u + 1}) : mapIdxMAux' f arr.size as = mapIdxM.go f as arr *> pure PUnit.unit

theorem List.mapIdxM'_eq_mapIdxM {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type u_1} (f : ℕ → α → m PUnit.{u + 1}) (as : List α) : mapIdxM' f as = mapIdxM f as *> pure PUnit.unit