Add @[grind] to Quotient.eq

Stream: mathlib4

[Jakub Nowak]

Shouldn't we add @[grind] to Quot.eq so that grind can derive r x y from Quot.mk r x = Quot.mk r y?

I've been hit by that while working on Sym2:

import Mathlib

theorem eq_iff {x y z w : α} : s(x, y) = s(z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z := by
  grind [cases Sym2.Rel]

I can make PR, but wanted to ask first, cause I'm not experienced with grind yet.

[Jakub Nowak]

Ah, wait, it's not the simple Quot.eq is mk r x = mk r y ↔ Relation.EqvGen r x y, not mk r x = mk r y ↔ r x y.
We should add @[grind] to Quotient.eq, not Quot.eq. It won't solve my problem with Sym2 though, I wonder why Sym2 is defined in terms of Quot and not Quotient when the setoid instance is like 10 lines above in the code.

[Kim Morrison]

docs#Quotient.eq

[Kim Morrison]

No, one should never annotate lemmas of the form (x = y) ↔ P x y for grind. If you are tempted, make sure to use @[grind?], and see the (bad!) patterns that grind attempts to use.

A general piece of advice is that if you are trying to annotate an equality or iff for grind, with the expectation that it will rewrite the LHS into the RHS, you should always use @[grind =] (which requires that the entire LHS is the pattern) rather than @[grind] (which is free to choose other patterns). @[grind =] will (helpfully) not be allowed on Quotient.eq.

[Robin Arnez]

I guess you'd need something like a SolverExtension?

[Robin Arnez]

Very helpfully not allowed :-)

import Mathlib

/-- info: Quotient.eq: [@Quotient.mk #3 #2 #1, @Quotient.mk _ #2 #0] -/
#guard_msgs in
attribute [grind? =] Quotient.eq

[Jakub Nowak]

Yeah, I've also already noticed that grind = generates better pattern then grind. Although, the pattern generated by grind would still work, it's just less efficient I think? Not sure.

I think adding Quotient.eq to grind wouldn't help much anyway. Because grind isn't be able to rewrite Rel.setoid α p q to Rel α p q. See #lean4 > grind cannot see past CoeFun.