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)
:
Array.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)
:
Array.findSomeRev? f (l.push a) = Array.findSomeRev? f l
@[simp]
theorem
Array.findSome?_guard
{α : Type u_1}
{p : α → Bool}
(l : Array α)
:
Array.findSome? (Option.guard fun (x : α) => p x = true) l = Array.find? p l
@[simp]
theorem
Array.getElem?_zero_filterMap
{α : Type u_1}
{β : Type u_2}
(f : α → Option β)
(l : Array α)
:
(Array.filterMap f l)[0]? = Array.findSome? f l
@[simp]
theorem
Array.getElem_zero_filterMap
{α : Type u_1}
{β : Type u_2}
(f : α → Option β)
(l : Array α)
(h : 0 < (Array.filterMap f l).size)
:
(Array.filterMap f l)[0] = (Array.findSome? f l).get ⋯
@[simp]
theorem
Array.back?_filterMap
{α : Type u_1}
{β : Type u_2}
(f : α → Option β)
(l : Array α)
:
(Array.filterMap f l).back? = Array.findSomeRev? f l
@[simp]
theorem
Array.back!_filterMap
{β : Type u_1}
{α : Type u_2}
[Inhabited β]
(f : α → Option β)
(l : Array α)
:
(Array.filterMap f l).back! = (Array.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 (Array.findSome? f l) = Array.findSome? (Option.map g ∘ f) l
theorem
Array.findSome?_map
{β : Type u_1}
{γ : Type u_2}
{α✝ : Type u_3}
{p : γ → Option α✝}
(f : β → γ)
(l : Array β)
:
Array.findSome? p (Array.map f l) = Array.findSome? (p ∘ f) l
theorem
Array.findSome?_append
{α : Type u_1}
{α✝ : Type u_2}
{f : α → Option α✝}
{l₁ l₂ : Array α}
:
Array.findSome? f (l₁ ++ l₂) = (Array.findSome? f l₁).or (Array.findSome? f l₂)
theorem
Array.getElem?_zero_flatten
{α : Type u_1}
(L : Array (Array α))
:
L.flatten[0]? = Array.findSome? (fun (l : Array α) => l[0]?) L
theorem
Array.getElem_zero_flatten.proof
{α : Type u_1}
{L : Array (Array α)}
(h : 0 < L.flatten.size)
:
(Array.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] = (Array.findSome? (fun (l : Array α) => l[0]?) L).get ⋯
theorem
Array.back?_flatten
{α : Type u_1}
{L : Array (Array α)}
:
L.flatten.back? = Array.findSomeRev? (fun (l : Array α) => l.back?) L
@[simp]
theorem
Array.findSome?_mkArray_of_pos
{n : Nat}
{α✝ : Type u_1}
{α✝¹ : Type u_2}
{f : α✝ → Option α✝¹}
{a : α✝}
(h : 0 < n)
:
Array.findSome? f (mkArray n a) = f a
find? #
@[simp]
@[simp]
theorem
Array.findRev?_push_of_pos
{α : Type}
{p : α → Bool}
{a : α}
(l : Array α)
(h : p a = true)
:
Array.findRev? p (l.push a) = some a
@[simp]
theorem
Array.findRev?_cons_of_neg
{α : Type}
{p : α → Bool}
{a : α}
(l : Array α)
(h : ¬p a = true)
:
Array.findRev? p (l.push a) = Array.findRev? p l
theorem
Array.find?_some
{α : Type u_1}
{p : α → Bool}
{a : α}
{xs : Array α}
(h : Array.find? p xs = some a)
:
theorem
Array.mem_of_find?_eq_some
{α : Type u_1}
{p : α → Bool}
{a : α}
{xs : Array α}
(h : Array.find? p xs = some a)
:
a ∈ xs
theorem
Array.get_find?_mem
{α : Type u_1}
{p : α → Bool}
{xs : Array α}
(h : (Array.find? p xs).isSome = true)
:
(Array.find? p xs).get h ∈ xs
@[simp]
theorem
Array.find?_filter
{α : Type u_1}
{xs : Array α}
(p q : α → Bool)
:
Array.find? q (Array.filter p xs) = Array.find? (fun (a : α) => decide (p a = true ∧ q a = true)) xs
@[simp]
theorem
Array.getElem?_zero_filter
{α : Type u_1}
(p : α → Bool)
(l : Array α)
:
(Array.filter p l)[0]? = Array.find? p l
@[simp]
theorem
Array.getElem_zero_filter
{α : Type u_1}
(p : α → Bool)
(l : Array α)
(h : 0 < (Array.filter p l).size)
:
(Array.filter p l)[0] = (Array.find? p l).get ⋯
@[simp]
theorem
Array.back?_filter
{α : Type}
(p : α → Bool)
(l : Array α)
:
(Array.filter p l).back? = Array.findRev? p l
@[simp]
theorem
Array.back!_filter
{α : Type}
[Inhabited α]
(p : α → Bool)
(l : Array α)
:
(Array.filter p l).back! = (Array.findRev? p l).get!
@[simp]
theorem
Array.find?_filterMap
{α : Type u_1}
{β : Type u_2}
(xs : Array α)
(f : α → Option β)
(p : β → Bool)
:
Array.find? p (Array.filterMap f xs) = (Array.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 β)
:
Array.find? p (Array.map f xs) = Option.map f (Array.find? (p ∘ f) xs)
@[simp]
theorem
Array.find?_append
{α : Type u_1}
{p : α → Bool}
{l₁ l₂ : Array α}
:
Array.find? p (l₁ ++ l₂) = (Array.find? p l₁).or (Array.find? p l₂)
@[simp]
theorem
Array.find?_flatten
{α : Type u_1}
(xs : Array (Array α))
(p : α → Bool)
:
Array.find? p xs.flatten = Array.findSome? (fun (x : Array α) => Array.find? p x) xs
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)
:
Array.find? p (Array.flatMap f xs) = Array.findSome? (fun (x : α) => Array.find? p (f x)) xs
@[simp]
theorem
Array.get_find?_mkArray
{α : Type u_1}
(n : Nat)
(a : α)
(p : α → Bool)
(h : (Array.find? p (mkArray n a)).isSome = true)
:
(Array.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)
:
Array.find? p (Array.pmap f xs H) = Option.map
(fun (x : { x : α // x ∈ xs }) =>
match x with
| ⟨a, m⟩ => f a ⋯)
(Array.find?
(fun (x : { x : α // x ∈ xs }) =>
match x with
| ⟨a, m⟩ => p (f a ⋯))
xs.attach)