Lemmas about List.findSome?, List.find?, List.findIdx, List.findIdx?, List.idxOf, and List.lookup.

findSome?

@[simp]

theorem List.findSome?_cons_of_isSome {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {a : α✝} {l : List α✝} (h : (f a).isSome = true) : findSome? f (a :: l) = f a

@[simp]

theorem List.findSome?_cons_of_isNone {α✝ : Type u_1} {α✝¹ : Type u_2} {f : α✝ → Option α✝¹} {a : α✝} {l : List α✝} (h : (f a).isNone = true) : findSome? f (a :: l) = findSome? f l

theorem List.exists_of_findSome?_eq_some {α : Type u_1} {β : Type u_2} {b : β} {l : List α} {f : α → Option β} (w : findSome? f l = some b) : ∃ (a : α), a ∈ l ∧ f a = some b

@[simp]

theorem List.findSome?_eq_none_iff {α✝ : Type u_1} {α✝¹ : Type u_2} {p : α✝ → Option α✝¹} {l : List α✝} : findSome? p l = none ↔ ∀ (x : α✝), x ∈ l → p x = none

@[simp]

theorem List.findSome?_isSome_iff {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} : (findSome? f l).isSome = true ↔ ∃ (x : α), x ∈ l ∧ (f x).isSome = true

theorem List.findSome?_eq_some_iff {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} {b : β} : findSome? f l = some b ↔ ∃ (l₁ : List α), ∃ (a : α), ∃ (l₂ : List α), l = l₁ ++ a :: l₂ ∧ f a = some b ∧ ∀ (x : α), x ∈ l₁ → f x = none

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

@[simp]

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

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

@[simp]

theorem List.head?_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} : (filterMap f l).head? = findSome? f l

@[simp]

theorem List.head_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} (h : filterMap f l ≠ []) : (filterMap f l).head h = (findSome? f l).get ⋯

@[simp]

theorem List.getLast?_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} : (filterMap f l).getLast? = findSome? f l.reverse

@[simp]

