simp rejects perm lemma rewrite that previously worked (regression after #12000)

[kim-em]

Description

After #12000 ("fix: split ngen on async elab"), simp incorrectly rejects a valid rewrite when a lemma is treated as a perm lemma.

Specifically, simp [zsmul_comm] fails where it previously succeeded. The workaround simp [zsmul_comm _ z] (with explicit argument) works because it's no longer treated as a perm lemma.

Bisect Result

Using lean-bisect, the regression was identified:

• Last working commit: 8435dea274b0
• First broken commit: c7d3401417b3 (PR fix: split ngen on async elab #12000)

The change to the name generator appears to affect simp's AC ordering (acLt) used for perm lemma decisions.

Minimal Reproduction

notation "ℤ" => Int

class AddZero (M : Type _) extends Zero M, Add M

class AddZeroClass (M : Type u) extends AddZero M where
  zero_add : ∀ a : M, 0 + a = a
  add_zero : ∀ a : M, a + 0 = a

class AddMonoid (M : Type u)  extends AddZeroClass M where
  nsmul : Nat → M → M
  nsmul_zero : ∀ x, nsmul 0 x = 0 := by intros; rfl
  nsmul_succ : ∀ (n : Nat) (x), nsmul (n + 1) x = nsmul n x + x := by intros; rfl

instance AddMonoid.toNatSMul {M : Type _} [AddMonoid M] : SMul Nat M := sorry

class IsAddTorsionFree (M : Type _) [AddMonoid M] where
  nsmul_right_injective ⦃n : Nat⦄ (hn : n ≠ 0) : Function.Injective fun a : M ↦ n • a

class InvolutiveNeg (A : Type _) extends Neg A where
  neg_neg : ∀ x : A, - -x = x

class SubNegMonoid (G : Type u) extends AddMonoid G, Neg G, Sub G where
  sub := fun a b => a + -b
  sub_eq_add_neg : ∀ a b : G, a - b = a + -b := by intros; rfl
  zsmul : Int → G → G
  zsmul_zero' : ∀ a : G, zsmul 0 a = 0 := by intros; rfl
  zsmul_succ' (n : Nat) (a : G) : zsmul n.succ a = zsmul n a + a := by intros; rfl
  zsmul_neg' (n : Nat) (a : G) : zsmul (Int.negSucc n) a = -zsmul n.succ a := by intros; rfl

instance SubNegMonoid.toZSMul {M} [SubNegMonoid M] : SMul Int M := sorry

class SubtractionMonoid (G : Type u) extends SubNegMonoid G, InvolutiveNeg G where
  neg_add_rev (a b : G) : -(a + b) = -b + -a
  neg_eq_of_add (a b : G) : a + b = 0 → -a = b

class SubtractionCommMonoid (G : Type u)  extends SubtractionMonoid G

class AddGroup (A : Type u) extends SubNegMonoid A where
  neg_add_cancel : ∀ a : A, -a + a = 0

instance AddGroup.toSubtractionMonoid [AddGroup G] : SubtractionMonoid G :=
  { neg_neg := sorry, neg_add_rev := sorry, neg_eq_of_add := sorry }

class AddCommGroup (G : Type u)  extends AddGroup G

instance AddCommGroup.toSubtractionCommMonoid [AddCommGroup G] : SubtractionCommMonoid G :=
  { ‹AddCommGroup G›, AddGroup.toSubtractionMonoid with }

theorem zsmul_comm {α : Type _} [SubtractionMonoid α] (a : α) (m n : Int) :
    n • m • a = m • n • a := sorry

theorem zsmul_sub {α : Type _} [SubtractionCommMonoid α] (a b : α) (n : Int) :
    n • (a - b) = n • a - n • b := sorry

theorem zsmul_right_inj {G : Type _} [AddGroup G] [IsAddTorsionFree G] {n : Int} {a b : G}
    (hn : n ≠ 0) : n • a = n • b ↔ a = b := sorry

variable {G : Type _} [AddCommGroup G] {a b p : G} {z : Int}

def ModEq (a b p : G) : Prop := sorry
notation:50 a " ≡ " b " [PMOD " p "]" => ModEq a b p
theorem modEq_iff_zsmul : a ≡ b [PMOD p] ↔ ∃ m : Int, m • p = b - a := sorry

-- SUCCESS: With explicit args, zsmul_comm is not treated as a perm lemma
example [IsAddTorsionFree G] (hn : z ≠ 0) :
    z • a ≡ z • b [PMOD z • p] ↔ a ≡ b [PMOD p] := by
  simp [modEq_iff_zsmul, ← zsmul_sub, zsmul_comm _ z, zsmul_right_inj hn]

-- FAILURE: Without explicit args, zsmul_comm is treated as a perm lemma and rejected
example [IsAddTorsionFree G] (hn : z ≠ 0) :
    z • a ≡ z • b [PMOD z • p] ↔ a ≡ b [PMOD p] := by
  simp [modEq_iff_zsmul, ← zsmul_sub, zsmul_comm, zsmul_right_inj hn]
  -- Error: unsolved goals
  -- ⊢ (∃ m, m • z • p = z • (b - a)) ↔ ∃ m, m • p = b - a

Expected behavior

Both simp [zsmul_comm _ z] and simp [zsmul_comm] should successfully apply the rewrite.

Actual behavior

simp [zsmul_comm] is treated as a perm lemma, and the AC ordering rejects the rewrite m • z • p ==> z • m • p.

Versions

• First broken: nightly-2026-01-15 (commit c7d3401)
• Last working: nightly-2026-01-14 (commit 8435dea)

Impact

This regression breaks proofs in Mathlib that rely on simp [zsmul_comm] without explicit arguments. The workaround is to add explicit arguments like simp [zsmul_comm _ z].

[kim-em]

The minimal reproduction above was produced using lean-minimizer, starting from a Mathlib proof in Mathlib.Algebra.Group.ModEq.

[kim-em]

@Kha, do you want to take another look at #12000? I can look into it if you prefer.

[Rob23oba]

I'll give you a simpler mwe:

variable {a : Nat}

--set_option Elab.async false

theorem th (b : Nat) (h : a + b = 3) : b + a = 3 := by
  simp [Nat.add_comm, h]

The proof works

• in older versions
• when a : Nat becomes a parameter of the theorem
• when Elab.async is disabled
• when theorem th becomes an example

but not in versions after #12000 when left unchanged.

pp.raw shows:
a = _uniq.6 and b = _uniq.101.2 and _uniq > _uniq.101 and thus a = _uniq.6 > _uniq.101.2 = b while previously a < b

[Kha]

Thanks both. So the fvar ids after and before are

#eval Name.lt (.num (.num `_uniq 102) 2) (.num `_uniq 7)  -- true
#eval Name.lt (.num `_uniq 100) (.num `_uniq 5)  -- false

So NameGenerator.mkChild is not compatible with the (unstated?) assumption that later fvars compare greater according to Name.lt (and thus perm lemmas reorder fvars in declaration order). This seems... extremely unfortunate. I think we should revert #12000 until we come up with a solution. /cc @kim-em

[kim-em]

Created PRs to address this:

• fix: revert "split ngen on async elab" #12148 - Reverts fix: split ngen on async elab #12000
• test: add regression test for perm lemma fvar ordering #12149 - Adds regression test based on @Rob23oba's simpler MWE

Also opened #12150 to track the original go-to-definition issue that #12000 was trying to fix.