feat: add List.eraseDupsBy and basic lemmas

src/Init/Data/List/Basic.lean

@@ -2249,6 +2249,26 @@ Examples:
 def intercalate (sep : List α) (xs : List (List α)) : List α :=
   (intersperse sep xs).flatten
 
+/-! ### eraseDupsBy -/
+
+/--
+Erases duplicated elements in the list, using a given comparison function,
+keeping the first occurrence of duplicated elements.
+
+`O(|l|^2)`.
+
+Examples:
+ * `[1, 3, 4, 2, 1, 5].eraseDupsBy (· % 3 == · % 3) = [1, 3, 2]`
+-/
+def eraseDupsBy {α} (r : α → α → Bool) (as : List α) : List α :=
+  loop as []
+where
+  loop : List α → List α → List α
+  | [],    bs => bs.reverse
+  | a::as, bs => match bs.any (r a) with
+    | true  => loop as bs
+    | false => loop as (a::bs)
+
 /-! ### eraseDups -/
 
 /--
@@ -2260,14 +2280,28 @@ Examples:
  * `[1, 3, 2, 2, 3, 5].eraseDups = [1, 3, 2, 5]`
  * `["red", "green", "green", "blue"].eraseDups = ["red", "green", "blue"]`
 -/
-def eraseDups {α} [BEq α] (as : List α) : List α :=
-  loop as []
+def eraseDups {α} [BEq α] (as : List α) : List α := eraseDupsBy (· == ·) as
+
+/-! ### eraseRepsBy -/
+
+/--
+Erases repeated elements, using a given comparison function,
+keeping the first element of each run.
+
+`O(|l|)`.
+
+Example:
+* `[1, 3, 2, 2, 2, 3, 3, 7].eraseRepsBy (· % 4 == · % 5) = [1, 3, 2, 3]`
+-/
+def eraseRepsBy {α} (r : α → α → Bool) : List α → List α
+  | []    => []
+  | a::as => loop a as []
 where
-  loop : List α → List α → List α
-  | [],    bs => bs.reverse
-  | a::as, bs => match bs.elem a with
-    | true  => loop as bs
-    | false => loop as (a::bs)
+  loop : α → List α → List α → List α
+  | a, [], acc => (a::acc).reverse
+  | a, a'::as, acc => match r a a' with
+    | true  => loop a as acc
+    | false => loop a' as (a::acc)
 
 /-! ### eraseReps -/
 
@@ -2279,15 +2313,7 @@ Erases repeated elements, keeping the first element of each run.
 Example:
 * `[1, 3, 2, 2, 2, 3, 3, 5].eraseReps = [1, 3, 2, 3, 5]`
 -/
-def eraseReps {α} [BEq α] : List α → List α
-  | []    => []
-  | a::as => loop a as []
-where
-  loop {α} [BEq α] : α → List α → List α → List α
-  | a, [], acc => (a::acc).reverse
-  | a, a'::as, acc => match a == a' with
-    | true  => loop a as acc
-    | false => loop a' as (a::acc)
+def eraseReps {α} [BEq α] (as : List α) : List α := eraseRepsBy (· == ·) as
 
 /-! ### span -/
 
@@ -2359,6 +2385,8 @@ Examples:
 def removeAll [BEq α] (xs ys : List α) : List α :=
   xs.filter (fun x => !ys.elem x)
 
+@[simp] theorem nil_removeAll [BEq α] {ys : List α} : [].removeAll ys = [] := rfl
+
 /-!
 # Runtime re-implementations using `@[csimp]`
 

src/Init/Data/List/Lemmas.lean

@@ -3457,6 +3457,81 @@ theorem all_eq_not_any_not {l : List α} {p : α → Bool} : l.all p = !l.any (!
     (l.insert a).all f = (f a && l.all f) := by
   simp [all_eq]
 
+/-! ### `removeAll` -/
+
+@[simp] theorem removeAll_nil [BEq α] {xs : List α} : xs.removeAll [] = xs := by
+  simp [removeAll]
+
+theorem cons_removeAll [BEq α] {x : α} {xs ys : List α} :
+    (x :: xs).removeAll ys =
+      if ys.contains x = false then
+        x :: xs.removeAll ys
+      else
+        xs.removeAll ys := by
+  simp [removeAll, filter_cons]
+
+theorem removeAll_cons [BEq α] {xs : List α} {y : α} {ys : List α} :
+    xs.removeAll (y :: ys) = (xs.filter fun x => !x == y).removeAll ys := by
+  simp [removeAll, Bool.and_comm]
+
+@[simp] theorem filter_removeAll_filter [BEq α] [LawfulBEq α] {p : α → Bool} {xs ys : List α} :
+    (xs.filter p).removeAll (ys.filter p) = (xs.filter p).removeAll ys := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [filter_cons]
+    split
+    · simp [cons_removeAll]
+      split
+      · rw [if_neg] <;> simp_all
+      · rw [if_pos] <;> simp_all
+    · simp [ih]
+
+/-! ### `eraseDupsBy` and `eraseDups` -/
+
+@[simp] theorem eraseDupsBy_nil : ([] : List α).eraseDupsBy r = [] := rfl
+
+private theorem eraseDupsBy_loop_cons {as bs : List α} {r : α → α → Bool} :
+    eraseDupsBy.loop r as bs = bs.reverse ++ eraseDupsBy.loop r (as.filter fun a => !bs.any (r a)) [] := by
+  match as with
+  | nil => simp [eraseDupsBy.loop]
+  | cons a as =>
+    conv => lhs; unfold eraseDupsBy.loop
+    simp only [filter_cons]
+    split <;> rename_i h
+    · simp only [h, Bool.not_true, Bool.false_eq_true, ↓reduceIte]
+      rw [eraseDupsBy_loop_cons]
+    · simp only [h, Bool.not_false, ↓reduceIte]
+      rw [eraseDupsBy_loop_cons, eraseDupsBy.loop]
+      have : (filter (fun a => !bs.any (r a)) as).length < as.length + 1 :=
+        lt_add_one_of_le (List.length_filter_le _ as)
+      rw [eraseDupsBy_loop_cons (bs := [a])]
+      simp
+termination_by as.length
+
+theorem eraseDupsBy_cons :
+    (a :: as).eraseDupsBy r = a :: (as.filter fun b => r b a = false).eraseDupsBy r := by
+  simp only [eraseDupsBy, eraseDupsBy.loop, any_nil]
+  rw [eraseDupsBy_loop_cons]
+  simp
+
+@[simp] theorem eraseDups_nil [BEq α] : ([] : List α).eraseDups = [] := rfl
+theorem eraseDups_cons [BEq α] {a : α} {as : List α} :
+    (a :: as).eraseDups = a :: (as.filter fun b => !b == a).eraseDups := by
+  simp [eraseDups, eraseDupsBy_cons]
+
+theorem eraseDups_append [BEq α] [LawfulBEq α] {as bs : List α} :
+    (as ++ bs).eraseDups = as.eraseDups ++ (bs.removeAll as).eraseDups := by
+  match as with
+  | nil => simp
+  | cons a as =>
+    simp only [cons_append, eraseDups_cons, filter_append, cons.injEq, true_and]
+    have : (filter (fun b => !b == a) as).length < as.length + 1 :=
+      lt_add_one_of_le (List.length_filter_le _ as)
+    rw [eraseDups_append]
+    simp [removeAll_cons]
+termination_by as.length
+
 /-! ### Legacy lemmas about `get`, `get?`, and `get!`.
 
 Hopefully these should not be needed, in favour of lemmas about `xs[i]`, `xs[i]?`, and `xs[i]!`,