theorem List.getLast_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} (h : filterMap f l ≠ []) : (filterMap f l).getLast h = (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 (findSome? f l) = findSome? (Option.map g ∘ f) l

theorem List.findSome?_map {β : Type u_1} {γ : Type u_2} {α✝ : Type u_3} {p : γ → Option α✝} {f : β → γ} {l : List β} : findSome? p (map f l) = findSome? (p ∘ f) l

theorem List.head_flatten {α : Type u_1} {L : List (List α)} (h : ∃ (l : List α), l ∈ L ∧ l ≠ []) : L.flatten.head ⋯ = (findSome? head? L).get ⋯

theorem List.getLast_flatten {α : Type u_1} {L : List (List α)} (h : ∃ (l : List α), l ∈ L ∧ l ≠ []) : L.flatten.getLast ⋯ = (findSome? getLast? L.reverse).get ⋯

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

theorem List.Sublist.findSome?_isSome {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} {l₁ l₂ : List α} (h : l₁.Sublist l₂) : (findSome? f l₁).isSome = true → (findSome? f l₂).isSome = true

theorem List.Sublist.findSome?_eq_none {α : Type u_1} {α✝ : Type u_2} {f : α → Option α✝} {l₁ l₂ : List α} (h : l₁.Sublist l₂) : findSome? f l₂ = none → findSome? f l₁ = none

theorem List.IsPrefix.findSome?_eq_some {α : Type u_1} {β : Type u_2} {b : β} {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <+: l₂) : findSome? f l₁ = some b → findSome? f l₂ = some b

theorem List.IsPrefix.findSome?_eq_none {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <+: l₂) : findSome? f l₂ = none → findSome? f l₁ = none

theorem List.IsSuffix.findSome?_eq_none {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <:+ l₂) : findSome? f l₂ = none → findSome? f l₁ = none

theorem List.IsInfix.findSome?_eq_none {α : Type u_1} {β : Type u_2} {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <:+: l₂) : findSome? f l₂ = none → findSome? f l₁ = none

find?

@[simp]

theorem List.find?_cons_of_pos {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} {l : List α✝} (h : p a = true) : find? p (a :: l) = some a

@[simp]

theorem List.find?_cons_of_neg {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} {l : List α✝} (h : ¬p a = true) : find? p (a :: l) = find? p l

@[simp]

theorem List.find?_eq_none {α✝ : Type u_1} {p : α✝ → Bool} {l : List α✝} : find? p l = none ↔ ∀ (x : α✝), x ∈ l → ¬p x = true

theorem List.find?_eq_some_iff_append {α✝ : Type u_1} {b : α✝} {p : α✝ → Bool} {xs : List α✝} : find? p xs = some b ↔ p b = true ∧ ∃ (as : List α✝), ∃ (bs : List α✝), xs = as ++ b :: bs ∧ ∀ (a : α✝), a ∈ as → (!p a) = true

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

@[simp]

theorem List.find?_cons_eq_some {α✝ : Type u_1} {a : α✝} {xs : List α✝} {p : α✝ → Bool} {b : α✝} : find? p (a :: xs) = some b ↔ p a = true ∧ a = b ∨ (!p a) = true ∧ find? p xs = some b

@[simp]

theorem List.find?_isSome {α : Type u_1} {xs : List α} {p : α → Bool} : (find? p xs).isSome = true ↔ ∃ (x : α), x ∈ xs ∧ p x = true

theorem List.find?_some {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} {l : List α✝} : find? p l = some a → p a = true

theorem List.mem_of_find?_eq_some {α✝ : Type u_1} {p : α✝ → Bool} {a : α✝} {l : List α✝} : find? p l = some a → a ∈ l

theorem List.get_find?_mem {α : Type u_1} {xs : List α} {p : α → Bool} (h : (find? p xs).isSome = true) : (find? p xs).get h ∈ xs

@[simp]

theorem List.find?_filter {α : Type u_1} {xs : List α} {p q : α → Bool} : find? q (filter p xs) = find? (fun (a : α) => decide (p a = true ∧ q a = true)) xs

@[simp]

theorem List.head?_filter {α : Type u_1} {p : α → Bool} {l : List α} : (filter p l).head? = find? p l

@[simp]

theorem List.head_filter {α : Type u_1} {p : α → Bool} {l : List α} (h : filter p l ≠ []) : (filter p l).head h = (find? p l).get ⋯

@[simp]

theorem List.getLast?_filter {α : Type u_1} {p : α → Bool} {l : List α} : (filter p l).getLast? = find? p l.reverse

@[simp]

theorem List.getLast_filter {α : Type u_1} {p : α → Bool} {l : List α} (h : filter p l ≠ []) : (filter p l).getLast h = (find? p l.reverse).get ⋯

@[simp]

theorem List.find?_filterMap {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → Option β} {p : β → Bool} : find? p (filterMap f xs) = (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 β} : find? p (map f l) = Option.map f (find? (p ∘ f) l)

@[simp]

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

theorem List.find?_flatten_eq_none_iff {α : Type u_1} {xs : List (List α)} {p : α → Bool} : find? p xs.flatten = none ↔ ∀ (ys : List α), ys ∈ xs → ∀ (x : α), x ∈ ys → (!p x) = true

theorem List.find?_flatten_eq_some_iff {α : Type u_1} {xs : List (List α)} {p : α → Bool} {a : α} : find? p xs.flatten = some a ↔ p a = true ∧ ∃ (as : List (List α)), ∃ (ys : List α), ∃ (zs : List α), ∃ (bs : List (List α)), xs = as ++ (ys ++ a :: zs) :: bs ∧ (∀ (l : List α), l ∈ as → ∀ (x : α), x ∈ l → (!p x) = true) ∧ ∀ (x : α), x ∈ ys → (!p x) = true

If find? p returns some a from xs.flatten, 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?_flatMap {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → List β} {p : β → Bool} : find? p (flatMap f xs) = findSome? (fun (x : α) => find? p (f x)) xs

theorem List.find?_flatMap_eq_none_iff {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → List β} {p : β → Bool} : find? p (flatMap f xs) = none ↔ ∀ (x : α), x ∈ xs → ∀ (y : β), y ∈ f x → (!p y) = true

theorem List.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 List.find?_replicate_of_length_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 List.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 List.find?_replicate_of_neg {α✝ : Type u_1} {p : α✝ → Bool} {n : Nat} {a : α✝} (h : ¬p a = true) : find? p (replicate n a) = none

theorem List.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 List.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 List.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 List.Sublist.find?_isSome {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α} (h : l₁.Sublist l₂) : (find? p l₁).isSome = true → (find? p l₂).isSome = true

theorem List.Sublist.find?_eq_none {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α} (h : l₁.Sublist l₂) : find? p l₂ = none → find? p l₁ = none

theorem List.IsPrefix.find?_eq_some {α : Type u_1} {b : α} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) : find? p l₁ = some b → find? p l₂ = some b

