Theorems about Array.

Preliminaries

toList

@[simp]

theorem Array.toList_inj {α : Type u_1} {a b : Array α} : a.toList = b.toList ↔ a = b

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Array.toArray_eq {α✝ : Type u_1} {a : List α✝} {v : Array α✝} : a.toArray = v ↔ a = v.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} {l : Array α✝} (h : l.size = 0) : l = #[]

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

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

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

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

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

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

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

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

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

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.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

L[i] and L[i]?

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

theorem Array.getElem?_push_size {α : Type u_1} {a : Array α} {x : α} : (a.push x)[a.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} {l₁ l₂ : Array α} (h : ∀ (i : Nat), l₁[i]? = l₂[i]?) : l₁ = l₂

mem

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

@[simp]

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

theorem Array.mem_push_self {α : Type u_1} {a : Array α} {x : α} : x ∈ a.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} {a : Array α} {x : α} (y : α) (h : x ∈ a) : x ∈ a.push y

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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 : α} {l : Array α} : (∀ (a' : α), a' ∈ l → ¬a = a') ↔ ¬a ∈ l

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

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 : α} {l : Array α} : a ∈ l.push b → b ∈ l → a ∈ l

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

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

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

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

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

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

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

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

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

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

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

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

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

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

isEmpty

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

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} {l : Array α} : l.all p = true ↔ ∀ (x : α), x ∈ l → 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 : α} {l : Array α} : elem a l = l.contains a

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

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

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

@[simp]

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

@[simp]

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

Variant of any_push with a side condition on stop.

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

@[simp]

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

Variant of all_push with a side condition on stop.

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

@[simp]

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

set

@[simp]

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

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

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

Equations

• @Array.getElem_set_eq = @Array.getElem_set_self

@[simp]

theorem Array.getElem?_set_self {α : Type u_1} (a : Array α) (i : Nat) (h : i < a.size) (v : α) : (a.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} (a : Array α) (i : Nat) (h : i < a.size) (v : α) : (a.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} (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat} (pj : j < (a.set i v h').size) (h : i ≠ j) : (a.set i v h')[j] = a[j]

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

theorem Array.mem_or_eq_of_mem_set {α : Type u_1} {as : Array α} {i : Nat} {a b : α} {w : i < as.size} (h : a ∈ as.set i b w) : a ∈ as ∨ 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} (as : Array α) (index : Nat) (val : α) : (as.setIfInBounds index val).size = as.size

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

@[simp]

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

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

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

Equations

• @Array.getElem_setIfInBounds_eq = @Array.getElem_setIfInBounds_self

@[simp]

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

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

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

@[simp]

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

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

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

Equations

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

Simplifies a normal form from get!

@[simp]

theorem Array.toList_setIfInBounds {α : Type u_1} (a : Array α) (i : Nat) (x : α) : (a.setIfInBounds i x).toList = a.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 : α} {v w : Array α} : (v.push a == w.push b) = (v == w && 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 α] {l₁ l₂ : Array α} : ((l₁.isEqv l₂ fun (x1 x2 : α) => x1 == x2) = true) = (l₁ = l₂)

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 β) (arr : Array α) : mapM f arr = foldlM (fun (bs : Array β) (a : α) => bs.push <$> f a) #[] arr

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

@[simp]

theorem Array.toList_map {α : Type u_1} {β : Type u_2} (f : α → β) (arr : Array α) : (map f arr).toList = List.map f arr.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 : α → β) (arr : Array α) : (map f arr).size = arr.size

@[simp]

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

@[simp]

theorem Array.getElem?_map {α : Type u_1} {β : Type u_2} (f : α → β) (as : Array α) (i : Nat) : (map f as)[i]? = Option.map f as[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} (l : Array α) : map id l = l

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

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) (l : Array α) : map f l = l

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 : α → β} {l : Array α} : b ∈ map f l ↔ ∃ (a : α), a ∈ l ∧ 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 : α → β} {l : Array α} {P : β → Prop} : (∀ (i : β), i ∈ map f l → P i) ↔ ∀ (j : α), j ∈ l → P (f j)

