Properties of list utilities

Miscellaneous list lemmas: Forall/Rel₂, Disj, Subset, removeAll/replaceAll, uniq, and zip/map results.

Key theorems

• List.Forall_mem_iff, List.Forall_append, List.Forall_flatMap, List.all_mono, List.forall_of_all_decide
• List.Disjoint_app, List.Disjoint_Nodup_iff
• List.nodup_uniq, List.length_dedup_of_subset_le
• List.length_eq_of_nodup_of_mem_iff, List.inj_implies_nodup, List.sum_size_le
• List.nodupB_eq_true_iff — the linear nodupB check decides Nodup
• List.mem_groupValuesByKey, List.of_mem_groupValuesByKey — membership in groupValuesByKey

theorem List.all_mono {α : Type} {source target : α → Bool} {xs : List α} (hmono : ∀ (x : α), source x = true → target x = true) (h : xs.all source = true) : xs.all target = true

List.all is monotone under pointwise implication between Boolean predicates.

theorem List.forall_of_all_decide {α : Type} {l : List α} {p : α → Prop} [DecidablePred p] (h : (l.all fun (x : α) => decide (p x)) = true) (x : α) : x ∈ l → p x

Every element of a list satisfies a decidable predicate when the list's all check of it passes.

@[simp]

theorem List.Forall_nil {α : Type u_1} (p : α → Prop) : Forall p [] ↔ True

@[simp]

theorem List.Forall_cons {α : Type u_1} (p : α → Prop) (x : α) (l : List α) : Forall p (x :: l) ↔ p x ∧ Forall p l

theorem List.Forall_mem_iff {α : Type u_1} {p : α → Prop} {l : List α} : Forall p l ↔ ∀ (x : α), x ∈ l → p x

theorem List.Forall_append {α✝ : Type u_1} {P : α✝ → Prop} {a b : List α✝} : Forall P (a ++ b) ↔ Forall P a ∧ Forall P b

theorem List.Disjoint_nil_left {α : Type u_1} (l : List α) : [].Disj l

The empty list is disjoint from anything.

theorem List.Disjoint_singleton_left {α : Type u_1} {a : α} {l : List α} : [a].Disj l ↔ ¬a ∈ l

A singleton is disjoint from l iff its element is not in l.

theorem List.Disjoint_cons_left {α : Type u_1} {a : α} {l₁ l₂ : List α} : (a :: l₁).Disj l₂ ↔ ¬a ∈ l₂ ∧ l₁.Disj l₂

Disjointness on a cons splits into head-membership and tail-disjointness.

Nodup / membership length lemmas

theorem List.length_eq_of_nodup_of_mem_iff {κ : Type u_1} [BEq κ] [LawfulBEq κ] {l₁ l₂ : List κ} (d₁ : l₁.Nodup) (d₂ : l₂.Nodup) (hmem : ∀ (a : κ), a ∈ l₁ ↔ a ∈ l₂) : l₁.length = l₂.length

Two duplicate-free lists with the same membership have equal length.

theorem List.inj_implies_nodup {α : Type u_1} (l : List α) (p : ∀ (i j : Nat) (p : i < l.length) (q : j < l.length), l[i] = l[j] → i = j) : l.Nodup

theorem List.sum_size_le {α : Type u_1} (f : α → Nat) {l : List α} {x : α} (x_in : x ∈ l) : f x ≤ (map f l).sum

An element's measure is bounded by the sum of the mapped measures.

theorem List.append_subset_append {α : Type u_1} {a a' b b' : List α} (ha : a ⊆ a') (hb : b ⊆ b') : a ++ b ⊆ a' ++ b'

Monotonicity of list ⊆ under ++.

theorem List.mem_map_snd_zip {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) (v : β) (h : v ∈ map Prod.snd (l₁.zip l₂)) : v ∈ l₂

Values in the snd projection of a zip are members of the second list.

theorem List.nodup_uniq {α : Type} [DecidableEq α] (l : List α) : l.uniq.Nodup

A deduplicated list satisfies Nodup.

theorem List.length_dedup_le {α : Type} [DecidableEq α] (l : List α) : l.uniq.length ≤ l.length

The upper bound of the length of a deduplicated list is the length of the original list.

theorem List.length_dedup_cons_le {α : Type} [DecidableEq α] (a : α) (l : List α) : l.uniq.length ≤ (a :: l).uniq.length

