RFC: simp attribute to accept ← modifier

[nomeata]

Proposal

When invoking the simp tactic, it is possible to write simp [foo, ↓bar, ←baz], but the attribute version of extending the simpset only supports

attribute [simp] foo
attribute [simp ↓] bar

but not

attribute [simp ←] bar

to add the inverse of a rewrite rule to the simp set.

Adding support for this presumably amounts to extending the syntax in Lean.Parser.Attr.simp and then setting the inv parameter to Lean.Meta.addSimpTheorem in Lean.Meta.mkSimpAttr.

I assume there is no reason this isn’t already the case beyond “nobody asked for it yet”?

Context

The alternative rsimp simpset that’s part of the plan in #5806 benefits from being able to write

attribute [simp ←] Nat.add_eq

instead of

@[rsimp] def Nat.add_eq_symm := fun a b => (@Nat.add_eq a b).symm

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.