Lemmas about List.findSome?, List.find?, List.findIdx, List.findIdx?, and List.indexOf. #
findSome? #
@[simp]
theorem
List.findSome?_cons_of_isNone :
∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {a : α} (l : List α),
(f a).isNone = true → List.findSome? f (a :: l) = List.findSome? f l
@[reducible, inline, deprecated List.findSome?_eq_none_iff]
Instances For
@[simp]
theorem
List.findSome?_guard
{α : Type u_1}
{p : α → Bool}
(l : List α)
:
List.findSome? (Option.guard fun (x : α) => p x = true) l = List.find? p l
@[simp]
theorem
List.filterMap_head?
{α : Type u_1}
{β : Type u_2}
(f : α → Option β)
(l : List α)
:
(List.filterMap f l).head? = List.findSome? f l
@[simp]
theorem
List.filterMap_head
{α : Type u_1}
{β : Type u_2}
(f : α → Option β)
(l : List α)
(h : List.filterMap f l ≠ [])
:
(List.filterMap f l).head h = (List.findSome? f l).get ⋯
@[simp]
theorem
List.filterMap_getLast?
{α : Type u_1}
{β : Type u_2}
(f : α → Option β)
(l : List α)
:
(List.filterMap f l).getLast? = List.findSome? f l.reverse
@[simp]
theorem
List.filterMap_getLast
{α : Type u_1}
{β : Type u_2}
(f : α → Option β)
(l : List α)
(h : List.filterMap f l ≠ [])
:
(List.filterMap f l).getLast h = (List.findSome? f l.reverse).get ⋯
@[simp]
theorem
List.map_findSome?
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → Option β)
(g : β → γ)
(l : List α)
:
Option.map g (List.findSome? f l) = List.findSome? (Option.map g ∘ f) l
theorem
List.findSome?_map
{β : Type u_1}
{γ : Type u_2}
:
∀ {α : Type u_3} {p : γ → Option α} (f : β → γ) (l : List β), List.findSome? p (List.map f l) = List.findSome? (p ∘ f) l
theorem
List.findSome?_append
{α : Type u_1}
:
∀ {α_1 : Type u_2} {f : α → Option α_1} {l₁ l₂ : List α},
List.findSome? f (l₁ ++ l₂) = (List.findSome? f l₁).or (List.findSome? f l₂)
theorem
List.findSome?_replicate :
∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : Nat} {a : α},
List.findSome? f (List.replicate n a) = if n = 0 then none else f a
@[simp]
theorem
List.findSome?_replicate_of_pos
{n : Nat}
:
∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {a : α}, 0 < n → List.findSome? f (List.replicate n a) = f a
@[simp]
theorem
List.findSome?_replicate_of_isSome :
∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : Nat} {a : α},
(f a).isSome = true → List.findSome? f (List.replicate n a) = if n = 0 then none else f a
@[simp]
theorem
List.findSome?_replicate_of_isNone :
∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : Nat} {a : α},
(f a).isNone = true → List.findSome? f (List.replicate n a) = none
theorem
List.Sublist.findSome?_isSome
{α : Type u_1}
:
∀ {α_1 : Type u_2} {f : α → Option α_1} {l₁ l₂ : List α},
l₁.Sublist l₂ → (List.findSome? f l₁).isSome = true → (List.findSome? f l₂).isSome = true
theorem
List.Sublist.findSome?_eq_none
{α : Type u_1}
:
∀ {α_1 : Type u_2} {f : α → Option α_1} {l₁ l₂ : List α},
l₁.Sublist l₂ → List.findSome? f l₂ = none → List.findSome? f l₁ = none
theorem
List.IsPrefix.findSome?_eq_some
{α : Type u_1}
{β : Type u_2}
{b : β}
{l₁ : List α}
{l₂ : List α}
{f : α → Option β}
(h : l₁ <+: l₂)
:
List.findSome? f l₁ = some b → List.findSome? f l₂ = some b
theorem
List.IsPrefix.findSome?_eq_none
{α : Type u_1}
{β : Type u_2}
{l₁ : List α}
{l₂ : List α}
{f : α → Option β}
(h : l₁ <+: l₂)
:
List.findSome? f l₂ = none → List.findSome? f l₁ = none
theorem
List.IsSuffix.findSome?_eq_none
{α : Type u_1}
{β : Type u_2}
{l₁ : List α}
{l₂ : List α}
{f : α → Option β}
(h : l₁ <:+ l₂)
:
List.findSome? f l₂ = none → List.findSome? f l₁ = none
theorem
List.IsInfix.findSome?_eq_none
{α : Type u_1}
{β : Type u_2}
{l₁ : List α}
{l₂ : List α}
{f : α → Option β}
(h : l₁ <:+: l₂)
:
List.findSome? f l₂ = none → List.findSome? f l₁ = none
find? #
@[simp]
theorem
List.find?_singleton
{α : Type u_1}
(a : α)
(p : α → Bool)
:
List.find? p [a] = if p a = true then some a else none
@[simp]
theorem
List.find?_cons_of_neg :
∀ {α : Type u_1} {p : α → Bool} {a : α} (l : List α), ¬p a = true → List.find? p (a :: l) = List.find? p l
theorem
List.get_find?_mem
{α : Type u_1}
(xs : List α)
(p : α → Bool)
(h : (List.find? p xs).isSome = true)
:
(List.find? p xs).get h ∈ xs
@[simp]
theorem
List.find?_filter
{α : Type u_1}
(xs : List α)
(p : α → Bool)
(q : α → Bool)
:
List.find? q (List.filter p xs) = List.find? (fun (a : α) => decide (p a = true ∧ q a = true)) xs
@[simp]
theorem
List.filter_head?
{α : Type u_1}
(p : α → Bool)
(l : List α)
:
(List.filter p l).head? = List.find? p l
@[simp]
theorem
List.filter_head
{α : Type u_1}
(p : α → Bool)
(l : List α)
(h : List.filter p l ≠ [])
:
(List.filter p l).head h = (List.find? p l).get ⋯
@[simp]
theorem
List.filter_getLast?
{α : Type u_1}
(p : α → Bool)
(l : List α)
:
(List.filter p l).getLast? = List.find? p l.reverse
@[simp]
theorem
List.filter_getLast
{α : Type u_1}
(p : α → Bool)
(l : List α)
(h : List.filter p l ≠ [])
:
(List.filter p l).getLast h = (List.find? p l.reverse).get ⋯
@[simp]
theorem
List.find?_filterMap
{α : Type u_1}
{β : Type u_2}
(xs : List α)
(f : α → Option β)
(p : β → Bool)
:
List.find? p (List.filterMap f xs) = (List.find? (fun (a : α) => Option.any p (f a)) xs).bind f
@[simp]
theorem
List.find?_map
{β : Type u_1}
{α : Type u_2}
{p : α → Bool}
(f : β → α)
(l : List β)
:
List.find? p (List.map f l) = Option.map f (List.find? (p ∘ f) l)
@[simp]
theorem
List.find?_append
{α : Type u_1}
{p : α → Bool}
{l₁ : List α}
{l₂ : List α}
:
List.find? p (l₁ ++ l₂) = (List.find? p l₁).or (List.find? p l₂)
@[simp]
theorem
List.find?_join
{α : Type u_1}
(xs : List (List α))
(p : α → Bool)
:
List.find? p xs.join = List.findSome? (fun (x : List α) => List.find? p x) xs
If find? p returns some a from xs.join, then p a holds, and
some list in xs contains a, and no earlier element of that list satisfies p.
Moreover, no earlier list in xs has an element satisfying p.
@[simp]
theorem
List.find?_bind
{α : Type u_1}
{β : Type u_2}
(xs : List α)
(f : α → List β)
(p : β → Bool)
:
List.find? p (xs.bind f) = List.findSome? (fun (x : α) => List.find? p (f x)) xs
theorem
List.find?_replicate :
∀ {α : Type u_1} {p : α → Bool} {n : Nat} {a : α},
List.find? p (List.replicate n a) = if n = 0 then none else if p a = true then some a else none
@[simp]
theorem
List.find?_replicate_of_length_pos
{n : Nat}
:
∀ {α : Type u_1} {p : α → Bool} {a : α}, 0 < n → List.find? p (List.replicate n a) = if p a = true then some a else none
@[simp]
theorem
List.find?_replicate_of_pos :
∀ {α : Type u_1} {p : α → Bool} {n : Nat} {a : α},
p a = true → List.find? p (List.replicate n a) = if n = 0 then none else some a
@[simp]
theorem
List.find?_replicate_of_neg :
∀ {α : Type u_1} {p : α → Bool} {n : Nat} {a : α}, ¬p a = true → List.find? p (List.replicate n a) = none
theorem
List.find?_replicate_eq_none
{α : Type u_1}
{n : Nat}
{a : α}
{p : α → Bool}
:
List.find? p (List.replicate n a) = none ↔ n = 0 ∨ (!p a) = true
@[simp]
theorem
List.get_find?_replicate
{α : Type u_1}
(n : Nat)
(a : α)
(p : α → Bool)
(h : (List.find? p (List.replicate n a)).isSome = true)
:
(List.find? p (List.replicate n a)).get h = a
theorem
List.Sublist.find?_isSome
{α : Type u_1}
{p : α → Bool}
{l₁ : List α}
{l₂ : List α}
(h : l₁.Sublist l₂)
:
(List.find? p l₁).isSome = true → (List.find? p l₂).isSome = true
theorem
List.Sublist.find?_eq_none
{α : Type u_1}
{p : α → Bool}
{l₁ : List α}
{l₂ : List α}
(h : l₁.Sublist l₂)
:
List.find? p l₂ = none → List.find? p l₁ = none
theorem
List.IsPrefix.find?_eq_some
{α : Type u_1}
{b : α}
{l₁ : List α}
{l₂ : List α}
{p : α → Bool}
(h : l₁ <+: l₂)
:
List.find? p l₁ = some b → List.find? p l₂ = some b
theorem
List.IsPrefix.find?_eq_none
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
{p : α → Bool}
(h : l₁ <+: l₂)
:
List.find? p l₂ = none → List.find? p l₁ = none
theorem
List.IsSuffix.find?_eq_none
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
{p : α → Bool}
(h : l₁ <:+ l₂)
:
List.find? p l₂ = none → List.find? p l₁ = none
theorem
List.IsInfix.find?_eq_none
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
{p : α → Bool}
(h : l₁ <:+: l₂)
:
List.find? p l₂ = none → List.find? p l₁ = none
theorem
List.find?_pmap
{α : Type u_1}
{β : Type u_2}
{P : α → Prop}
(f : (a : α) → P a → β)
(xs : List α)
(H : ∀ (a : α), a ∈ xs → P a)
(p : β → Bool)
:
List.find? p (List.pmap f xs H) = Option.map
(fun (x : { x : α // x ∈ xs }) =>
match x with
| ⟨a, m⟩ => f a ⋯)
(List.find?
(fun (x : { x : α // x ∈ xs }) =>
match x with
| ⟨a, m⟩ => p (f a ⋯))
xs.attach)
findIdx #
theorem
List.findIdx_cons
{α : Type u_1}
(p : α → Bool)
(b : α)
(l : List α)
:
List.findIdx p (b :: l) = bif p b then 0 else List.findIdx p l + 1
theorem
List.findIdx_cons.findIdx_go_succ
{α : Type u_1}
(p : α → Bool)
(l : List α)
(n : Nat)
:
List.findIdx.go p l (n + 1) = List.findIdx.go p l n + 1
theorem
List.findIdx_of_getElem?_eq_some
{α : Type u_1}
{p : α → Bool}
{y : α}
{xs : List α}
(w : xs[List.findIdx p xs]? = some y)
:
theorem
List.findIdx_getElem
{α : Type u_1}
{p : α → Bool}
{xs : List α}
{w : List.findIdx p xs < xs.length}
:
p xs[List.findIdx p xs] = true
@[deprecated List.findIdx_of_getElem?_eq_some]
theorem
List.findIdx_of_get?_eq_some
{α : Type u_1}
{p : α → Bool}
{y : α}
{xs : List α}
(w : xs.get? (List.findIdx p xs) = some y)
:
@[deprecated List.findIdx_getElem]
theorem
List.findIdx_get
{α : Type u_1}
{p : α → Bool}
{xs : List α}
{w : List.findIdx p xs < xs.length}
:
p (xs.get ⟨List.findIdx p xs, w⟩) = true
theorem
List.findIdx_getElem?_eq_getElem_of_exists
{α : Type u_1}
{p : α → Bool}
{xs : List α}
(h : ∃ (x : α), x ∈ xs ∧ p x = true)
:
xs[List.findIdx p xs]? = some xs[List.findIdx p xs]
@[deprecated List.findIdx_getElem?_eq_getElem_of_exists]
theorem
List.findIdx_get?_eq_get_of_exists
{α : Type u_1}
{p : α → Bool}
{xs : List α}
(h : ∃ (x : α), x ∈ xs ∧ p x = true)
:
xs.get? (List.findIdx p xs) = some (xs.get ⟨List.findIdx p xs, ⋯⟩)
theorem
List.findIdx_eq_length_of_false
{α : Type u_1}
{p : α → Bool}
{xs : List α}
(h : ∀ (x : α), x ∈ xs → p x = false)
:
List.findIdx p xs = xs.length
theorem
List.findIdx_le_length
{α : Type u_1}
(p : α → Bool)
{xs : List α}
:
List.findIdx p xs ≤ xs.length
theorem
List.not_of_lt_findIdx
{α : Type u_1}
{p : α → Bool}
{xs : List α}
{i : Nat}
(h : i < List.findIdx p xs)
:
p does not hold for elements with indices less than xs.findIdx p.
theorem
List.findIdx_append
{α : Type u_1}
(p : α → Bool)
(l₁ : List α)
(l₂ : List α)
:
List.findIdx p (l₁ ++ l₂) = if ∃ (x : α), x ∈ l₁ ∧ p x = true then List.findIdx p l₁ else List.findIdx p l₂ + l₁.length
theorem
List.IsPrefix.findIdx_le
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
{p : α → Bool}
(h : l₁ <+: l₂)
:
List.findIdx p l₁ ≤ List.findIdx p l₂
theorem
List.IsPrefix.findIdx_eq_of_findIdx_lt_length
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
{p : α → Bool}
(h : l₁ <+: l₂)
(lt : List.findIdx p l₁ < l₁.length)
:
List.findIdx p l₂ = List.findIdx p l₁
theorem
List.findIdx_le_findIdx
{α : Type u_1}
{l : List α}
{p : α → Bool}
{q : α → Bool}
(h : ∀ (x : α), x ∈ l → p x = true → q x = true)
:
List.findIdx q l ≤ List.findIdx p l
findIdx? #
@[simp]
@[simp]
theorem
List.findIdx?_succ
{α : Type u_1}
{xs : List α}
{p : α → Bool}
{i : Nat}
:
List.findIdx? p xs (i + 1) = Option.map (fun (i : Nat) => i + 1) (List.findIdx? p xs i)
@[simp]
theorem
List.findIdx?_start_succ
{α : Type u_1}
{xs : List α}
{p : α → Bool}
{i : Nat}
:
List.findIdx? p xs (i + 1) = Option.map (fun (k : Nat) => k + (i + 1)) (List.findIdx? p xs)
theorem
List.findIdx?_isSome
{α : Type u_1}
{xs : List α}
{p : α → Bool}
:
(List.findIdx? p xs).isSome = xs.any p
theorem
List.findIdx?_eq_some_iff_findIdx_eq
{α : Type u_1}
{xs : List α}
{p : α → Bool}
{i : Nat}
:
List.findIdx? p xs = some i ↔ i < xs.length ∧ List.findIdx p xs = i
theorem
List.findIdx?_eq_some_of_exists
{α : Type u_1}
{xs : List α}
{p : α → Bool}
(h : ∃ (x : α), x ∈ xs ∧ p x = true)
:
List.findIdx? p xs = some (List.findIdx p xs)
theorem
List.findIdx?_eq_none_iff_findIdx_eq
{α : Type u_1}
{xs : List α}
{p : α → Bool}
:
List.findIdx? p xs = none ↔ List.findIdx p xs = xs.length
theorem
List.findIdx?_eq_guard_findIdx_lt
{α : Type u_1}
{xs : List α}
{p : α → Bool}
:
List.findIdx? p xs = Option.guard (fun (i : Nat) => i < xs.length) (List.findIdx p xs)
@[simp]
theorem
List.findIdx?_map
{β : Type u_1}
{α : Type u_2}
{p : α → Bool}
(f : β → α)
(l : List β)
:
List.findIdx? p (List.map f l) = List.findIdx? (p ∘ f) l
@[simp]
theorem
List.findIdx?_append
{α : Type u_1}
{xs : List α}
{ys : List α}
{p : α → Bool}
:
List.findIdx? p (xs ++ ys) = (List.findIdx? p xs).or (Option.map (fun (i : Nat) => i + xs.length) (List.findIdx? p ys))
theorem
List.findIdx?_join
{α : Type u_1}
{l : List (List α)}
{p : α → Bool}
:
List.findIdx? p l.join = Option.map
(fun (i : Nat) =>
Nat.sum (List.map List.length (List.take i l)) + (Option.map (fun (xs : List α) => List.findIdx p xs) l[i]?).getD 0)
(List.findIdx? (fun (x : List α) => x.any p) l)
@[simp]
theorem
List.findIdx?_replicate
{n : Nat}
:
∀ {α : Type u_1} {a : α} {p : α → Bool},
List.findIdx? p (List.replicate n a) = if 0 < n ∧ p a = true then some 0 else none
theorem
List.findIdx?_eq_findSome?_enum
{α : Type u_1}
{xs : List α}
{p : α → Bool}
:
List.findIdx? p xs = List.findSome?
(fun (x : Nat × α) =>
match x with
| (i, a) => if p a = true then some i else none)
xs.enum
theorem
List.findIdx?_eq_fst_find?_enum
{α : Type u_1}
{xs : List α}
{p : α → Bool}
:
List.findIdx? p xs = Option.map (fun (x : Nat × α) => x.fst)
(List.find?
(fun (x : Nat × α) =>
match x with
| (fst, x) => p x)
xs.enum)
theorem
List.findIdx?_eq_none_of_findIdx?_eq_none
{α : Type u_1}
{xs : List α}
{p : α → Bool}
{q : α → Bool}
(w : ∀ (x : α), x ∈ xs → p x = true → q x = true)
:
List.findIdx? q xs = none → List.findIdx? p xs = none
theorem
List.Sublist.findIdx?_isSome
{α : Type u_1}
{p : α → Bool}
{l₁ : List α}
{l₂ : List α}
(h : l₁.Sublist l₂)
:
(List.findIdx? p l₁).isSome = true → (List.findIdx? p l₂).isSome = true
theorem
List.Sublist.findIdx?_eq_none
{α : Type u_1}
{p : α → Bool}
{l₁ : List α}
{l₂ : List α}
(h : l₁.Sublist l₂)
:
List.findIdx? p l₂ = none → List.findIdx? p l₁ = none
theorem
List.IsPrefix.findIdx?_eq_some
{α : Type u_1}
{i : Nat}
{l₁ : List α}
{l₂ : List α}
{p : α → Bool}
(h : l₁ <+: l₂)
:
List.findIdx? p l₁ = some i → List.findIdx? p l₂ = some i
theorem
List.IsPrefix.findIdx?_eq_none
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
{p : α → Bool}
(h : l₁ <+: l₂)
:
List.findIdx? p l₂ = none → List.findIdx? p l₁ = none
theorem
List.IsSuffix.findIdx?_eq_none
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
{p : α → Bool}
(h : l₁ <:+ l₂)
:
List.findIdx? p l₂ = none → List.findIdx? p l₁ = none
theorem
List.IsInfix.findIdx?_eq_none
{α : Type u_1}
{l₁ : List α}
{l₂ : List α}
{p : α → Bool}
(h : l₁ <:+: l₂)
:
List.findIdx? p l₂ = none → List.findIdx? p l₁ = none
indexOf #
theorem
List.indexOf_cons
{α : Type u_1}
{x : α}
{xs : List α}
{y : α}
[BEq α]
:
List.indexOf y (x :: xs) = bif x == y then 0 else List.indexOf y xs + 1
lookup #
theorem
List.lookup_append
{α : Type u_2}
[BEq α]
[LawfulBEq α]
{β : Type u_1}
{l₁ : List (α × β)}
{l₂ : List (α × β)}
{k : α}
:
List.lookup k (l₁ ++ l₂) = (List.lookup k l₁).or (List.lookup k l₂)
theorem
List.lookup_replicate
{α : Type u_2}
[BEq α]
[LawfulBEq α]
{n : Nat}
{a : α}
:
∀ {α_1 : Type u_1} {b : α_1} {k : α},
List.lookup k (List.replicate n (a, b)) = if n = 0 then none else if (k == a) = true then some b else none
theorem
List.lookup_replicate_of_pos
{α : Type u_2}
[BEq α]
[LawfulBEq α]
{n : Nat}
{a : α}
:
∀ {α_1 : Type u_1} {b : α_1} {k : α},
0 < n → List.lookup k (List.replicate n (a, b)) = if (k == a) = true then some b else none
theorem
List.lookup_replicate_self
{α : Type u_2}
[BEq α]
[LawfulBEq α]
{n : Nat}
:
∀ {α_1 : Type u_1} {b : α_1} {a : α}, List.lookup a (List.replicate n (a, b)) = if n = 0 then none else some b
@[simp]
theorem
List.lookup_replicate_self_of_pos
{α : Type u_2}
[BEq α]
[LawfulBEq α]
{n : Nat}
:
∀ {α_1 : Type u_1} {b : α_1} {a : α}, 0 < n → List.lookup a (List.replicate n (a, b)) = some b
@[simp]
theorem
List.lookup_replicate_ne
{α : Type u_2}
[BEq α]
[LawfulBEq α]
{a : α}
{n : Nat}
:
∀ {α_1 : Type u_1} {b : α_1} {k : α}, (!k == a) = true → List.lookup k (List.replicate n (a, b)) = none
theorem
List.Sublist.lookup_eq_none
{α : Type u_2}
[BEq α]
[LawfulBEq α]
{β : Type u_1}
{k : α}
{l₁ : List (α × β)}
{l₂ : List (α × β)}
(h : l₁.Sublist l₂)
:
List.lookup k l₂ = none → List.lookup k l₁ = none
theorem
List.IsPrefix.lookup_eq_none
{α : Type u_2}
[BEq α]
[LawfulBEq α]
{β : Type u_1}
{k : α}
{l₁ : List (α × β)}
{l₂ : List (α × β)}
(h : l₁ <+: l₂)
:
List.lookup k l₂ = none → List.lookup k l₁ = none
theorem
List.IsSuffix.lookup_eq_none
{α : Type u_2}
[BEq α]
[LawfulBEq α]
{β : Type u_1}
{k : α}
{l₁ : List (α × β)}
{l₂ : List (α × β)}
(h : l₁ <:+ l₂)
:
List.lookup k l₂ = none → List.lookup k l₁ = none
theorem
List.IsInfix.lookup_eq_none
{α : Type u_2}
[BEq α]
[LawfulBEq α]
{β : Type u_1}
{k : α}
{l₁ : List (α × β)}
{l₂ : List (α × β)}
(h : l₁ <:+: l₂)
:
List.lookup k l₂ = none → List.lookup k l₁ = none