Consider excluding obviously-looping local equations from the norm simp call

[JLimperg]

Example:

import Aesop

example (n : Nat) : n > 0 → ¬ (n = n - 1) := by
  aesop

This makes simp loop because it repeatedly rewrites n ==> n - 1. We could detect equations of this form and by default exclude them from the norm simp call.

[yangky11]

Hi @JLimperg, related to this issue, I'm wondering why aesop doesn't just check whether the goal has changed after a normalization tactic and throw an error?

[JLimperg]

Whether the goal has changed is not so easy to detect. You can check for identity of metavariables, which is fast but unreliable. You can check for structural equality of the goal metavariables (contexts and types), which is O(n) in the size of the goal, but then you should also ignore things like changed FVarIds and MVarIds (as long as their types/values are still the same). Lean does not provide a suitable method, but I've now implemented one, so it might indeed be a good idea to use that. Alternatively, I could expose it as a combinator for normalization rules to use if they can't detect goal changes more efficiently (which most rules can).

The example above would not be affected either way because the rewrite rule n ==> n - 1 actually changes the goal in each iteration.