how to make `grind` tactic aware of type class instances?

Stream: general

[Syed Shaazib Tanvir]

I have the following code

class SetTheory where
  Set : Type u
  Object : Type v
  mem : Object → Set → Prop
  extensionality (x : Set) (y : Set) : (∀ z : Object, mem z x ↔ mem z y) → x = y
  empty : Set
  empty_set_axiom : ∀ x : Object, ¬mem x empty
  singleton (x : Object) : Set
  singleton_axiom (x : Object) : ∀ y : Object, mem y (singleton x) ↔ y = x
  pair_axiom (x : Object) (y : Object) : ∃ z : Set, ∀ w : Object, mem w z ↔ (w = x ∨ w = y)
  pairwise_union (x : Set) (y : Set) : Set
  pairwise_union_axiom (x : Set) (y : Set) (z : Object)
    : mem z (pairwise_union x y) ↔ (mem z x ∨ mem z y)

export SetTheory (Set Object)
variable [SetTheory]

@[grind]
instance SetTheory.instMembership : Membership Object Set where
  mem x y := mem y x

@[grind]
instance SetTheory.instUnion : Union Set where
  union x y := pairwise_union x y

theorem SetTheory.union_comm (x y : Set) : x ∪ y = y ∪ x := by
  change pairwise_union x y = pairwise_union y x
  apply extensionality
  intro z
  constructor
  · grind only [pairwise_union_axiom]
  · grind only [pairwise_union_axiom]

Removing the change pairwise_union x y = pairwise_union y x causes the grind tactic to fail even though the relevant type class instances have the @[grind] attribute. How can I fix this?

[Miyahara Kō]

Generally speaking, grind attributes for instances essentially do nothing.
You should remove grind attributes from instances and make new grind lemmas, and change grind only into grind.

[Marcus Rossel]

@Miyahara Kō what kind of grind lemmas should be implemented? I've had similar situations where I was expecting grind to just understand what a given notation (implemented on type classes) unfolds to, and ended up adding explicit lemmas just for unfolding the notation. But that felt a bit strange as other tactics like simp don't require such lemmas.

[Théophile]

This issue I opened the last month is probably relevant: lean4#11708

The corresponding MWE is:

class Test (α: Type) where
  pred: α → Prop

instance: Test Unit where
  pred _ := True

example: Test.pred () := by
  fail_if_success grind [Test.pred]
  grind [Test.pred, instTestUnit]

[Miyahara Kō]

@Marcus Rossel

class SetTheory where
  Set : Type u
  Object : Type v
  mem : Object → Set → Prop
  extensionality (x : Set) (y : Set) : (∀ z : Object, mem z x ↔ mem z y) → x = y
  empty : Set
  empty_set_axiom : ∀ x : Object, ¬mem x empty
  singleton (x : Object) : Set
  singleton_axiom (x : Object) : ∀ y : Object, mem y (singleton x) ↔ y = x
  pair_axiom (x : Object) (y : Object) : ∃ z : Set, ∀ w : Object, mem w z ↔ (w = x ∨ w = y)
  pairwise_union (x : Set) (y : Set) : Set
  pairwise_union_axiom (x : Set) (y : Set) (z : Object)
    : mem z (pairwise_union x y) ↔ (mem z x ∨ mem z y)

export SetTheory (Set Object)
variable [SetTheory]

instance SetTheory.instMembership : Membership Object Set where
  mem x y := mem y x

@[grind =]
theorem SetTheory.mem_def {x : Object} {y : Set} : x ∈ y ↔ SetTheory.mem x y :=
  Iff.rfl

instance SetTheory.instUnion : Union Set where
  union x y := pairwise_union x y

@[grind =]
theorem SetTheory.union_def (x y : Set) : x ∪ y = pairwise_union x y :=
  rfl

theorem SetTheory.union_comm (x y : Set) : x ∪ y = y ∪ x := by
  apply extensionality
  intro z
  constructor
  · grind [pairwise_union_axiom]
  · grind [pairwise_union_axiom]

[Miyahara Kō]

My refactored version

class SetTheory (Object : outParam (Type u)) (Set : Type v) extends
    Membership Object Set, EmptyCollection Set, Singleton Object Set, Union Set where
  ext {x y : Set} : (∀ z : Object, z ∈ x ↔ z ∈ y) → x = y
  notMem_empty : ∀ x, x ∉ (∅ : Set)
  mem_singleton {x y : Object} : y ∈ ({x} : Set) ↔ y = x
  exists_pair (x y : Object) : ∃ z : Set, ∀ w : Object, w ∈ z ↔ (w = x ∨ w = y)
  mem_union {x y : Set} {z : Object} : z ∈ x ∪ y ↔ z ∈ x ∨ z ∈ y

namespace SetTheory

variable {Object : Type u} {Set : Type v} [SetTheory Object Set]

attribute [ext, grind ext] ext

attribute [grind .] notMem_empty

attribute [grind =] mem_singleton mem_union

theorem union_comm (x y : Set) : x ∪ y = y ∪ x := by
  grind

end SetTheory