getting `ring` to work on non-rings?

Stream: Is there code for X?

[Alex Kontorovich]

Is there such a thing as ring?? It would be quite useful, e.g., in situations like this:

import Mathlib

example {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] (intVIII intVII intV intIV : E) :
    intVIII - (-intVII + intV + intIV) = intVII - intV + intVIII - intIV := by
  sorry -- ring fails

Here is some annoying trivial identity, but ring fails because E is not assumed to be a ring. But if we replace the type of intIV : E etc by ℂ, then ring works. Could ring? say what it did to prove the identity in the case of ℂ, so I can try the same series of moves in the more general setting...?

[Johan Commelin]

The way ring works means that a ring? doesn't really make sense, unfortunately.

[Johan Commelin]

I guess that in principle, one could try to reconstruct a sequence of rws from the term that ring produces (if it produces one). But that seems nontrivial.

[Johan Commelin]

But there is ring1, right? Doesn't that try to put expressions in "normal form"?

[Jireh Loreaux]

No, that's ring_nf

[Eric Rodriguez]

does abel work here?

[Alex Kontorovich]

Yes!! Thank you!

[Kevin Buzzard]

It's not a ring but it is an abelian group:-)

[Alex Kontorovich]

Yep, I didn't know abel existed. Learn something new every day!...

[Patrick Massot]

Maybe you could benefit from rereading Chapter 8 of #mil then.

[Patrick Massot]

(this is where abel is mentioned in #mil)

[Alex Kontorovich]

I'm sure I'd benefit a lot from reading Chapters 1 - 11!... (Just need a few more hours in a day...)