Properties of Lists

This file contains useful lemmas about standard list functions and our custom variations on these.

any

theorem List.any_of_mem {α : Type u_1} {f : α → Bool} {x : α} {xs : List α} (h₁ : x ∈ xs) (h₂ : f x = true) : xs.any f = true

all

theorem List.all_pmap_subtype {α : Type u_1} {p : α → Prop} (f : α → Bool) (as : List α) (h : ∀ (a : α), a ∈ as → p a) : ((pmap Subtype.mk as h).all fun (x : { a : α // p a }) => f x.val) = as.all f

Copied from Mathlib. We can delete this if it gets added to Batteries.

map, map₁, map₂, map₃, and attach variants

theorem List.map_congr {α : Type u_1} {β : Type u_2} {f g : α → β} {l : List α} : (∀ (x : α), x ∈ l → f x = g x) → map f l = map g l

Copied from Mathlib. We can delete this if it gets added to Batteries.

theorem List.map_eq_doubleton {α : Type u_1} {β : Type u_2} {f : α → β} {xs : List α} {y₁ y₂ : β} : map f xs = [y₁, y₂] → ∃ (x₁ : α), ∃ (x₂ : α), xs = [x₁, x₂]

Similar to the standard library's map_eq_singleton_iff, but for doubleton.

We could probably make this an iff but currently don't need to.

theorem List.map_pmap_subtype {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : α → β) (as : List α) (h : ∀ (a : α), a ∈ as → p a) : map (fun (x : { a : α // p a }) => f x.val) (pmap Subtype.mk as h) = map f as

Copied from Mathlib. We can delete this if it gets added to Batteries.

theorem List.map_pmap_subtype_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {p : α × β → Prop} (f : β → γ) (xs : List (α × β)) (h : ∀ (pair : α × β), pair ∈ xs → p pair) : map (fun (x : { pair : α × β // p pair }) => (x.val.fst, f x.val.snd)) (pmap Subtype.mk xs h) = map (fun (pair : α × β) => (pair.fst, f pair.snd)) xs

Not actually a special case of map_pmap_subtype -- you can use this in places you can't use map_pmap_subtype because the LHS function (being mapped) doesn't fit the map_pmap_subtype form but does fit this form (where the application of f is not the outermost AST node of the function, basically)

theorem List.attach_def {α : Type u_1} {as : List α} : as.attach = pmap Subtype.mk as ⋯

theorem List.mem_attach₂ {α : Type u_1} {β : Type u_2} [SizeOf α] [SizeOf β] {as : List (α × β)} {pair : { x : α × β // sizeOf x.snd < 1 + sizeOf as }} : pair ∈ as.attach₂ → (pair.val.fst, pair.val.snd) ∈ as

theorem List.mem_attach₂_iff {α : Type u_1} {β : Type u_2} [SizeOf α] [SizeOf β] {xs : List (α × β)} {pair : { x : α × β // sizeOf x.snd < 1 + sizeOf xs }} : pair ∈ xs.attach₂ ↔ pair.val ∈ xs

@[simp]

theorem List.all_attach₂ {α : Type u_1} {β : Type u_2} [SizeOf α] [SizeOf β] {as : List (α × β)} {f : α × β → Bool} : (as.attach₂.all fun (x : { x : α × β // sizeOf x.snd < 1 + sizeOf as }) => match x with | ⟨pair, property⟩ => f pair) = as.all f

@[simp]

theorem List.all_attach₂_snd {α : Type u_1} {β : Type u_2} [SizeOf α] [SizeOf β] {as : List (α × β)} {f : β → Bool} : (as.attach₂.all fun (x : { x : α × β // sizeOf x.snd < 1 + sizeOf as }) => match x with | ⟨(fst, b), property⟩ => f b) = as.all fun (x : α × β) => match x with | (fst, b) => f b

theorem List.map₁_eq_map {α : Type u_1} {β : Type u_2} (f : α → β) (as : List α) : (as.map₁ fun (x : { x : α // x ∈ as }) => f x.val) = map f as

theorem List.map₂_eq_map {γ : Type u_1} {α : Type u} {β : Type v} [SizeOf α] [SizeOf β] {xs : List (α × β)} (f : α × β → γ) : (xs.map₂ fun (x : { x : α × β // sizeOf x.snd < 1 + sizeOf xs }) => f x.val) = map f xs

theorem List.map₃_eq_map {γ : Type u_1} {α : Type u} {β : Type v} [SizeOf α] [SizeOf β] {xs : List (α × β)} (f : α × β → γ) : (xs.map₃ fun (x : { x : α × β // sizeOf x.snd < 1 + (1 + sizeOf xs) }) => f x.val) = map f xs

theorem List.map₂_eq_map_snd {γ : Type u_1} {α : Type u} {β : Type v} [SizeOf α] [SizeOf β] {xs : List (α × β)} (f : β → γ) : (xs.map₂ fun (x : { x : α × β // sizeOf x.snd < 1 + sizeOf xs }) => match x with | ⟨(a, b), property⟩ => (a, f b)) = map (fun (x : α × β) => match x with | (a, b) => (a, f b)) xs

Not actually a special case of map₂_eq_map -- you can use this in places you can't use map₂_eq_map because the LHS function (being mapped) doesn't fit the map₂_eq_map form but does fit this form (where the application of f is not the outermost AST node of the function, basically)

theorem List.map₃_eq_map_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SizeOf α] [SizeOf β] {xs : List (α × β)} (f : β → γ) : (xs.map₃ fun (x : { x : α × β // sizeOf x.snd < 1 + (1 + sizeOf xs) }) => match x with | ⟨(a, b), property⟩ => (a, f b)) = map (fun (x : α × β) => match x with | (a, b) => (a, f b)) xs

same as map₂_eq_map_snd but for map₃

flatMap

theorem List.exists_iff_mem_flatMap {α : Type u_1} {β : Type u_2} [DecidableEq β] {f : α → List β} {xs : List α} {b : β} : b ∈ flatMap f xs ↔ ∃ (a : α), a ∈ xs ∧ b ∈ f a

As of this writing, the standard-library lemma List.exists_of_mem_flatMap is a →, but it's trivial to extend it to ↔ and makes some things easier, so we do that here

Forall₂

The following lemmas are copied from Mathlib. They live in Cedar.List rather than List so that a file can import both Cedar and Mathlib without a duplicate-declaration error. Code inside the Cedar namespace can still refer to them as List.<name>, since Lean resolves names in enclosing namespaces first.

theorem Cedar.List.forall₂_nil_left_iff {α✝ : Type u_1} {α✝¹ : Type u_2} {R : α✝ → α✝¹ → Prop} {l : List α✝¹} : List.Forall₂ R [] l ↔ l = []

Copied from Mathlib

theorem Cedar.List.forall₂_nil_right_iff {α✝ : Type u_1} {β✝ : Type u_2} {R : α✝ → β✝ → Prop} {l : List α✝} : List.Forall₂ R l [] ↔ l = []

Copied from Mathlib

theorem Cedar.List.Forall₂.imp {α✝ : Type u_1} {α✝¹ : Type u_2} {R S : α✝ → α✝¹ → Prop} (H : ∀ (a : α✝) (b : α✝¹), R a b → S a b) {l₁ : List α✝} {l₂ : List α✝¹} (h : List.Forall₂ R l₁ l₂) : List.Forall₂ S l₁ l₂

Copied from Mathlib

theorem Cedar.List.forall₂_cons_left_iff {α✝ : Type u_1} {α✝¹ : Type u_2} {R : α✝ → α✝¹ → Prop} {a : α✝} {l : List α✝} {u : List α✝¹} : List.Forall₂ R (a :: l) u ↔ ∃ (b : α✝¹), ∃ (u' : List α✝¹), R a b ∧ List.Forall₂ R l u' ∧ u = b :: u'

Copied from Mathlib

theorem Cedar.List.forall₂_cons_right_iff {α✝ : Type u_1} {α✝¹ : Type u_2} {R : α✝ → α✝¹ → Prop} {b : α✝¹} {l : List α✝¹} {u : List α✝} : List.Forall₂ R u (b :: l) ↔ ∃ (a : α✝), ∃ (u' : List α✝), R a b ∧ List.Forall₂ R u' l ∧ u = a :: u'

Copied from Mathlib

theorem List.forall₂_singleton_right_iff {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {xs : List α} {y : β} : Forall₂ R xs [y] ↔ ∃ (x : α), R x y ∧ xs = [x]

theorem List.forall₂_pair_right_iff {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {xs : List α} {y₁ y₂ : β} : Forall₂ R xs [y₁, y₂] ↔ ∃ (x₁ : α), ∃ (x₂ : α), R x₁ y₁ ∧ R x₂ y₂ ∧ xs = [x₁, x₂]

theorem List.forall₂_implies_all_left {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {xs : List α} {ys : List β} : Forall₂ R xs ys → ∀ (x : α), x ∈ xs → ∃ (y : β), y ∈ ys ∧ R x y

Note the converse is not true: counterexample R is =, xs is [1], ys is [1, 2]

theorem List.forall₂_implies_all_right {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {xs : List α} {ys : List β} : Forall₂ R xs ys → ∀ (y : β), y ∈ ys → ∃ (x : α), x ∈ xs ∧ R x y

theorem List.forall₂_iff_map_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → γ} {g : β → γ} {xs : List α} {ys : List β} : Forall₂ (fun (x : α) (y : β) => f x = g y) xs ys ↔ map f xs = map g ys

theorem List.forall₂_fun_subset_implies {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {xs xs' : List α} {ys ys' : List β} : Forall₂ R xs ys → Forall₂ R xs' ys' → (∀ {x : α} {y y' : β}, R x y → R x y' → y = y') → xs ⊆ xs' → ys ⊆ ys'

theorem List.forall₂_fun_equiv_implies {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {xs xs' : List α} {ys ys' : List β} : Forall₂ R xs ys → Forall₂ R xs' ys' → (∀ {x : α} {y y' : β}, R x y → R x y' → y = y') → xs ≡ xs' → ys ≡ ys'

The converse (ys ≡ ys' → xs ≡ xs') doesn't hold without requiring R to be injective (as well as functional).

theorem List.map_preserves_forall₂ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {f : α → α'} {g : β → β'} {p₁ : α → β → Prop} {p₂ : α' → β' → Prop} {xs : List α} {ys : List β} (h : ∀ (x : α) (y : β), p₁ x y → p₂ (f x) (g y)) (hforall₂ : Forall₂ p₁ xs ys) : Forall₂ p₂ (map f xs) (map g ys)

theorem List.forall₂_swap {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {xs : List α} {ys : List β} (hforall₂ : Forall₂ (fun (y : β) (x : α) => R x y) ys xs) : Forall₂ R xs ys

theorem List.forall₂_compose_mapM_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l₁ : List α} {l₂ : List β} {l₃ : List γ} {R₁ : α → β → Prop} {R₂ : α → γ → Prop} {f : β → Option γ} (h : Forall₂ R₁ l₁ l₂) (hmapM : mapM f l₂ = some l₃) (hf : ∀ (a : α) (b : β), R₁ a b → ∃ (c : γ), f b = some c ∧ R₂ a c) : Forall₂ R₂ l₁ l₃

Applying mapM on the RHS list of Forall₂ leads to new Forall₂ relation if certain conditions are met.

theorem List.forall₂_eq_implies_filterMap {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} {p : α → β → Prop} {f : α → Option β} (h : Forall₂ p l₁ l₂) (hp : ∀ (a : α) (b : β), p a b → f a = some b) : filterMap f l₁ = l₂

theorem List.forall₂_trans_ish {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : List α} {ys : List β} {zs : List γ} {Q : α → β → Prop} {R : α → γ → Prop} {S : β → γ → Prop} (h₁ : Forall₂ Q xs ys) (h₂ : Forall₂ R xs zs) : (∀ {a : α} {b : β} {c : γ}, Q a b → R a c → S b c) → Forall₂ S ys zs

kind of a transitivity property, if you squint

theorem List.forall₂_find?_some {α : Type u_1} {β : Type u_2} [DecidableEq α] {r : α × β → α × β → Prop} {xs ys : List (α × β)} {k : α} {x : α × β} (hkeys : ∀ (x y : α × β), r x y → y.fst = x.fst) (hrel : Forall₂ r xs ys) (hfind : find? (fun (x : α × β) => x.fst == k) xs = some x) : ∃ (y : α × β), find? (fun (x : α × β) => x.fst == k) ys = some y ∧ r x y

In key-preserving related lists, an entry found for a key has a related entry found for it.

theorem List.forall₂_find?_none {α : Type u_1} {β : Type u_2} [DecidableEq α] {r : α × β → α × β → Prop} {xs ys : List (α × β)} {k : α} (hkeys : ∀ (x y : α × β), r x y → y.fst = x.fst) (hrel : Forall₂ r xs ys) (hfind : find? (fun (x : α × β) => x.fst == k) xs = none) : find? (fun (x : α × β) => x.fst == k) ys = none

In key-preserving related lists, a key absent from one list is absent from the other.

mapM, mapM', mapM₁, and mapM₂

theorem List.mapM_some {α : Type u_1} {xs : List α} : mapM some xs = some xs

theorem List.mapM_isSome {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → Option β} : (mapM f xs).isSome = xs.all fun (value : α) => (f value).isSome

mapM succeeds exactly when every application succeeds.

theorem List.mapM₁_def {m : Type u_1 → Type u_2} [Monad m] {α : Type u_3} {β : Type u_1} (xs : List α) (f : { x : α // x ∈ xs } → m β) : xs.mapM₁ f = mapM f xs.attach

Equation lemma for List.mapM₁, for clients that cannot unfold it.

theorem List.mapM₁_eq_mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (f : α → m β) (as : List α) : (as.mapM₁ fun (x : { x : α // x ∈ as }) => f x.val) = mapM f as

theorem List.mapM₂_eq_mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} [Monad m] [LawfulMonad m] [SizeOf α] [SizeOf β] (f : α × β → m γ) (as : List (α × β)) : (as.mapM₂ fun (x : { _x : α × β // sizeOf _x.snd < 1 + sizeOf as }) => f x.val) = mapM f as

theorem List.mapM₂_eq_map_snd {m : Type (max u_1 u) → Type u_2} {γ : Type (max u_1 u)} {α : Type u} {β : Type v} [SizeOf α] [SizeOf β] [Monad m] [LawfulMonad m] {xs : List (α × β)} (f : β → m γ) : (xs.mapM₂ fun (x : { x : α × β // sizeOf x.snd < 1 + sizeOf xs }) => match x with | ⟨(a, b), property⟩ => do let __do_lift ← f b pure (a, __do_lift)) = mapM (fun (x : α × β) => match x with | (a, b) => do let __do_lift ← f b pure (a, __do_lift)) xs

See notes on map₂_eq_map_snd. This has a similar relationship to mapM₂_eq_mapM as map₂_eq_map_snd does to map₂_eq_map.

theorem List.mapM₃_eq_mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} [Monad m] [LawfulMonad m] [SizeOf α] [SizeOf β] (f : α × β → m γ) (as : List (α × β)) : (as.mapM₃ fun (x : { x : α × β // sizeOf x.snd < 1 + (1 + sizeOf as) }) => f x.val) = mapM f as

theorem List.mapM_implies_nil {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Except β γ} {as : List α} (h₁ : mapM f as = Except.ok []) : as = []

theorem List.mapM_head_tail {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Except β γ} {x : α} {xs : List α} {y : γ} {ys : List γ} : mapM f (x :: xs) = Except.ok (y :: ys) → mapM f xs = Except.ok ys

theorem List.mapM'_preserves_length {α✝ : Type u_1} {ε✝ : Type u_2} {α✝¹ : Type u_3} {f : α✝ → Except ε✝ α✝¹} {xs : List α✝} {ys : List α✝¹} : mapM' f xs = Except.ok ys → xs.length = ys.length

theorem List.mapM_preserves_length {α✝ : Type u_1} {ε✝ : Type u_2} {α✝¹ : Type u_3} {f : α✝ → Except ε✝ α✝¹} {xs : List α✝} {ys : List α✝¹} : mapM f xs = Except.ok ys → xs.length = ys.length

theorem List.not_mem_implies_not_mem_mapM_key_id {α β : Type} {ks : List α} {kvs : List (α × β)} {fn : α → Option β} {k : α} (hm : mapM (fun (k : α) => do let __do_lift ← fn k some (k, __do_lift)) ks = some kvs) (hl : ¬k ∈ ks) (v : β) : ¬(k, v) ∈ kvs

theorem List.mapM'_ok_iff_forall₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Except γ β} {xs : List α} {ys : List β} : mapM' f xs = Except.ok ys ↔ Forall₂ (fun (x : α) (y : β) => f x = Except.ok y) xs ys

theorem List.mapM'_some_iff_forall₂ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : List α} {ys : List β} : mapM' f xs = some ys ↔ Forall₂ (fun (x : α) (y : β) => f x = some y) xs ys

Copy of mapM'_ok_iff_forall₂ but for option instead of exception

theorem List.mapM_ok_iff_forall₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Except γ β} {xs : List α} {ys : List β} : mapM f xs = Except.ok ys ↔ Forall₂ (fun (x : α) (y : β) => f x = Except.ok y) xs ys

theorem List.mapM_some_iff_forall₂ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : List α} {ys : List β} : mapM f xs = some ys ↔ Forall₂ (fun (x : α) (y : β) => f x = some y) xs ys

theorem List.mapM_implies_forall₂ {α : Type u_1} {ε : Type u_2} {β : Type u_3} {f : α → Except ε β} {p : α → β → Prop} {xs : List α} {ys : List β} (h : ∀ (x : α) (y : β), x ∈ xs → f x = Except.ok y → p x y) (hmapM : mapM f xs = Except.ok ys) : Forall₂ p xs ys

Introduces forall₂ through the input output relation of a f through List.mapM. This is slightly stronger than the forward direction of mapM_ok_iff_forall₂ since it allowed an extra x ∈ xs condition in h.

theorem List.mapM_implies_forall₂_option {α : Type u_1} {β : Type u_2} {f : α → Option β} {p : α → β → Prop} {xs : List α} {ys : List β} (h : ∀ (x : α) (y : β), x ∈ xs → f x = some y → p x y) (hmapM : mapM f xs = some ys) : Forall₂ p xs ys

Same as mapM_implies_forall₂ but for Option

theorem List.mapM'_ok_implies_all_ok {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Except γ β} {xs : List α} {ys : List β} : mapM' f xs = Except.ok ys → ∀ (x : α), x ∈ xs → ∃ (y : β), y ∈ ys ∧ f x = Except.ok y

Note that the converse is not true: counterexample xs is [1], ys is [1, 2], f is Except.ok

But for a limited converse, see all_ok_implies_mapM'_ok

theorem List.mapM_ok_implies_all_ok {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Except γ β} {xs : List α} {ys : List β} : mapM f xs = Except.ok ys → ∀ (x : α), x ∈ xs → ∃ (y : β), y ∈ ys ∧ f x = Except.ok y

theorem List.all_ok_implies_mapM'_ok {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Except γ β} {xs : List α} : (∀ (x : α), x ∈ xs → ∃ (y : β), f x = Except.ok y) → ∃ (ys : List β), mapM' f xs = Except.ok ys

theorem List.all_ok_implies_mapM_ok {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Except γ β} {xs : List α} : (∀ (x : α), x ∈ xs → ∃ (y : β), f x = Except.ok y) → ∃ (ys : List β), mapM f xs = Except.ok ys

theorem List.mapM'_ok_implies_all_from_ok {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Except γ β} {xs : List α} {ys : List β} : mapM' f xs = Except.ok ys → ∀ (y : β), y ∈ ys → ∃ (x : α), x ∈ xs ∧ f x = Except.ok y

Note that the converse is not true: counterexample ys is [1], xs is [1, 2], f is Except.ok

But for a limited converse, see all_from_ok_implies_mapM'_ok

theorem List.mapM_ok_implies_all_from_ok {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Except γ β} {xs : List α} {ys : List β} : mapM f xs = Except.ok ys → ∀ (y : β), y ∈ ys → ∃ (x : α), x ∈ xs ∧ f x = Except.ok y

theorem List.all_from_ok_implies_mapM'_ok {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Except γ β} {ys : List β} : (∀ (y : β), y ∈ ys → ∃ (x : α), f x = Except.ok y) → ∃ (xs : List α), mapM' f xs = Except.ok ys

theorem List.all_from_ok_implies_mapM_ok {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Except γ β} {ys : List β} : (∀ (y : β), y ∈ ys → ∃ (x : α), f x = Except.ok y) → ∃ (xs : List α), mapM f xs = Except.ok ys

theorem List.mapM'_error_implies_exists_error {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Except γ β} {xs : List α} {e : γ} : mapM' f xs = Except.error e → ∃ (x : α), x ∈ xs ∧ f x = Except.error e

The converse is not true: counterexample xs is [1, 2] and f is Except.error. In that case, f 2 = .error 2 but xs.mapM' f = .error 1.

But for a limited converse, see element_error_implies_mapM_error

theorem List.mapM_error_implies_exists_error {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Except γ β} {xs : List α} {e : γ} : mapM f xs = Except.error e → ∃ (x : α), x ∈ xs ∧ f x = Except.error e

theorem List.filterMapM_error_implies_exists_error {α : Type u_1} {β : Type u_2} {ε : Type u_3} {f : α → Except ε (Option β)} {xs : List α} {e : ε} : filterMapM f xs = Except.error e → ∃ (x : α), x ∈ xs ∧ f x = Except.error e

theorem List.element_error_implies_mapM'_error {α : Type u_1} {ε : Type u_2} {β : Type u_3} {x : α} {xs : List α} {f : α → Except ε β} {e : ε} : x ∈ xs → f x = Except.error e → ∃ (e' : ε), mapM' f xs = Except.error e'

If applying f to any of xs produces an error, then xs.mapM' f must also produce an error (not necessarily the same error)

Limited converse of mapM'_error_implies_exists_error

theorem List.element_error_implies_mapM_error {α : Type u_1} {ε : Type u_2} {β : Type u_3} {x : α} {xs : List α} {f : α → Except ε β} {e : ε} : x ∈ xs → f x = Except.error e → ∃ (e' : ε), mapM f xs = Except.error e'

theorem List.element_to_option_none_implies_mapM_none {α : Type u_1} {β : Type u_2} {ε : Type u_3} {ls : List α} {x : α} {f : α → Except ε β} (h₁ : x ∈ ls) (h₂ : (f x).toOption = none) : (mapM f ls).toOption = none

theorem List.mapM'_ok_eq_filterMap {ε : Type u_1} {α : Type u_2} {β : Type u_3} {f : α → Except ε β} {xs : List α} {ys : List β} : mapM' f xs = Except.ok ys → filterMap (fun (x : α) => match f x with | Except.ok y => some y | Except.error a => none) xs = ys

theorem List.mapM_ok_eq_filterMap {ε : Type u_1} {α : Type u_2} {β : Type u_3} {f : α → Except ε β} {xs : List α} {ys : List β} : mapM f xs = Except.ok ys → filterMap (fun (x : α) => match f x with | Except.ok y => some y | Except.error a => none) xs = ys

theorem List.mapM'_some_implies_all_some {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : List α} {ys : List β} : mapM' f xs = some ys → ∀ (x : α), x ∈ xs → ∃ (y : β), y ∈ ys ∧ f x = some y

Note that the converse is not true: counterexample xs is [1], ys is [1, 2], f is Option.some

But for a limited converse, see all_some_implies_mapM'_some

theorem List.mapM_some_implies_all_some {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : List α} {ys : List β} : mapM f xs = some ys → ∀ (x : α), x ∈ xs → ∃ (y : β), y ∈ ys ∧ f x = some y

theorem List.mem_mapM_some_implies_exists_unmapped_helper {α : Type u_1} {β : Type u_2} {y : β} {f : α → Option β} {xs : List α} {ys : List β} : Forall₂ (fun (x : α) (y : β) => f x = some y) xs ys → y ∈ ys → ∃ (x : α), x ∈ xs ∧ f x = some y

theorem List.mem_mapM_some_implies_exists_unmapped {α : Type u_1} {β : Type u_2} {y : β} {f : α → Option β} {xs : List α} {ys : List β} : mapM f xs = some ys → y ∈ ys → ∃ (x : α), x ∈ xs ∧ f x = some y

theorem List.all_some_implies_mapM'_some {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : List α} : (∀ (x : α), x ∈ xs → ∃ (y : β), f x = some y) → ∃ (ys : List β), mapM' f xs = some ys

theorem List.all_some_implies_mapM_some {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : List α} : (∀ (x : α), x ∈ xs → ∃ (y : β), f x = some y) → ∃ (ys : List β), mapM f xs = some ys

theorem List.mapM'_some_implies_all_from_some {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : List α} {ys : List β} : mapM' f xs = some ys → ∀ (y : β), y ∈ ys → ∃ (x : α), x ∈ xs ∧ f x = some y

Note that the converse is not true: counterexample ys is [1], xs is [1, 2], f is Option.some

But for a limited converse, see all_from_some_implies_mapM'_some

theorem List.mapM_some_implies_all_from_some {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : List α} {ys : List β} : mapM f xs = some ys → ∀ (y : β), y ∈ ys → ∃ (x : α), x ∈ xs ∧ f x = some y

theorem List.all_from_some_implies_mapM'_some {α : Type u_1} {β : Type u_2} {f : α → Option β} {ys : List β} : (∀ (y : β), y ∈ ys → ∃ (x : α), f x = some y) → ∃ (xs : List α), mapM' f xs = some ys

theorem List.all_from_some_implies_mapM_some {α : Type u_1} {β : Type u_2} {f : α → Option β} {ys : List β} : (∀ (y : β), y ∈ ys → ∃ (x : α), f x = some y) → ∃ (xs : List α), mapM f xs = some ys

theorem List.mapM'_none_iff_exists_none {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : List α} : mapM' f xs = none ↔ ∃ (x : α), x ∈ xs ∧ f x = none

theorem List.mapM_none_iff_exists_none {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : List α} : mapM f xs = none ↔ ∃ (x : α), x ∈ xs ∧ f x = none

theorem List.mapM'_some_eq_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : List α} {ys : List β} : mapM' f xs = some ys → filterMap f xs = ys

theorem List.mapM_some_eq_filterMap {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : List α} {ys : List β} : mapM f xs = some ys → filterMap f xs = ys

theorem List.mapM'_some_subset {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs xs' : List α} {ys : List β} : mapM' f xs = some ys → xs' ⊆ xs → ∃ (ys' : List β), mapM' f xs' = some ys'

theorem List.mapM_some_subset {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs xs' : List α} {ys : List β} : mapM f xs = some ys → xs' ⊆ xs → ∃ (ys' : List β), mapM f xs' = some ys'

theorem List.forall₂_implies_mapM_eq {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} {ε : Type u_4} {xs : List α₁} {ys : List α₂} (f : α₁ → Except ε β) (g : α₂ → Except ε β) : Forall₂ (fun (x : α₁) (y : α₂) => f x = g y) xs ys → mapM f xs = mapM g ys

theorem List.mapM'_congr {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {f g : α → m β} {l : List α} : (∀ (x : α), x ∈ l → f x = g x) → mapM' f l = mapM' g l

our own variant of map_congr, for mapM'

theorem List.mapM_congr {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {f g : α → m β} {l : List α} : (∀ (x : α), x ∈ l → f x = g x) → mapM f l = mapM g l

our own variant of map_congr, for mapM

theorem List.to_option_distr_mapM' {α : Type u_1} {β : Type u_2} {ε : Type u_3} {l : List α} {f : α → Except ε β} : (mapM' f l).toOption = mapM' (Except.toOption ∘ f) l

theorem List.to_option_distr_mapM {α : Type u_1} {β : Type u_2} {ε : Type u_3} {l : List α} {f : α → Except ε β} : (mapM f l).toOption = mapM (Except.toOption ∘ f) l

theorem List.mapM_to_option_congr {α : Type u_1} {β : Type u_2} {ε₁ : Type u_3} {ε₂ : Type u_4} {l : List α} {f : α → Except ε₁ β} {g : α → Except ε₂ β} : (∀ (x : α), x ∈ l → (f x).toOption = (g x).toOption) → (mapM f l).toOption = (mapM g l).toOption

foldl

theorem List.foldl_pmap_subtype {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : β → α → β) (as : List α) (init : β) (h : ∀ (a : α), a ∈ as → p a) : foldl (fun (b : β) (x : { a : α // p a }) => f b x.val) init (pmap Subtype.mk as h) = foldl f init as

theorem List.foldl_congr {β : Type u_1} {α : Type u_2} {f g : β → α → β} {init : β} {l : List α} : (∀ (b : β) (x : α), x ∈ l → f b x = g b x) → foldl f init l = foldl g init l

foldlM

theorem List.foldlM_of_assoc_some {α : Type u_1} (f : α → α → Option α) (x₀ x₁ x₂ x₃ : α) (xs : List α) (h₁ : ∀ (x₁ x₂ x₃ : α), (do let x₄ ← f x₁ x₂ f x₄ x₃) = do let x₄ ← f x₂ x₃ f x₁ x₄) (h₂ : f x₀ x₁ = some x₂) (h₃ : foldlM f x₂ xs = some x₃) : (do let y ← foldlM f x₁ xs f x₀ y) = some x₃

theorem List.foldlM_of_assoc_none' {α : Type u_1} (f : α → α → Option α) (x₀ x₁ x₂ : α) (xs : List α) (h₁ : ∀ (x₁ x₂ x₃ : α), (do let x₄ ← f x₁ x₂ f x₄ x₃) = do let x₄ ← f x₂ x₃ f x₁ x₄) (h₂ : f x₀ x₁ = none) (h₃ : foldlM f x₁ xs = some x₂) : f x₀ x₂ = none

theorem List.foldlM_of_assoc_none {α : Type u_1} (f : α → α → Option α) (x₀ x₁ x₂ : α) (xs : List α) (h₁ : ∀ (x₁ x₂ x₃ : α), (do let x₄ ← f x₁ x₂ f x₄ x₃) = do let x₄ ← f x₂ x₃ f x₁ x₄) (h₂ : f x₀ x₁ = some x₂) (h₃ : foldlM f x₂ xs = none) : (do let y ← foldlM f x₁ xs f x₀ y) = none

theorem List.foldlM_of_assoc {α : Type u_1} (f : α → α → Option α) (x₀ x₁ : α) (xs : List α) (h₁ : ∀ (x₁ x₂ x₃ : α), (do let x₄ ← f x₁ x₂ f x₄ x₃) = do let x₄ ← f x₂ x₃ f x₁ x₄) : foldlM f x₀ (x₁ :: xs) = do let y ← foldlM f x₁ xs f x₀ y

find?

theorem List.find?_pair_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [BEq α] (f : β → γ) (xs : List (α × β)) (k : α) : Option.map (fun (x : α × β) => (x.fst, f x.snd)) (find? (fun (x : α × β) => x.fst == k) xs) = find? (fun (x : α × γ) => x.fst == k) (map (fun (x : α × β) => (x.fst, f x.snd)) xs)

theorem List.find?_fst_map_implies_find? {α : Type u_1} {β : Type u_2} {γ : Type u_3} [BEq α] {f : β → γ} {xs : List (α × β)} {k : α} {fx : α × γ} : find? (fun (x : α × γ) => x.fst == k) (map (Prod.map id f) xs) = some fx → ∃ (x : α × β), find? (fun (x : α × β) => x.fst == k) xs = some x ∧ fx = Prod.map id f x

theorem List.find?_implies_find?_fst_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} [BEq α] [ReflBEq α] {l : List (α × β)} {k : α} {v : β} {f : α → β → γ} (h : find? (fun (x : α × β) => x.fst == k) l = some (k, v)) : find? (fun (x : α × γ) => x.fst == k) (map (fun (x : α × β) => match x with | (k, v) => (k, f k v)) l) = some (k, f k v)

theorem List.find?_implies_append_find? {α : Type u_1} {a b : List α} {v : α} {f : α → Bool} (h : find? f a = some v) : find? f (a ++ b) = some v

theorem List.not_find?_some_iff_find?_none {α : Type u_1} {p : α → Bool} {xs : List α} : (∀ (x : α), x ∈ xs → ¬find? p xs = some x) ↔ find? p xs = none

theorem List.find?_exact_iff_mem {α : Type u_1} [DecidableEq α] {l : List α} {v : α} : find? (fun (x : α) => x == v) l = some v ↔ v ∈ l

filterMap

theorem Cedar.List.filterMap_congr {α : Type u_1} {β : Type u_2} {f g : α → Option β} {l : List α} : (∀ (x : α), x ∈ l → f x = g x) → List.filterMap f l = List.filterMap g l

our own variant of map_congr, for filterMap

theorem List.filterMap_empty_iff_all_none {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : List α} : filterMap f xs = [] ↔ ∀ (x : α), x ∈ xs → f x = none

theorem List.filterMap_nonempty_iff_exists_some {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : List α} : filterMap f xs ≠ [] ↔ ∃ (x : α), x ∈ xs ∧ (f x).isSome = true

theorem List.f_implies_g_then_subset {α : Type u_1} {β : Type u_2} {f g : α → Option β} {xs : List α} : (∀ (a : α) (b : β), f a = some b → g a = some b) → filterMap f xs ⊆ filterMap g xs

forM and mapM

theorem List.mapM_forM {α β : Type} (f : α → Except β PUnit) (xs : List α) (ys : List PUnit) : mapM f xs = Except.ok ys → xs.forM f = Except.ok ()

theorem List.forM_mapM {α β : Type} (f : α → Except β PUnit) (xs : List α) : xs.forM f = Except.ok () → ∃ (ys : List PUnit), mapM f xs = Except.ok ys

theorem List.forM_ok_implies_all_ok {α β : Type} (xs : List α) (f : α → Except β Unit) : xs.forM f = Except.ok () → ∀ (x : α), x ∈ xs → f x = Except.ok ()

theorem List.forM_ok_implies_all_ok' {α β : Type} {xs : List α} {f : α → Except β Unit} : xs.forM f = Except.ok () → ∀ (x : α), x ∈ xs → f x = Except.ok ()

theorem List.all_ok_implies_forM_ok {α β : Type} (xs : List α) (f : α → Except β Unit) : (∀ (x : α), x ∈ xs → f x = Except.ok ()) → xs.forM f = Except.ok ()

removeAll

theorem List.removeAll_singleton_cons_of_neq {α : Type u_1} [DecidableEq α] (x y : α) (xs : List α) : x ≠ y → (x :: xs).removeAll [y] = x :: xs.removeAll [y]

theorem List.removeAll_singleton_cons_of_eq {α : Type u_1} [DecidableEq α] (x : α) (xs : List α) : (x :: xs).removeAll [x] = xs.removeAll [x]

theorem List.mem_removeAll_singleton_of_eq {α : Type u_1} [DecidableEq α] (x : α) (xs : List α) : ¬x ∈ xs.removeAll [x]

theorem List.removeAll_singleton_equiv {α : Type u_1} [DecidableEq α] (x : α) (xs : List α) : x :: xs ≡ x :: xs.removeAll [x]

theorem List.length_removeAll_le {α : Type u_1} [BEq α] (xs ys : List α) : (xs.removeAll ys).length ≤ xs.length

theorem List.mem_pmap_subtype {α : Type u_1} {p : α → Prop} (as : List α) (h : ∀ (a : α), a ∈ as → p a) (a : α) (ha : p a) : ⟨a, ha⟩ ∈ pmap Subtype.mk as h ↔ a ∈ as

theorem List.find?_compose {α : Type u_1} {β : Sort u_2} (f : α → β) (p₁ : β → Bool) (p₂ : α → Bool) {xs : List α} : (∀ (x : α), (p₁ ∘ f) x = p₂ x) → find? (p₁ ∘ f) xs = find? p₂ xs

theorem List.mem_implies_mem_eraseDups {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} {x : α} (hmem : x ∈ xs) : x ∈ xs.eraseDups

theorem List.mem_eraseDups_implies_mem {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} {x : α} (hmem : x ∈ xs.eraseDups) : x ∈ xs

theorem List.mem_iff_mem_eraseDups {α : Type u_1} [BEq α] [LawfulBEq α] {xs : List α} {x : α} : x ∈ xs ↔ x ∈ xs.eraseDups

theorem List.mapM_preserves_SortedBy {γ : Type u_1} {α : Type u_2} {β : Type u_3} [LT γ] {l₁ : List α} {l₂ : List β} {f : α → Option β} {k₁ : α → γ} {k₂ : β → γ} (hsorted : SortedBy k₁ l₁) (hmapM : mapM f l₁ = some l₂) (hkey : ∀ (a : α) (b : β), f a = some b → k₁ a = k₂ b) : SortedBy k₂ l₂

mapM preserves SortedBy if the keys are preserved

theorem List.map_restricted_id {α : Type u_1} {l : List α} {f : α → α} (hf : ∀ (x : α), x ∈ l → f x = x) : map f l = l

theorem List.findSome?_unique {α : Type u_1} {β : Type u_2} [BEq α] [LawfulBEq α] {l : List α} {x : α} {y : β} {f : α → Option β} (hfind : x ∈ l) (hf : ∀ (x' : α), (∃ (y' : β), f x' = some y') → x' = x) (hx : f x = some y) : findSome? f l = some y

theorem List.find?_unique_entry {α : Type u_1} {l : List α} {f : α → Bool} {v : α} (hf : ∀ (x : α), x ∈ l → f x = true → x = v) (hmem : v ∈ l) (hv : f v = true) : find? f l = some v

theorem List.find?_stronger_pred {α : Type u_1} {l : List α} {v : α} {f g : α → Bool} (hfind : find? f l = some v) (hg : ∀ (x : α), x ∈ l → g x = true → f x = true) (hv : g v = true) : find? g l = some v

theorem List.mem_of_map_implies_exists_unmapped {α : Type u_1} {β : Type u_2} {l : List α} {v₂ : β} {f : α → β} : v₂ ∈ map f l → ∃ (v₁ : α), v₁ ∈ l ∧ v₂ = f v₁

theorem List.mem_map_iff_find? {β : Type u_1} {α : Type u_2} [BEq β] [LawfulBEq β] {k : β} {f : α → β} {kvs : List α} : k ∈ map f kvs ↔ (find? (fun (x : α) => f x == k) kvs).isSome = true

theorem List.mem_implies_find? {α : Type u_1} {l : List α} {k : α} {f : α → Bool} (hmem : k ∈ l) (hk : f k = true) (hf : ∀ (k' : α), f k' = true → k' = k) : find? f l = some k

theorem List.filterMap_eq_filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l₁ : List α} {l₂ : List β} {p : α → β → Prop} {f₁ : α → Option γ} {f₂ : β → Option γ} (h : Forall₂ p l₁ l₂) (hp : ∀ (a : α) (b : β), p a b → f₁ a = f₂ b) : filterMap f₁ l₁ = filterMap f₂ l₂

theorem List.find?_filter_if_find? {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] {k : α} {val : β} {l : List (α × β)} (p : α → β → Bool) : find? (fun (x : α × β) => x.fst == k) l = some (k, val) → p k val = true → find? (fun (x : α × β) => x.fst == k) (filter (fun (kv : α × β) => p kv.fst kv.snd) l) = some (k, val)

theorem List.find?_filter_sorted {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] [DecidableEq α] [LT α] [Cedar.Data.StrictLT α] [DecidableLT α] (k : α) (val : β) (l : List (α × β)) (p : α → β → Bool) : SortedBy Prod.fst l → find? (fun (x : α × β) => x.fst == k) (filter (fun (kv : α × β) => p kv.fst kv.snd) l) = some (k, val) → find? (fun (x : α × β) => x.fst == k) l = some (k, val) ∧ p k val = true

theorem List.anyM_some_implies_any {α : Type u_1} {xs : List α} {b : Bool} (f : α → Option Bool) (g : α → Bool) : (∀ (x : α) (b : Bool), f x = some b → g x = b) → anyM f xs = some b → xs.any g = b

theorem List.ternary_any_some_implies_any {α : Type u_1} {xs : List α} {b : Bool} (f : α → Option Bool) (g : α → Bool) : (∀ (x : α) (b : Bool), f x = some b → g x = b) → xs.ternaryAny f = some b → xs.any g = b