fix(tactic/ring): fix loop in ring (#5711)
This occurs because when we name the atoms in `A * B = 2`, `A` is the
first and `B` is the second, and once we put it in horner form it ends up
as `B * A = 2`; but then when we go to rewrite it again `B` is named atom
number 1 and `A` is atom number 2, so we write it the other way around
and end up back at `A * B = 2`. The solution implemented here is to
retain the atom map across calls to `ring.eval` while simp is driving
it, so we end up rewriting it to `B * A = 2` in the first place but in the
second pass we still think `B` is the second atom so we stick with the
`B * A` order.
Fixes #2672
