groebner basis algorithm

Stream: maths

[Jalex Stark]

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]

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

[Yury G. Kudryashov]

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]

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]

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]

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

[Yury G. Kudryashov]

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]

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]

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

[Alex J. Best]

@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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Rob Lewis]

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]

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

[Kevin Buzzard]

I guess this shouldn't be in mathlib?

[Kevin Buzzard]

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

[Rob Lewis]

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]

It's similar to worries about #1083

[Kevin Buzzard]

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]

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]

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

[Johan Commelin]

Or sage.groebner

[Rob Lewis]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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

[Kevin Buzzard]

rofl

[Mario Carneiro]

@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]

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]

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]

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

[Rob Lewis]

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]

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
the right answer
-/

[Kenny Lau]

thanks for the explanation; that makes it very clear

[Kevin Buzzard]

I never know if you are being sarcastic ;-)

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

But your ring++ specification didn't have this

[Mario Carneiro]

that is true

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

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]

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

[Kevin Buzzard]

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]

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]

because I can write sage code from there

[Mario Carneiro]

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]

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]

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

[Kevin Buzzard]

oh but they're just obvious ;-)

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

We see it in the wild all the time

[Mario Carneiro]

the lean wild

[Mario Carneiro]

same with nat equalities

[Kevin Buzzard]

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

[Kevin Buzzard]

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?

[Mario Carneiro]

Sure you do

[Kevin Buzzard]

Oh OK I stand corrected!

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

except that we can move to int

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

Now that I don't know.

[Mario Carneiro]

In particular does it need additional hypotheses on the semiring

[Kevin Buzzard]

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

[Mario Carneiro]

that's... bad, right?

[Kevin Buzzard]

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]

Mario Carneiro said:

that's... bad, right?

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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

[Mario Carneiro]

it's also not even cancellative

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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,
  rw [mul_add, mul_add] at h1,
  linarith,
end

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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