Skip to main content
Proof Assistants Beta

You are not logged in. Your edit will be placed in a queue until it is peer reviewed.

We welcome edits that make the post easier to understand and more valuable for readers. Because community members review edits, please try to make the post substantially better than how you found it, for example, by fixing grammar or adding additional resources and hyperlinks.

4
  • $\begingroup$ Few comments: There are actually two searches to consider. One is how it finds the simp lemmas in the environment to apply. The next is which lemma to apply first and at which position in the formula. (I don't know the exact answer for either.) At least in some cases you can make simp go into an infinite loop. The first is with a simp lemma which expands like 0=0+0. It will reach a maximum recursion depth and fail. The other is with something like foo = baz and baz = foo. In these cases you get a "maximum number of steps exceeded" or maximum heartbeats error depending on the situation. $\endgroup$
    – Jason Rute
    Commented Sep 20, 2023 at 18:00
  • $\begingroup$ The reason that simp usually behaves well is that users are very careful about which lemmas are labeled as simp lemmas in the library (as the document you linked goes into detail about). $\endgroup$
    – Jason Rute
    Commented Sep 20, 2023 at 18:03
  • $\begingroup$ A good set of simp lemmas will converge to a normal form (if not solve the goal) and it shouldn't matter which order they are applied. A "smarter simp" is the rw_search tactic which attempts to prove two terms are equal with a series of rewrites, although it is for a slightly different use case than simp and there is no expectation of reaching a normal form, so backtracking search is required in rw_search. $\endgroup$
    – Jason Rute
    Commented Sep 20, 2023 at 18:19
  • 1
    $\begingroup$ @JasonRute Interesting... I think you could turn this into an answer. $\endgroup$
    – Weier
    Commented Sep 20, 2023 at 20:33