Lemmas about `Vector.findSome?`, `Vector.find?`, `Vector.findFinIdx?`. #

We are still missing results about idxOf?, findIdx, and findIdx?.

findSome? #

source

@[simp]

theorem Vector.findSome?_empty {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} :

findSome? f #v[] = none

source

@[simp]

theorem Vector.findSome?_push {α : Type u_1} {n : Nat} {a : α} {α✝ : Type u_2} {f : α → Option α✝} {xs : Vector α n} :

findSome? f (xs.push a) = (findSome? f xs).or (f a)

source

theorem Vector.findSome?_singleton {α : Type u_1} {β : Type u_2} {a : α} {f : α → Option β} :

findSome? f #v[a] = f a

source

@[simp]

theorem Vector.findSomeRev?_push_of_isSome {α : Type u_1} {n : Nat} {α✝ : Type u_2} {f : α → Option α✝} {a : α} {xs : Vector α n} {h : (f a).isSome = true} :

findSomeRev? f (xs.push a) = f a

source

@[simp]

theorem Vector.findSomeRev?_push_of_isNone {α : Type u_1} {n : Nat} {α✝ : Type u_2} {f : α → Option α✝} {a : α} {xs : Vector α n} {h : (f a).isNone = true} :

findSomeRev? f (xs.push a) = findSomeRev? f xs

source

