issue !4#8875: linarith can no longer solve a simple problem

Stream: triage

[Random Issue Bot]

Today I chose issue 8875 for discussion!

linarith can no longer solve a simple problem
Created by @Eric Wieser (@eric-wieser) on 2023-12-07
Labels: bug

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue #8875 for discussion!

linarith can no longer solve a simple problem
Created by @Eric Wieser (@eric-wieser) on 2023-12-07
Labels: bug

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue #8875 for discussion!

linarith can no longer solve a simple problem
Created by @Eric Wieser (@eric-wieser) on 2023-12-07
Labels: bug

Is this issue still relevant? Any recent updates? Anyone making progress?

[Violeta Hernández]

This example compiles fine on current Mathlib:

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 (config := { oracle := .fourierMotzkin })

[Kevin Buzzard]

Yes, I am unclear about whther this is still relevant. Does grind also work?

[Eric Wieser]

I guess #24903 fixed this

[Eric Wieser]

Though my guess is that by changing the hash table structure, failures here have been replaced with failures elsewhere that we haven't found

[Eric Wieser]

Maybe a good test would be to compile mathlib with the default oracle changed, and see if anything fails