The lower bound of the length of a deduplicated list with an element consed onto it (i.e., (a :: l)) is the length of the deduplicated list l.

theorem List.mem_dedup_of_mem {α : Type} [DecidableEq α] (l : List α) (a : α) : a ∈ l.uniq → a ∈ l

theorem List.mem_of_mem_dedup {α : Type} [DecidableEq α] (l : List α) (a : α) : a ∈ l → a ∈ l.uniq

theorem List.mem_of_dedup {α : Type} [DecidableEq α] (l : List α) (a : α) : a ∈ l ↔ a ∈ l.uniq

An element a is in a list l iff it is in the deduplicated version of l.

theorem List.uniqTR.go_eq {α : Type} [DecidableEq α] (l acc : List α) : go l acc = acc.reverse ++ l.uniq

@[csimp]

theorem List.dedup_eq_dedupTR : @uniq = @uniqTR

List.uniq is equivalent to uniqTR at compile time.

theorem List.length_dedup_cons_of_mem {α : Type} [DecidableEq α] (a : α) (l : List α) (h : a ∈ l) : (a :: l).uniq.length = l.uniq.length

theorem List.length_dedup_cons_of_not_mem {α : Type} [DecidableEq α] (a : α) (l : List α) (h : ¬a ∈ l) : (a :: l).uniq.length = 1 + l.uniq.length

theorem List.mem_append_left_of_mem_dedup {α : Type} [DecidableEq α] (a : α) (l₁ l₂ : List α) (h1 : ¬a ∈ l₂.uniq) (h2 : a ∈ (l₁ ++ l₂).uniq) : a ∈ l₁

theorem List.mem_append_right_of_mem_dedup {α : Type} [DecidableEq α] (a : α) (l₁ l₂ : List α) (h1 : ¬a ∈ l₁.uniq) (h2 : a ∈ (l₁ ++ l₂).uniq) : a ∈ l₂

theorem List.length_dedup_append_le_sum {α : Type} [DecidableEq α] (l₁ l₂ : List α) : (l₁ ++ l₂).uniq.length ≤ l₁.uniq.length + l₂.uniq.length

theorem List.removeAll_of_cons {α : Type} [DecidableEq α] (x : α) (xs ys : List α) (h : ¬x ∈ ys) : (x :: xs).removeAll ys = x :: xs.removeAll ys

theorem List.length_dedup_of_removeAll {α : Type} [DecidableEq α] (a : α) (l : List α) (h : a ∈ l) : l.uniq.length = 1 + (l.removeAll [a]).uniq.length

theorem List.length_dedup_append_le_left {α : Type} [DecidableEq α] (l₁ l₂ : List α) : l₁.uniq.length ≤ (l₁ ++ l₂).uniq.length

theorem List.length_dedup_append_all_in_right {α : Type} [DecidableEq α] (l₁ l₂ : List α) (h : (l₁.all fun (e : α) => decide (e ∈ l₂)) = true) : (l₁ ++ l₂).uniq.length = l₂.uniq.length

theorem List.length_dedup_append_subset_right {α : Type} [DecidableEq α] (l₁ l₂ : List α) (h : l₁ ⊆ l₂) : (l₁ ++ l₂).uniq.length = l₂.uniq.length

theorem List.length_dedup_append_all_in_left {α : Type} [DecidableEq α] (l₁ l₂ : List α) (h : (l₂.all fun (e : α) => decide (e ∈ l₁)) = true) : (l₁ ++ l₂).uniq.length = l₁.uniq.length

theorem List.length_dedup_all_in_eq {α : Type} [DecidableEq α] (l₁ l₂ : List α) (h1 : (l₁.all fun (e : α) => decide (e ∈ l₂)) = true) (h2 : (l₂.all fun (e : α) => decide (e ∈ l₁)) = true) : l₁.uniq.length = l₂.uniq.length

theorem List.length_dedup_subset_eq {α : Type} [DecidableEq α] (l₁ l₂ : List α) (h1 : l₁ ⊆ l₂) (h2 : l₂ ⊆ l₁) : l₁.uniq.length = l₂.uniq.length

theorem List.length_dedup_append_le_right {α : Type} [DecidableEq α] (l₁ l₂ : List α) : l₂.uniq.length ≤ (l₁ ++ l₂).uniq.length

