simps generates wrong lemma for OrderIso symm_apply

[kckennylau]

Since OrderIso is defined as an abbrev of RelIso, @[simps!] automatically uses RelIso.symm for the symm_apply projection, so in the code below the automatically generated lemma foo_symm_apply actually has type (RelIso.symm foo) a✝ = f a✝, which is undesirable (and doesn't use OrderIso.symm.

Unfortunately, there are no easy ways to fix this, since we have 52 automatically generated lemmas involving RelIso.symm _ _ = _ and 59 manually proved lemmas involving e.symm _ = _.

The possible solutions are:

1. Go through each of the 52 lemmas generated by simps, manually remove them and prove the OrderIso.symm version, and then add a linter against using @[simps!] on OrderIso. Resistance: the smallest.
2. Remove OrderIso.symm entirely, and just use RelIso.symm. Resistance: this is still defeq abuse, and the resulting term would not have the correct type, i.e. the resulting term will have type RelIso instead of OrderIso.
3. Allow simps to be configured on definitions, not just structure. Resistance: probably will take a long time until this actually happens.
4. Have a simp lemma e.symm x = RelIso.symm e x. Resistance: this will break the 59 simp lemmas above.
5. Have a simp lemma RelIso.symm e x = e.symm x. Resistance: this doesn't actually fix the problem, because @[simps!] will still generate the wrong lemma.

For now, 1. seems to be the least of the evils.

import Mathlib

axiom f : ℕ → ℕ
axiom f_eq {n} : f n = n

@[simps!] noncomputable def foo : ℕ ≃o ℕ where
  toFun := f
  invFun := f
  left_inv _ := by simp [f_eq]
  right_inv _ := by simp [f_eq]
  map_rel_iff' := by simp [f_eq]

#check foo_symm_apply -- (RelIso.symm foo) a✝ = f a✝

example (n) : foo.symm n = sorry := by simp -- no progress

(Link to web editor)

[SproutSeeds]

Hi all, I am planning a local first pass on this issue this week. I will run style preflight and local gate before opening any draft PR. If someone is already working on this, happy to coordinate and I can switch targets.

[SproutSeeds]

I can still reproduce this on current master.

• The original sample still gives foo_symm_apply : (RelIso.symm foo) a✝ = f a✝, and simp still makes no progress on foo.symm.
• trace.simps.verbose points to the core reason: @[simps!] is reducing OrderIso to RelIso before it chooses projection data, so it is generating foo_symm_apply from the stored RelIso symm_apply projection rather than from an OrderIso.symm-based surface.
• I checked whether this could be patched locally by registering OrderIso-specific simps projections, but initialize_simps_projections OrderIso ... hard-errors because OrderIso is an abbrev, not a structure.
• I also tested the two bridge-lemma directions from the issue body:
  • RelIso.symm e x = e.symm x did not fix the sample simp behavior.
  • e.symm x = (RelIso.symm e) x did fix the sample behavior, which matches the issue body's option 4, but it also pushes simplification toward RelIso.symm.

So my current read is that I do not yet see a narrow local patch that both fixes the generated theorem shape and preserves the existing OrderIso.symm API normal form. That still makes the issue body's option 1 look like the smallest viable repo-local path, unless simps grows explicit support for abbrev-specific projection configuration.