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

@[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_map_injOn {α β : Type} [DecidableEq β] {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.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.

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).