linarith and "not equal"

Stream: new members

[Joe]

linarith works properly when the goal is of the form ¬ a = b, but it will fail if the goal is a ≠ b:

import tactic.linarith

variables (a b : ℚ)

lemma foo1 (ha : a < b) : ¬ a = b := by linarith -- succeed

lemma foo2 (ha : a < b) : a ≠ b := by linarith -- failed

I think this can be fixed easily by adding a corresponding pattern to get_contr_lemma_name:

| `(%%a ≠ %%b) := return `not.intro

[Joe]

However, if a ≠ b or ¬ a = b are hypotheses, linarith will fail in both cases:

lemma bar1 (ha : a ≠ b) : ¬ a = b := by linarith -- failed

lemma bar2 (ha : ¬ a = b) : ¬ a = b := by linarith -- failed

I think I can add support for this, but I'm not sure if this is intended.

[Joe]

It will make linarith exponential, since each ≠ will split into two goals. @Rob Lewis

[Rob Lewis]

Huh. Failing on ≠ goals is definitely an oversight, I'll fix that. Thanks for pointing that out!

[Rob Lewis]

Not using ≠ hypotheses is intentional. linarith shouldn't have that kind of exponential behavior.

[Johan Commelin]

@Rob Lewis Can you explain why bar2 in the example should fail?

[Johan Commelin]

I don't understand enough of the algorithm I guess.

[Johan Commelin]

Is it just that inequality in hypothesis is generally bad?

[Joe]

I think linarith proves a ≠ b → goal by proving a < b → goal and b < a → goal.

[Rob Lewis]

I think the algorithm can be adjusted to use ≠ hypotheses "natively," and this should probably be done at some point. But disequalities don't quite fit into the same framework as (in)equalities.

[Rob Lewis]

I think linarith proves a ≠ b → goal by proving a < b → goal and b < a → goal.

linarith doesn't prove this at all right now, but it's the "cheap" way to do it. Cheap in implementation time, not in runtime.

[Joe]

Yeah, I know. I was just mimicking the way linarith proves a = b.
But I'm curious, what is a better way of using ≠ hypotheses? What does "natively" mean?

[Rob Lewis]

Well, I meant "native" in the sense that it could handle disequality without encoding it into symbols it already knows about. But my claim is wrong, or at least, the half-baked algorithm I had in mind isn't complete. The proper way to handle disequality (and arbitrary logical formulas more generally) is with an SMT solver.