@[simp]

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

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

@[simp]

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

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

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

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 : α → β} {l : Array α} {l₂ : Array β} {b : β} : map f l = l₂.push b ↔ ∃ (l₁ : Array α), ∃ (a : α), l = l₁.push a ∧ map f l₁ = l₂ ∧ f a = b

@[simp]

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

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

theorem Array.map_eq_iff {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → α✝¹} {l : Array α✝} {l' : Array α✝¹} : map f l = l' ↔ ∀ (i : Nat), l'[i]? = Option.map f l[i]?

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Array.back?_map {α : Type u_1} {β : Type u_2} {f : α → β} {l : Array α} : (map f l).back? = Option.map f l.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 β) (arr : Array α) : mapM f arr = List.toArray <$> List.mapM f arr.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 β) (arr : Array α) : toList <$> mapM f arr = List.mapM f arr.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 (r : Array β) (a : α) => r.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) (ass : Array (Array α)) : P ass

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) (ass : Array (Array (Array α))) : P ass

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} {as bs : Array α} (h : as = bs) {f g : α → Bool} (h' : f = g) {start stop start' stop' : Nat} (h₁ : start = start') (h₂ : stop = stop') : filter f as start stop = filter g bs start' stop'

@[simp]

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

theorem Array.toList_filter {α : Type u_1} (p : α → Bool) (l : Array α) : (filter p l).toList = List.filter p l.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 : α} {l : Array α} (h : p a = true) (w : stop = l.size + 1) : filter p (l.push a) 0 stop = (filter p l).push a

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

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

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

@[simp]

theorem Array.filter_append {α : Type u_1} {p : α → Bool} (l₁ l₂ : Array α) : filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂

theorem Array.filter_eq_append_iff {α : Type u_1} {l L₁ L₂ : Array α} {p : α → Bool} : filter p l = L₁ ++ L₂ ↔ ∃ (l₁ : Array α), ∃ (l₂ : Array α), l = l₁ ++ l₂ ∧ filter p l₁ = L₁ ∧ filter p l₂ = L₂

theorem Array.filter_eq_push_iff {α : Type u_1} {p : α → Bool} {l l' : Array α} {a : α} : filter p l = l'.push a ↔ ∃ (l₁ : Array α), ∃ (l₂ : Array α), l = l₁.push a ++ l₂ ∧ filter p l₁ = l' ∧ p a = true ∧ ∀ (x : α), x ∈ l₂ → ¬p x = true

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

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 β) (l : Array α) (w : stop = l.size) : (filterMap f l 0 stop).toList = List.filterMap f l.toList

theorem Array.toList_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : Array α) : (filterMap f l).toList = List.filterMap f l.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 : α} {l : Array α} (h : f a = none) (w : stop = l.size + 1) : filterMap f (l.push a) 0 stop = filterMap f l

@[simp]

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

@[simp]

theorem Array.filterMap_eq_map {α : Type u_1} {β : Type u_2} (f : α → β) : (fun (as : Array α) => filterMap (some ∘ f) as) = map f

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

theorem Array.filterMap_append {α : Type u_1} {β : Type u_2} (l l' : Array α) (f : α → Option β) : filterMap f (l ++ l') = filterMap f l ++ filterMap f l'

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

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 α✝¹} {l : Array α✝} : filterMap f l = #[] ↔ ∀ (a : α✝), a ∈ l → f a = none

theorem Array.filterMap_eq_push_iff {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : Array α} {l' : Array β} {b : β} : filterMap f l = l'.push b ↔ ∃ (l₁ : Array α), ∃ (a : α), ∃ (l₂ : Array α), l = l₁.push a ++ l₂ ∧ filterMap f l₁ = l' ∧ f a = some b ∧ ∀ (x : α), x ∈ l₂ → 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} (as bs : Array α) : (as ++ bs).size = as.size + bs.size

@[simp]

theorem Array.append_push {α : Type u_1} {as bs : Array α} {a : α} : as ++ bs.push a = (as ++ bs).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} {as bs : Array α} {xs : List α} : as ++ bs = xs.toArray ↔ as.toList ++ bs.toList = xs

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 : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t

