Timeline for How does Lean `simp` tactic work?
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 10, 2023 at 14:06 | history | bumped | CommunityBot | This question has answers that may be good or bad; the system has marked it active so that they can be reviewed. | |
| Oct 11, 2023 at 13:49 | answer | added | tom | timeline score: 3 | |
| Sep 20, 2023 at 20:33 | comment | added | Weier | @JasonRute Interesting... I think you could turn this into an answer. | |
| Sep 20, 2023 at 18:24 | history | edited | Weier | CC BY-SA 4.0 |
Ooops
|
| Sep 20, 2023 at 18:19 | comment | added | Jason Rute |
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.
|
|
| Sep 20, 2023 at 18:03 | comment | added | Jason Rute | 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). | |
| Sep 20, 2023 at 18:00 | comment | added | Jason Rute |
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.
|
|
| Sep 20, 2023 at 15:32 | history | asked | Weier | CC BY-SA 4.0 |