Zulip Chat Archive

Stream: new members

Topic: Working with inequalities


view this post on Zulip Rick Love (Aug 19 2020 at 14:58):

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

view this post on Zulip Jujian Zhang (Aug 19 2020 at 15:00):

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

view this post on Zulip Rick Love (Aug 19 2020 at 15:02):

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

view this post on Zulip Rick Love (Aug 19 2020 at 15:05):

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.

view this post on Zulip Alex J. Best (Aug 19 2020 at 15:19):

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.

view this post on Zulip Rick Love (Aug 19 2020 at 16:08):

@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?

view this post on Zulip Alex J. Best (Aug 19 2020 at 16:12):

What do you mean by primary values?

view this post on Zulip Rick Love (Aug 19 2020 at 17:03):

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.

view this post on Zulip Rick Love (Aug 19 2020 at 17:05):

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

view this post on Zulip Kyle Miller (Aug 19 2020 at 18:03):

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

view this post on Zulip Rick Love (Aug 21 2020 at 00:11):

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


Last updated: May 09 2021 at 19:11 UTC