Commit 2024-11-21 03:58 ebe784ec

fix: more stable choice of representative for atoms in ring and abel (#19119) 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.