Theorems about Array.

Preliminaries

toList

@[simp]

theorem Array.toList_inj {α : Type u_1} {xs ys : Array α} : xs.toList = ys.toList ↔ xs = ys

@[simp]

theorem Array.toList_eq_nil_iff {α : Type u_1} (xs : Array α) : xs.toList = [] ↔ xs = #[]

@[simp]

theorem Array.mem_toList_iff {α : Type u_1} (a : α) (xs : Array α) : a ∈ xs.toList ↔ a ∈ xs

@[simp]

theorem Array.length_toList {α : Type u_1} {xs : Array α} : xs.toList.length = xs.size

theorem Array.eq_toArray {α✝ : Type u_1} {xs : Array α✝} {as : List α✝} : xs = as.toArray ↔ xs.toList = as

theorem Array.toArray_eq {α✝ : Type u_1} {as : List α✝} {xs : Array α✝} : as.toArray = xs ↔ as = xs.toList

empty

@[simp]

theorem Array.empty_eq {α : Type u_1} {xs : Array α} : #[] = xs ↔ xs = #[]

theorem Array.size_empty {α : Type u_1} : #[].size = 0

@[simp]

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

size

theorem Array.eq_empty_of_size_eq_zero {α✝ : Type u_1} {xs : Array α✝} (h : xs.size = 0) : xs = #[]

theorem Array.ne_empty_of_size_eq_add_one {n : Nat} {α✝ : Type u_1} {xs : Array α✝} (h : xs.size = n + 1) : xs ≠ #[]

theorem Array.ne_empty_of_size_pos {α✝ : Type u_1} {xs : Array α✝} (h : 0 < xs.size) : xs ≠ #[]

theorem Array.size_eq_zero_iff {α✝ : Type u_1} {xs : Array α✝} : xs.size = 0 ↔ xs = #[]

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

abbrev Array.size_eq_zero {α✝ : Type u_1} {xs : Array α✝} : xs.size = 0 ↔ xs = #[]

Equations

• @Array.size_eq_zero = @Array.size_eq_zero_iff

theorem Array.eq_empty_iff_size_eq_zero {α✝ : Type u_1} {xs : Array α✝} : xs = #[] ↔ xs.size = 0

theorem Array.size_pos_of_mem {α : Type u_1} {a : α} {xs : Array α} (h : a ∈ xs) : 0 < xs.size

theorem Array.exists_mem_of_size_pos {α : Type u_1} {xs : Array α} (h : 0 < xs.size) : ∃ (a : α), a ∈ xs

theorem Array.size_pos_iff_exists_mem {α : Type u_1} {xs : Array α} : 0 < xs.size ↔ ∃ (a : α), a ∈ xs

theorem Array.exists_mem_of_size_eq_add_one {α : Type u_1} {n : Nat} {xs : Array α} (h : xs.size = n + 1) : ∃ (a : α), a ∈ xs

theorem Array.size_pos_iff {α : Type u_1} {xs : Array α} : 0 < xs.size ↔ xs ≠ #[]

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

abbrev Array.size_pos {α : Type u_1} {xs : Array α} : 0 < xs.size ↔ xs ≠ #[]

Equations

• @Array.size_pos = @Array.size_pos_iff

theorem Array.size_eq_one_iff {α : Type u_1} {xs : Array α} : xs.size = 1 ↔ ∃ (a : α), xs = #[a]

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

abbrev Array.size_eq_one {α : Type u_1} {xs : Array α} : xs.size = 1 ↔ ∃ (a : α), xs = #[a]

Equations

• @Array.size_eq_one = @Array.size_eq_one_iff

L[i] and L[i]?

@[simp]

theorem Array.getElem?_eq_none_iff {α : Type u_1} {i : Nat} {xs : Array α} : xs[i]? = none ↔ xs.size ≤ i

@[simp]

theorem Array.none_eq_getElem?_iff {α : Type u_1} {xs : Array α} {i : Nat} : none = xs[i]? ↔ xs.size ≤ i

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

@[simp]

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

theorem Array.getElem?_eq_some_iff {α : Type u_1} {i : Nat} {b : α} {xs : Array α} : xs[i]? = some b ↔ ∃ (h : i < xs.size), xs[i] = b

theorem Array.some_eq_getElem?_iff {α : Type u_1} {b : α} {i : Nat} {xs : Array α} : some b = xs[i]? ↔ ∃ (h : i < xs.size), xs[i] = b

@[simp]

theorem Array.some_getElem_eq_getElem?_iff {α : Type u_1} (xs : Array α) (i : Nat) (h : i < xs.size) : some xs[i] = xs[i]? ↔ True

@[simp]

theorem Array.getElem?_eq_some_getElem_iff {α : Type u_1} (xs : Array α) (i : Nat) (h : i < xs.size) : xs[i]? = some xs[i] ↔ True

theorem Array.getElem_eq_iff {α : Type u_1} {x : α} {xs : Array α} {i : Nat} {h : i < xs.size} : xs[i] = x ↔ xs[i]? = some x

theorem Array.getElem_eq_getElem?_get {α : Type u_1} (xs : Array α) (i : Nat) (h : i < xs.size) : xs[i] = xs[i]?.get ⋯

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

@[simp]

theorem Array.getElem?_empty {α : Type u_1} {i : Nat} : #[][i]? = none

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

@[simp]

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

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

theorem Array.getElem?_push {α : Type u_1} {i : Nat} {xs : Array α} {x : α} : (xs.push x)[i]? = if i = xs.size then some x else xs[i]?

@[simp]

