simp can't rewrite definitions backwards

[alreadydone]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

rw can rewrite backwards using the equational lemma associated to a definition, but simp, simp_rw, simp only cannot.

Steps to Reproduce

def double (n : ℕ) : ℕ := n + n

example (n : ℕ) : double n = n + n := by
  simp_rw [← double]

Expected behavior: No goals

rw [← double], simp_rw [double], rw [double] exhibit this correct behavior.

Actual behavior:

invalid '←' modifier, 'double' is a declaration name to be unfolded

simp only [← double] and simp [← double] exhibit the same bad behavior.

Reproduces how often: every time

Versions

Lean (version 4.0.0-nightly-2023-08-15, commit b5a7367, Release)
MacOS Ventura 13.5

[semorrison]

This is the intended behaviour. simp and rw simply handle "unfolding definitions" differently, and it is not intended that you can "refold" a definition using simp.

[alreadydone]

The irreplaceable use case of simp_rw is to rewrite under a binder, which rw can't do. (It's convenient that it can rewrite multiple times, but that's just more cumbersome with rw.) What should I do to refold a definition under a binder? It's infeasible to manually write a equational lemma for every definition, right?

[semorrison]

My guess is this happens infrequently enough (I don't think I've ever wanted to do this!) that writing an equational lemma on the spot, to use in simp_rw is the right solution. But this discussion should happen on zulip, I think.