Stream: maths

Topic: groebner basis algorithm

Jalex Stark (May 11 2020 at 21:28):

I don't really know what a groebner basis algorithm is, except that

1. it's a generalization of the ring tactic and

2. sage has an implementation that is fast enough to be useful to people doing exploratory mathematics

question: does the grobner basis method produce small witnesses checkable by ring? if so, can we get ring++ in Lean by "just" shelling out to an oracle?

Yury G. Kudryashov (May 11 2020 at 21:45):

Yes, this is possible but you need to understand what elements of the coefficients ring are equal to zero.

Yury G. Kudryashov (May 11 2020 at 21:47):

Coq has a per-field/ring set of tactics that deal with coefficients, and this set of tactics is used by ring, field, and groebner (not sure about exact names).

Alex J. Best (May 11 2020 at 21:49):

I've also had this thought, I think this is a really achievable goal, what's needed is enough of the theory to give Buchberger's criterion, this should be enough that lean can check the witness, then Sage or Singular can be called to produce a basis.

Yury G. Kudryashov (May 11 2020 at 21:51):

If all we want is a tactic that solves a goal $P_1(x_1, \dots, x_n) = 0, \dots, P_k(x_1, \dots, x_n)=0 \vdash Q(x_1, \dots, x_n)=0$, then we don't need any theory to check the witness.

Yury G. Kudryashov (May 11 2020 at 21:54):

Because the witness has a form $R(P_1, \dots, P_k)=Q^m$.

Yury G. Kudryashov (May 11 2020 at 21:55):

On the other hand, it would be nice to have a function that verifies is_groebner_basis predicate but this can be postponed.

Kevin Buzzard (May 11 2020 at 22:09):

Yes this is a job which would be perfect for an external solver like sage and it would not surprise me at all if @William Stein could help. @Rob Lewis set this up with Mathematica before, right?

Kevin Buzzard (May 11 2020 at 22:09):

The "normal"algebra package finds a relation and then ring formally checks it

Alex J. Best (May 11 2020 at 22:10):

@Gabriel Ebner's hammer project would also be a good template for calling an external program, parsing the result into lean and then doing something with it I think.

Alex J. Best (May 11 2020 at 22:15):

It would be great to have a Sage link, but I think for this purpose calling one of the underlying libraries of Sage to calculate groebner bases might be simpler (and faster) to begin with.

Anne Baanen (May 12 2020 at 08:30):

Some people at the VU have worked on Gröbner bases a while back, but I believe it's dormant now. I'll ask about the current state and see if they want to share the work in progress.

Kenny Lau (May 12 2020 at 08:32):

every project not PR'd into mathlib is lost in time

Kevin Buzzard (May 12 2020 at 08:59):

Do you know if they were actually implementing the algorithm in Lean? Because this is one of these situations where a result is far easier to check than to discover, the discovering might be best left to an external program

Rob Lewis (May 12 2020 at 09:02):

The project at the VU did implement the algorithm in Lean, but I think resurrecting it will be a big challenge.

Rob Lewis (May 12 2020 at 09:03):

Doing this with an external computation is totally reasonable. The problem is, how do we integrate that into mathlib? Do we make Sage a dependency for compiling the library?

Rob Lewis (May 12 2020 at 09:03):

Who wants to stay up to date on compatibility with different OSs, Python versions, Sage versions, ...?

Kevin Buzzard (May 12 2020 at 09:04):

I guess this shouldn't be in mathlib?

Kevin Buzzard (May 12 2020 at 09:04):

Or the tactic should just break if the dependency isn't there?

Rob Lewis (May 12 2020 at 09:04):

We don't need to leave calls to Sage in the library, so maybe it's not a requirement to compile. But there's still some presumption that if the tactic is available someone keeps it working.

Rob Lewis (May 12 2020 at 09:05):

It's similar to worries about #1083

Kevin Buzzard (May 12 2020 at 09:06):

This is one of these tactics like library_search where you run it once and it says "type this instead" and whoever types this instead doesn't need sage

Rob Lewis (May 12 2020 at 09:07):

Right, but if you want to run it once, you do need Sage, so a lot of people are going to show up on this chat asking "why doesn't groebner work for me?"

Johan Commelin (May 12 2020 at 09:08):

Maybe if we call it groebner_sage we will get less of those questions?

Johan Commelin (May 12 2020 at 09:08):

Or sage.groebner

Rob Lewis (May 12 2020 at 09:09):

Again, it's the same situation as #1083 or sledgehammer or anything with external dependencies. I'm not saying don't do it. Just make sure it's worth the support costs.

Rob Lewis (May 12 2020 at 09:09):

