Bootstrapping theorems about arrays

This file contains some theorems about Array and List needed for Std.List.Basic.

@[simp]

theorem Array.mkEmpty_eq (α : Type u_1) (n : Nat) : Array.mkEmpty n = #[]

@[simp]

theorem Array.size_toArray {α : Type u_1} (as : List α) : (List.toArray as).size = as.length

@[simp]

theorem Array.size_mk {α : Type u_1} (as : List α) : { data := as }.size = as.length

theorem Array.getElem_eq_data_get {α : Type u_1} {i : Nat} (a : Array α) (h : i < a.size) : a[i] = a.data.get ⟨i, h⟩

theorem Array.foldlM_eq_foldlM_data.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.data)

theorem 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 0 = List.foldlM f init arr.data

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

theorem Array.foldrM_eq_reverse_foldlM_data.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.data).reverse = Array.foldrM.fold f arr 0 i h init

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

theorem 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 arr.size = List.foldrM f init arr.data

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

@[simp]

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

theorem Array.foldrM_push {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) : Array.foldrM f init (arr.push a) (arr.push a).size = do let init ← f a init Array.foldrM f init arr arr.size

@[simp]

theorem Array.foldrM_push' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) : Array.foldrM f init (arr.push a) (arr.size + 1) = do let init ← f a init Array.foldrM f init arr arr.size

theorem Array.foldr_push {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (arr : Array α) (a : α) : Array.foldr f init (arr.push a) (arr.push a).size = Array.foldr f (f a init) arr arr.size

@[simp]

theorem Array.foldr_push' {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (arr : Array α) (a : α) : Array.foldr f init (arr.push a) (arr.size + 1) = Array.foldr f (f a init) arr arr.size

@[simp]

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

@[simp]

theorem Array.toList_eq {α : Type u_1} (arr : Array α) : arr.toList = arr.data

@[inline]

def Array.toListRev {α : Type u_1} (arr : Array α) : List α

A more efficient version of arr.toList.reverse.

Equations

• arr.toListRev = Array.foldl (fun (l : List α) (t : α) => t :: l) [] arr 0

@[simp]

theorem Array.toListRev_eq {α : Type u_1} (arr : Array α) : arr.toListRev = arr.data.reverse

theorem Array.get_push_lt {α : Type u_1} (a : Array α) (x : α) (i : Nat) (h : i < a.size) : let_fun this := ⋯; (a.push x)[i] = a[i]

@[simp]

theorem Array.get_push_eq {α : Type u_1} (a : Array α) (x : α) : (a.push x)[a.size] = x

theorem Array.get_push {α : Type u_1} (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) : (a.push x)[i] = if h : i < a.size then a[i] else x

theorem Array.mapM_eq_foldlM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) : Array.mapM f arr = Array.foldlM (fun (bs : Array β) (a : α) => bs.push <$> f a) #[] arr 0

theorem Array.mapM_eq_foldlM.aux {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) (i : Nat) (r : Array β) : Array.mapM.map f arr i r = List.foldlM (fun (bs : Array β) (a : α) => bs.push <$> f a) r (List.drop i arr.data)

@[simp]

theorem Array.map_data {α : Type u_1} {β : Type u_2} (f : α → β) (arr : Array α) : (Array.map f arr).data = List.map f arr.data

@[simp]

theorem Array.size_map {α : Type u_1} {β : Type u_2} (f : α → β) (arr : Array α) : (Array.map f arr).size = arr.size

@[simp]

theorem Array.pop_data {α : Type u_1} (arr : Array α) : arr.pop.data = arr.data.dropLast

@[simp]

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

@[simp]

theorem Array.append_data {α : Type u_1} (arr : Array α) (arr' : Array α) : (arr ++ arr').data = arr.data ++ arr'.data

@[simp]

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

@[simp]

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

@[simp]

theorem Array.appendList_nil {α : Type u_1} (arr : Array α) : arr ++ [] = arr

@[simp]

theorem Array.appendList_cons {α : Type u_1} (arr : Array α) (a : α) (l : List α) : arr ++ a :: l = arr.push a ++ l

theorem Array.foldl_data_eq_bind {α : Type u_1} {β : Type u_2} (l : List α) (acc : Array β) (F : Array β → α → Array β) (G : α → List β) (H : ∀ (acc : Array β) (a : α), (F acc a).data = acc.data ++ G a) : (List.foldl F acc l).data = acc.data ++ l.bind G

theorem Array.foldl_data_eq_map {α : Type u_1} {β : Type u_2} (l : List α) (acc : Array β) (G : α → β) : (List.foldl (fun (acc : Array β) (a : α) => acc.push (G a)) acc l).data = acc.data ++ List.map G l

