Adding new instances

Stream: new members

[Riccardo Brasca]

What is the general attitude for adding new instances? Should we add as much instances as possible or it is better to keep their number not too high (for performance reasons for example). I see that there is no algebra R I.quotient, where I is an ideal of R. Should I add it?

[Mario Carneiro]

The rules for adding instances are more complicated than that. It comes down to how the instance affects the overall search problem. Loops are bad, more instances are bad but only very slightly; instances are organized according to their type class (in this case algebra), so it depends on whether there are already many instances in this class and also how many search problems for other things go via this class (I would think not many, because algebra already has two input arguments).

[Mario Carneiro]

The other major thing is whether there will be any competition for the things that this instance will satisfy, because non-defeq diamonds in the typeclass system are also bad

[Eric Wieser]

This sounds like a more powerful version of docs#mul_action.quotient, right?

[Riccardo Brasca]

Yes. It is very easy ,ring_hom.to_algebra (ideal.quotient.mk I) is enough. To me it seems very natural to have it, but I can write it down explicitly in my theorems of course.

[Eric Wieser]

smul is defined as a * xunder the quotient, right?

[Riccardo Brasca]

Yes, it is (ideal.quotient.mk a) * x.

[Riccardo Brasca]

There is absolutely nothing deep or interesting in this particular case, I was just wondering how to deal with missing instances that from a mathematical point of view are obvious.

[Eric Wieser]

I only ask because I was worried that it might not be defeq to the mul_action instance

[Riccardo Brasca]

Ah, I see that there are subtle problems sometimes...

[Eric Wieser]

Although actually that's not relevant here, ideals are not quotient_groups.

Your instance sounds like a good ide ato me