Ring-normalization in linarith

Stream: mathlib4

[Heather Macbeth]

I noticed that the current implementation of linarith effectively ring-normalizes twice.

Example: suppose we are running the core method docs#Linarith.proveFalseByLinarith on the comparisons-with-zero y * (x + z) < 0, 1 - y * x < 0, - z * y < 0.

First this list is sent through the method docs#Linarith.linearFormsAndMaxVar, which parses each LHS as a linear combination of monomials in atoms -- here the atoms are x, y, z and the monomials which appear are 1, x * y and y * z, so we get (<, [0, 1, 1]), (<, [1, -1, 0]), (<, [0, 0, -1]) . This method is basically a custom, proof-free implementation of ring within the linarith tactic code.

Then later, once the oracle has returned the right combination of these inequalities to produce a contradiction, 1 * (y * (x + z)) + 1 * (1 - y * x) + 1 * (- z * y) < 0, the tactic ring is run directly on the LHS (to check that it ring-normalizes to zero).

[Heather Macbeth]

@Rob Lewis @Mario Carneiro Did you ever consider sharing more code between ring and linarith? One could use ring directly for the parsing of each LHS in linearFormsAndMaxVar, saving the proofs, and then adapt the final ring call so that it used this information -- do you have an estimate of how much this might improve performance?

[Mario Carneiro]

this could be improved by having linarith call the ring internal function rather than the frontend on that contradiction

[Heather Macbeth]

(Cross-ref: Pretty sure this discussion between Rob and Mario is contemporary with the existing implementation)

[Heather Macbeth]

Mario Carneiro said:

this could be improved by having linarith call the ring internal function rather than the frontend on that contradiction

That makes sense, but I think what I was trying to propose is different? Namely, you could save the list of normalized LHSs as docs#Mathlib.Tactic.Ring.ExSum objects, and then the final normalization step only consists of a single layer of docs#Mathlib.Tactic.Ring.evalMul and a single layer of docs#Mathlib.Tactic.Ring.evalAdd.

[Mario Carneiro]

yes we're saying the same thing; skip the call to eval and instead call the internal functions

[Mario Carneiro]

meaning that you would be storing atoms as ExProd objects most likely (not ExSum since linarith breaks down the additive structure of expressions)

[Heather Macbeth]

