chore: add grind test for fastEraseDups (#8310)

This PR adds @TwoFX's `List.fastEraseDups` example, with the proof
golfed further using `grind`, as a test case for `grind`.

src/Init/Data/BEq.lean

@@ -27,7 +27,7 @@ class EquivBEq (α) [BEq α] : Prop extends PartialEquivBEq α, ReflBEq α
 theorem BEq.symm [BEq α] [PartialEquivBEq α] {a b : α} : a == b → b == a :=
   PartialEquivBEq.symm
 
-theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
+@[grind] theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
   Bool.eq_iff_iff.2 ⟨BEq.symm, BEq.symm⟩
 
 theorem bne_comm [BEq α] [PartialEquivBEq α] {a b : α} : (a != b) = (b != a) := by

src/Init/Data/List/Lemmas.lean

@@ -599,7 +599,7 @@ theorem decide_forall_mem {l : List α} {p : α → Prop} [DecidablePred p] :
 @[simp] theorem all_eq_false {l : List α} : l.all p = false ↔ ∃ x, x ∈ l ∧ ¬p x := by
   simp [all_eq]
 
-theorem any_beq [BEq α] {l : List α} {a : α} : (l.any fun x => a == x) = l.contains a := by
+@[grind] theorem any_beq [BEq α] {l : List α} {a : α} : (l.any fun x => a == x) = l.contains a := by
   induction l <;> simp_all [contains_cons]
 
 /-- Variant of `any_beq` with `==` reversed. -/
@@ -607,7 +607,7 @@ theorem any_beq' [BEq α] [PartialEquivBEq α] {l : List α} :
     (l.any fun x => x == a) = l.contains a := by
   simp only [BEq.comm, any_beq]
 
-theorem all_bne [BEq α] {l : List α} : (l.all fun x => a != x) = !l.contains a := by
+@[grind] theorem all_bne [BEq α] {l : List α} : (l.all fun x => a != x) = !l.contains a := by
   induction l <;> simp_all [bne]
 
 /-- Variant of `all_bne` with `!=` reversed. -/

tests/lean/run/grind_fastEraseDups.lean

@@ -0,0 +1,29 @@
+
+import Std.Data.HashSet
+
+open Std
+
+set_option grind.warning false
+
+namespace List
+
+-- Fast duplicate-removing function, using a hash set to check if an element was seen before
+def fastEraseDups [BEq α] [Hashable α] (l : List α) : List α :=
+  go l [] ∅
+where
+  go : List α → List α → Std.HashSet α → List α
+  | [], seenl, _ => seenl.reverse
+  | (x::l), seenl, seen => if x ∈ seen then go l seenl seen else go l (x::seenl) (seen.insert x)
+
+-- Easy to verify using available hash set lemmas
+theorem eraseDups_eq_fastEraseDups [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
+    (l : List α) : l.eraseDups = l.fastEraseDups :=
+  loop_eq_go _ _ _ (by simp)
+where
+  loop_eq_go (l seenl : List α) (seen : Std.HashSet α) (hs : ∀ x, seenl.contains x ↔ x ∈ seen) :
+      eraseDupsBy.loop (· == ·) l seenl = fastEraseDups.go l seenl seen := by
+    induction l generalizing seenl seen with
+    | nil => grind [eraseDupsBy.loop, fastEraseDups.go]
+    | cons x => cases h : seenl.contains x <;> grind [eraseDupsBy.loop, fastEraseDups.go]
+
+end List