theorem Array.mem_append_left {α : Type u_1} {a : α} {l₁ : Array α} (l₂ : Array α) (h : a ∈ l₁) : a ∈ l₁ ++ l₂

theorem Array.mem_append_right {α : Type u_1} {a : α} (l₁ : Array α) {l₂ : Array α} (h : a ∈ l₂) : a ∈ l₁ ++ l₂

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

theorem Array.append_of_mem {α : Type u_1} {a : α} {l : Array α} (h : a ∈ l) : ∃ (s : Array α), ∃ (t : Array α), l = s.push a ++ t

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 : α} {l : Array α} : a ∈ l ↔ ∃ (s : Array α), ∃ (t : Array α), l = s.push a ++ t

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

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

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

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

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

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

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

theorem Array.getElem_append_left' {α : Type u_1} (l₂ : Array α) {l₁ : Array α} {i : Nat} (hi : i < l₁.size) : l₁[i] = (l₁ ++ l₂)[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} (l₁ : Array α) {l₂ : Array α} {i : Nat} (hi : i < l₂.size) : l₂[i] = (l₁ ++ l₂)[i + l₁.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} {l l₁ l₂ : Array α} (eq : l = l₁.push a ++ l₂) (h : l₁.size = i) : l[i] = a

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Array.append_eq_empty_iff {α✝ : Type u_1} {p q : Array α✝} : p ++ q = #[] ↔ p = #[] ∧ q = #[]

@[simp]

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

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

theorem Array.append_ne_empty_of_right_ne_empty {α : Type u_1} {t : Array α} (s : Array α) : t ≠ #[] → s ++ t ≠ #[]

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

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

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

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

theorem Array.append_eq_append_iff {α : Type u_1} {a b c d : Array α} : a ++ b = c ++ d ↔ (∃ (a' : Array α), c = a ++ a' ∧ b = a' ++ d) ∨ ∃ (c' : Array α), a = c ++ c' ∧ d = c' ++ b

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

theorem Array.filterMap_eq_append_iff {α : Type u_1} {β : Type u_2} {l : Array α} {L₁ L₂ : Array β} {f : α → Option β} : filterMap f l = L₁ ++ L₂ ↔ ∃ (l₁ : Array α), ∃ (l₂ : Array α), l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

theorem Array.append_eq_filterMap_iff {α : Type u_1} {β : Type u_2} {L₁ L₂ : Array β} {l : Array α} {f : α → Option β} : L₁ ++ L₂ = filterMap f l ↔ ∃ (l₁ : Array α), ∃ (l₂ : Array α), l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

@[simp]

theorem Array.map_append {α : Type u_1} {β : Type u_2} (f : α → β) (l₁ l₂ : Array α) : map f (l₁ ++ l₂) = map f l₁ ++ map f l₂

theorem Array.map_eq_append_iff {α : Type u_1} {β : Type u_2} {l : Array α} {L₁ L₂ : Array β} {f : α → β} : map f l = L₁ ++ L₂ ↔ ∃ (l₁ : Array α), ∃ (l₂ : Array α), l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

theorem Array.append_eq_map_iff {α : Type u_1} {β : Type u_2} {L₁ L₂ : Array β} {l : Array α} {f : α → β} : L₁ ++ L₂ = map f l ↔ ∃ (l₁ : Array α), ∃ (l₂ : Array α), l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

flatten

@[simp]

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

@[simp]

theorem Array.toList_flatten {α : Type u_1} {l : Array (Array α)} : l.flatten.toList = (List.map toList l.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

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} (L : Array (Array α)) : L.flatten.size = (map size L).sum

@[simp]

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

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

@[simp]

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

@[simp]

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

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

theorem Array.exists_of_mem_flatten {α✝ : Type u_1} {L : Array (Array α✝)} {a : α✝} : a ∈ L.flatten → ∃ (l : Array α✝), l ∈ L ∧ a ∈ l

theorem Array.mem_flatten_of_mem {α✝ : Type u_1} {L : Array (Array α✝)} {l : Array α✝} {a : α✝} (lL : l ∈ L) (al : a ∈ l) : a ∈ L.flatten

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

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

@[simp]

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

@[simp]

theorem Array.filterMap_flatten {α : Type u_1} {β : Type u_2} (f : α → Option β) (L : Array (Array α)) : filterMap f L.flatten = (map (fun (as : Array α) => filterMap f as) L).flatten

@[simp]

theorem Array.filter_flatten {α : Type u_1} (p : α → Bool) (L : Array (Array α)) : filter p L.flatten = (map (fun (as : Array α) => filter p as) L).flatten

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

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

@[simp]

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

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

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

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

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

theorem Array.eq_iff_flatten_eq {α : Type u_1} {L L' : Array (Array α)} : L = L' ↔ L.flatten = L'.flatten ∧ map size L = map size L'

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

flatMap

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

theorem Array.forall_mem_flatMap {β : Type u_1} {α : Type u_2} {p : β → Prop} {l : Array α} {f : α → Array β} : (∀ (x : β), x ∈ flatMap f l → p x) ↔ ∀ (a : α), a ∈ l → ∀ (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} (l : Array α) : flatMap (fun (x : α) => #[x]) l = l

@[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} (l : Array α) (f : α → Array β) (g : β → Array γ) : flatMap g (flatMap f l) = flatMap (fun (x : α) => flatMap g (f x)) l

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

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

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

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

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

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

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 m : Nat} (h : m < n) : (mkArray n a)[m]? = 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 : α} {l : Array α} (h : ∀ (b : α), b ∈ l → b = a) : l = mkArray l.size a

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

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

@[simp]

theorem Array.map_const {α : Type u_1} {β : Type u_2} (l : Array α) (b : β) : map (Function.const α b) l = mkArray l.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} (l : Array α) (b : β) : map (fun (x : α) => b) l = mkArray l.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} {l₁ l₂ : Array α} {a : α} : l₁ ++ l₂ = mkArray n a ↔ l₁.size + l₂.size = n ∧ l₁ = mkArray l₁.size a ∧ l₂ = mkArray l₂.size a

