feat: grind attributes for relation typeclasses

src/Init/Core.lean

@@ -2420,6 +2420,10 @@ theorem lt_of_lt_of_eq {a b c : α} [LT α] (h₁ : a < b) (h₂ : b = c) : a <
 namespace Std
 variable {α : Sort u}
 
+-- Note: the classes carrying properties are all marked `attribute [grind cases]` in `Init.Grind.Cases`,
+-- so these facts are available to `grind`.
+-- If `grind` later gains native handling of any of these, those attributes can be removed.
+
 /--
 `Associative op` indicates `op` is an associative operation,
 i.e. `(a ∘ b) ∘ c = a ∘ (b ∘ c)`.

src/Init/Grind/Cases.lean

@@ -11,3 +11,7 @@ import Init.Grind.Tactics
 
 attribute [grind cases eager] And Prod False Empty True PUnit Exists Subtype
 attribute [grind cases] Or
+
+attribute [grind cases] Std.Associative Std.Commutative Std.IdempotentOp
+  Std.LawfulLeftIdentity Std.LawfulRightIdentity Std.LawfulIdentity Std.LawfulCommIdentity
+  Std.Refl Std.Antisymm Std.Asymm Std.Total Std.Irrefl

tests/lean/run/grind_relation_typeclasses.lean

@@ -0,0 +1,54 @@
+set_option grind.warning false
+
+example [Mul α] [Std.Commutative (α := α) (· * ·)] {a b : α} : a * b = b * a := by
+  grind
+
+example [Mul α] [Std.Associative (α := α) (· * ·)] {a b : α} : a * b * c = a * (b * c) := by
+  grind
+
+example [Mul α] [Std.Commutative (α := α) (· * ·)] [Std.Associative (α := α) (· * ·)] {a b c : α} :
+    a * b * c = b * (a * c) := by
+  grind
+
+example [Mul α] [Std.IdempotentOp (α := α) (· * ·)] {a : α} : a * a = a := by
+  grind
+
+example [Mul α] [Std.IdempotentOp (α := α) (· * ·)] [Std.Commutative (α := α) (· * ·)]
+    [Std.Associative (α := α) (· * ·)] {a : α} :
+    a * b * a = a * b := by
+  grind
+
+example [Mul α] (a b : α) [Std.LawfulLeftIdentity (α := α) (· * ·) (a : α)] : a * b = b := by
+  grind
+
+example [Mul α] (a b : α) [Std.LawfulRightIdentity (α := α) (· * ·) (a : α)] : b * a = b := by
+  grind
+
+example [Mul α] (a b : α) [Std.LawfulRightIdentity (α := α) (· * ·) (a : α)] : b * a * a = b := by
+  grind
+
+example [Mul α] (a b : α) [Std.LawfulIdentity (α := α) (· * ·) (a : α)]
+    [Std.Associative (α := α) (· * ·)] : a * b * a = b := by
+  grind
+
+example [Mul α] (a b : α) [Std.Commutative (α := α) (· * ·)] [Std.LawfulCommIdentity (α := α) (· * ·) (a : α)]
+    [Std.Associative (α := α) (· * ·)] : a * b * a = b := by
+  grind
+
+example {r : α → α → Prop} [Std.Refl r] {a : α} : r a a := by grind
+
+example [Mul α] {r : α → α → Prop} [Std.Commutative (α := α) (· * ·)] [Std.Refl r] :
+    r (a * b) (b * a) := by grind
+
+example {r : α → α → Prop} [Std.Antisymm r] {a b : α} : r a b → r b a → a = b := by grind
+example {r : α → α → Prop} [Std.Asymm r] {a b : α} : r a b → r b a → False := by grind
+example {r : α → α → Prop} [Std.Asymm r] {a b : α} : r a b → ¬ r b a := by grind
+example {r : α → α → Prop} [Std.Asymm r] : Std.Antisymm r := by grind [Std.Antisymm] -- We haven't put `@[grind]` on `Std.Antisymm.mk`.
+example {r : α → α → Prop} [Std.Total r] {a b : α} : ¬ r a b → r b a := by grind
+example {r : α → α → Prop} [Std.Irrefl r] {a : α} : ¬ r a a := by grind
+example [Mul α] {r : α → α → Prop} [Std.Commutative (α := α) (· * ·)] [Std.Irrefl r] :
+    ¬ r (a * b) (b * a) := by
+  grind
+example [Mul α] {r : α → α → Prop} [Std.Commutative (α := α) (· * ·)] [Std.Total r]
+    (h : ¬ r (a * b) (b * a)) : False := by
+  grind