## Stream: new members

### Topic: linarith and "not equal"

#### Joe (Aug 06 2019 at 08:27):

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 (Aug 06 2019 at 08:28):

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 (Aug 06 2019 at 08:31):

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

#### Rob Lewis (Aug 06 2019 at 08:37):

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

#### Rob Lewis (Aug 06 2019 at 08:37):

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

#### Johan Commelin (Aug 06 2019 at 08:43):

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

#### Johan Commelin (Aug 06 2019 at 08:44):

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

#### Johan Commelin (Aug 06 2019 at 08:44):

Is it just that inequality in hypothesis is generally bad?

#### Joe (Aug 06 2019 at 08:49):

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

#### Rob Lewis (Aug 06 2019 at 08:49):

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 (Aug 06 2019 at 08:50):

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 (Aug 06 2019 at 09:04):

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 (Aug 06 2019 at 10:10):

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.

Last updated: Dec 20 2023 at 11:08 UTC