Ah, got it, I thought you were just proposing to switch from the current method (calling evalTactic (← `(tactic| ring1)) on a generated stuff = 0 goal) to directly calling docs#Mathlib.Tactic.Ring.eval ... which might indeed save a bit of time but not as much

[Mario Carneiro]

(I think they would also be monic monomials but ring doesn't have a dedicated type for that)

[Mario Carneiro]

It might be problematic that ring is strongly typed and linarith is not as much

[Heather Macbeth]

I think there's already a step where linarith groups hypotheses by their ambient type, so you could keep around the type information from that step onwards.

[Heather Macbeth]

Anyway ... any estimate of how much this deduplication might affect performance?

[Mario Carneiro]

not really, it could be significant but probably not too much

[Mario Carneiro]

There are some expensive steps in the part that would be skipped here, like defeq checking every subterm against every atom

[Heather Macbeth]

By "skipped here" do you mean in the "before" or the "after"?

[Mario Carneiro]

after

[Mario Carneiro]

the delta is the running of the match expression in eval, which is moderately expensive because it calls into lean unification

[Mario Carneiro]

whether it dominates the run time or not depends a lot on the goal itself

[Mario Carneiro]

it can be the most expensive part if you have a lot of definitions that are expensive to compare

[Heather Macbeth]

It also has to ring-normalize twice, right? So if say (x + y) ^ 4 appears and it has to expand that out twice (once without proof and once with proof), shouldn't that also be expensive?

[Mario Carneiro]

ah that's true, ring doesn't cache subterm evaluation, maybe it should

[Mario Carneiro]

and doing this would indeed skip that cost

[Heather Macbeth]

But would that help? In the current implementation, the first time of expanding out is done by linarith's internal "ring-like" function, not by ring itself.

[Mario Carneiro]

well with your proposal linarith would call ring's normalization function on each atom early in the process

[Mario Carneiro]

on the other hand, maybe that's wasted work if the atom doesn't participate in the final contradiction

[Heather Macbeth]

Ah, good point!

[Mario Carneiro]

you could have a thunk there to compute it lazily but not recompute it

[Heather Macbeth]

At that point, I guess you have to re-implement ring too, to be flexible to whether you want a proof-ful or proof-less ring call.

[Mario Carneiro]

how do you figure?

[Heather Macbeth]

Hmm, did I misunderstand your proposal?

[Mario Carneiro]

For each atom, you would store it as an expression as currently, but also store a function to compute it to an ExProd on demand and cache the result

[Mario Carneiro]

or just work it out manually with an Option ExProd

[Heather Macbeth]

By "atom" you mean what linarith calls a "monomial", right? Like x^3 * y or x * y * z -- so an atom for linarith but not an atom for ring?

[Mario Carneiro]

yes

[Heather Macbeth]

I guess I was thinking that there are expensive parts even before you get to monomials: expanding (x + y) ^ 4 into monomials (even before normalizing those monomials) would be expensive, right?

[Mario Carneiro]

hm, when does that happen currently?

[Mario Carneiro]

Oh, I guess my assertion was false, linarith atoms are in general ExSum not ExProd because of things like that

[Heather Macbeth]

https://github.com/leanprover-community/mathlib4/blob/e8818a7d64e68e8ecc8c15bafc7964cb471fd2fb/Mathlib/Tactic/Linarith/Parsing.lean#L158

[Heather Macbeth]

I think linarith does the expanding out into "monomials" (which are effectively ExProds) and then runs the oracle using those as the atoms.

[Mario Carneiro]

but if you had (x + y) ^ 4 in a linarith goal, it would treat it as an atom, no?

[Mario Carneiro]

it would not be expanded until it got to ring

[Mario Carneiro]

and in fact it should probably never be expanded, since linarith has reason to believe it has a contradiction without expanding it

[Heather Macbeth]

No, IIUC it is treated as a linear combination of the atoms x^4, x^3y, x^2y^2, etc.

[Heather Macbeth]

import Mathlib

example (x y : ℝ) (h1 : (x + y) ^ 2 = 10) (h2 : (x - y) ^ 2 = 6) : x * y = 1 := by linarith

[Mario Carneiro]

interesting

[Mario Carneiro]

okay so I take back my assertion that my previous assertion was false

[Mario Carneiro]

it does make you wonder if that function couldn't just be eval itself

[Mario Carneiro]

unfortunately linarith hasn't gotten much love in a while, it's pretty much just a direct port of the lean 3 version, while ring was a complete rewrite

[Mario Carneiro]

Now I am remembering that we had plans for a sum of squares tactic in bonn that didn't go anywhere :(

[Heather Macbeth]

Mario Carneiro said:

unfortunately linarith hasn't gotten much love in a while, it's pretty much just a direct port of the lean 3 version, while ring was a complete rewrite

Yes, I've been looking a bit more closely at it since I want to share some code between it and linear_combination-for-inequalities. There are a few other places where I have (naive?) questions about the implementation -- like, for example, there's a lot of mkApp .... and I wonder about switching all that stuff over to q(...).

[Mario Carneiro]

yes I would like to do that, it's just a lot of code and by the time it was ported it was too late to suggest starting afresh

[Kim Morrison]

Never too late to start afresh. :-)

[Kim Morrison]

I wish we didn't use identifying-atoms-up-to-defeq, which is potentially super slow, and just ran CanonM.

[Kim Morrison]

Much better performance, and not much loss of capability.

[Mario Carneiro]

Why not make CanonM have a reducibility flag? I'd be happy to switch the default but I don't want to sacrifice the capability

[Kim Morrison]

It does already, see CanonM.run'.