theorem List.length_dedup_of_all_in_not_mem_lt {α : Type} [DecidableEq α] (l₁ l₂ : List α) (a : α) (h1 : (l₁.all fun (e : α) => decide (e ∈ l₂)) = true) (h2 : ¬a ∈ l₁) (h3 : a ∈ l₂) : l₁.uniq.length < l₂.uniq.length

theorem List.length_dedup_of_subset_not_mem_lt {α : Type} [DecidableEq α] (l₁ l₂ : List α) (a : α) (h1 : l₁ ⊆ l₂) (h2 : ¬a ∈ l₁) (h3 : a ∈ l₂) : l₁.uniq.length < l₂.uniq.length

theorem List.length_dedup_of_subset_le {α : Type} [DecidableEq α] (l₁ l₂ : List α) (h : l₁ ⊆ l₂) : l₁.uniq.length ≤ l₂.uniq.length

theorem List.subset_nodup_length {α : Type u_1} {s1 s2 : List α} (hn : s1.Nodup) (hsub : s1 ⊆ s2) : s1.length ≤ s2.length

theorem List.occurrences_len_eq_dedup {α : Type} [DecidableEq α] (l : List α) : l.uniq.length = l.occurrences.length

theorem List.occurrences_find {α : Type} [DecidableEq α] (l : List α) (x : α) (hx : x ∈ l) : find? (fun (x_1 : α × Nat) => match x_1 with | (k, snd) => k == x) l.occurrences = some (x, count x l)

theorem List.filter_length_le_of_imp {α : Type u_1} {L : List α} {P Q : α → Bool} (h_imp : ∀ (x : α), x ∈ L → P x = true → Q x = true) : (filter P L).length ≤ (filter Q L).length

If P x → Q x for all x ∈ L, then (L.filter P).length ≤ (L.filter Q).length.

theorem List.filter_length_lt_of_imp_witness {α : Type u_1} {L : List α} {P Q : α → Bool} {a : α} (h_imp : ∀ (x : α), x ∈ L → P x = true → Q x = true) (h_in : a ∈ L) (hQa : Q a = true) (hPa : ¬P a = true) : (filter P L).length < (filter Q L).length

If P x → Q x for all x ∈ L, and there is a witness a ∈ L with Q a but ¬P a, then (L.filter P).length < (L.filter Q).length.

theorem List.removeAll_eq_nil_of_forall_mem {α : Type u_1} [BEq α] [LawfulBEq α] {xs ys : List α} (h : ∀ (x : α), x ∈ xs → x ∈ ys) : xs.removeAll ys = []

If every element of xs is in ys, then xs.removeAll ys = [].

theorem List.removeAll_not_mem {α : Type u_1} [BEq α] [LawfulBEq α] {x : α} {xs : List α} (h : ¬x ∈ xs) : xs.removeAll [x] = xs

