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

findSome?

@[simp]

theorem Array.findSome?_empty {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} : findSome? f #[] = none

@[simp]

theorem Array.findSome?_push {α : Type u_1} {a : α} {α✝ : Type u_2} {f : α → Option α✝} {xs : Array α} : findSome? f (xs.push a) = (findSome? f xs).or (f a)

theorem Array.findSome?_singleton {α : Type u_1} {β : Type u_2} {a : α} {f : α → Option β} : findSome? f #[a] = f a

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

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

theorem Array.findSomeRev?_push {α : Type u_1} {β : Type u_2} {xs : Array α} {a : α} {f : α → Option β} : findSomeRev? f (xs.push a) = (f a).or (findSomeRev? f xs)

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

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

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

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

theorem Array.isSome_findSome? {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Option β} : (findSome? f xs).isSome = xs.any fun (x : α) => (f x).isSome

@[simp]

theorem Array.findSome?_guard {α : Type u_1} {p : α → Bool} {xs : Array α} : findSome? (Option.guard p) xs = find? p xs

theorem Array.find?_eq_findSome?_guard {α : Type u_1} {p : α → Bool} {xs : Array α} : find? p xs = findSome? (Option.guard p) xs

@[simp]

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

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

@[simp]

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

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

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

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

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)

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

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

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 ⋯

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

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

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

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

find?

@[simp]

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

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 : α} {xs : Array α} (h : p a = true) : findRev? p (xs.push a) = some a

@[simp]

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

theorem Array.finRev?_push {α : Type} {p : α → Bool} {a : α} {xs : Array α} : findRev? p (xs.push a) = (Option.guard p a).or (findRev? p xs)

@[simp]

theorem Array.find?_eq_none {α✝ : Type u_1} {p : α✝ → Bool} {xs : Array α✝} : find? p xs = none ↔ ∀ (x : α✝), x ∈ xs → ¬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

theorem Array.isSome_find? {α : Type u_1} {xs : Array α} {f : α → Bool} : (find? f xs).isSome = xs.any fun (x : α) => f x

theorem Array.find?_push {α : Type u_1} {a : α} {p : α → Bool} {xs : Array α} : find? p (xs.push a) = (find? p xs).or (if p a = true then some a else none)

@[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} {xs : Array α} : (filter p xs)[0]? = find? p xs

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

@[simp]

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

@[simp]

theorem Array.back!_filter {α : Type} [Inhabited α] {p : α → Bool} {xs : Array α} : (filter p xs).back! = (findRev? p xs).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} {xs ys : Array α} : find? p (xs ++ ys) = (find? p xs).or (find? p ys)

@[simp]

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

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

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.

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

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

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

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

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

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

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

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

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

findIdx

theorem Array.findIdx_empty {α✝ : Type u_1} {p : α✝ → Bool} : findIdx p #[] = 0

theorem Array.findIdx_singleton {α : Type u_1} {a : α} {p : α → Bool} : findIdx p #[a] = if p a = true then 0 else 1

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} {xs ys : Array α} : findIdx p (xs ++ ys) = if findIdx p xs < xs.size then findIdx p xs else findIdx p ys + xs.size

theorem Array.findIdx_push {α : Type u_1} {xs : Array α} {a : α} {p : α → Bool} : findIdx p (xs.push a) = if findIdx p xs < xs.size then findIdx p xs else xs.size + if p a = true then 0 else 1

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

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

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

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

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

@[simp]

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

theorem Array.findIdx?_singleton {α : Type u_1} {a : α} {p : α → Bool} : findIdx? p #[a] = if p a = true then some 0 else 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

@[simp]

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

@[simp]

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) => decide (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} {f : β → α} {xs : Array β} {p : α → Bool} : findIdx? p (map f xs) = findIdx? (p ∘ f) xs

@[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?_push {α : Type u_1} {xs : Array α} {a : α} {p : α → Bool} : findIdx? p (xs.push a) = (findIdx? p xs).or (if p a = true then some xs.size else none)

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)

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

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} {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

@[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) => decide (j < i))