theorem List.IsPrefix.find?_eq_none {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) : find? p l₂ = none → find? p l₁ = none

theorem List.IsSuffix.find?_eq_none {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+ l₂) : find? p l₂ = none → find? p l₁ = none

theorem List.IsInfix.find?_eq_none {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+: l₂) : find? p l₂ = none → 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} : 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)

findIdx? (preliminary lemmas)

@[simp]

theorem List.findIdx?_nil {α : Type u_1} {p : α → Bool} : findIdx? p [] = none

theorem List.findIdx?_cons {α✝ : Type u_1} {x : α✝} {xs : List α✝} {p : α✝ → Bool} : findIdx? p (x :: xs) = if p x = true then some 0 else Option.map (fun (i : Nat) => i + 1) (findIdx? p xs)

@[simp]

theorem List.findIdx?_singleton {α : Type u_1} {a : α} {p : α → Bool} : findIdx? p [a] = if p a = true then some 0 else none

findIdx

theorem List.findIdx_cons {α : Type u_1} {p : α → Bool} {b : α} {l : List α} : findIdx p (b :: l) = if p b = true then 0 else findIdx p l + 1

@[simp]

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

theorem List.findIdx_of_getElem?_eq_some {α : Type u_1} {p : α → Bool} {y : α} {xs : List α} (w : xs[findIdx p xs]? = some y) : p y = true

theorem List.findIdx_getElem {α : Type u_1} {p : α → Bool} {xs : List α} {w : findIdx p xs < xs.length} : p xs[findIdx p xs] = true

theorem List.findIdx_lt_length_of_exists {α : Type u_1} {p : α → Bool} {xs : List α} (h : ∃ (x : α), x ∈ xs ∧ p x = true) : findIdx p xs < xs.length

theorem List.findIdx_getElem?_eq_getElem_of_exists {α : Type u_1} {p : α → Bool} {xs : List α} (h : ∃ (x : α), x ∈ xs ∧ p x = true) : xs[findIdx p xs]? = some xs[findIdx p xs]

@[simp]

theorem List.findIdx_eq_length {α : Type u_1} {p : α → Bool} {xs : List α} : findIdx p xs = xs.length ↔ ∀ (x : α), x ∈ xs → p x = false

theorem List.findIdx_eq_length_of_false {α : Type u_1} {p : α → Bool} {xs : List α} (h : ∀ (x : α), x ∈ xs → p x = false) : findIdx p xs = xs.length

theorem List.findIdx_le_length {α : Type u_1} {p : α → Bool} {xs : List α} : findIdx p xs ≤ xs.length

@[simp]

theorem List.findIdx_lt_length {α : Type u_1} {p : α → Bool} {xs : List α} : findIdx p xs < xs.length ↔ ∃ (x : α), x ∈ xs ∧ p x = true

