finset.map_add

Stream: general

[Kevin Buzzard]

In the list.Ico, multiset.Ico and finset.Ico namespaces, we have

theorem map_add (n m k : ℕ) : (Ico n m).map ((+) k) = Ico (n + k) (m + k) :=

This looks a bit distasteful to me, because if I've understood the map correctly, it's \lam x, k + x and the conclusion involves x + k. I find myself in a situation where I need k + x so I am proposing changing these names to map_add_left and map_add_right. I have several questions:

1) What is the idiomatic way to write \lam x, x + k?
2) Are the names good, and if so, which is map_add_left and which is map_add_right?
3) There is also

theorem map_sub (n m k : ℕ) (h₁ : k ≤ n) : (Ico n m).map (λ x, x - k) = Ico (n - k) (m - k) :=

I think there's space for a map_sub_left and map_sub_right (under appropriate inequality hypotheses). Are these appropriate names (in some order) for \lam x, x - k and \lam x, k - x? And the latter maps Ico a b to Ico (k + 1 - b) (k + 1 - a), or is it k - b + 1 or 1 + k - b or ... ? Are any of these choices clearly "better" than any other?

[Eric Wieser]

Probably not idiomatic, but I think \lam x, x + k is (+ k) (without the parens of ((+) k))

[Eric Wieser]

I assume the left / right thing can be resolved by looking at add_left_cancel style lemma namse?

[Anne Baanen]

1) I would vote for λ x, x + k just because it's clearest on which side the + sign stands.
2) I agree that we should have map_add_left and map_add_right with the correct direction of addition. Isn't the rule based on which argument is fixed, so λ x, x + k is called add_right?
3) If you can write them easily, it would be good to have. But at the moment I'm refactoring the whole of finset.range/list.range/list.Ico, so don't invest too much time. Again, I believe the order of left and right should be swapped.

[Anne Baanen]

Version of map_add after the refactor: https://github.com/leanprover-community/mathlib/blob/fin_range/src/data/list/enum.lean#L515

[Anne Baanen]

With instantiation for ℕ here: https://github.com/leanprover-community/mathlib/blob/fin_range/src/data/list/enum.lean#L605

[Kevin Buzzard]

OK maybe I'll hold back on this. I was responding to this comment on a recent PR of mine which is somehow getting bigger and bigger and should probably be closed and broken up.