linarith

Stream: new members

[Joachim Breitner]

Am I expecting too much from linarith? I am surprised this fails:

    change w.to_list.length ≠ 0 at hlen0,
    change w.to_list.length ≠ 1 at hlen1,
    have hlen : w.to_list.length ≥ 2, by linarith,

[Joachim Breitner]

Here is a #mwe:

example (n : nat) (h0 : n ≠ 0) (n1 : n ≠ 1) : n > 1 := by linarith

[Joachim Breitner]

Ah, judging from the docs, linarith isn’t actually for nat

[Alex J. Best]

You can use tactic#omega for this (but it's not allowed in mathlib anymore).

[Mario Carneiro]

linarith doesn't know much about nat, but I feel like it should be able to do this one. Maybe it works if you add n >= 0?

[Mario Carneiro]

example (n : nat) (h0 : n > 0) (n1 : n < 1) : n > 1 := by linarith -- ok
example (n : nat) (h0 : n > 0) (n1 : n > 1) : n > 1 := by linarith -- ok
example (n : nat) (h0 : n > 0) (n1 : n ≠ 1) : n > 1 := by linarith -- fail

It looks like the issue is that the transformation of a ≠ bto a < b or a > b happens after the nat preprocessor. cc: @Rob Lewis

[Rob Lewis]

No, the split_ne preprocessor isn't enabled by default (linarith isn't an SMT solver, etc etc)

[Rob Lewis]

example (n : nat) (h0 : n > 0) (n1 : n ≠ 1) : n > 1 := by linarith {split_ne := tt}

[Rob Lewis]

@Joachim Breitner note that if you use this for your original goal, it's doing exactly the dumb thing you'd hope it wouldn't: it's running linarith four times, once for every combination of cases. This is why split_ne is disabled by default. Exponential blowup in the number of disequalities in the context.

[Joachim Breitner]

Thanks! Luckily, it seems I don’t even need this reasoning. Classical case of a pen-and-paper-proof making too strong assumptions, and I only need to handle 0 and positive separately.