Updated `ring_exp` paper

Stream: general

[Anne Baanen]

I've been updating the short paper on ring_exp, now it should be (almost) ready to submit to Springer. The latest version is available here: https://www.cs.vu.nl/~tbn305/publicaties/2020-ring_exp.pdf I'm very grateful to the Lean community for the help they have already given. If you have time to read it this week, I would really appreciate any feedback.

[Kevin Buzzard]

+1 for using 37 as an example of a nat.

[Kevin Buzzard]

I don't understand why you bother telling people that on random expressions ring_exp is slower; I have consistently found ring_exp to be faster. I'm writing a proof right now which uses ring and I just tried replacing it with ring_exp and there is a 30% speed-up. My experience with ring_exp on highly non-random examples is extremely positive and so you might want to mention that there is anecdotal evidence that it is performing better in practice with single-variable polynomial calculations of degree 3 or more, which is what often comes up in my work.

[Kevin Buzzard]

Last (silly) comment -- in the last-but-one sentence of the paper it sounds like you are accusing Gabriel etc of being the anonymous reviewers :-) You could put "Gabriel Ebner, ..., and the anonymous reviewers read this paper..." to avoid this ambiguity.

[Kevin Buzzard]

Do you have any time to do a test suite of random expressions in one variable with degrees between 3 and 10?

[Bryan Gin-ge Chen]

Some minor typos:

On page 2:

The ring_exp tactic does not use reflection but directly constructs proof terms to type checked by Lean’s kernel,

On page 6:

on linear expressions such as passed by linarith, ring_exp is 1.67 times slower than ring.

[Anne Baanen]

Kevin Buzzard said:

I don't understand why you bother telling people that on random expressions ring_exp is slower; I have consistently found ring_exp to be faster. I'm writing a proof right now which uses ring and I just tried replacing it with ring_exp and there is a 30% speed-up. My experience with ring_exp on highly non-random examples is extremely positive and so you might want to mention that there is anecdotal evidence that it is performing better in practice with single-variable polynomial calculations of degree 3 or more, which is what often comes up in my work.

It doesn't seem as uniformly positive to me. My own anecdotal evidence is that it's easy to find worse performance for either tactic in practice. Visually looking through the benchmark output, ring seems to be not too much worse than ring_exp when it loses the race, compared to ring_exp losing by a lot when it does. So ring_exp is about 30% faster than ring on showing (1 + x + x^2 + x^3 + x^4) * (x - 1) = x^5 - 1, but 4 times slower than ring on showing (x - 1)^4 = (1 - x)^4 (I think because (a + b)^4 is unfolded into a bunch of multiplications, which ring tends to be faster at).

[Kevin Buzzard]

OK, then maybe what you have is fine.

[Anne Baanen]

Thank you for the benchmark suggestion. With a fixed degree, ring_exp seems to catch up somewhat to ring. I will let it run for a couple of hours to compare the distributions.

[Mario Carneiro]

Just an FYI, but I have some work optimizing ring in progress. The plan is to back port all the performance tricks used in ring_exp to ring, and if possible see what can be done to merge the two without performance regression

[Kevin Buzzard]

Could one mention this in the paper? The work has inspired other work etc