Lemmas about List.*Idx functions. #
Some specification lemmas for List.mapIdx
, List.mapIdxM
, List.foldlIdx
and List.foldrIdx
.
@[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]
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
Instances For
@[deprecated]
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
Instances For
@[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)
Instances For
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)
Instances For
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)
Instances For
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