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 "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)
Instances For
@[deprecated "Deprecated without replacement." (since := "2025-01-29")]
theorem
List.indexesValues_eq_filter_enum
{α : Type u}
(p : α → Prop)
[DecidablePred p]
(as : List α)
:
@[deprecated "Deprecated without replacement." (since := "2025-01-29")]
theorem
List.findIdxs_eq_map_indexesValues
{α : Type u}
(p : α → Prop)
[DecidablePred p]
(as : List α)
:
@[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)
Instances For
@[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]
:
@[deprecated "Deprecated without replacement." (since := "2025-01-29")]
@[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)
Instances For
@[deprecated "Deprecated without replacement." (since := "2025-01-29")]
@[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 α)
:
@[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 α)
:
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})
:
theorem
List.mapIdxM'_eq_mapIdxM
{m : Type u → Type v}
[Monad m]
[LawfulMonad m]
{α : Type u_1}
(f : ℕ → α → m PUnit.{u + 1})
(as : List α)
: