Documentation

Init.Data.Array.Find

Lemmas about Array.findSome?, Array.find?, Array.findIdx, Array.findIdx?, Array.idxOf`. #

findSome? #

source
@[simp]
theorem Array.findSomeRev?_push_of_isSome {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} {a : α} {xs : Array α} (h : (f a).isSome = true) :
findSomeRev? f (xs.push a) = f a
source
@[simp]
theorem Array.findSomeRev?_push_of_isNone {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} {a : α} {xs : Array α} (h : (f a).isNone = true) :
findSomeRev? f (xs.push a) = findSomeRev? f xs
source
theorem Array.exists_of_findSome?_eq_some {α : Type u_1} {β : Type u_2} {b : β} {f : α → Option β} {xs : Array α} (w : findSome? f xs = some b) :
∃ (a : α), a ∈ xs ∧ f a = some b
source
@[simp]
theorem Array.findSome?_eq_none_iff {α✝ : Type u_1} {α✝¹ : Type u_2} {p : α✝ → Option α✝¹} {xs : Array α✝} :
findSome? p xs = none ↔ ∀ (x : α✝), x ∈ xs → p x = none
source
@[simp]
theorem Array.findSome?_isSome_iff {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} :
(findSome? f xs).isSome = true ↔ ∃ (x : α), x ∈ xs ∧ (f x).isSome = true
source
theorem Array.findSome?_eq_some_iff {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} {b : β} :
findSome? f xs = some b ↔ ∃ (ys : Array α), ∃ (a : α), ∃ (zs : Array α), xs = ys.push a ++ zs ∧ f a = some b ∧ ∀ (x : α), x ∈ ys → f x = none
source
@[simp]
theorem Array.findSome?_guard {α : Type u_1} {p : α → Bool} {xs : Array α} :
findSome? (Option.guard fun (x : α) => p x = true) xs = find? p xs
source
theorem Array.find?_eq_findSome?_guard {α : Type u_1} {p : α → Bool} {xs : Array α} :
find? p xs = findSome? (Option.guard fun (x : α) => p x = true) xs
source
@[simp]
theorem Array.getElem?_zero_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} :
(filterMap f xs)[0]? = findSome? f xs
source
@[simp]
theorem Array.getElem_zero_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} (h : 0 < (filterMap f xs).size) :
(filterMap f xs)[0] = (findSome? f xs).get ⋯
source
@[simp]
theorem Array.back?_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α} :
(filterMap f xs).back? = findSomeRev? f xs
source
@[simp]
theorem Array.back!_filterMap {β : Type u_1} {α : Type u_2} [Inhabited β] {f : α → Option β} {xs : Array α} :
(filterMap f xs).back! = (findSomeRev? f xs).getD default
source
@[simp]
theorem Array.map_findSome? {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → γ} {xs : Array α} :
Option.map g (findSome? f xs) = findSome? (Option.map g ∘ f) xs
source
theorem Array.findSome?_map {β : Type u_1} {γ : Type u_2} {α✝ : Type u_3} {p : γ → Option α✝} {f : β → γ} {xs : Array β} :
findSome? p (map f xs) = findSome? (p ∘ f) xs
source
theorem Array.findSome?_append {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} {xs ys : Array α} :
findSome? f (xs ++ ys) = (findSome? f xs).or (findSome? f ys)
source
theorem Array.getElem?_zero_flatten {α : Type u_1} (xss : Array (Array α)) :
xss.flatten[0]? = findSome? (fun (xs : Array α) => xs[0]?) xss
source
theorem Array.getElem_zero_flatten.proof {α : Type u_1} {xss : Array (Array α)} (h : 0 < xss.flatten.size) :
(findSome? (fun (xs : Array α) => xs[0]?) xss).isSome = true
source
theorem Array.getElem_zero_flatten {α : Type u_1} {xss : Array (Array α)} (h : 0 < xss.flatten.size) :
xss.flatten[0] = (findSome? (fun (xs : Array α) => xs[0]?) xss).get ⋯
source
theorem Array.findSome?_replicate {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {n : Nat} {a : α✝} :
findSome? f (replicate n a) = if n = 0 then none else f a
source
@[reducible, inline, deprecated Array.findSome?_replicate (since := "2025-03-18")]
abbrev Array.findSome?_mkArray {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {n : Nat} {a : α✝} :
findSome? f (replicate n a) = if n = 0 then none else f a
Equations
source
@[simp]
theorem Array.findSome?_replicate_of_pos {n : Nat} {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {a : α✝} (h : 0 < n) :
findSome? f (replicate n a) = f a
source
@[reducible, inline, deprecated Array.findSome?_replicate_of_pos (since := "2025-03-18")]
abbrev Array.findSome?_mkArray_of_pos {n : Nat} {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {a : α✝} (h : 0 < n) :
findSome? f (replicate n a) = f a
Equations
source
@[simp]
theorem Array.findSome?_replicate_of_isSome {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {n : Nat} {a : α✝} :
(f a).isSome = true → findSome? f (replicate n a) = if n = 0 then none else f a
source
@[reducible, inline, deprecated Array.findSome?_replicate_of_isSome (since := "2025-03-18")]
abbrev Array.findSome?_mkArray_of_isSome {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {n : Nat} {a : α✝} :
(f a).isSome = true → findSome? f (replicate n a) = if n = 0 then none else f a
Equations
source
@[simp]
theorem Array.findSome?_replicate_of_isNone {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {n : Nat} {a : α✝} (h : (f a).isNone = true) :
findSome? f (replicate n a) = none
source
@[reducible, inline, deprecated Array.findSome?_replicate_of_isNone (since := "2025-03-18")]
abbrev Array.findSome?_mkArray_of_isNone {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {n : Nat} {a : α✝} (h : (f a).isNone = true) :
findSome? f (replicate n a) = none
Equations

find? #

source
@[simp]
theorem Array.find?_singleton {α : Type u_1} {a : α} {p : α → Bool} :
find? p #[a] = if p a = true then some a else none
source
@[simp]
theorem Array.findRev?_push_of_pos {α : Type} {p : α → Bool} {a : α} {xs : Array α} (h : p a = true) :
findRev? p (xs.push a) = some a
source
@[simp]
theorem Array.findRev?_cons_of_neg {α : Type} {p : α → Bool} {a : α} {xs : Array α} (h : ¬p a = true) :
findRev? p (xs.push a) = findRev? p xs
source
@[simp]
theorem Array.find?_eq_none {α✝ : Type u_1} {p : α✝ → Bool} {xs : Array α✝} :
find? p xs = none ↔ ∀ (x : α✝), x ∈ xs → ¬p x = true
source
theorem Array.find?_eq_some_iff_append {α : Type u_1} {p : α → Bool} {b : α} {xs : Array α} :
find? p xs = some b ↔ p b = true ∧ ∃ (as : Array α), ∃ (bs : Array α), xs = as.push b ++ bs ∧ ∀ (a : α), a ∈ as → (!p a) = true
source
@[simp]
theorem Array.find?_push_eq_some {α : Type u_1} {a : α} {p : α → Bool} {b : α} {xs : Array α} :
find? p (xs.push a) = some b ↔ find? p xs = some b ∨ find? p xs = none ∧ p a = true ∧ a = b
source
@[simp]
theorem Array.find?_isSome {α : Type u_1} {xs : Array α} {p : α → Bool} :
(find? p xs).isSome = true ↔ ∃ (x : α), x ∈ xs ∧ p x = true
source
theorem Array.find?_some {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α} (h : find? p xs = some a) :
p a = true
source
theorem Array.mem_of_find?_eq_some {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α} (h : find? p xs = some a) :
a ∈ xs
source
theorem Array.get_find?_mem {α : Type u_1} {p : α → Bool} {xs : Array α} (h : (find? p xs).isSome = true) :
(find? p xs).get h ∈ xs
source
@[simp]
theorem Array.find?_filter {α : Type u_1} {xs : Array α} (p q : α → Bool) :
find? q (filter p xs) = find? (fun (a : α) => decide (p a = true ∧ q a = true)) xs
source
@[simp]
theorem Array.getElem?_zero_filter {α : Type u_1} {p : α → Bool} {xs : Array α} :
(filter p xs)[0]? = find? p xs
source
@[simp]
theorem Array.getElem_zero_filter {α : Type u_1} {p : α → Bool} {xs : Array α} (h : 0 < (filter p xs).size) :
(filter p xs)[0] = (find? p xs).get ⋯
source
@[simp]
theorem Array.back?_filter {α : Type} {p : α → Bool} {xs : Array α} :
(filter p xs).back? = findRev? p xs
source
@[simp]
theorem Array.back!_filter {α : Type} [Inhabited α] {p : α → Bool} {xs : Array α} :
(filter p xs).back! = (findRev? p xs).get!
source
@[simp]
theorem Array.find?_filterMap {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Option β} {p : β → Bool} :
find? p (filterMap f xs) = (find? (fun (a : α) => Option.any p (f a)) xs).bind f
source
@[simp]
theorem Array.find?_map {β : Type u_1} {α : Type u_2} {p : α → Bool} {f : β → α} {xs : Array β} :
find? p (map f xs) = Option.map f (find? (p ∘ f) xs)
source
@[simp]
theorem Array.find?_append {α : Type u_1} {p : α → Bool} {xs ys : Array α} :
find? p (xs ++ ys) = (find? p xs).or (find? p ys)
source
@[simp]
theorem Array.find?_flatten {α : Type u_1} {xss : Array (Array α)} {p : α → Bool} :
find? p xss.flatten = findSome? (fun (x : Array α) => find? p x) xss
source
theorem Array.find?_flatten_eq_none_iff {α : Type u_1} {xss : Array (Array α)} {p : α → Bool} :
find? p xss.flatten = none ↔ ∀ (ys : Array α), ys ∈ xss → ∀ (x : α), x ∈ ys → (!p x) = true
source
@[reducible, inline, deprecated Array.find?_flatten_eq_none_iff (since := "2025-02-03")]
abbrev Array.find?_flatten_eq_none {α : Type u_1} {xss : Array (Array α)} {p : α → Bool} :
find? p xss.flatten = none ↔ ∀ (ys : Array α), ys ∈ xss → ∀ (x : α), x ∈ ys → (!p x) = true
Equations
source
theorem Array.find?_flatten_eq_some_iff {α : Type u_1} {xss : Array (Array α)} {p : α → Bool} {a : α} :
find? p xss.flatten = some a ↔ p a = true ∧ ∃ (as : Array (Array α)), ∃ (ys : Array α), ∃ (zs : Array α), ∃ (bs : Array (Array α)), xss = as.push (ys.push a ++ zs) ++ bs ∧ (∀ (ws : Array α), ws ∈ as → ∀ (x : α), x ∈ ws → (!p x) = true) ∧ ∀ (x : α), x ∈ ys → (!p x) = true

If find? p returns some a from xs.flatten, then p a holds, and some array in xs contains a, and no earlier element of that array satisfies p. Moreover, no earlier array in xs has an element satisfying p.

source
@[reducible, inline, deprecated Array.find?_flatten_eq_some_iff (since := "2025-02-03")]
abbrev Array.find?_flatten_eq_some {α : Type u_1} {xss : Array (Array α)} {p : α → Bool} {a : α} :
find? p xss.flatten = some a ↔ p a = true ∧ ∃ (as : Array (Array α)), ∃ (ys : Array α), ∃ (zs : Array α), ∃ (bs : Array (Array α)), xss = as.push (ys.push a ++ zs) ++ bs ∧ (∀ (ws : Array α), ws ∈ as → ∀ (x : α), x ∈ ws → (!p x) = true) ∧ ∀ (x : α), x ∈ ys → (!p x) = true
Equations
source
@[simp]
theorem Array.find?_flatMap {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} {p : β → Bool} :
find? p (flatMap f xs) = findSome? (fun (x : α) => find? p (f x)) xs
source
theorem Array.find?_flatMap_eq_none_iff {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} {p : β → Bool} :
find? p (flatMap f xs) = none ↔ ∀ (x : α), x ∈ xs → ∀ (y : β), y ∈ f x → (!p y) = true
source
@[reducible, inline, deprecated Array.find?_flatMap_eq_none_iff (since := "2025-02-03")]
abbrev Array.find?_flatMap_eq_none {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} {p : β → Bool} :
find? p (flatMap f xs) = none ↔ ∀ (x : α), x ∈ xs → ∀ (y : β), y ∈ f x → (!p y) = true
Equations
source
theorem Array.find?_replicate {α✝ : Type u_1} {p : α✝ → Bool} {n : Nat} {a : α✝} :
find? p (replicate n a) = if n = 0 then none else if p a = true then some a else none
source
@[reducible, inline, deprecated Array.find?_replicate (since := "2025-03-18")]
abbrev Array.find?_mkArray {α✝ : Type u_1} {p : α✝ → Bool} {n : Nat} {a : α✝} :
find? p (replicate n a) = if n = 0 then none else if p a = true then some a else none
Equations
source
@[simp]
theorem Array.find?_replicate_of_size_pos {n : Nat} {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} (h : 0 < n) :
find? p (replicate n a) = if p a = true then some a else none
source
@[reducible, inline, deprecated Array.find?_replicate_of_size_pos (since := "2025-03-18")]
abbrev Array.find?_mkArray_of_length_pos {n : Nat} {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} (h : 0 < n) :
find? p (replicate n a) = if p a = true then some a else none
Equations
source
@[simp]
theorem Array.find?_replicate_of_pos {α✝ : Type u_1} {p : α✝ → Bool} {n : Nat} {a : α✝} (h : p a = true) :
find? p (replicate n a) = if n = 0 then none else some a
source
@[reducible, inline, deprecated Array.find?_replicate_of_pos (since := "2025-03-18")]
abbrev Array.find?_mkArray_of_pos {α✝ : Type u_1} {p : α✝ → Bool} {n : Nat} {a : α✝} (h : p a = true) :
find? p (replicate n a) = if n = 0 then none else some a
Equations
source
@[simp]
theorem Array.find?_replicate_of_neg {α✝ : Type u_1} {p : α✝ → Bool} {n : Nat} {a : α✝} (h : ¬p a = true) :
find? p (replicate n a) = none
source
@[reducible, inline, deprecated Array.find?_replicate_of_neg (since := "2025-03-18")]
abbrev Array.find?_mkArray_of_neg {α✝ : Type u_1} {p : α✝ → Bool} {n : Nat} {a : α✝} (h : ¬p a = true) :
find? p (replicate n a) = none
Equations
source
theorem Array.find?_replicate_eq_none_iff {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} :
find? p (replicate n a) = none ↔ n = 0 ∨ (!p a) = true
source
@[reducible, inline, deprecated Array.find?_replicate_eq_none_iff (since := "2025-03-18")]
abbrev Array.find?_mkArray_eq_none_iff {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} :
find? p (replicate n a) = none ↔ n = 0 ∨ (!p a) = true
Equations
source
@[simp]
theorem Array.find?_replicate_eq_some_iff {α : Type u_1} {n : Nat} {a b : α} {p : α → Bool} :
find? p (replicate n a) = some b ↔ n ≠ 0 ∧ p a = true ∧ a = b
source
@[reducible, inline, deprecated Array.find?_replicate_eq_some_iff (since := "2025-03-18")]
abbrev Array.find?_mkArray_eq_some_iff {α : Type u_1} {n : Nat} {a b : α} {p : α → Bool} :
find? p (replicate n a) = some b ↔ n ≠ 0 ∧ p a = true ∧ a = b
Equations
source
@[reducible, inline, deprecated Array.find?_replicate_eq_some_iff (since := "2025-02-03")]
abbrev Array.find?_mkArray_eq_some {α : Type u_1} {n : Nat} {a b : α} {p : α → Bool} :
find? p (replicate n a) = some b ↔ n ≠ 0 ∧ p a = true ∧ a = b
Equations
source
@[simp]
theorem Array.get_find?_replicate {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} (h : (find? p (replicate n a)).isSome = true) :
(find? p (replicate n a)).get h = a
source
@[reducible, inline, deprecated Array.get_find?_replicate (since := "2025-03-18")]
abbrev Array.get_find?_mkArray {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} (h : (find? p (replicate n a)).isSome = true) :
(find? p (replicate n a)).get h = a
Equations
source
theorem Array.find?_pmap {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α} (H : ∀ (a : α), a ∈ xs → P a) {p : β → Bool} :
find? p (pmap f xs H) = Option.map (fun (x : { x : α // x ∈ xs }) => match x with | ⟨a, m⟩ => f a ⋯) (find? (fun (x : { x : α // x ∈ xs }) => match x with | ⟨a, m⟩ => p (f a ⋯)) xs.attach)
source
theorem Array.find?_eq_some_iff_getElem {α : Type u_1} {xs : Array α} {p : α → Bool} {b : α} :
find? p xs = some b ↔ p b = true ∧ ∃ (i : Nat), ∃ (h : i < xs.size), xs[i] = b ∧ ∀ (j : Nat) (hj : j < i), (!p xs[j]) = true

findIdx #

source
theorem Array.findIdx_of_getElem?_eq_some {α : Type u_1} {p : α → Bool} {y : α} {xs : Array α} (w : xs[findIdx p xs]? = some y) :
p y = true
source
theorem Array.findIdx_getElem {α : Type u_1} {p : α → Bool} {xs : Array α} {w : findIdx p xs < xs.size} :
p xs[findIdx p xs] = true
source
theorem Array.findIdx_lt_size_of_exists {α : Type u_1} {p : α → Bool} {xs : Array α} (h : ∃ (x : α), x ∈ xs ∧ p x = true) :
findIdx p xs < xs.size
source
theorem Array.findIdx_getElem?_eq_getElem_of_exists {α : Type u_1} {p : α → Bool} {xs : Array α} (h : ∃ (x : α), x ∈ xs ∧ p x = true) :
xs[findIdx p xs]? = some xs[findIdx p xs]
source
@[simp]
theorem Array.findIdx_eq_size {α : Type u_1} {p : α → Bool} {xs : Array α} :
findIdx p xs = xs.size ↔ ∀ (x : α), x ∈ xs → p x = false
source
theorem Array.findIdx_eq_size_of_false {α : Type u_1} {p : α → Bool} {xs : Array α} (h : ∀ (x : α), x ∈ xs → p x = false) :
findIdx p xs = xs.size
source
theorem Array.findIdx_le_size {α : Type u_1} {p : α → Bool} {xs : Array α} :
findIdx p xs ≤ xs.size
source
@[simp]
theorem Array.findIdx_lt_size {α : Type u_1} {p : α → Bool} {xs : Array α} :
findIdx p xs < xs.size ↔ ∃ (x : α), x ∈ xs ∧ p x = true
source
theorem Array.not_of_lt_findIdx {α : Type u_1} {p : α → Bool} {xs : Array α} {i : Nat} (h : i < findIdx p xs) :
p xs[i] = false

p does not hold for elements with indices less than xs.findIdx p.

source
theorem Array.le_findIdx_of_not {α : Type u_1} {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.size) (h2 : ∀ (j : Nat) (hji : j < i), p xs[j] = false) :
i ≤ findIdx p xs

If ¬ p xs[j] for all j < i, then i ≤ xs.findIdx p.

source
theorem Array.lt_findIdx_of_not {α : Type u_1} {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.size) (h2 : ∀ (j : Nat) (hji : j ≤ i), ¬p xs[j] = true) :
i < findIdx p xs

If ¬ p xs[j] for all j ≤ i, then i < xs.findIdx p.

source
theorem Array.findIdx_eq {α : Type u_1} {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.size) :
findIdx p xs = i ↔ p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), p xs[j] = false

xs.findIdx p = i iff p xs[i] and ¬ p xs [j] for all j < i.

source
theorem Array.findIdx_append {α : Type u_1} {p : α → Bool} {xs ys : Array α} :
findIdx p (xs ++ ys) = if findIdx p xs < xs.size then findIdx p xs else findIdx p ys + xs.size
source
theorem Array.findIdx_le_findIdx {α : Type u_1} {xs : Array α} {p q : α → Bool} (h : ∀ (x : α), x ∈ xs → p x = true → q x = true) :
findIdx q xs ≤ findIdx p xs
source
@[simp]
theorem Array.findIdx_subtype {α : Type u_1} {p : α → Prop} {xs : Array { x : α // p x }} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) :
findIdx f xs = findIdx g xs.unattach
source
theorem Array.false_of_mem_extract_findIdx {α : Type u_1} {x : α} {xs : Array α} {p : α → Bool} (h : x ∈ xs.extract 0 (findIdx p xs)) :
p x = false
source
@[simp]
theorem Array.findIdx_extract {α : Type u_1} {xs : Array α} {i : Nat} {p : α → Bool} :
findIdx p (xs.extract 0 i) = min i (findIdx p xs)
source
@[simp]
theorem Array.min_findIdx_findIdx {α : Type u_1} {xs : Array α} {p q : α → Bool} :
min (findIdx p xs) (findIdx q xs) = findIdx (fun (a : α) => p a || q a) xs

findIdx? #

source
@[simp]
theorem Array.findIdx?_empty {α : Type u_1} {p : α → Bool} :
findIdx? p #[] = none
source
@[simp]
theorem Array.findIdx?_eq_none_iff {α : Type u_1} {xs : Array α} {p : α → Bool} :
findIdx? p xs = none ↔ ∀ (x : α), x ∈ xs → p x = false
source
theorem Array.findIdx?_isSome {α : Type u_1} {xs : Array α} {p : α → Bool} :
(findIdx? p xs).isSome = xs.any p
source
theorem Array.findIdx?_isNone {α : Type u_1} {xs : Array α} {p : α → Bool} :
(findIdx? p xs).isNone = xs.all fun (x : α) => decide ¬p x = true
source
theorem Array.findIdx?_eq_some_iff_findIdx_eq {α : Type u_1} {xs : Array α} {p : α → Bool} {i : Nat} :
findIdx? p xs = some i ↔ i < xs.size ∧ findIdx p xs = i
source
theorem Array.findIdx?_eq_some_of_exists {α : Type u_1} {xs : Array α} {p : α → Bool} (h : ∃ (x : α), x ∈ xs ∧ p x = true) :
findIdx? p xs = some (findIdx p xs)
source
theorem Array.findIdx?_eq_none_iff_findIdx_eq {α : Type u_1} {xs : Array α} {p : α → Bool} :
findIdx? p xs = none ↔ findIdx p xs = xs.size
source
theorem Array.findIdx?_eq_guard_findIdx_lt {α : Type u_1} {xs : Array α} {p : α → Bool} :
findIdx? p xs = Option.guard (fun (i : Nat) => i < xs.size) (findIdx p xs)
source
theorem Array.findIdx?_eq_some_iff_getElem {α : Type u_1} {xs : Array α} {p : α → Bool} {i : Nat} :
findIdx? p xs = some i ↔ ∃ (h : i < xs.size), p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true
source
theorem Array.of_findIdx?_eq_some {α : Type u_1} {i : Nat} {xs : Array α} {p : α → Bool} (w : findIdx? p xs = some i) :
match xs[i]? with | some a => p a = true | none => false = true
source
theorem Array.of_findIdx?_eq_none {α : Type u_1} {xs : Array α} {p : α → Bool} (w : findIdx? p xs = none) (i : Nat) :
match xs[i]? with | some a => ¬p a = true | none => true = true
source
@[simp]
theorem Array.findIdx?_map {β : Type u_1} {α : Type u_2} {f : β → α} {xs : Array β} {p : α → Bool} :
findIdx? p (map f xs) = findIdx? (p ∘ f) xs
source
@[simp]
theorem Array.findIdx?_append {α : Type u_1} {xs ys : Array α} {p : α → Bool} :
findIdx? p (xs ++ ys) = (findIdx? p xs).or (Option.map (fun (i : Nat) => i + xs.size) (findIdx? p ys))
source
theorem Array.findIdx?_flatten {α : Type u_1} {xss : Array (Array α)} {p : α → Bool} :
findIdx? p xss.flatten = Option.map (fun (i : Nat) => (map size (xss.take i)).sum + (Option.map (fun (xs : Array α) => findIdx p xs) xss[i]?).getD 0) (findIdx? (fun (x : Array α) => x.any p) xss)
source
@[simp]
theorem Array.findIdx?_replicate {n : Nat} {α✝ : Type u_1} {a : α✝} {p : α✝ → Bool} :
findIdx? p (replicate n a) = if 0 < n ∧ p a = true then some 0 else none
source
@[reducible, inline, deprecated Array.findIdx?_replicate (since := "2025-03-18")]
abbrev Array.findIdx?_mkArray {n : Nat} {α✝ : Type u_1} {a : α✝} {p : α✝ → Bool} :
findIdx? p (replicate n a) = if 0 < n ∧ p a = true then some 0 else none
Equations
source
theorem Array.findIdx?_eq_findSome?_zipIdx {α : Type u_1} {xs : Array α} {p : α → Bool} :
findIdx? p xs = findSome? (fun (x : α × Nat) => match x with | (a, i) => if p a = true then some i else none) xs.zipIdx
source
theorem Array.findIdx?_eq_fst_find?_zipIdx {α : Type u_1} {xs : Array α} {p : α → Bool} :
findIdx? p xs = Option.map (fun (x : α × Nat) => x.snd) (find? (fun (x : α × Nat) => match x with | (x, snd) => p x) xs.zipIdx)
source
theorem Array.findIdx?_eq_none_of_findIdx?_eq_none {α : Type u_1} {xs : Array α} {p q : α → Bool} (w : ∀ (x : α), x ∈ xs → p x = true → q x = true) :
findIdx? q xs = none → findIdx? p xs = none
source
theorem Array.findIdx_eq_getD_findIdx? {α : Type u_1} {xs : Array α} {p : α → Bool} :
findIdx p xs = (findIdx? p xs).getD xs.size
source
theorem Array.findIdx?_eq_some_le_of_findIdx?_eq_some {α : Type u_1} {xs : Array α} {p q : α → Bool} (w : ∀ (x : α), x ∈ xs → p x = true → q x = true) {i : Nat} (h : findIdx? p xs = some i) :
∃ (j : Nat), j ≤ i ∧ findIdx? q xs = some j
source
@[simp]
theorem Array.findIdx?_subtype {α : Type u_1} {p : α → Prop} {xs : Array { x : α // p x }} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) :
findIdx? f xs = findIdx? g xs.unattach
source
@[simp]
theorem Array.findIdx?_take {α : Type u_1} {xs : Array α} {i : Nat} {p : α → Bool} :
findIdx? p (xs.take i) = (findIdx? p xs).bind (Option.guard fun (j : Nat) => j < i)

findFinIdx? #

source
@[simp]
theorem Array.findFinIdx?_empty {α : Type u_1} {p : α → Bool} :
findFinIdx? p #[] = none
source
theorem Array.findFinIdx?_congr {α : Type u_1} {p : α → Bool} {xs ys : Array α} (w : xs = ys) :
findFinIdx? p xs = Option.map (fun (i : Fin ys.size) => Fin.cast ⋯ i) (findFinIdx? p ys)
source
theorem Array.findFinIdx?_eq_pmap_findIdx? {α : Type u_1} {xs : Array α} {p : α → Bool} :
findFinIdx? p xs = Option.pmap (fun (i : Nat) (m : i ∈ findIdx? p xs) => ⟨i, ⋯⟩) (findIdx? p xs) ⋯
source
@[simp]
theorem Array.findFinIdx?_eq_none_iff {α : Type u_1} {xs : Array α} {p : α → Bool} :
findFinIdx? p xs = none ↔ ∀ (x : α), x ∈ xs → ¬p x = true
source
@[simp]
theorem Array.findFinIdx?_eq_some_iff {α : Type u_1} {xs : Array α} {p : α → Bool} {i : Fin xs.size} :
findFinIdx? p xs = some i ↔ p xs[i] = true ∧ ∀ (j : Fin xs.size) (hji : j < i), ¬p xs[j] = true
source
@[simp]
theorem Array.findFinIdx?_subtype {α : Type u_1} {p : α → Prop} {xs : Array { x : α // p x }} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) :
findFinIdx? f xs = Option.map (fun (i : Fin xs.unattach.size) => Fin.cast ⋯ i) (findFinIdx? g xs.unattach)

idxOf #

The verification API for idxOf is still incomplete. The lemmas below should be made consistent with those for findIdx (and proved using them).

source
theorem Array.idxOf_append {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : Array α} {a : α} :
idxOf a (xs ++ ys) = if a ∈ xs then idxOf a xs else idxOf a ys + xs.size
source
theorem Array.idxOf_eq_size {α : Type u_1} {a : α} [BEq α] [LawfulBEq α] {xs : Array α} (h : ¬a ∈ xs) :
idxOf a xs = xs.size
source
theorem Array.idxOf_lt_length {α : Type u_1} {a : α} [BEq α] [LawfulBEq α] {xs : Array α} (h : a ∈ xs) :
idxOf a xs < xs.size

idxOf? #

The verification API for idxOf? is still incomplete. The lemmas below should be made consistent with those for findIdx? (and proved using them).

source
@[simp]
theorem Array.idxOf?_empty {α : Type u_1} {a : α} [BEq α] :
#[].idxOf? a = none
source
@[simp]
theorem Array.idxOf?_eq_none_iff {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
xs.idxOf? a = none ↔ ¬a ∈ xs

finIdxOf? #

The verification API for finIdxOf? is still incomplete. The lemmas below should be made consistent with those for findFinIdx? (and proved using them).

source
theorem Array.idxOf?_eq_map_finIdxOf?_val {α : Type u_1} [BEq α] {xs : Array α} {a : α} :
xs.idxOf? a = Option.map (fun (x : Fin xs.size) => ↑x) (xs.finIdxOf? a)
source
@[simp]
theorem Array.finIdxOf?_empty {α : Type u_1} {a : α} [BEq α] :
#[].finIdxOf? a = none
source
@[simp]
theorem Array.finIdxOf?_eq_none_iff {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
xs.finIdxOf? a = none ↔ ¬a ∈ xs
source
@[simp]
theorem Array.finIdxOf?_eq_some_iff {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} {a : α} {i : Fin xs.size} :
xs.finIdxOf? a = some i ↔ xs[i] = a ∧ ∀ (j : Fin xs.size), j < i → ¬xs[j] = a