theorem List.not_of_lt_findIdx {α : Type u_1} {p : α → Bool} {xs : List α} {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 List.le_findIdx_of_not {α : Type u_1} {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length) (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 List.lt_findIdx_of_not {α : Type u_1} {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length) (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 List.findIdx_eq {α : Type u_1} {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length) : 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.

@[simp]

theorem List.lt_findIdx_iff {α : Type u_1} (xs : List α) (p : α → Bool) (i : Nat) : i < findIdx p xs ↔ ∃ (h : i < xs.length), ∀ (j : Nat) (hj : j ≤ i), p xs[j] = false

@[simp]

theorem List.findIdx_map {α : Type u_1} {β : Type u_2} (xs : List α) (f : α → β) (p : β → Bool) : findIdx p (map f xs) = findIdx (p ∘ f) xs

theorem List.findIdx_append {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α} : findIdx p (l₁ ++ l₂) = if findIdx p l₁ < l₁.length then findIdx p l₁ else findIdx p l₂ + l₁.length

theorem List.IsPrefix.findIdx_le {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) : findIdx p l₁ ≤ findIdx p l₂

theorem List.IsPrefix.findIdx_eq_of_findIdx_lt_length {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) (lt : findIdx p l₁ < l₁.length) : findIdx p l₂ = findIdx p l₁

theorem List.findIdx_le_findIdx {α : Type u_1} {l : List α} {p q : α → Bool} (h : ∀ (x : α), x ∈ l → p x = true → q x = true) : findIdx q l ≤ findIdx p l

@[simp]

theorem List.findIdx_subtype {α : Type u_1} {p : α → Prop} {l : List { x : α // p x }} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : findIdx f l = findIdx g l.unattach

findIdx?

@[simp]

theorem List.findIdx?_eq_none_iff {α : Type u_1} {xs : List α} {p : α → Bool} : findIdx? p xs = none ↔ ∀ (x : α), x ∈ xs → p x = false

@[simp]

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

@[simp]

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

theorem List.findIdx?_eq_some_iff_findIdx_eq {α : Type u_1} {xs : List α} {p : α → Bool} {i : Nat} : findIdx? p xs = some i ↔ i < xs.length ∧ 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) : findIdx? p xs = some (findIdx p xs)

theorem List.findIdx?_eq_none_iff_findIdx_eq {α : Type u_1} {xs : List α} {p : α → Bool} : findIdx? p xs = none ↔ findIdx p xs = xs.length

theorem List.findIdx?_eq_guard_findIdx_lt {α : Type u_1} {xs : List α} {p : α → Bool} : findIdx? p xs = Option.guard (fun (i : Nat) => decide (i < xs.length)) (findIdx p xs)

theorem List.findIdx?_eq_some_iff_getElem {α : Type u_1} {xs : List α} {p : α → Bool} {i : Nat} : findIdx? p xs = some i ↔ ∃ (h : i < xs.length), p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true

theorem List.of_findIdx?_eq_some {α : Type u_1} {i : Nat} {xs : List α} {p : α → Bool} (w : findIdx? p xs = some i) : match xs[i]? with | some a => p a = true | none => false = true

theorem List.of_findIdx?_eq_none {α : Type u_1} {xs : List α} {p : α → Bool} (w : findIdx? p xs = none) (i : Nat) : match xs[i]? with | some a => ¬p a = true | none => true = true

@[simp]

theorem List.findIdx?_map {β : Type u_1} {α : Type u_2} {p : α → Bool} {f : β → α} {l : List β} : findIdx? p (map f l) = findIdx? (p ∘ f) l

@[simp]

theorem List.findIdx?_append {α : Type u_1} {xs ys : List α} {p : α → Bool} : findIdx? p (xs ++ ys) = (findIdx? p xs).or (Option.map (fun (i : Nat) => i + xs.length) (findIdx? p ys))

theorem List.findIdx?_flatten {α : Type u_1} {l : List (List α)} {p : α → Bool} : findIdx? p l.flatten = Option.map (fun (i : Nat) => (map length (take i l)).sum + (Option.map (fun (xs : List α) => findIdx p xs) l[i]?).getD 0) (findIdx? (fun (x : List α) => x.any p) l)

@[simp]

theorem List.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 List.findIdx?_eq_findSome?_zipIdx {α : Type u_1} {xs : List α} {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 List.findIdx?_eq_fst_find?_zipIdx {α : Type u_1} {xs : List α} {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 List.findIdx?_eq_none_of_findIdx?_eq_none {α : Type u_1} {xs : List α} {p q : α → Bool} (w : ∀ (x : α), x ∈ xs → p x = true → q x = true) : findIdx? q xs = none → findIdx? p xs = none

theorem List.Sublist.findIdx?_isSome {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α} (h : l₁.Sublist l₂) : (findIdx? p l₁).isSome = true → (findIdx? p l₂).isSome = true

theorem List.Sublist.findIdx?_eq_none {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α} (h : l₁.Sublist l₂) : findIdx? p l₂ = none → findIdx? p l₁ = none

theorem List.IsPrefix.findIdx?_eq_some {α : Type u_1} {i : Nat} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) : findIdx? p l₁ = some i → findIdx? p l₂ = some i

theorem List.IsPrefix.findIdx?_eq_none {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) : findIdx? p l₂ = none → findIdx? p l₁ = none

theorem List.IsSuffix.findIdx?_eq_none {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+ l₂) : findIdx? p l₂ = none → findIdx? p l₁ = none

theorem List.IsInfix.findIdx?_eq_none {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+: l₂) : findIdx? p l₂ = none → findIdx? p l₁ = none

theorem List.findIdx_eq_getD_findIdx? {α : Type u_1} {xs : List α} {p : α → Bool} : findIdx p xs = (findIdx? p xs).getD xs.length

@[simp]

theorem List.findIdx?_subtype {α : Type u_1} {p : α → Prop} {l : List { x : α // p x }} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : findIdx? f l = findIdx? g l.unattach

findFinIdx?

@[simp]

theorem List.findFinIdx?_nil {α : Type u_1} {p : α → Bool} : findFinIdx? p [] = none

theorem List.findIdx?_go_eq_map_findFinIdx?_go_val {α : Type u_1} {l xs : List α} {p : α → Bool} {i : Nat} {h : xs.length + i = l.length} : findIdx?.go p xs i = Option.map (fun (x : Fin l.length) => ↑x) (findFinIdx?.go p l xs i h)

theorem List.findIdx?_eq_map_findFinIdx?_val {α : Type u_1} {xs : List α} {p : α → Bool} : findIdx? p xs = Option.map (fun (x : Fin xs.length) => ↑x) (findFinIdx? p xs)

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

theorem List.findFinIdx?_cons {α : Type u_1} {p : α → Bool} {x : α} {xs : List α} : findFinIdx? p (x :: xs) = if p x = true then some 0 else Option.map Fin.succ (findFinIdx? p xs)

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

@[simp]

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

@[simp]

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

@[simp]

theorem List.findFinIdx?_eq_some_iff {α : Type u_1} {xs : List α} {p : α → Bool} {i : Fin xs.length} : findFinIdx? p xs = some i ↔ p xs[i] = true ∧ ∀ (j : Fin xs.length) (hji : j < i), ¬p xs[j] = true

@[simp]

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

@[simp]

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

@[simp]

theorem List.findFinIdx?_subtype {α : Type u_1} {p : α → Prop} {l : List { x : α // p x }} {f : { x : α // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : findFinIdx? f l = Option.map (fun (i : Fin l.unattach.length) => Fin.cast ⋯ i) (findFinIdx? g l.unattach)

find? and findFinIdx?

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

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

theorem List.find?_eq_getElem?_findIdx {α : Type u_1} {xs : List α} {p : α → Bool} : find? p xs = xs[findIdx p 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 List.idxOf_cons {α : Type u_1} {x : α} {xs : List α} {y : α} [BEq α] : idxOf y (x :: xs) = if (x == y) = true then 0 else idxOf y xs + 1

@[simp]

theorem List.idxOf_cons_self {α : Type u_1} {a : α} [BEq α] [ReflBEq α] {l : List α} : idxOf a (a :: l) = 0

@[simp]

theorem List.getElem_idxOf {α : Type u_1} [BEq α] [LawfulBEq α] {x : α} {xs : List α} (h : idxOf x xs < xs.length) : xs[idxOf x xs] = x

Indexing a list at the position idxOf x recovers x, provided x occurs in the list.

theorem List.idxOf_append {α : Type u_1} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} {a : α} : idxOf a (l₁ ++ l₂) = if a ∈ l₁ then idxOf a l₁ else idxOf a l₂ + l₁.length

theorem List.idxOf_eq_length {α : Type u_1} {a : α} [BEq α] [LawfulBEq α] {l : List α} (h : ¬a ∈ l) : idxOf a l = l.length

theorem List.idxOf_lt_length_of_mem {α : Type u_1} {a : α} [BEq α] [EquivBEq α] {l : List α} (h : a ∈ l) : idxOf a l < l.length

theorem List.idxOf_le_length {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} : idxOf a l ≤ l.length

theorem List.idxOf_lt_length_iff {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} : idxOf a l < l.length ↔ a ∈ l

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 List.idxOf?_eq_map_finIdxOf?_val {α : Type u_1} [BEq α] {xs : List α} {a : α} : idxOf? a xs = Option.map (fun (x : Fin xs.length) => ↑x) (finIdxOf? a xs)

@[simp]

theorem List.finIdxOf?_nil {α : Type u_1} {a : α} [BEq α] : finIdxOf? a [] = none

theorem List.finIdxOf?_cons {α : Type u_1} {b : α} [BEq α] {a : α} {xs : List α} : finIdxOf? b (a :: xs) = if (a == b) = true then some ⟨0, ⋯⟩ else Option.map (fun (x : Fin xs.length) => x.succ) (finIdxOf? b xs)

@[simp]

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

@[simp]

theorem List.finIdxOf?_eq_some_iff {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} {i : Fin l.length} : finIdxOf? a l = some i ↔ l[i] = a ∧ ∀ (j : Fin l.length), j < i → ¬l[j] = a

@[simp]

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

@[simp]

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

idxOf?

The verification API for idxOf? is still incomplete. The lemmas below should be made consistent with those for findIdx? (and proved using them).

@[simp]

theorem List.idxOf?_nil {α : Type u_1} {a : α} [BEq α] : idxOf? a [] = none

theorem List.idxOf?_cons {α : Type u_1} [BEq α] {a : α} {xs : List α} {b : α} : idxOf? b (a :: xs) = if (a == b) = true then some 0 else Option.map (fun (x : Nat) => x + 1) (idxOf? b xs)

@[simp]

theorem List.idxOf?_singleton {α : Type u_1} [BEq α] {a b : α} : idxOf? b [a] = if (a == b) = true then some 0 else none

@[simp]

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

theorem List.idxOf?_eq_some_iff {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} {i : Nat} : idxOf? a l = some i ↔ ∃ (h : i < l.length), l[i] = a ∧ ∀ (j : Nat) (x : j < i), ¬l[j] = a

@[simp]

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

theorem List.isNone_idxOf? {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} : ((idxOf? a l).isNone = true) = ¬a ∈ l

theorem List.finIdxOf?_eq_pmap_idxOf? {α : Type u_1} {l : List α} {a : α} [BEq α] [LawfulBEq α] : finIdxOf? a l = Option.pmap (fun (i : Nat) (h : idxOf? a l = some i) => ⟨i, ⋯⟩) (idxOf? a l) ⋯

find? and idxOf?

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

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

theorem List.findIdx_eq_getD_bind_find?_idxOf? {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} {p : α → Bool} : findIdx p xs = ((find? p xs).bind fun (a : α) => idxOf? a xs).getD xs.length

lookup

@[simp]

theorem List.lookup_cons_self {α : Type u_2} [BEq α] {β✝ : Type u_1} {b : β✝} {es : List (α × β✝)} [ReflBEq α] {k : α} : lookup k ((k, b) :: es) = some b

@[simp]

theorem List.lookup_singleton {α : Type u_1} [BEq α] {c a b : α} : lookup c [(a, b)] = if (c == a) = true then some b else none

theorem List.lookup_eq_findSome? {α : Type u_2} [BEq α] {β : Type u_1} {l : List (α × β)} {k : α} : lookup k l = findSome? (fun (p : α × β) => if (k == p.fst) = true then some p.snd else none) l

@[simp]

theorem List.lookup_eq_none_iff {α : Type u_2} [BEq α] {β : Type u_1} {l : List (α × β)} {k : α} : lookup k l = none ↔ ∀ (p : α × β), p ∈ l → (k != p.fst) = true

@[simp]

theorem List.lookup_isSome_iff {α : Type u_2} [BEq α] {β : Type u_1} {l : List (α × β)} {k : α} : (lookup k l).isSome = true ↔ ∃ (p : α × β), p ∈ l ∧ (k == p.fst) = true

theorem List.lookup_eq_some_iff {α : Type u_2} [BEq α] {β : Type u_1} [LawfulBEq α] {l : List (α × β)} {k : α} {b : β} : lookup k l = some b ↔ ∃ (l₁ : List (α × β)), ∃ (l₂ : List (α × β)), l = l₁ ++ (k, b) :: l₂ ∧ ∀ (p : α × β), p ∈ l₁ → (k != p.fst) = true

theorem List.lookup_append {α : Type u_2} [BEq α] {β : Type u_1} {l₁ l₂ : List (α × β)} {k : α} : lookup k (l₁ ++ l₂) = (lookup k l₁).or (lookup k l₂)

theorem List.lookup_replicate {α : Type u_2} [BEq α] {n : Nat} {a : α} {α✝ : Type u_1} {b : α✝} {k : α} : lookup k (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 α] {n : Nat} {a : α} {α✝ : Type u_1} {b : α✝} {k : α} (h : 0 < n) : lookup k (replicate n (a, b)) = if (k == a) = true then some b else none

theorem List.lookup_replicate_self {α : Type u_2} [BEq α] {n : Nat} {α✝ : Type u_1} {b : α✝} [ReflBEq α] {a : α} : lookup a (replicate n (a, b)) = if n = 0 then none else some b

@[simp]

theorem List.lookup_replicate_self_of_pos {α : Type u_2} [BEq α] {n : Nat} {α✝ : Type u_1} {b : α✝} [ReflBEq α] {a : α} (h : 0 < n) : lookup a (replicate n (a, b)) = some b

@[simp]

theorem List.lookup_replicate_ne {α : Type u_2} [BEq α] {a : α} {n : Nat} {α✝ : Type u_1} {b : α✝} {k : α} (h : (!k == a) = true) : lookup k (replicate n (a, b)) = none

theorem List.Sublist.lookup_isSome {α : Type u_2} [BEq α] {β : Type u_1} {k : α} {l₁ l₂ : List (α × β)} (h : l₁.Sublist l₂) : (lookup k l₁).isSome = true → (lookup k l₂).isSome = true

theorem List.Sublist.lookup_eq_none {α : Type u_2} [BEq α] {β : Type u_1} {k : α} {l₁ l₂ : List (α × β)} (h : l₁.Sublist l₂) : lookup k l₂ = none → lookup k l₁ = none

theorem List.IsPrefix.lookup_eq_some {α : Type u_2} [BEq α] {β : Type u_1} {k : α} {b : β} {l₁ l₂ : List (α × β)} (h : l₁ <+: l₂) : lookup k l₁ = some b → lookup k l₂ = some b

theorem List.IsPrefix.lookup_eq_none {α : Type u_2} [BEq α] {β : Type u_1} {k : α} {l₁ l₂ : List (α × β)} (h : l₁ <+: l₂) : lookup k l₂ = none → lookup k l₁ = none

theorem List.IsSuffix.lookup_eq_none {α : Type u_2} [BEq α] {β : Type u_1} {k : α} {l₁ l₂ : List (α × β)} (h : l₁ <:+ l₂) : lookup k l₂ = none → lookup k l₁ = none

theorem List.IsInfix.lookup_eq_none {α : Type u_2} [BEq α] {β : Type u_1} {k : α} {l₁ l₂ : List (α × β)} (h : l₁ <:+: l₂) : lookup k l₂ = none → lookup k l₁ = none