theorem Vector.findSomeRev?_push {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {a : α} {f : α → Option β} :

findSomeRev? f (xs.push a) = (f a).or (findSomeRev? f xs)

source

theorem Vector.exists_of_findSome?_eq_some {α : Type u_1} {β : Type u_2} {n : Nat} {b : β} {f : α → Option β} {xs : Vector α n} (w : findSome? f xs = some b) :

∃ (a : α), a ∈ xs ∧ f a = some b

source

@[simp]

theorem Vector.findSome?_eq_none_iff {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → Option β} {xs : Vector α n} :

findSome? f xs = none ↔ ∀ (x : α), x ∈ xs → f x = none

source

@[simp]

theorem Vector.findSome?_isSome_iff {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → Option β} {xs : Vector α n} :

(findSome? f xs).isSome = true ↔ ∃ (x : α), x ∈ xs ∧ (f x).isSome = true

source

theorem Vector.findSome?_eq_some_iff {α : Type u_1} {β : Type u_2} {n : Nat} {f : α → Option β} {xs : Vector α n} {b : β} :

findSome? f xs = some b ↔ ∃ (k₁ : Nat ), ∃ (k₂ : Nat ), ∃ (w : n = k₁ + 1 + k₂), ∃ (ys : Vector α k₁), ∃ (a : α), ∃ (zs : Vector α k₂), xs = Vector.cast ⋯ (ys.push a ++ zs) ∧ f a = some b ∧ ∀ (x : α), x ∈ ys → f x = none

source

theorem Vector.isSome_findSome? {α : Type u_1} {n : Nat} {β : Type u_2} {xs : Vector α n} {f : α → Option β} :

(findSome? f xs).isSome = xs.any fun (x : α) => (f x).isSome

source

@[simp]

theorem Vector.findSome?_guard {α : Type} {n : Nat} {p : α → Bool} {xs : Vector α n} :

findSome? (Option.guard p) xs = find? p xs

source

theorem Vector.find?_eq_findSome?_guard {α : Type} {n : Nat} {p : α → Bool} {xs : Vector α n} :

find? p xs = findSome? (Option.guard p) xs

source

@[simp]

theorem Vector.map_findSome? {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} {f : α → Option β} {g : β → γ} {xs : Vector α n} :

Option.map g (findSome? f xs) = findSome? (Option.map g ∘ f) xs

source

theorem Vector.findSome?_map {β : Type u_1} {γ : Type u_2} {n : Nat} {α✝ : Type u_3} {p : γ → Option α✝} {f : β → γ} {xs : Vector β n} :

findSome? p (map f xs) = findSome? (p ∘ f) xs

source

theorem Vector.findSome?_append {α : Type u_1} {n₁ n₂ : Nat} {α✝ : Type u_2} {f : α → Option α✝} {xs : Vector α n₁} {ys : Vector α n₂} :

findSome? f (xs ++ ys) = (findSome? f xs).or (findSome? f ys)

source

theorem Vector.getElem?_zero_flatten {α : Type u_1} {m n : Nat} {xss : Vector (Vector α m) n} :

xss.flatten[0]? = findSome? (fun (xs : Vector α m) => xs[0]?) xss

source

theorem Vector.getElem_zero_flatten.proof {α : Type u_1} {m n : Nat} {xss : Vector (Vector α m) n} (h : 0 < n * m) :

(findSome? (fun (xs : Vector α m) => xs[0]?) xss).isSome = true

source

theorem Vector.getElem_zero_flatten {α : Type u_1} {m n : Nat} {xss : Vector (Vector α m) n} (h : 0 < n * m) :

xss.flatten[0] = (findSome? (fun (xs : Vector α m) => xs[0]?) xss).get ⋯

source

theorem Vector.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

@[simp]

theorem Vector.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

@[simp]

theorem Vector.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

@[simp]

theorem Vector.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? #

source

@[simp]

theorem Vector.find?_empty {α✝ : Type} {p : α✝ → Bool} :

find? p #v[] = none

source

theorem Vector.find?_singleton {α : Type} {a : α} {p : α → Bool} :

find? p #v[a] = if p a = true then some a else none

source

@[simp]

theorem Vector.findRev?_push_of_pos {α : Type} {n : Nat} {p : α → Bool} {a : α} {xs : Vector α n} (h : p a = true) :

findRev? p (xs.push a) = some a

source

@[simp]

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

findRev? p (xs.push a) = findRev? p xs

source

theorem Vector.finRev?_push {α : Type} {n : Nat} {p : α → Bool} {a : α} {xs : Vector α n} :

findRev? p (xs.push a) = (Option.guard p a).or (findRev? p xs)

source

@[simp]

theorem Vector.find?_eq_none {α✝ : Type} {p : α✝ → Bool} {n✝ : Nat} {l : Vector α✝ n✝} :

find? p l = none ↔ ∀ (x : α✝), x ∈ l → ¬p x = true

source

theorem Vector.find?_eq_some_iff_append {α : Type} {n : Nat} {p : α → Bool} {b : α} {xs : Vector α n} :

find? p xs = some b ↔ p b = true ∧ ∃ (k₁ : Nat ), ∃ (k₂ : Nat ), ∃ (w : n = k₁ + 1 + k₂), ∃ (as : Vector α k₁), ∃ (bs : Vector α k₂), xs = Vector.cast ⋯ (as.push b ++ bs) ∧ ∀ (a : α), a ∈ as → (!p a) = true

source

theorem Vector.isSome_find? {α : Type} {n : Nat} {xs : Vector α n} {f : α → Bool} :

(find? f xs).isSome = xs.any fun (x : α) => f x

source

theorem Vector.find?_push {α : Type} {n : Nat} {a : α} {p : α → Bool} {xs : Vector α n} :

find? p (xs.push a) = (find? p xs).or (if p a = true then some a else none)

source

@[simp]

theorem Vector.find?_push_eq_some {α : Type} {n : Nat} {a : α} {p : α → Bool} {b : α} {xs : Vector α n} :

find? p (xs.push a) = some b ↔ find? p xs = some b ∨ find? p xs = none ∧ p a = true ∧ a = b

source

@[simp]

theorem Vector.find?_isSome {α : Type} {n : Nat} {xs : Vector α n} {p : α → Bool} :

(find? p xs).isSome = true ↔ ∃ (x : α), x ∈ xs ∧ p x = true

source

theorem Vector.find?_some {α : Type} {n : Nat} {p : α → Bool} {a : α} {xs : Vector α n} (h : find? p xs = some a) :

p a = true

source

theorem Vector.mem_of_find?_eq_some {α : Type} {n : Nat} {p : α → Bool} {a : α} {xs : Vector α n} (h : find? p xs = some a) :

a ∈ xs

source

theorem Vector.get_find?_mem {α : Type} {n : Nat} {p : α → Bool} {xs : Vector α n} (h : (find? p xs).isSome = true) :

(find? p xs).get h ∈ xs

source

@[simp]

theorem Vector.find?_map {β α : Type} {n : Nat} {p : α → Bool} {f : β → α} {xs : Vector β n} :

find? p (map f xs) = Option.map f (find? (p ∘ f) xs)

source

@[simp]

theorem Vector.find?_append {α : Type} {n₁ n₂ : Nat} {p : α → Bool} {xs : Vector α n₁} {ys : Vector α n₂} :

find? p (xs ++ ys) = (find? p xs).or (find? p ys)

source

@[simp]

theorem Vector.find?_flatten {α : Type} {m n : Nat} {xs : Vector (Vector α m) n} {p : α → Bool} :

find? p xs.flatten = findSome? (find? p) xs

source

theorem Vector.find?_flatten_eq_none_iff {α : Type} {m n : Nat} {xs : Vector (Vector α m) n} {p : α → Bool} :

find? p xs.flatten = none ↔ ∀ (ys : Vector α m), ys ∈ xs → ∀ (x : α), x ∈ ys → (!p x) = true

source

@[simp]

theorem Vector.find?_flatMap {α : Type u_1} {n : Nat} {β : Type} {m : Nat} {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :

find? p (xs.flatMap f) = findSome? (fun (x : α) => find? p (f x)) xs

source

theorem Vector.find?_flatMap_eq_none_iff {α : Type u_1} {n : Nat} {β : Type} {m : Nat} {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :

find? p (xs.flatMap f) = none ↔ ∀ (x : α), x ∈ xs → ∀ (y : β), y ∈ f x → (!p y) = true

source

theorem Vector.find?_replicate {α✝ : Type} {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

@[simp]

theorem Vector.find?_replicate_of_size_pos {n : Nat} {α✝ : Type} {p : α✝ → Bool} {a : α✝} (h : 0 < n) :

find? p (replicate n a) = if p a = true then some a else none

source

@[simp]

theorem Vector.find?_replicate_of_pos {α✝ : Type} {p : α✝ → Bool} {n : Nat} {a : α✝} (h : p a = true) :

find? p (replicate n a) = if n = 0 then none else some a

source

@[simp]

theorem Vector.find?_replicate_of_neg {α✝ : Type} {p : α✝ → Bool} {n : Nat} {a : α✝} (h : ¬p a = true) :

find? p (replicate n a) = none

source

theorem Vector.find?_replicate_eq_none_iff {α : Type} {n : Nat} {a : α} {p : α → Bool} :

find? p (replicate n a) = none ↔ n = 0 ∨ (!p a) = true

source

@[simp]

theorem Vector.find?_replicate_eq_some_iff {α : Type} {n : Nat} {a b : α} {p : α → Bool} :

find? p (replicate n a) = some b ↔ n ≠ 0 ∧ p a = true ∧ a = b

source

@[simp]

theorem Vector.get_find?_replicate {α : Type} {n : Nat} {a : α} {p : α → Bool} (h : (find? p (replicate n a)).isSome = true) :

(find? p (replicate n a)).get h = a

source

theorem Vector.find?_pmap {α β : Type} {n : Nat} {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n} (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 Vector.find?_eq_some_iff_getElem {α : Type} {n : Nat} {xs : Vector α n} {p : α → Bool} {b : α} :

find? p xs = some b ↔ p b = true ∧ ∃ (i : Nat ), ∃ (h : i < n), xs[i] = b ∧ ∀ (j : Nat) (hj : j < i), (!p xs[j]) = true

findFinIdx? #

source

theorem Vector.findFinIdx?_empty {α : Type u_1} {p : α → Bool} :

findFinIdx? p #v[] = none

source

theorem Vector.findFinIdx?_singleton {α : Type u_1} {a : α} {p : α → Bool} :

Array.findFinIdx? p #[a] = if p a = true then some ⟨0, ⋯⟩ else none

source

theorem Vector.findFinIdx?_congr {α : Type u_1} {n : Nat} {p : α → Bool} {xs ys : Vector α n} (w : xs = ys) :

findFinIdx? p xs = findFinIdx? p ys

source

@[simp]

theorem Vector.findFinIdx?_eq_none_iff {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Bool} :

findFinIdx? p xs = none ↔ ∀ (x : α), x ∈ xs → ¬p x = true

source

theorem Vector.findFinIdx?_push {α : Type u_1} {n : Nat} {xs : Vector α n} {a : α} {p : α → Bool} :

findFinIdx? p (xs.push a) = (Option.map Fin.castSucc (findFinIdx? p xs)).or (if p a = true then some ⟨n, ⋯⟩ else none)

source

theorem Vector.findFinIdx?_append {α : Type u_1} {n₁ n₂ : Nat} {xs : Vector α n₁} {ys : Vector α n₂} {p : α → Bool} :

findFinIdx? p (xs ++ ys) = (Option.map (Fin.castLE ⋯) (findFinIdx? p xs)).or (Option.map (Fin.natAdd n₁) (findFinIdx? p ys))

source

@[simp]

theorem Vector.isSome_findFinIdx? {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Bool} :

(findFinIdx? p xs).isSome = xs.any p

source

@[simp]

theorem Vector.isNone_findFinIdx? {α : Type u_1} {n : Nat} {xs : Vector α n} {p : α → Bool} :

(findFinIdx? p xs).isNone = xs.all fun (x : α) => decide ¬p x = true

source

@[simp]

theorem Vector.findFinIdx?_subtype {α : Type u_1} {n : Nat} {p : α → Prop} {xs : Vector { x : α // p x } n} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) :

findFinIdx? f xs = findFinIdx? g xs.unattach