Documentation

Std.Data.Array.Lemmas

@[simp]
theorem getElem_fin {Cont : Type u_1} {Elem : Type u_2} {Dom : ContNatProp} {n : Nat} [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
a[i] = a[i]
@[simp]
theorem getElem?_fin {Cont : Type u_1} {Elem : Type u_2} {Dom : ContNatProp} {n : Nat} [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Decidable (Dom a i)] :
a[i]? = a[i]?
@[simp]
theorem getElem!_fin {Cont : Type u_1} {Elem : Type u_2} {Dom : ContNatProp} {n : Nat} [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Decidable (Dom a i)] [Inhabited Elem] :
a[i]! = a[i]!
theorem getElem?_pos {Cont : Type u_1} {Idx : Type u_2} {Elem : Type u_3} {Dom : ContIdxProp} [GetElem Cont Idx Elem Dom] (a : Cont) (i : Idx) (h : Dom a i) [Decidable (Dom a i)] :
a[i]? = some a[i]
theorem getElem?_neg {Cont : Type u_1} {Idx : Type u_2} {Elem : Type u_3} {Dom : ContIdxProp} [GetElem Cont Idx Elem Dom] (a : Cont) (i : Idx) (h : ¬Dom a i) [Decidable (Dom a i)] :
a[i]? = none
@[simp]
theorem mkArray_data {α : Type u_1} (n : Nat) (v : α) :
(mkArray n v).data = List.replicate n v
@[simp]
theorem getElem_mkArray {α : Type u_1} {i : Nat} (n : Nat) (v : α) (h : i < Array.size (mkArray n v)) :
(mkArray n v)[i] = v
@[simp]
theorem Array.singleton_def {α : Type u_1} (v : α) :
@[simp]
theorem Array.toArray_data {α : Type u_1} (a : Array α) :
List.toArray a.data = a
@[simp]
theorem Array.data_length {α : Type u_1} {l : Array α} :
theorem Array.mem_data {α : Type u_1} {a : α} {l : Array α} :
a l.data a l

mem #

theorem Array.not_mem_nil {α : Type u_1} (a : α) :
¬a #[]
theorem Array.getElem?_mem {α : Type u_1} {l : Array α} {i : Fin (Array.size l)} :
l[i] l

get lemmas #

theorem Array.getElem_fin_eq_data_get {α : Type u_1} (a : Array α) (i : Fin (List.length a.data)) :
a[i] = List.get a.data i
@[simp]
theorem Array.ugetElem_eq_getElem {α : Type u_1} (a : Array α) {i : USize} (h : USize.toNat i < Array.size a) :
a[i] = a[USize.toNat i]
theorem Array.getElem?_eq_getElem {α : Type u_1} (a : Array α) (i : Nat) (h : i < Array.size a) :
a[i]? = some a[i]
theorem Array.get?_len_le {α : Type u_1} (a : Array α) (i : Nat) (h : Array.size a i) :
a[i]? = none
theorem Array.getElem_mem_data {α : Type u_1} {i : Nat} (a : Array α) (h : i < Array.size a) :
a[i] a.data
theorem Array.getElem?_eq_data_get? {α : Type u_1} (a : Array α) (i : Nat) :
a[i]? = List.get? a.data i
theorem Array.get?_eq_data_get? {α : Type u_1} (a : Array α) (i : Nat) :
Array.get? a i = List.get? a.data i
theorem Array.get!_eq_get? {α : Type u_1} {n : Nat} [Inhabited α] (a : Array α) :
@[simp]
theorem Array.back_eq_back? {α : Type u_1} [Inhabited α] (a : Array α) :
@[simp]
theorem Array.back?_push {α : Type u_1} {x : α} (a : Array α) :
theorem Array.back_push {α : Type u_1} {x : α} [Inhabited α] (a : Array α) :
theorem Array.get?_push_lt {α : Type u_1} (a : Array α) (x : α) (i : Nat) (h : i < Array.size a) :
(Array.push a x)[i]? = some a[i]
theorem Array.get?_push_eq {α : Type u_1} (a : Array α) (x : α) :
theorem Array.get?_push {α : Type u_1} {x : α} {i : Nat} {a : Array α} :
(Array.push a x)[i]? = if i = Array.size a then some x else a[i]?
@[simp]
theorem Array.get?_size {α : Type u_1} {a : Array α} :
a[Array.size a]? = none
@[simp]
theorem Array.data_set {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) (v : α) :
(Array.set a i v).data = List.set a.data (i) v
theorem Array.get_set_eq {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) (v : α) :
(Array.set a i v)[i] = v
theorem Array.get?_set_eq {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) (v : α) :
(Array.set a i v)[i]? = some v
@[simp]
theorem Array.get?_set_ne {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) {j : Nat} (v : α) (h : i j) :
(Array.set a i v)[j]? = a[j]?
theorem Array.get?_set {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) (j : Nat) (v : α) :
(Array.set a i v)[j]? = if i = j then some v else a[j]?
theorem Array.get_set {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) (j : Nat) (hj : j < Array.size a) (v : α) :
(Array.set a i v)[j] = if i = j then v else a[j]
@[simp]
theorem Array.get_set_ne {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) {j : Nat} (v : α) (hj : j < Array.size a) (h : i j) :
(Array.set a i v)[j] = a[j]
theorem Array.getElem_setD {α : Type u_1} (a : Array α) (i : Nat) (v : α) (h : i < Array.size (Array.setD a i v)) :
(Array.setD a i v)[i] = v
theorem Array.set_set {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) (v : α) (v' : α) :
Array.set (Array.set a i v) { val := i, isLt := } v' = Array.set a i v'
theorem Array.swap_def {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) (j : Fin (Array.size a)) :
Array.swap a i j = Array.set (Array.set a i (Array.get a j)) { val := j, isLt := } (Array.get a i)
theorem Array.data_swap {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) (j : Fin (Array.size a)) :
(Array.swap a i j).data = List.set (List.set a.data (i) (Array.get a j)) (j) (Array.get a i)
theorem Array.get?_swap {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) (j : Fin (Array.size a)) (k : Nat) :
(Array.swap a i j)[k]? = if j = k then some a[i] else if i = k then some a[j] else a[k]?
@[simp]
theorem Array.swapAt_def {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) (v : α) :
Array.swapAt a i v = (a[i], Array.set a i v)
theorem Array.swapAt!_def {α : Type u_1} (a : Array α) (i : Nat) (v : α) (h : i < Array.size a) :
Array.swapAt! a i v = (a[i], Array.set a { val := i, isLt := h } v)
@[simp]
theorem Array.data_pop {α : Type u_1} (a : Array α) :
(Array.pop a).data = List.dropLast a.data
@[simp]
theorem Array.pop_empty {α : Type u_1} :
Array.pop #[] = #[]
@[simp]
theorem Array.pop_push {α : Type u_1} {x : α} (a : Array α) :
@[simp]
theorem Array.getElem_pop {α : Type u_1} (a : Array α) (i : Nat) (hi : i < Array.size (Array.pop a)) :
(Array.pop a)[i] = a[i]
theorem Array.eq_empty_of_size_eq_zero {α : Type u_1} {as : Array α} (h : Array.size as = 0) :
as = #[]
theorem Array.eq_push_of_size_ne_zero {α : Type u_1} {as : Array α} (h : Array.size as 0) :
∃ (bs : Array α), ∃ (c : α), as = Array.push bs c
theorem Array.size_eq_length_data {α : Type u_1} (as : Array α) :
@[simp]
theorem Array.size_swap! {α : Type u_1} (a : Array α) (i : Nat) (j : Nat) :
@[simp]
theorem Array.size_reverse {α : Type u_1} (a : Array α) :
theorem Array.size_reverse.go {α : Type u_1} (as : Array α) (i : Nat) (j : Fin (Array.size as)) :
@[simp]
@[simp]
theorem Array.reverse_data {α : Type u_1} (a : Array α) :
(Array.reverse a).data = List.reverse a.data
theorem Array.reverse_data.go {α : Type u_1} (a : Array α) (as : Array α) (i : Nat) (j : Nat) (hj : j < Array.size as) (h : i + j + 1 = Array.size a) (h₂ : Array.size as = Array.size a) (H : ∀ (k : Nat), List.get? as.data k = if i k k j then List.get? a.data k else List.get? (List.reverse a.data) k) (k : Nat) :
List.get? (Array.reverse.loop as i { val := j, isLt := hj }).data k = List.get? (List.reverse a.data) k
@[simp]
theorem Array.size_ofFn_go {α : Type u_1} {n : Nat} (f : Fin nα) (i : Nat) (acc : Array α) :
Array.size (Array.ofFn.go f i acc) = Array.size acc + (n - i)
@[simp]
theorem Array.size_ofFn {n : Nat} {α : Type u_1} (f : Fin nα) :
theorem Array.getElem_ofFn_go {n : Nat} {α : Type u_1} (f : Fin nα) (i : Nat) {acc : Array α} {k : Nat} (hki : k < n) (hin : i n) (hi : i = Array.size acc) (hacc : ∀ (j : Nat) (hj : j < Array.size acc), acc[j] = f { val := j, isLt := }) :
(Array.ofFn.go f i acc)[k] = f { val := k, isLt := hki }
@[simp]
theorem Array.getElem_ofFn {n : Nat} {α : Type u_1} (f : Fin nα) (i : Nat) (h : i < Array.size (Array.ofFn f)) :
(Array.ofFn f)[i] = f { val := i, isLt := }
theorem Array.forIn_eq_data_forIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (as : Array α) (b : β) (f : αβm (ForInStep β)) :
forIn as b f = forIn as.data b f
theorem Array.forIn_eq_data_forIn.loop {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (as : Array α) (f : αβm (ForInStep β)) {i : Nat} {h : i Array.size as} {b : β} {j : Nat} :
j + i = Array.size asArray.forIn.loop as f i h b = forIn (List.drop j as.data) b f

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 (Array.size as)) (b : β), motive (i) bmotive (i + 1) (f b as[i])) :
motive (Array.size as) (Array.foldl f init as 0)
theorem Array.foldl_induction.go {α : Type u_1} {β : Type u_2} {as : Array α} (motive : NatβProp) {f : βαβ} (hf : ∀ (i : Fin (Array.size as)) (b : β), motive (i) bmotive (i + 1) (f b as[i])) {i : Nat} {j : Nat} {b : β} (h₁ : j Array.size as) (h₂ : Array.size as i + j) (H : motive j b) :
motive (Array.size as) (Array.foldlM.loop f as (Array.size as) i j b)
theorem Array.foldr_induction {α : Type u_1} {β : Type u_2} {as : Array α} (motive : NatβProp) {init : β} (h0 : motive (Array.size as) init) {f : αββ} (hf : ∀ (i : Fin (Array.size as)) (b : β), motive (i + 1) bmotive (i) (f as[i] b)) :
motive 0 (Array.foldr f init as (Array.size as))
theorem Array.foldr_induction.go {α : Type u_1} {β : Type u_2} {as : Array α} (motive : NatβProp) {f : αββ} (hf : ∀ (i : Fin (Array.size as)) (b : β), motive (i + 1) bmotive (i) (f as[i] b)) {i : Nat} {b : β} (hi : i Array.size as) (H : motive i b) :
motive 0 (Array.foldrM.fold f as 0 i hi b)

zipWith / zip #

theorem Array.zipWith_eq_zipWith_data {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (as : Array α) (bs : Array β) :
(Array.zipWith as bs f).data = List.zipWith f as.data bs.data
theorem Array.zipWith_eq_zipWith_data.loop {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) :
i Array.size asi Array.size bs(Array.zipWithAux f as bs i cs).data = cs.data ++ List.zipWith f (List.drop i as.data) (List.drop i bs.data)
theorem Array.size_zipWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (as : Array α) (bs : Array β) (f : αβγ) :
theorem Array.zip_eq_zip_data {α : Type u_1} {β : Type u_2} (as : Array α) (bs : Array β) :
(Array.zip as bs).data = List.zip as.data bs.data
theorem Array.size_zip {α : Type u_1} {β : Type u_2} (as : Array α) (bs : Array β) :

map #

@[simp]
theorem Array.mem_map {α : Type u_1} {β : Type u_2} {b : β} {f : αβ} {l : Array α} :
b Array.map f l ∃ (a : α), a l f a = b
theorem Array.mapM_eq_mapM_data {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : αm β) (arr : Array α) :
Array.mapM f arr = do let __do_lift ← List.mapM f arr.data pure { data := __do_lift }
theorem Array.mapM_map_eq_foldl {α : Type u_1} {β : Type u_2} {b : Array β} (as : Array α) (f : αβ) (i : Nat) :
Array.mapM.map f as i b = Array.foldl (fun (r : Array β) (a : α) => Array.push r (f a)) b as i
theorem Array.map_eq_foldl {α : Type u_1} {β : Type u_2} (as : Array α) (f : αβ) :
Array.map f as = Array.foldl (fun (r : Array β) (a : α) => Array.push r (f a)) #[] as 0
theorem Array.map_induction {α : Type u_1} {β : Type u_2} (as : Array α) (f : αβ) (motive : NatProp) (h0 : motive 0) (p : Fin (Array.size as)βProp) (hs : ∀ (i : Fin (Array.size as)), motive ip i (f as[i]) motive (i + 1)) :
motive (Array.size as) ∃ (eq : Array.size (Array.map f as) = Array.size as), ∀ (i : Nat) (h : i < Array.size as), p { val := i, isLt := h } (Array.map f as)[i]
theorem Array.map_spec {α : Type u_1} {β : Type u_2} (as : Array α) (f : αβ) (p : Fin (Array.size as)βProp) (hs : ∀ (i : Fin (Array.size as)), p i (f as[i])) :
∃ (eq : Array.size (Array.map f as) = Array.size as), ∀ (i : Nat) (h : i < Array.size as), p { val := i, isLt := h } (Array.map f as)[i]
@[simp]
theorem Array.getElem_map {α : Type u_1} {β : Type u_2} (f : αβ) (as : Array α) (i : Nat) (h : i < Array.size (Array.map f as)) :
(Array.map f as)[i] = f as[i]

mapIdx #

theorem Array.mapIdx_induction {α : Type u_1} {β : Type u_2} (as : Array α) (f : Fin (Array.size as)αβ) (motive : NatProp) (h0 : motive 0) (p : Fin (Array.size as)βProp) (hs : ∀ (i : Fin (Array.size as)), motive ip i (f i as[i]) motive (i + 1)) :
motive (Array.size as) ∃ (eq : Array.size (Array.mapIdx as f) = Array.size as), ∀ (i : Nat) (h : i < Array.size as), p { val := i, isLt := h } (Array.mapIdx as f)[i]
theorem Array.mapIdx_induction.go {α : Type u_1} {β : Type u_2} (as : Array α) (f : Fin (Array.size as)αβ) (motive : NatProp) (p : Fin (Array.size as)βProp) (hs : ∀ (i : Fin (Array.size as)), motive ip i (f i as[i]) motive (i + 1)) {bs : Array β} {i : Nat} {j : Nat} {h : i + j = Array.size as} (h₁ : j = Array.size bs) (h₂ : ∀ (i : Nat) (h : i < Array.size as) (h' : i < Array.size bs), p { val := i, isLt := h } bs[i]) (hm : motive j) :
let arr := Array.mapIdxM.map as f i j h bs; motive (Array.size as) ∃ (eq : Array.size arr = Array.size as), ∀ (i : Nat) (h : i < Array.size as), p { val := i, isLt := h } arr[i]
theorem Array.mapIdx_spec {α : Type u_1} {β : Type u_2} (as : Array α) (f : Fin (Array.size as)αβ) (p : Fin (Array.size as)βProp) (hs : ∀ (i : Fin (Array.size as)), p i (f i as[i])) :
∃ (eq : Array.size (Array.mapIdx as f) = Array.size as), ∀ (i : Nat) (h : i < Array.size as), p { val := i, isLt := h } (Array.mapIdx as f)[i]
@[simp]
theorem Array.size_mapIdx {α : Type u_1} {β : Type u_2} (a : Array α) (f : Fin (Array.size a)αβ) :
@[simp]
@[simp]
theorem Array.getElem_mapIdx {α : Type u_1} {β : Type u_2} (a : Array α) (f : Fin (Array.size a)αβ) (i : Nat) (h : i < Array.size (Array.mapIdx a f)) :
(Array.mapIdx a f)[i] = f { val := i, isLt := } a[i]

modify #

@[simp]
theorem Array.size_modify {α : Type u_1} (a : Array α) (i : Nat) (f : αα) :
theorem Array.get_modify {α : Type u_1} {f : αα} {arr : Array α} {x : Nat} {i : Nat} (h : i < Array.size arr) :
Array.get (Array.modify arr x f) { val := i, isLt := } = if x = i then f (Array.get arr { val := i, isLt := h }) else Array.get arr { val := i, isLt := h }

filter #

@[simp]
theorem Array.filter_data {α : Type u_1} (p : αBool) (l : Array α) :
(Array.filter p l 0).data = List.filter p l.data
@[simp]
theorem Array.filter_filter {α : Type u_1} {p : αBool} (q : αBool) (l : Array α) :
Array.filter p (Array.filter q l 0) 0 = Array.filter (fun (a : α) => decide (p a = true q a = true)) l 0
theorem Array.size_filter_le {α : Type u_1} (p : αBool) (l : Array α) :
@[simp]
theorem Array.mem_filter :
∀ {α : Type u_1} {x : α} {p : αBool} {as : Array α}, x Array.filter p as 0 x as p x = true
theorem Array.mem_of_mem_filter {α : Type u_1} {p : αBool} {a : α} {l : Array α} (h : a Array.filter p l 0) :
a l

filterMap #

@[simp]
theorem Array.filterMap_data {α : Type u_1} {β : Type u_2} (f : αOption β) (l : Array α) :
(Array.filterMap f l 0).data = List.filterMap f l.data
@[simp]
theorem Array.mem_filterMap {α : Type u_1} {β : Type u_2} (f : αOption β) (l : Array α) {b : β} :
b Array.filterMap f l 0 ∃ (a : α), a l f a = some b

join #

@[simp]
theorem Array.join_data {α : Type u_1} {l : Array (Array α)} :
(Array.join l).data = List.join (List.map Array.data l.data)
theorem Array.mem_join {α : Type u_1} {a : α} {L : Array (Array α)} :
a Array.join L ∃ (l : Array α), l L a l

empty #

theorem Array.size_empty {α : Type u_1} :
theorem Array.empty_data {α : Type u_1} :
#[].data = []

append #

theorem Array.push_eq_append_singleton {α : Type u_1} (as : Array α) (x : α) :
Array.push as x = as ++ #[x]
@[simp]
theorem Array.mem_append {α : Type u_1} {a : α} {s : Array α} {t : Array α} :
a s ++ t a s a t
theorem Array.size_append {α : Type u_1} (as : Array α) (bs : Array α) :
theorem Array.get_append_left {α : Type u_1} {i : Nat} {as : Array α} {bs : Array α} {h : i < Array.size (as ++ bs)} (hlt : i < Array.size as) :
(as ++ bs)[i] = as[i]
theorem Array.get_append_right {α : Type u_1} {i : Nat} {as : Array α} {bs : Array α} {h : i < Array.size (as ++ bs)} (hle : Array.size as i) (hlt : optParam (i - Array.size as < Array.size bs) ) :
(as ++ bs)[i] = bs[i - Array.size as]
@[simp]
theorem Array.append_nil {α : Type u_1} (as : Array α) :
as ++ #[] = as
@[simp]
theorem Array.nil_append {α : Type u_1} (as : Array α) :
#[] ++ as = as
theorem Array.append_assoc {α : Type u_1} (as : Array α) (bs : Array α) (cs : Array α) :
as ++ bs ++ cs = as ++ (bs ++ cs)

extract #

theorem Array.extract_loop_zero {α : Type u_1} (as : Array α) (bs : Array α) (start : Nat) :
Array.extract.loop as 0 start bs = bs
theorem Array.extract_loop_succ {α : Type u_1} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) (h : start < Array.size as) :
Array.extract.loop as (size + 1) start bs = Array.extract.loop as size (start + 1) (Array.push bs as[start])
theorem Array.extract_loop_of_ge {α : Type u_1} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) (h : start Array.size as) :
Array.extract.loop as size start bs = bs
theorem Array.extract_loop_eq_aux {α : Type u_1} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) :
Array.extract.loop as size start bs = bs ++ Array.extract.loop as size start #[]
theorem Array.extract_loop_eq {α : Type u_1} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) (h : start + size Array.size as) :
Array.extract.loop as size start bs = bs ++ Array.extract as start (start + size)
theorem Array.size_extract_loop {α : Type u_1} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) :
Array.size (Array.extract.loop as size start bs) = Array.size bs + min size (Array.size as - start)
@[simp]
theorem Array.size_extract {α : Type u_1} (as : Array α) (start : Nat) (stop : Nat) :
Array.size (Array.extract as start stop) = min stop (Array.size as) - start
theorem Array.get_extract_loop_lt_aux {α : Type u_1} {i : Nat} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) (hlt : i < Array.size bs) :
i < Array.size (Array.extract.loop as size start bs)
theorem Array.get_extract_loop_lt {α : Type u_1} {i : Nat} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) (hlt : i < Array.size bs) (h : optParam (i < Array.size (Array.extract.loop as size start bs)) ) :
(Array.extract.loop as size start bs)[i] = bs[i]
theorem Array.get_extract_loop_ge_aux {α : Type u_1} {i : Nat} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) (hge : i Array.size bs) (h : i < Array.size (Array.extract.loop as size start bs)) :
start + i - Array.size bs < Array.size as
theorem Array.get_extract_loop_ge {α : Type u_1} {i : Nat} (as : Array α) (bs : Array α) (size : Nat) (start : Nat) (hge : i Array.size bs) (h : i < Array.size (Array.extract.loop as size start bs)) (h' : optParam (start + i - Array.size bs < Array.size as) ) :
(Array.extract.loop as size start bs)[i] = as[start + i - Array.size bs]
theorem Array.get_extract_aux {α : Type u_1} {i : Nat} {as : Array α} {start : Nat} {stop : Nat} (h : i < Array.size (Array.extract as start stop)) :
start + i < Array.size as
@[simp]
theorem Array.get_extract {α : Type u_1} {i : Nat} {as : Array α} {start : Nat} {stop : Nat} (h : i < Array.size (Array.extract as start stop)) :
(Array.extract as start stop)[i] = as[start + i]
@[simp]
theorem Array.extract_all {α : Type u_1} (as : Array α) :
theorem Array.extract_empty_of_stop_le_start {α : Type u_1} (as : Array α) {start : Nat} {stop : Nat} (h : stop start) :
Array.extract as start stop = #[]
theorem Array.extract_empty_of_size_le_start {α : Type u_1} (as : Array α) {start : Nat} {stop : Nat} (h : Array.size as start) :
Array.extract as start stop = #[]
@[simp]
theorem Array.extract_empty {α : Type u_1} (start : Nat) (stop : Nat) :
Array.extract #[] start stop = #[]

any #

theorem Array.anyM_loop_iff_exists {α : Type u_1} (p : αBool) (as : Array α) (start : Nat) (stop : Nat) (h : stop Array.size as) :
Array.anyM.loop p as stop h start = true ∃ (i : Fin (Array.size as)), start i i < stop p as[i] = true
theorem Array.any_iff_exists {α : Type u_1} (p : αBool) (as : Array α) (start : Nat) (stop : Nat) :
Array.any as p start stop = true ∃ (i : Fin (Array.size as)), start i i < stop p as[i] = true
theorem Array.any_eq_true {α : Type u_1} (p : αBool) (as : Array α) :
Array.any as p 0 = true ∃ (i : Fin (Array.size as)), p as[i] = true
theorem Array.any_def {α : Type u_1} {p : αBool} (as : Array α) :
Array.any as p 0 = List.any as.data p

all #

theorem Array.all_eq_not_any_not {α : Type u_1} (p : αBool) (as : Array α) (start : Nat) (stop : Nat) :
Array.all as p start stop = !Array.any as (fun (x : α) => !p x) start stop
theorem Array.all_iff_forall {α : Type u_1} (p : αBool) (as : Array α) (start : Nat) (stop : Nat) :
Array.all as p start stop = true ∀ (i : Fin (Array.size as)), start i i < stopp as[i] = true
theorem Array.all_eq_true {α : Type u_1} (p : αBool) (as : Array α) :
Array.all as p 0 = true ∀ (i : Fin (Array.size as)), p as[i] = true
theorem Array.all_def {α : Type u_1} {p : αBool} (as : Array α) :
Array.all as p 0 = List.all as.data p
theorem Array.all_eq_true_iff_forall_mem {α : Type u_1} {p : αBool} {l : Array α} :
Array.all l p 0 = true ∀ (x : α), x lp x = true

contains #

theorem Array.contains_def {α : Type u_1} [DecidableEq α] {a : α} {as : Array α} :

erase #

swap #

@[simp]
theorem Array.get_swap_right {α : Type u_1} (a : Array α) {i : Fin (Array.size a)} {j : Fin (Array.size a)} :
(Array.swap a i j)[j] = a[i]
@[simp]
theorem Array.get_swap_left {α : Type u_1} (a : Array α) {i : Fin (Array.size a)} {j : Fin (Array.size a)} :
(Array.swap a i j)[i] = a[j]
@[simp]
theorem Array.get_swap_of_ne {α : Type u_1} {p : Nat} (a : Array α) {i : Fin (Array.size a)} {j : Fin (Array.size a)} (hp : p < Array.size a) (hi : p i) (hj : p j) :
(Array.swap a i j)[p] = a[p]
theorem Array.get_swap {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) (j : Fin (Array.size a)) (k : Nat) (hk : k < Array.size a) :
(Array.swap a i j)[k] = if k = i then a[j] else if k = j then a[i] else a[k]
theorem Array.get_swap' {α : Type u_1} (a : Array α) (i : Fin (Array.size a)) (j : Fin (Array.size a)) (k : Nat) (hk' : k < Array.size (Array.swap a i j)) :
(Array.swap a i j)[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 : Fin (Array.size a)} {j : Fin (Array.size a)} :
Array.swap (Array.swap a i j) { val := i, isLt := } { val := j, isLt := } = a
theorem Array.swap_comm {α : Type u_1} (a : Array α) {i : Fin (Array.size a)} {j : Fin (Array.size a)} :
Array.swap a i j = Array.swap a j i