have `ring` fall back to `noncomm_ring`?

Stream: general

[Scott Morrison]

Now that we have a basic version of noncomm_ring available (that just calls simp with an appropriate simpset, then abel), could we arrange so that ring falls back to noncomm_ring when it can't find an appropriate comm_semiring instance?

[Scott Morrison]

I had a bit of a look through ring, but couldn't work out how to do this.

[Mario Carneiro]

ring already has fallback behavior, and it also doesn't a priori know what type it is working over, so not finding a comm_ring instance is possibly not a failure. All of which makes it difficult to use noncomm_ring as backup. Plus this is always going to be slower than calling noncomm_ring directly.

[Mario Carneiro]

That is, there are valid uses of ring when applied to an equality of non-commutative rings. Currently ring will act as a normalizer on any embedded subterms that are in commutative rings