Documentation

Init.Data.Array.Lemmas

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 α) :
@[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 α} :
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} :
@[simp]
theorem Array.mkEmpty_eq (α : Type u_1) (n : Nat) :

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) :
theorem Array.ne_empty_of_size_pos {α✝ : Type u_1} {l : Array α✝} (h : 0 < l.size) :
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 : α✝} :
@[simp]
theorem Array.mkArray_zero {α✝ : Type u_1} {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 α} :
@[simp]
theorem Array.none_eq_getElem?_iff {α : Type u_1} {a : Array α} {i : Nat} :
theorem Array.getElem?_eq_none {α : Type u_1} {i : Nat} {a : Array α} (h : a.size i) :
@[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) :
@[simp]
theorem Array.getElem?_eq_some_getElem_iff {α : Type u_1} (a : Array α) (i : Nat) (h : i < a.size) :
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} :
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) :
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 : α) :
@[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 : ¬pArray α} :
(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 : pArray α} :
(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 ap x) p a ∀ (x : α), x xsp 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 : α) :
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 bb la 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) :
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 ya 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) :
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 lp a

isEmpty #

@[simp]
theorem Array.isEmpty_toList {α : Type u_1} {l : Array α} :
theorem Array.isEmpty_iff {α : Type u_1} {l : Array α} :
theorem Array.isEmpty_eq_false_iff_exists_mem {α : Type u_1} {xs : Array α} :
xs.isEmpty = false (x : α), x xs
@[simp]
theorem Array.isEmpty_eq_true {α : Type u_1} {l : Array α} :
@[simp]
theorem Array.isEmpty_eq_false {α : Type u_1} {l : Array α} :

Decidability of bounded quantifiers #

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

any / all #

