Lemmas about Array.findSome?, Array.find?.

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

@[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 {α : Type u_1} {xs : Array (Array α)} {p : α → Bool} : find? p xs.flatten = none ↔ ∀ (ys : Array α), ys ∈ xs → ∀ (x : α), x ∈ ys → (!p x) = true

theorem 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

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 {α : 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?_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 {α : Type u_1} {n : Nat} {a : α} {p : α → Bool} : find? p (mkArray n a) = none ↔ n = 0 ∨ (!p a) = true

@[simp]

theorem 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

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