Erasure of duplicates in a list

This file proves basic results about List.dedup (definition in Data.List.Defs). dedup l returns l without its duplicates. It keeps the earliest (that is, rightmost) occurrence of each.

Tags

duplicate, multiplicity, nodup, nub

@[simp]

theorem List.dedup_nil {α : Type u_1} [DecidableEq α] : [].dedup = []

theorem List.dedup_cons_of_mem' {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : a ∈ l.dedup) : (a :: l).dedup = l.dedup

theorem List.dedup_cons_of_notMem' {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : ¬a ∈ l.dedup) : (a :: l).dedup = a :: l.dedup

theorem List.dedup_cons' {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : (a :: l).dedup = if a ∈ l.dedup then l.dedup else a :: l.dedup

@[simp]

theorem List.mem_dedup {α : Type u_1} [DecidableEq α] {a : α} {l : List α} : a ∈ l.dedup ↔ a ∈ l

@[simp]

theorem List.dedup_cons_of_mem {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : a ∈ l) : (a :: l).dedup = l.dedup

@[simp]

theorem List.dedup_cons_of_notMem {α : Type u_1} [DecidableEq α] {a : α} {l : List α} (h : ¬a ∈ l) : (a :: l).dedup = a :: l.dedup

theorem List.dedup_cons {α : Type u_1} [DecidableEq α] (a : α) (l : List α) : (a :: l).dedup = if a ∈ l then l.dedup else a :: l.dedup

theorem List.dedup_sublist {α : Type u_1} [DecidableEq α] (l : List α) : l.dedup.Sublist l

theorem List.dedup_subset {α : Type u_1} [DecidableEq α] (l : List α) : l.dedup ⊆ l

theorem List.subset_dedup {α : Type u_1} [DecidableEq α] (l : List α) : l ⊆ l.dedup

theorem List.nodup_dedup {α : Type u_1} [DecidableEq α] (l : List α) : l.dedup.Nodup

theorem List.headI_dedup {α : Type u_1} [DecidableEq α] [Inhabited α] (l : List α) : l.dedup.headI = if l.headI ∈ l.tail then l.tail.dedup.headI else l.headI

theorem List.tail_dedup {α : Type u_1} [DecidableEq α] [Inhabited α] (l : List α) : l.dedup.tail = if l.headI ∈ l.tail then l.tail.dedup.tail else l.tail.dedup

theorem List.dedup_eq_self {α : Type u_1} [DecidableEq α] {l : List α} : l.dedup = l ↔ l.Nodup

theorem List.nodup_iff_sublist_dedup {α : Type u_1} [DecidableEq α] {l : List α} : l.Nodup ↔ l.Sublist l.dedup

theorem List.nodup_iff_length_dedup_eq {α : Type u_1} [DecidableEq α] {l : List α} : l.Nodup ↔ l.dedup.length = l.length

theorem List.nodup_iff_le_length_dedup {α : Type u_1} [DecidableEq α] {l : List α} : l.Nodup ↔ l.length ≤ l.dedup.length

theorem List.dedup_eq_cons {α : Type u_1} [DecidableEq α] (l : List α) (a : α) (l' : List α) : l.dedup = a :: l' ↔ a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'

@[simp]

theorem List.dedup_eq_nil {α : Type u_1} [DecidableEq α] (l : List α) : l.dedup = [] ↔ l = []

theorem List.Nodup.dedup {α : Type u_1} [DecidableEq α] {l : List α} (h : l.Nodup) : l.dedup = l

@[simp]

theorem List.dedup_idem {α : Type u_1} [DecidableEq α] {l : List α} : l.dedup.dedup = l.dedup

theorem List.dedup_append {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup

theorem List.dedup_map_of_injective {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α → β} (hf : Function.Injective f) (xs : List α) : (map f xs).dedup = map f xs.dedup

theorem List.Subset.dedup_append_right {α : Type u_1} [DecidableEq α] {xs ys : List α} (h : xs ⊆ ys) : (xs ++ ys).dedup = ys.dedup

Note that the weaker List.Subset.dedup_append_left is proved later.

theorem List.Disjoint.union_eq {α : Type u_1} [DecidableEq α] {xs ys : List α} (h : xs.Disjoint ys) : xs ∪ ys = xs.dedup ++ ys

theorem List.Disjoint.dedup_append {α : Type u_1} [DecidableEq α] {xs ys : List α} (h : xs.Disjoint ys) : (xs ++ ys).dedup = xs.dedup ++ ys.dedup

theorem List.replicate_dedup {α : Type u_1} [DecidableEq α] {x : α} {k : ℕ} : k ≠ 0 → (replicate k x).dedup = [x]

theorem List.count_dedup {α : Type u_1} [DecidableEq α] (l : List α) (a : α) : count a l.dedup = if a ∈ l then 1 else 0

theorem List.Perm.dedup {α : Type u_1} [DecidableEq α] {l₁ l₂ : List α} (p : l₁.Perm l₂) : l₁.dedup.Perm l₂.dedup