Finset.range vs Finset.Iio

Stream: mathlib4

[Violeta Hernández]

Might I ask why we have two names for exactly the same thing? We even have docs#Nat.Iio_eq_range linking them together.

[Yury G. Kudryashov]

Finset.range was there long before Finset.Iio

[Yury G. Kudryashov]

I think that we should

• move code around so that the definition of LocallyFiniteOrder can be imported by the time we define Finset.range;
• migrate from Finset.range to Finset.Iio, deprecate the former;
• once Finset.range name is up to be reused, redefine it as Finset.univ.image f.

[Yury G. Kudryashov]

But I have no time to do it.

[Bhavik Mehta]

Note we're still missing quite a lot of the basic helpful rewrite lemmas for Finset.Iio (and indeed most of the finset intervals), eg docs#Finset.range_add_one, so I'd prefer for the finset interval api to be a bit more complete before making the migration. The shortest sequence of rewrites I know for that lemma in Iio language is

import Mathlib

example {n : ℕ} : Finset.Iio (n + 1) = insert n (Finset.Iio n) := by
  rw [Finset.Iio_insert, ← Finset.Iio_succ_eq_Iic, Order.succ_eq_add_one]

and similar things apply for the other finset intervals too.

[Yury G. Kudryashov]

In order to migrate from Finset.range to Finset.Iio, we need Finset.Iio versions of all Finset.range lemmas (with appropriate typeclass assumptions instead of Nat). That's why it needs more time than I have for this.

[Weiyi Wang]

While I generally dislike having multiple ways of spelling the same thing, it is funny how I have been seeing this particular one fine without realizing it, probably because I have already seen a lot of specialized [0, n) range in the programming world