theorem Array.getElem?_push_size {α : Type u_1} {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some x

@[simp]

theorem Array.getElem_singleton {α : Type u_1} {i : Nat} (a : α) (h : i < 1) : #[a][i] = a

theorem Array.getElem?_singleton {α : Type u_1} (a : α) (i : Nat) : #[a][i]? = if i = 0 then some a else none

theorem Array.ext_getElem? {α : Type u_1} {xs ys : Array α} (h : ∀ (i : Nat), xs[i]? = ys[i]?) : xs = ys

pop

@[simp]

theorem Array.pop_empty {α : Type u_1} : #[].pop = #[]

@[simp]

theorem Array.pop_push {α : Type u_1} {x : α} (xs : Array α) : (xs.push x).pop = xs

@[simp]

theorem Array.getElem_pop {α : Type u_1} {xs : Array α} {i : Nat} (h : i < xs.pop.size) : xs.pop[i] = xs[i]

theorem Array.getElem?_pop {α : Type u_1} (xs : Array α) (i : Nat) : xs.pop[i]? = if i < xs.size - 1 then xs[i]? else none

theorem Array.back_pop {α : Type u_1} {xs : Array α} (h : 0 < xs.pop.size) : xs.pop.back h = xs[xs.size - 2]

theorem Array.back?_pop {α : Type u_1} {xs : Array α} : xs.pop.back? = if xs.size ≤ 1 then none else xs[xs.size - 2]?

@[simp]

theorem Array.pop_append_of_ne_empty {α : Type u_1} {xs ys : Array α} (h : ys ≠ #[]) : (xs ++ ys).pop = xs ++ ys.pop

push

@[simp]

theorem Array.push_ne_empty {α : Type u_1} {a : α} {xs : Array α} : xs.push a ≠ #[]

@[simp]

theorem Array.push_ne_self {α : Type u_1} {a : α} {xs : Array α} : xs.push a ≠ xs

@[simp]

theorem Array.ne_push_self {α : Type u_1} {a : α} {xs : Array α} : xs ≠ xs.push a

theorem Array.back_eq_of_push_eq {α : Type u_1} {a b : α} {xs ys : Array α} (h : xs.push a = ys.push b) : a = b

theorem Array.pop_eq_of_push_eq {α : Type u_1} {a b : α} {xs ys : Array α} (h : xs.push a = ys.push b) : xs = ys

theorem Array.push_inj_left {α : Type u_1} {a : α} {xs ys : Array α} : xs.push a = ys.push a ↔ xs = ys

theorem Array.push_inj_right {α : Type u_1} {a b : α} {xs : Array α} : xs.push a = xs.push b ↔ a = b

theorem Array.push_eq_push {α : Type u_1} {a b : α} {xs ys : Array α} : xs.push a = ys.push b ↔ a = b ∧ xs = ys

theorem Array.push_eq_append_singleton {α : Type u_1} (as : Array α) (x : α) : as.push x = as ++ #[x]

theorem Array.exists_push_of_ne_empty {α : Type u_1} {xs : Array α} (h : xs ≠ #[]) : ∃ (ys : Array α), ∃ (a : α), xs = ys.push a

theorem Array.ne_empty_iff_exists_push {α : Type u_1} {xs : Array α} : xs ≠ #[] ↔ ∃ (ys : Array α), ∃ (a : α), xs = ys.push a

theorem Array.exists_push_of_size_pos {α : Type u_1} {xs : Array α} (h : 0 < xs.size) : ∃ (ys : Array α), ∃ (a : α), xs = ys.push a

theorem Array.size_pos_iff_exists_push {α : Type u_1} {xs : Array α} : 0 < xs.size ↔ ∃ (ys : Array α), ∃ (a : α), xs = ys.push a

theorem Array.exists_push_of_size_eq_add_one {α : Type u_1} {n : Nat} {xs : Array α} (h : xs.size = n + 1) : ∃ (ys : Array α), ∃ (a : α), xs = ys.push a

theorem Array.eq_push_pop_back!_of_size_ne_zero {α : Type u_1} [Inhabited α] {xs : Array α} (h : xs.size ≠ 0) : xs = xs.pop.push xs.back!

theorem Array.eq_push_of_size_ne_zero {α : Type u_1} {xs : Array α} (h : xs.size ≠ 0) : ∃ (bs : Array α), ∃ (c : α), xs = bs.push c

theorem Array.singleton_inj {α✝ : Type u_1} {a b : α✝} : #[a] = #[b] ↔ a = b

mkArray

@[simp]

theorem Array.size_mkArray {α : Type u_1} (n : Nat) (v : α) : (mkArray n v).size = n

@[simp]

theorem Array.toList_mkArray {n : Nat} {α✝ : Type u_1} {a : α✝} : (mkArray n a).toList = List.replicate n a

@[simp]

theorem Array.mkArray_zero {α✝ : Type u_1} {a : α✝} : mkArray 0 a = #[]

theorem Array.mkArray_succ {n : Nat} {α✝ : Type u_1} {a : α✝} : mkArray (n + 1) a = (mkArray n a).push a

@[simp]

theorem Array.getElem_mkArray {α : Type u_1} {i : Nat} (n : Nat) (v : α) (h : i < (mkArray n v).size) : (mkArray n v)[i] = v

theorem Array.getElem?_mkArray {α : Type u_1} (n : Nat) (v : α) (i : Nat) : (mkArray n v)[i]? = if i < n then some v else none

mem

theorem Array.not_mem_empty {α : Type u_1} (a : α) : ¬a ∈ #[]

@[simp]

theorem Array.mem_push {α : Type u_1} {xs : Array α} {x y : α} : x ∈ xs.push y ↔ x ∈ xs ∨ x = y

theorem Array.mem_push_self {α : Type u_1} {xs : Array α} {x : α} : x ∈ xs.push x

theorem Array.eq_push_append_of_mem {α : Type u_1} {xs : Array α} {x : α} (h : x ∈ xs) : ∃ (as : Array α), ∃ (bs : Array α), xs = as.push x ++ bs ∧ ¬x ∈ as

theorem Array.mem_push_of_mem {α : Type u_1} {xs : Array α} {x : α} (y : α) (h : x ∈ xs) : x ∈ xs.push y

theorem Array.exists_mem_of_ne_empty {α : Type u_1} (xs : Array α) (h : xs ≠ #[]) : ∃ (x : α), x ∈ xs

theorem Array.eq_empty_iff_forall_not_mem {α : Type u_1} {xs : Array α} : xs = #[] ↔ ∀ (a : α), ¬a ∈ xs

@[simp]

theorem Array.mem_dite_empty_left {α : Type u_1} {p : Prop} {x : α} [Decidable p] {xs : ¬p → Array α} : (x ∈ if h : p then #[] else xs h) ↔ ∃ (h : ¬p), x ∈ xs h

@[simp]

theorem Array.mem_dite_empty_right {α : Type u_1} {p : Prop} {x : α} [Decidable p] {xs : p → Array α} : (x ∈ if h : p then xs h else #[]) ↔ ∃ (h : p), x ∈ xs h

@[simp]

theorem Array.mem_ite_empty_left {α : Type u_1} {p : Prop} {x : α} [Decidable p] {xs : Array α} : (x ∈ if p then #[] else xs) ↔ ¬p ∧ x ∈ xs

@[simp]

theorem Array.mem_ite_empty_right {α : Type u_1} {p : Prop} {x : α} [Decidable p] {xs : Array α} : (x ∈ if p then xs else #[]) ↔ p ∧ x ∈ xs

theorem Array.eq_of_mem_singleton {α✝ : Type u_1} {b a : α✝} (h : a ∈ #[b]) : a = b

@[simp]

theorem Array.mem_singleton {α : Type u_1} {a b : α} : a ∈ #[b] ↔ a = b

theorem Array.forall_mem_push {α : Type u_1} {p : α → Prop} {xs : Array α} {a : α} : (∀ (x : α), x ∈ xs.push a → p x) ↔ p a ∧ ∀ (x : α), x ∈ xs → p x

theorem Array.forall_mem_ne {α : Type u_1} {a : α} {xs : Array α} : (∀ (a' : α), a' ∈ xs → ¬a = a') ↔ ¬a ∈ xs

theorem Array.forall_mem_ne' {α : Type u_1} {a : α} {xs : Array α} : (∀ (a' : α), a' ∈ xs → ¬a' = a) ↔ ¬a ∈ xs

theorem Array.exists_mem_empty {α : Type u_1} (p : α → Prop) : ¬∃ (x : α), ∃ (x_1 : x ∈ #[]), p x

theorem Array.forall_mem_empty {α : Type u_1} (p : α → Prop) (x : α) : x ∈ #[] → p x

theorem Array.exists_mem_push {α : Type u_1} {p : α → Prop} {a : α} {xs : Array α} : (∃ (x : α), ∃ (x_1 : x ∈ xs.push a), p x) ↔ p a ∨ ∃ (x : α), ∃ (x_1 : x ∈ xs), p x

theorem Array.forall_mem_singleton {α : Type u_1} {p : α → Prop} {a : α} : (∀ (x : α), x ∈ #[a] → p x) ↔ p a

theorem Array.mem_empty_iff {α : Type u_1} (a : α) : a ∈ #[] ↔ False

theorem Array.mem_singleton_self {α : Type u_1} (a : α) : a ∈ #[a]

theorem Array.mem_of_mem_push_of_mem {α : Type u_1} {a b : α} {xs : Array α} : a ∈ xs.push b → b ∈ xs → a ∈ xs

theorem Array.eq_or_ne_mem_of_mem {α : Type u_1} {a b : α} {xs : Array α} (h' : a ∈ xs.push b) : a = b ∨ a ≠ b ∧ a ∈ xs

theorem Array.ne_empty_of_mem {α : Type u_1} {a : α} {xs : Array α} (h : a ∈ xs) : xs ≠ #[]

theorem Array.mem_of_ne_of_mem {α : Type u_1} {a y : α} {xs : Array α} (h₁ : a ≠ y) (h₂ : a ∈ xs.push y) : a ∈ xs

theorem Array.ne_of_not_mem_push {α : Type u_1} {a b : α} {xs : Array α} (h : ¬a ∈ xs.push b) : a ≠ b

theorem Array.not_mem_of_not_mem_push {α : Type u_1} {a b : α} {xs : Array α} (h : ¬a ∈ xs.push b) : ¬a ∈ xs

theorem Array.not_mem_push_of_ne_of_not_mem {α : Type u_1} {a y : α} {xs : Array α} : a ≠ y → ¬a ∈ xs → ¬a ∈ xs.push y

theorem Array.ne_and_not_mem_of_not_mem_push {α : Type u_1} {a y : α} {xs : Array α} : ¬a ∈ xs.push y → a ≠ y ∧ ¬a ∈ xs

theorem Array.getElem_of_mem {α : Type u_1} {a : α} {xs : Array α} (h : a ∈ xs) : ∃ (i : Nat), ∃ (h : i < xs.size), xs[i] = a

theorem Array.getElem?_of_mem {α : Type u_1} {a : α} {xs : Array α} (h : a ∈ xs) : ∃ (i : Nat), xs[i]? = some a

theorem Array.mem_of_getElem {α : Type u_1} {xs : Array α} {i : Nat} {h : i < xs.size} {a : α} (e : xs[i] = a) : a ∈ xs

theorem Array.mem_of_getElem? {α : Type u_1} {xs : Array α} {i : Nat} {a : α} (e : xs[i]? = some a) : a ∈ xs

theorem Array.mem_iff_getElem {α : Type u_1} {a : α} {xs : Array α} : a ∈ xs ↔ ∃ (i : Nat), ∃ (h : i < xs.size), xs[i] = a

theorem Array.mem_iff_getElem? {α : Type u_1} {a : α} {xs : Array α} : a ∈ xs ↔ ∃ (i : Nat), xs[i]? = some a

theorem Array.forall_getElem {α : Type u_1} {xs : Array α} {p : α → Prop} : (∀ (i : Nat) (h : i < xs.size), p xs[i]) ↔ ∀ (a : α), a ∈ xs → p a

isEmpty

@[simp]

theorem Array.isEmpty_toList {α : Type u_1} {xs : Array α} : xs.toList.isEmpty = xs.isEmpty

theorem Array.isEmpty_eq_false_iff_exists_mem {α : Type u_1} {xs : Array α} : xs.isEmpty = false ↔ ∃ (x : α), x ∈ xs

@[simp]

theorem Array.isEmpty_iff {α : Type u_1} {xs : Array α} : xs.isEmpty = true ↔ xs = #[]

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

abbrev Array.isEmpty_eq_true {α : Type u_1} {xs : Array α} : xs.isEmpty = true ↔ xs = #[]

Equations

• @Array.isEmpty_eq_true = @Array.isEmpty_iff

@[simp]

theorem Array.isEmpty_eq_false_iff {α : Type u_1} {xs : Array α} : xs.isEmpty = false ↔ xs ≠ #[]

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

abbrev Array.isEmpty_eq_false {α : Type u_1} {xs : Array α} : xs.isEmpty = false ↔ xs ≠ #[]

Equations

• @Array.isEmpty_eq_false = @Array.isEmpty_eq_false_iff

theorem Array.isEmpty_iff_size_eq_zero {α : Type u_1} {xs : Array α} : xs.isEmpty = true ↔ xs.size = 0

Decidability of bounded quantifiers

instance Array.instDecidableForallForallMemOfDecidablePred {α : Type u_1} {xs : Array α} {p : α → Prop} [DecidablePred p] : Decidable (∀ (x : α), x ∈ xs → p x)

Equations

• Array.instDecidableForallForallMemOfDecidablePred = decidable_of_iff (∀ (i : Nat) (h : i < xs.size), p xs[i]) ⋯

instance Array.instDecidableExistsAndMemOfDecidablePred {α : Type u_1} {xs : Array α} {p : α → Prop} [DecidablePred p] : Decidable (∃ (x : α), x ∈ xs ∧ p x)

Equations

• Array.instDecidableExistsAndMemOfDecidablePred = decidable_of_iff (∃ (i : Nat), ∃ (h : i < xs.size), p xs[i]) ⋯

any / all

theorem Array.anyM_eq_anyM_loop {m : Type → Type u_1} {α : Type u_2} [Monad m] (p : α → m Bool) (as : Array α) (start stop : Nat) : anyM p as start stop = 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 stop : Nat) (h : min stop as.size ≤ start) : anyM p as start stop = pure false

@[irreducible]

theorem Array.anyM_loop_cons {m : Type → Type u_1} {α : Type u_2} [Monad m] (p : α → m Bool) (a : α) (as : List α) (stop start : Nat) (h : stop + 1 ≤ (a :: as).length) : anyM.loop p { toList := a :: as } (stop + 1) h (start + 1) = anyM.loop p { toList := as } stop ⋯ start

@[simp, irreducible]

theorem Array.anyM_toList {m : Type → Type u_1} {α : Type u_2} [Monad m] (p : α → m Bool) (as : Array α) : List.anyM p as.toList = anyM p as

@[irreducible]

theorem Array.anyM_loop_iff_exists {α : Type u_1} {p : α → Bool} {as : Array α} {start stop : Nat} (h : stop ≤ as.size) : anyM.loop p as stop h start = true ↔ ∃ (i : Nat), ∃ (x : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] = true

theorem Array.any_iff_exists {α : Type u_1} {p : α → Bool} {as : Array α} {start stop : Nat} : as.any p start stop = true ↔ ∃ (i : Nat), ∃ (x : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] = true

@[simp]

theorem Array.any_eq_true {α : Type u_1} {p : α → Bool} {as : Array α} : as.any p = true ↔ ∃ (i : Nat), ∃ (x : i < as.size), p as[i] = true

@[simp]

theorem Array.any_eq_false {α : Type u_1} {p : α → Bool} {as : Array α} : as.any p = false ↔ ∀ (i : Nat) (x : i < as.size), ¬p as[i] = true

@[simp]

theorem Array.any_toList {α : Type u_1} {p : α → Bool} (as : Array α) : as.toList.any p = as.any p

theorem Array.allM_eq_not_anyM_not {m : Type → Type u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) : allM p as = (fun (x : Bool) => !x) <$> anyM (fun (x : α) => (fun (x : Bool) => !x) <$> p x) as

@[simp]

theorem Array.allM_toList {m : Type → Type u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) : List.allM p as.toList = allM p as

theorem Array.all_eq_not_any_not {α : Type u_1} (p : α → Bool) (as : Array α) (start stop : Nat) : as.all p start stop = !as.any (fun (x : α) => !p x) start stop

theorem Array.all_iff_forall {α : Type u_1} {p : α → Bool} {as : Array α} {start stop : Nat} : as.all p start stop = true ↔ ∀ (i : Nat) (x : i < as.size), start ≤ i ∧ i < stop → p as[i] = true

@[simp]

theorem Array.all_eq_true {α : Type u_1} {p : α → Bool} {as : Array α} : as.all p = true ↔ ∀ (i : Nat) (x : i < as.size), p as[i] = true

@[simp]

theorem Array.all_eq_false {α : Type u_1} {p : α → Bool} {as : Array α} : as.all p = false ↔ ∃ (i : Nat), ∃ (x : i < as.size), ¬p as[i] = true

@[simp]

theorem Array.all_toList {α : Type u_1} {p : α → Bool} (as : Array α) : as.toList.all p = as.all p

theorem Array.all_eq_true_iff_forall_mem {α : Type u_1} {p : α → Bool} {xs : Array α} : xs.all p = true ↔ ∀ (x : α), x ∈ xs → p x = true

@[simp]

theorem List.anyM_toArray' {m : Type → Type u_1} {α : Type u_2} {stop : Nat} [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) (h : stop = l.toArray.size) : Array.anyM p l.toArray 0 stop = anyM p l

Variant of anyM_toArray with a side condition on stop.

@[simp]

theorem List.any_toArray' {α : Type u_1} {stop : Nat} (p : α → Bool) (l : List α) (h : stop = l.toArray.size) : l.toArray.any p 0 stop = l.any p

Variant of any_toArray with a side condition on stop.

@[simp]

theorem List.allM_toArray' {m : Type → Type u_1} {α : Type u_2} {stop : Nat} [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) (h : stop = l.toArray.size) : Array.allM p l.toArray 0 stop = allM p l

Variant of allM_toArray with a side condition on stop.

@[simp]

theorem List.all_toArray' {α : Type u_1} {stop : Nat} (p : α → Bool) (l : List α) (h : stop = l.toArray.size) : l.toArray.all p 0 stop = l.all p

Variant of all_toArray with a side condition on stop.

theorem List.anyM_toArray {m : Type → Type u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) : Array.anyM p l.toArray = anyM p l

theorem List.any_toArray {α : Type u_1} (p : α → Bool) (l : List α) : l.toArray.any p = l.any p

theorem List.allM_toArray {m : Type → Type u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) : Array.allM p l.toArray = allM p l

theorem List.all_toArray {α : Type u_1} (p : α → Bool) (l : List α) : l.toArray.all p = l.all p

theorem Array.any_eq_true' {α : Type u_1} {p : α → Bool} {as : Array α} : as.any p = true ↔ ∃ (x : α), x ∈ as ∧ p x = true

Variant of any_eq_true in terms of membership rather than an array index.

theorem Array.any_eq_false' {α : Type u_1} {p : α → Bool} {as : Array α} : as.any p = false ↔ ∀ (x : α), x ∈ as → ¬p x = true

Variant of any_eq_false in terms of membership rather than an array index.

theorem Array.all_eq_true' {α : Type u_1} {p : α → Bool} {as : Array α} : as.all p = true ↔ ∀ (x : α), x ∈ as → p x = true

Variant of all_eq_true in terms of membership rather than an array index.

theorem Array.all_eq_false' {α : Type u_1} {p : α → Bool} {as : Array α} : as.all p = false ↔ ∃ (x : α), x ∈ as ∧ ¬p x = true

Variant of all_eq_false in terms of membership rather than an array index.

theorem Array.any_eq {α : Type u_1} {xs : Array α} {p : α → Bool} : xs.any p = decide (∃ (i : Nat), ∃ (h : i < xs.size), p xs[i] = true)

theorem Array.any_eq' {α : Type u_1} {xs : Array α} {p : α → Bool} : xs.any p = decide (∃ (x : α), x ∈ xs ∧ p x = true)

Variant of any_eq in terms of membership rather than an array index.

theorem Array.all_eq {α : Type u_1} {xs : Array α} {p : α → Bool} : xs.all p = decide (∀ (i : Nat) (x : i < xs.size), p xs[i] = true)

theorem Array.all_eq' {α : Type u_1} {xs : Array α} {p : α → Bool} : xs.all p = decide (∀ (x : α), x ∈ xs → p x = true)

Variant of all_eq in terms of membership rather than an array index.

theorem Array.decide_exists_mem {α : Type u_1} {xs : Array α} {p : α → Prop} [DecidablePred p] : decide (∃ (x : α), x ∈ xs ∧ p x) = xs.any fun (b : α) => decide (p b)

theorem Array.decide_forall_mem {α : Type u_1} {xs : Array α} {p : α → Prop} [DecidablePred p] : decide (∀ (x : α), x ∈ xs → p x) = xs.all fun (b : α) => decide (p b)

@[simp]

theorem List.contains_toArray {α : Type u_1} [BEq α] {l : List α} {a : α} : l.toArray.contains a = l.contains a

theorem List.elem_toArray {α : Type u_1} [BEq α] {l : List α} {a : α} : Array.elem a l.toArray = elem a l

theorem Array.any_beq {α : Type u_1} [BEq α] {xs : Array α} {a : α} : (xs.any fun (x : α) => a == x) = xs.contains a

theorem Array.any_beq' {α : Type u_1} {a : α} [BEq α] [PartialEquivBEq α] {xs : Array α} : (xs.any fun (x : α) => x == a) = xs.contains a

Variant of any_beq with == reversed.

theorem Array.all_bne {α : Type u_1} {a : α} [BEq α] {xs : Array α} : (xs.all fun (x : α) => a != x) = !xs.contains a

theorem Array.all_bne' {α : Type u_1} {a : α} [BEq α] [PartialEquivBEq α] {xs : Array α} : (xs.all fun (x : α) => x != a) = !xs.contains a

Variant of all_bne with != reversed.

theorem Array.mem_of_contains_eq_true {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {as : Array α} : as.contains a = true → a ∈ as

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

abbrev Array.mem_of_elem_eq_true {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {as : Array α} : as.contains a = true → a ∈ as

Equations

• @Array.mem_of_elem_eq_true = @Array.mem_of_contains_eq_true

theorem Array.contains_eq_true_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a ∈ as) : as.contains a = true

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

abbrev Array.elem_eq_true_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a ∈ as) : as.contains a = true

Equations

• @Array.elem_eq_true_of_mem = @Array.contains_eq_true_of_mem

instance Array.instDecidableMemOfLawfulBEq {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (as : Array α) : Decidable (a ∈ as)

Equations

• Array.instDecidableMemOfLawfulBEq a as = decidable_of_decidable_of_iff ⋯

@[simp]

theorem Array.elem_eq_contains {α : Type u_1} [BEq α] {a : α} {xs : Array α} : elem a xs = xs.contains a

theorem Array.elem_iff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs : Array α} : elem a xs = true ↔ a ∈ xs

theorem Array.contains_iff {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {xs : Array α} : xs.contains a = true ↔ a ∈ xs

theorem Array.elem_eq_mem {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (xs : Array α) : elem a xs = decide (a ∈ xs)

@[simp]

theorem Array.contains_eq_mem {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (xs : Array α) : xs.contains a = decide (a ∈ xs)

@[simp]

theorem Array.any_push' {α : Type u_1} {stop : Nat} [BEq α] {xs : Array α} {a : α} {p : α → Bool} (h : stop = xs.size + 1) : (xs.push a).any p 0 stop = (xs.any p || p a)

Variant of any_push with a side condition on stop.

theorem Array.any_push {α : Type u_1} [BEq α] {xs : Array α} {a : α} {p : α → Bool} : (xs.push a).any p = (xs.any p || p a)

@[simp]

theorem Array.all_push' {α : Type u_1} {stop : Nat} [BEq α] {xs : Array α} {a : α} {p : α → Bool} (h : stop = xs.size + 1) : (xs.push a).all p 0 stop = (xs.all p && p a)

Variant of all_push with a side condition on stop.

theorem Array.all_push {α : Type u_1} [BEq α] {xs : Array α} {a : α} {p : α → Bool} : (xs.push a).all p = (xs.all p && p a)

@[simp]

theorem Array.contains_push {α : Type u_1} [BEq α] {xs : Array α} {a b : α} : (xs.push a).contains b = (xs.contains b || b == a)

set

@[simp]

theorem Array.getElem_set_self {α : Type u_1} (xs : Array α) (i : Nat) (h : i < xs.size) (v : α) : (xs.set i v h)[i] = v

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

abbrev Array.getElem_set_eq {α : Type u_1} (xs : Array α) (i : Nat) (h : i < xs.size) (v : α) : (xs.set i v h)[i] = v

Equations

• @Array.getElem_set_eq = @Array.getElem_set_self

@[simp]

theorem Array.getElem?_set_self {α : Type u_1} (xs : Array α) (i : Nat) (h : i < xs.size) (v : α) : (xs.set i v h)[i]? = some v

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

abbrev Array.getElem?_set_eq {α : Type u_1} (xs : Array α) (i : Nat) (h : i < xs.size) (v : α) : (xs.set i v h)[i]? = some v

Equations

• @Array.getElem?_set_eq = @Array.getElem?_set_self

@[simp]

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

@[simp]

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

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

theorem Array.getElem?_set {α : Type u_1} (xs : Array α) (i : Nat) (h : i < xs.size) (v : α) (j : Nat) : (xs.set i v h)[j]? = if i = j then some v else xs[j]?

@[simp]

theorem Array.set_getElem_self {α : Type u_1} {xs : Array α} {i : Nat} (h : i < xs.size) : xs.set i xs[i] h = xs

@[simp]

theorem Array.set_eq_empty_iff {α : Type u_1} {xs : Array α} (i : Nat) (a : α) (h : i < xs.size) : xs.set i a h = #[] ↔ xs = #[]

theorem Array.set_comm {α : Type u_1} (a b : α) {i j : Nat} (xs : Array α) {hi : i < xs.size} {hj : j < (xs.set i a hi).size} (h : i ≠ j) : (xs.set i a hi).set j b hj = (xs.set j b ⋯).set i a ⋯

@[simp]

theorem Array.set_set {α : Type u_1} (a b : α) (xs : Array α) (i : Nat) (h : i < xs.size) : (xs.set i a h).set i b ⋯ = xs.set i b h

theorem Array.mem_set {α : Type u_1} (xs : Array α) (i : Nat) (h : i < xs.size) (a : α) : a ∈ xs.set i a h

theorem Array.mem_or_eq_of_mem_set {α : Type u_1} {xs : Array α} {i : Nat} {a b : α} {w : i < xs.size} (h : a ∈ xs.set i b w) : a ∈ xs ∨ a = b

setIfInBounds

@[simp]

theorem Array.set!_eq_setIfInBounds : @set! = @setIfInBounds

@[reducible, inline, deprecated Array.set!_eq_setIfInBounds (since := "2024-12-12")]

abbrev Array.set!_is_setIfInBounds : @set! = @setIfInBounds

Equations

• Array.set!_is_setIfInBounds = Array.set!_eq_setIfInBounds

@[simp]

theorem Array.size_setIfInBounds {α : Type u_1} (xs : Array α) (i : Nat) (a : α) : (xs.setIfInBounds i a).size = xs.size

theorem Array.getElem_setIfInBounds {α : Type u_1} (xs : Array α) (i : Nat) (a : α) (j : Nat) (hj : j < xs.size) : (xs.setIfInBounds i a)[j] = if i = j then a else xs[j]

@[simp]

theorem Array.getElem_setIfInBounds_self {α : Type u_1} (xs : Array α) {i : Nat} (a : α) (h : i < (xs.setIfInBounds i a).size) : (xs.setIfInBounds i a)[i] = a

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

abbrev Array.getElem_setIfInBounds_eq {α : Type u_1} (xs : Array α) {i : Nat} (a : α) (h : i < (xs.setIfInBounds i a).size) : (xs.setIfInBounds i a)[i] = a

Equations

• @Array.getElem_setIfInBounds_eq = @Array.getElem_setIfInBounds_self

@[simp]

theorem Array.getElem_setIfInBounds_ne {α : Type u_1} (xs : Array α) {i : Nat} (a : α) {j : Nat} (hj : j < xs.size) (h : i ≠ j) : (xs.setIfInBounds i a)[j] = xs[j]

theorem Array.getElem?_setIfInBounds {α : Type u_1} {xs : Array α} {i j : Nat} {a : α} : (xs.setIfInBounds i a)[j]? = if i = j then if i < xs.size then some a else none else xs[j]?

theorem Array.getElem?_setIfInBounds_self {α : Type u_1} (xs : Array α) {i : Nat} (a : α) : (xs.setIfInBounds i a)[i]? = if i < xs.size then some a else none

@[simp]

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

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

abbrev Array.getElem?_setIfInBounds_eq {α : Type u_1} (xs : Array α) {i : Nat} (a : α) : (xs.setIfInBounds i a)[i]? = if i < xs.size then some a else none

Equations

• @Array.getElem?_setIfInBounds_eq = @Array.getElem?_setIfInBounds_self

@[simp]

theorem Array.getElem?_setIfInBounds_ne {α : Type u_1} {xs : Array α} {i j : Nat} (h : i ≠ j) {a : α} : (xs.setIfInBounds i a)[j]? = xs[j]?

theorem Array.setIfInBounds_eq_of_size_le {α : Type u_1} {xs : Array α} {i : Nat} (h : xs.size ≤ i) {a : α} : xs.setIfInBounds i a = xs

@[simp]

theorem Array.setIfInBounds_eq_empty_iff {α : Type u_1} {xs : Array α} (i : Nat) (a : α) : xs.setIfInBounds i a = #[] ↔ xs = #[]

theorem Array.setIfInBounds_comm {α : Type u_1} (a b : α) {i j : Nat} (xs : Array α) (h : i ≠ j) : (xs.setIfInBounds i a).setIfInBounds j b = (xs.setIfInBounds j b).setIfInBounds i a

@[simp]

theorem Array.setIfInBounds_setIfInBounds {α : Type u_1} (a b : α) (xs : Array α) (i : Nat) : (xs.setIfInBounds i a).setIfInBounds i b = xs.setIfInBounds i b

theorem Array.mem_setIfInBounds {α : Type u_1} (xs : Array α) (i : Nat) (h : i < xs.size) (a : α) : a ∈ xs.setIfInBounds i a

theorem Array.mem_or_eq_of_mem_setIfInBounds {α : Type u_1} {xs : Array α} {i : Nat} {a b : α} (h : a ∈ xs.setIfInBounds i b) : a ∈ xs ∨ a = b

@[simp]

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

Simplifies a normal form from get!

@[simp]

theorem Array.toList_setIfInBounds {α : Type u_1} (xs : Array α) (i : Nat) (x : α) : (xs.setIfInBounds i x).toList = xs.toList.set i x

BEq

@[simp]

theorem Array.beq_empty_iff {α : Type u_1} [BEq α] {xs : Array α} : (xs == #[]) = xs.isEmpty

@[simp]

theorem Array.empty_beq_iff {α : Type u_1} [BEq α] {xs : Array α} : (#[] == xs) = xs.isEmpty

@[simp]

theorem Array.push_beq_push {α : Type u_1} [BEq α] {a b : α} {xs ys : Array α} : (xs.push a == ys.push b) = (xs == ys && a == b)

theorem Array.size_eq_of_beq {α : Type u_1} [BEq α] {xs ys : Array α} (h : (xs == ys) = true) : xs.size = ys.size

@[simp, irreducible]

theorem Array.mkArray_beq_mkArray {α : Type u_1} [BEq α] {a b : α} {n : Nat} : (mkArray n a == mkArray n b) = (n == 0 || a == b)

@[simp]

theorem Array.reflBEq_iff {α : Type u_1} [BEq α] : ReflBEq (Array α) ↔ ReflBEq α

@[simp]

theorem Array.lawfulBEq_iff {α : Type u_1} [BEq α] : LawfulBEq (Array α) ↔ LawfulBEq α

isEqv

@[simp]

theorem Array.isEqv_eq {α : Type u_1} [DecidableEq α] {xs ys : Array α} : ((xs.isEqv ys fun (x1 x2 : α) => x1 == x2) = true) = (xs = ys)

back

theorem Array.back_eq_getElem {α : Type u_1} (xs : Array α) (h : 0 < xs.size) : xs.back h = xs[xs.size - 1]

theorem Array.back?_eq_getElem? {α : Type u_1} (xs : Array α) : xs.back? = xs[xs.size - 1]?

@[simp]

theorem Array.back_mem {α : Type u_1} {xs : Array α} (h : 0 < xs.size) : xs.back h ∈ xs

map

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

@[irreducible]

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 β) (xs : Array α) (i : Nat) (bs : Array β) : mapM.map f xs i bs = List.foldlM (fun (bs : Array β) (a : α) => bs.push <$> f a) bs (List.drop i xs.toList)

@[simp]

theorem Array.toList_map {α : Type u_1} {β : Type u_2} (f : α → β) (xs : Array α) : (map f xs).toList = List.map f xs.toList

@[simp]

theorem List.map_toArray {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : Array.map f l.toArray = (map f l).toArray

@[simp]

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

@[simp]

theorem Array.getElem_map {α : Type u_1} {β : Type u_2} (f : α → β) (xs : Array α) (i : Nat) (hi : i < (map f xs).size) : (map f xs)[i] = f xs[i]

@[simp]

theorem Array.getElem?_map {α : Type u_1} {β : Type u_2} (f : α → β) (xs : Array α) (i : Nat) : (map f xs)[i]? = Option.map f xs[i]?

@[simp]

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

@[simp]

theorem Array.map_empty {α : Type u_1} {β : Type u_2} (f : α → β) : map f #[] = #[]

@[simp]

theorem Array.map_push {α : Type u_1} {β : Type u_2} {f : α → β} {as : Array α} {x : α} : map f (as.push x) = (map f as).push (f x)

@[simp]

theorem Array.map_id_fun {α : Type u_1} : map id = id

@[simp]

theorem Array.map_id_fun' {α : Type u_1} : (map fun (a : α) => a) = id

map_id_fun' differs from map_id_fun by representing the identity function as a lambda, rather than id.

theorem Array.map_id {α : Type u_1} (xs : Array α) : map id xs = xs

theorem Array.map_id' {α : Type u_1} (xs : Array α) : map (fun (a : α) => a) xs = xs

map_id' differs from map_id by representing the identity function as a lambda, rather than id.

theorem Array.map_id'' {α : Type u_1} {f : α → α} (h : ∀ (x : α), f x = x) (xs : Array α) : map f xs = xs

Variant of map_id, with a side condition that the function is pointwise the identity.

theorem Array.map_singleton {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : map f #[a] = #[f a]

@[simp]

theorem Array.mem_map {α : Type u_1} {β : Type u_2} {b : β} {f : α → β} {xs : Array α} : b ∈ map f xs ↔ ∃ (a : α), a ∈ xs ∧ f a = b

theorem Array.exists_of_mem_map {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → α✝¹} {l : Array α✝} {b : α✝¹} (h : b ∈ map f l) : ∃ (a : α✝), a ∈ l ∧ f a = b

theorem Array.mem_map_of_mem {α : Type u_1} {β : Type u_2} {l : Array α} {a : α} (f : α → β) (h : a ∈ l) : f a ∈ map f l

theorem Array.forall_mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {P : β → Prop} : (∀ (i : β), i ∈ map f xs → P i) ↔ ∀ (j : α), j ∈ xs → P (f j)

@[simp]

theorem Array.map_eq_empty_iff {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} : map f xs = #[] ↔ xs = #[]

theorem Array.eq_empty_of_map_eq_empty {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} (h : map f xs = #[]) : xs = #[]

@[simp]

theorem Array.map_inj_left {α : Type u_1} {β : Type u_2} {xs : Array α} {f g : α → β} : map f xs = map g xs ↔ ∀ (a : α), a ∈ xs → f a = g a

theorem Array.map_inj_right {α : Type u_1} {β : Type u_2} {xs ys : Array α} {f : α → β} (w : ∀ (x y : α), f x = f y → x = y) : map f xs = map f ys ↔ xs = ys

theorem Array.map_congr_left {α✝ : Type u_1} {xs : Array α✝} {α✝¹ : Type u_2} {f g : α✝ → α✝¹} (h : ∀ (a : α✝), a ∈ xs → f a = g a) : map f xs = map g xs

theorem Array.map_inj {α✝ : Type u_1} {α✝¹ : Type u_2} {f g : α✝ → α✝¹} : map f = map g ↔ f = g

theorem Array.map_eq_push_iff {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {ys : Array β} {b : β} : map f xs = ys.push b ↔ ∃ (zs : Array α), ∃ (a : α), xs = zs.push a ∧ map f zs = ys ∧ f a = b

@[simp]

theorem Array.map_eq_singleton_iff {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {b : β} : map f xs = #[b] ↔ ∃ (a : α), xs = #[a] ∧ f a = b

theorem Array.map_eq_map_iff {α : Type u_1} {β : Type u_2} {f g : α → β} {xs : Array α} : map f xs = map g xs ↔ ∀ (a : α), a ∈ xs → f a = g a

theorem Array.map_eq_iff {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {ys : Array β} : map f xs = ys ↔ ∀ (i : Nat), ys[i]? = Option.map f xs[i]?

theorem Array.map_eq_foldl {α : Type u_1} {β : Type u_2} (f : α → β) (xs : Array α) : map f xs = foldl (fun (bs : Array β) (a : α) => bs.push (f a)) #[] xs

@[simp]

theorem Array.map_set {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {i : Nat} {h : i < xs.size} {a : α} : map f (xs.set i a h) = (map f xs).set i (f a) ⋯

@[simp]

theorem Array.map_setIfInBounds {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {i : Nat} {a : α} : map f (xs.setIfInBounds i a) = (map f xs).setIfInBounds i (f a)

@[simp]

theorem Array.map_pop {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} : map f xs.pop = (map f xs).pop

@[simp]

theorem Array.back?_map {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} : (map f xs).back? = Option.map f xs.back?

@[simp]

theorem Array.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} {as : Array α} : map g (map f as) = map (g ∘ f) as

theorem Array.mapM_eq_mapM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (xs : Array α) : mapM f xs = List.toArray <$> List.mapM f xs.toList

@[simp]

theorem Array.toList_mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (xs : Array α) : toList <$> mapM f xs = List.mapM f xs.toList

@[irreducible, deprecated "Use `mapM_eq_foldlM` instead" (since := "2025-01-08")]

theorem Array.mapM_map_eq_foldl {α : Type u_1} {β : Type u_2} {b : Array β} (as : Array α) (f : α → β) (i : Nat) : mapM.map f as i b = foldl (fun (acc : Array β) (a : α) => acc.push (f a)) b as i

theorem Array.array₂_induction {α : Type u_1} (P : Array (Array α) → Prop) (of : ∀ (xss : List (List α)), P (List.map List.toArray xss).toArray) (xss : Array (Array α)) : P xss

Use this as induction ass using array₂_induction on a hypothesis of the form ass : Array (Array α). The hypothesis ass will be replaced with a hypothesis ass : List (List α), and former appearances of ass in the goal will be replaced with (ass.map List.toArray).toArray.

theorem Array.array₃_induction {α : Type u_1} (P : Array (Array (Array α)) → Prop) (of : ∀ (xss : List (List (List α))), P (List.map List.toArray (List.map (fun (xs : List (List α)) => List.map List.toArray xs) xss)).toArray) (xss : Array (Array (Array α))) : P xss

Use this as induction ass using array₃_induction on a hypothesis of the form ass : Array (Array (Array α)). The hypothesis ass will be replaced with a hypothesis ass : List (List (List α)), and former appearances of ass in the goal will be replaced with ((ass.map (fun xs => xs.map List.toArray)).map List.toArray).toArray.

filter

theorem Array.filter_congr {α : Type u_1} {xs ys : Array α} (h : xs = ys) {f g : α → Bool} (h' : f = g) {start stop start' stop' : Nat} (h₁ : start = start') (h₂ : stop = stop') : filter f xs start stop = filter g ys start' stop'

@[simp]

theorem Array.toList_filter' {α : Type u_1} {stop : Nat} (p : α → Bool) (xs : Array α) (h : stop = xs.size) : (filter p xs 0 stop).toList = List.filter p xs.toList

theorem Array.toList_filter {α : Type u_1} (p : α → Bool) (xs : Array α) : (filter p xs).toList = List.filter p xs.toList

@[simp]

theorem List.filter_toArray' {α : Type u_1} {stop : Nat} (p : α → Bool) (l : List α) (h : stop = l.length) : Array.filter p l.toArray 0 stop = (filter p l).toArray

theorem List.filter_toArray {α : Type u_1} (p : α → Bool) (l : List α) : Array.filter p l.toArray = (filter p l).toArray

@[simp]

theorem Array.filter_push_of_pos {α : Type u_1} {stop : Nat} {p : α → Bool} {a : α} {xs : Array α} (h : p a = true) (w : stop = xs.size + 1) : filter p (xs.push a) 0 stop = (filter p xs).push a

@[simp]

theorem Array.filter_push_of_neg {α : Type u_1} {stop : Nat} {p : α → Bool} {a : α} {xs : Array α} (h : ¬p a = true) (w : stop = xs.size + 1) : filter p (xs.push a) 0 stop = filter p xs

theorem Array.filter_push {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α} : filter p (xs.push a) = if p a = true then (filter p xs).push a else filter p xs

theorem Array.size_filter_le {α : Type u_1} (p : α → Bool) (xs : Array α) : (filter p xs).size ≤ xs.size

@[simp]

theorem Array.filter_eq_self {α : Type u_1} {p : α → Bool} {xs : Array α} : filter p xs = xs ↔ ∀ (a : α), a ∈ xs → p a = true

@[simp]

theorem Array.filter_size_eq_size {α : Type u_1} {p : α → Bool} {xs : Array α} : (filter p xs).size = xs.size ↔ ∀ (a : α), a ∈ xs → p a = true

@[simp]

theorem Array.mem_filter {α : Type u_1} {p : α → Bool} {xs : Array α} {a : α} : a ∈ filter p xs ↔ a ∈ xs ∧ p a = true

@[simp]

theorem Array.filter_eq_empty_iff {α : Type u_1} {p : α → Bool} {xs : Array α} : filter p xs = #[] ↔ ∀ (a : α), a ∈ xs → ¬p a = true

theorem Array.forall_mem_filter {α : Type u_1} {p : α → Bool} {xs : Array α} {P : α → Prop} : (∀ (i : α), i ∈ filter p xs → P i) ↔ ∀ (j : α), j ∈ xs → p j = true → P j

@[simp]

theorem Array.filter_filter {α : Type u_1} {p : α → Bool} (q : α → Bool) (xs : Array α) : filter p (filter q xs) = filter (fun (a : α) => p a && q a) xs

theorem Array.foldl_filter {α : Type u_1} {β : Type u_2} (p : α → Bool) (f : β → α → β) (xs : Array α) (init : β) : foldl f init (filter p xs) = foldl (fun (x : β) (y : α) => if p y = true then f x y else x) init xs

theorem Array.foldr_filter {α : Type u_1} {β : Type u_2} (p : α → Bool) (f : α → β → β) (xs : Array α) (init : β) : foldr f init (filter p xs) = foldr (fun (x : α) (y : β) => if p x = true then f x y else y) init xs

theorem Array.filter_map {β : Type u_1} {α : Type u_2} {p : α → Bool} (f : β → α) (xs : Array β) : filter p (map f xs) = map f (filter (p ∘ f) xs)

theorem Array.map_filter_eq_foldl {α : Type u_1} {β : Type u_2} (f : α → β) (p : α → Bool) (xs : Array α) : map f (filter p xs) = foldl (fun (acc : Array β) (x : α) => bif p x then acc.push (f x) else acc) #[] xs

@[simp]

theorem Array.filter_append {α : Type u_1} {stop : Nat} {p : α → Bool} (xs ys : Array α) (w : stop = xs.size + ys.size) : filter p (xs ++ ys) 0 stop = filter p xs ++ filter p ys

theorem Array.filter_eq_append_iff {α : Type u_1} {xs ys zs : Array α} {p : α → Bool} : filter p xs = ys ++ zs ↔ ∃ (as : Array α), ∃ (bs : Array α), xs = as ++ bs ∧ filter p as = ys ∧ filter p bs = zs

theorem Array.filter_eq_push_iff {α : Type u_1} {p : α → Bool} {xs ys : Array α} {a : α} : filter p xs = ys.push a ↔ ∃ (as : Array α), ∃ (bs : Array α), xs = as.push a ++ bs ∧ filter p as = ys ∧ p a = true ∧ ∀ (x : α), x ∈ bs → ¬p x = true

theorem Array.mem_of_mem_filter {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α} (h : a ∈ filter p xs) : a ∈ xs

@[simp]

theorem Array.size_filter_pos_iff {α : Type u_1} {xs : Array α} {p : α → Bool} : 0 < (filter p xs).size ↔ ∃ (x : α), x ∈ xs ∧ p x = true

@[simp]

theorem Array.size_filter_lt_size_iff_exists {α : Type u_1} {xs : Array α} {p : α → Bool} : (filter p xs).size < xs.size ↔ ∃ (x : α), x ∈ xs ∧ ¬p x = true

filterMap

theorem Array.filterMap_congr {α : Type u_1} {β : Type u_2} {as bs : Array α} (h : as = bs) {f g : α → Option β} (h' : f = g) {start stop start' stop' : Nat} (h₁ : start = start') (h₂ : stop = stop') : filterMap f as start stop = filterMap g bs start' stop'

@[simp]

theorem Array.toList_filterMap' {α : Type u_1} {β : Type u_2} {stop : Nat} (f : α → Option β) (xs : Array α) (w : stop = xs.size) : (filterMap f xs 0 stop).toList = List.filterMap f xs.toList

theorem Array.toList_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (xs : Array α) : (filterMap f xs).toList = List.filterMap f xs.toList

@[simp]

theorem List.filterMap_toArray' {α : Type u_1} {β : Type u_2} {stop : Nat} (f : α → Option β) (l : List α) (h : stop = l.length) : Array.filterMap f l.toArray 0 stop = (filterMap f l).toArray

theorem List.filterMap_toArray {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α) : Array.filterMap f l.toArray = (filterMap f l).toArray

@[simp]

theorem Array.filterMap_push_none {α : Type u_1} {β : Type u_2} {stop : Nat} {f : α → Option β} {a : α} {xs : Array α} (h : f a = none) (w : stop = xs.size + 1) : filterMap f (xs.push a) 0 stop = filterMap f xs

@[simp]

theorem Array.filterMap_push_some {α : Type u_1} {β : Type u_2} {stop : Nat} {f : α → Option β} {a : α} {xs : Array α} {b : β} (h : f a = some b) (w : stop = xs.size + 1) : filterMap f (xs.push a) 0 stop = (filterMap f xs).push b

@[simp]

theorem Array.filterMap_eq_map {α : Type u_1} {β : Type u_2} {stop : Nat} {as : Array α} (f : α → β) (w : stop = as.size) : filterMap (some ∘ f) as 0 stop = map f as

@[simp]

theorem Array.filterMap_eq_map' {α : Type u_1} {β : Type u_2} {stop : Nat} {as : Array α} (f : α → β) (w : stop = as.size) : filterMap (fun (x : α) => some (f x)) as 0 stop = map f as

Variant of filterMap_eq_map with some ∘ f expanded out to a lambda.

theorem Array.filterMap_some_fun {α : Type u_1} : (fun (as : Array α) => filterMap some as) = id

@[simp]

theorem Array.filterMap_some {α : Type u_1} (xs : Array α) : filterMap some xs = xs

theorem Array.map_filterMap_some_eq_filterMap_isSome {α : Type u_1} {β : Type u_2} (f : α → Option β) (xs : Array α) : map some (filterMap f xs) = filter (fun (b : Option β) => b.isSome) (map f xs)

theorem Array.size_filterMap_le {α : Type u_1} {β : Type u_2} (f : α → Option β) (xs : Array α) : (filterMap f xs).size ≤ xs.size

@[simp]

theorem Array.filterMap_size_eq_size {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} {xs : Array α} : (filterMap f xs).size = xs.size ↔ ∀ (a : α), a ∈ xs → (f a).isSome = true

@[simp]

theorem Array.filterMap_eq_filter {α : Type u_1} {stop : Nat} {as : Array α} (p : α → Bool) (w : stop = as.size) : filterMap (Option.guard fun (x : α) => p x = true) as 0 stop = filter p as

theorem Array.filterMap_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β) (g : β → Option γ) (xs : Array α) : filterMap g (filterMap f xs) = filterMap (fun (x : α) => (f x).bind g) xs

theorem Array.map_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β) (g : β → γ) (xs : Array α) : map g (filterMap f xs) = filterMap (fun (x : α) => Option.map g (f x)) xs

@[simp]

theorem Array.filterMap_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → Option γ) (xs : Array α) : filterMap g (map f xs) = filterMap (g ∘ f) xs

theorem Array.filter_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (p : β → Bool) (xs : Array α) : filter p (filterMap f xs) = filterMap (fun (x : α) => Option.filter p (f x)) xs

theorem Array.filterMap_filter {α : Type u_1} {β : Type u_2} (p : α → Bool) (f : α → Option β) (xs : Array α) : filterMap f (filter p xs) = filterMap (fun (x : α) => if p x = true then f x else none) xs

@[simp]

theorem Array.mem_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} {b : β} : b ∈ filterMap f xs ↔ ∃ (a : α), a ∈ xs ∧ f a = some b

theorem Array.forall_mem_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} {P : β → Prop} : (∀ (i : β), i ∈ filterMap f xs → P i) ↔ ∀ (j : α), j ∈ xs → ∀ (b : β), f j = some b → P b

@[simp]

theorem Array.filterMap_append {stop : Nat} {α : Type u_1} {β : Type u_2} {xs ys : Array α} (f : α → Option β) (w : stop = xs.size + ys.size) : filterMap f (xs ++ ys) 0 stop = filterMap f xs ++ filterMap f ys

theorem Array.map_filterMap_of_inv {α : Type u_1} {β : Type u_2} (f : α → Option β) (g : β → α) (H : ∀ (x : α), Option.map g (f x) = some x) (xs : Array α) : map g (filterMap f xs) = xs

theorem Array.forall_none_of_filterMap_eq_empty {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {xs : Array α✝} (h : filterMap f xs = #[]) (x : α✝) : x ∈ xs → f x = none

@[simp]

theorem Array.filterMap_eq_nil_iff {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} {xs : Array α} : filterMap f xs = #[] ↔ ∀ (a : α), a ∈ xs → f a = none

theorem Array.filterMap_eq_push_iff {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} {ys : Array β} {b : β} : filterMap f xs = ys.push b ↔ ∃ (as : Array α), ∃ (a : α), ∃ (bs : Array α), xs = as.push a ++ bs ∧ filterMap f as = ys ∧ f a = some b ∧ ∀ (x : α), x ∈ bs → f x = none

@[simp]

theorem Array.size_filterMap_pos_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Option β} : 0 < (filterMap f xs).size ↔ ∃ (x : α), ∃ (x_1 : x ∈ xs), ∃ (b : β), f x = some b

@[simp]

theorem Array.size_filterMap_lt_size_iff_exists {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Option β} : (filterMap f xs).size < xs.size ↔ ∃ (x : α), ∃ (x_1 : x ∈ xs), f x = none

singleton

@[simp]

theorem Array.singleton_def {α : Type u_1} (v : α) : Array.singleton v = #[v]

append

@[simp]

theorem Array.size_append {α : Type u_1} (xs ys : Array α) : (xs ++ ys).size = xs.size + ys.size

@[simp]

theorem Array.push_append {α : Type u_1} {a : α} {xs ys : Array α} : (xs ++ ys).push a = xs ++ ys.push a

theorem Array.append_push {α : Type u_1} {xs ys : Array α} {a : α} : xs ++ ys.push a = (xs ++ ys).push a

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

@[simp]

theorem Array.toArray_eq_append_iff {α : Type u_1} {xs : List α} {as bs : Array α} : xs.toArray = as ++ bs ↔ xs = as.toList ++ bs.toList

@[simp]

theorem Array.append_eq_toArray_iff {α : Type u_1} {xs ys : Array α} {as : List α} : xs ++ ys = as.toArray ↔ xs.toList ++ ys.toList = as

theorem Array.singleton_eq_toArray_singleton {α : Type u_1} (a : α) : #[a] = #[a]

@[simp]

theorem Array.empty_append_fun {α : Type u_1} : (fun (x : Array α) => #[] ++ x) = id

@[simp]

theorem Array.mem_append {α : Type u_1} {a : α} {xs ys : Array α} : a ∈ xs ++ ys ↔ a ∈ xs ∨ a ∈ ys

theorem Array.mem_append_left {α : Type u_1} {a : α} {xs : Array α} (ys : Array α) (h : a ∈ xs) : a ∈ xs ++ ys

theorem Array.mem_append_right {α : Type u_1} {a : α} (xs : Array α) {ys : Array α} (h : a ∈ ys) : a ∈ xs ++ ys

theorem Array.not_mem_append {α : Type u_1} {a : α} {xs ys : Array α} (h₁ : ¬a ∈ xs) (h₂ : ¬a ∈ ys) : ¬a ∈ xs ++ ys

theorem Array.append_of_mem {α : Type u_1} {a : α} {xs : Array α} (h : a ∈ xs) : ∃ (as : Array α), ∃ (bs : Array α), xs = as.push a ++ bs

See also eq_push_append_of_mem, which proves a stronger version in which the initial array must not contain the element.

theorem Array.mem_iff_append {α : Type u_1} {a : α} {xs : Array α} : a ∈ xs ↔ ∃ (as : Array α), ∃ (bs : Array α), xs = as.push a ++ bs

theorem Array.forall_mem_append {α : Type u_1} {p : α → Prop} {xs ys : Array α} : (∀ (x : α), x ∈ xs ++ ys → p x) ↔ (∀ (x : α), x ∈ xs → p x) ∧ ∀ (x : α), x ∈ ys → p x

theorem Array.getElem_append {α : Type u_1} {i : Nat} {xs ys : Array α} (h : i < (xs ++ ys).size) : (xs ++ ys)[i] = if h' : i < xs.size then xs[i] else ys[i - xs.size]

@[simp]

theorem Array.getElem_append_left {α : Type u_1} {i : Nat} {xs ys : Array α} {h : i < (xs ++ ys).size} (hlt : i < xs.size) : (xs ++ ys)[i] = xs[i]

@[simp]

theorem Array.getElem_append_right {α : Type u_1} {i : Nat} {xs ys : Array α} {h : i < (xs ++ ys).size} (hle : xs.size ≤ i) : (xs ++ ys)[i] = ys[i - xs.size]

theorem Array.getElem?_append_left {α : Type u_1} {xs ys : Array α} {i : Nat} (hn : i < xs.size) : (xs ++ ys)[i]? = xs[i]?

theorem Array.getElem?_append_right {α : Type u_1} {xs ys : Array α} {i : Nat} (h : xs.size ≤ i) : (xs ++ ys)[i]? = ys[i - xs.size]?

theorem Array.getElem?_append {α : Type u_1} {xs ys : Array α} {i : Nat} : (xs ++ ys)[i]? = if i < xs.size then xs[i]? else ys[i - xs.size]?

theorem Array.getElem_append_left' {α : Type u_1} (ys : Array α) {xs : Array α} {i : Nat} (hi : i < xs.size) : xs[i] = (xs ++ ys)[i]

Variant of getElem_append_left useful for rewriting from the small array to the big array.

theorem Array.getElem_append_right' {α : Type u_1} (xs : Array α) {ys : Array α} {i : Nat} (hi : i < ys.size) : ys[i] = (xs ++ ys)[i + xs.size]

Variant of getElem_append_right useful for rewriting from the small array to the big array.

theorem Array.getElem_of_append {α : Type u_1} {a : α} {i : Nat} {xs ys zs : Array α} (eq : xs = ys.push a ++ zs) (h : ys.size = i) : xs[i] = a

@[simp]

theorem Array.append_singleton {α : Type u_1} {a : α} {as : Array α} : as ++ #[a] = as.push a

@[simp]

theorem Array.append_singleton_assoc {α : Type u_1} {a : α} {xs ys : Array α} : xs ++ (#[a] ++ ys) = xs.push a ++ ys

theorem Array.push_eq_append {α : Type u_1} {a : α} {as : Array α} : as.push a = as ++ #[a]

theorem Array.append_inj {α : Type u_1} {xs₁ xs₂ ys₁ ys₂ : Array α} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) (hl : xs₁.size = xs₂.size) : xs₁ = xs₂ ∧ ys₁ = ys₂

theorem Array.append_inj_right {α : Type u_1} {xs₁ xs₂ ys₁ ys₂ : Array α} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) (hl : xs₁.size = xs₂.size) : ys₁ = ys₂

theorem Array.append_inj_left {α : Type u_1} {xs₁ xs₂ ys₁ ys₂ : Array α} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) (hl : xs₁.size = xs₂.size) : xs₁ = xs₂

theorem Array.append_inj' {α : Type u_1} {xs₁ xs₂ ys₁ ys₂ : Array α} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) (hl : ys₁.size = ys₂.size) : xs₁ = xs₂ ∧ ys₁ = ys₂

Variant of append_inj instead requiring equality of the sizes of the second arrays.

theorem Array.append_inj_right' {α : Type u_1} {xs₁ xs₂ ys₁ ys₂ : Array α} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) (hl : ys₁.size = ys₂.size) : ys₁ = ys₂

Variant of append_inj_right instead requiring equality of the sizes of the second arrays.

theorem Array.append_inj_left' {α : Type u_1} {xs₁ xs₂ ys₁ ys₂ : Array α} (h : xs₁ ++ ys₁ = xs₂ ++ ys₂) (hl : ys₁.size = ys₂.size) : xs₁ = xs₂

Variant of append_inj_left instead requiring equality of the sizes of the second arrays.

theorem Array.append_right_inj {α : Type u_1} {ys₁ ys₂ : Array α} (xs : Array α) : xs ++ ys₁ = xs ++ ys₂ ↔ ys₁ = ys₂

theorem Array.append_left_inj {α : Type u_1} {xs₁ xs₂ : Array α} (ys : Array α) : xs₁ ++ ys = xs₂ ++ ys ↔ xs₁ = xs₂

@[simp]

theorem Array.append_left_eq_self {α : Type u_1} {xs ys : Array α} : xs ++ ys = ys ↔ xs = #[]

@[simp]

theorem Array.self_eq_append_left {α : Type u_1} {xs ys : Array α} : ys = xs ++ ys ↔ xs = #[]

@[simp]

theorem Array.append_right_eq_self {α : Type u_1} {xs ys : Array α} : xs ++ ys = xs ↔ ys = #[]

@[simp]

theorem Array.self_eq_append_right {α : Type u_1} {xs ys : Array α} : xs = xs ++ ys ↔ ys = #[]

@[simp]

theorem Array.append_eq_empty_iff {α : Type u_1} {xs ys : Array α} : xs ++ ys = #[] ↔ xs = #[] ∧ ys = #[]

@[simp]

theorem Array.empty_eq_append_iff {α : Type u_1} {xs ys : Array α} : #[] = xs ++ ys ↔ xs = #[] ∧ ys = #[]

theorem Array.append_ne_empty_of_left_ne_empty {α : Type u_1} {xs ys : Array α} (h : xs ≠ #[]) : xs ++ ys ≠ #[]

theorem Array.append_ne_empty_of_right_ne_empty {α : Type u_1} {xs ys : Array α} (h : ys ≠ #[]) : xs ++ ys ≠ #[]

theorem Array.append_eq_push_iff {α : Type u_1} {xs ys zs : Array α} {x : α} : xs ++ ys = zs.push x ↔ ys = #[] ∧ xs = zs.push x ∨ ∃ (ys' : Array α), ys = ys'.push x ∧ zs = xs ++ ys'

theorem Array.push_eq_append_iff {α : Type u_1} {xs ys zs : Array α} {x : α} : zs.push x = xs ++ ys ↔ ys = #[] ∧ xs = zs.push x ∨ ∃ (ys' : Array α), ys = ys'.push x ∧ zs = xs ++ ys'

theorem Array.append_eq_singleton_iff {α : Type u_1} {xs ys : Array α} {x : α} : xs ++ ys = #[x] ↔ xs = #[] ∧ ys = #[x] ∨ xs = #[x] ∧ ys = #[]

theorem Array.singleton_eq_append_iff {α : Type u_1} {xs ys : Array α} {x : α} : #[x] = xs ++ ys ↔ xs = #[] ∧ ys = #[x] ∨ xs = #[x] ∧ ys = #[]

theorem Array.append_eq_append_iff {α : Type u_1} {ws xs ys zs : Array α} : ws ++ xs = ys ++ zs ↔ (∃ (as : Array α), ys = ws ++ as ∧ xs = as ++ zs) ∨ ∃ (cs : Array α), ws = ys ++ cs ∧ zs = cs ++ xs

theorem Array.set_append {α : Type u_1} {xs ys : Array α} {i : Nat} {x : α} (h : i < (xs ++ ys).size) : (xs ++ ys).set i x h = if h' : i < xs.size then xs.set i x h' ++ ys else xs ++ ys.set (i - xs.size) x ⋯

@[simp]

theorem Array.set_append_left {α : Type u_1} {xs ys : Array α} {i : Nat} {x : α} (h : i < xs.size) : (xs ++ ys).set i x ⋯ = xs.set i x h ++ ys

@[simp]

theorem Array.set_append_right {α : Type u_1} {xs ys : Array α} {i : Nat} {x : α} (h' : i < (xs ++ ys).size) (h : xs.size ≤ i) : (xs ++ ys).set i x h' = xs ++ ys.set (i - xs.size) x ⋯

theorem Array.setIfInBounds_append {α : Type u_1} {xs ys : Array α} {i : Nat} {x : α} : (xs ++ ys).setIfInBounds i x = if i < xs.size then xs.setIfInBounds i x ++ ys else xs ++ ys.setIfInBounds (i - xs.size) x

@[simp]

theorem Array.setIfInBounds_append_left {α : Type u_1} {xs ys : Array α} {i : Nat} {x : α} (h : i < xs.size) : (xs ++ ys).setIfInBounds i x = xs.setIfInBounds i x ++ ys

@[simp]

theorem Array.setIfInBounds_append_right {α : Type u_1} {xs ys : Array α} {i : Nat} {x : α} (h : xs.size ≤ i) : (xs ++ ys).setIfInBounds i x = xs ++ ys.setIfInBounds (i - xs.size) x

theorem Array.filterMap_eq_append_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {ys zs : Array β} {f : α → Option β} : filterMap f xs = ys ++ zs ↔ ∃ (as : Array α), ∃ (bs : Array α), xs = as ++ bs ∧ filterMap f as = ys ∧ filterMap f bs = zs

theorem Array.append_eq_filterMap_iff {α : Type u_1} {β : Type u_2} {xs ys : Array β} {zs : Array α} {f : α → Option β} : xs ++ ys = filterMap f zs ↔ ∃ (as : Array α), ∃ (bs : Array α), zs = as ++ bs ∧ filterMap f as = xs ∧ filterMap f bs = ys

@[simp]

theorem Array.map_append {α : Type u_1} {β : Type u_2} (f : α → β) (xs ys : Array α) : map f (xs ++ ys) = map f xs ++ map f ys

theorem Array.map_eq_append_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {ys zs : Array β} {f : α → β} : map f xs = ys ++ zs ↔ ∃ (as : Array α), ∃ (bs : Array α), xs = as ++ bs ∧ map f as = ys ∧ map f bs = zs

theorem Array.append_eq_map_iff {α : Type u_1} {β : Type u_2} {xs ys : Array β} {zs : Array α} {f : α → β} : xs ++ ys = map f zs ↔ ∃ (as : Array α), ∃ (bs : Array α), zs = as ++ bs ∧ map f as = xs ∧ map f bs = ys

flatten

@[simp]

theorem Array.flatten_empty {α : Type u_1} : #[].flatten = #[]

@[simp]

theorem Array.toList_flatten {α : Type u_1} {xss : Array (Array α)} : xss.flatten.toList = (List.map toList xss.toList).flatten

@[simp]

theorem Array.flatten_map_toArray {α : Type u_1} (L : List (List α)) : (map List.toArray L.toArray).flatten = L.flatten.toArray

@[simp]

theorem Array.flatten_toArray_map {α : Type u_1} (L : List (List α)) : (List.map List.toArray L).toArray.flatten = L.flatten.toArray

@[simp]

theorem Array.flatten_toArray {α : Type u_1} (l : List (Array α)) : l.toArray.flatten = (List.map toList l).flatten.toArray

@[simp]

theorem Array.size_flatten {α : Type u_1} (xss : Array (Array α)) : xss.flatten.size = (map size xss).sum

@[simp]

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

theorem Array.mem_flatten {α : Type u_1} {a : α} {xss : Array (Array α)} : a ∈ xss.flatten ↔ ∃ (xs : Array α), xs ∈ xss ∧ a ∈ xs

@[simp]

theorem Array.flatten_eq_empty_iff {α : Type u_1} {xss : Array (Array α)} : xss.flatten = #[] ↔ ∀ (xs : Array α), xs ∈ xss → xs = #[]

@[simp]

theorem Array.empty_eq_flatten_iff {α : Type u_1} {xss : Array (Array α)} : #[] = xss.flatten ↔ ∀ (xs : Array α), xs ∈ xss → xs = #[]

theorem Array.flatten_ne_empty_iff {α : Type u_1} {xss : Array (Array α)} : xss.flatten ≠ #[] ↔ ∃ (xs : Array α), xs ∈ xss ∧ xs ≠ #[]

theorem Array.exists_of_mem_flatten {α✝ : Type u_1} {xss : Array (Array α✝)} {x : α✝} : x ∈ xss.flatten → ∃ (xs : Array α✝), xs ∈ xss ∧ x ∈ xs

theorem Array.mem_flatten_of_mem {α✝ : Type u_1} {xss : Array (Array α✝)} {xs : Array α✝} {a : α✝} (ml : xs ∈ xss) (ma : a ∈ xs) : a ∈ xss.flatten

theorem Array.forall_mem_flatten {α : Type u_1} {p : α → Prop} {xss : Array (Array α)} : (∀ (x : α), x ∈ xss.flatten → p x) ↔ ∀ (xs : Array α), xs ∈ xss → ∀ (x : α), x ∈ xs → p x

theorem Array.flatten_eq_flatMap {α : Type u_1} {xss : Array (Array α)} : xss.flatten = flatMap id xss

@[simp]

theorem Array.map_flatten {α : Type u_1} {β : Type u_2} (f : α → β) (xss : Array (Array α)) : map f xss.flatten = (map (map f) xss).flatten

@[simp]

theorem Array.filterMap_flatten {α : Type u_1} {β : Type u_2} {stop : Nat} (f : α → Option β) (xss : Array (Array α)) (w : stop = xss.flatten.size) : filterMap f xss.flatten 0 stop = (map (fun (as : Array α) => filterMap f as) xss).flatten

@[simp]

theorem Array.filter_flatten {α : Type u_1} {stop : Nat} (p : α → Bool) (xss : Array (Array α)) (w : stop = xss.flatten.size) : filter p xss.flatten 0 stop = (map (fun (as : Array α) => filter p as) xss).flatten

theorem Array.flatten_filter_not_isEmpty {α : Type u_1} {xss : Array (Array α)} : (filter (fun (xs : Array α) => !xs.isEmpty) xss).flatten = xss.flatten

theorem Array.flatten_filter_ne_empty {α : Type u_1} [DecidablePred fun (xs : Array α) => xs ≠ #[]] {xss : Array (Array α)} : (filter (fun (xs : Array α) => decide (xs ≠ #[])) xss).flatten = xss.flatten

@[simp]

theorem Array.flatten_append {α : Type u_1} (xss₁ xss₂ : Array (Array α)) : (xss₁ ++ xss₂).flatten = xss₁.flatten ++ xss₂.flatten

theorem Array.flatten_push {α : Type u_1} (xss : Array (Array α)) (xs : Array α) : (xss.push xs).flatten = xss.flatten ++ xs

theorem Array.flatten_flatten {α : Type u_1} {xss : Array (Array (Array α))} : xss.flatten.flatten = (map flatten xss).flatten

theorem Array.flatten_eq_push_iff {α : Type u_1} {xss : Array (Array α)} {ys : Array α} {y : α} : xss.flatten = ys.push y ↔ ∃ (as : Array (Array α)), ∃ (bs : Array α), ∃ (cs : Array (Array α)), xss = as.push (bs.push y) ++ cs ∧ (∀ (xs : Array α), xs ∈ cs → xs = #[]) ∧ ys = as.flatten ++ bs

theorem Array.push_eq_flatten_iff {α : Type u_1} {xss : Array (Array α)} {ys : Array α} {y : α} : ys.push y = xss.flatten ↔ ∃ (as : Array (Array α)), ∃ (bs : Array α), ∃ (cs : Array (Array α)), xss = as.push (bs.push y) ++ cs ∧ (∀ (xs : Array α), xs ∈ cs → xs = #[]) ∧ ys = as.flatten ++ bs

theorem Array.eq_iff_flatten_eq {α : Type u_1} {xss₁ xss₂ : Array (Array α)} : xss₁ = xss₂ ↔ xss₁.flatten = xss₂.flatten ∧ map size xss₁ = map size xss₂

Two arrays of subarrays are equal iff their flattens coincide, as well as the sizes of the subarrays.

@[simp]

theorem Array.flatten_toArray_map_toArray {α : Type u_1} (xss : List (List α)) : (List.map List.toArray xss).toArray.flatten = xss.flatten.toArray

flatMap

theorem Array.flatMap_def {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → Array β) : flatMap f xs = (map f xs).flatten

@[simp]

theorem Array.flatMap_empty {α : Type u_1} {β : Type u_2} (f : α → Array β) : flatMap f #[] = #[]

theorem Array.flatMap_toList {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → List β) : List.flatMap f xs.toList = (flatMap (fun (a : α) => (f a).toArray) xs).toList

@[simp]

theorem Array.toList_flatMap {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → Array β) : (flatMap f xs).toList = List.flatMap (fun (a : α) => (f a).toList) xs.toList

theorem Array.flatMap_toArray_cons {α : Type u_1} {β : Type u_2} (f : α → Array β) (a : α) (as : List α) : flatMap f (a :: as).toArray = f a ++ flatMap f as.toArray

@[simp]

theorem Array.flatMap_toArray {α : Type u_1} {β : Type u_2} (f : α → Array β) (as : List α) : flatMap f as.toArray = (List.flatMap (fun (a : α) => (f a).toList) as).toArray

@[simp]

theorem Array.flatMap_id {α : Type u_1} (xss : Array (Array α)) : flatMap id xss = xss.flatten

@[simp]

theorem Array.flatMap_id' {α : Type u_1} (xss : Array (Array α)) : flatMap (fun (xs : Array α) => xs) xss = xss.flatten

@[simp]

theorem Array.size_flatMap {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → Array β) : (flatMap f xs).size = (map (fun (a : α) => (f a).size) xs).sum

@[simp]

theorem Array.mem_flatMap {α : Type u_1} {β : Type u_2} {f : α → Array β} {b : β} {xs : Array α} : b ∈ flatMap f xs ↔ ∃ (a : α), a ∈ xs ∧ b ∈ f a

theorem Array.exists_of_mem_flatMap {β : Type u_1} {α : Type u_2} {b : β} {xs : Array α} {f : α → Array β} : b ∈ flatMap f xs → ∃ (a : α), a ∈ xs ∧ b ∈ f a

theorem Array.mem_flatMap_of_mem {β : Type u_1} {α : Type u_2} {b : β} {xs : Array α} {f : α → Array β} {a : α} (al : a ∈ xs) (h : b ∈ f a) : b ∈ flatMap f xs

@[simp]

theorem Array.flatMap_eq_empty_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} : flatMap f xs = #[] ↔ ∀ (x : α), x ∈ xs → f x = #[]

theorem Array.forall_mem_flatMap {β : Type u_1} {α : Type u_2} {p : β → Prop} {xs : Array α} {f : α → Array β} : (∀ (x : β), x ∈ flatMap f xs → p x) ↔ ∀ (a : α), a ∈ xs → ∀ (b : β), b ∈ f a → p b

theorem Array.flatMap_singleton {α : Type u_1} {β : Type u_2} (f : α → Array β) (x : α) : flatMap f #[x] = f x

@[simp]

theorem Array.flatMap_singleton' {α : Type u_1} (xs : Array α) : flatMap (fun (x : α) => #[x]) xs = xs

@[simp]

theorem Array.flatMap_append {α : Type u_1} {β : Type u_2} (xs ys : Array α) (f : α → Array β) : flatMap f (xs ++ ys) = flatMap f xs ++ flatMap f ys

theorem Array.flatMap_assoc {γ : Type u_1} {α : Type u_2} {β : Type u_3} (xs : Array α) (f : α → Array β) (g : β → Array γ) : flatMap g (flatMap f xs) = flatMap (fun (x : α) => flatMap g (f x)) xs

theorem Array.map_flatMap {β : Type u_1} {γ : Type u_2} {α : Type u_3} (f : β → γ) (g : α → Array β) (xs : Array α) : map f (flatMap g xs) = flatMap (fun (a : α) => map f (g a)) xs

theorem Array.flatMap_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → Array γ) (xs : Array α) : flatMap g (map f xs) = flatMap (fun (a : α) => g (f a)) xs

theorem Array.map_eq_flatMap {α : Type u_1} {β : Type u_2} (f : α → β) (xs : Array α) : map f xs = flatMap (fun (x : α) => #[f x]) xs

theorem Array.filterMap_flatMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (xs : Array α) (g : α → Array β) (f : β → Option γ) : filterMap f (flatMap g xs) = flatMap (fun (a : α) => filterMap f (g a)) xs

theorem Array.filter_flatMap {α : Type u_1} {β : Type u_2} (xs : Array α) (g : α → Array β) (f : β → Bool) : filter f (flatMap g xs) = flatMap (fun (a : α) => filter f (g a)) xs

theorem Array.flatMap_eq_foldl {α : Type u_1} {β : Type u_2} (f : α → Array β) (xs : Array α) : flatMap f xs = foldl (fun (acc : Array β) (a : α) => acc ++ f a) #[] xs

mkArray

@[simp]

theorem Array.mkArray_one {α✝ : Type u_1} {a : α✝} : mkArray 1 a = #[a]

theorem Array.mkArray_succ' {n : Nat} {α✝ : Type u_1} {a : α✝} : mkArray (n + 1) a = #[a] ++ mkArray n a

Variant of mkArray_succ that prepends a at the beginning of the array.

@[simp]

theorem Array.mem_mkArray {α : Type u_1} {a b : α} {n : Nat} : b ∈ mkArray n a ↔ n ≠ 0 ∧ b = a

theorem Array.eq_of_mem_mkArray {α : Type u_1} {a b : α} {n : Nat} (h : b ∈ mkArray n a) : b = a

theorem Array.forall_mem_mkArray {α : Type u_1} {p : α → Prop} {a : α} {n : Nat} : (∀ (b : α), b ∈ mkArray n a → p b) ↔ n = 0 ∨ p a

@[simp]

theorem Array.mkArray_succ_ne_empty {α : Type u_1} (n : Nat) (a : α) : mkArray (n + 1) a ≠ #[]

@[simp]

theorem Array.mkArray_eq_empty_iff {α : Type u_1} {n : Nat} (a : α) : mkArray n a = #[] ↔ n = 0

@[simp]

theorem Array.getElem?_mkArray_of_lt {α✝ : Type u_1} {a : α✝} {n i : Nat} (h : i < n) : (mkArray n a)[i]? = some a

@[simp]

theorem Array.mkArray_inj {n : Nat} {α✝ : Type u_1} {a : α✝} {m : Nat} {b : α✝} : mkArray n a = mkArray m b ↔ n = m ∧ (n = 0 ∨ a = b)

theorem Array.eq_mkArray_of_mem {α : Type u_1} {a : α} {xs : Array α} (h : ∀ (b : α), b ∈ xs → b = a) : xs = mkArray xs.size a

theorem Array.eq_mkArray_iff {α : Type u_1} {a : α} {n : Nat} {xs : Array α} : xs = mkArray n a ↔ xs.size = n ∧ ∀ (b : α), b ∈ xs → b = a

theorem Array.map_eq_mkArray_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β} {b : β} : map f xs = mkArray xs.size b ↔ ∀ (x : α), x ∈ xs → f x = b

@[simp]

theorem Array.map_const {α : Type u_1} {β : Type u_2} (xs : Array α) (b : β) : map (Function.const α b) xs = mkArray xs.size b

@[simp]

theorem Array.map_const_fun {β : Type u_1} {α : Type u_2} (x : β) : map (Function.const α x) = fun (x_1 : Array α) => mkArray x_1.size x

theorem Array.map_const' {α : Type u_1} {β : Type u_2} (xs : Array α) (b : β) : map (fun (x : α) => b) xs = mkArray xs.size b

Variant of map_const using a lambda rather than Function.const.

@[simp]

theorem Array.set_mkArray_self {n : Nat} {α✝ : Type u_1} {a : α✝} {i : Nat} {h : i < (mkArray n a).size} : (mkArray n a).set i a h = mkArray n a

@[simp]

theorem Array.setIfInBounds_mkArray_self {n : Nat} {α✝ : Type u_1} {a : α✝} {i : Nat} : (mkArray n a).setIfInBounds i a = mkArray n a

@[simp]

theorem Array.mkArray_append_mkArray {n : Nat} {α✝ : Type u_1} {a : α✝} {m : Nat} : mkArray n a ++ mkArray m a = mkArray (n + m) a

theorem Array.append_eq_mkArray_iff {α : Type u_1} {n : Nat} {xs ys : Array α} {a : α} : xs ++ ys = mkArray n a ↔ xs.size + ys.size = n ∧ xs = mkArray xs.size a ∧ ys = mkArray ys.size a

theorem Array.mkArray_eq_append_iff {α : Type u_1} {n : Nat} {xs ys : Array α} {a : α} : mkArray n a = xs ++ ys ↔ xs.size + ys.size = n ∧ xs = mkArray xs.size a ∧ ys = mkArray ys.size a

@[simp]

theorem Array.map_mkArray {n : Nat} {α✝ : Type u_1} {a : α✝} {α✝¹ : Type u_2} {f : α✝ → α✝¹} : map f (mkArray n a) = mkArray n (f a)

theorem Array.filter_mkArray {stop n : Nat} {α✝ : Type u_1} {a : α✝} {p : α✝ → Bool} (w : stop = n) : filter p (mkArray n a) 0 stop = if p a = true then mkArray n a else #[]

@[simp]

theorem Array.filter_mkArray_of_pos {stop n : Nat} {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} (w : stop = n) (h : p a = true) : filter p (mkArray n a) 0 stop = mkArray n a

@[simp]

theorem Array.filter_mkArray_of_neg {stop n : Nat} {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} (w : stop = n) (h : ¬p a = true) : filter p (mkArray n a) 0 stop = #[]

theorem Array.filterMap_mkArray {α : Type u_1} {β : Type u_2} {stop n : Nat} {a : α} {f : α → Option β} (w : stop = n := by simp) : filterMap f (mkArray n a) 0 stop = match f a with | none => #[] | some b => mkArray n b

theorem Array.filterMap_mkArray_of_some {α : Type u_1} {β : Type u_2} {a : α} {b : β} {n : Nat} {f : α → Option β} (h : f a = some b) : filterMap f (mkArray n a) = mkArray n b

@[simp]

theorem Array.filterMap_mkArray_of_isSome {α : Type u_1} {β : Type u_2} {a : α} {n : Nat} {f : α → Option β} (h : (f a).isSome = true) : filterMap f (mkArray n a) = mkArray n ((f a).get h)

@[simp]

theorem Array.filterMap_mkArray_of_none {α : Type u_1} {β : Type u_2} {a : α} {n : Nat} {f : α → Option β} (h : f a = none) : filterMap f (mkArray n a) = #[]

@[simp]

theorem Array.flatten_mkArray_empty {n : Nat} {α : Type u_1} : (mkArray n #[]).flatten = #[]

@[simp]

theorem Array.flatten_mkArray_singleton {n : Nat} {α✝ : Type u_1} {a : α✝} : (mkArray n #[a]).flatten = mkArray n a

@[simp]

theorem Array.flatten_mkArray_mkArray {n m : Nat} {α✝ : Type u_1} {a : α✝} : (mkArray n (mkArray m a)).flatten = mkArray (n * m) a

theorem Array.flatMap_mkArray {α : Type u_1} {n : Nat} {a : α} {β : Type u_2} (f : α → Array β) : flatMap f (mkArray n a) = (mkArray n (f a)).flatten

@[simp]

theorem Array.isEmpty_mkArray {n : Nat} {α✝ : Type u_1} {a : α✝} : (mkArray n a).isEmpty = decide (n = 0)

@[simp]

theorem Array.sum_mkArray_nat (n a : Nat) : (mkArray n a).sum = n * a

Preliminaries about swap needed for reverse.

theorem Array.getElem?_swap {α : Type u_1} (xs : Array α) (i j : Nat) (hi : i < xs.size) (hj : j < xs.size) (k : Nat) : (xs.swap i j hi hj)[k]? = if j = k then some xs[i] else if i = k then some xs[j] else xs[k]?

reverse

@[simp]

theorem Array.size_reverse {α : Type u_1} (xs : Array α) : xs.reverse.size = xs.size

@[irreducible]

theorem Array.size_reverse.go {α : Type u_1} (as : Array α) (i : Nat) (j : Fin as.size) : (reverse.loop as i j).size = as.size

@[simp]

theorem Array.toList_reverse {α : Type u_1} (xs : Array α) : xs.reverse.toList = xs.toList.reverse

@[irreducible]

theorem Array.toList_reverse.go {α : Type u_1} (xs as : Array α) (i j : Nat) (hj : j < as.size) (h : i + j + 1 = xs.size) (h₂ : as.size = xs.size) (H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j then xs.toList[k]? else xs.toList.reverse[k]?) (k : Nat) : (reverse.loop as i ⟨j, hj⟩).toList[k]? = xs.toList.reverse[k]?

@[simp]

theorem List.reverse_toArray {α : Type u_1} (l : List α) : l.toArray.reverse = l.reverse.toArray

@[simp]

theorem Array.reverse_push {α : Type u_1} (xs : Array α) (a : α) : (xs.push a).reverse = #[a] ++ xs.reverse

@[simp]

theorem Array.mem_reverse {α : Type u_1} {x : α} {xs : Array α} : x ∈ xs.reverse ↔ x ∈ xs

@[simp]

theorem Array.getElem_reverse {α : Type u_1} (xs : Array α) (i : Nat) (hi : i < xs.reverse.size) : xs.reverse[i] = xs[xs.size - 1 - i]

theorem Array.getElem_eq_getElem_reverse {α : Type u_1} {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] = xs.reverse[xs.size - 1 - i]

@[simp]

theorem Array.reverse_eq_empty_iff {α : Type u_1} {xs : Array α} : xs.reverse = #[] ↔ xs = #[]

theorem Array.reverse_ne_empty_iff {α : Type u_1} {xs : Array α} : xs.reverse ≠ #[] ↔ xs ≠ #[]

@[simp]

theorem Array.isEmpty_reverse {α : Type u_1} {xs : Array α} : xs.reverse.isEmpty = xs.isEmpty

theorem Array.getElem?_reverse' {α : Type u_1} {xs : Array α} (i j : Nat) (h : i + j + 1 = xs.size) : xs.reverse[i]? = xs[j]?

Variant of getElem?_reverse with a hypothesis giving the linear relation between the indices.

@[simp]

theorem Array.getElem?_reverse {α : Type u_1} {xs : Array α} {i : Nat} (h : i < xs.size) : xs.reverse[i]? = xs[xs.size - 1 - i]?

@[simp]

theorem Array.reverse_reverse {α : Type u_1} (xs : Array α) : xs.reverse.reverse = xs

theorem Array.reverse_eq_iff {α : Type u_1} {xs ys : Array α} : xs.reverse = ys ↔ xs = ys.reverse

@[simp]

theorem Array.reverse_inj {α : Type u_1} {xs ys : Array α} : xs.reverse = ys.reverse ↔ xs = ys

@[simp]

theorem Array.reverse_eq_push_iff {α : Type u_1} {xs ys : Array α} {a : α} : xs.reverse = ys.push a ↔ xs = #[a] ++ ys.reverse

@[simp]

theorem Array.map_reverse {α : Type u_1} {β : Type u_2} (f : α → β) (xs : Array α) : map f xs.reverse = (map f xs).reverse

@[simp]

theorem Array.filter_reverse' {α : Type u_1} {stop : Nat} (p : α → Bool) (xs : Array α) (w : stop = xs.size) : filter p xs.reverse 0 stop = (filter p xs).reverse

Variant of filter_reverse with a hypothesis giving the stop condition.

theorem Array.filter_reverse {α : Type u_1} (p : α → Bool) (xs : Array α) : filter p xs.reverse = (filter p xs).reverse

@[simp]

theorem Array.filterMap_reverse' {α : Type u_1} {β : Type u_2} {stop : Nat} (f : α → Option β) (xs : Array α) (w : stop = xs.size) : filterMap f xs.reverse 0 stop = (filterMap f xs).reverse

Variant of filterMap_reverse with a hypothesis giving the stop condition.

theorem Array.filterMap_reverse {α : Type u_1} {β : Type u_2} (f : α → Option β) (xs : Array α) : filterMap f xs.reverse = (filterMap f xs).reverse

@[simp]

theorem Array.reverse_append {α : Type u_1} (xs ys : Array α) : (xs ++ ys).reverse = ys.reverse ++ xs.reverse

@[simp]

theorem Array.reverse_eq_append_iff {α : Type u_1} {xs ys zs : Array α} : xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse

theorem Array.reverse_flatten {α : Type u_1} (xss : Array (Array α)) : xss.flatten.reverse = (map reverse xss).reverse.flatten

Reversing a flatten is the same as reversing the order of parts and reversing all parts.

theorem Array.flatten_reverse {α : Type u_1} (xss : Array (Array α)) : xss.reverse.flatten = (map reverse xss).flatten.reverse

Flattening a reverse is the same as reversing all parts and reversing the flattened result.

theorem Array.reverse_flatMap {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → Array β) : (flatMap f xs).reverse = flatMap (reverse ∘ f) xs.reverse

theorem Array.flatMap_reverse {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → Array β) : flatMap f xs.reverse = (flatMap (reverse ∘ f) xs).reverse

@[simp]

theorem Array.reverse_mkArray {α : Type u_1} (n : Nat) (a : α) : (mkArray n a).reverse = mkArray n a

extract

theorem Array.extract_loop_zero {α : Type u_1} (xs ys : Array α) (start : Nat) : extract.loop xs 0 start ys = ys

theorem Array.extract_loop_succ {α : Type u_1} (xs ys : Array α) (size start : Nat) (h : start < xs.size) : extract.loop xs (size + 1) start ys = extract.loop xs size (start + 1) (ys.push xs[start])

theorem Array.extract_loop_of_ge {α : Type u_1} (xs ys : Array α) (size start : Nat) (h : start ≥ xs.size) : extract.loop xs size start ys = ys

theorem Array.extract_loop_eq_aux {α : Type u_1} (xs ys : Array α) (size start : Nat) : extract.loop xs size start ys = ys ++ extract.loop xs size start #[]

theorem Array.extract_loop_eq {α : Type u_1} (xs ys : Array α) (size start : Nat) (h : start + size ≤ xs.size) : extract.loop xs size start ys = ys ++ xs.extract start (start + size)

theorem Array.size_extract_loop {α : Type u_1} (xs ys : Array α) (size start : Nat) : (extract.loop xs size start ys).size = ys.size + min size (xs.size - start)

@[simp]

theorem Array.size_extract {α : Type u_1} (xs : Array α) (start stop : Nat) : (xs.extract start stop).size = min stop xs.size - start

theorem Array.getElem_extract_loop_lt_aux {α : Type u_1} {i : Nat} (xs ys : Array α) (size start : Nat) (hlt : i < ys.size) : i < (extract.loop xs size start ys).size

theorem Array.getElem_extract_loop_lt {α : Type u_1} {i : Nat} (xs ys : Array α) (size start : Nat) (hlt : i < ys.size) (h : i < (extract.loop xs size start ys).size := ⋯) : (extract.loop xs size start ys)[i] = ys[i]

theorem Array.getElem_extract_loop_ge_aux {α : Type u_1} {i : Nat} (xs ys : Array α) (size start : Nat) (hge : i ≥ ys.size) (h : i < (extract.loop xs size start ys).size) : start + i - ys.size < xs.size

theorem Array.getElem_extract_loop_ge {α : Type u_1} {i : Nat} (xs ys : Array α) (size start : Nat) (hge : i ≥ ys.size) (h : i < (extract.loop xs size start ys).size) (h' : start + i - ys.size < xs.size := ⋯) : (extract.loop xs size start ys)[i] = xs[start + i - ys.size]

theorem Array.getElem_extract_aux {α : Type u_1} {i : Nat} {xs : Array α} {start stop : Nat} (h : i < (xs.extract start stop).size) : start + i < xs.size

@[simp]

theorem Array.getElem_extract {α : Type u_1} {i : Nat} {xs : Array α} {start stop : Nat} (h : i < (xs.extract start stop).size) : (xs.extract start stop)[i] = xs[start + i]

theorem Array.getElem?_extract {α : Type u_1} {i : Nat} {xs : Array α} {start stop : Nat} : (xs.extract start stop)[i]? = if i < min stop xs.size - start then xs[start + i]? else none

theorem Array.extract_congr {α : Type u_1} {start start' stop stop' : Nat} {xs ys : Array α} (w : xs = ys) (h : start = start') (h' : stop = stop') : xs.extract start stop = ys.extract start' stop'

@[simp]

theorem Array.toList_extract {α : Type u_1} (xs : Array α) (start stop : Nat) : (xs.extract start stop).toList = xs.toList.extract start stop

@[simp]

theorem Array.extract_size {α : Type u_1} (xs : Array α) : xs.extract = xs

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

abbrev Array.extract_all {α : Type u_1} (xs : Array α) : xs.extract = xs

Equations

• @Array.extract_all = @Array.extract_size

theorem Array.extract_empty_of_stop_le_start {α : Type u_1} (xs : Array α) {start stop : Nat} (h : stop ≤ start) : xs.extract start stop = #[]

theorem Array.extract_empty_of_size_le_start {α : Type u_1} (xs : Array α) {start stop : Nat} (h : xs.size ≤ start) : xs.extract start stop = #[]

@[simp]

theorem Array.extract_empty {α : Type u_1} (start stop : Nat) : #[].extract start stop = #[]

@[simp]

theorem List.extract_toArray {α : Type u_1} (l : List α) (start stop : Nat) : l.toArray.extract start stop = (l.extract start stop).toArray

@[deprecated Array.extract_size (since := "2025-02-27")]

theorem Array.take_size {α : Type u_1} (xs : Array α) : xs.take xs.size = xs

shrink

@[simp]

theorem Array.size_shrink_loop {α : Type u_1} (xs : Array α) (n : Nat) : (shrink.loop n xs).size = xs.size - n

@[simp]

theorem Array.getElem_shrink_loop {α : Type u_1} (xs : Array α) (n i : Nat) (h : i < (shrink.loop n xs).size) : (shrink.loop n xs)[i] = xs[i]

@[simp]

theorem Array.size_shrink {α : Type u_1} (xs : Array α) (i : Nat) : (xs.shrink i).size = min i xs.size

@[simp]

theorem Array.getElem_shrink {α : Type u_1} (xs : Array α) (i j : Nat) (h : j < (xs.shrink i).size) : (xs.shrink i)[j] = xs[j]

@[simp]

theorem Array.toList_shrink {α : Type u_1} (xs : Array α) (i : Nat) : (xs.shrink i).toList = List.take i xs.toList

@[simp]

theorem Array.shrink_eq_take {α : Type u_1} (xs : Array α) (i : Nat) : xs.shrink i = xs.take i

foldlM and foldrM

theorem Array.foldlM_start_stop {α : Type u_1} {β : Type u_2} {m : Type u_2 → Type u_3} [Monad m] (xs : Array α) (f : β → α → m β) (b : β) (start stop : Nat) : foldlM f b xs start stop = foldlM f b (xs.extract start stop)

theorem Array.foldrM_start_stop {α : Type u_1} {β : Type u_2} {m : Type u_2 → Type u_3} [Monad m] (xs : Array α) (f : α → β → m β) (b : β) (start stop : Nat) : foldrM f b xs start stop = foldrM f b (xs.extract stop start)

theorem Array.foldlM_congr {β : Type u_1} {α : Type u_2} {start start' stop stop' : Nat} {m : Type u_1 → Type u_3} [Monad m] {f g : β → α → m β} {b : β} {xs xs' : Array α} (w : xs = xs') (h : ∀ (x : β) (y : α), f x y = g x y) (hstart : start = start') (hstop : stop = stop') : foldlM f b xs start stop = foldlM g b xs' start' stop'

theorem Array.foldrM_congr {α : Type u_1} {β : Type u_2} {start start' stop stop' : Nat} {m : Type u_2 → Type u_3} [Monad m] {f g : α → β → m β} {b : β} {xs xs' : Array α} (w : xs = xs') (h : ∀ (x : α) (y : β), f x y = g x y) (hstart : start = start') (hstop : stop = stop') : foldrM f b xs start stop = foldrM g b xs' start' stop'

@[simp]

theorem Array.foldlM_append' {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {stop : Nat} [Monad m] [LawfulMonad m] (f : β → α → m β) (b : β) (xs xs' : Array α) (w : stop = xs.size + xs'.size) : foldlM f b (xs ++ xs') 0 stop = do let init ← foldlM f b xs foldlM f init xs'

Variant of foldlM_append with a side condition for the stop argument.

theorem Array.foldlM_append {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] [LawfulMonad m] (f : β → α → m β) (b : β) (xs xs' : Array α) : foldlM f b (xs ++ xs') = do let init ← foldlM f b xs foldlM f init xs'

@[simp]

theorem Array.foldlM_loop_empty {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {s : Nat} {h : s ≤ #[].size} [Monad m] (f : β → α → m β) (init : β) (i j : Nat) : foldlM.loop f #[] s h i j init = pure init

@[simp]

theorem Array.foldlM_empty {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {start stop : Nat} [Monad m] (f : β → α → m β) (init : β) : foldlM f init #[] start stop = pure init

@[simp]

theorem Array.foldrM_fold_empty {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (init : β) (i j : Nat) (h : j ≤ #[].size) : foldrM.fold f #[] i j h init = pure init

@[simp]

theorem Array.foldrM_empty {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {start stop : Nat} [Monad m] (f : α → β → m β) (init : β) : foldrM f init #[] start stop = pure init

@[simp]

theorem Array.foldlM_push' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {stop : Nat} [Monad m] [LawfulMonad m] (xs : Array α) (a : α) (f : β → α → m β) (b : β) (w : stop = xs.size + 1) : foldlM f b (xs.push a) 0 stop = do let b ← foldlM f b xs f b a

Variant of foldlM_push with a side condition for the stop argument.

theorem Array.foldlM_push {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (xs : Array α) (a : α) (f : β → α → m β) (b : β) : foldlM f b (xs.push a) = do let b ← foldlM f b xs f b a

theorem Array.foldl_eq_foldlM {β : Type u_1} {α : Type u_2} {start stop : Nat} (f : β → α → β) (b : β) (xs : Array α) : foldl f b xs start stop = foldlM f b xs start stop

theorem Array.foldr_eq_foldrM {α : Type u_1} {β : Type u_2} {start stop : Nat} (f : α → β → β) (b : β) (xs : Array α) : foldr f b xs start stop = foldrM f b xs start stop

@[simp]

theorem Array.id_run_foldlM {β : Type u_1} {α : Type u_2} {start stop : Nat} (f : β → α → Id β) (b : β) (xs : Array α) : (foldlM f b xs start stop).run = foldl f b xs start stop

@[simp]

theorem Array.id_run_foldrM {α : Type u_1} {β : Type u_2} {start stop : Nat} (f : α → β → Id β) (b : β) (xs : Array α) : (foldrM f b xs start stop).run = foldr f b xs start stop

@[simp]

theorem Array.foldlM_reverse' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {stop : Nat} [Monad m] (xs : Array α) (f : β → α → m β) (b : β) (w : stop = xs.size) : foldlM f b xs.reverse 0 stop = foldrM (fun (x : α) (y : β) => f y x) b xs

Variant of foldlM_reverse with a side condition for the stop argument.

@[simp]

theorem Array.foldrM_reverse' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {start : Nat} [Monad m] (xs : Array α) (f : α → β → m β) (b : β) (w : start = xs.size) : foldrM f b xs.reverse start = foldlM (fun (x : β) (y : α) => f y x) b xs

Variant of foldrM_reverse with a side condition for the start argument.

theorem Array.foldlM_reverse {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (xs : Array α) (f : β → α → m β) (b : β) : foldlM f b xs.reverse = foldrM (fun (x : α) (y : β) => f y x) b xs

theorem Array.foldrM_reverse {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (xs : Array α) (f : α → β → m β) (b : β) : foldrM f b xs.reverse = foldlM (fun (x : β) (y : α) => f y x) b xs

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

@[simp]

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

Variant of foldrM_push with h : start = arr.size + 1 rather than (arr.push a).size as the argument.

foldl / foldr

theorem Array.foldl_induction {α : Type u_1} {β : Type u_2} {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive 0 init) {f : β → α → β} (hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → motive (↑i + 1) (f b as[i])) : motive as.size (foldl f init as)

@[irreducible]

theorem Array.foldl_induction.go {α : Type u_1} {β : Type u_2} {as : Array α} (motive : Nat → β → Prop) {f : β → α → β} (hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → motive (↑i + 1) (f b as[i])) {i j : Nat} {b : β} (h₁ : j ≤ as.size) (h₂ : as.size ≤ i + j) (H : motive j b) : motive as.size (foldlM.loop f as as.size ⋯ i j b)

theorem Array.foldr_induction {α : Type u_1} {β : Type u_2} {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive as.size init) {f : α → β → β} (hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)) : motive 0 (foldr f init as)

@[irreducible]

theorem Array.foldr_induction.go {α : Type u_1} {β : Type u_2} {as : Array α} (motive : Nat → β → Prop) {f : α → β → β} (hf : ∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)) {i : Nat} {b : β} (hi : i ≤ as.size) (H : motive i b) : motive 0 (foldrM.fold f as 0 i hi b)

theorem Array.foldl_congr {α : Type u_1} {β : Type u_2} {as bs : Array α} (h₀ : as = bs) {f g : β → α → β} (h₁ : f = g) {a b : β} (h₂ : a = b) {start start' stop stop' : Nat} (h₃ : start = start') (h₄ : stop = stop') : foldl f a as start stop = foldl g b bs start' stop'

theorem Array.foldr_congr {α : Type u_1} {β : Type u_2} {as bs : Array α} (h₀ : as = bs) {f g : α → β → β} (h₁ : f = g) {a b : β} (h₂ : a = b) {start start' stop stop' : Nat} (h₃ : start = start') (h₄ : stop = stop') : foldr f a as start stop = foldr g b bs start' stop'

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

@[simp]

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

Variant of foldr_push with the h : start = arr.size + 1 rather than (arr.push a).size as the argument.

@[simp]

theorem Array.foldl_push_eq_append {α : Type u_1} {β : Type u_2} {stop : Nat} {as : Array α} {bs : Array β} {f : α → β} (w : stop = as.size) : foldl (fun (acc : Array β) (a : α) => acc.push (f a)) bs as 0 stop = bs ++ map f as

@[simp]

theorem Array.foldl_cons_eq_append {α : Type u_1} {β : Type u_2} {stop : Nat} {as : Array α} {bs : List β} {f : α → β} (w : stop = as.size) : foldl (fun (acc : List β) (a : α) => f a :: acc) bs as 0 stop = (map f as).reverse.toList ++ bs

@[simp]

theorem Array.foldr_cons_eq_append {α : Type u_1} {β : Type u_2} {start : Nat} {as : Array α} {bs : List β} {f : α → β} (w : start = as.size) : foldr (fun (a : α) (acc : List β) => f a :: acc) bs as start = (map f as).toList ++ bs

@[simp]

theorem Array.foldr_cons_eq_append' {α : Type u_1} {start : Nat} {as : Array α} {bs : List α} (w : start = as.size) : foldr List.cons bs as start = as.toList ++ bs

Variant of foldr_cons_eq_append specialized to f = id.

@[simp]

theorem Array.foldr_append_eq_append {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → Array β) (ys : Array β) : foldr (fun (x1 : α) (x2 : Array β) => f x1 ++ x2) ys xs = (map f xs).flatten ++ ys

@[simp]

theorem Array.foldl_append_eq_append {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → Array β) (ys : Array β) : foldl (fun (x1 : Array β) (x2 : α) => x1 ++ f x2) ys xs = ys ++ (map f xs).flatten

@[simp]

theorem Array.foldr_flip_append_eq_append {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → Array β) (ys : Array β) : foldr (fun (x : α) (acc : Array β) => acc ++ f x) ys xs = ys ++ (map f xs).reverse.flatten

@[simp]

theorem Array.foldl_flip_append_eq_append {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → Array β) (ys : Array β) : foldl (fun (acc : Array β) (y : α) => f y ++ acc) ys xs = (map f xs).reverse.flatten ++ ys

theorem Array.foldl_map' {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} {stop : Nat} (f : β₁ → β₂) (g : α → β₂ → α) (xs : Array β₁) (init : α) (w : stop = xs.size) : foldl g init (map f xs) 0 stop = foldl (fun (x : α) (y : β₁) => g x (f y)) init xs

theorem Array.foldr_map' {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} {start : Nat} (f : α₁ → α₂) (g : α₂ → β → β) (xs : Array α₁) (init : β) (w : start = xs.size) : foldr g init (map f xs) start = foldr (fun (x : α₁) (y : β) => g (f x) y) init xs

theorem Array.foldl_map {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁ → β₂) (g : α → β₂ → α) (xs : Array β₁) (init : α) : foldl g init (map f xs) = foldl (fun (x : α) (y : β₁) => g x (f y)) init xs

theorem Array.foldr_map {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁ → α₂) (g : α₂ → β → β) (xs : Array α₁) (init : β) : foldr g init (map f xs) = foldr (fun (x : α₁) (y : β) => g (f x) y) init xs

theorem Array.foldl_filterMap' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {stop : Nat} (f : α → Option β) (g : γ → β → γ) (xs : Array α) (init : γ) (w : stop = (filterMap f xs).size) : foldl g init (filterMap f xs) 0 stop = foldl (fun (x : γ) (y : α) => match f y with | some b => g x b | none => x) init xs

theorem Array.foldr_filterMap' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {start : Nat} (f : α → Option β) (g : β → γ → γ) (xs : Array α) (init : γ) (w : start = (filterMap f xs).size) : foldr g init (filterMap f xs) start = foldr (fun (x : α) (y : γ) => match f x with | some b => g b y | none => y) init xs

theorem Array.foldl_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β) (g : γ → β → γ) (xs : Array α) (init : γ) : foldl g init (filterMap f xs) = foldl (fun (x : γ) (y : α) => match f y with | some b => g x b | none => x) init xs

theorem Array.foldr_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β) (g : β → γ → γ) (xs : Array α) (init : γ) : foldr g init (filterMap f xs) = foldr (fun (x : α) (y : γ) => match f x with | some b => g b y | none => y) init xs

theorem Array.foldl_map_hom' {α : Type u_1} {β : Type u_2} {stop : Nat} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (xs : Array α) (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) (w : stop = xs.size) : foldl f' (g a) (map g xs) 0 stop = g (foldl f a xs)

theorem Array.foldr_map_hom' {α : Type u_1} {β : Type u_2} {start : Nat} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (xs : Array α) (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) (w : start = xs.size) : foldr f' (g a) (map g xs) start = g (foldr f a xs)

theorem Array.foldl_map_hom {α : Type u_1} {β : Type u_2} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (xs : Array α) (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : foldl f' (g a) (map g xs) = g (foldl f a xs)

theorem Array.foldr_map_hom {α : Type u_1} {β : Type u_2} (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (xs : Array α) (h : ∀ (x y : α), f' (g x) (g y) = g (f x y)) : foldr f' (g a) (map g xs) = g (foldr f a xs)

@[simp]

theorem Array.foldrM_append' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {start : Nat} [Monad m] [LawfulMonad m] (f : α → β → m β) (b : β) (xs ys : Array α) (w : start = xs.size + ys.size) : foldrM f b (xs ++ ys) start = do let init ← foldrM f b ys foldrM f init xs

Variant of foldrM_append with a side condition for the start argument.

theorem Array.foldrM_append {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → β → m β) (b : β) (xs ys : Array α) : foldrM f b (xs ++ ys) = do let init ← foldrM f b ys foldrM f init xs

@[simp]

theorem Array.foldl_append' {α : Type u_1} {stop : Nat} {β : Type u_2} (f : β → α → β) (b : β) (xs ys : Array α) (w : stop = xs.size + ys.size) : foldl f b (xs ++ ys) 0 stop = foldl f (foldl f b xs) ys

@[simp]

theorem Array.foldr_append' {α : Type u_1} {β : Type u_2} {start : Nat} (f : α → β → β) (b : β) (xs ys : Array α) (w : start = xs.size + ys.size) : foldr f b (xs ++ ys) start = foldr f (foldr f b ys) xs

theorem Array.foldl_append {α : Type u_1} {β : Type u_2} (f : β → α → β) (b : β) (xs ys : Array α) : foldl f b (xs ++ ys) = foldl f (foldl f b xs) ys

theorem Array.foldr_append {α : Type u_1} {β : Type u_2} (f : α → β → β) (b : β) (xs ys : Array α) : foldr f b (xs ++ ys) = foldr f (foldr f b ys) xs

@[simp]

theorem Array.foldl_flatten' {β : Type u_1} {α : Type u_2} {stop : Nat} (f : β → α → β) (b : β) (xss : Array (Array α)) (w : stop = xss.flatten.size) : foldl f b xss.flatten 0 stop = foldl (fun (b : β) (xs : Array α) => foldl f b xs) b xss

@[simp]

theorem Array.foldr_flatten' {α : Type u_1} {β : Type u_2} {start : Nat} (f : α → β → β) (b : β) (xss : Array (Array α)) (w : start = xss.flatten.size) : foldr f b xss.flatten start = foldr (fun (xs : Array α) (b : β) => foldr f b xs) b xss

theorem Array.foldl_flatten {β : Type u_1} {α : Type u_2} (f : β → α → β) (b : β) (xss : Array (Array α)) : foldl f b xss.flatten = foldl (fun (b : β) (xs : Array α) => foldl f b xs) b xss

theorem Array.foldr_flatten {α : Type u_1} {β : Type u_2} (f : α → β → β) (b : β) (xss : Array (Array α)) : foldr f b xss.flatten = foldr (fun (xs : Array α) (b : β) => foldr f b xs) b xss

@[simp]

theorem Array.foldl_reverse' {α : Type u_1} {β : Type u_2} {stop : Nat} (xs : Array α) (f : β → α → β) (b : β) (w : stop = xs.size) : foldl f b xs.reverse 0 stop = foldr (fun (x : α) (y : β) => f y x) b xs

Variant of foldl_reverse with a side condition for the stop argument.

@[simp]

theorem Array.foldr_reverse' {α : Type u_1} {β : Type u_2} {start : Nat} (xs : Array α) (f : α → β → β) (b : β) (w : start = xs.size) : foldr f b xs.reverse start = foldl (fun (x : β) (y : α) => f y x) b xs

Variant of foldr_reverse with a side condition for the start argument.

theorem Array.foldl_reverse {α : Type u_1} {β : Type u_2} (xs : Array α) (f : β → α → β) (b : β) : foldl f b xs.reverse = foldr (fun (x : α) (y : β) => f y x) b xs

theorem Array.foldr_reverse {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → β → β) (b : β) : foldr f b xs.reverse = foldl (fun (x : β) (y : α) => f y x) b xs

theorem Array.foldl_eq_foldr_reverse {α : Type u_1} {β : Type u_2} (xs : Array α) (f : β → α → β) (b : β) : foldl f b xs = foldr (fun (x : α) (y : β) => f y x) b xs.reverse

theorem Array.foldr_eq_foldl_reverse {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → β → β) (b : β) : foldr f b xs = foldl (fun (x : β) (y : α) => f y x) b xs.reverse

@[simp]

theorem Array.foldr_push_eq_append {α : Type u_1} {β : Type u_2} {start : Nat} {as : Array α} {bs : Array β} {f : α → β} (w : start = as.size) : foldr (fun (a : α) (xs : Array β) => xs.push (f a)) bs as start = bs ++ (map f as).reverse

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

abbrev Array.foldr_flip_push_eq_append {α : Type u_1} {β : Type u_2} {start : Nat} {as : Array α} {bs : Array β} {f : α → β} (w : start = as.size) : foldr (fun (a : α) (xs : Array β) => xs.push (f a)) bs as start = bs ++ (map f as).reverse

Equations

• @Array.foldr_flip_push_eq_append = @Array.foldr_push_eq_append

theorem Array.foldl_assoc {α : Type u_1} {op : α → α → α} [ha : Std.Associative op] {xs : Array α} {a₁ a₂ : α} : foldl op (op a₁ a₂) xs = op a₁ (foldl op a₂ xs)

theorem Array.foldr_assoc {α : Type u_1} {op : α → α → α} [ha : Std.Associative op] {xs : Array α} {a₁ a₂ : α} : foldr op (op a₁ a₂) xs = op (foldr op a₁ xs) a₂

theorem Array.foldl_hom {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (xs : Array β) (init : α₁) (H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)) : foldl g₂ (f init) xs = f (foldl g₁ init xs)

theorem Array.foldr_hom {β₁ : Type u_1} {β₂ : Type u_2} {α : Type u_3} (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : α → β₂ → β₂) (xs : Array α) (init : β₁) (H : ∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)) : foldr g₂ (f init) xs = f (foldr g₁ init xs)

theorem Array.foldl_rel {α : Type u_1} {β : Type u_2} {xs : Array α} {f g : β → α → β} {a b : β} (r : β → β → Prop) (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) : r (foldl (fun (acc : β) (a : α) => f acc a) a xs) (foldl (fun (acc : β) (a : α) => g acc a) b xs)

We can prove that two folds over the same array are related (by some arbitrary relation) if we know that the initial elements are related and the folding function, for each element of the array, preserves the relation.

theorem Array.foldr_rel {α : Type u_1} {β : Type u_2} {xs : Array α} {f g : α → β → β} {a b : β} (r : β → β → Prop) (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c c' : β), r c c' → r (f a c) (g a c')) : r (foldr (fun (a : α) (acc : β) => f a acc) a xs) (foldr (fun (a : α) (acc : β) => g a acc) b xs)

We can prove that two folds over the same array are related (by some arbitrary relation) if we know that the initial elements are related and the folding function, for each element of the array, preserves the relation.

@[simp]

theorem Array.foldl_add_const {α : Type u_1} (xs : Array α) (a b : Nat) : foldl (fun (x : Nat) (x_1 : α) => x + a) b xs = b + a * xs.size

@[simp]

theorem Array.foldr_add_const {α : Type u_1} (xs : Array α) (a b : Nat) : foldr (fun (x : α) (x : Nat) => x + a) b xs = b + a * xs.size

Further results about back and back?

@[simp]

theorem Array.back?_eq_none_iff {α : Type u_1} {xs : Array α} : xs.back? = none ↔ xs = #[]

theorem Array.back?_eq_some_iff {α : Type u_1} {xs : Array α} {a : α} : xs.back? = some a ↔ ∃ (ys : Array α), xs = ys.push a

@[simp]

theorem Array.back?_isSome {α✝ : Type u_1} {xs : Array α✝} : xs.back?.isSome = true ↔ xs ≠ #[]

theorem Array.mem_of_back? {α : Type u_1} {xs : Array α} {a : α} (h : xs.back? = some a) : a ∈ xs

@[simp]

theorem Array.back_append_of_size_pos {α : Type u_1} {xs ys : Array α} {h₁ : 0 < (xs ++ ys).size} (h₂ : 0 < ys.size) : (xs ++ ys).back h₁ = ys.back h₂

theorem Array.back_append {α : Type u_1} {ys xs : Array α} (h : 0 < (xs ++ ys).size) : (xs ++ ys).back h = if h' : ys.isEmpty = true then xs.back ⋯ else ys.back ⋯

theorem Array.back_append_right {α : Type u_1} {xs ys : Array α} (h : 0 < ys.size) : (xs ++ ys).back ⋯ = ys.back h

theorem Array.back_append_left {α : Type u_1} {xs ys : Array α} (w : 0 < (xs ++ ys).size) (h : ys.size = 0) : (xs ++ ys).back w = xs.back ⋯

@[simp]

theorem Array.back?_append {α : Type u_1} {xs ys : Array α} : (xs ++ ys).back? = ys.back?.or xs.back?

theorem Array.back_filter_of_pos {α : Type u_1} {p : α → Bool} {xs : Array α} (w : 0 < xs.size) (h : p (xs.back w) = true) : (filter p xs).back ⋯ = xs.back w

theorem Array.back_filterMap_of_eq_some {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} {w : 0 < xs.size} {b : β} (h : f (xs.back w) = some b) : some ((filterMap f xs).back ⋯) = some b

theorem Array.back?_flatMap {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} : (flatMap f xs).back? = findSome? (fun (a : α) => (f a).back?) xs.reverse

theorem Array.back?_flatten {α : Type u_1} {xss : Array (Array α)} : xss.flatten.back? = findSome? (fun (xs : Array α) => xs.back?) xss.reverse

theorem Array.back?_mkArray {α : Type u_1} (a : α) (n : Nat) : (mkArray n a).back? = if n = 0 then none else some a

@[simp]

theorem Array.back_mkArray {n : Nat} {α✝ : Type u_1} {a : α✝} (w : 0 < n) : (mkArray n a).back ⋯ = a

Additional operations

leftpad

theorem Array.size_leftpad {α : Type u_1} (n : Nat) (a : α) (xs : Array α) : (leftpad n a xs).size = max n xs.size

theorem Array.size_rightpad {α : Type u_1} (n : Nat) (a : α) (xs : Array α) : (rightpad n a xs).size = max n xs.size

contains

theorem Array.elem_cons_self {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : elem a (xs.push a) = true

theorem Array.contains_eq_any_beq {α : Type u_1} [BEq α] (xs : Array α) (a : α) : xs.contains a = xs.any fun (x : α) => a == x

theorem Array.contains_iff_exists_mem_beq {α : Type u_1} [BEq α] {xs : Array α} {a : α} : xs.contains a = true ↔ ∃ (a' : α), a' ∈ xs ∧ (a == a') = true

theorem Array.contains_iff_mem {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : xs.contains a = true ↔ a ∈ xs

more lemmas about pop

theorem Array.pop_append {α : Type u_1} {xs ys : Array α} : (xs ++ ys).pop = if ys.isEmpty = true then xs.pop else xs ++ ys.pop

@[simp]

theorem Array.pop_mkArray {α : Type u_1} (n : Nat) (a : α) : (mkArray n a).pop = mkArray (n - 1) a

modify

@[simp]

theorem Array.size_modify {α : Type u_1} (xs : Array α) (i : Nat) (f : α → α) : (xs.modify i f).size = xs.size

theorem Array.getElem_modify {α : Type u_1} {f : α → α} {xs : Array α} {j i : Nat} (h : i < (xs.modify j f).size) : (xs.modify j f)[i] = if j = i then f xs[i] else xs[i]

@[simp]

theorem Array.toList_modify {α : Type u_1} {i : Nat} (xs : Array α) (f : α → α) : (xs.modify i f).toList = List.modify f i xs.toList

theorem Array.getElem_modify_self {α : Type u_1} {xs : Array α} {i : Nat} (f : α → α) (h : i < (xs.modify i f).size) : (xs.modify i f)[i] = f xs[i]

theorem Array.getElem_modify_of_ne {α : Type u_1} {j : Nat} {xs : Array α} {i : Nat} (h : i ≠ j) (f : α → α) (hj : j < (xs.modify i f).size) : (xs.modify i f)[j] = xs[j]

theorem Array.getElem?_modify {α : Type u_1} {xs : Array α} {i : Nat} {f : α → α} {j : Nat} : (xs.modify i f)[j]? = if i = j then Option.map f xs[j]? else xs[j]?

swap

@[simp]

theorem Array.getElem_swap_right {α : Type u_1} (xs : Array α) {i j : Nat} {hi : i < xs.size} {hj : j < xs.size} : (xs.swap i j hi hj)[j] = xs[i]

@[simp]

theorem Array.getElem_swap_left {α : Type u_1} (xs : Array α) {i j : Nat} {hi : i < xs.size} {hj : j < xs.size} : (xs.swap i j hi hj)[i] = xs[j]

@[simp]

theorem Array.getElem_swap_of_ne {α : Type u_1} {k : Nat} (xs : Array α) {i j : Nat} {hi : i < xs.size} {hj : j < xs.size} (hp : k < xs.size) (hi' : k ≠ i) (hj' : k ≠ j) : (xs.swap i j hi hj)[k] = xs[k]

theorem Array.getElem_swap' {α : Type u_1} (xs : Array α) (i j : Nat) {hi : i < xs.size} {hj : j < xs.size} (k : Nat) (hk : k < xs.size) : (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]

theorem Array.getElem_swap {α : Type u_1} (xs : Array α) (i j : Nat) {hi : i < xs.size} {hj : j < xs.size} (k : Nat) (hk : k < (xs.swap i j hi hj).size) : (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]

@[simp]

theorem Array.swap_swap {α : Type u_1} (xs : Array α) {i j : Nat} (hi : i < xs.size) (hj : j < xs.size) : (xs.swap i j hi hj).swap i j ⋯ ⋯ = xs

theorem Array.swap_comm {α : Type u_1} (xs : Array α) {i j : Nat} {hi : i < xs.size} {hj : j < xs.size} : xs.swap i j hi hj = xs.swap j i hj hi

@[simp]

theorem Array.size_swapIfInBounds {α : Type u_1} (xs : Array α) (i j : Nat) : (xs.swapIfInBounds i j).size = xs.size

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

abbrev Array.size_swap! {α : Type u_1} (xs : Array α) (i j : Nat) : (xs.swapIfInBounds i j).size = xs.size

Equations

• @Array.size_swap! = @Array.size_swapIfInBounds

swapAt

@[simp]

theorem Array.swapAt_def {α : Type u_1} (xs : Array α) (i : Nat) (v : α) (hi : i < xs.size) : xs.swapAt i v hi = (xs[i], xs.set i v hi)

theorem Array.size_swapAt {α : Type u_1} (xs : Array α) (i : Nat) (v : α) (hi : i < xs.size) : (xs.swapAt i v hi).snd.size = xs.size

@[simp]

theorem Array.swapAt!_def {α : Type u_1} (xs : Array α) (i : Nat) (v : α) (h : i < xs.size) : xs.swapAt! i v = (xs[i], xs.set i v h)

@[simp]

theorem Array.size_swapAt! {α : Type u_1} (xs : Array α) (i : Nat) (v : α) : (xs.swapAt! i v).snd.size = xs.size

replace

@[simp]

theorem Array.size_replace {α : Type u_1} [BEq α] {a b : α} {xs : Array α} : (xs.replace a b).size = xs.size

@[simp]

theorem Array.replace_of_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {xs : Array α} (h : ¬a ∈ xs) : xs.replace a b = xs

theorem Array.getElem?_replace {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {xs : Array α} {i : Nat} : (xs.replace a b)[i]? = if (xs[i]? == some a) = true then if a ∈ xs.take i then some a else some b else xs[i]?

theorem Array.getElem?_replace_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {xs : Array α} {i : Nat} (h : xs[i]? ≠ some a) : (xs.replace a b)[i]? = xs[i]?

theorem Array.getElem_replace {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {xs : Array α} {i : Nat} (h : i < xs.size) : (xs.replace a b)[i] = if (xs[i] == a) = true then if a ∈ xs.take i then a else b else xs[i]

theorem Array.getElem_replace_of_ne {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {xs : Array α} {i : Nat} {h : i < xs.size} (h' : xs[i] ≠ a) : (xs.replace a b)[i] = xs[i]

theorem Array.replace_append {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {xs ys : Array α} : (xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b

theorem Array.replace_append_left {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {xs ys : Array α} (h : a ∈ xs) : (xs ++ ys).replace a b = xs.replace a b ++ ys

theorem Array.replace_append_right {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {xs ys : Array α} (h : ¬a ∈ xs) : (xs ++ ys).replace a b = xs ++ ys.replace a b

theorem Array.replace_extract {α : Type u_1} [BEq α] [LawfulBEq α] {a b : α} {xs : Array α} {i : Nat} : (xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i

@[simp]

theorem Array.replace_mkArray_self {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {b a : α} (h : 0 < n) : (mkArray n a).replace a b = #[b] ++ mkArray (n - 1) a

@[simp]

theorem Array.replace_mkArray_ne {α : Type u_1} [BEq α] [LawfulBEq α] {n : Nat} {a b c : α} (h : (!b == a) = true) : (mkArray n a).replace b c = mkArray n a

Logic

any / all

theorem Array.not_any_eq_all_not {α : Type u_1} (xs : Array α) (p : α → Bool) : (!xs.any p) = xs.all fun (a : α) => !p a

theorem Array.not_all_eq_any_not {α : Type u_1} (xs : Array α) (p : α → Bool) : (!xs.all p) = xs.any fun (a : α) => !p a

theorem Array.and_any_distrib_left {α : Type u_1} (xs : Array α) (p : α → Bool) (q : Bool) : (q && xs.any p) = xs.any fun (a : α) => q && p a

theorem Array.and_any_distrib_right {α : Type u_1} (xs : Array α) (p : α → Bool) (q : Bool) : (xs.any p && q) = xs.any fun (a : α) => p a && q

theorem Array.or_all_distrib_left {α : Type u_1} (xs : Array α) (p : α → Bool) (q : Bool) : (q || xs.all p) = xs.all fun (a : α) => q || p a

theorem Array.or_all_distrib_right {α : Type u_1} (xs : Array α) (p : α → Bool) (q : Bool) : (xs.all p || q) = xs.all fun (a : α) => p a || q

theorem Array.any_eq_not_all_not {α : Type u_1} (xs : Array α) (p : α → Bool) : xs.any p = !xs.all fun (x : α) => !p x

@[simp]

theorem Array.any_map' {α : Type u_1} {β : Type u_2} {stop : Nat} {f : α → β} {xs : Array α} {p : β → Bool} (w : stop = xs.size) : (map f xs).any p 0 stop = xs.any (p ∘ f)

Variant of any_map with a side condition for the stop argument.

@[simp]

theorem Array.all_map' {α : Type u_1} {β : Type u_2} {stop : Nat} {f : α → β} {xs : Array α} {p : β → Bool} (w : stop = xs.size) : (map f xs).all p 0 stop = xs.all (p ∘ f)

Variant of all_map with a side condition for the stop argument.

theorem Array.any_map {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {p : β → Bool} : (map f xs).any p = xs.any (p ∘ f)

theorem Array.all_map {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {p : β → Bool} : (map f xs).all p = xs.all (p ∘ f)

@[simp]

theorem Array.any_filter' {α : Type u_1} {stop : Nat} {xs : Array α} {p q : α → Bool} (w : stop = (filter p xs).size) : (filter p xs).any q 0 stop = xs.any fun (a : α) => p a && q a

Variant of any_filter with a side condition for the stop argument.

@[simp]

theorem Array.all_filter' {α : Type u_1} {stop : Nat} {xs : Array α} {p q : α → Bool} (w : stop = (filter p xs).size) : (filter p xs).all q 0 stop = xs.all fun (a : α) => decide (p a = true → q a = true)

Variant of all_filter with a side condition for the stop argument.

theorem Array.any_filter {α : Type u_1} {xs : Array α} {p q : α → Bool} : (filter p xs).any q = xs.any fun (a : α) => p a && q a

theorem Array.all_filter {α : Type u_1} {xs : Array α} {p q : α → Bool} : (filter p xs).all q = xs.all fun (a : α) => decide (p a = true → q a = true)

@[simp]

theorem Array.any_filterMap' {α : Type u_1} {β : Type u_2} {stop : Nat} {xs : Array α} {f : α → Option β} {p : β → Bool} (w : stop = (filterMap f xs).size) : (filterMap f xs).any p 0 stop = xs.any fun (a : α) => match f a with | some b => p b | none => false

Variant of any_filterMap with a side condition for the stop argument.

@[simp]

theorem Array.all_filterMap' {α : Type u_1} {β : Type u_2} {stop : Nat} {xs : Array α} {f : α → Option β} {p : β → Bool} (w : stop = (filterMap f xs).size) : (filterMap f xs).all p 0 stop = xs.all fun (a : α) => match f a with | some b => p b | none => true

Variant of all_filterMap with a side condition for the stop argument.

theorem Array.any_filterMap {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Option β} {p : β → Bool} : (filterMap f xs).any p = xs.any fun (a : α) => match f a with | some b => p b | none => false

theorem Array.all_filterMap {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Option β} {p : β → Bool} : (filterMap f xs).all p = xs.all fun (a : α) => match f a with | some b => p b | none => true

@[simp]

theorem Array.any_append' {α : Type u_1} {stop : Nat} {f : α → Bool} {xs ys : Array α} (w : stop = (xs ++ ys).size) : (xs ++ ys).any f 0 stop = (xs.any f || ys.any f)

Variant of any_append with a side condition for the stop argument.

@[simp]

theorem Array.all_append' {α : Type u_1} {stop : Nat} {f : α → Bool} {xs ys : Array α} (w : stop = (xs ++ ys).size) : (xs ++ ys).all f 0 stop = (xs.all f && ys.all f)

Variant of all_append with a side condition for the stop argument.

theorem Array.any_append {α : Type u_1} {f : α → Bool} {xs ys : Array α} : (xs ++ ys).any f = (xs.any f || ys.any f)

theorem Array.all_append {α : Type u_1} {f : α → Bool} {xs ys : Array α} : (xs ++ ys).all f = (xs.all f && ys.all f)

theorem Array.anyM_congr {m : Type → Type u_1} {α : Type u_2} {start₁ start₂ stop₁ stop₂ : Nat} [Monad m] {xs ys : Array α} (w : xs = ys) {p q : α → m Bool} (h : ∀ (a : α), p a = q a) (wstart : start₁ = start₂) (wstop : stop₁ = stop₂) : anyM p xs start₁ stop₁ = anyM q ys start₂ stop₂

theorem Array.any_congr {α : Type u_1} {start₁ start₂ stop₁ stop₂ : Nat} {xs ys : Array α} (w : xs = ys) {p q : α → Bool} (h : ∀ (a : α), p a = q a) (wstart : start₁ = start₂) (wstop : stop₁ = stop₂) : xs.any p start₁ stop₁ = ys.any q start₂ stop₂

theorem Array.allM_congr {m : Type → Type u_1} {α : Type u_2} {start₁ start₂ stop₁ stop₂ : Nat} [Monad m] {xs ys : Array α} (w : xs = ys) {p q : α → m Bool} (h : ∀ (a : α), p a = q a) (wstart : start₁ = start₂) (wstop : stop₁ = stop₂) : allM p xs start₁ stop₁ = allM q ys start₂ stop₂

theorem Array.all_congr {α : Type u_1} {start₁ start₂ stop₁ stop₂ : Nat} {xs ys : Array α} (w : xs = ys) {p q : α → Bool} (h : ∀ (a : α), p a = q a) (wstart : start₁ = start₂) (wstop : stop₁ = stop₂) : xs.all p start₁ stop₁ = ys.all q start₂ stop₂

@[simp]

theorem Array.any_flatten' {α : Type u_1} {stop : Nat} {f : α → Bool} {xss : Array (Array α)} (w : stop = xss.flatten.size) : xss.flatten.any f 0 stop = xss.any fun (x : Array α) => x.any f

@[simp]

theorem Array.all_flatten' {α : Type u_1} {stop : Nat} {f : α → Bool} {xss : Array (Array α)} (w : stop = xss.flatten.size) : xss.flatten.all f 0 stop = xss.all fun (x : Array α) => x.all f

theorem Array.any_flatten {α : Type u_1} {f : α → Bool} {xss : Array (Array α)} : xss.flatten.any f = xss.any fun (x : Array α) => x.any f

theorem Array.all_flatten {α : Type u_1} {f : α → Bool} {xss : Array (Array α)} : xss.flatten.all f = xss.all fun (x : Array α) => x.all f

@[simp]

theorem Array.any_flatMap' {α : Type u_1} {β : Type u_2} {stop : Nat} {xs : Array α} {f : α → Array β} {p : β → Bool} (w : stop = (flatMap f xs).size) : (flatMap f xs).any p 0 stop = xs.any fun (a : α) => (f a).any p

Variant of any_flatMap with a side condition for the stop argument.

@[simp]

theorem Array.all_flatMap' {α : Type u_1} {β : Type u_2} {stop : Nat} {xs : Array α} {f : α → Array β} {p : β → Bool} (w : stop = (flatMap f xs).size) : (flatMap f xs).all p 0 stop = xs.all fun (a : α) => (f a).all p

Variant of all_flatMap with a side condition for the stop argument.

theorem Array.any_flatMap {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} {p : β → Bool} : (flatMap f xs).any p = xs.any fun (a : α) => (f a).any p

theorem Array.all_flatMap {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} {p : β → Bool} : (flatMap f xs).all p = xs.all fun (a : α) => (f a).all p

@[simp]

theorem Array.any_reverse' {α : Type u_1} {stop : Nat} {f : α → Bool} {xs : Array α} (w : stop = xs.size) : xs.reverse.any f 0 stop = xs.any f

Variant of any_reverse with a side condition for the stop argument.

@[simp]

theorem Array.all_reverse' {α : Type u_1} {stop : Nat} {f : α → Bool} {xs : Array α} (w : stop = xs.size) : xs.reverse.all f 0 stop = xs.all f

Variant of all_reverse with a side condition for the stop argument.

theorem Array.any_reverse {α : Type u_1} {f : α → Bool} {xs : Array α} : xs.reverse.any f = xs.any f

theorem Array.all_reverse {α : Type u_1} {f : α → Bool} {xs : Array α} : xs.reverse.all f = xs.all f

@[simp]

theorem Array.any_mkArray {α : Type u_1} {f : α → Bool} {n : Nat} {a : α} : (mkArray n a).any f = if n = 0 then false else f a

@[simp]

theorem Array.all_mkArray {α : Type u_1} {f : α → Bool} {n : Nat} {a : α} : (mkArray n a).all f = if n = 0 then true else f a

toListRev

@[inline]

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

A more efficient version of arr.toList.reverse; for verification purposes we immediately simplify it.

Equations

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

@[simp]

theorem Array.toListRev_eq {α : Type u_1} (xs : Array α) : xs.toListRev = xs.toList.reverse

appendList

@[simp]

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

@[simp]

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

Preliminaries about ofFn

@[simp, irreducible]

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

@[simp]

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

@[irreducible]

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, ⋯⟩) : (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 < (ofFn f).size) : (ofFn f)[i] = f ⟨i, ⋯⟩

theorem Array.getElem?_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) (i : Nat) : (ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none

Preliminaries about range and range'

@[simp]

theorem Array.size_range' {start size step : Nat} : (range' start size step).size = size

@[simp]

theorem Array.toList_range' {start size step : Nat} : (range' start size step).toList = List.range' start size step

@[simp]

theorem Array.getElem_range' {start size step i : Nat} (h : i < (range' start size step).size) : (range' start size step)[i] = start + step * i

theorem Array.getElem?_range' {start size step i : Nat} : (range' start size step)[i]? = if i < size then some (start + step * i) else none

@[simp]

theorem List.toArray_range' (start size step : Nat) : (range' start size step).toArray = Array.range' start size step

@[simp]

theorem Array.size_range {n : Nat} : (range n).size = n

@[simp]

theorem Array.toList_range (n : Nat) : (range n).toList = List.range n

@[simp]

theorem Array.getElem_range {n i : Nat} (h : i < (range n).size) : (range n)[i] = i

theorem Array.getElem?_range {n i : Nat} : (range n)[i]? = if i < n then some i else none

@[simp]

theorem List.toArray_range (n : Nat) : (range n).toArray = Array.range n

Content below this point has not yet been aligned with List.

sum

theorem Array.sum_eq_sum_toList {α : Type u_1} [Add α] [Zero α] (as : Array α) : as.toList.sum = as.sum

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

theorem Array.foldl_toList_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).toList = acc.toList ++ List.map G l

uset

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

get

@[simp]

theorem Array.getD_eq_getD_getElem? {α : Type u_1} (xs : Array α) (i : Nat) (d : α) : xs.getD i d = xs[i]?.getD d

theorem Array.getElem!_eq_getD {α : Type u_1} {i : Nat} [Inhabited α] (xs : Array α) : xs[i]! = xs.getD i default

mem

@[simp]

theorem Array.mem_toList {α : Type u_1} {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs

theorem Array.not_mem_nil {α : Type u_1} (a : α) : ¬a ∈ #[]

get lemmas

theorem Array.lt_of_getElem {α : Type u_1} {x : α} {xs : Array α} {i : Nat} {hidx : i < xs.size} : xs[i] = x → i < xs.size

theorem Array.getElem_fin_eq_getElem_toList {α : Type u_1} (xs : Array α) (i : Fin xs.size) : xs[i] = xs.toList[i]

@[simp]

theorem Array.ugetElem_eq_getElem {α : Type u_1} (xs : Array α) {i : USize} (h : i.toNat < xs.size) : xs[i] = xs[i.toNat]

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

theorem Array.getElem_mem_toList {α : Type u_1} (xs : Array α) (i : Nat) (h : i < xs.size) : xs[i] ∈ xs.toList

theorem Array.back!_eq_back? {α : Type u_1} [Inhabited α] (xs : Array α) : xs.back! = xs.back?.getD default

@[simp]

theorem Array.back?_push {α : Type u_1} {x : α} (xs : Array α) : (xs.push x).back? = some x

@[simp]

theorem Array.back!_push {α : Type u_1} {x : α} [Inhabited α] (xs : Array α) : (xs.push x).back! = x

theorem Array.getElem?_push_lt {α : Type u_1} (xs : Array α) (x : α) (i : Nat) (h : i < xs.size) : (xs.push x)[i]? = some xs[i]

theorem Array.getElem?_push_eq {α : Type u_1} (xs : Array α) (x : α) : (xs.push x)[xs.size]? = some x

@[simp]

theorem Array.getElem?_size {α : Type u_1} {xs : Array α} : xs[xs.size]? = none

forIn

@[simp]

theorem Array.forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (xs : Array α) (b : β) (f : α → β → m (ForInStep β)) : forIn xs.toList b f = forIn xs b f

@[simp]

theorem Array.forIn'_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (xs : Array α) (b : β) (f : (a : α) → a ∈ xs.toList → β → m (ForInStep β)) : forIn' xs.toList b f = forIn' xs b fun (a : α) (m : a ∈ xs) (b : β) => f a ⋯ b

contains

theorem Array.contains_def {α : Type u_1} [DecidableEq α] {a : α} {xs : Array α} : xs.contains a = true ↔ a ∈ xs

instance Array.instDecidableMemOfDecidableEq {α : Type u_1} [DecidableEq α] (a : α) (xs : Array α) : Decidable (a ∈ xs)

Equations

• Array.instDecidableMemOfDecidableEq a xs = decidable_of_iff (xs.contains a = true) ⋯

isPrefixOf

@[simp]

theorem Array.isPrefixOf_toList {α : Type u_1} [BEq α] {xs ys : Array α} : xs.toList.isPrefixOf ys.toList = xs.isPrefixOf ys

zipWith

@[simp]

theorem Array.toList_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (xs : Array α) (ys : Array β) : (zipWith f xs ys).toList = List.zipWith f xs.toList ys.toList

@[simp]

theorem Array.toList_zip {α : Type u_1} {β : Type u_2} (xs : Array α) (ys : Array β) : (xs.zip ys).toList = xs.toList.zip ys.toList

@[simp]

theorem Array.toList_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option α → Option β → γ) (xs : Array α) (ys : Array β) : (zipWithAll f xs ys).toList = List.zipWithAll f xs.toList ys.toList

@[simp]

theorem Array.size_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (xs : Array α) (ys : Array β) (f : α → β → γ) : (zipWith f xs ys).size = min xs.size ys.size

@[simp]

theorem Array.size_zip {α : Type u_1} {β : Type u_2} (xs : Array α) (ys : Array β) : (xs.zip ys).size = min xs.size ys.size

@[simp]

theorem Array.getElem_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (xs : Array α) (ys : Array β) (f : α → β → γ) (i : Nat) (hi : i < (zipWith f xs ys).size) : (zipWith f xs ys)[i] = f xs[i] ys[i]

findSomeM?, findM?, findSome?, find?

@[simp]

theorem Array.findSomeM?_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (p : α → m (Option β)) (xs : Array α) : List.findSomeM? p xs.toList = findSomeM? p xs

@[simp]

theorem Array.findM?_toList {m : Type → Type} {α : Type} [Monad m] [LawfulMonad m] (p : α → m Bool) (xs : Array α) : List.findM? p xs.toList = findM? p xs

@[simp]

theorem Array.findSome?_toList {α : Type u_1} {β : Type u_2} (p : α → Option β) (xs : Array α) : List.findSome? p xs.toList = findSome? p xs

@[simp]

theorem Array.find?_toList {α : Type u_1} (p : α → Bool) (xs : Array α) : List.find? p xs.toList = find? p xs

@[simp]

theorem Array.finIdxOf?_toList {α : Type u_1} [BEq α] (a : α) (xs : Array α) : List.finIdxOf? a xs.toList = Option.map (Fin.cast ⋯) (xs.finIdxOf? a)

@[simp]

theorem Array.findFinIdx?_toList {α : Type u_1} (p : α → Bool) (xs : Array α) : List.findFinIdx? p xs.toList = Option.map (Fin.cast ⋯) (findFinIdx? p xs)

More theorems about List.toArray, followed by an Array operation.

Our goal is to have simp "pull List.toArray outwards" as much as possible.

theorem List.toListRev_toArray {α : Type u_1} (l : List α) : l.toArray.toListRev = l.reverse

@[simp]

theorem List.take_toArray {α : Type u_1} (l : List α) (i : Nat) : l.toArray.take i = (take i l).toArray

@[simp]

theorem List.mapM_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) : Array.mapM f l.toArray = toArray <$> mapM f l

theorem List.uset_toArray {α : Type u_1} (l : List α) (i : USize) (a : α) (h : i.toNat < l.toArray.size) : l.toArray.uset i a h = (l.set i.toNat a).toArray

@[simp]

theorem List.modify_toArray {α : Type u_1} {i : Nat} (f : α → α) (l : List α) : l.toArray.modify i f = (modify f i l).toArray

@[simp]

theorem List.flatten_toArray {α : Type u_1} (L : List (List α)) : (Array.map toArray L.toArray).flatten = L.flatten.toArray

@[simp]

theorem Array.toList_takeWhile {α : Type u_1} (p : α → Bool) (as : Array α) : (takeWhile p as).toList = List.takeWhile p as.toList

@[simp]

theorem Array.toList_eraseIdx {α : Type u_1} (xs : Array α) (i : Nat) (h : i < xs.size) : (xs.eraseIdx i h).toList = xs.toList.eraseIdx i

@[simp]

theorem Array.toList_eraseIdxIfInBounds {α : Type u_1} (xs : Array α) (i : Nat) : (xs.eraseIdxIfInBounds i).toList = xs.toList.eraseIdx i

findSomeRevM?, findRevM?, findSomeRev?, findRev?

@[simp]

theorem Array.findSomeRevM?_eq_findSomeM?_reverse {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m (Option β)) (xs : Array α) : findSomeRevM? f xs = findSomeM? f xs.reverse

@[simp]

theorem Array.findRevM?_eq_findM?_reverse {m : Type → Type} {α : Type} [Monad m] [LawfulMonad m] (f : α → m Bool) (xs : Array α) : findRevM? f xs = findM? f xs.reverse

@[simp]

theorem Array.findSomeRev?_eq_findSome?_reverse {α : Type u_1} {β : Type u_2} (f : α → Option β) (xs : Array α) : findSomeRev? f xs = findSome? f xs.reverse

@[simp]

theorem Array.findRev?_eq_find?_reverse {α : Type} (f : α → Bool) (xs : Array α) : findRev? f xs = find? f xs.reverse

unzip

@[simp]

theorem Array.fst_unzip {α : Type u_1} {β : Type u_2} (xs : Array (α × β)) : xs.unzip.fst = map Prod.fst xs

@[simp]

theorem Array.snd_unzip {α : Type u_1} {β : Type u_2} (xs : Array (α × β)) : xs.unzip.snd = map Prod.snd xs

theorem Array.toList_fst_unzip {α : Type u_1} {β : Type u_2} (xs : Array (α × β)) : xs.unzip.fst.toList = xs.toList.unzip.fst

theorem Array.toList_snd_unzip {α : Type u_1} {β : Type u_2} (xs : Array (α × β)) : xs.unzip.snd.toList = xs.toList.unzip.snd

@[simp]

theorem List.unzip_toArray {α : Type u_1} {β : Type u_2} (as : List (α × β)) : as.toArray.unzip = Prod.map toArray toArray as.unzip

@[simp]

theorem List.firstM_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Alternative m] (as : List α) (f : α → m β) : Array.firstM f as.toArray = firstM f as

Deprecations

@[reducible, inline, deprecated List.setIfInBounds_toArray (since := "2024-11-24")]

abbrev List.setD_toArray {α : Type u_1} (l : List α) (i : Nat) (a : α) : l.toArray.setIfInBounds i a = (l.set i a).toArray

Equations

• @List.setD_toArray = @List.setIfInBounds_toArray

@[deprecated Array.size_toArray (since := "2024-12-11")]

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

@[deprecated Array.getElem?_eq_getElem (since := "2024-12-11")]

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

@[deprecated Array.getElem?_eq_none (since := "2024-12-11")]

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

@[simp, deprecated "`get?` is deprecated" (since := "2025-02-12")]

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

@[deprecated Array.getElem?_eq_none (since := "2024-12-11")]

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

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

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

Equations

• @Array.getD_get? = @Array.getD_getElem?

@[reducible, inline, deprecated Array.getD_eq_getD_getElem? (since := "2025-02-12")]

abbrev Array.getD_eq_get? {α : Type u_1} (xs : Array α) (i : Nat) (d : α) : xs.getD i d = xs[i]?.getD d

Equations

• @Array.getD_eq_get? = @Array.getD_eq_getD_getElem?

@[deprecated Array.getElem!_eq_getD (since := "2025-02-12")]

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

@[deprecated "Use `a[i]!` instead of `a.get! i`." (since := "2025-02-12")]

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

@[reducible, inline, deprecated Array.get!_eq_getD_getElem? (since := "2025-02-12")]

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

Equations

• @Array.get!_eq_getElem? = @Array.get!_eq_getD_getElem?

@[reducible, inline, deprecated Array.mem_of_back? (since := "2024-10-21")]

abbrev Array.mem_of_back?_eq_some {α : Type u_1} {xs : Array α} {a : α} (h : xs.back? = some a) : a ∈ xs

Equations

• @Array.mem_of_back?_eq_some = @Array.mem_of_back?

@[reducible, inline, deprecated Array.getElem?_size_le (since := "2024-10-21")]

abbrev Array.get?_len_le {α : Type u_1} (xs : Array α) (i : Nat) (h : xs.size ≤ i) : xs[i]? = none

Equations

• @Array.get?_len_le = @Array.getElem?_size_le

@[deprecated "`Array.get?` is deprecated, use `a[i]?` instead." (since := "2025-02-12")]

theorem Array.get?_eq_get?_toList {α : Type u_1} (xs : Array α) (i : Nat) : xs.get? i = xs.toList.get? i

@[reducible, inline, deprecated Array.get!_eq_getD_getElem? (since := "2025-02-12")]

abbrev Array.get!_eq_get? {α : Type u_1} [Inhabited α] (xs : Array α) (i : Nat) : xs.get! i = xs[i]?.getD default

Equations

• @Array.get!_eq_get? = @Array.get!_eq_getD_getElem?

@[reducible, inline, deprecated Array.getElem?_push_lt (since := "2024-10-21")]

abbrev Array.get?_push_lt {α : Type u_1} (xs : Array α) (x : α) (i : Nat) (h : i < xs.size) : (xs.push x)[i]? = some xs[i]

Equations

• @Array.get?_push_lt = @Array.getElem?_push_lt

@[reducible, inline, deprecated Array.getElem?_push_eq (since := "2024-10-21")]

abbrev Array.get?_push_eq {α : Type u_1} (xs : Array α) (x : α) : (xs.push x)[xs.size]? = some x

Equations

• @Array.get?_push_eq = @Array.getElem?_push_eq

@[reducible, inline, deprecated Array.getElem?_push (since := "2024-10-21")]

abbrev Array.get?_push {α : Type u_1} {i : Nat} {xs : Array α} {x : α} : (xs.push x)[i]? = if i = xs.size then some x else xs[i]?

Equations

• @Array.get?_push = @Array.getElem?_push

@[reducible, inline, deprecated Array.getElem?_size (since := "2024-10-21")]

abbrev Array.get?_size {α : Type u_1} {xs : Array α} : xs[xs.size]? = none

Equations

• @Array.get?_size = @Array.getElem?_size

@[deprecated Array.getElem_set_self (since := "2025-01-17")]

theorem Array.get_set_eq {α : Type u_1} (xs : Array α) (i : Nat) (v : α) (h : i < xs.size) : (xs.set i v h)[i] = v

@[reducible, inline, deprecated Array.foldl_toList_eq_flatMap (since := "2024-10-16")]

abbrev Array.foldl_toList_eq_bind {α : Type u_1} {β : Type u_2} (l : List α) (acc : Array β) (F : Array β → α → Array β) (G : α → List β) (H : ∀ (acc : Array β) (a : α), (F acc a).toList = acc.toList ++ G a) : (List.foldl F acc l).toList = acc.toList ++ List.flatMap G l

Equations

• @Array.foldl_toList_eq_bind = @Array.foldl_toList_eq_flatMap

@[reducible, inline, deprecated Array.foldl_toList_eq_flatMap (since := "2024-10-16")]

abbrev 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).toList = acc.toList ++ G a) : (List.foldl F acc l).toList = acc.toList ++ List.flatMap G l

Equations

• @Array.foldl_data_eq_bind = @Array.foldl_toList_eq_flatMap

@[reducible, inline, deprecated Array.getElem_mem (since := "2024-10-17")]

abbrev Array.getElem?_mem {α : Type u_1} {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs

Equations

• @Array.getElem?_mem = @Array.getElem_mem

@[reducible, inline, deprecated Array.getElem_fin_eq_getElem_toList (since := "2024-10-17")]

abbrev Array.getElem_fin_eq_toList_get {α : Type u_1} (xs : Array α) (i : Fin xs.size) : xs[i] = xs.toList[i]

Equations

• @Array.getElem_fin_eq_toList_get = @Array.getElem_fin_eq_getElem_toList

@[reducible, inline, deprecated "Use reverse direction of `getElem?_toList`" (since := "2024-10-17")]

abbrev Array.getElem?_eq_toList_getElem? {α : Type u_1} {xs : Array α} {i : Nat} : xs.toList[i]? = xs[i]?

Equations

• @Array.getElem?_eq_toList_getElem? = @Array.getElem?_toList

@[reducible, inline, deprecated Array.getElem?_swap (since := "2024-10-17")]

abbrev Array.get?_swap {α : Type u_1} (xs : Array α) (i j : Nat) (hi : i < xs.size) (hj : j < xs.size) (k : Nat) : (xs.swap i j hi hj)[k]? = if j = k then some xs[i] else if i = k then some xs[j] else xs[k]?

Equations

• @Array.get?_swap = @Array.getElem?_swap

@[reducible, inline, deprecated Array.getElem_push (since := "2024-10-21")]

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

Equations

• @Array.get_push = @Array.getElem_push

@[reducible, inline, deprecated Array.getElem_push_lt (since := "2024-10-21")]

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

Equations

• @Array.get_push_lt = @Array.getElem_push_lt

@[reducible, inline, deprecated Array.getElem_push_eq (since := "2024-10-21")]

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

Equations

• @Array.get_push_eq = @Array.getElem_push_eq

@[reducible, inline, deprecated Array.back!_eq_back? (since := "2024-10-31")]

abbrev Array.back_eq_back? {α : Type u_1} [Inhabited α] (xs : Array α) : xs.back! = xs.back?.getD default

Equations

• @Array.back_eq_back? = @Array.back!_eq_back?

@[reducible, inline, deprecated Array.back!_push (since := "2024-10-31")]

abbrev Array.back_push {α : Type u_1} {x : α} [Inhabited α] (xs : Array α) : (xs.push x).back! = x

Equations

• @Array.back_push = @Array.back!_push

@[reducible, inline, deprecated Array.eq_push_pop_back!_of_size_ne_zero (since := "2024-10-31")]

abbrev Array.eq_push_pop_back_of_size_ne_zero {α : Type u_1} [Inhabited α] {xs : Array α} (h : xs.size ≠ 0) : xs = xs.pop.push xs.back!

Equations

• @Array.eq_push_pop_back_of_size_ne_zero = @Array.eq_push_pop_back!_of_size_ne_zero

@[reducible, inline, deprecated Array.set!_is_setIfInBounds (since := "2024-11-24")]

abbrev Array.set_is_setIfInBounds : @set! = @setIfInBounds

Equations

• Array.set_is_setIfInBounds = Array.set!_eq_setIfInBounds

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

abbrev Array.size_setD {α : Type u_1} (xs : Array α) (i : Nat) (a : α) : (xs.setIfInBounds i a).size = xs.size

Equations

• @Array.size_setD = @Array.size_setIfInBounds

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

abbrev Array.getElem_setD_eq {α : Type u_1} (xs : Array α) {i : Nat} (a : α) (h : i < (xs.setIfInBounds i a).size) : (xs.setIfInBounds i a)[i] = a

Equations

• @Array.getElem_setD_eq = @Array.getElem_setIfInBounds_self

@[reducible, inline, deprecated Array.getElem?_setIfInBounds_eq (since := "2024-11-24")]

abbrev Array.get?_setD_eq {α : Type u_1} (xs : Array α) {i : Nat} (a : α) : (xs.setIfInBounds i a)[i]? = if i < xs.size then some a else none

Equations

• @Array.get?_setD_eq = @Array.getElem?_setIfInBounds_self

@[reducible, inline, deprecated Array.getD_get?_setIfInBounds (since := "2024-11-24")]

abbrev Array.getD_setD {α : Type u_1} (xs : Array α) (i : Nat) (v d : α) : (xs.setIfInBounds i v)[i]?.getD d = if i < xs.size then v else d

Equations

• @Array.getD_setD = @Array.getD_get?_setIfInBounds

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

abbrev Array.getElem_setD {α : Type u_1} (xs : Array α) (i : Nat) (a : α) (j : Nat) (hj : j < xs.size) : (xs.setIfInBounds i a)[j] = if i = j then a else xs[j]

Equations

• @Array.getElem_setD = @Array.getElem_setIfInBounds

@[deprecated List.getElem_toArray (since := "2024-11-29")]

theorem Array.getElem_mk {α : Type u_1} {xs : List α} {i : Nat} (h : i < xs.length) : { toList := xs }[i] = xs[i]

@[deprecated Array.getElem_toList (since := "2024-12-08")]

theorem Array.getElem_eq_getElem_toList {α : Type u_1} {i : Nat} {xs : Array α} (h : i < xs.size) : xs[i] = xs.toList[i]

@[deprecated Array.getElem?_toList (since := "2024-12-08")]

theorem Array.getElem?_eq_getElem?_toList {α : Type u_1} (xs : Array α) (i : Nat) : xs[i]? = xs.toList[i]?

@[deprecated LawfulGetElem.getElem?_def (since := "2024-12-08")]

theorem Array.getElem?_eq {α : Type u_1} {xs : Array α} {i : Nat} : xs[i]? = if h : i < xs.size then some xs[i] else none

map

@[deprecated "Use `toList_map` or `List.map_toArray` to characterize `Array.map`." (since := "2025-01-06")]

theorem Array.map_induction {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → β) (motive : Nat → Prop) (h0 : motive 0) (p : Fin xs.size → β → Prop) (hs : ∀ (i : Fin xs.size), motive ↑i → p i (f xs[i]) ∧ motive (↑i + 1)) : motive xs.size ∧ ∃ (eq : (map f xs).size = xs.size), ∀ (i : Nat) (h : i < xs.size), p ⟨i, h⟩ (map f xs)[i]

@[deprecated "Use `toList_map` or `List.map_toArray` to characterize `Array.map`." (since := "2025-01-06")]

theorem Array.map_spec {α : Type u_1} {β : Type u_2} (xs : Array α) (f : α → β) (p : Fin xs.size → β → Prop) (hs : ∀ (i : Fin xs.size), p i (f xs[i])) : ∃ (eq : (map f xs).size = xs.size), ∀ (i : Nat) (h : i < xs.size), p ⟨i, h⟩ (map f xs)[i]

set

@[reducible, inline, deprecated Array.getElem?_set_eq (since := "2025-02-27")]

abbrev Array.get?_set_eq {α : Type u_1} (xs : Array α) (i : Nat) (h : i < xs.size) (v : α) : (xs.set i v h)[i]? = some v

Equations

• @Array.get?_set_eq = @Array.getElem?_set_self

@[reducible, inline, deprecated Array.getElem?_set_ne (since := "2025-02-27")]

abbrev Array.get?_set_ne {α : Type u_1} (xs : Array α) (i : Nat) (h : i < xs.size) {j : Nat} (v : α) (ne : i ≠ j) : (xs.set i v h)[j]? = xs[j]?

Equations

• @Array.get?_set_ne = @Array.getElem?_set_ne

@[reducible, inline, deprecated Array.getElem?_set (since := "2025-02-27")]

abbrev Array.get?_set {α : Type u_1} (xs : Array α) (i : Nat) (h : i < xs.size) (v : α) (j : Nat) : (xs.set i v h)[j]? = if i = j then some v else xs[j]?

Equations

• @Array.get?_set = @Array.getElem?_set

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

abbrev Array.get_set {α : Type u_1} (xs : Array α) (i : Nat) (h' : i < xs.size) (v : α) (j : Nat) (h : j < (xs.set i v h').size) : (xs.set i v h')[j] = if i = j then v else xs[j]

Equations

• @Array.get_set = @Array.getElem_set

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

abbrev Array.get_set_ne {α : Type u_1} (xs : Array α) (i : Nat) (h' : i < xs.size) (v : α) {j : Nat} (pj : j < xs.size) (h : i ≠ j) : (xs.set i v h')[j] = xs[j]

Equations

• @Array.get_set_ne = @Array.getElem_set_ne