rw works but simp_rw does not

Stream: lean4

[Bolton Bailey]

I have the following example:

import Mathlib

def StateM.get_set_get_set (s : σ)
    (q : σ → StateM σ β) (f g : σ → σ) :
    (do
      let s' <- get
      set (f s')
      let s'' <- get
      set (g s'')
      q s'')
    =
    (do
      let s' <- get
      set (g <| f s')
      q (f s')) := by
  ext s'
  simp_rw [StateT.run_bind, StateT.run_set, StateT.run_get, Id.bind_eq, Id.pure_eq]

section test

def foo : StateM ℕ Unit :=
  do
    let x ← get
    set (x + 1)
    let x ← get
    set (x + 1)
    let x ← get
    set (x + 1)
    let x ← get
    set (x + 1)
    let x ← get
    set (x + 1)
    let x ← get
    set (x + 1)

def foo' : StateM ℕ Unit :=
  do
    let x ← get
    set (x + 6)

example : foo = foo' := by
  simp [foo, foo']
  -- simp_rw [StateM.get_set_get_set] -- simp made no progress
  rw [StateM.get_set_get_set] -- works fine
  rw [StateM.get_set_get_set] -- works fine
  rw [StateM.get_set_get_set] -- works fine
  sorry

Why does rw work, but simp_rw/simp only doesn't? Is there a way to get the simplifier to work here?

[Mario Carneiro]

your simp lemma has a spurious (s : σ) argument

[Bolton Bailey]

So it does. This fixes it, thanks.

[Bolton Bailey]

I don't seem to get any unused argument warning on the lemma for that, though.

[Mario Carneiro]

#lint spots it

[Mario Carneiro]

(among other issues)

[Bolton Bailey]

Screenshot-2024-01-02-at-12.52.54-AM.png

[Bolton Bailey]

Here you can see it catches the h argument as unused, so clearly the VSCode linter is working on some level, but it doesn't catch the n or s argument.

[Mario Carneiro]

It seems to have something to do with autoimplicits:

example (a : σ) (q : StateM σ β) : True := trivial -- q unused
example (a : σ) (q : StateM σ Nat) : True := trivial -- a, q unused
example {β} (a : σ) (q : StateM σ β) : True := trivial -- a, q unused
example (a : σ) {β} (q : StateM σ β) : True := trivial -- a, q unused

[Mario Carneiro]

my guess is that there is some not-yet-solved metavariable involved and the unused argument linter pessimistically assumes it could depend on a