Lemmas about List.*Idx functions.

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

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

@[deprecated List.mapIdx_go_append]

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

Alias of List.mapIdx_go_append.

@[deprecated List.mapIdx_go_length]

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

Alias of List.mapIdx_go_length.

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

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

@[deprecated List.mapIdx_eq_nil_iff]

theorem List.mapIdx_eq_nil {α : Type u_1} {α✝ : Type u_2} {f : ℕ → α → α✝} {l : List α} : List.mapIdx f l = [] ↔ l = []

Alias of List.mapIdx_eq_nil_iff.

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

@[deprecated List.get_mapIdx]

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

Alias of List.get_mapIdx.

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

@[deprecated]

def List.oldMapIdxCore {α : Type u} {β : Type v} (f : ℕ → α → β) : ℕ → List α → List β

Lean3 map_with_index helper function

Equations

• List.oldMapIdxCore f x [] = []
• List.oldMapIdxCore f x (a :: as) = f x a :: List.oldMapIdxCore f (x + 1) as

@[deprecated]

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

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

Equations

• List.oldMapIdx f as = List.oldMapIdxCore f 0 as

@[deprecated]

theorem List.oldMapIdxCore_eq {α : Type u} {β : Type v} (l : List α) (f : ℕ → α → β) (n : ℕ) : List.oldMapIdxCore f n l = List.oldMapIdx (fun (i : ℕ) (a : α) => f (i + n) a) l

@[deprecated]

theorem List.oldMapIdxCore_append {α : Type u} {β : Type v} (f : ℕ → α → β) (n : ℕ) (l₁ l₂ : List α) : List.oldMapIdxCore f n (l₁ ++ l₂) = List.oldMapIdxCore f n l₁ ++ List.oldMapIdxCore f (n + l₁.length) l₂

@[deprecated]

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

@[deprecated]

theorem List.new_def_eq_old_def {α : Type u} {β : Type v} (f : ℕ → α → β) (l : List α) : List.mapIdx f l = List.oldMapIdx f l

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)

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

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

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

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

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

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.1 a p.2) a (List.enumFrom start bs)

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

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

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

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

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

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)

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

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

theorem List.mapIdxM_eq_mmap_enum {α : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] {β : Type u} (f : ℕ → α → m β) (as : List α) : as.mapIdxM f = 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} ) : List.mapIdxMAux' f arr.size as = List.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 α) : List.mapIdxM' f as = as.mapIdxM f *> pure PUnit.unit