[Merged by Bors] - fix: more stable choice of representative for atoms in ring and abel

[hrmacbeth]

Algebraic normalization tactics (ring, abel, etc.) typically require a concept of "atom", with expressions which are t-defeq (for some transparency t) being identified. However, the particular representative of this equivalence class which turns up in the final normalized expression is basically random. (It often ends up being the "first", in some tree sense, occurrence of the equivalence class in the expression being normalized.)

This ends up being particularly unpredictable when multiple expressions are being normalized simultaneously, e.g. with ring_nf or abel_nf: it can occur that in different expressions, a different representative of the equivalence class is chosen. For example, on current Mathlib,

example (x : ℤ) (R : ℤ → ℤ → Prop) : True := by
  let a := x
  have h : R (a + x) (x + a) := sorry
  ring_nf at h

the statement of h after the ring-normalization step is h : R (a * 2) (x * 2). Here a and x are reducibly defeq. When normalizing a + x, the representative a was chosen for the equivalence class; when normalizing x + a, the representative x was chosen.

This PR implements a fix. The AtomM monad (which is used for atom-tracking in ring, abel, etc.) has its addAtom function modified to report, not just the index of an atom, but also the stored form of the atom. Then the code surrounding addAtom calls in the ring, abel and module tactics is modified to use the stored form of the atom, rather than the form actually encountered at that point in the expression.

---

[github-actions]

PR summary 86eb01d068

Import changes exceeding 2%

%	File
+5.26%	Mathlib.Util.AtomM

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Util.AtomM	19	20	+1 (+5.26%)

Import changes for all files

Files	Import difference
Mathlib.Util.AtomM	1

---

Declarations diff

+ AtomM.addAtomQ
++ myId

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Vierkantor]

Zulip thread discussing this PR: https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2319119.20atom.20representatives.20for.20ring.20and.20abel

[Vierkantor]

One thing I was worried about but seems to be okay is compatibility with CanonM, but we could easily add a CanonM.canon call around addAtom, so that should be all good.

@eric-wieser, any further review comments?

[hrmacbeth]

Thanks for these improvements!

[eric-wieser]

bors d+

Thanks!

[mathlib-bors]

✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[hrmacbeth]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style