chore: cleanup of grind tests

src/Init/Data/List/Basic.lean

@@ -673,7 +673,7 @@ instance : Std.Associative (α := List α) (· ++ ·) := ⟨append_assoc⟩
 theorem append_cons (as : List α) (b : α) (bs : List α) : as ++ b :: bs = as ++ [b] ++ bs := by
   simp
 
-@[simp] theorem concat_eq_append {as : List α} {a : α} : as.concat a = as ++ [a] := by
+@[simp, grind =] theorem concat_eq_append {as : List α} {a : α} : as.concat a = as ++ [a] := by
   induction as <;> simp [concat, *]
 
 theorem reverseAux_eq_append {as bs : List α} : reverseAux as bs = reverseAux as [] ++ bs := by

src/Std/Data/ExtDHashMap/Lemmas.lean

@@ -51,15 +51,10 @@ theorem not_insert_eq_empty [EquivBEq α] [LawfulHashable α] {k : α} {v : β k
 theorem mem_iff_contains [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m ↔ m.contains a :=
   Iff.rfl
 
-@[simp, grind =]
+@[simp, grind _=_]
 theorem contains_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a ↔ a ∈ m :=
   Iff.rfl
 
--- We need to specify the pattern for the reverse direction manually,
--- as the default heuristic leaves the `ExtDHashMap α β` argument as a wildcard.
-grind_pattern contains_iff_mem => @Membership.mem α (ExtDHashMap α β) _ m a
-
-
 theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : m.contains a = m.contains b :=
   m.inductionOn fun _ => DHashMap.contains_congr hab
 

tests/lean/grind/algebra/ordered_modules.lean

@@ -23,40 +23,15 @@ example (a b c : R) (_ : a < b) (_ : b < c) : a < c := by grind
 example (a : R) (h : 2 * a < 0) : a < 0 := by grind
 example (a : R) (h : 2 * a < 0) : 0 ≤ -a := by grind
 
-example (a b : R) (_ : a < b) (_ : b < a) : False := by grind
-example (a b : R) (_ : a < b ∧ b < a) : False := by grind
-example (a b : R) (_ : a < b) : a ≠ b := by grind
-
 example (a b c e v0 v1 : R) (h1 : v0 = 5 * a) (h2 : v1 = 3 * b) (h3 : v0 + v1 + c = 10 * e) :
     v0 + 5 * e + (v1 - 3 * e) + (c - 2 * e) = 10 * e := by
   grind
 
-example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) : False := by
-  grind
-example (x y z : R) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) : False := by
-  grind
-
-example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : x * y < 5) (h3 : 12 * y - 4 * z < 0) :
-    False := by grind
-example (x y z : R) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : 12 * y - 4 * z < 0) :
-    False := by grind
-
-example (x y z : Int) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3*y := by
-  grind
 example (x y z : R) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
   grind
 