theorem Array.mkArray_eq_append_iff {α : Type u_1} {n : Nat} {l₁ l₂ : Array α} {a : α} : mkArray n a = l₁ ++ l₂ ↔ l₁.size + l₂.size = n ∧ l₁ = mkArray l₁.size a ∧ l₂ = mkArray l₂.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} (a : Array α) (i j : Nat) (hi : i < a.size) (hj : j < a.size) (k : Nat) : (a.swap i j hi hj)[k]? = if j = k then some a[i] else if i = k then some a[j] else a[k]?

reverse

@[simp]

theorem Array.size_reverse {α : Type u_1} (a : Array α) : a.reverse.size = a.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} (a : Array α) : a.reverse.toList = a.toList.reverse

@[irreducible]

theorem Array.toList_reverse.go {α : Type u_1} (a as : Array α) (i j : Nat) (hj : j < as.size) (h : i + j + 1 = a.size) (h₂ : as.size = a.size) (H : ∀ (k : Nat), as.toList[k]? = if i ≤ k ∧ k ≤ j then a.toList[k]? else a.toList.reverse[k]?) (k : Nat) : (reverse.loop as i ⟨j, hj⟩).toList[k]? = a.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} (as : Array α) (a : α) : (as.push a).reverse = #[a] ++ as.reverse

@[simp]

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

@[simp]

theorem Array.getElem_reverse {α : Type u_1} (as : Array α) (i : Nat) (hi : i < as.reverse.size) : as.reverse[i] = as[as.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 ≠ #[]

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

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

@[simp]

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

@[simp]

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

theorem Array.reverse_eq_iff {α : Type u_1} {as bs : Array α} : as.reverse = bs ↔ as = bs.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 : α → β) (l : Array α) : map f l.reverse = (map f l).reverse

@[simp]

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

@[simp]

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

@[simp]

