Not solved by linarith

Stream: new members

[Elias Fåkvam]

Why is this not solved by linarith? at first i thought it might be because 0-1 would not make sense, but adding the positivity of j did not help.
its part of a longer poof but i have included all the imports in case they might be the problem.

import tactic
open function
open nat
open classical

lemma mytest (j > 0) : j-1 < j:=
begin
linarith,
end

[Ayush Agrawal]

Hi @Elias Fåkvam i am also noob here but, as far as I know linarith is not able to find the contradiction (0 < 0) just from (j > 0) and (j - 1 >= j) as linear combinations with nat numbers would not give 0 here. Gimme a sec and I'll provide some more insights here. Any others plz correct me!

[Ayush Agrawal]

Maybe this might make it more clear:
u can use set_option trace.linarith true for peeking what's going on

trying to split hypotheses
linarith is running on the following hypotheses:
[ℕ, j > 0, j - 1 ≥ j]
Preprocessing: filter terms that are not proofs of comparisons
[j - 1 ≥ j, j > 0]
Preprocessing: replace negations of comparisons
[j > 0, j - 1 ≥ j]
Preprocessing: move nats to ints
[0 < ↑j, ↑j ≤ ↑(j - 1), 0 ≤ ↑(j - 1), 0 ≤ ↑j]
Preprocessing: strengthen strict inequalities over int
[0 ≤ ↑j, 0 ≤ ↑(j - 1), ↑j ≤ ↑(j - 1), 0 + 1 ≤ ↑j]
Preprocessing: make comparisons with zero
[0 + 1 - ↑j ≤ 0, ↑j - ↑(j - 1) ≤ 0, -↑(j - 1) ≤ 0, -↑j ≤ 0]
Preprocessing: cancel denominators
[-↑j ≤ 0, -↑(j - 1) ≤ 0, ↑j - ↑(j - 1) ≤ 0, 0 + 1 - ↑j ≤ 0]
after preprocessing, linarith has 4 facts:
[-↑j ≤ 0, -↑(j - 1) ≤ 0, ↑j - ↑(j - 1) ≤ 0, 0 + 1 - ↑j ≤ 0]
hypotheses appear in 1 different types

[Ayush Agrawal]

u can read resources on Fourier–Motzkin elimination from wiki and https://leanprover-community.github.io/mathlib_docs/tactic/linarith/elimination.html to get what linarith uses. Here at the last line above u can observe that linear combinations of the facts with natural number coefficients greater than one is not possible for linarith to find contradiction 0 < 0 so it is failing. Hope this helps. lemme know it u need more insights!

[Ayush Agrawal]

Its interesting tho, since it should be able to find the contradiction using -1 + (j - (j -1)) this should be both zero and less than 0! @Yaël Dillies can u take a look here? is due to lack of treatment of - - 1 -> 1?

[Yaël Dillies]

I am no linarith expert but the problem is that it doesn't try to replace ↑(j - 1) with ↑j - 1.

[Ayush Agrawal]

Hmm yes! Interesting to think about the nuances here though :)

[Ruben Van de Velde]

I'm not sure linarith tries to do anything with the weird nat subtraction

[Yaël Dillies]

Seems like it could use docs#tactic.zify

[Alex J. Best]

linarith does use zify as a preprocessing step, it just doesn't use zify with the extra hypotheses included unfortunately. It should definitely be possible to support this if we wanted, but the obvious 1-line fix of including all hypotheses in the zify call doesn't work as it then uses the hypotheses to simplify themselves, resulting in trivial hypotheses.

[Alex J. Best]

Also @Elias Fåkvam you should try and only work with less than and less than an equal to (rather than > and \ge), a long time ago mathlib made the decision that having two equivalent but distinct ways of saying the same thing wasn't worth the headache, so decided to only use < and \le, hence many tactics and lemmas won't work flawlessly with > and \ge now.

[Alex J. Best]

I just made #9822 to track this.