agda
Add agda-presburger into stdlib
IMHO, some tactic for Presburger arithmetic (including inequalities) belongs to the stdlib.
I was thinking of https://github.com/gallais/agda-presburger; @gallais confirmed he'd be willing to relicense it https://twitter.com/anormalform/status/1209621155499429888, but he also said that some further work would be needed.
There's also the tactic in #254, but it's not so clear if it's complete (I can't find it claimed in words, and I can tell the code doesn't include a completeness proof), while agda-presburger includes a completeness proof.
This would be great if you're willing to put in the effort of porting it :+1: It would probably be best if you could do it in small chunks though, I'm not sure I'd be able face wading through a PR of the whole thing in one go!
While we're introducing @oisdk's new algebraic solvers I think we should take the opportunity to move them to a new top-level Tactic directory especially for containing things like this?
Wow, that sounds a lot of effort. I confess porting that myself is beyond the budget I have in the near future. I suspect it'd be best to keep most of the code outside of the public API.
Nevertheless, this is one of the main issues that pushed me to Coq (when at the end of my PhD thesis I started using step-indexed logical relations), and I'm sure I can't be the only one.
It would. Should we have a list somewhere? I will likely have summer students again. And this is much more well-delimited than some of the other things I've tried to make them work on!
