Working with inequalities

Stream: new members

[Rick Love]

Seriously, it seems like I can work around most things but subtraction in naturals is very frustrating in how much time it takes to clear. I understand the need to keep everything non-negative, but I am having trouble finishing the proof when I get to the inequalities:

Currently I am stuck with this:

a b : ℕ,
ha : 0 < a,
hab : b < a
⊢ 0 < a - b

[Jujian Zhang]

example (a b : ℕ) (ha : 0 < a) (hab : b < a) : 0 < a - b :=
begin
  exact nat.sub_pos_of_lt hab,
end

I think this works

[Rick Love]

Thank you, I knew I had seen that but I couldn't find it. I thought I had done a library_search, but probably not at this point

[Rick Love]

Does anyone else have that problem?
I make a lot of progress thinking through the higher level proofs, but then get stuck messing with subtraction for an hour.

[Alex J. Best]

100% yes, personally I work through the high level proof and when I hit some annoying nat subtraction thing that I can't do immediately (but am sure is true) I sorry it and move on and finish the big picture. Then later (or the next day) I go through and do the nat subtraction things, quite often at that point I notice there is an easier way to set things up to avoid the nat subtraction type goal, e.g. work with ints, use different variables etc. This workflow can often help as once the big proof outline is done you can see all the small facts you need, quite often some of them are used more than once and can be small lemmas for instance. It also means you dont waste time proving all the small things along the way but then at the end notice your big picture proof strategy doesn't work.

[Rick Love]

@Alex J. Best that is great advice! Thanks!

Also, I was wondering why I was limiting myself to naturals. Do you find any problems using integers with some constraints that the primary values are positive?

[Alex J. Best]

What do you mean by primary values?

[Rick Love]

Alex J. Best said:

What do you mean by primary values?

Well the givens in the proof are that the involved integers are positive. However, I don't see any reason why values internal in the proof should be limited to the natural numbers.

[Rick Love]

Anyway, I'll give it a go with Integers and see if it removes the frustration.

[Kyle Miller]

Rick Love said:

Well the givens in the proof are that the involved integers are positive. However, I don't see any reason why values internal in the proof should be limited to the natural numbers.

I haven't used it myself, but there is the zify tactic (pronounced zee-ih-fie). https://leanprover-community.github.io/mathlib_docs/tactic/zify.html

[Rick Love]

@Kyle Miller zify looks like it will be very useful. Thanks!