linarith error in structured proof

Stream: mathlib4

[Heather Macbeth]

I encountered an issue today with linarith that reminds me of some recent bugs in abel (mathlib4#1394) and polyrith (mathlib4#1574): a failure in a structured tactic proof which is highly dependent on that particular structure and goes away if you try to reorganize or minimize. So maybe like those it's a missing whnfR or withMainContext?

import Mathlib.Tactic.Linarith

example [LinearOrderedCommRing α] (h : ∃ x : α, 0 ≤ x) : True := by
  cases' h with x h
  have : 0 ≤ x
  · linarith -- fails
  trivial

[Heather Macbeth]

I have tested it on the branch with the bugfix for
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linarith.20with.20discharger
so it's not the same issue.

[Mario Carneiro]

mathlib4#1775

[Heather Macbeth]

Heather Macbeth said:

So maybe like those it's a missing whnfR or withMainContext?

today's fix owed to the third member of the holy trinity, instantiateMVars

[Heather Macbeth]

@Mario Carneiro I tried out your fix and it doesn't actually seem to fix my original test case? You have adjusted the test slightly and it passes your version but not mine.

[Heather Macbeth]

import Mathlib.Tactic.Linarith

-- works
example [LinearOrderedCommRing α] (h : ∃ x : α, 0 ≤ x) : True := by
  cases' h with x h
  have : 0 ≤ x := by linarith
  trivial

example [LinearOrderedCommRing α] (h : ∃ x : α, 0 ≤ x) : True := by
  cases' h with x h
  have : 0 ≤ x
  · linarith -- fails
  trivial

[Mario Carneiro]

hm, I made it pass the original test case before modifying it, but that was on a branch with other changes as well from which the bug fix was extracted

[Mario Carneiro]

Indeed that was the issue. There is still a separate bug preventing me from doing the whole refactor, but I can at least do this part without breaking any tests.