Zulip Chat Archive

Stream: general

Topic: New versions of Presburger tactics


view this post on Zulip Seul Baek (Oct 30 2018 at 08:15):

This project has been neglected for a long time, so I decided to tidy it up a bit. The new versions are available at https://github.com/skbaek/qe/. The main changes are :

1. Now there are tactics for nat, although they are slower than int equivalents due to quantifiers added during translation
2. There are versions that use znum instead of int in the shadow syntax for optimization
3. Makes more use of typeclasses
4. Also includes a tactic for DLO without endpoints for rat
5. The leanpkg.toml file is fixed, so you can install it using leanpkg

The main tactics are in the main.lean files of each directory. You can see the tests.lean files for examples of how they are used. As you might expect, znum is more efficient when handling large numbers, so there are examples which time out for int-based tactics but works with znum.

3 and 4 were done just to show that the shared-framework approach is viable. The idea (from Tobias Nipkow) is that QE-based FoL decision procedures mostly follow the same scheme, so the common part should be factored out using some module or typeclass system. Once this work is done, it is easy to cook up more decision procedures, since all you need to do is define (and prove soundness for) a single quantifier elimination step.

view this post on Zulip Patrick Massot (Oct 30 2018 at 08:56):

Thanks! Could you include a glossary of what all those acronyms mean? Maybe in a README.md?

view this post on Zulip Patrick Massot (Oct 30 2018 at 09:01):

What are all those commented out lines in the test files? Things that should work but don't?

view this post on Zulip Patrick Massot (Oct 30 2018 at 09:02):

For the purpose of using tests as documentation, it would probably be more efficient to move those test files somewhere more visible

view this post on Zulip Seul Baek (Oct 30 2018 at 09:19):

Thanks! Could you include a glossary of what all those acronyms mean? Maybe in a README.md?

Yes, I should either do that, or actually give intelligible names to definitions, which I was too lazy to type out when doing the proofs.

view this post on Zulip Seul Baek (Oct 30 2018 at 09:24):

The commented out lines are either theorems which currently time out, or nontheorems which would be useful for testing the soundness of unverified vm-versions of the tactics (which currently don't exist, but are easy to implement if necessary).

view this post on Zulip Seul Baek (Oct 30 2018 at 09:35):

Do you mean that it would be useful to add some introductory information about the tactics for users, and include tests as part of it? So far I've been using the tests just to check that it works, but I guess you're right that this would be more helpful as documentation.

view this post on Zulip Rob Lewis (Oct 30 2018 at 09:49):

Maybe call them "examples" instead of "tests," if they're being used as documentation. But yeah, this would be super helpful!

view this post on Zulip Rob Lewis (Oct 30 2018 at 09:49):

How much of mathlib does this depend on?

view this post on Zulip Rob Lewis (Oct 30 2018 at 10:08):

This looks great, by the way, I'm excited to try it out.

view this post on Zulip Seul Baek (Oct 30 2018 at 10:22):

It depends mainly on the int and nat libraries, along with some inequality stuff from algebraic libraries. At one point I needed some gcd lemmas not included in the master branch, so the current .toml file is tweaked to get 3.4.1 instead. But when I look for it now I can't pinpoint that incompatibility, so perhaps it works with master now.

view this post on Zulip Seul Baek (Oct 30 2018 at 10:23):

Thanks!

view this post on Zulip Tobias Grosser (Oct 30 2018 at 10:26):

Very interesting.

view this post on Zulip Tobias Grosser (Oct 30 2018 at 13:03):

@Seul Baek , when trying to compile this I get some errors:

$leanpkg  build
configuring qe 0.1
test: unrecognized option: -d
mathlib: cloning https://github.com/leanprover/mathlib to _target/deps/mathlib
> mkdir -p _target/deps/mathlib
> git clone https://github.com/leanprover/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 8, done.
remote: Counting objects: 100% (8/8), done.
remote: Compressing objects: 100% (7/7), done.
remote: Total 8217 (delta 1), reused 1 (delta 1), pack-reused 8209
Receiving objects: 100% (8217/8217), 5.24 MiB | 1.50 MiB/s, done.
Resolving deltas: 100% (5901/5901), done.
> git checkout --detach dbb3ff0b5b2e42aa71d8167d7efdb3aa12d6e483    # in directory _target/deps/mathlib
HEAD is now at dbb3ff0 feat(data/zmod/quadratic_reciprocity): quadratic reciprocity (#327)
> lean --make src
/home/grosser/Projects/qe/src/dnf/bak/qe.lean:1:0: error: file 'basic' not found in the LEAN_PATH
/home/grosser/Projects/qe/src/dnf/bak/qe.lean:1:0: error: file 'tauto' not found in the LEAN_PATH
/home/grosser/Projects/qe/src/dnf/bak/qe.lean:1:0: error: file 'list' not found in the LEAN_PATH
/home/grosser/Projects/qe/src/dnf/bak/qe_eq.lean:1:0: error: file 'axms' not found in the LEAN_PATH
/home/grosser/Projects/qe/src/dnf/main.lean:1:0: error: file 'dp' not found in the LEAN_PATH
/home/grosser/Projects/qe/src/dnf/main.lean:1:0: error: file 'pfrm' not found in the LEAN_PATH
/home/grosser/Projects/qe/src/dnf/main.lean:1:0: error: file 'reify' not found in the LEAN_PATH
/home/grosser/Projects/qe/src/lia/int_atm/dot_prod.lean:1:0: error: file 'list' not found in the LEAN_PATH
/home/grosser/Projects/qe/src/dnf/bak/qe.lean:1:0: error: invalid import: basic
could not resolve import: basic
/home/grosser/Projects/qe/src/dnf/bak/qe.lean:1:0: error: invalid import: tauto
could not resolve import: tauto
/home/grosser/Projects/qe/src/dnf/bak/qe.lean:1:0: error: invalid import: list
could not resolve import: list
/home/grosser/Projects/qe/src/dnf/main.lean:1:0: error: invalid import: dp
could not resolve import: dp
/home/grosser/Projects/qe/src/dnf/main.lean:1:0: error: invalid import: pfrm
could not resolve import: pfrm
/home/grosser/Projects/qe/src/dnf/main.lean:1:0: error: invalid import: reify
could not resolve import: reify
/home/grosser/Projects/qe/src/lia/int_atm/dot_prod.lean:1:0: error: invalid import: list
could not resolve import: list

view this post on Zulip Seul Baek (Oct 30 2018 at 13:43):

Oops, I forgot to push the commit in which I deleted older versions of files. I think it should work now.

view this post on Zulip Tobias Grosser (Oct 30 2018 at 19:35):

I also needed:

diff --git a/src/list.lean b/src/list.lean
index 6af0ace..369287c 100644
--- a/src/list.lean
+++ b/src/list.lean
@@ -248,3 +248,5 @@ begin
   intro heq, constructor; intros h a ha,
   rw ← heq, apply h _ ha, rw heq, apply h _ ha,
 end
+
+end list

view this post on Zulip Tobias Grosser (Oct 30 2018 at 20:23):

Nice. Some expressions already work nicely.

view this post on Zulip Tobias Grosser (Oct 30 2018 at 20:23):

Others time out quite a bit.


Last updated: May 10 2021 at 23:11 UTC