/ know who's tasked with supporting it and what they're willing to help with.

Mario Carneiro (May 12 2020 at 09:15):

I think the first step is to write the ring ++ tactic that can be used as the target for these groebner calls

Mario Carneiro (May 12 2020 at 09:19):

I'm imagining an interface like ring [(x + y, h1), (z, <- h2)] which checks that if the goal is a = b and h1 : l1 = r1 and h2 : l2 = r2, then a - (x + y) * l1 - z * r2 = b - (x + y) * r1 - z * l2 is an equality in commutative rings

Mario Carneiro (May 12 2020 at 09:21):

Importantly, you don't need sage to use this tactic; in many instances it is perfectly within the ability of the user to come up with coefficients making the invocation work

Kevin Buzzard (May 12 2020 at 09:24):

Wow, this looks like a much easier endeavour and Mario is absolutely right, in many cases the user will be able to solve for the coefficients by themselves. And in the manual it could say "if you are lazy and don't want to work out the coefficients of h1 and h2 yourself, then type "sage.ring_hint" and cut and paste the resulting code into sage, and then cut and paste the output of the sage code back into Lean" :-)

Chris Hughes (May 12 2020 at 09:27):

Even if you do need sage, can sage not just return a certificate that can be passed as an argument to the tactic?

Chris Hughes (May 12 2020 at 09:28):

So there's one version that interfaces with sage and one that just asks for the certificate.

Mario Carneiro (May 12 2020 at 09:28):

yes, but if the replacement tactic is so arcane that it can't be used directly, then you still need to use sage to construct the proof

Kevin Buzzard (May 12 2020 at 09:29):

In @Daniel Fabian 's example from yesterday, he had

h1 : f (2 * (a + k)) + 2 * f (l - a) = f (f (k + l)),
h2 : f (2 * (b + k)) + 2 * f (l - b) = f (f (k + l))
⊢ 2 * (f (l - a) - f (l - b)) = f (2 * (b + k)) - f (2 * (a + k))


and ring++ [(1,h1),(1,<-h2)] would do it, as would ring++ [(1,h1),(-1,h2)] (note in particular that there is no need for <- I guess). The fact that these numbers are +-1 is why linarith solved it, but in general they won't be.

Mario Carneiro (May 12 2020 at 09:30):

the back arrow (and the subtractions in my gloss of what they mean) are to support semirings

rofl

Mario Carneiro (May 12 2020 at 09:31):

@Chris Hughes for example, if you are a maintainer and are fixing a broken proof, and the certificate no longer works, you need to have sage to regenerate the proof

Chris Hughes (May 12 2020 at 09:39):

If you were fairly strict about how to use it, then it might be okay. As in you always used it as have _ : by groebner [certificate], then the proofs would be fairly stable

Rob Lewis (May 12 2020 at 09:39):

If this is implemented, it would be great if the Sage call could fall back to a Lean implementation. Try the fast one first, but if Sage isn't there, do it natively. A rudimentary meta groebner basis algorithm isn't crazy hard.

Mario Carneiro (May 12 2020 at 09:45):

how expensive is FFI to sage/mathematica? Is it possible that the lean version will win for not being "external"?

Rob Lewis (May 12 2020 at 09:47):

It depends how much effort you put into the architecture of both. Sage and Mathematica are both very expensive to start up. If you don't have a server running, the native version will probably win for small problems, especially if you do a decent job implementing it.

Kevin Buzzard (May 12 2020 at 09:57):

In case there are any people who don't really know what Groebner bases are, here is a summary of what is going on.

import tactic

example (a b : ℤ) (h1 : a^2 = b^2) (h2 : a^3=b^4) : a^8=b^10 :=
begin
-- proof which contains a human-generated mathematical idea
rw (show a^8 = a^2 * a^3 * a^3, by ring),
rw h1,
rw h2,
ring -- note ring called twice, once to implement the idea and once to finish the job
end

-- the Commelin-Barton trick
@[reducible] def eq.lhs {α : Type*} {x y : α} (e : x = y) : α := x
@[reducible] def eq.rhs {α : Type*} {x y : α} (e : x = y) : α := y

example (a b : ℤ) (h1 : a^2 = b^2) (h2 : a^3 = b^4) : a^8 = b^10 :=
begin
-- "the same" human-generated idea, in a different format
suffices : a^8  + a^6*h1.rhs + b^6*h2.rhs + a^3*b^2*h2.rhs =
b^10 + a^6*h1.lhs + b^6*h2.lhs + a^3*b^2*h2.lhs,
{ rw (show eq.lhs h1 = eq.rhs h1, from h1) at this,
rw (show eq.lhs h2 = eq.rhs h2, from h2) at this,
simp at this, exact this}, -- note: no ring needed
unfold eq.lhs eq.rhs,
ring,
end

