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

findSome?

@[simp]

theorem Array.findSomeRev?_push_of_isSome {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} {a : α} (l : Array α) (h : (f a).isSome = true) : findSomeRev? f (l.push a) = f a

@[simp]

theorem Array.findSomeRev?_push_of_isNone {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} {a : α} (l : Array α) (h : (f a).isNone = true) : findSomeRev? f (l.push a) = findSomeRev? f l

theorem Array.exists_of_findSome?_eq_some {α : Type u_1} {β : Type u_2} {b : β} {f : α → Option β} {l : Array α} (w : findSome? f l = some b) : ∃ (a : α), a ∈ l ∧ f a = some b

@[simp]

theorem Array.findSome?_eq_none_iff {α✝ : Type u_1} {α✝¹ : Type u_2} {p : α✝ → Option α✝¹} {l : Array α✝} : findSome? p l = none ↔ ∀ (x : α✝), x ∈ l → p x = none

@[simp]

theorem Array.findSome?_isSome_iff {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : Array α} : (findSome? f l).isSome = true ↔ ∃ (x : α), x ∈ l ∧ (f x).isSome = true

theorem Array.findSome?_eq_some_iff {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : Array α} {b : β} : findSome? f l = some b ↔ ∃ (l₁ : Array α), ∃ (a : α), ∃ (l₂ : Array α), l = l₁.push a ++ l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

@[simp]

theorem Array.findSome?_guard {α : Type u_1} {p : α → Bool} (l : Array α) : findSome? (Option.guard fun (x : α) => p x = true) l = find? p l

theorem Array.find?_eq_findSome?_guard {α : Type u_1} {p : α → Bool} (l : Array α) : find? p l = findSome? (Option.guard fun (x : α) => p x = true) l

@[simp]

theorem Array.getElem?_zero_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : Array α) : (filterMap f l)[0]? = findSome? f l

@[simp]

theorem Array.getElem_zero_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : Array α) (h : 0 < (filterMap f l).size) : (filterMap f l)[0] = (findSome? f l).get ⋯

@[simp]

theorem Array.back?_filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : Array α) : (filterMap f l).back? = findSomeRev? f l

@[simp]

theorem Array.back!_filterMap {β : Type u_1} {α : Type u_2} [Inhabited β] (f : α → Option β) (l : Array α) : (filterMap f l).back! = (findSomeRev? f l).getD default

@[simp]

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

theorem Array.findSome?_map {β : Type u_1} {γ : Type u_2} {α✝ : Type u_3} {p : γ → Option α✝} (f : β → γ) (l : Array β) : findSome? p (map f l) = findSome? (p ∘ f) l

theorem Array.findSome?_append {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} {l₁ l₂ : Array α} : findSome? f (l₁ ++ l₂) = (findSome? f l₁).or (findSome? f l₂)

theorem Array.getElem?_zero_flatten {α : Type u_1} (L : Array (Array α)) : L.flatten[0]? = findSome? (fun (l : Array α) => l[0]?) L

theorem Array.getElem_zero_flatten.proof {α : Type u_1} {L : Array (Array α)} (h : 0 < L.flatten.size) : (findSome? (fun (l : Array α) => l[0]?) L).isSome = true

theorem Array.getElem_zero_flatten {α : Type u_1} {L : Array (Array α)} (h : 0 < L.flatten.size) : L.flatten[0] = (findSome? (fun (l : Array α) => l[0]?) L).get ⋯

theorem Array.back?_flatten {α : Type u_1} {L : Array (Array α)} : L.flatten.back? = findSomeRev? (fun (l : Array α) => l.back?) L

theorem Array.findSome?_mkArray {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {n : Nat} {a : α✝} : findSome? f (mkArray n a) = if n = 0 then none else f a

@[simp]

theorem Array.findSome?_mkArray_of_pos {n : Nat} {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {a : α✝} (h : 0 < n) : findSome? f (mkArray n a) = f a

@[simp]

theorem Array.findSome?_mkArray_of_isSome {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {n : Nat} {a : α✝} : (f a).isSome = true → findSome? f (mkArray n a) = if n = 0 then none else f a

@[simp]

theorem Array.findSome?_mkArray_of_isNone {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {n : Nat} {a : α✝} (h : (f a).isNone = true) : findSome? f (mkArray n a) = none

find?

@[simp]

theorem Array.find?_singleton {α : Type u_1} (a : α) (p : α → Bool) : find? p #[a] = if p a = true then some a else none

@[simp]

theorem Array.findRev?_push_of_pos {α : Type} {p : α → Bool} {a : α} (l : Array α) (h : p a = true) : findRev? p (l.push a) = some a

@[simp]

theorem Array.findRev?_cons_of_neg {α : Type} {p : α → Bool} {a : α} (l : Array α) (h : ¬p a = true) : findRev? p (l.push a) = findRev? p l

@[simp]

theorem Array.find?_eq_none {α✝ : Type u_1} {p : α✝ → Bool} {l : Array α✝} : find? p l = none ↔ ∀ (x : α✝), x ∈ l → ¬p x = true

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

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

@[simp]

theorem Array.find?_isSome {α : Type u_1} {xs : Array α} {p : α → Bool} : (find? p xs).isSome = true ↔ ∃ (x : α), x ∈ xs ∧ p x = true

theorem Array.find?_some {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α} (h : find? p xs = some a) : p a = true

theorem Array.mem_of_find?_eq_some {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α} (h : find? p xs = some a) : a ∈ xs

theorem Array.get_find?_mem {α : Type u_1} {p : α → Bool} {xs : Array α} (h : (find? p xs).isSome = true) : (find? p xs).get h ∈ xs

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

@[simp]

theorem Array.getElem?_zero_filter {α : Type u_1} (p : α → Bool) (l : Array α) : (filter p l)[0]? = find? p l

@[simp]

theorem Array.getElem_zero_filter {α : Type u_1} (p : α → Bool) (l : Array α) (h : 0 < (filter p l).size) : (filter p l)[0] = (find? p l).get ⋯

@[simp]

theorem Array.back?_filter {α : Type} (p : α → Bool) (l : Array α) : (filter p l).back? = findRev? p l

@[simp]

theorem Array.back!_filter {α : Type} [Inhabited α] (p : α → Bool) (l : Array α) : (filter p l).back! = (findRev? p l).get!

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

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

@[simp]

theorem Array.find?_append {α : Type u_1} {p : α → Bool} {l₁ l₂ : Array α} : find? p (l₁ ++ l₂) = (find? p l₁).or (find? p l₂)

@[simp]

theorem Array.find?_flatten {α : Type u_1} (xs : Array (Array α)) (p : α → Bool) : find? p xs.flatten = findSome? (fun (x : Array α) => find? p x) xs

theorem Array.find?_flatten_eq_none_iff {α : Type u_1} {xs : Array (Array α)} {p : α → Bool} : find? p xs.flatten = none ↔ ∀ (ys : Array α), ys ∈ xs → ∀ (x : α), x ∈ ys → (!p x) = true

@[reducible, inline, deprecated Array.find?_flatten_eq_none_iff (since := "2025-02-03")]

abbrev Array.find?_flatten_eq_none {α : Type u_1} {xs : Array (Array α)} {p : α → Bool} : find? p xs.flatten = none ↔ ∀ (ys : Array α), ys ∈ xs → ∀ (x : α), x ∈ ys → (!p x) = true

Equations

• @Array.find?_flatten_eq_none = @Array.find?_flatten_eq_none_iff

theorem Array.find?_flatten_eq_some_iff {α : Type u_1} {xs : Array (Array α)} {p : α → Bool} {a : α} : find? p xs.flatten = some a ↔ p a = true ∧ ∃ (as : Array (Array α)), ∃ (ys : Array α), ∃ (zs : Array α), ∃ (bs : Array (Array α)), xs = as.push (ys.push a ++ zs) ++ bs ∧ (∀ (a : Array α), a ∈ as → ∀ (x : α), x ∈ a → (!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.

@[reducible, inline, deprecated Array.find?_flatten_eq_some_iff (since := "2025-02-03")]

abbrev Array.find?_flatten_eq_some {α : Type u_1} {xs : Array (Array α)} {p : α → Bool} {a : α} : find? p xs.flatten = some a ↔ p a = true ∧ ∃ (as : Array (Array α)), ∃ (ys : Array α), ∃ (zs : Array α), ∃ (bs : Array (Array α)), xs = as.push (ys.push a ++ zs) ++ bs ∧ (∀ (a : Array α), a ∈ as → ∀ (x : α), x ∈ a → (!p x) = true) ∧ ∀ (x : α), x ∈ ys → (!p x) = true

Equations

• @Array.find?_flatten_eq_some = @Array.find?_flatten_eq_some_iff

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

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

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

• @Array.find?_flatMap_eq_none = @Array.find?_flatMap_eq_none_iff

theorem Array.find?_mkArray {α✝ : Type u_1} {p : α✝ → Bool} {n : Nat} {a : α✝} : find? p (mkArray n a) = if n = 0 then none else if p a = true then some a else none

@[simp]

theorem Array.find?_mkArray_of_length_pos {n : Nat} {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} (h : 0 < n) : find? p (mkArray n a) = if p a = true then some a else none

@[simp]

theorem Array.find?_mkArray_of_pos {α✝ : Type u_1} {p : α✝ → Bool} {n : Nat} {a : α✝} (h : p a = true) : find? p (mkArray n a) = if n = 0 then none else some a

@[simp]

theorem Array.find?_mkArray_of_neg {α✝ : Type u_1} {p : α✝ → Bool} {n : Nat} {a : α✝} (h : ¬p a = true) : find? p (mkArray n a) = none

theorem Array.find?_mkArray_eq_none_iff {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} : find? p (mkArray n a) = none ↔ n = 0 ∨ (!p a) = true

@[reducible, inline, deprecated Array.find?_mkArray_eq_none_iff (since := "2025-02-03")]

abbrev Array.find?_mkArray_eq_none {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} : find? p (mkArray n a) = none ↔ n = 0 ∨ (!p a) = true

Equations

• @Array.find?_mkArray_eq_none = @Array.find?_mkArray_eq_none_iff

@[simp]

theorem Array.find?_mkArray_eq_some_iff {α : Type u_1} {n : Nat} {a b : α} {p : α → Bool} : find? p (mkArray n a) = some b ↔ n ≠ 0 ∧ p a = true ∧ a = b

@[reducible, inline, deprecated Array.find?_mkArray_eq_some_iff (since := "2025-02-03")]

abbrev Array.find?_mkArray_eq_some {α : Type u_1} {n : Nat} {a b : α} {p : α → Bool} : find? p (mkArray n a) = some b ↔ n ≠ 0 ∧ p a = true ∧ a = b

Equations

• @Array.find?_mkArray_eq_some = @Array.find?_mkArray_eq_some_iff

@[simp]

theorem Array.get_find?_mkArray {α : Type u_1} (n : Nat) (a : α) (p : α → Bool) (h : (find? p (mkArray n a)).isSome = true) : (find? p (mkArray n a)).get h = a

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)

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

findFinIdx?

@[simp]

theorem Array.findFinIdx?_empty {α : Type u_1} {p : α → Bool} : findFinIdx? p #[] = none

theorem Array.findFinIdx?_congr {α : Type u_1} {p : α → Bool} {l₁ l₂ : Array α} (w : l₁ = l₂) : findFinIdx? p l₁ = Option.map (fun (i : Fin l₂.size) => Fin.cast ⋯ i) (findFinIdx? p l₂)

@[simp]

theorem Array.findFinIdx?_subtype {α : Type u_1} {p : α → Prop} {l : Array { x : α // p x }} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : findFinIdx? f l = Option.map (fun (i : Fin l.unattach.size) => Fin.cast ⋯ i) (findFinIdx? g l.unattach)

findIdx

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

theorem Array.findIdx_getElem {α : Type u_1} {p : α → Bool} {xs : Array α} {w : findIdx p xs < xs.size} : p xs[findIdx p xs] = true

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

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]

@[simp]

theorem Array.findIdx_eq_size {α : Type u_1} {p : α → Bool} {xs : Array α} : findIdx p xs = xs.size ↔ ∀ (x : α), x ∈ xs → p x = false

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

theorem Array.findIdx_le_size {α : Type u_1} (p : α → Bool) {xs : Array α} : findIdx p xs ≤ xs.size

@[simp]

theorem Array.findIdx_lt_size {α : Type u_1} {p : α → Bool} {xs : Array α} : findIdx p xs < xs.size ↔ ∃ (x : α), x ∈ xs ∧ p x = true

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.

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.

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.

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.

theorem Array.findIdx_append {α : Type u_1} (p : α → Bool) (l₁ l₂ : Array α) : findIdx p (l₁ ++ l₂) = if findIdx p l₁ < l₁.size then findIdx p l₁ else findIdx p l₂ + l₁.size

theorem Array.findIdx_le_findIdx {α : Type u_1} {l : Array α} {p q : α → Bool} (h : ∀ (x : α), x ∈ l → p x = true → q x = true) : findIdx q l ≤ findIdx p l

@[simp]

theorem Array.findIdx_subtype {α : Type u_1} {p : α → Prop} {l : Array { x : α // p x }} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : findIdx f l = findIdx g l.unattach

findIdx?

@[simp]

theorem Array.findIdx?_empty {α : Type u_1} {p : α → Bool} : findIdx? p #[] = none

@[simp]

theorem Array.findIdx?_eq_none_iff {α : Type u_1} {xs : Array α} {p : α → Bool} : findIdx? p xs = none ↔ ∀ (x : α), x ∈ xs → p x = false

theorem Array.findIdx?_isSome {α : Type u_1} {xs : Array α} {p : α → Bool} : (findIdx? p xs).isSome = xs.any p

theorem Array.findIdx?_isNone {α : Type u_1} {xs : Array α} {p : α → Bool} : (findIdx? p xs).isNone = xs.all fun (x : α) => decide ¬p x = true

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

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)

theorem Array.findIdx?_eq_none_iff_findIdx_eq {α : Type u_1} {xs : Array α} {p : α → Bool} : findIdx? p xs = none ↔ findIdx p xs = xs.size

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)

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

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

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

@[simp]

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

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

theorem Array.findIdx?_flatten {α : Type u_1} {l : Array (Array α)} {p : α → Bool} : findIdx? p l.flatten = Option.map (fun (i : Nat) => (map size (l.take i)).sum + (Option.map (fun (xs : Array α) => findIdx p xs) l[i]?).getD 0) (findIdx? (fun (x : Array α) => x.any p) l)

@[simp]

theorem Array.findIdx?_mkArray {n : Nat} {α✝ : Type u_1} {a : α✝} {p : α✝ → Bool} : findIdx? p (mkArray n a) = if 0 < n ∧ p a = true then some 0 else none

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

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)

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

theorem Array.findIdx_eq_getD_findIdx? {α : Type u_1} {xs : Array α} {p : α → Bool} : findIdx p xs = (findIdx? p xs).getD xs.size

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

@[simp]

theorem Array.findIdx?_subtype {α : Type u_1} {p : α → Prop} {l : Array { x : α // p x }} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : findIdx? f l = findIdx? g l.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).

theorem Array.idxOf_append {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ : Array α} {a : α} : idxOf a (l₁ ++ l₂) = if a ∈ l₁ then idxOf a l₁ else idxOf a l₂ + l₁.size

theorem Array.idxOf_eq_size {α : Type u_1} {a : α} [BEq α] [LawfulBEq α] {l : Array α} (h : ¬a ∈ l) : idxOf a l = l.size

theorem Array.idxOf_lt_length {α : Type u_1} {a : α} [BEq α] [LawfulBEq α] {l : Array α} (h : a ∈ l) : idxOf a l < l.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).

@[simp]

theorem Array.idxOf?_empty {α : Type u_1} {a : α} [BEq α] : #[].idxOf? a = none

@[simp]

theorem Array.idxOf?_eq_none_iff {α : Type u_1} [BEq α] [LawfulBEq α] {l : Array α} {a : α} : l.idxOf? a = none ↔ ¬a ∈ l

finIdxOf?

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)