How to use Grind.ToInt with a new type

Stream: lean4

[Chris Bailey]

Some people in the area are working through the Lean companion to Tao's analysis book, and chapter 4 entails construction of Int as a quotient over pairs of Nat.

I was curious whether some basic proofs (here addAssoc and addComm) could be completed by leaning on Grind.ToInt and the other related type classes (let's set aside that this sort of side steps the educational value). I'm curious why this strategy seems to work if I manually invoke the relevant lemmas (like ToInt.toInt_inj and ToInt.Add.toInt_add), but does not "just work" with a single grind call, since it does seem to work with just a call to grind for types like Fin. The debug trace when invoked against Fin does show a "found" instance of ToInt.toInt, while the debug trace for QInt does not.

There's a lot of noise/setup in this file, but the relevant proofs (and failures) are at the bottom: playground link

Am I doing something wrong in the implementation here, or is this just not supported?