example (a b : ℤ) (h1 : a^2 = b^2) (h2 : a^3 = b^4) : a^8 = b^10 :=
begin
-- the above script, all packed into a tactic
ring++ [(a^6, ←h1), (b^6+a^3*b^2, ←h2)]
-- doesn't work yet though
end

/-
The underlying question: Let R be the ring ℤ[A,B] and let I be the ideal (A^2-B^2,A^3-B^4).
Is A^8-B^10 in I? Yes it is, because it's A^6(A^2-B^2)+(A^3B^2+B^6)(A^3-B^4)

The point is a computer algebra package such as SAGE could find the representation of A^8-B^10
and then ring++ can just take the inputs and check that the computer algebra package gave
-/


Kenny Lau (May 12 2020 at 10:00):

thanks for the explanation; that makes it very clear

Kevin Buzzard (May 12 2020 at 10:00):

I never know if you are being sarcastic ;-)

Mario Carneiro (May 12 2020 at 10:00):

your proof is a bit unexpected. I would have expected something akin to h1 * h2 * h2

Mario Carneiro (May 12 2020 at 10:01):

I guess this is part of the grobner basis idea that this can be written as a linear function of the h's

Kevin Buzzard (May 12 2020 at 10:01):

Yes, the problem is that to prove (h2.lhs)^2=(h2.rhs)^2 you have to write 0 as a difference of two squares and observe that one of the factors is zero

Kevin Buzzard (May 12 2020 at 10:02):

b^6+a^3b^2=b^2(b^4+a^3) which is the LHS+RHS factor for h2.

Mario Carneiro (May 12 2020 at 10:02):

but that's not true, right? I mean h2.lhs^2 = h2.rhs^2 follows trivially from h2.lhs = h2.rhs

Kevin Buzzard (May 12 2020 at 10:03):

But your ring++ specification didn't have this

that is true

Kevin Buzzard (May 12 2020 at 10:03):

I could only subtract c*h1.lhs and c*h1.rhs, but I know how all this works in practice so I just worked around it

Mario Carneiro (May 12 2020 at 10:03):

I was thinking abot being able to write some equation like h1 * h2 * h2 where it means what you think it means

Mario Carneiro (May 12 2020 at 10:04):

If ring++ is to be a human usable tactic, I think it should probably allow such things even if they aren't strictly required for the ideal membership problem

Kevin Buzzard (May 12 2020 at 10:05):

If you're happy with more work for you, that's great. I'm observing that ring++ in the form you proposed seems to me to be writable in a small amount of code and provides a tool which looks like it might already be really useful.

Mario Carneiro (May 12 2020 at 10:06):

I believe that a grobner basis algorithm will always produce a certificate which is a linear function of the hypotheses

Kevin Buzzard (May 12 2020 at 10:06):

It should be easy to write the Sage code which turns (h1 : a^2 = b^2) (h2 : a^3 = b^4) : a^8 = b^10 into  ring++ [(a^6, ←h1), (b^6+a^3*b^2, ←h2)]

Kevin Buzzard (May 12 2020 at 10:08):

You are proposing making something easier for humans to use, and of course the easier it is for humans to use the better, but what has dawned on me is that even this "stupid" version of ring++ where there is no syntax for being able to add h1.lhs*h3.rhs^2 to one side and h1.rhs*h3.lhs^2 to the other, is still something which has got far more power than I had realised.

Kevin Buzzard (May 12 2020 at 10:09):

because I can write sage code from there

Mario Carneiro (May 12 2020 at 10:10):

I think another way to think about the coefficients you got is to successively rewrite a^2 * a^3 * a^3 = b^2 * a^3 * a^3 = b^2 * b^4 * a^3 = b^2 * b^4 * b^4. Each equality is a coefficient times one of the hypotheses, and the chaining is adding the functions together, so you get a linear combination in the end

Kevin Buzzard (May 12 2020 at 10:22):

I think that what's happening now is that you are interested in making some kind of better, or easier-to-use algorithm, but this is not the kind of thing I know anything about; I can already see the path to enlightenment and it uses external forces which I have (computer algebra packages), so as far as I am concerned the problem is solved.

Mario Carneiro (May 12 2020 at 10:33):

rather, I'm reverse engineering where you got those constants since they weren't in the first version of the proof

Kevin Buzzard (May 12 2020 at 10:34):

oh but they're just obvious ;-)

Kevin Buzzard (May 12 2020 at 10:34):

The second rewrite is really two rewrites. I am doing them separately

