Documentation

Mathlib.Data.List.Indexes

Lemmas about List.*Idx functions. #

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

@[simp]
theorem List.mapIdx_nil {α : Type u_1} {β : Type u_2} (f : αβ) :
List.mapIdx f [] = []
theorem List.list_reverse_induction {α : Type u} (p : List αProp) (base : p []) (ind : ∀ (l : List α) (e : α), p lp (l ++ [e])) (l : List α) :
p l
theorem List.mapIdxGo_append {α : Type u} {β : Type v} (f : αβ) (l₁ : List α) (l₂ : List α) (arr : Array β) :
List.mapIdx.go f (l₁ ++ l₂) arr = List.mapIdx.go f l₂ (List.mapIdx.go f l₁ arr).toArray
theorem List.mapIdxGo_length {α : Type u} {β : Type v} (f : αβ) (l : List α) (arr : Array β) :
(List.mapIdx.go f l arr).length = l.length + arr.size
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
theorem List.length_mapIdx_go {α : Type u} {β : Type v} (f : αβ) (l : List α) (arr : Array β) :
(List.mapIdx.go f l arr).length = l.length + arr.size
@[simp]
theorem List.length_mapIdx {α : Type u} {β : Type v} (l : List α) (f : αβ) :
(List.mapIdx f l).length = l.length
theorem List.getElem?_mapIdx_go {α : Type u} {β : Type v} (f : αβ) (l : List α) (arr : Array β) (i : ) :
(List.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} {β : Type v} (l : List α) (f : αβ) (i : ) :
(List.mapIdx f l)[i]? = Option.map (f i) l[i]?
theorem List.mapIdx_eq_enum_map {α : Type u} {β : Type v} (l : List α) (f : αβ) :
@[simp]
theorem List.mapIdx_cons {α : Type u} {β : Type v} (l : List α) (f : αβ) (a : α) :
List.mapIdx f (a :: l) = f 0 a :: List.mapIdx (fun (i : ) => f (i + 1)) l
theorem List.mapIdx_append {α : Type u} {β : Type v} (K : List α) (L : List α) (f : αβ) :
List.mapIdx f (K ++ L) = List.mapIdx f K ++ List.mapIdx (fun (i : ) (a : α) => f (i + K.length) a) L
@[simp]
theorem List.mapIdx_eq_nil {α : Type u} {β : Type v} {f : αβ} {l : List α} :
List.mapIdx f l = [] l = []
theorem List.get_mapIdx {α : Type u} {β : Type v} (l : List α) (f : αβ) (i : ) (h : i < l.length) (h' : optParam (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' : optParam (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
Instances For
    @[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
    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₁ : List α) (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 α) :
      def List.foldrIdxSpec {α : Type u} {β : Type v} (f : αββ) (b : β) (as : List α) (start : ) :
      β

      Specification of foldrIdx.

      Equations
      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 α) :
        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
        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] :
          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
          Instances For
            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) = Seq.seq (List.cons <$> f start a) fun (x : Unit) => 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} ) :
            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 = SeqRight.seqRight (as.mapIdxM f) fun (x : Unit) => pure PUnit.unit