How to Build a Simp Set That Only Unfolds Notations in Lean 4

So far, I have repeatedly written dsimp [(· < ·), MyNat.lt] to unfold the definition of m < n. This time, I create a tactic to reduce that repetition. The textbook I'm still using is "Learning Lean from Scratch: Hands-On Development of a Formal Mathematics Library."

A Naive Approach and Its Problem

The simplest approach is to register the equivalence m < n ↔ m + 1 ≤ n with simp.

theorem MyNat.lt_def (m n : MyNat) : m < n ↔ m + 1 ≤ n := by
  rfl
section
  attribute [local simp] MyNat.lt_def
  example (m n : MyNat) : m < n := by
    simp_all
    guard_target =ₛ m + 1 ≤ n
    -- Unnecessary simplification rules are also being applied.
    sorry
end

With this approach, calling simp also applies ordinary simp rules along with MyNat.lt_def. This is inconvenient when I only want to unfold the target notation.

Defining notation_simp

Using register_simp_attr notation_simp, I create a dedicated simp attribute, and a macro that applies only the registered lemmas via simp only.

macro_rules
| `(tactic| notation_simp $[[$simpArgs,*]]? $[at $location]?) =>
  let args := simpArgs.map (·.getElems) |>.getD #[]
  `(tactic| simp only [notation_simp, $args,*] $[at $location]?)
end

This defines a dedicated simp lemma set (notation_simp) intended only for unfolding and simplifying specific notations, and the tactic is a short shortcut for invoking it.

Next, I register MyNat.lt_def to notation_simp.

attribute [notation_simp] MyNat.lt_def

Checking the Behavior

I can confirm that notation_simp unfolds only m < n.

example (m n : MyNat) : m < n := by
  notation_simp
  guard_target =ₛ m + 1 ≤ n
  sorry

It can be used the same way as the ordinary simp tactic, e.g. notation_simp at *.

example (m n : MyNat) (h : m < n) : m + 1 ≤ n := by
  notation_simp at *
  assumption

I also confirm that this has no effect on plain simp.

example (m n : MyNat) : m < n := by
  -- `simp` made no progress
  -- simp

Adding notation_simp?

Finally, I add notation_simp?, which shows which lemmas were used in the unfolding.

section
open Lean Parser Tactic
syntax "notation_simp?" (simpArgs)? (location)? : tactic
macro_rules
| `(tactic| notation_simp? $[[$simpArgs,*]]? $[at $location]?) =>
  let args := simpArgs.map (·.getElems) |>.getD #[]
  `(tactic| simp? only [notation_simp, $args,*] $[at $location]?)
end
example (m n : MyNat) : m < n := by
  notation_simp?
  -- Try this:
  -- [apply] simp only [MyNat.lt_def]

The code is available on the GitHub repository.