non-idempotent `dsimp`

Stream: lean4

[Alex Meiburg]

I ran into this issue, where dsimp at * isn't idempotent, i.e. re-running it made further progress. I had the same issue with simp that confused me more, at first, but it reduced to the same basic issue as here.

mwe with no Mathlib:

theorem bad (x : Fin 6) (y : Fin x) (h : x < y.val) : False := by
  rcases x with ⟨x, hx⟩
  rcases y with ⟨y, hy⟩
  dsimp at * --makes some progress
  dsimp at * --makes more progress
  sorry

What happens is that h refers back to hy, so dsimp doesn't want to simplify hy. It does simplify h, though, in a way which _removes_ the reference to hy. Then on a second call to dsimp at * it is able to - and does - simplify hy.

[Alex Meiburg]

Is this an issue in Lean I should report? It leads to, at least, very confusing behavior (imo) where I was writing simp at *; simp at * but couldn't understand for a while why I couldn't combine it into one.

[Alex Meiburg]

Actually, here's a very simple extension that needs 3 applications to converge!

theorem bad (x : Fin (3 + 3)) (y : Fin x) (h : x < y.val) : False := by
  rcases x with ⟨x, hx⟩
  rcases y with ⟨y, hy⟩
  dsimp at * --makes some progress
  dsimp at * --makes more progress
  dsimp at * --makes even more!
  sorry

[Alex Meiburg]

Well I created lean4#8300