findFinIdx?

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

theorem Array.findFinIdx?_singleton {α : Type u_1} {a : α} {p : α → Bool} : findFinIdx? p #[a] = if p a = true then some ⟨0, ⋯⟩ else none

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)

theorem Array.findFinIdx?_eq_pmap_findIdx? {α : Type u_1} {xs : Array α} {p : α → Bool} : findFinIdx? p xs = Option.pmap (fun (i : Nat) (m : findIdx? p xs = some i) => ⟨i, ⋯⟩) (findIdx? p xs) ⋯

@[simp]

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

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

theorem Array.findFinIdx?_push {α : Type u_1} {xs : Array α} {a : α} {p : α → Bool} : findFinIdx? p (xs.push a) = (Option.map (Fin.castLE ⋯) (findFinIdx? p xs)).or (if p a = true then some ⟨xs.size, ⋯⟩ else none)

theorem Array.findFinIdx?_append {α : Type u_1} {xs ys : Array α} {p : α → Bool} : findFinIdx? p (xs ++ ys) = (Option.map (Fin.castLE ⋯) (findFinIdx? p xs)).or (Option.map (Fin.cast ⋯) (Option.map (Fin.natAdd xs.size) (findFinIdx? p ys)))

@[simp]

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

@[simp]

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

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

find? and findFinIdx?

theorem Array.find?_eq_map_findFinIdx?_getElem {α : Type u_1} {xs : Array α} {p : α → Bool} : find? p xs = Option.map (fun (x : Fin xs.size) => xs[x]) (findFinIdx? p xs)

theorem Array.find?_eq_bind_findIdx?_getElem? {α : Type u_1} {xs : Array α} {p : α → Bool} : find? p xs = (findIdx? p xs).bind fun (x : Nat) => xs[x]?

theorem Array.find?_eq_getElem?_findIdx {α : Type u_1} {xs : Array α} {p : α → Bool} : find? p xs = xs[findIdx p xs]?

theorem Array.findIdx?_eq_bind_find?_idxOf? {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} {p : α → Bool} : findIdx? p xs = (find? p xs).bind fun (x : α) => xs.idxOf? x

theorem Array.findFinIdx?_eq_bind_find?_finIdxOf? {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} {p : α → Bool} : findFinIdx? p xs = (find? p xs).bind fun (x : α) => xs.finIdxOf? x

theorem Array.findIdx_eq_getD_bind_find?_idxOf? {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} {p : α → Bool} : findIdx p xs = ((find? p xs).bind fun (x : α) => xs.idxOf? x).getD 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).

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

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

theorem Array.idxOf_lt_length_of_mem {α : Type u_1} {a : α} [BEq α] [LawfulBEq α] {xs : Array α} (h : a ∈ xs) : idxOf a xs < xs.size

theorem Array.idxOf_le_size {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : idxOf a xs ≤ xs.size

theorem Array.idxOf_lt_size_iff {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : idxOf a xs < xs.size ↔ a ∈ xs

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?_empty {α : Type u_1} {a : α} [BEq α] : #[].idxOf? a = none

@[simp]

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

@[simp]

theorem Array.isSome_idxOf? {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : (xs.idxOf? a).isSome = true ↔ a ∈ xs

theorem Array.isNone_idxOf? {α : Type u_1} [BEq α] [LawfulBEq α] {xs : Array α} {a : α} : ((xs.idxOf? a).isNone = true) = ¬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).

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)

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

@[simp]

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

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

@[simp]

theorem Array.isSome_finIdxOf? {α : Type u_1} [BEq α] [PartialEquivBEq α] {xs : Array α} {a : α} : (xs.finIdxOf? a).isSome = xs.contains a

@[simp]

theorem Array.isNone_finIdxOf? {α : Type u_1} [BEq α] [PartialEquivBEq α] {xs : Array α} {a : α} : (xs.finIdxOf? a).isNone = !xs.contains a