theorem Array.reverse_append {α : Type u_1} (as bs : Array α) : (as ++ bs).reverse = bs.reverse ++ as.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} (L : Array (Array α)) : L.flatten.reverse = (map reverse L).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} (L : Array (Array α)) : L.reverse.flatten = (map reverse L).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} (l : Array α) (f : α → Array β) : (flatMap f l).reverse = flatMap (reverse ∘ f) l.reverse

theorem Array.flatMap_reverse {α : Type u_1} {β : Type u_2} (l : Array α) (f : α → Array β) : flatMap f l.reverse = (flatMap (reverse ∘ f) l).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} (as bs : Array α) (start : Nat) : extract.loop as 0 start bs = bs

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

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

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

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

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

@[simp]

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

Equations

• @Array.extract_all = @Array.extract_size

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

theorem Array.extract_empty_of_size_le_start {α : Type u_1} (as : Array α) {start stop : Nat} (h : as.size ≤ start) : as.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

foldlM and foldrM

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

theorem Array.foldrM_start_stop {α : Type u_1} {β : Type u_2} {m : Type u_2 → Type u_3} [Monad m] (l : Array α) (f : α → β → m β) (b : β) (start stop : Nat) : foldrM f b l start stop = foldrM f b (l.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 : β} {l l' : Array α} (w : l = l') (h : ∀ (x : β) (y : α), f x y = g x y) (hstart : start = start') (hstop : stop = stop') : foldlM f b l start stop = foldlM g b l' 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 : β} {l l' : Array α} (w : l = l') (h : ∀ (x : α) (y : β), f x y = g x y) (hstart : start = start') (hstop : stop = stop') : foldrM f b l start stop = foldrM g b l' 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 : β) (l l' : Array α) (w : stop = l.size + l'.size) : foldlM f b (l ++ l') 0 stop = do let init ← foldlM f b l foldlM f init l'

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 : β) (l l' : Array α) : foldlM f b (l ++ l') = do let init ← foldlM f b l foldlM f init l'

@[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] (l : Array α) (a : α) (f : β → α → m β) (b : β) (w : stop = l.size + 1) : foldlM f b (l.push a) 0 stop = do let b ← foldlM f b l 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] (l : Array α) (a : α) (f : β → α → m β) (b : β) : foldlM f b (l.push a) = do let b ← foldlM f b l f b a

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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] (l : Array α) (f : α → β → m β) (b : β) (w : start = l.size) : foldrM f b l.reverse start = foldlM (fun (x : β) (y : α) => f y x) b l

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] (l : Array α) (f : β → α → m β) (b : β) : foldlM f b l.reverse = foldrM (fun (x : α) (y : β) => f y x) b l

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

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

@[simp]

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

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 : β) (arr : Array α) (a : α) : foldr f init (arr.push a) = foldr f (f a init) arr

@[simp]

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

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} (l l' : Array α) : foldl push l' l = l' ++ l

@[simp]

theorem Array.foldr_flip_push_eq_append {α : Type u_1} (l l' : Array α) : foldr (fun (x : α) (y : Array α) => y.push x) l' l = l' ++ l.reverse

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

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

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

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

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

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

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

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

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

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

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

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

@[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 : β) (l l' : Array α) (w : start = l.size + l'.size) : foldrM f b (l ++ l') start = do let init ← foldrM f b l' foldrM f init l

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 : β) (l l' : Array α) : foldrM f b (l ++ l') = do let init ← foldrM f b l' foldrM f init l

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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} (l : Array α) (f : α → β → β) (b : β) (w : start = l.size) : foldr f b l.reverse start = foldl (fun (x : β) (y : α) => f y x) b l

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

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

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

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

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

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

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

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

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

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

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} {l : Array α} {f g : α → β → β} {a b : β} (r : β → β → Prop) (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) : r (foldr (fun (a : α) (acc : β) => f a acc) a l) (foldr (fun (a : α) (acc : β) => g a acc) b l)

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} (l : Array α) (a b : Nat) : foldl (fun (x : Nat) (x_1 : α) => x + a) b l = b + a * l.size

@[simp]

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

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

@[simp]

theorem Array.toArray_toList {α : Type u_1} (a : Array α) : a.toList.toArray = a

@[deprecated Array.size_toArray (since := "2024-12-11")]

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

