simp/dsimp are not idempotent

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

I expect that simp and dsimp are typically idempotent, that is, re-running the tactic twice in a row with the same lemmas and same targets shouldn't make new progress. This expectation is violated in the following example:

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

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. In the third call, there are no references to hx, so it is able to simplify the 3 + 3 into 6.

Context

Zulip thread

Steps to Reproduce

See live.lean-lang.org

Expected behavior: Running simp or dsimp multiple times with the same arguments and targets shouldn't make new progress. Simplification should continue in a loop until it makes no more progress.

Actual behavior: (d)simp skips certain simplifying (some?) terms that appear in later ones. When simplification removes this dependency, (d)simp doesn't return and simplify those. On a repeated call, it does, so it makes new progress.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the minimal Lean example in the issue and reproduce the repeated dsimp at * behavior, then read the linked Zulip thread for context. Trace the simp/dsimp entry points and simplification order; done means repeated runs with the same arguments make no further progress in the reported case.