!4#2323 – mono

Stream: PR reviews

[Thomas Murrills]

So—assuming it passes CI—the mono tactic is finally done (!4#2323)! Yay!

However...

This is a big PR. I know people are busy, and I don't want to slow things down. I'm happy to factor things out into smaller PR's, postpone features, or really just whatever helps things go smoothly. Please feel free to let me know.

Part of what's contributing to the size are the additions to Tactic.Backtracking, which provides functionality that's like backtrack (in solve_by_elim), but minimizes the number of resulting goals. Btw: I hope to rewrite this in nondeterministic language once we add nondeterminism to mathlib4, so a major chance to refactor/rewrite it lies in the future.

I've at least done a fair amount of git surgery to streamline the commit history; however, I've never been on the reviewing end of a PR in that way, so again feel free to let me know if the commits would be better split differently. :)

[Scott Morrison]

Okay, this is indeed a big PR. :-) First question: could we postpone the whole BacktrackOptimize part of this?

(I do love this sort of stuff, don't worry, but I'd much prefer to review it as a "these changes make the results better" PR separately from a "these give us the functionality" PR.)

[Thomas Murrills]

Maybe! :) I’ll see if I can get by with the old solve_by_elim behavior for mono*. It won’t be perfect, but it might suffice for now!