@[inline]

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

A more efficient version of arr.toList.reverse.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Array.foldl_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} (a : Array α) (v : α) (i : USize) (h : i.toNat < a.size) : (a.uset i v h).size = a.size

get

@[deprecated Array.getElem?_eq_getElem (since := "2024-12-11")]

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

@[deprecated Array.getElem?_eq_none (since := "2024-12-11")]

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

@[simp]

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

@[deprecated Array.getElem?_eq_none (since := "2024-12-11")]

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

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

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

Equations

• @Array.getD_get? = @Array.getD_getElem?

@[simp]

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

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

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

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

@[simp]

theorem Array.ofFn_zero {α : Type u_1} (f : Fin 0 → α) : ofFn f = #[]

theorem Array.ofFn_succ {n : Nat} {α : Type u_1} (f : Fin (n + 1) → α) : ofFn f = (ofFn fun (i : Fin n) => f i.castSucc).push (f ⟨n, ⋯⟩)

mem

@[simp]

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

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

get lemmas

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

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

@[simp]

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

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

@[reducible, inline, deprecated Array.getElem?_size_le (since := "2024-10-21")]

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

Equations

• @Array.get?_len_le = @Array.getElem?_size_le

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

theorem Array.get?_eq_get?_toList {α : Type u_1} (a : Array α) (i : Nat) : a.get? i = a.toList.get? i

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

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

@[simp]

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

@[simp]

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

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

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

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

@[reducible, inline, deprecated Array.getElem?_push_lt (since := "2024-10-21")]

abbrev Array.get?_push_lt {α : Type u_1} (a : Array α) (x : α) (i : Nat) (h : i < a.size) : (a.push x)[i]? = some a[i]

Equations

• @Array.get?_push_lt = @Array.getElem?_push_lt

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

@[reducible, inline, deprecated Array.getElem?_push_eq (since := "2024-10-21")]

abbrev Array.get?_push_eq {α : Type u_1} (a : Array α) (x : α) : (a.push x)[a.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} {a : Array α} {x : α} : (a.push x)[i]? = if i = a.size then some x else a[i]?

Equations

• @Array.get?_push = @Array.getElem?_push

@[simp]

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

@[reducible, inline, deprecated Array.getElem?_size (since := "2024-10-21")]

abbrev Array.get?_size {α : Type u_1} {a : Array α} : a[a.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} (a : Array α) (i : Nat) (v : α) (h : i < a.size) : (a.set i v h)[i] = v

theorem Array.get?_set_eq {α : Type u_1} (a : Array α) (i : Nat) (v : α) (h : i < a.size) : (a.set i v h)[i]? = some v

@[simp]

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

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

theorem Array.get_set {α : Type u_1} (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a.size) (v : α) : (a.set i v hi)[j] = if i = j then v else a[j]

@[simp]

theorem Array.get_set_ne {α : Type u_1} (a : Array α) (i : Nat) (hi : i < a.size) {j : Nat} (v : α) (hj : j < a.size) (h : i ≠ j) : (a.set i v hi)[j] = a[j]

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem Array.size_eq_length_toList {α : Type u_1} (as : Array α) : as.size = as.toList.length

@[simp]

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

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

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

Equations

• @Array.size_swap! = @Array.size_swapIfInBounds

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

shrink

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

forIn

@[simp]

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

@[simp]

theorem Array.forIn'_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (as : Array α) (b : β) (f : (a : α) → a ∈ as.toList → β → m (ForInStep β)) : forIn' as.toList b f = forIn' as b fun (a : α) (m : a ∈ as) (b : β) => f a ⋯ b

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} (as : Array α) (f : α → β) (motive : Nat → Prop) (h0 : motive 0) (p : Fin as.size → β → Prop) (hs : ∀ (i : Fin as.size), motive ↑i → p i (f as[i]) ∧ motive (↑i + 1)) : motive as.size ∧ ∃ (eq : (map f as).size = as.size), ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ (map f as)[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} (as : Array α) (f : α → β) (p : Fin as.size → β → Prop) (hs : ∀ (i : Fin as.size), p i (f as[i])) : ∃ (eq : (map f as).size = as.size), ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ (map f as)[i]

