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} [DecidableEq α] : List.dedup [] = []

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

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

@[simp]

theorem List.dedup_idem {α : Type u} [DecidableEq α] {l : List α} : List.dedup (List.dedup l) = List.dedup l

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

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

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

theorem List.sum_map_count_dedup_filter_eq_countP {α : Type u} [DecidableEq α] (p : α → Bool) (l : List α) : List.sum (List.map (fun x => List.count x l) (List.filter p (List.dedup l))) = List.countP p l

Summing the count of x over a list filtered by some p is just countP applied to p

theorem List.sum_map_count_dedup_eq_length {α : Type u} [DecidableEq α] (l : List α) : List.sum (List.map (fun x => List.count x l) (List.dedup l)) = List.length l