More powerful version of linarith?

Stream: Is there code for X?

[Herman Chau]

Is there a more powerful version of the tactic linarith that incorporates lt_iff_le_and_ne? Here's a minimal example where I can't prove the goal directly with linarith, but can do it once I prove an intermediate inequality using lt_iff_le_and_ne.

import Mathlib.Tactic.Linarith

theorem eq_two_of_one_le_one_ne_lt_three (n:ℕ) (h: 1 ≤ n) (h': 1 ≠ n) (h'': n < 3) : n = 2 := by
  have : 2 ≤ n := by exact Nat.lt_iff_le_and_ne.mpr ⟨h, h'⟩
  linarith

[Eric Wieser]

omega works here

[Herman Chau]

Perfect, that's exactly what I'm looking for. Thank you!

[Kyle Miller]

There's also a linarith preprocessor you can enable to have it do cases on 1 < n and 1 > n:

theorem eq_two_of_one_le_one_ne_lt_three (n:ℕ) (h: 1 ≤ n) (h': 1 ≠ n) (h'': n < 3) : n = 2 := by
  linarith (config := { splitNe := true })

[Herman Chau]

Actually a quick follow up question: Is linarith completely subsumed by omega when trying to prove statements using linear arithmetic on natural numbers?

[Kevin Buzzard]

My mental model of those tactics says the answer is yes, but hopefully an expert can chime in. My mental model also says that there might be non-linear inequalities on the naturals which nlinarith can solve but omega cannot, because omega doesn't know what to do with $n^2$.

[Herman Chau]

Kyle Miller said:

There's also a linarith preprocessor you can enable to have it do cases on 1 < n and 1 > n:

theorem eq_two_of_one_le_one_ne_lt_three (n:ℕ) (h: 1 ≤ n) (h': 1 ≠ n) (h'': n < 3) : n = 2 := by
  linarith (config := { splitNe := true })

Oh interesting, I didn't know that there were config options for linarith. Thanks!

[Kevin Buzzard]

Do you see them when you hover over the tactic in VS Code? If not then it would be interesting to try and get a complete list of them from somewhere and add this to the docstring of the tactic. This bold approach makes mathlib better.

[Herman Chau]

Yes, it looks like the docstring does contain the list of arguments to config and what they do, but I had just never read through them.

I have been often treating tactics as black boxes, but I'm learning how useful it can be to peek under the hood a bit :)