simp? failure with simp working

Stream: mathlib4

[Nailin Guan]

I have a mwe for this wierd situation.

public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

lemma foo {R R' : Type*} [CommRing R] [IsLocalRing R] [CommRing R'] [IsLocalRing R']
    (e : R ≃+* R') : (IsLocalRing.maximalIdeal R').comap e = IsLocalRing.maximalIdeal R := by
  ext
  simp

changing into simp? fails here.

[Ruben Van de Velde]

If you run simp? again you get

import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

lemma foo {R R' : Type*} [CommRing R] [IsLocalRing R] [CommRing R'] [IsLocalRing R']
    (e : R ≃+* R') : (IsLocalRing.maximalIdeal R').comap e = IsLocalRing.maximalIdeal R := by
  ext
  simp only [Ideal.mem_comap, IsLocalRing.mem_maximalIdeal, map_mem_nonunits_iff, mem_nonunits_iff]
  simp only [MulEquiv.isUnit_map]

Not sure what's wrong here

[Michael Stoll]

This is an issue with simp using priorities, but simp only not doing that. Compare the traces:

[Meta.Tactic.simp.rewrite] Ideal.mem_comap:1000:
      x✝ ∈ Ideal.comap e (IsLocalRing.maximalIdeal R')
    ==>
      e x✝ ∈ IsLocalRing.maximalIdeal R'
[Meta.Tactic.simp.rewrite] IsLocalRing.mem_maximalIdeal:1000:
      e x✝ ∈ IsLocalRing.maximalIdeal R'
    ==>
      e x✝ ∈ nonunits R'
[Meta.Tactic.simp.rewrite] map_mem_nonunits_iff:10000:  <----
      e x✝ ∈ nonunits R'
    ==>
      x✝ ∈ nonunits R
[Meta.Tactic.simp.rewrite] mem_nonunits_iff:1000:
      x✝ ∈ nonunits R
    ==>
      ¬IsUnit x✝
[Meta.Tactic.simp.rewrite] IsLocalRing.mem_maximalIdeal:1000:
      x✝ ∈ IsLocalRing.maximalIdeal R
    ==>
      x✝ ∈ nonunits R
[Meta.Tactic.simp.rewrite] iff_self:1000:
      ¬IsUnit x✝ ↔ ¬IsUnit x✝
    ==>
      True

and

[Meta.Tactic.simp.rewrite] Ideal.mem_comap:1000:
      x✝ ∈ Ideal.comap e (IsLocalRing.maximalIdeal R')
    ==>
      e x✝ ∈ IsLocalRing.maximalIdeal R'
[Meta.Tactic.simp.rewrite] IsLocalRing.mem_maximalIdeal:1000:
      e x✝ ∈ IsLocalRing.maximalIdeal R'
    ==>
      e x✝ ∈ nonunits R'
[Meta.Tactic.simp.rewrite] mem_nonunits_iff:1000:
      e x✝ ∈ nonunits R'
    ==>
      ¬IsUnit (e x✝)
[Meta.Tactic.simp.rewrite] IsLocalRing.mem_maximalIdeal:1000:
      x✝ ∈ IsLocalRing.maximalIdeal R
    ==>
      x✝ ∈ nonunits R
[Meta.Tactic.simp.rewrite] mem_nonunits_iff:1000:
      x✝ ∈ nonunits R
    ==>
      ¬IsUnit x✝

The higher priority of docs#map_mem_nonunits_iff makes simp use it, which then enables further simplifications. But simp only does not look at these priorities, so it first applies some other lemma, which leads to a different path (this also has the effect that the linter says that map_mem_nonunits_iff is unused in the simp only call).

Ultimately, this indicates a lack of confluence of simp lemmas. One should be able to fix this by adding a simp lemma that makes the process confluent again. (Presumably a lemma that transfers docs#IsUnit via a docs#RingEquiv .)

[Michael Stoll]

In fact, docs#MulEquiv.isUnit_map is a simp lemma. The problem (I think) is that simp? just lists the lemmas that the original simp call uses, and the list then may not contain lemmas needed for the confluence. Indeed,

import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

lemma foo {R R' : Type*} [CommRing R] [IsLocalRing R] [CommRing R'] [IsLocalRing R']
    (e : R ≃+* R') : (IsLocalRing.maximalIdeal R').comap e = IsLocalRing.maximalIdeal R := by
  ext
  simp only [Ideal.mem_comap, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, MulEquiv.isUnit_map]

works.

[Kevin Buzzard]

Is there a reason that simp only doesn't use priorities?

[Kim Morrison]

It sort of does use priorities, the problem just that when we add things in the argument list we don't look up the priorities from the environment simp attribute if present.

It's a bit unclear to me what we want here. I like that simp only's behaviour is independent of whatever crap people have put in the environment, and looking up the priorities would break that.

[Violeta Hernández]

just spitballing, maybe simp? could call simp only with some +priority option?

[Kim Morrison]

Yes, or maybe even run the simp only output, and if it failed retry with simp +priority.

To be honest, sounds like a lot of work, although this is a pain point that has come up multiple times.

If someone would be game to write an RFC for the two new pieces of behavior (or suggest an alternative approach), and demonstrate that people agree it's a good approach, I'd be willing to try implementing.