Erasing duplicates by a comparison

List.eraseDupsBy r l keeps, in order, each entry of l that r relates to no entry kept before it. This file supplies the lemmas that core Lean lacks: the result is a sublist of l (List.eraseDupsBy_sublist), no kept entry is related to an earlier one (List.pairwise_eraseDupsBy), and every entry of l is related to some kept entry or is one (List.exists_mem_eraseDupsBy). The function is also a left fold that appends an entry when no kept entry is related to it (List.eraseDupsBy_eq_foldl), which lets fold rules certify it.

Main results

• List.eraseDupsBy_eq_foldl: eraseDupsBy as a left fold.
• List.eraseDupsBy_sublist, List.pairwise_eraseDupsBy, List.exists_mem_eraseDupsBy.
• List.nodup_map_eraseDupsBy: erasing duplicates by equal labels keeps distinct labels.
• List.nodup_eraseDupsBy_eq, List.mem_eraseDupsBy_eq: erasing duplicates by equality keeps one copy of each entry.

theorem List.eraseDupsBy_eq_foldl {α : Type u_1} {r : α → α → Bool} (l : List α) : eraseDupsBy r l = foldl (fun (kept : List α) (a : α) => if kept.any (r a) = true then kept else kept ++ [a]) [] l

eraseDupsBy appends each entry that is related to no entry kept so far.

theorem List.eraseDupsBy_sublist {α : Type u_1} {r : α → α → Bool} (l : List α) : (eraseDupsBy r l).Sublist l

eraseDupsBy keeps a sublist.

theorem List.pairwise_eraseDupsBy {α : Type u_1} {r : α → α → Bool} (l : List α) : Pairwise (fun (a b : α) => r b a = false) (eraseDupsBy r l)

No entry kept by eraseDupsBy is related to an earlier kept entry.

theorem List.exists_mem_eraseDupsBy {α : Type u_1} {r : α → α → Bool} {l : List α} {a : α} : a ∈ l → ∃ (b : α), b ∈ eraseDupsBy r l ∧ (a = b ∨ r a b = true)

Every entry of l is kept by eraseDupsBy, or related to a kept entry.

theorem List.nodup_map_eraseDupsBy {α : Type u_1} {κ : Type u_2} [DecidableEq κ] (f : α → κ) (l : List α) : (map f (eraseDupsBy (fun (a b : α) => decide (f a = f b)) l)).Nodup

Erasing duplicates by equal labels keeps entries with distinct labels.

theorem List.nodup_eraseDupsBy_eq {α : Type u_1} [DecidableEq α] (l : List α) : (eraseDupsBy (fun (a b : α) => decide (a = b)) l).Nodup

Erasing duplicates by equality leaves no duplicates.

theorem List.mem_eraseDupsBy_eq {α : Type u_1} [DecidableEq α] {l : List α} {a : α} : a ∈ eraseDupsBy (fun (a b : α) => decide (a = b)) l ↔ a ∈ l

Erasing duplicates by equality keeps every entry.