Zulip Chat Archive

Stream: maths

Topic: small changes in nat and ordered groups inequalities


view this post on Zulip Adam Kurkiewicz (Apr 07 2018 at 11:43):

Proposal 1.

The following lemma is useful:

nat.le_add_right : ∀ (n k : ℕ), n ≤ n + k

could we have the following lemma in mathlib:

def  nat.le_add_right_of_le:  ∀ (n m k : nat) (n_le_m : n <= m), n <= m + k
    | n m 0 n_le_m := n_le_m
    | n m (k +  1) n_le_m := nat.le_succ_of_le (nat.le_add_right_of_le n m k n_le_m)

Proposal 2.

Can we rename lt_add_of_pos_of_lt to lt_add_right_of_pos_of_lt and lt_add_of_lt_of_pos lt_add_left_of_lt_of_pos? Can we perhaps make things more standard, and change the signature of lt_add_of_lt_of_pos and rename it to lt_add_of_pos_of_lt?

Proposal 3.

Can we have this in mathlib: def nat.le_mul_right_of_le_of_pos: ∀ (n m k : nat) (n_le_m : n <= m) (k_pos : 0 < k), n <= m * k := sorry (I haven't tried proving it yet, but I assume induction should work too quite straightforwardly). Perhaps we would want a more general result too in ordered_group.lean, i.e. le_mul_right_of_le_of_pos?

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 12:36):

Just to comment that theorem nat.le_add_right_of_le (n m k : nat) (n_le_m : n <= m) : n <= m + k := le_trans n_le_m $ nat.le_add_right _ _

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 12:40):

Things like lt_add_of_pos_of_lt are in the core lean library and it's very difficult currently to change anything in the core library, as the devs are busy with Lean 4 and are not amenable to "minor" changes like this. When Lean 4 hits a bunch of maths might be moved out of the core library and this might be the time to change these things. However I really want a place where comments such as this can sit festering until the devs are ready; it's difficult to find such a place as you can see from the Lean FAQ that opening minor issues is currently not really welcome.

view this post on Zulip Kevin Buzzard (Apr 07 2018 at 12:55):

Proposal 3 also looks like a case for transitivity, because it's naturally the conjunction of n <=m and m <= m * k

view this post on Zulip Adam Kurkiewicz (Apr 07 2018 at 20:11):

Thanks, I didn't realise that these were from standard library. I thought it was in mathlib in ordered_group.lean, but actually it is in standard library ordered_group.lean. It appears that many lemmas are copied over to mathlib from standard library, but they appear with a single apostrophe at the end in mathlib!

I think you're talking about a place to keep the backlog. I've seen people using trello boards for this purpose. I've set one up for this:
https://trello.com/b/we2kRiDw/lean-4-proposals

I've added you to it. Happy to add everybody else if this is what we want to use? If a different solution catches on, I can migrate these proposals over.

view this post on Zulip Mario Carneiro (Apr 07 2018 at 20:13):

The "apostrophe lemmas" have a different typeclass assumption, namely ordered_comm_group, which doesn't exist in core

view this post on Zulip Mario Carneiro (Apr 07 2018 at 20:14):

in an ideal world the core lemmas would be removed since you get them from the mathlib lemmas by typeclass inference, but core lib is basically frozen for now

view this post on Zulip Adam Kurkiewicz (Apr 07 2018 at 20:15):

I see, this all makes sense now.

view this post on Zulip Adam Kurkiewicz (Apr 07 2018 at 20:17):

Do apostrophed lemmas somehow shadow non-apostrophed lemmas? Certainly vscode doesn't autosuggest them for me.

view this post on Zulip Mario Carneiro (Apr 07 2018 at 20:18):

No, that sort of shadowing isn't allowed by lean. You have to have the file imported to see them in autosuggest

view this post on Zulip Mario Carneiro (Apr 07 2018 at 20:19):

One possibility is a "core lib wishlist" file we can maintain on mathlib. I used pending.lean for this briefly, but I've since become convinced that Leo is unlikely to ever accept a change from mathlib, so I have spent most of my time working around core as it exists rather than trying to change it. Such a wishlist may become useful if we ever fork lean, but I don't see what other good it would do.

view this post on Zulip Adam Kurkiewicz (Apr 07 2018 at 20:32):

Sounds a bit nuclear. Surely there must be a way for mathlib and stdlib to work closely together? Are main goals/objectives of lean and mathlib different?

view this post on Zulip Mario Carneiro (Apr 07 2018 at 20:33):

Trust me, this isn't what I want, but Leo has gone hermit in a big way and we have to work around this if we want to keep using and improving lean

view this post on Zulip Mario Carneiro (Apr 07 2018 at 20:34):

For now I'm keeping the possibility open but not making any steps towards a fork until it becomes absolutely necessary

view this post on Zulip Patrick Massot (Apr 08 2018 at 07:54):

I really hope Lean 4 and its reduced core lib will make all these problem disappear


Last updated: May 11 2021 at 16:22 UTC