The doc at https://leanprover-community.github.io/extras/simp.html says about
all it does is repeatedly replace (or rewrite) subterms of the form A by B, for all applicable facts of the form A = B or A ↔ B. The simplifier mindlessly rewrites until it can rewrite no more.
This raises some questions as to how this works in practice:
simponly perform a brute force search or is it smarter?
- How does
simpnever end in a cyclic behavior?
- Is there some limit in the number of steps it takes to try to obtain the target?