Zulip Chat Archive

Stream: Is there code for X?

Topic: For naturals m < m', there is a positive integer s.th....


view this post on Zulip Jakob Scholbach (Apr 12 2021 at 09:28):

Is this in mathlib?

lemma sub_diff (m m' : ) (h : m < m') :  s : , 0 < s  m' = m + s :=
begin
  use m' - m,
  split,
  { omega },
  { exact (nat.add_sub_of_le (le_of_lt h)).symm }
end

view this post on Zulip Johan Commelin (Apr 12 2021 at 09:33):

The version with <= conditions exists.

view this post on Zulip Markus Himmel (Apr 12 2021 at 09:33):

There is docs#nat.exists_eq_add_of_lt which is similar to what you are looking for

view this post on Zulip Johan Commelin (Apr 12 2021 at 09:34):

I was thinking of https://leanprover-community.github.io/mathlib_docs/algebra/ordered_monoid.html#le_iff_exists_add

view this post on Zulip Eric Wieser (Apr 12 2021 at 09:35):

That golfs to

lemma nat.exists_eq_add_of_lt' (m m' : ) (h : m < m') :  s : , 0 < s  m' = m + s :=
let k, hk := nat.exists_eq_add_of_lt h in k.succ, k.zero_lt_succ, hk

view this post on Zulip Eric Wieser (Apr 12 2021 at 09:36):

But it's often more convenient to work in terms of n.succ instead of 0 < n

view this post on Zulip Johan Commelin (Apr 12 2021 at 09:38):

That's often true locally, but if you want to apply results in a different part of the library, then 0 < n is typically more flexible.

view this post on Zulip Johan Commelin (Apr 12 2021 at 09:39):

Because then you're often just handed a n : nat, and you don't want to case on it before applying a lemma.

view this post on Zulip Eric Wieser (Apr 12 2021 at 09:48):

Worth PR'ing the above, perhaps as nat.exists_eq_add_nonneg_of_lt then?

view this post on Zulip Jakob Scholbach (Apr 12 2021 at 11:20):

@Eric Wieser : OK, -- I'm in the middle of a PR #6743 in which I need this. Is it better to keep PRs affecting such fundamental files such as algebra.ordered_monoid separate or could I just as well edit algebra.ordered_monoid in the course of that PR #6743?

view this post on Zulip Eric Wieser (Apr 12 2021 at 11:32):

I'd recommend:

  • adding the lemma wherever is most convenient for now, and continuing the PR - putting it in the right place right now will make your builds very slow
  • creating a new PR with just that lemma, in the right place

By the time the first complex PR is close to ready to merge, chances are the second one is already merged, and all you have to do is remove your copy of the lemma

view this post on Zulip Yury G. Kudryashov (Apr 12 2021 at 20:08):

I usually put lemma into correct files and use --old.


Last updated: May 17 2021 at 16:26 UTC