Do better than `grind`/`grobner`

Stream: general

[Weiyi Wang]

I have a few ideal membership problem that I'd like to verify in Lean, but it seems that they are too large for grind/grobner, or any tactic that I know to handle. I opened https://github.com/leanprover/lean4/issues/11861 for this, which understandably is low priority as a performance enhancement request, but I am still seeking for a solution to my own problem.

One of the lemma I'd like to prove is this one (the same one attached in the issue). I have tried the following

• grind
• Ask sage to verify it, and generate the cofactors for each ideal generator as certificates. However these coefficients are several hundreds of KB long, and it overflows the stack when checking in Lean, even if I raise the stack limit
• Break down the computation into multiple stage and ask sage to reduce the polynomial at intermediate result: the intermediate result is still too long to even state in Lean. Lean hits recursion limit in instance synthesize

So the only way left I can think of is to somehow implement a better grobner basis implementation in Lean for my specialized problem. I know that my polynomials all have integer coefficients, and I can delegate the initial calculation of grobner basis to sage, so I only need to implement the reduction part. How feasible is it to do better, given that I think grind is already very advanced?

The rough implementation idea I have is

• implement an adhoc computable polynomial, possibly just as a list of monomials?
• map arithmetic to polynomial arithmetic
• define the reduction procedure as a program, and prove a theorem that this program doesn't change the ideal membership
• decide (or, native_decide if I have to, which I accept for my own challenging problem) that the polynomial reduces to 0

Does this sound good enough?

[Kim Morrison]

Without using native_decide it is going to be a very challenging problem.

In your linked example, I tried with

set_option maxHeartbeats 0 in
set_option maxRecDepth 10_000 in

and

  grobner (ringSteps := 1_000_000)

after a few cycles of reading grind's diagnostics (in the "Issues" and "Thresholds" sections it tells you which limits to raise), but this still results in a server crash eventually, after consuming more than 128gb of RAM.

[Weiyi Wang]

Got it. I am ok to have native_decide for now. This is just formalizing an old math problem for fun without intention to contribute it to mathlib anyway, and having a solution is better than having a sorry there for personal satisfaction.

[Weiyi Wang]

There might be a way for me to avoid native_decide by verbosely write down the reduction steps. This was what I wanted to do with the third bullet point in my previous attempts. It didn't work because the plan expression in the statements is too long for type class system to handle. I hope that if I encode it into an opaque list it won't invoke the system bypass the limits

[Weiyi Wang]

I already hit the first wall quickly... I'd like to use docs#MonomialOrder to avoid re-inventing the wheel, but it uses Finsupp, which seems ... very noncomputable? I just wanted to convert to my Fin n → ℕ to Fin n →₀ ℕ, using docs#Finsupp.equivFunOnFinite, but that immediately gives me noncomputable error alright that's easy enough to resolve with a one liner Finsupp.mk (Finset.univ.filter (m.exp · ≠ 0)) m.exp (by simp)

[Weiyi Wang]

I guess it is because it uses Finite but not Fintype...

[Niels Voss]

Is the proof too large for the kernel to handle or too large for the elaborator (e.g. tactics, typeclasses, type inference)? If the former, there's not much you can do except to restructure the proof; if the latter, you might be able to just bypass the elaborator completely and only have the kernel check it.

[Weiyi Wang]

For the three attempts I had, I know the third one is in elaborator. The second one might be in elaborator as well (something under the linear_combination tactic). For the first one, grind is too blackboxy for me to think

[Weiyi Wang]

Although I said I accept native_decide, I still want to see how far I can get with kernel. Now I am learning the hard way that it is not easy to make something reducible by kernel, let alone efficiently lol

[Weiyi Wang]

Is the proof too large for the kernel to handle or too large for the elaborator (e.g. tactics, typeclasses, type inference)?

So I think the real answer to this is that it is too large for the kernel. I now have a bare bone computable polynomial implementation, and I let the kernel compute an expression around the same size of my problem. Eventually it hit stack overflow after I raise all the soft limits. I know it is not elaborator problem because I can send the same expression to #eval and compute without problem

[Vlad Tsyrklevich]

Does stack overflow just mean you need to adjust your ulimit -s? I am not familiar with if you're talking about stack memory or some internal stack

[Weiyi Wang]

I hit the same kind of stack overflow message with previous attemp 2 as well. There I tried both setting ulimit and Leans's --tstack option but it didn't help

[Weiyi Wang]

Alright I finally proved my lemma... with native_decide and 3 minutes build time :face_with_peeking_eye:

[Kim Morrison]

Nice! Are there reusable components? It would be great to have an example recorded somewhere for people who need to do large Grobner reductions.

[Weiyi Wang]

I have it uploaded to my current project repo but it's still a mess at the moment. Going tk have some fun optimizing and cleaning up in the following days

[Weiyi Wang]

For whoever searched for this thread, I recorded my first proof of the lemma in the OP here. I am going to learn writing tactics and wrap the scaffolding in a nicer way