-example (x y z : Int) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) (h3 : x * y < 5) : ¬ 12*y - 4* z < 0 := by
-  grind
-example (x y z : R) (h1 : 2 * x < 3 * y) (h2 : -4 * x + 2 * z < 0) : ¬ 12 * y - 4 * z < 0 := by
-  grind
-
-example (x y z : Int) (hx : ¬ x > 3 * y) (h2 : ¬ y > 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
-  grind
 example (x y z : R) (hx : ¬ x > 3 * y) (h2 : ¬ y > 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
   grind
 
-example (x y z : Nat) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
-  grind
 example (x y z : R) (hx : x ≤ 3 * y) (h2 : y ≤ 2 * z) (h3 : x ≥ 6 * z) : x = 3 * y := by
   grind

tests/lean/grind/dhashmap_pattern.lean

@@ -1,43 +0,0 @@
-import Std.Data.HashMap
-import Std.Data.TreeMap
-
-open Std
-
-/--
-info: Std.DTreeMap.contains_iff_mem.{u, v} {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp}
-  {k : α} : t.contains k = true ↔ k ∈ t
--/
-#guard_msgs in
-#check DTreeMap.contains_iff_mem
-
--- I like what `[grind _=_]` does here!
-/--
-info: DTreeMap.contains_iff_mem: [@DTreeMap.contains #4 #3 #2 #1 #0, true]
----
-info: DTreeMap.contains_iff_mem: [@Membership.mem #4 (@DTreeMap _ #3 #2) _ #1 #0]
--/
-#guard_msgs in
-attribute [grind? _=_] DTreeMap.contains_iff_mem
-
--- Similarly for every other `contains_iff_mem` we encounter (`List`, `Array`, `Vector`, `HashSet`, `HashMap`, etc.)
-
--- But:
-
-/--
-info: Std.DHashMap.contains_iff_mem.{u, v} {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : DHashMap α β}
-  {a : α} : m.contains a = true ↔ a ∈ m
--/
-#guard_msgs in
-#check DHashMap.contains_iff_mem
-
--- Here the reverse direction of `[grind _=_]` gives a pattern than matches too often: `@Membership.mem #5 _ _ #1 #0`.
-/--
-info: DHashMap.contains_iff_mem: [@DHashMap.contains #5 #4 #3 #2 #1 #0, true]
----
-info: DHashMap.contains_iff_mem: [@Membership.mem #5 _ _ #1 #0]
--/
-#guard_msgs in
-attribute [grind? _=_] DHashMap.contains_iff_mem
-
--- We can do this manually with
-grind_pattern DHashMap.contains_iff_mem => @Membership.mem α (DHashMap α β) _ m a

tests/lean/grind/experiments/list_count.lean

@@ -2,18 +2,8 @@
 
 open List
 
-
 variable [BEq α] [LawfulBEq α]
 
-theorem filter_beq {l : List α} (a : α) : l.filter (· == a) = replicate (count a l) a := by
-  ext
-  grind
-
-theorem count_flatten {a : α} {l : List (List α)} : count a l.flatten = (l.map (count a)).sum := by
-  grind (ematch := 10) (gen := 10) -- fails
-
-theorem count_concat_self {a : α} {l : List α} : count a (concat l a) = count a l + 1 := by grind [concat_eq_append] -- fails?!
-
 theorem count_eq_length {l : List α} : count a l = l.length ↔ ∀ b ∈ l, a = b := by
   induction l with grind
 
@@ -27,7 +17,3 @@ theorem replicate_count_eq_of_count_eq_length {l : List α} (h : count a l = len
 theorem count_filterMap {α} [BEq β] {b : β} {f : α → Option β} {l : List α} :
     count b (filterMap f l) = countP (fun a => f a == some b) l := by
   grind
-
-theorem count_flatMap {α} [BEq β] {l : List α} {f : α → List β} {x : β} :
-    count x (l.flatMap f) = sum (map (count x ∘ f) l) := by
-  grind

tests/lean/grind/experiments/map.lean

@@ -4,7 +4,8 @@ import Std.Data.ExtHashMap
 open Std
 
 -- Do we want this?
-example (m : HashMap Nat Nat) (h : m.isEmpty) : m[3]? = none := by grind [HashMap.getElem?_of_isEmpty]
+grind_pattern HashMap.getElem?_of_isEmpty => m.isEmpty, m[a]?
+example (m : HashMap Nat Nat) (h : m.isEmpty) : m[3]? = none := by grind
 
 -- Do this for List etc?
 -- attribute [grind] HashMap.getElem?_eq_some_getElem -- Do we do this for list?

tests/lean/run/grind_list_count.lean

@@ -210,4 +210,13 @@ theorem filter_beq {l : List α} (a : α) : l.filter (· == a) = replicate (coun
   ext
   grind
 
+theorem count_flatten {α} [BEq α] {a : α} {l : List (List α)} : count a l.flatten = (l.map (count a)).sum := by
+  grind
+
+theorem count_concat_self {a : α} {l : List α} : count a (concat l a) = count a l + 1 := by grind
+
+theorem count_flatMap {α} [BEq β] {l : List α} {f : α → List β} {x : β} :
+    count x (l.flatMap f) = sum (map (count x ∘ f) l) := by
+  grind
+
 end count