Why can't linarith prove this goal

Stream: new members

[Timothy Mou]

Why can't linarith prove this goal:

example (i n : ℕ) : i < n + 1 → ¬ (i = n) → i < n := by
  linarith

[Timothy Mou]

What tactic should I use for linear integer arithmetic?

[Matthew Ballard]

Another option is omega

[Timothy Mou]

Thanks. It's a bit hard to search for this stuff, and I incorrectly assumed linarith was the analogue of Coq's lia

[Matthew Ballard]

I would think linarithshould do this also.

[Matthew Ballard]

omega seems (is?) much more recent so documentation needs to catch up

[Kyle Miller]

though linarith doesn't know about the fact that there are no natural numbers between n and n + 1

[Patrick Massot]

Kyle, this isn’t the issue. There are two completely independent issues. First linarith doesn’t do intro, this is simply not its job. And, for performance reasons, it doesn’t split not equal assumptions into two inequalities cases (since this could lead to a huge number of cases). So you can get a proof with:

[Patrick Massot]

example (i n : ℕ) : i < n + 1 → ¬ (i = n) → i < n := by
  intro h₁ h₂
  linarith (config := {splitNe := true})

[Patrick Massot]

To be honest I was never really convinced by the argument in favor of the splitNe := false default.

[Patrick Massot]

And I think the way linarith “knows” there is no natural number between n and n+1 is simply by preprocessing the inequality i < n into i + 1 ≤ n.