Linarith with nats

Stream: mathlib4

[Chris Bailey]

Is there a tactic that works well for what appear to be simple goals on Nat and Int? I was told to use linarith, but it seems to have trouble with natural number, e.g. it's not able to solve this via linarith [h] (library_search also fails):

S.B : Nat
h: S.B > 1
⊢ S.B - 1 < S.B

[Sky Wilshaw]

(ignore that)

[Sky Wilshaw]

You might be able to get somewhere with zify then linarith, but I haven't tried.

[Eric Wieser]

docs4#Nat.pred_lt

[Chris Bailey]

@Eric Wieser

Thanks, maybe I should have been more specific. The example was just supposed to illustrate the kind of goal I'm talking about, I have a lot of small Nat problems like this that I would like to be able to solve with a tactic. I'm not struggling to prove this specific goal (I did indeed use Nat.pred_lt to close it out).

[Kevin Buzzard]

Unfortunately the lean 3 tactic is our buggy omega.

[Heather Macbeth]

linarith will work on Nat problems where the Nats behave "mathematically correctly". Your example has content only because of our weird definition of Nat subtraction, so linarith can't do it.

See if you can reorganize your arguments to avoid Nat subtraction. If you can, linarith will probably be more useful to you.

[Chris Bailey]

Thanks Kevin and Heather. I'll try to stick to stating things in terms of addition, I wasn't aware that Nat subtraction was that much of an issue for linarith.

[Scott Morrison]

It's only when you can trivially lift to Int that linarith copes with Nat (it is just calling zify as a pre-processor).

[Scott Morrison]

I don't think the Lean 3 implementation of omega is buggy, particularly, just the author is no longer active and no one wants to deal with the code.