Zulip Chat Archive

We have two linarith PRs now: #2637 from @Mario Carneiro adds some nonlinear preprocessing and #2995 improves parsing into a linear structure. These are independent but the latter makes the former much more useful. A third change is on a branch (https://github.com/leanprover-community/mathlib/tree/linarith-speedup), it changes the representation of linear combinations to speed things up.

I also want to refactor the frontend because it's turned into a mess.

I propose that (when they're ready) we merge, in order, #2995, the branch, and #2637. Once the first two are in, there are interesting tests to add for the third. Further nlinarith improvements will be possible after refactoring the frontend. Does this sound okay? Trying to do the refactor while three semi-dependent PRs are floating around sounds like merge conflict hell.

Rob Lewis (Jun 11 2020 at 14:41):

I implemented a redundancy filter for the variable elimination step. Should have done this a long time ago. It has some extra overhead, so there's no effective change in speed on the old test file. But the nlinarith example goes from 8 seconds to 1.5.

Rob Lewis (Jun 11 2020 at 14:42):

Consider this a polite request for a review for the outstanding linarith PRs :) this will be yet another "independent" change that will be hard to merge.

Rob Lewis (Jun 14 2020 at 17:30):

Two of these are now merged. #2637 (nlinarith) is now updated to show that it can solve some tests. I'd love more tests here, but please confirm that nra solves them in Coq first!

Rob Lewis (Jun 14 2020 at 17:31):

Some of the changes I made to @Mario Carneiro 's code in #2637 are temporary. It'll change a lot in the linarith frontend refactor.

Rob Lewis (Jun 14 2020 at 17:32):

The redundancy filter should be mostly independent of the frontend changes, so I can do those at once.

Bryan Gin-ge Chen (Jun 18 2020 at 15:46):

There are now 3 open linarith-related PRs (thanks, Rob!): #3079, #3108, #3109

#3079 looks good to me, but I'm not really fluent in tactic-speak or the details of Fourier-Motzkin. Since it promises a nice speedup and also improves the generated proofs along the way, I think it'd be great to get it merged.

#3108 and #3109 introduce some mini-tactics, and they also look ready to me too.

Rob Lewis (Jun 18 2020 at 16:07):

I wouldn't be surprised if there were bugs in #3079. But it builds the library and passes the tests; I'm not sure reviews will catch them and I'm not sure what more to check for. I think it's ready for testing in production.

Rob Lewis (Jun 18 2020 at 16:09):

The next linarith PR will be a massive refactor. Sorry in advance to whoever reviews that! The new tactics in #3108 and #3109 are the most user-facing parts of it though, a lot of it is moving around internals.

Rob Lewis (Jun 19 2020 at 09:53):

#3113 is up (obviously blocked by #3108 and #3109)! Sorry again for the big diff.

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib