Match equations not allowed in simp only theorem list

[JLimperg]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In the following example, a simp only list suggested by simp? fails:

-- works
theorem foo₁ (a : Nat) (ha : a = 37) :
    (match h : a with | 42 => by simp_all | n => n) = 37 := by
  simp? [ha]
  -- Try this: simp only [ha, Nat.reduceEqDiff, imp_self, foo₁.match_1.eq_2]

-- fails
theorem foo₂ (a : Nat) (ha : a = 37) :
    (match h : a with | 42 => by simp_all | n => n) = 37 := by
  simp only [ha, Nat.reduceEqDiff, imp_self, foo₂.match_1.eq_2]
  -- invalid field notation, type is not of the form (C ...) where C is a constant
  --   foo₂

The issue might be that on-demand generation of match equations is not triggered by simp only.

Versions

nightly-2024-05-22

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

I think your analysis is correct. So either match equations become public API, and should take part in the lazy definition generation, or there needs to be a way to say “equations for this match” like with functions. Or both. The former is probably easier.

[leodemoura]

match equational theorems are supposed to be internal and are applied even if simp only does not list them. For example, the following works as expected

theorem foo₂ (a : Nat) (ha : a = 37) :
    (match h : a with | 42 => by simp_all | n => n) = 37 := by
  simp only [ha, Nat.reduceEqDiff, imp_self]

So, we can't simply omit match equational theorems when generating the simp only command at simp?.