modify

@[simp]

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

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

@[simp]

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

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

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

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

contains

theorem Array.contains_def {α : Type u_1} [DecidableEq α] {a : α} {as : Array α} : as.contains a = true ↔ a ∈ as

instance Array.instDecidableMemOfDecidableEq {α : Type u_1} [DecidableEq α] (a : α) (as : Array α) : Decidable (a ∈ as)

Equations

• Array.instDecidableMemOfDecidableEq a as = decidable_of_iff (as.contains a = true) ⋯

swap

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

eraseIdx

theorem Array.eraseIdx_eq_eraseIdxIfInBounds {α : Type u_1} {a : Array α} {i : Nat} (h : i < a.size) : a.eraseIdx i h = a.eraseIdxIfInBounds i

isPrefixOf

@[simp]

theorem Array.isPrefixOf_toList {α : Type u_1} [BEq α] {as bs : Array α} : as.toList.isPrefixOf bs.toList = as.isPrefixOf bs

zipWith

@[simp]

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

@[simp]

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

@[simp]

theorem Array.toList_zipWithAll {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : Option α → Option β → γ) (as : Array α) (bs : Array β) : (zipWithAll f as bs).toList = List.zipWithAll f as.toList bs.toList

@[simp]

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

@[simp]

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

@[simp]

theorem Array.getElem_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (as : Array α) (bs : Array β) (f : α → β → γ) (i : Nat) (hi : i < (zipWith f as bs).size) : (zipWith f as bs)[i] = f as[i] bs[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 β)) (as : Array α) : List.findSomeM? p as.toList = findSomeM? p as

@[simp]

theorem Array.findM?_toList {m : Type → Type} {α : Type} [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) : List.findM? p as.toList = findM? p as

@[simp]

theorem Array.findSome?_toList {α : Type u_1} {β : Type u_2} (p : α → Option β) (as : Array α) : List.findSome? p as.toList = findSome? p as

@[simp]

theorem Array.find?_toList {α : Type u_1} (p : α → Bool) (as : Array α) : List.find? p as.toList = find? p as

@[simp]

theorem Array.finIdxOf?_toList {α : Type u_1} [BEq α] (a : α) (v : Array α) : List.finIdxOf? a v.toList = Option.map (Fin.cast ⋯) (v.finIdxOf? a)

@[simp]

theorem Array.findFinIdx?_toList {α : Type u_1} (p : α → Bool) (v : Array α) : List.findFinIdx? p v.toList = Option.map (Fin.cast ⋯) (findFinIdx? p v)

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 α) (n : Nat) : l.toArray.take n = (take n 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 List.toArray_range (n : Nat) : (range n).toArray = Array.range n

@[simp]

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

@[simp]

theorem List.toArray_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) : (ofFn f).toArray = Array.ofFn f

@[simp]

theorem Array.mapM_id {α : Type u_1} {β : Type u_2} {l : Array α} {f : α → Id β} : mapM f l = map f l

@[simp]

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

@[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} (as : Array α) (i : Nat) (h : i < as.size) : (as.eraseIdx i h).toList = as.toList.eraseIdx i

@[simp]

theorem Array.toList_eraseIdxIfInBounds {α : Type u_1} (as : Array α) (i : Nat) : (as.eraseIdxIfInBounds i).toList = as.toList.eraseIdx i

flatten

@[simp]

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

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 β)) (as : Array α) : findSomeRevM? f as = findSomeM? f as.reverse

@[simp]

theorem Array.findRevM?_eq_findM?_reverse {m : Type → Type} {α : Type} [Monad m] [LawfulMonad m] (f : α → m Bool) (as : Array α) : findRevM? f as = findM? f as.reverse

@[simp]

theorem Array.findSomeRev?_eq_findSome?_reverse {α : Type u_1} {β : Type u_2} (f : α → Option β) (as : Array α) : findSomeRev? f as = findSome? f as.reverse

@[simp]