theorem Array.anyM_eq_anyM_loop {m : TypeType 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 : TypeType 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 : TypeType 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 : TypeType u_1} {α : Type u_2} [Monad m] (p : αm Bool) (as : Array α) :
@[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 : TypeType 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 : TypeType u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : αm Bool) (as : Array α) :
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 < stopp 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 lp x = true
@[simp]
theorem List.anyM_toArray' {m : TypeType 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 : TypeType 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 : TypeType u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : αm Bool) (l : List α) :
theorem List.any_toArray {α : Type u_1} (p : αBool) (l : List α) :
l.toArray.any p = l.any p
theorem List.allM_toArray {m : TypeType u_1} {α : Type u_2} [Monad m] [LawfulMonad m] (p : αm Bool) (l : List α) :
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 asp 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 xsp 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 xsp x) = xs.all fun (b : α) => decide (p b)
@[simp]
theorem List.contains_toArray {α : Type u_1} [BEq α] {l : List α} {a : α} :
theorem List.elem_toArray {α : Type u_1} [BEq α] {l : List α} {a : α} :
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 = truea 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 = truea as
Equations
theorem Array.contains_eq_true_of_mem {α : Type u_1} [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a as) :
@[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) :
Equations
@[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
@[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
@[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 #

@[reducible, inline, deprecated Array.set!_eq_setIfInBounds (since := "2024-12-12")]
Equations
@[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
@[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 : α) :
@[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 : α) :
Equations
@[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 : α} :
@[simp]
theorem Array.setIfInBounds_eq_empty_iff {α : Type u_1} {as : Array α} (n : Nat) (a : α) :
theorem Array.setIfInBounds_comm {α : Type u_1} (a b : α) {i j : Nat} (as : Array α) (h : i j) :
@[simp]
theorem Array.setIfInBounds_setIfInBounds {α : Type u_1} (a b : α) (as : Array α) (i : Nat) :
theorem Array.mem_setIfInBounds {α : Type u_1} (as : Array α) (i : Nat) (h : i < as.size) (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 : α) :

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 α] :
@[simp]
theorem Array.lawfulBEq_iff {α : Type u_1} [BEq α] :

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 α) :
@[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 β) :
@[simp]
theorem Array.map_empty {α : Type u_1} {β : Type u_2} (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} :
@[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 lP i) ∀ (j : α), j lP (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 lf a = g a
theorem Array.map_inj_right {α : Type u_1} {β : Type u_2} {l l' : Array α} {f : αβ} (w : ∀ (x y : α), f x = f yx = 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 lf 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 lf 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 α} :
@[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 α) :
@[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 α) :
@[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 α) :
@[simp]
theorem List.filter_toArray' {α : Type u_1} {stop : Nat} (p : αBool) (l : List α) (h : stop = l.length) :
theorem List.filter_toArray {α : Type u_1} (p : αBool) (l : List α) :
@[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 α) :
@[simp]
theorem Array.filter_eq_self {α : Type u_1} {p : αBool} {l : Array α} :
filter p l = l ∀ (a : α), a lp a = true
@[simp]
theorem Array.filter_size_eq_size {α : Type u_1} {p : αBool} {l : Array α} :
(filter p l).size = l.size ∀ (a : α), a lp 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 lP i) ∀ (j : α), j lp j = trueP 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) :
theorem Array.toList_filterMap {α : Type u_1} {β : Type u_2} (f : αOption β) (l : Array α) :
@[simp]
theorem List.filterMap_toArray' {α : Type u_1} {β : Type u_2} {stop : Nat} (f : αOption β) (l : List α) (h : stop = l.length) :
theorem List.filterMap_toArray {α : Type u_1} {β : Type u_2} (f : αOption β) (l : List α) :
@[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 α) :
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 α) :
@[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 lP i) ∀ (j : α), j l∀ (b : β), f j = some bP 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 xsf x = none
@[simp]
theorem Array.filterMap_eq_nil_iff {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝Option α✝¹} {l : Array α✝} :
filterMap f l = #[] ∀ (a : α✝), a lf 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 : α) :

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
@[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} :
@[simp]
@[simp]
theorem Array.size_flatten {α : Type u_1} (L : Array (Array α)) :
@[simp]
theorem Array.flatten_singleton {α : Type u_1} (l : Array α) :
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 Ll = #[]
@[simp]
theorem Array.empty_eq_flatten_iff {α : Type u_1} {L : Array (Array α)} :
#[] = L.flatten ∀ (l : Array α), l Ll = #[]
theorem Array.flatten_ne_empty_iff {α : Type u_1} {xs : Array (Array α)} :
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) :
theorem Array.forall_mem_flatten {α : Type u_1} {p : αProp} {L : Array (Array α)} :
(∀ (x : α), x L.flattenp x) ∀ (l : Array α), l L∀ (x : α), x lp x
theorem Array.flatten_eq_flatMap {α : Type u_1} {L : Array (Array α)} :
@[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_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 csl = #[]) 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 csl = #[]) 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 α)) :
@[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 lf x = #[]
theorem Array.forall_mem_flatMap {β : Type u_1} {α : Type u_2} {p : βProp} {l : Array α} {f : αArray β} :
(∀ (x : β), x flatMap f lp x) ∀ (a : α), a l∀ (b : β), b f ap 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 : α✝} :
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 ap 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 lb = 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 lb = 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 lf x = b
@[simp]
theorem Array.map_const {α : Type u_1} {β : Type u_2} (l : Array α) (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} :
@[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) :
@[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) :
@[simp]
theorem Array.flatten_mkArray_empty {n : Nat} {α : Type u_1} :
@[simp]
theorem Array.flatten_mkArray_singleton {n : Nat} {α✝ : Type u_1} {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 α) :
@[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 α) :
@[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 α) :
@[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 α} :
theorem Array.reverse_ne_empty_iff {α : Type u_1} {xs : Array α} :
theorem Array.getElem?_reverse' {α : Type u_1} {l : Array α} (i j : Nat) (h : i + j + 1 = l.size) :

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 α) :
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 α) :
@[simp]
theorem Array.filterMap_reverse {α : Type u_1} {β : Type u_2} (f : αOption β) (l : Array α) :
@[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

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

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 β) :
theorem Array.flatMap_reverse {α : Type u_1} {β : Type u_2} (l : Array α) (f : αArray β) :
@[simp]
theorem Array.reverse_mkArray {α : Type u_1} (n : Nat) (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
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 initfoldlM 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 initfoldlM 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 bfoldlM 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 bfoldlM 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 initf 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 initf 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) bmotive (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) bmotive (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) bmotive (↑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) bmotive (↑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 initfoldrM 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 initfoldrM 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 α) :
@[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
@[simp]
theorem Array.toListRev_eq {α : Type u_1} (arr : Array α) :
@[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) :
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) :
@[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) :
@[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
@[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α) :
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 : α) :

get lemmas #

