## Stream: general

### Topic: bug in linarith

#### Scott Morrison (Nov 02 2022 at 05:22):

While writing tests for the port of linarith to Lean 4, I think I've encountered a bug in the implementation of Fourier-Motzkin elimination in Lean 3, but haven't yet identified what is wrong.

Here's the evidence:

def mathlib3ex : list comp :=
[
⟨ineq.le, [(2, 1), (1, -1)]⟩,
⟨ineq.le, [(3, 1), (1, -1)]⟩,
⟨ineq.le, [(4, 1), (1, -1)]⟩,
⟨ineq.le, [(5, -1), (1, 1)]⟩,
⟨ineq.le, [(6, 1), (4, -1)]⟩,
⟨ineq.le, [(7, 1), (5, -1), (2, -1), (1, 1)]⟩,
⟨ineq.le, [(8, 1), (5, -1), (3, -1), (1, 1)]⟩,
⟨ineq.le, [(9, 1), (8, -1)]⟩,
⟨ineq.le, [(10, 1), (7, -1)]⟩,
⟨ineq.le, [(11, 1), (6, -1)]⟩,
⟨ineq.lt, [(0, -1)]⟩,
⟨ineq.lt, [(11, -1), (10, -1), (9, -1), (5, 3)]⟩
]

def mathlib4ex : list comp :=
[
⟨ineq.le, [(5, -1), (2, 1)]⟩,
⟨ineq.le, [(6, -1), (3, 1)]⟩,
⟨ineq.le, [(7, -1), (1, 1)]⟩,
⟨ineq.le, [(9, -1), (8, 1)]⟩,
⟨ineq.le, [(9, 1), (4, -1)]⟩,
⟨ineq.le, [(9, 1), (8, -1), (7, 1), (4, -1)]⟩,
⟨ineq.le, [(10, -1), (9, 1), (6, 1), (4, -1)]⟩,
⟨ineq.le, [(10, 1), (9, -1)]⟩,
⟨ineq.le, [(11, -1), (5, 1)]⟩,
⟨ineq.le, [(11, 1), (9, -1)]⟩,
⟨ineq.lt, [(0, -1)]⟩,
⟨ineq.lt, [(4, 3), (3, -1), (2, -1), (1, -1)]⟩
]

#eval fourier_motzkin.produce_certificate mathlib3ex 11 -- succeeds, i.e. found a contradiction
#eval fourier_motzkin.produce_certificate mathlib4ex 11 -- fails, i.e. no contradiction found


to the bottom of src/tactic/linarith/elimination.lean (this is in mathlib3), you'll see that we find a contradiction from the first set of inequalities, but not from the second.