theorem Array.findRev?_eq_find?_reverse {α : Type} (f : α → Bool) (as : Array α) : findRev? f as = find? f as.reverse

unzip

@[simp]

theorem Array.fst_unzip {α : Type u_1} {β : Type u_2} (as : Array (α × β)) : as.unzip.fst = map Prod.fst as

@[simp]

theorem Array.snd_unzip {α : Type u_1} {β : Type u_2} (as : Array (α × β)) : as.unzip.snd = map Prod.snd as

take

@[simp]

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

countP and count

@[simp]

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

@[simp]

theorem Array.countP_toList {α : Type u_1} {p : α → Bool} (as : Array α) : List.countP p as.toList = countP p as

@[simp]

theorem List.count_toArray {α : Type u_1} [BEq α] (l : List α) (a : α) : Array.count a l.toArray = count a l

@[simp]

theorem Array.count_toList {α : Type u_1} [BEq α] (as : Array α) (a : α) : List.count a as.toList = count a as

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

theorem Array.toList_fst_unzip {α : Type u_1} {β : Type u_2} (as : Array (α × β)) : as.unzip.fst.toList = as.toList.unzip.fst

theorem Array.toList_snd_unzip {α : Type u_1} {β : Type u_2} (as : Array (α × β)) : as.unzip.snd.toList = as.toList.unzip.snd

@[simp]

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

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

Deprecations

@[reducible, inline, deprecated List.back!_toArray (since := "2024-10-31")]

abbrev List.back_toArray {α : Type u_1} [Inhabited α] (l : List α) : l.toArray.back! = l.getLast!

Equations

• @List.back_toArray = @List.back!_toArray

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

@[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} {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l

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} (a : Array α) (i : Fin a.size) : a[i] = a.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} {a : Array α} {i : Nat} : a.toList[i]? = a[i]?

Equations

• @Array.getElem?_eq_toList_getElem? = @Array.getElem?_toList

@[reducible, inline, deprecated Array.get?_eq_get?_toList (since := "2024-10-17")]

abbrev Array.get?_eq_toList_get? {α : Type u_1} (a : Array α) (i : Nat) : a.get? i = a.toList.get? i

Equations

• @Array.get?_eq_toList_get? = @Array.get?_eq_get?_toList

@[reducible, inline, deprecated Array.getElem?_swap (since := "2024-10-17")]

abbrev Array.get?_swap {α : Type u_1} (a : Array α) (i j : Nat) (hi : i < a.size) (hj : j < a.size) (k : Nat) : (a.swap i j hi hj)[k]? = if j = k then some a[i] else if i = k then some a[j] else a[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} (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) : (a.push x)[i] = if h : i < a.size then a[i] else x

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} (a : Array α) (x : α) (i : Nat) (h : i < a.size) : let_fun this := ⋯; (a.push x)[i] = a[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} (a : Array α) (x : α) : (a.push x)[a.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 α] (a : Array α) : a.back! = a.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 α] (a : Array α) : (a.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 α] {as : Array α} (h : as.size ≠ 0) : as = as.pop.push as.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} (as : Array α) (index : Nat) (val : α) : (as.setIfInBounds index val).size = as.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} (as : Array α) {i : Nat} (v : α) (h : i < (as.setIfInBounds i v).size) : (as.setIfInBounds i v)[i] = v

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} (as : Array α) {i : Nat} (v : α) : (as.setIfInBounds i v)[i]? = if i < as.size then some v 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} (a : Array α) (i : Nat) (v d : α) : (a.setIfInBounds i v)[i]?.getD d = if i < a.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} (as : Array α) (i : Nat) (v : α) (j : Nat) (hj : j < (as.setIfInBounds i v).size) : (as.setIfInBounds i v)[j] = if i = j then v else as[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} {a : Array α} (h : i < a.size) : a[i] = a.toList[i]

@[deprecated Array.getElem?_toList (since := "2024-12-08")]

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

@[deprecated LawfulGetElem.getElem?_def (since := "2024-12-08")]

theorem Array.getElem?_eq {α : Type u_1} {a : Array α} {i : Nat} : a[i]? = if h : i < a.size then some a[i] else none