theorem Array.size_uset {α : Type u_1} (a : Array α) (v : α) (i : USize) (h : i.toNat < a.size) : (a.uset i v h).size = a.size

theorem Array.anyM_eq_anyM_loop {m : Type → Type u_1} {α : Type u_2} [Monad m] (p : α → m Bool) (as : Array α) (start : Nat) (stop : Nat) : Array.anyM p as start stop = Array.anyM.loop p as (min stop as.size) ⋯ start

theorem Array.anyM_stop_le_start {m : Type → Type u_1} {α : Type u_2} [Monad m] (p : α → m Bool) (as : Array α) (start : Nat) (stop : Nat) (h : min stop as.size ≤ start) : Array.anyM p as start stop = pure false

theorem Array.mem_def {α : Type u_1} (a : α) (as : Array α) : a ∈ as ↔ a ∈ as.data

get

@[simp]

theorem Array.get_eq_getElem {α : Type u_1} (a : Array α) (i : Fin a.size) : a.get i = a[↑i]

theorem Array.getElem?_lt {α : Type u_1} (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some a[i]

theorem Array.getElem?_ge {α : Type u_1} (a : Array α) {i : Nat} (h : i ≥ a.size) : a[i]? = none

@[simp]

theorem Array.get?_eq_getElem? {α : Type u_1} (a : Array α) (i : Nat) : a.get? i = a[i]?

theorem Array.getElem?_len_le {α : Type u_1} (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = none

theorem Array.getD_get? {α : Type u_1} (a : Array α) (i : Nat) (d : α) : a[i]?.getD d = if p : i < a.size then a[i] else d

@[simp]

theorem Array.getD_eq_get? {α : Type u_1} (a : Array α) (n : Nat) (d : α) : a.getD n d = a[n]?.getD d

theorem Array.get!_eq_getD {α : Type u_1} {n : Nat} [Inhabited α] (a : Array α) : a.get! n = a.getD n default

@[simp]

theorem Array.get!_eq_getElem? {α : Type u_1} [Inhabited α] (a : Array α) (i : Nat) : a.get! i = (a.get? i).getD default

set

@[simp]

theorem Array.getElem_set_eq {α : Type u_1} (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (eq : ↑i = j) (p : j < (a.set i v).size) : (a.set i v)[j] = v

@[simp]

theorem Array.getElem_set_ne {α : Type u_1} (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size) (h : ↑i ≠ j) : (a.set i v)[j] = a[j]

theorem Array.getElem_set {α : Type u_1} (a : Array α) (i : Fin a.size) (v : α) (j : Nat) (h : j < (a.set i v).size) : (a.set i v)[j] = if ↑i = j then v else a[j]

@[simp]

theorem Array.getElem?_set_eq {α : Type u_1} (a : Array α) (i : Fin a.size) (v : α) : (a.set i v)[↑i]? = some v

@[simp]

theorem Array.getElem?_set_ne {α : Type u_1} (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (ne : ↑i ≠ j) : (a.set i v)[j]? = a[j]?

setD

@[simp]

theorem Array.set!_is_setD : @Array.set! = @Array.setD

@[simp]

theorem Array.size_setD {α : Type u_1} (a : Array α) (index : Nat) (val : α) : (a.setD index val).size = a.size

@[simp]

theorem Array.getElem_setD_eq {α : Type u_1} (a : Array α) {i : Nat} (v : α) (h : i < (a.setD i v).size) : (a.setD i v)[i] = v

@[simp]

theorem Array.getElem?_setD_eq {α : Type u_1} (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a.setD i v)[i]? = some v

@[simp]

theorem Array.getD_get?_setD {α : Type u_1} (a : Array α) (i : Nat) (v : α) (d : α) : (a.setD i v)[i]?.getD d = if i < a.size then v else d

Simplifies a normal form from get!

ofFn

@[simp]

theorem Array.size_ofFn_go {α : Type u_1} {n : Nat} (f : Fin n → α) (i : Nat) (acc : Array α) : (Array.ofFn.go f i acc).size = acc.size + (n - i)

@[simp]

theorem Array.size_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) : (Array.ofFn f).size = n

theorem Array.getElem_ofFn_go {n : Nat} {α : Type u_1} (f : Fin n → α) (i : Nat) {acc : Array α} {k : Nat} (hki : k < n) (hin : i ≤ n) (hi : i = acc.size) (hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩) : (Array.ofFn.go f i acc)[k] = f ⟨k, hki⟩

@[simp]

theorem Array.getElem_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) (i : Nat) (h : i < (Array.ofFn f).size) : (Array.ofFn f)[i] = f ⟨i, ⋯⟩