theorem List.foldl_subtype_zip_val {α : Type u_1} {β : Type u_2} {γ : Type u_3} (P : α → Prop) (f : γ → α → β → γ) (init : γ) (l₁ : List { x : α // P x }) (l₂ : List β) : foldl (fun (acc : γ) (p : { x : α // P x } × β) => f acc p.fst.val p.snd) init (l₁.zip l₂) = foldl (fun (acc : γ) (p : α × β) => f acc p.fst p.snd) init ((map Subtype.val l₁).zip l₂)

foldl over a zipped subtype list equals foldl over the zipped projected list.

theorem List.foldl_zip_congr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : γ → α → β → γ) (l₁ l₁' : List α) (l₂ l₂' : List β) (h_len₁ : l₁.length = l₁'.length) (h_len₂ : l₂.length = l₂'.length) (h_f : ∀ (i : Nat) (hi₁ : i < l₁.length) (hi₂ : i < l₂.length) (acc : γ), f acc l₁[i] l₂[i] = f acc l₁'[i] l₂'[i]) (init : γ) : foldl (fun (acc : γ) (p : α × β) => f acc p.fst p.snd) init (l₁.zip l₂) = foldl (fun (acc : γ) (p : α × β) => f acc p.fst p.snd) init (l₁'.zip l₂')

foldl over zipped lists is congruent when the function produces equal results on corresponding elements.

theorem List.nodup_of_nodup_map {α : Type u_1} {β : Type u_2} (f : α → β) {l : List α} (h : (map f l).Nodup) : l.Nodup

A list whose image under f is duplicate-free is duplicate-free.

theorem List.nodup_map_injOn {α β : Type} {f : α → β} {l : List α} (hnd : (map f l).Nodup) {a b : α} (ha : a ∈ l) (hb : b ∈ l) (hab : f a = f b) : a = b

theorem List.filter_compl_length {α : Type u_1} (l : List α) (p : α → Bool) : (filter p l).length + (filter (not ∘ p) l).length = l.length

Filtering a list by p and its complement preserves total length.

theorem List.partition_length {α : Type u_1} (l : List α) (p : α → Bool) : (partition p l).fst.length + (partition p l).snd.length = l.length

List.partition preserves total length.

theorem List.lookup_of_mem_nodup {α β : Type} [BEq α] [LawfulBEq α] (l : List (α × β)) (h_nodup : (map Prod.fst l).Nodup) (k : α) (v : β) (h_mem : (k, v) ∈ l) : lookup k l = some v

If a list of pairs has unique keys (Nodup), then membership implies the key can be looked up to find the corresponding value.

theorem List.nodupB_eq_true_iff {α : Type} [BEq α] [Hashable α] [LawfulBEq α] [LawfulHashable α] (l : List α) : l.nodupB = true ↔ l.Nodup

nodupB decides List.Nodup: it accepts a list exactly when the list has no duplicate elements.

theorem List.nodup_of_nodupB {α : Type} [BEq α] [Hashable α] [LawfulBEq α] [LawfulHashable α] {l : List α} (h : l.nodupB = true) : l.Nodup

If nodupB accepts a list, the list has no duplicate elements.

theorem List.mem_groupValuesByKey {K V : Type} [BEq K] [Hashable K] [LawfulBEq K] {keep : V → Bool} {l : List (K × V)} {x : K} {L : V} (hm : (x, L) ∈ l) (hk : keep L = true) : L ∈ (groupValuesByKey keep l).getD x []

A pair of l whose value passes keep has its value recorded under its key in groupValuesByKey keep l.

theorem List.of_mem_groupValuesByKey {K V : Type} [BEq K] [Hashable K] [LawfulBEq K] {keep : V → Bool} {l : List (K × V)} {x : K} {L : V} (h : L ∈ (groupValuesByKey keep l).getD x []) : (x, L) ∈ l

Every value recorded under key x in groupValuesByKey keep l comes from a pair (x, value) of l.

theorem List.orderedPairs_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : (map f l).orderedPairs = map (fun (q : α × α) => (f q.fst, f q.snd)) l.orderedPairs

The ordered pairs of a mapped list are the mapped pairs.

theorem List.mem_orderedPairs {α : Type u_1} {l : List α} {a b : α} : (a, b) ∈ l.orderedPairs → a ∈ l ∧ b ∈ l

Both elements of an ordered pair of a list belong to the list.

theorem List.Rel₂.head {α : Type u_1} {β : Type u_2} {a : α} {as : List α} {b : β} {bs : List β} {R : α → β → Prop} (h : Rel₂ R (a :: as) (b :: bs)) : R a b

theorem List.Rel₂.tail {α : Type u_1} {β : Type u_2} {a : α} {as : List α} {b : β} {bs : List β} {R : α → β → Prop} (h : Rel₂ R (a :: as) (b :: bs)) : Rel₂ R as bs

theorem List.Rel₂.length_eq {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {as : List α} {bs : List β} (h : Rel₂ R as bs) : as.length = bs.length

theorem List.Rel₂.get? {α : Type u_1} {β : Type u_2} {a : α} {b : β} {R : α → β → Prop} {as : List α} {bs : List β} (h : Rel₂ R as bs) (i : Nat) (ha : as[i]? = some a) (hb : bs[i]? = some b) : R a b

theorem List.Rel₂.getElem?_some {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l1 : List α} {l2 : List β} (h : Rel₂ R l1 l2) {i : Nat} {a : α} (ha : l1[i]? = some a) : ∃ (b : β), l2[i]? = some b ∧ R a b

If Rel₂ R l1 l2 and l1[i]? = some a, then there exists b with l2[i]? = some b and R a b.

theorem List.Rel₂.append {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l₁ l₂ : List α} {l₁' l₂' : List β} : Rel₂ R l₁ l₁' → Rel₂ R l₂ l₂' → Rel₂ R (l₁ ++ l₂) (l₁' ++ l₂')

Lists related position by position, concatenated, are related position by position.

theorem List.Rel₂.ne_nil {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l : List α} {l' : List β} (h : Rel₂ R l l') (hl : l ≠ []) : l' ≠ []

A list related position by position to a nonempty list is nonempty.

theorem List.Rel₂.append_singleton {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l : List α} {a : α} {l' : List β} : Rel₂ R (l ++ [a]) l' → ∃ (m : List β), ∃ (b : β), l' = m ++ [b] ∧ Rel₂ R l m ∧ R a b

A list related position by position to l ++ [a] is some m ++ [b], with m related to l and b to a.

theorem List.Rel₂.imp {α : Type u_1} {β : Type u_2} {R S : α → β → Prop} (H : ∀ (a : α) (b : β), R a b → S a b) {l : List α} {l' : List β} : Rel₂ R l l' → Rel₂ S l l'

Lists related position by position by R are related by any relation that R implies.

theorem List.Rel₂.unique {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l : List α} {l1 l2 : List β} (hR : ∀ (a : α) (b c : β), R a b → R a c → b = c) (h1 : Rel₂ R l l1) (h2 : Rel₂ R l l2) : l1 = l2

A pointwise relation that relates each element to at most one element relates a list to at most one list.

theorem List.Rel₂.eq {α : Type u_1} {R : α → α → Prop} {l1 l2 : List α} (hR : ∀ (a b : α), R a b → a = b) (h : Rel₂ R l1 l2) : l1 = l2

A pointwise relation that implies equality relates only equal lists.

theorem List.Rel₂.refl {α : Type u_1} {R : α → α → Prop} (hR : ∀ (a : α), R a a) (l : List α) : Rel₂ R l l

A reflexive relation relates every list to itself pointwise.

theorem List.Sublist.flatMap_of_sublist {α : Type u_1} {β : Type u_2} (f : α → List β) {l1 l2 : List α} (h : l1.Sublist l2) : (flatMap f l1).Sublist (flatMap f l2)

flatMap preserves the sublist relation.

Zip / map lemmas

theorem zip_map_fst_eq {α β : Type} (l1 : List α) (l2 : List β) : l1.length = l2.length → List.map Prod.fst (l1.zip l2) = l1

theorem zip_map_snd_eq {α β : Type} (l1 : List α) (l2 : List β) : l1.length = l2.length → List.map Prod.snd (l1.zip l2) = l2

theorem zip_find_mem_snd {α : Type u_1} {β : Type u_2} [BEq α] (l1 : List α) (l2 : List β) (x : α) (p : α × β) (h : List.find? (fun (p : α × β) => p.fst == x) (l1.zip l2) = some p) : p.snd ∈ l2

If find? returns a pair from a zipped list, its second component belongs to the second input list.

theorem perm_append_swap_middle {α : Type u_1} (a b c d : List α) : (a ++ b ++ (c ++ d)).Perm (a ++ c ++ (b ++ d))

(a ++ b) ++ (c ++ d) is a permutation of (a ++ c) ++ (b ++ d).

theorem foldl_insert_lookup {γ β : Type} (l : List γ) (key : γ → String) (val : γ → β) (m : Std.HashMap String β) (k : String) (v : β) : (List.foldl (fun (acc : Std.HashMap String β) (d : γ) => acc.insert (key d) (val d)) m l)[k]? = some v → (∃ (d : γ), d ∈ l ∧ key d = k ∧ val d = v) ∨ m[k]? = some v

After inserting key d ↦ val d into m for each d ∈ l, a lookup finds a value some d contributed or one m held.

theorem List.forall_eq_self_of_map_eq_self {α : Type} {F : α → α} {l : List α} (h : map F l = l) (t : α) : t ∈ l → F t = t

If l.map F = l, then F fixes every element of l.

theorem List.find?_zip_map_right {α β : Type} [BEq α] [LawfulBEq α] (f : β → β) (keys : List α) (vals : List β) (x : α) : find? (fun (p : α × β) => p.fst == x) (keys.zip (map f vals)) = Option.map (fun (p : α × β) => (p.fst, f p.snd)) (find? (fun (p : α × β) => p.fst == x) (keys.zip vals))

Looking a key up in zip keys (vals.map f) applies f to the lookup in zip keys vals.

theorem List.Rel₂.exists_of_mem_left {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {l1 : List α} {l2 : List β} (h : Rel₂ R l1 l2) {a : α} (ha : a ∈ l1) : ∃ (b : β), b ∈ l2 ∧ R a b

Every element of the left list of a pointwise relation is related to an element of the right list.

theorem List.Rel₂.map_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : α → β → Prop} {l1 : List α} {l2 : List β} {f : α → γ} {g : β → γ} (hfg : ∀ (a : α) (b : β), R a b → f a = g b) (h : Rel₂ R l1 l2) : map f l1 = map g l2

Pointwise related lists have equal images under two maps that agree on related elements.

theorem List.Rel₂.reverse {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : List α} {b : List β} (h : Rel₂ R a b) : Rel₂ R a.reverse b.reverse

Reversing both lists preserves a pointwise relation.

theorem List.findSome?_pair_rel {α : Type u_1} {β : Type u_2} [BEq α] {R : β → β → Prop} (k : α) {l1 l2 : List (α × β)} (h : Rel₂ (fun (p q : α × β) => p.fst = q.fst ∧ R p.snd q.snd) l1 l2) : findSome? (fun (p : α × β) => if (p.fst == k) = true then some p.snd else none) l1 = none ∧ findSome? (fun (p : α × β) => if (p.fst == k) = true then some p.snd else none) l2 = none ∨ ∃ (d : β), ∃ (r : β), findSome? (fun (p : α × β) => if (p.fst == k) = true then some p.snd else none) l1 = some d ∧ findSome? (fun (p : α × β) => if (p.fst == k) = true then some p.snd else none) l2 = some r ∧ R d r

Searching key-aligned, pointwise-related association lists for a key fails on both or finds related values.

theorem List.findSome?_congr {α β γ : Type} (R : β → γ → Prop) (f : α → Option β) (g : α → Option γ) (l : List α) (hstep : ∀ (a : α), a ∈ l → f a = none ∧ g a = none ∨ ∃ (b : β), ∃ (c : γ), f a = some b ∧ g a = some c ∧ R b c) : findSome? f l = none ∧ findSome? g l = none ∨ ∃ (b : β), ∃ (c : γ), findSome? f l = some b ∧ findSome? g l = some c ∧ R b c

If f and g fail together or give R-related results on each element, so do their findSome? searches.

theorem List.findSome?_prop {α β : Type} (f : α → Option β) (P : β → Prop) (l : List α) (hstep : ∀ (a : α), a ∈ l → ∀ (b : β), f a = some b → P b) (b : β) : findSome? f l = some b → P b

If every result of f satisfies P, so does the result of l.findSome? f.

theorem List.mem_zip_map_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l₁ : List α} {l₂ : List β} (F : β → γ) {a : α} {b : β} (h : (a, b) ∈ l₁.zip l₂) : (a, F b) ∈ l₁.zip (map F l₂)

Mapping F over the right list of a zip maps the right component of each pair.

theorem List.mem_zip_map_self {α : Type u_1} {β : Type u_2} (l : List α) (g : α → β) {a : α} (h : a ∈ l) : (a, g a) ∈ l.zip (map g l)

Each element of a list is paired with its image in the zip of the list with its images.

theorem find?_zip_of_mem {α β : Type} [BEq α] [LawfulBEq α] (as : List α) (bs : List β) (a : α) (b : β) (hmem : (a, b) ∈ as.zip bs) (hnd : as.Nodup) : List.find? (fun (q : α × β) => q.fst == a) (as.zip bs) = some (a, b)

With distinct keys, searching a zip returns the pair stored under a member key.

theorem List.map_fst_zip_sublist {α : Type u_1} {β : Type u_2} (l : List α) (r : List β) : (map Prod.fst (l.zip r)).Sublist l

The key projection of a zip is a sublist of its left input.

theorem List.sublist_flatMap_of_mem {α β : Type} (f : α → List β) (l : List α) (a : α) (ha : a ∈ l) : (f a).Sublist (flatMap f l)

For a ∈ l, f a is a sublist of l.flatMap f.

theorem List.map_mapIdx_ignore_index {α β γ : Type} (l : List α) (g : β → γ) (f : Nat → α → β) : (∀ (i j : Nat) (a : α), g (f i a) = g (f j a)) → map g (mapIdx f l) = map (fun (a : α) => g (f 0 a)) l

map g after mapIdx f is an ordinary map when g (f i a) does not depend on i.

theorem List.foldl_add_start {α : Type} (g : α → Nat) (l : List α) (n : Nat) : foldl (fun (acc : Nat) (a : α) => acc + g a) n l = n + foldl (fun (acc : Nat) (a : α) => acc + g a) 0 l

A fold that adds element weights splits off its initial accumulator.

theorem List.length_filter_ge_of_nodup {α : Type} (xs l : List α) (hxs : xs.Nodup) (p : α → Bool) (hp : ∀ (a : α), p a = true ↔ ¬a ∈ l) : xs.length ≤ (filter p xs).length + l.length

Removing members of l from a duplicate-free list discards at most l.length elements.

theorem List.nodup_map_of_injective {α β : Type} (fn : α → β) (l : List α) (hinj : Function.Injective fn) (h : l.Nodup) : (map fn l).Nodup

An injective map preserves duplicate-freedom.

theorem forall2_exists_left {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {as : List α} {bs : List β} (h : List.Rel₂ R as bs) (b : β) : b ∈ bs → ∃ (a : α), a ∈ as ∧ R a b

Every right-hand member of pointwise-related lists has a related left-hand member.

theorem zip_find?_of_forall₂ {α β γ : Type} [BEq α] {R : β → γ → Prop} (vars : List α) (valsA : List β) (valsB : List γ) (x : α) (hrel : List.Rel₂ R valsA valsB) : List.find? (fun (p : α × β) => p.fst == x) (vars.zip valsA) = none ∧ List.find? (fun (p : α × γ) => p.fst == x) (vars.zip valsB) = none ∨ ∃ (y : α), ∃ (a : β), ∃ (b : γ), List.find? (fun (p : α × β) => p.fst == x) (vars.zip valsA) = some (y, a) ∧ List.find? (fun (p : α × γ) => p.fst == x) (vars.zip valsB) = some (y, b) ∧ R a b

Looking a key up in zips of one key list with position-wise R-related value lists misses in both or finds R-related values.

theorem acc_cons_shift {α : Type u_1} {a : α} {out acc tail : List α} (h : out = (a :: acc).reverse ++ tail) : out = acc.reverse ++ a :: tail

Moving one element into a reversed accumulator exposes it at the front of the suffix.

theorem List.forall₂_filter_zip {α β γ : Type} (R : α → β → Prop) (p : γ → Bool) (a₁ : List α) (a₂ : List β) (hR : Rel₂ R a₁ a₂) (tys : List γ) : Rel₂ (fun (q : α × γ) (r : β × γ) => R q.fst r.fst ∧ q.snd = r.snd) (filter (fun (q : α × γ) => p q.snd) (a₁.zip tys)) (filter (fun (q : β × γ) => p q.snd) (a₂.zip tys))

Zipping position-wise R-related lists with one list tys and filtering by a test on the tys component keeps them related, with equal tys components.

theorem List.forall₂_filterMap {α β α' β' : Type} (R : α → β → Prop) (S : α' → β' → Prop) (f : α → Option α') (g : β → Option β') (hstep : ∀ (a : α) (b : β), R a b → f a = none ∧ g b = none ∨ ∃ (x : α'), ∃ (y : β'), f a = some x ∧ g b = some y ∧ S x y) (l₁ : List α) (l₂ : List β) (hR : Rel₂ R l₁ l₂) : Rel₂ S (filterMap f l₁) (filterMap g l₂)

If on R-related entries f and g both decline or give S-related results, then filterMap takes R-related lists to S-related lists.

theorem List.append_eq_append_cons {α : Type u_1} {a b pre post : List α} {e : α} (h : a ++ b = pre ++ e :: post) : (∃ (post₁ : List α), a = pre ++ e :: post₁ ∧ post = post₁ ++ b) ∨ ∃ (pre₂ : List α), pre = a ++ pre₂ ∧ b = pre₂ ++ e :: post

A position in a concatenation lies in its left part or in its right part.