8
$\begingroup$

The doc at https://leanprover-community.github.io/extras/simp.html says about simp:

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:

  • Does simp only perform a brute force search or is it smarter?
  • How does simp never end in a cyclic behavior?
  • Is there some limit in the number of steps it takes to try to obtain the target?
Improve this question
$\endgroup$
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

1 Answer 1

Reset to default
3
$\begingroup$

  1. simp is using discrimination tree to find a small(ish) set of theorems that could be used for a rewrite at a particular place of the expression. simp then tries tries them all until it finds applicable one.

  2. It can end up in a cycle. That usually means that you have a simp theorem that is not "simplifying", e.g. like the mentioned 0=0+0. People say that rhs of simp rule has to be in "simp normal form" but I don't think there is a solid definition for it.

  3. There is an internal counter. If reached simp ends with an error.

The interesting question is, how does simp decide where to apply a rewrite rule?

simp runs in two passes, top to bottom(pre) and bottom to top(post). Example, for an expression id (5 + 0) + 0 simp would do something like this

pre: id (5 + 0) + 0
pre: id (5 + 0)
pre: 5 + 0
pre: 5
post: 5
pre: 0
post: 0
post: 5 + 0 ==> 5
post: id 5 ==> 5
post: 0
post: 5 + 0 ==> 5

Here all applied simp theorems were marked to be used in 'post' phase(defaut behavior).

*1. The query to the discrimination three is done at every post/pre step.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.