(This is available in the branch#linarith_bug.)

However these sets of inequalities are the same, up to renaming variables (and then re-sorting the linear expressions so the terms are in descending order again), and hence should be equisatisfiable!

In pcomp.maybe_minimal there is an implementation of Imbert's first theorem. If we remove this check we successfully find a contradiction in both cases, leading me to suspect that this check has been mis-implemented, but so far I don't see what could be wrong.

(I encountered this problem in the mathlib4 implementation, which is meant to be identical except that for unimportant reasons the variable orders are different; a test was failing that succeeded in mathlib3, and I could minimise to this.)

If anyone, e.g. @Rob Lewis (who implemented linarith in the first place!) or @Reid Barton (who I recall has an implementation of FM elsewhere) has any ideas about what's going on here, that would be very helpful.

#### Reid Barton (Nov 02 2022 at 05:39):

Does that mean that the test in mathlib3 that was succeeding is actually incorrect?

#### Mario Carneiro (Nov 02 2022 at 05:48):

What is the contradiction that was found? Is it actually a contradiction?

#### Mario Carneiro (Nov 02 2022 at 05:51):

#eval do
coeff ← fourier_motzkin.produce_certificate mathlib3ex 11,
tactic.trace coeff.to_list
-- [(11, 1), (9, 1), (8, 1), (7, 1), (6, 1), (5, 1), (4, 1), (3, 1), (2, 1), (1, 1), (0, 1)]


#### Mario Carneiro (Nov 02 2022 at 05:57):

def mathlib3ex : list comp :=
[
⟨ineq.le, [(2, 1), (1, -1)]⟩,
⟨ineq.le, [(3, 1), (1, -1)]⟩,
⟨ineq.le, [(4, 1), (1, -1)]⟩,
⟨ineq.le, [(5, -1), (1, 1)]⟩,
⟨ineq.le, [(6, 1), (4, -1)]⟩,
⟨ineq.le, [(7, 1), (5, -1), (2, -1), (1, 1)]⟩,
⟨ineq.le, [(8, 1), (5, -1), (3, -1), (1, 1)]⟩,
⟨ineq.le, [(9, 1), (8, -1)]⟩,
⟨ineq.le, [(10, 1), (7, -1)]⟩,
⟨ineq.le, [(11, 1), (6, -1)]⟩,
⟨ineq.lt, [(11, -1), (10, -1), (9, -1), (5, 3)]⟩
]

#eval tactic.trace (mathlib3ex.foldl comp.add ⟨ineq.eq, []⟩)
-- []<0


The contradiction seems to be correct

#### Mario Carneiro (Nov 02 2022 at 06:26):

Here's a minimization of the example:

def mathlib4ex : list comp :=
[⟨ineq.le, [(3, -1), (2, 1)]⟩,
⟨ineq.le, [(3, 1), (1, -1)]⟩,
⟨ineq.le, [(3, -1)]⟩,
⟨ineq.lt, [(3, 1), (2, -1), (1, 1)]⟩]

#eval fourier_motzkin.produce_certificate (mathlib4ex.map (λ x, ⟨x.1, list.merge_sort (λ a b, a.1 > b.1) x.2⟩)) 3


changing 3 to 0, or rearranging any of the coefficients (preserving the sum) makes the failure go away

#### Mario Carneiro (Nov 02 2022 at 08:00):

Okay, here's an explanation of what happens in the code. We start out with the initial equations E0, ..., E3:

step 0:
E0: -x2 <= 0: history = {E0}, explicit = {}, implicit = {}
E1: x2 - x0 <= 0: history = {E1}, explicit = {}, implicit = {}
E2: -x2 + x1 <= 0: history = {E2}, explicit = {}, implicit = {}
E3: x2 - x1 + x0 < 0: history = {E3}, explicit = {}, implicit = {}


We eliminate x2 by adding E0 + E1 and E2 + E3 (and also two others that won't matter):

step 1:
E01 = E0 + E1: -x0 <= 0: history = {E0, E1}, explicit = {x2}, implicit = {}
E23 = E2 + E3: x0 < 0: history = {E2, E3}, explicit = {x2}, implicit = {x1}


The explicit set indicates that x2 was eliminated from each equation "on purpose", but x1 was also eliminated from E23 "on accident" and so it shows up in the implicit list for E23.

We then eliminate x1, which does nothing (except for deleting the extra unnecessary equations) because the equations already don't have x1 present.

We then eliminate x0:

step 2:
E0123 = E01 + E23: 0 < 0: history = {E0, E1, E2, E3}, explicit = {x0, x2}, implicit = {}


x0 has been added to the explicit list because this is a new equation constructed by elimination of x0. x1 is not in the implicit list because neither E01 nor E23 contains an occurrence of x1.

We apply the theorem now and conclude that since |history| = 4 > 3 = |explicit ∪ implicit| + 1, the newly generated equation E0123 is redundant, so we discard it and get a consistent state, leading to failure of the algorithm.

#### Mario Carneiro (Nov 02 2022 at 08:32):

Here's a standalone test case:

example (a b c z : ℚ) (_ : a ≤ z) (E0 : b ≤ c) (E1 : c ≤ a) (E2 : 0 ≤ c) : b ≤ a + c := by linarith -- fail


#### Scott Morrison (Nov 02 2022 at 09:46):

Thanks for the minimization! So... the conclusion we've reached here is that either

1. our interpretation (i.e. as implemented in mathlib3) of the theorem must be incorrect, because it is incorrect to discard E01234, or
2. our interpretation is correct and the theorem is false?

#### Mario Carneiro (Nov 02 2022 at 09:50):

I think the implementation of the theorem is incorrect in the interpretation of x1 as not being an implicitly eliminated variable of E0123. Wikipedia says that it should include all variables from equations in the history which are not in the explicit list, and x1 is in E2 which is in the history of E0123. I think the fix is to union the vars fields when you merge equations instead of recalculating it from the combined equation.

#17307

#### Scott Morrison (Nov 02 2022 at 10:16):

Actually, I better rewrite some doc-strings.

#### Scott Morrison (Nov 02 2022 at 10:27):

Okay, I've updated the doc-strings.

However over on the mathlib4 side, while this fix does fix the failure I initially reported in this thread, it doesn't appear to fix the failure I originally identified (and semi-minimised to put in this thread). So perhaps let's not hurry to merge this fix until I have that sorted out too.

#### Kevin Buzzard (Nov 02 2022 at 11:53):

Thank you so much Scott and Mario for this work. There's one thing I'm confused about -- if the lean 3 implementation has a bug then why is the output of the lean 3 test not incorrect?

#### Yaël Dillies (Nov 02 2022 at 13:32):

What do you mean by "incorrect"? It doesn't output anything incorrect but rather thinks it can't solve cases that should be able to.

#### Eric Rodriguez (Nov 02 2022 at 13:58):

I wonder how many proofs could be golfed now because of this bugfix...

#### Scott Morrison (Nov 03 2022 at 03:47):

I'm still seeing problems in the mathlib4 implementation (i.e. cases where linarith fails, but should succeed), but where if I ask it to reject fewer constraints according to Imbert's theorem, it succeeds. This suggests I still have the implementation of Imbert's theorem incorrect. :-(

#### Scott Morrison (Nov 03 2022 at 03:48):

Does someone have access to https://doi.org/10.1016/B978-0-444-88771-9.50019-2, and could send me a copy?

#### Scott Morrison (Nov 03 2022 at 03:48):

I think I'd prefer to read it at the source than try to parse too many masters theses trying to restate the result. :-)

#### Scott Morrison (Nov 03 2022 at 03:52):

Or if someone wants to compare the wikipedia description and the implementation, you can look either in #17307, or mathlib4#526. The mathlib4 PR has the advantage that it has a failing test, that succeeds if you change the 1 +  in maybeMinimal to 2 + , so can be used to test alternative interpretations...

#### Scott Morrison (Nov 03 2022 at 06:17):

Okay, I think I have this sorted out.

Sadly, the performance of Fourier-Motzkin elimination in larger examples is highly sensitive to the variable/equation ordering, and it's easy to have things either work fine or crash by adding and removing .reverse...

#### Scott Morrison (Nov 03 2022 at 07:02):

Okay, I've got this sorted out, and updated the PR.

#### Scott Morrison (Nov 03 2022 at 07:03):

The new interpretation of "implicitly eliminated variable" now results in all the tests (including the new one!) working in both mathlib3 and mathlib4, and follows the text of the original paper. (However, it doesn't seem to agree with a formula the original paper uses later, so I left a note for future readers... The original paper also has some confusing typos in a critical example... :-)

#### Kevin Buzzard (Nov 03 2022 at 07:06):

Re the typos: clearly the solution to that is to formalise the paper.

#### Reid Barton (Nov 03 2022 at 07:07):

I was only able to access the author's later 1993 paper, but I found the description of the theorem and associated algorithm there very unclear and I'm not surprised that it might have been interpreted incorrectly.

#### Moritz Doll (Nov 03 2022 at 09:12):

Kevin Buzzard said:

Re the typos: clearly the solution to that is to formalise the paper.

Well if we formalize every math paper that has typos in it, we'd be here forever :big_smile:

#### Mario Carneiro (Nov 03 2022 at 09:13):

the ones without typos are also helpful

#### Moritz Doll (Nov 03 2022 at 09:13):

I don't know any papers without typos..

#### Ruben Van de Velde (Nov 03 2022 at 09:18):

Reid Barton said:

I was only able to access the author's later 1993 paper, but I found the description of the theorem and associated algorithm there very unclear and I'm not surprised that it might have been interpreted incorrectly.

Maybe you could find a master's student to clarify it in their thesis

#### Eric Wieser (Nov 21 2022 at 12:06):

The fixed version seems much more likely to timeout than the original; for instance on

example (a b : ℤ)
(h₁ : a < b)
(ha : 1 * a * a - 3 * a - 2 = 0)
(hb : b * b - 3 * b - 2 = 0) :
(1 * a * a + b * b) - 2 * a * b = 17 :=
begin
nlinarith only [h₁, ha, hb],
end


Perhaps it's a coincidence that nlinarith was able to solve this in the first place; but it also seems plausible that we're now stuck in an infinite loop somewhere.

#### Scott Morrison (Nov 22 2022 at 23:44):

Yes, the bug was causing it to drop constraints, so it's no particular surprise if some big problems now timeout. The cost of correctness. :-)

Last updated: Aug 03 2023 at 10:10 UTC