Zulip Chat Archive

Stream: general

Topic: Cooper's algorithm

Seul Baek (May 20 2018 at 00:19):

I've implemented Cooper's algorithm for linear integer arithmetic as a Lean tactic (https://github.com/skbaek/qelim). It's still quite limited, but it should work for simple goals.

cooper is the completely verified tactic that is proof-producing all the way. Unfortunately, it is unusably slow.
cooper_vm is the partially verified tactic whose first step (replacing the original goal with the new quantifier-eliminated goal) is proof-producing. The second step (evaluating the new goal to a tautology) is trusted.
The tactics assume sentential goals, so you'll have to generalize variables and hypotheses before calling it.
The implementation is based on Tobias Nipkow's paper (http://www21.in.tum.de/~nipkow/pubs/jar10.pdf).
I've added a few test cases (qelim/lia/cooper/tests.lean) from John Harrison's book.
Right now I'm having trouble making absolute paths work. All references to mathlib are relative.

Mario Carneiro (May 20 2018 at 00:22):

Hey! Seul's here! And he brings gifts

Mario Carneiro (May 20 2018 at 00:34):

I notice that your atom type uses int. This will kill your efficiency, if you are doing kernel evaluation. You should use znum instead

Mario Carneiro (May 20 2018 at 00:38):

Re: paths, do you have a leanpkg.toml file in your project? I don't see one, but it's important for making file resolution work

Mario Carneiro (May 20 2018 at 00:43):

For others who may not be aware: this is basically the omega tactic everyone's been talking about, although Cooper's is a slightly different algorithm for the same problem

Andrew Ashworth (May 20 2018 at 03:35):

Thanks for releasing this! It looks like it was quite a substantial effort, with the first commit being a few months ago. I definitely want to spend some time looking over it!

Seul Baek (May 20 2018 at 21:09):

I notice that your atom type uses int. This will kill your efficiency, if you are doing kernel evaluation. You should use znum instead

Thanks for the suggestion! Maybe this is what's making cooper so much slower than cooper_vm.

Seul Baek (May 20 2018 at 21:13):

Re: paths, do you have a leanpkg.toml file in your project? I don't see one, but it's important for making file resolution work

I'm actually having problems with mathlib itself—when I clone mathlib it won't work as is, because Lean doesn't like its absolute paths for some reason. It works after I manually relativize them. This is strange because mathlib does have a leanpkg.toml file.

Kevin Buzzard (May 20 2018 at 21:15):

You want to make mathlib a dependency for your project

Kevin Buzzard (May 20 2018 at 21:16):

if you use leanpkg and add mathlib as a dependency then it should sort out everything for you

Kevin Buzzard (May 20 2018 at 21:17):

see section 1.4.3 of the reference manual

Kevin Buzzard (May 20 2018 at 21:17):

https://leanprover.github.io/reference/using_lean.html#using-the-package-manager

Kevin Buzzard (May 20 2018 at 21:18):

I am really grateful for your work by the way, and maybe @Patrick Massot will be even more grateful -- Patrick maybe this solves some of your nat woes?

Patrick Massot (May 21 2018 at 09:18):

I hope it can help me. I need to find some time to try it.

Patrick Massot (May 21 2018 at 09:18):

Maybe I'm not trying very hard to find this time because I'm afraid I'll be disappointed

Patrick Massot (May 21 2018 at 10:17):

Any hint about how to actually import that cooper thing?

Patrick Massot (May 21 2018 at 10:18):

I tried leanpkg add skbaek/qelim and then import

Patrick Massot (May 21 2018 at 10:18):

I tried adding a leanpkg.toml to it

Patrick Massot (May 21 2018 at 10:18):

But import lia.cooper.main doesn't work

Patrick Massot (May 21 2018 at 10:36):

@Mario Carneiro Did you manage to import this tactic?

Mario Carneiro (May 21 2018 at 10:37):

I haven't attempted it, no

Mario Carneiro (May 21 2018 at 10:38):

You could just copy the files into your project

Patrick Massot (May 21 2018 at 10:40):

Then all mathlib imports fail...

Patrick Massot (May 21 2018 at 10:40):

I guess we need to wait a bit more until this can be tested

Seul Baek (May 28 2018 at 19:02):

I figured out what was wrong and added a .toml file. Now you can install and use the repo using leanpkg.

Johan Commelin (May 28 2018 at 19:42):

This is cool!

Johan Commelin (May 28 2018 at 19:42):

Is it planned to merge this into mathlib? Or will it remain a separate lib?

Johan Commelin (May 28 2018 at 19:42):

I'm not sure what the planning is in general: a monolithic lib, or distributed libs

Patrick Massot (May 28 2018 at 20:13):

@Seul Baek Do you have any example of use? I can now import the lib, but haven't yet managed to proved anything using Cooper

Patrick Massot (May 28 2018 at 20:31):

actually I can prove stuff about integers (that ring also proves), so maybe I misunderstood the scope of this tactic. I thought it would work on natural numbers

Patrick Massot (May 28 2018 at 20:32):

With nat I always get type error at eval_expr, argument has type ℕ but is expected to have type ℤ

Mario Carneiro (May 28 2018 at 20:36):

The core tactic is designed to work on int. There are some missing preprocessing steps to prove natural number theorems

Mario Carneiro (May 28 2018 at 20:37):

Of course a nat quantifier is the same as an int quantifier with the additional assumption 0 <= n

Patrick Massot (May 28 2018 at 20:37):

What do you get in addition to ring then?

Mario Carneiro (May 28 2018 at 20:37):

I think Seul's tactic is still more of a backend thing

Mario Carneiro (May 28 2018 at 20:38):

it needs a front end to generalize and revert quantifiers, and convert nats to ints

Patrick Massot (May 28 2018 at 20:39):

Do you know whether he's working on this?

Mario Carneiro (May 28 2018 at 20:39):

ring will not be able to prove that \forall n : int, n <= 0 \/ n >= 1 for example

Mario Carneiro (May 28 2018 at 20:39):

Or 3 | n -> 5 | n -> 15 | n

Mario Carneiro (May 28 2018 at 20:40):

or 3 | n -> n > 0 -> n*n - n > 0

Mario Carneiro (May 28 2018 at 20:41):

oh wait actually that last one might not work because of the square

Patrick Massot (May 28 2018 at 20:41):

This sounds pretty nice

Mario Carneiro (May 28 2018 at 20:42):

but more importantly, it allows full quantifier alternation

Patrick Massot (May 28 2018 at 20:42):

But Lean doesn't let me state the divisibility stuff

Mario Carneiro (May 28 2018 at 20:42):

type 3 \| n

Patrick Massot (May 28 2018 at 20:43):

Oh, Johan will like this unicode trickery

Patrick Massot (May 28 2018 at 20:44):

example  : ∀ (n : ℤ), (3 ∣ n) → (5 ∣ n) → (15 ∣ n) :=
by cooper

doesn't work though

Mario Carneiro (May 28 2018 at 21:10):

looking at the code, it's pretty sparse on extended syntax

Mario Carneiro (May 28 2018 at 21:11):

you have to use exists ~~and forall~~ and times and le

Mario Carneiro (May 28 2018 at 21:11):

I'm not even sure equality is supported

Mario Carneiro (May 28 2018 at 21:11):

so you would have to write \ex k, 3 * k <= n /\ n <= 3 * k instead of 3 | n

Kenny Lau (May 28 2018 at 21:14):

I thought everything is decidable

Seul Baek (May 28 2018 at 21:14):

@Johan Commelin I'm not sure what'd be the best way to integrate this to other libraries in the long term. It'll stay separate for the short term for convenience of further development.

Mario Carneiro (May 28 2018 at 21:15):

actually I take it back, forall is also not supported

Mario Carneiro (May 28 2018 at 21:15):

you have to use negation and exists

Seul Baek (May 28 2018 at 21:18):

@Patrick Massot It should definitely be possible to write a preprocessor for nat, although I'm not working on it at the moment. I'm trying to first replace int with znum to improve efficiency.

Seul Baek (May 28 2018 at 21:22):

@Mario Carneiro forall and equality are indirectly supported by the rewriting step before calling the main quantifier elimination tactic. E.g., cooper_vm works for forall (x: int), exists (y : int), x = 1 + y

Mario Carneiro (May 28 2018 at 21:24):

oh, I see it

Mario Carneiro (May 28 2018 at 21:24):

I guess you should add the definition of dvd in that list

Seul Baek (May 28 2018 at 21:28):

You mean the list of indirectly supported relations?

Mario Carneiro (May 28 2018 at 21:28):

yes

Mario Carneiro (May 28 2018 at 21:28):

as a simp lemma in the preprocessing

Mario Carneiro (May 28 2018 at 21:29):

something like a | b <-> ∃ c, b = a * c

Mario Carneiro (May 28 2018 at 21:29):

surprisingly not stated as a theorem that I can see, but easy to prove by refl

Seul Baek (May 28 2018 at 21:32):

Yes, I think it should be possible to do this even more directly (w/o preprocessing), since the internal syntax already includes dvd

Patrick Massot (May 29 2018 at 08:46):

Thanks Seul and Mario. I'll wait a bit more then (a tactic handling ℕ crazyness is what I really need).

Kevin Buzzard (May 29 2018 at 11:22):

surprisingly not stated as a theorem that I can see, but easy to prove by refl

Hey wait a minute! I asked for the name of a theorem recently (if a structure is made with a : A and b : B then (structure.mk a b).a = a) and you said "oh that's true by refl so it doesn't have a name"

Kevin Buzzard (May 29 2018 at 11:23):

What's the algorithm for determining whether an equality whose proofs is rfl gets blessed with a name?

Mario Carneiro (May 29 2018 at 11:31):

It doesn't usually matter, Seul is writing a tactic so he needs to have names for his automation. It's fine even if he just declares a local theorem with a particular statement he can rely on.

Mario Carneiro (May 29 2018 at 11:32):

For example there are lots of theorems in tactic.ring that are like this - they have very particular statements to make it easy for the automation, but no one would ever use those theorems otherwise