Bootstrapping theorems about arrays

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

@[deprecated "Use indexing notation `as[i]` instead" (since := "2025-02-17")]

def Array.get {α : Type u} (a : Array α) (i : Nat) (h : i < a.size) : α

Use the indexing notation a[i] instead.

Access an element from an array without needing a runtime bounds checks, using a Nat index and a proof that it is in bounds.

This function does not use get_elem_tactic to automatically find the proof that the index is in bounds. This is because the tactic itself needs to look up values in arrays.

Equations

• a.get i h = a.toList.get ⟨i, h⟩

@[deprecated "Use indexing notation `as[i]!` instead" (since := "2025-02-17")]

def Array.get! {α : Type u} [Inhabited α] (a : Array α) (i : Nat) : α

Use the indexing notation a[i]! instead.

Access an element from an array, or panic if the index is out of bounds.

Equations

• a.get! i = a.getD i default

@[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)

@[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

@[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

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

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

@[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

@[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

@[simp]

theorem Array.push_toList {α : Type u_1} (xs : Array α) (a : α) : (xs.push a).toList = xs.toList ++ [a]

@[simp]

theorem Array.toListAppend_eq {α : Type u_1} (xs : Array α) (l : List α) : xs.toListAppend l = xs.toList ++ l

@[simp]

theorem Array.toListImpl_eq {α : Type u_1} (xs : Array α) : xs.toListImpl = xs.toList

@[simp]

theorem Array.toList_pop {α : Type u_1} (xs : Array α) : xs.pop.toList = xs.toList.dropLast

@[reducible, inline, deprecated Array.toList_pop (since := "2025-02-17")]

abbrev Array.pop_toList {α : Type u_1} (xs : Array α) : xs.pop.toList = xs.toList.dropLast

Equations

• @Array.pop_toList = @Array.toList_pop

@[simp]

theorem Array.append_eq_append {α : Type u_1} (xs ys : Array α) : xs.append ys = xs ++ ys

@[simp]

theorem Array.toList_append {α : Type u_1} (xs ys : Array α) : (xs ++ ys).toList = xs.toList ++ ys.toList

@[simp]

theorem Array.toList_empty {α : Type u_1} : #[].toList = []

@[simp]

theorem Array.append_empty {α : Type u_1} (xs : Array α) : xs ++ #[] = xs

@[reducible, inline, deprecated Array.append_empty (since := "2025-01-13")]

abbrev Array.append_nil {α : Type u_1} (xs : Array α) : xs ++ #[] = xs

Equations

• @Array.append_nil = @Array.append_empty

@[simp]

theorem Array.empty_append {α : Type u_1} (xs : Array α) : #[] ++ xs = xs

@[reducible, inline, deprecated Array.empty_append (since := "2025-01-13")]

abbrev Array.nil_append {α : Type u_1} (xs : Array α) : #[] ++ xs = xs

Equations

• @Array.nil_append = @Array.empty_append

@[simp]

theorem Array.append_assoc {α : Type u_1} (xs ys zs : Array α) : xs ++ ys ++ zs = xs ++ (ys ++ zs)

@[simp]

theorem Array.appendList_eq_append {α : Type u_1} (xs : Array α) (l : List α) : xs.appendList l = xs ++ l

@[simp]

theorem Array.toList_appendList {α : Type u_1} (xs : Array α) (l : List α) : (xs ++ l).toList = xs.toList ++ l

@[reducible, inline, deprecated Array.toList_appendList (since := "2024-12-11")]

abbrev Array.appendList_toList {α : Type u_1} (xs : Array α) (l : List α) : (xs ++ l).toList = xs.toList ++ l

Equations

• @Array.appendList_toList = @Array.toList_appendList

@[deprecated "Use the reverse direction of `foldrM_toList`." (since := "2024-11-13")]

theorem Array.foldrM_eq_foldrM_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.foldrM f init xs.toList

@[deprecated "Use the reverse direction of `foldlM_toList`." (since := "2024-11-13")]

theorem Array.foldlM_eq_foldlM_toList {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (f : β → α → m β) (init : β) (xs : Array α) : foldlM f init xs = List.foldlM f init xs.toList

@[deprecated "Use the reverse direction of `foldr_toList`." (since := "2024-11-13")]

theorem Array.foldr_eq_foldr_toList {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (xs : Array α) : foldr f init xs = List.foldr f init xs.toList

@[deprecated "Use the reverse direction of `foldl_toList`." (since := "2024-11-13")]

theorem Array.foldl_eq_foldl_toList {β : Type u_1} {α : Type u_2} (f : β → α → β) (init : β) (xs : Array α) : foldl f init xs = List.foldl f init xs.toList

@[reducible, inline, deprecated Array.foldlM_toList (since := "2024-09-09")]

abbrev Array.foldlM_eq_foldlM_data {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

Equations

• @Array.foldlM_eq_foldlM_data = @Array.foldlM_toList

@[reducible, inline, deprecated Array.foldl_toList (since := "2024-09-09")]

abbrev Array.foldl_eq_foldl_data {β : Type u_1} {α : Type u_2} (f : β → α → β) (init : β) (xs : Array α) : List.foldl f init xs.toList = foldl f init xs

Equations

• @Array.foldl_eq_foldl_data = @Array.foldl_toList

@[reducible, inline, deprecated Array.foldrM_eq_reverse_foldlM_toList (since := "2024-09-09")]

abbrev Array.foldrM_eq_reverse_foldlM_data {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

Equations

• @Array.foldrM_eq_reverse_foldlM_data = @Array.foldrM_eq_reverse_foldlM_toList

@[reducible, inline, deprecated Array.foldrM_toList (since := "2024-09-09")]

abbrev Array.foldrM_eq_foldrM_data {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

Equations

• @Array.foldrM_eq_foldrM_data = @Array.foldrM_toList

@[reducible, inline, deprecated Array.foldr_toList (since := "2024-09-09")]

abbrev Array.foldr_eq_foldr_data {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (xs : Array α) : List.foldr f init xs.toList = foldr f init xs

Equations

• @Array.foldr_eq_foldr_data = @Array.foldr_toList

@[reducible, inline, deprecated Array.push_toList (since := "2024-09-09")]

abbrev Array.push_data {α : Type u_1} (xs : Array α) (a : α) : (xs.push a).toList = xs.toList ++ [a]

Equations

• @Array.push_data = @Array.push_toList

@[reducible, inline, deprecated Array.toListImpl_eq (since := "2024-09-09")]

abbrev Array.toList_eq {α : Type u_1} (xs : Array α) : xs.toListImpl = xs.toList

Equations

• @Array.toList_eq = @Array.toListImpl_eq

@[reducible, inline, deprecated Array.pop_toList (since := "2024-09-09")]

abbrev Array.pop_data {α : Type u_1} (xs : Array α) : xs.pop.toList = xs.toList.dropLast

Equations

• @Array.pop_data = @Array.toList_pop

@[reducible, inline, deprecated Array.toList_append (since := "2024-09-09")]

abbrev Array.append_data {α : Type u_1} (xs ys : Array α) : (xs ++ ys).toList = xs.toList ++ ys.toList

Equations

• @Array.append_data = @Array.toList_append

@[reducible, inline, deprecated Array.toList_appendList (since := "2024-09-09")]

abbrev Array.appendList_data {α : Type u_1} (xs : Array α) (l : List α) : (xs ++ l).toList = xs.toList ++ l

Equations

• @Array.appendList_data = @Array.toList_appendList