search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
581 stars 236 forks source link

Add agda-presburger into stdlib #1041

Open Blaisorblade opened 4 years ago

Blaisorblade commented 4 years ago

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.

MatthewDaggitt commented 4 years ago

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?

Blaisorblade commented 4 years ago

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.