Tactic for solving equations in the language of commutative (semi)rings. This version of ring fails if the target is not an equality that is provable by the axioms of commutative (semi)rings.

Tactic for solving equations in the language of commutative (semi)rings. Attempts to prove the goal outright if there is no at specifier and the target is an equality, but if this fails it falls back to rewriting all ring expressions into a normal form. When writing a normal form, ring SOP will use sum-of-products form instead of horner form. ring! will use a more aggressive reducibility setting to identify atoms.