linarith regression

Stream: mathlib4

[Eric Wieser]

This works:

import data.real.basic

example (a b c d e : ℚ)
    (ha : 2 * a + b + c + d + e = 4)
    (hb : a + 2 * b + c + d + e = 5)
    (hc : a + b + 2 * c + d + e = 6)
    (hd : a + b + c + 2 * d + e = 7)
    (he : a + b + c + d + 2 * e = 8) :
    e = 3 := by
  linarith

but no longer works in mathlib4:

import Mathlib

example (a b c d e : ℚ)
    (ha : 2 * a + b + c + d + e = 4)
    (hb : a + 2 * b + c + d + e = 5)
    (hc : a + b + 2 * c + d + e = 6)
    (hd : a + b + c + 2 * d + e = 7)
    (he : a + b + c + d + 2 * e = 8) :
    e = 3 := by
  linarith

[Heather Macbeth]

Could it be #2717?

[Kevin Buzzard]

In this case, removing hypotheses definitely won't help :-)

[Eric Wieser]

Filed as #8875

[Scott Morrison]

I don't have time to do this now, but adding the line:

  dbgTrace s!"Eliminating {a}:\n{(← getPCompSet).toList}" fun _ => do

after the line

def elimVarM (a : ℕ) : LinarithM Unit := do

in Mathlib/Tactic/Linarith/Elimination.lean should give all the tracing information required to understand the bug.

[Scott Morrison]

Here is the output on Eric's problem:

Eliminating 5:
[[(5, -2), (4, -1), (3, -1), (2, -1), (1, -1), (0, 4)]=0, [(5, -1), (4, -2), (3, -1), (2, -1), (1, -1), (0, 5)]=0, [(5, -1), (4, -1), (3, -2), (2, -1), (1, -1), (0, 6)]=0, [(5, -1), (4, -1), (3, -1), (2, -2), (1, -1), (0, 7)]=0, [(5, -1), (4, -1), (3, -1), (2, -1), (1, -2), (0, 8)]=0, [(5, 1), (4, 1), (3, 1), (2, 1), (1, 2), (0, -8)]=0, [(5, 1), (4, 1), (3, 1), (2, 2), (1, 1), (0, -7)]=0, [(5, 1), (4, 1), (3, 2), (2, 1), (1, 1), (0, -6)]=0, [(5, 1), (4, 2), (3, 1), (2, 1), (1, 1), (0, -5)]=0, [(5, 2), (4, 1), (3, 1), (2, 1), (1, 1), (0, -4)]=0, [(0, -1)]<0, [(1, 1), (0, -3)]<0]
Eliminating 4:
[[]=0, [(2, -1), (1, 1), (0, -1)]=0, [(2, 1), (1, -1), (0, 1)]=0, [(3, -1), (1, 1), (0, -2)]=0, [(3, -1), (2, 1), (0, -1)]=0, [(3, 1), (1, -1), (0, 2)]=0, [(3, 1), (2, -1), (0, 1)]=0, [(4, -3), (3, -1), (2, -1), (1, -1), (0, 6)]=0, [(4, -1), (1, 1), (0, -3)]=0, [(4, -1), (2, 1), (0, -2)]=0, [(4, -1), (3, -3), (2, -1), (1, -1), (0, 8)]=0, [(4, -1), (3, -1), (2, -3), (1, -1), (0, 10)]=0, [(4, -1), (3, -1), (2, -1), (1, -3), (0, 12)]=0, [(4, -1), (3, 1), (0, -1)]=0, [(4, 1), (1, -1), (0, 3)]=0, [(4, 1), (2, -1), (0, 2)]=0, [(4, 1), (3, -1), (0, 1)]=0, [(4, 1), (3, 1), (2, 1), (1, 3), (0, -12)]=0, [(4, 1), (3, 1), (2, 3), (1, 1), (0, -10)]=0, [(4, 1), (3, 3), (2, 1), (1, 1), (0, -8)]=0, [(4, 3), (3, 1), (2, 1), (1, 1), (0, -6)]=0, [(0, -1)]<0, [(1, 1), (0, -3)]<0]
Eliminating 3:
[[]=0, [(2, -1), (1, 1), (0, -1)]=0, [(2, 1), (1, -1), (0, 1)]=0, [(3, -4), (2, -1), (1, -1), (0, 9)]=0, [(3, -1), (1, 1), (0, -2)]=0, [(3, -1), (2, -4), (1, -1), (0, 12)]=0, [(3, -1), (2, -1), (1, -4), (0, 15)]=0, [(3, -1), (2, 1), (0, -1)]=0, [(3, 1), (1, -1), (0, 2)]=0, [(3, 1), (2, -1), (0, 1)]=0, [(3, 1), (2, 1), (1, 4), (0, -15)]=0, [(3, 1), (2, 4), (1, 1), (0, -12)]=0, [(3, 4), (2, 1), (1, 1), (0, -9)]=0, [(0, -1)]<0, [(1, 1), (0, -3)]<0]
Eliminating 2:
[[]=0, [(2, -5), (1, -1), (0, 13)]=0, [(2, -1), (1, -5), (0, 17)]=0, [(2, -1), (1, 1), (0, -1)]=0, [(2, 1), (1, -1), (0, 1)]=0, [(2, 1), (1, 5), (0, -17)]=0, [(2, 5), (1, 1), (0, -13)]=0, [(0, -1)]<0, [(1, 1), (0, -3)]<0]
Eliminating 1:
[[]=0, [(0, -1)]<0, [(1, 1), (0, -3)]<0]
Eliminating 0:
[[]=0, [(0, -1)]<0]

[Eric Wieser]

It looks like the "eliminating 2` step is wrong (that is, things go wrong across the "eliminating 1" log line)

[Scott Morrison]

Yes. It looks like maybeMinimal is always returning false for the new constraints generated in that step.

[Scott Morrison]

I don't have time to look at this right now, but branch#debug_linarith has lots of dbgTrace statements, and this example added to tests/linarith.lean.

[Scott Morrison]

Oh: it's a failing test :-)

[Scott Morrison]

It's been a while since I thought about this "minimal history" business. My guess is that whenever we have an equation, we put both the equation and its negation into the list of constraints. These appear separately in the history, but perhaps (?!) they are not meant to. This would certainly break the maybeMinimal test.

[Scott Morrison]

However I'm not really sure how this could be different from the mathlib3 implementation...

[Eric Wieser]

It sounds like I may have sniped you into having time for this after all (I have no more today anyway)

[Eric Wieser]

I pushed some better logging, but I guess we probably need to add the same logging to mathlib3 to see what changed