Documentation

Init.Data.Array.Bootstrap

Bootstrapping theorems about arrays #

This file contains some theorems about Array and List needed for Init.Data.List.Impl.

source
@[irreducible]
theorem Array.foldlM_toList.aux {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] {f : β → α → m β} {xs : Array α} {i j : Nat} (H : xs.size ≤ i + j) {b : β} :
foldlM.loop f xs xs.size ⋯ i j b = List.foldlM f b (List.drop j xs.toList)
source
@[simp]
theorem Array.foldlM_toList {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] {f : β → α → m β} {init : β} {xs : Array α} :
List.foldlM f init xs.toList = foldlM f init xs
source
@[simp]
theorem Array.foldl_toList {β : Type u_1} {α : Type u_2} (f : β → α → β) {init : β} {xs : Array α} :
List.foldl f init xs.toList = foldl f init xs
source
theorem Array.foldrM_eq_reverse_foldlM_toList.aux {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {f : α → β → m β} {xs : Array α} {init : β} {i : Nat} (h : i ≤ xs.size) :
List.foldlM (fun (x : β) (y : α) => f y x) init (List.take i xs.toList).reverse = foldrM.fold f xs 0 i h init
source
theorem Array.foldrM_eq_reverse_foldlM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {f : α → β → m β} {init : β} {xs : Array α} :
foldrM f init xs = List.foldlM (fun (x : β) (y : α) => f y x) init xs.toList.reverse
source
@[simp]
theorem Array.foldrM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {f : α → β → m β} {init : β} {xs : Array α} :
List.foldrM f init xs.toList = foldrM f init xs
source
@[simp]
theorem Array.foldr_toList {α : Type u_1} {β : Type u_2} (f : α → β → β) {init : β} {xs : Array α} :
List.foldr f init xs.toList = foldr f init xs
source
@[simp]
theorem Array.toList_push {α : Type u_1} {xs : Array α} {x : α} :
(xs.push x).toList = xs.toList ++ [x]
source
@[reducible, inline, deprecated Array.toList_push (since := "2025-05-26")]
abbrev Array.push_toList {α : Type u_1} {xs : Array α} {x : α} :
(xs.push x).toList = xs.toList ++ [x]
Equations
Instances For
    source
    @[simp]
    theorem Array.toListAppend_eq {α : Type u_1} {xs : Array α} {l : List α} :
    xs.toListAppend l = xs.toList ++ l
    source
    @[simp]
    theorem Array.toListImpl_eq {α : Type u_1} {xs : Array α} :
    xs.toListImpl = xs.toList
    source
    @[simp]
    theorem Array.toList_pop {α : Type u_1} {xs : Array α} :
    xs.pop.toList = xs.toList.dropLast
    source
    @[simp]
    theorem Array.append_eq_append {α : Type u_1} {xs ys : Array α} :
    xs.append ys = xs ++ ys
    source
    @[simp]
    theorem Array.toList_append {α : Type u_1} {xs ys : Array α} :
    (xs ++ ys).toList = xs.toList ++ ys.toList
    source
    @[simp]
    theorem Array.toList_empty {α : Type u_1} :
    #[].toList = []
    source
    @[simp]
    theorem Array.append_empty {α : Type u_1} {xs : Array α} :
    xs ++ #[] = xs
    source
    @[simp]
    theorem Array.empty_append {α : Type u_1} {xs : Array α} :
    #[] ++ xs = xs
    source
    @[simp]
    theorem Array.append_assoc {α : Type u_1} {xs ys zs : Array α} :
    xs ++ ys ++ zs = xs ++ (ys ++ zs)
    source
    @[simp]
    theorem Array.appendList_eq_append {α : Type u_1} {xs : Array α} {l : List α} :
    xs.appendList l = xs ++ l
    source
    @[simp]
    theorem Array.toList_appendList {α : Type u_1} {xs : Array α} {l : List α} :
    (xs ++ l).toList = xs.toList ++ l