Kevin Buzzard (May 12 2020 at 10:34):

The first changes $a^6a^2$ into $a^6b^2$

Mario Carneiro (May 12 2020 at 10:34):

as for making ring ++, there is no real added difficulty in multiplying equations compared to adding them. Especially if you give the remainder term, this is pretty trivial and you can have the equations under arbitrary functions

Kevin Buzzard (May 12 2020 at 10:35):

the second changes $a^6b^2$ into $a^3b^6$ and the third changes that to $b^{10}$. I guess I wrote them in a different order though.

Mario Carneiro (May 12 2020 at 10:36):

actually, the version I proposed might still not be sufficient for semirings unless you include transitivity

Kevin Buzzard (May 12 2020 at 10:36):

I am too unimaginative to imagine the syntax for "now add h1.L*h3.R^2 to one side and h1.R*h3.L^2 to the other"

Mario Carneiro (May 12 2020 at 10:37):

I am just thinking about literally writing ring h1 * h2 * h2

Kevin Buzzard (May 12 2020 at 10:38):

Of course I personally don't care about semirings. If I ever have an equality between naturals which I want to prove, then I can embed it into the integers and prove it there, and if it uses subtraction then I already did something wrong (I didn't embed into the integers early enough).

Kevin Buzzard (May 12 2020 at 10:38):

Nat subtraction does not exist in maths so you never see it in the wild

Mario Carneiro (May 12 2020 at 10:38):

We see it in the wild all the time

the lean wild

Mario Carneiro (May 12 2020 at 10:39):

same with nat equalities

Kevin Buzzard (May 12 2020 at 10:39):

Now we have norm_cast I just move between nat and int freely.

Kevin Buzzard (May 12 2020 at 10:39):

Yeah you see nat subtraction in CS Lean, but in CS lean you surely don't see complicated Groebner bases questions? omega will do for you, right?

Sure you do

Kevin Buzzard (May 12 2020 at 10:40):

Oh OK I stand corrected!

Mario Carneiro (May 12 2020 at 10:40):

That problem that you used in the example could just as easily have been on nat

Kevin Buzzard (May 12 2020 at 10:40):

Sure, but it's not a problem a computer scientist needs to solve when they're verifying that their code has no bugs

Kevin Buzzard (May 12 2020 at 10:40):

whereas it's the sort of thing which comes up all the time in number theory

Kevin Buzzard (May 12 2020 at 10:41):

except that we can move to int

Mario Carneiro (May 12 2020 at 10:41):

I know for a fact that linear arithmetic comes up all the time, and this is essentially the equality version

Kevin Buzzard (May 12 2020 at 10:42):

but you already have linarith, which Patrick observed solved Daniel Fabian's question.

Mario Carneiro (May 12 2020 at 10:42):

Do we have a generic construction for putting negation in a semiring?

Kevin Buzzard (May 12 2020 at 10:43):

You mean localising it? I think that @Amelia Livingston has worked her socks off with this.

Kevin Buzzard (May 12 2020 at 10:43):

although she is in the middle of UG maths exams now (like Chris)

Mario Carneiro (May 12 2020 at 10:43):

is it good enough to be used behind the scenes by ring ++?

Kevin Buzzard (May 12 2020 at 10:44):

Now that I don't know.

Mario Carneiro (May 12 2020 at 10:44):

In particular does it need additional hypotheses on the semiring

Kevin Buzzard (May 12 2020 at 10:44):

The map from the semiring to its ringification won't be injective in general

Kevin Buzzard (May 12 2020 at 10:49):

Mario Carneiro said:

I am just thinking about literally writing ring h1 * h2 * h2

My example is too superficial perhaps. In general life won't be as easy as this.

Kevin Buzzard (May 12 2020 at 10:50):

Mario Carneiro said:

Well the question as to whether a computer scientist cares about a non-ring semiring whose map to its ringification is not injective is one for which I'd be surprised to hear that the answer was "yes", but you already surprised me once.

Mario Carneiro (May 12 2020 at 10:50):

Isn't it though? At least for everything covered by grobner basis algorithm it is ring a * h1 + b * h2.symm and so on

Kevin Buzzard (May 12 2020 at 10:50):

Yes, but we just got lucky that the goal literally was h1h2^2

Mario Carneiro (May 12 2020 at 10:51):

Well the question as to whether a computer scientist cares about a non-ring semiring whose map to its ringification is not injective is one for which I'd be surprised to hear that the answer was "yes", but you already surprised me once.

The CS problem is not that the map is not injective, but rather that we don't have available the knowledge that the map is injective

Kevin Buzzard (May 12 2020 at 10:53):

