instances for grind #27620

Stream: mathlib4

[Kim Morrison]

In #27620, I added some instances for grind's algebraic machinery. In that PR, I chose to just put the instances at the first place they could be defined.

@Oliver Nash asked in the comments if it would be better to collect instances for grind in separate files. In fact, we already have some of this: the Lean.Grind.Ring instances are constructed in Mathlib.Algebra.Ring.GrindInstances. I did that one because there wasn't a natural home: it needs both

import Mathlib.Algebra.Ring.Defs
import Mathlib.Data.Int.Cast.Basic

My preference is to by default leave instances strewn about the library (perhaps with the convention that we never open namespaces to construct them, so searching for Lean.Grind. suffices to find them?).

But I'm happy to have suggestions here (from library experts) about better practices.

Note also that we are going to have many code blobs interacting with grind in future, for example just as we have positivity extensions all over Mathlib, we are likely going to have interval propagators for grind all over Mathlib. So additional costs of placement of these things needs to be weighed against a larger scale than then ~5 instances for grind we have so far.

[Oliver Nash]

Thanks for raising this Kim. Thinking about this some more I can't quite tell what I prefer for now. I expect the tradeoffs to be clearer once we have more examples.

It seems to me that it will be easier to collect instances than to disperse so maintaining the status quo (i.e., sprinkling instances through the library) seems like the right move for now.