Bootstrapping theorems about arrays

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

@[irreducible]

theorem Array.foldlM_eq_foldlM_toList.aux {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (f : β → α → m β) (arr : Array α) (i : Nat) (j : Nat) (H : arr.size ≤ i + j) (b : β) : Array.foldlM.loop f arr arr.size ⋯ i j b = List.foldlM f b (List.drop j arr.toList)

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

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

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 β) (arr : Array α) (init : β) (i : Nat) (h : i ≤ arr.size) : List.foldlM (fun (x : β) (y : α) => f y x) init (List.take i arr.toList).reverse = Array.foldrM.fold f arr 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 : β) (arr : Array α) : Array.foldrM f init arr = List.foldlM (fun (x : β) (y : α) => f y x) init arr.toList.reverse

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Array.pop_toList {α : Type u_1} (arr : Array α) : arr.pop.toList = arr.toList.dropLast

@[simp]

theorem Array.append_eq_append {α : Type u_1} (arr : Array α) (arr' : Array α) : arr.append arr' = arr ++ arr'

@[simp]

theorem Array.toList_append {α : Type u_1} (arr : Array α) (arr' : Array α) : (arr ++ arr').toList = arr.toList ++ arr'.toList

@[simp]

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

@[simp]

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

@[reducible, inline, deprecated Array.foldlM_eq_foldlM_toList]

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

Equations

• @Array.foldlM_eq_foldlM_data = @Array.foldlM_eq_foldlM_toList

@[reducible, inline, deprecated Array.foldl_eq_foldl_toList]

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

Equations

• @Array.foldl_eq_foldl_data = @Array.foldl_eq_foldl_toList

@[reducible, inline, deprecated Array.foldrM_eq_reverse_foldlM_toList]

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 : β) (arr : Array α) : Array.foldrM f init arr = List.foldlM (fun (x : β) (y : α) => f y x) init arr.toList.reverse

Equations

• @Array.foldrM_eq_reverse_foldlM_data = @Array.foldrM_eq_reverse_foldlM_toList

@[reducible, inline, deprecated Array.foldrM_eq_foldrM_toList]

abbrev Array.foldrM_eq_foldrM_data {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (init : β) (arr : Array α) : Array.foldrM f init arr = List.foldrM f init arr.toList

Equations

• @Array.foldrM_eq_foldrM_data = @Array.foldrM_eq_foldrM_toList

@[reducible, inline, deprecated Array.foldr_eq_foldr_toList]

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

Equations

• @Array.foldr_eq_foldr_data = @Array.foldr_eq_foldr_toList

@[reducible, inline, deprecated Array.push_toList]

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

Equations

• @Array.push_data = @Array.push_toList

@[reducible, inline, deprecated Array.toListImpl_eq]

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

Equations

• @Array.toList_eq = @Array.toListImpl_eq

@[reducible, inline, deprecated Array.pop_toList]

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

Equations

• @Array.pop_data = @Array.pop_toList

@[reducible, inline, deprecated Array.toList_append]

abbrev Array.append_data {α : Type u_1} (arr : Array α) (arr' : Array α) : (arr ++ arr').toList = arr.toList ++ arr'.toList

Equations

• @Array.append_data = @Array.toList_append

@[reducible, inline, deprecated Array.appendList_toList]

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

Equations

• @Array.appendList_data = @Array.appendList_toList