@[simp]

theorem getElem_fin {Cont : Type u_1} {Elem : Type u_2} {Dom : Cont → Nat → Prop} {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 : Cont → Nat → Prop} {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 : Cont → Nat → Prop} {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 : Cont → Idx → Prop} [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 : Cont → Idx → Prop} [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 : α) : Array.singleton v = #[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 α} : List.length l.data = Array.size l

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 α) : Array.get! a n = Option.getD (Array.get? a n) default

@[simp]

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

@[simp]

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

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

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 : α) : (Array.push a x)[Array.size a]? = some 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 α) : Array.pop (Array.push a x) = a

@[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_pop_back_of_size_ne_zero {α : Type u_1} [Inhabited α] {as : Array α} (h : Array.size as ≠ 0) : as = Array.push (Array.pop as) (Array.back 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 α) : Array.size as = List.length as.data

@[simp]

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

@[simp]

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

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

@[simp]

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

@[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 → α) : Array.size (Array.ofFn f) = 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 as → Array.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) b → motive (↑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) b → motive (↑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) b → motive (↑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) b → motive (↑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 as → i ≤ 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 : α → β → γ) : Array.size (Array.zipWith as bs f) = min (Array.size as) (Array.size bs)

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 β) : Array.size (Array.zip as bs) = min (Array.size as) (Array.size bs)

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 : Nat → Prop) (h0 : motive 0) (p : Fin (Array.size as) → β → Prop) (hs : ∀ (i : Fin (Array.size as)), motive ↑i → p 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 : Nat → Prop) (h0 : motive 0) (p : Fin (Array.size as) → β → Prop) (hs : ∀ (i : Fin (Array.size as)), motive ↑i → p 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 : Nat → Prop) (p : Fin (Array.size as) → β → Prop) (hs : ∀ (i : Fin (Array.size as)), motive ↑i → p 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) → α → β) : Array.size (Array.mapIdx a f) = Array.size a

@[simp]

theorem Array.size_zipWithIndex {α : Type u_1} (as : Array α) : Array.size (Array.zipWithIndex as) = Array.size as

@[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 : α → α) : Array.size (Array.modify a i f) = Array.size a

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 α) : Array.size (Array.filter p l 0) ≤ Array.size l

@[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} : Array.size #[] = 0

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 α) : Array.size (as ++ bs) = Array.size as + Array.size bs

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 α) : Array.extract as 0 (Array.size as) = as

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 < stop → p 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 ∈ l → p x = true

contains

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

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

Equations

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

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