theorem Array.lt_of_getElem {α : Type u_1} {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size} :
a[idx] = xidx < a.size
theorem Array.getElem_fin_eq_getElem_toList {α : Type u_1} (a : Array α) (i : Fin a.size) :
@[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) :
@[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) :
Equations
theorem Array.getElem_mem_toList {α : Type u_1} {i : Nat} (a : Array α) (h : i < a.size) :
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 α) :
@[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
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
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
@[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
@[simp]
theorem Array.getElem?_size {α : Type u_1} {a : Array α} :
@[reducible, inline, deprecated Array.getElem?_size (since := "2024-10-21")]
abbrev Array.get?_size {α : Type u_1} {a : Array α} :
Equations
@[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 α) :
@[simp]
theorem Array.pop_empty {α : Type u_1} :
@[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 α) :
@[simp]
theorem Array.size_swapIfInBounds {α : Type u_1} (a : Array α) (i j : Nat) :
@[reducible, inline, deprecated Array.size_swapIfInBounds (since := "2024-11-24")]
abbrev Array.size_swap! {α : Type u_1} (a : Array α) (i j : Nat) :
Equations
@[simp]
theorem Array.size_range {n : Nat} :
(range n).size = n
@[simp]
@[simp]
theorem Array.getElem_range {n i : Nat} (h : i < (range n).size) :
(range n)[i] = i
@[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) :
@[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 : NatProp) (h0 : motive 0) (p : Fin as.sizeβProp) (hs : ∀ (i : Fin as.size), motive ip 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

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) :

isPrefixOf #

@[simp]
theorem Array.isPrefixOf_toList {α : Type u_1} [BEq α] {as bs : Array α} :

zipWith #

@[simp]
theorem Array.toList_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (as : Array α) (bs : Array β) :
@[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 β) :
@[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 α) :
@[simp]
theorem Array.findM?_toList {m : TypeType} {α : Type} [Monad m] [LawfulMonad m] (p : αm Bool) (as : Array α) :
@[simp]
theorem Array.findSome?_toList {α : Type u_1} {β : Type u_2} (p : αOption β) (as : Array α) :
@[simp]
theorem Array.find?_toList {α : Type u_1} (p : αBool) (as : Array α) :
@[simp]
theorem Array.finIdxOf?_toList {α : Type u_1} [BEq α] (a : α) (v : Array α) :
@[simp]
theorem Array.findFinIdx?_toList {α : Type u_1} (p : αBool) (v : Array α) :

More theorems about List.toArray, followed by an Array operation. #

Our goal is to have simp "pull List.toArray outwards" as much as possible.

@[simp]
theorem List.take_toArray {α : Type u_1} (l : List α) (n : Nat) :
@[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 α) :
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]
@[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α) :
@[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α) :
@[simp]
theorem Array.toList_takeWhile {α : Type u_1} (p : αBool) (as : Array α) :
@[simp]
theorem Array.toList_eraseIdx {α : Type u_1} (as : Array α) (i : Nat) (h : i < as.size) :
@[simp]
theorem Array.toList_eraseIdxIfInBounds {α : Type u_1} (as : Array α) (i : Nat) :

flatten #

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 α) :
@[simp]
theorem Array.findRevM?_eq_findM?_reverse {m : TypeType} {α : Type} [Monad m] [LawfulMonad m] (f : αm Bool) (as : Array α) :
@[simp]
theorem Array.findSomeRev?_eq_findSome?_reverse {α : Type u_1} {β : Type u_2} (f : αOption β) (as : Array α) :
@[simp]
theorem Array.findRev?_eq_find?_reverse {α : Type} (f : αBool) (as : Array α) :

unzip #

@[simp]
theorem Array.fst_unzip {α : Type u_1} {β : Type u_2} (as : Array (α × β)) :
@[simp]
theorem Array.snd_unzip {α : Type u_1} {β : Type u_2} (as : Array (α × β)) :

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 α) :
@[simp]
theorem Array.countP_toList {α : Type u_1} {p : αBool} (as : Array α) :
@[simp]
theorem List.count_toArray {α : Type u_1} [BEq α] (l : List α) (a : α) :
@[simp]
theorem Array.count_toList {α : Type u_1} [BEq α] (as : Array α) (a : α) :
@[simp]
theorem List.unzip_toArray {α : Type u_1} {β : Type u_2} (as : List (α × β)) :
@[simp]
theorem List.firstM_toArray {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Alternative m] (as : List α) (f : αm β) :
theorem Array.toList_fst_unzip {α : Type u_1} {β : Type u_2} (as : Array (α × β)) :
theorem Array.toList_snd_unzip {α : Type u_1} {β : Type u_2} (as : Array (α × β)) :
@[simp]
theorem Array.flatMap_empty {α : Type u_1} {β : Type u_2} (f : αArray β) :
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 α) :
Equations
@[reducible, inline, deprecated List.setIfInBounds_toArray (since := "2024-11-24")]
abbrev List.setD_toArray {α : Type u_1} (l : List α) (i : Nat) (a : α) :
Equations
@[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) :
Equations
@[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) :
Equations
@[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
@[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) :
Equations
@[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} :
Equations
@[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
@[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
@[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
@[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
@[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
@[reducible, inline, deprecated Array.back!_eq_back? (since := "2024-10-31")]
abbrev Array.back_eq_back? {α : Type u_1} [Inhabited α] (a : Array α) :
Equations
@[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
@[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
@[reducible, inline, deprecated Array.set!_is_setIfInBounds (since := "2024-11-24")]
Equations
@[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
@[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
@[reducible, inline, deprecated Array.getElem?_setIfInBounds_eq (since := "2024-11-24")]
abbrev Array.get?_setD_eq {α : Type u_1} (as : Array α) {i : Nat} (v : α) :
Equations
@[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
@[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
@[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) :
@[deprecated Array.getElem?_toList (since := "2024-12-08")]
theorem Array.getElem?_eq_getElem?_toList {α : Type u_1} (a : Array α) (i : Nat) :
@[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