Batteries.Data.Array.Lemmas

source

theorem Array.forIn_eq_forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :

forIn as b f = forIn as.toList b f

source

@[deprecated Array.forIn_eq_forIn_toList]

theorem Array.forIn_eq_forIn_data {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :

forIn as b f = forIn as.toList b f

Alias of Array.forIn_eq_forIn_toList.

source

@[deprecated Array.forIn_eq_forIn_data]

theorem Array.forIn_eq_data_forIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (as : Array α) (b : β) (f : α → β → m (ForInStep β)) :

forIn as b f = forIn as.toList b f

Alias of Array.forIn_eq_forIn_toList.

zipWith / zip #

source

theorem Array.toList_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (as : Array α) (bs : Array β) :

(as.zipWith bs f).toList = List.zipWith f as.toList bs.toList

source

@[irreducible]

theorem Array.toList_zipWith.loop {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) :

i ≤ as.size → i ≤ bs.size → (Array.zipWithAux f as bs i cs).toList = cs.toList ++ List.zipWith f (List.drop i as.toList) (List.drop i bs.toList)

source

@[deprecated Array.toList_zipWith]

theorem Array.data_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (as : Array α) (bs : Array β) :

(as.zipWith bs f).toList = List.zipWith f as.toList bs.toList

Alias of Array.toList_zipWith.

source

@[deprecated Array.data_zipWith]

theorem Array.zipWith_eq_zipWith_data {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (as : Array α) (bs : Array β) :

(as.zipWith bs f).toList = List.zipWith f as.toList bs.toList

Alias of Array.toList_zipWith.

source

@[simp]

theorem Array.size_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (as : Array α) (bs : Array β) (f : α → β → γ) :

(as.zipWith bs f).size = min as.size bs.size

source

theorem Array.toList_zip {α : Type u_1} {β : Type u_2} (as : Array α) (bs : Array β) :

(as.zip bs).toList = as.toList.zip bs.toList

source

@[deprecated Array.toList_zip]

theorem Array.data_zip {α : Type u_1} {β : Type u_2} (as : Array α) (bs : Array β) :

(as.zip bs).toList = as.toList.zip bs.toList

Alias of Array.toList_zip.

source

@[deprecated Array.data_zip]

theorem Array.zip_eq_zip_data {α : Type u_1} {β : Type u_2} (as : Array α) (bs : Array β) :

(as.zip bs).toList = as.toList.zip bs.toList

Alias of Array.toList_zip.

source

@[simp]

theorem Array.size_zip {α : Type u_1} {β : Type u_2} (as : Array α) (bs : Array β) :

(as.zip bs).size = min as.size bs.size

filter #

source

theorem Array.size_filter_le {α : Type u_1} (p : α → Bool) (l : Array α) :

(Array.filter p l).size ≤ l.size

flatten #

source

@[deprecated Array.toList_flatten]

theorem Array.data_join {α : Type u_1} {l : Array (Array α)} :

l.flatten.toList = (List.map Array.toList l.toList).flatten

Alias of Array.toList_flatten.

source

@[deprecated Array.toList_flatten]

theorem Array.join_data {α : Type u_1} {l : Array (Array α)} :

l.flatten.toList = (List.map Array.toList l.toList).flatten

Alias of Array.toList_flatten.

source

@[deprecated Array.mem_flatten]

theorem Array.mem_join {α : Type u_1} {a : α} {L : Array (Array α)} :

a ∈ L.flatten ↔ ∃ (l : Array α), l ∈ L ∧ a ∈ l

Alias of Array.mem_flatten.

indexOf? #

source

theorem Array.indexOf?_toList {α : Type u_1} [BEq α] {a : α} {l : Array α} :

List.indexOf? a l.toList = Option.map Fin.val (l.indexOf? a)

source

@[irreducible]

theorem Array.indexOf?_toList.aux {α : Type u_1} [BEq α] {a : α} (l : Array α) (i : Nat) :

Option.map (fun (x : Nat) => x + i) (List.indexOf? a (List.drop i l.toList)) = Option.map Fin.val (l.indexOfAux a i)

erase #

source

@[simp]

theorem Array.eraseIdx!_eq_eraseIdx {α : Type u_1} (a : Array α) (i : Nat) :

a.eraseIdx! i = a.eraseIdx i

source

@[simp]

theorem Array.size_eraseIdx {α : Type u_1} (a : Array α) (i : Nat) :

(a.eraseIdx i).size = if i < a.size then a.size - 1 else a.size

set #

source

theorem Array.size_set! {α : Type u_1} (a : Array α) (i : Nat) (v : α) :

(a.set! i v).size = a.size

map #

source

theorem Array.mapM_empty {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) :

Array.mapM f #[] = pure #[]

source

theorem Array.map_empty {α : Type u_1} {β : Type u_2} (f : α → β) :

Array.map f #[] = #[]

mem #

source

theorem Array.mem_singleton {α✝ : Type u_1} {b a : α✝} :

a ∈ #[b] ↔ a = b

append #

source

theorem Array.append_empty {α : Type u_1} (as : Array α) :

as ++ #[] = as

Alias of Array.append_nil.

source

theorem Array.empty_append {α : Type u_1} (as : Array α) :

#[] ++ as = as

Alias of Array.nil_append.

insertAt #

source

@[simp]

theorem Array.size_insertAt {α : Type u_1} (as : Array α) (i : Fin (as.size + 1)) (v : α) :

(as.insertAt i v).size = as.size + 1

source

theorem Array.getElem_insertAt_lt {α : Type u_1} (as : Array α) (i : Fin (as.size + 1)) (v : α) (k : Nat) (hlt : k < ↑i) {hk : k < (as.insertAt i v).size} {hk' : k < as.size} :

(as.insertAt i v)[k] = as[k]

source

theorem Array.getElem_insertAt_gt {α : Type u_1} (as : Array α) (i : Fin (as.size + 1)) (v : α) (k : Nat) (hgt : k > ↑i) {hk : k < (as.insertAt i v).size} {hk' : k - 1 < as.size} :

(as.insertAt i v)[k] = as[k - 1]

source

theorem Array.getElem_insertAt_eq {α : Type u_1} (as : Array α) (i : Fin (as.size + 1)) (v : α) (k : Nat) (heq : ↑i = k) {hk : k < (as.insertAt i v).size} :

(as.insertAt i v)[k] = v

ofFn #

source

@[simp]

theorem Array.toList_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) :

(Array.ofFn f).toList = List.ofFn f

finRange #

source

@[simp]

theorem Array.size_finRange (n : Nat) :

(Array.finRange n).size = n

source

@[simp]

theorem Array.getElem_finRange (n i : Nat) (h : i < (Array.finRange n).size) :

(Array.finRange n)[i] = ⟨i, ⋯⟩

source

@[simp]

theorem Array.toList_finRange (n : Nat) :

(Array.finRange n).toList = List.finRange n