example (a b c d e : ℤ) (h1 : a+b = c+d) (h2 : a^2+b^2=c^2+d^2) : a^2-c^2+e*b-e*d=d^2-b^2+e*a-e*c :=


This is the sort of goal I'd really like to be able to dispatch quickly. Goals like this come up annoyingly often.

Kevin Buzzard (May 12 2020 at 10:54):

You have that the map from nat to int is injective. I've seen no coherent argument from you for why to make the tactic work for semirings. If it works for all commutative rings and nat, will the CS people be satisfied? I conjecture that the maths people will.

Kevin Buzzard (May 12 2020 at 10:55):

I wouldn't use it with nat anyway, because if I have a question about nat then I will coerce to int, work there, and coerce back. This will always work for me because I don't do pathological things with naturals like subtract them until I have coerced to int.

Mario Carneiro (May 12 2020 at 10:55):

commutative rings and nat is probably enough? There are also ennreal, enat and a few other examples of semirings that are not commutative rings or nat in mathlib

Kevin Buzzard (May 12 2020 at 10:56):

Oh! I could quite imagine ennreal being something that people might need. This is a nice example.

Mario Carneiro (May 12 2020 at 10:56):

it's also not even cancellative

Kevin Buzzard (May 12 2020 at 10:56):

I never quite know how seriously to take arithmetic in types like ennreal.

Kevin Buzzard (May 12 2020 at 10:56):

Sure it's a really important target type for certain norms

Kevin Buzzard (May 12 2020 at 10:57):

but what one actually does in practice with outputs of norm functions -- I am not so sure that people end up doing complicated polynomial arithmetic with them, or if they did then they might be able to say "if a=infinity then what we actually want to prove is trivial, and if a is finite let's just coerce back into the reals"

Mario Carneiro (May 12 2020 at 10:58):

Here's an interface that would work with semirings: ring_rw [a*h1] tries to find a b such that goal.lhs = a * h1.lhs + b and then rewrites it to a * h1.rhs + b

Mario Carneiro (May 12 2020 at 10:59):

and you can have a sequence of such, and it closes with ring

Kevin Buzzard (May 12 2020 at 11:26):

My example

example (a b c d e : ℤ) (h1 : a+b = c+d) (h2 : a^2+b^2=c^2+d^2) : a^2-c^2+e*b-e*d=d^2-b^2-e*a+e*c :=


is a great example of what is currently hard to do. If h1 : a = F(b,c,d,e) then you can just eliminate all a's with rw h1 and you now have 1 fewer generator. When you're down to 0 generators you've won. With the example you don't have just one variable on one side in either hypothesis so currently you have to start faffing around with various eq_add_iff_sub_eq-type lemmas.

Kevin Buzzard (May 12 2020 at 11:28):

oh hang on, it's also not true (sign error fixed)

Kevin Buzzard (May 12 2020 at 11:29):

example (a b c d e : ℤ) (h1 : a+b = c+d) (h2 : a^2+b^2=c^2+d^2) : a^2-c^2+e*b-e*d=d^2-b^2-e*a+e*c :=
begin
apply_fun (λ x, e*x) at h1,
linarith,
end


This is the sort of hackery I'd come up with for that

Mario Carneiro (May 12 2020 at 11:31):

with ring_rw, I'm imagining that it will make it match, even if it doesn't obviously match. So if you ring_rw [h2] on that goal, a^2-c^2+e*b-e*d turns into (a^2+b^2)-c^2+e*b-e*d-b^2 and then it gets rewritten to (c^2+d^2)-c^2+e*b-e*d-b^2, which it can also simplify if desired.

Mario Carneiro (May 12 2020 at 11:32):

After cancelling factors, the goal generated by ring_rw [h2] might be e*b-e*d=-e*a+e*c

Kevin Buzzard (May 12 2020 at 11:32):

I multiplied one equation by e; if I'd also multiplied the non-linear equation by something it would have been harder to sort out. In general you have to know what factor to multiply by which is what your original ring++ was asking for.

Kevin Buzzard (May 12 2020 at 11:33):

ring_rw [h2] is just like ring++ [(1,h2)]

Mario Carneiro (May 12 2020 at 11:33):

Right, ring_rw [h1] at this point would not solve the goal, it would make a mess, but ring_rw [-e * h1] would work

Mario Carneiro (May 12 2020 at 11:34):

Yes, this is an alternative interface in terms of multiple rewrites instead of linear functions

Kevin Buzzard (May 12 2020 at 11:34):

Yes, I now see that the way you're thinking about it is going to make it far easier for humans to use.

Last updated: May 10 2021 at 08:14 UTC