!4#2920 backtracking code in solve_by_elim

Stream: PR reviews

[Scott Morrison]

Could someone have a look at !4#2920? This is a refactor of solve_by_elim that separates out the backtracking management from the lemma application. There is no change in behaviour or algorith, it's just separation of distinct concerns. I have a followup PR to make that revamps the backtracking code completely, giving it a much more sensible API that will hopefully be helpful for working with nondeterministic tactics generally. But I'd like this simple PR through first.

[Scott Morrison]

In particular, if you have complaints about the API for controlling backtracking in this PR being baroque or unnecessarily complicated: yes, I know! :-) It's just what is currently in mathlib4, and I'll make it saner in the next PR.

[Alex J. Best]

Do you plan to use aesop (or its internals) in the next PR? Backtracking search on mvars sounds quite similar to what aesop is doing, at least superficially, I have no idea how easy it is to make use of for non-aesop tactics

[Kyle Miller]

There's not very much that goes into backtracking search itself. In a sense, it's just these three lines that drive backtracking, and the rest is policy.

I'd worry that trying to make everything that uses backtracking search to use the same engine would complicate things, but if aesop already has something to do backtracking search with solve_by_elim-like policies then it could be worth looking into.

[Scott Morrison]

There is now a follow-up PR to this one, at https://github.com/leanprover-community/mathlib4/pull/3480, which simplifies how apply_rules is implemented in terms of solve_by_elim. Now that the backtracking is separate from the lemma application, we can just not backtrack, rather than hack no-backtracking on top of backtracking code!