dropping Set.Ico etc in favor of new core syntax

Stream: mathlib4

[Eric Wieser]

From a docstring somewhere, Lean now has:

• a...=b is the range of elements greater than or equal to a and less than or equal to b.
• a<...=b is the range of elements greater than a and less than or equal to b.
• a...b or a...<b is the range of elements greater than or equal to a and less than b.
• a<...b or a<...<b is the range of elements greater than a and less than b.
• *...=b is the range of elements less than or equal to b.
• *...b or *...<b is the range of elements less than b.
• a...* is the range of elements greater than or equal to a.
• a<...* is the range of elements greater than a.

Should mathlib provide the instances to coerce these to sets?

[Yaël Dillies]

Wait, where is this syntax from?

[Eric Wieser]

I'm afraid I didn't write that down, but it's referenced in the 4.22.0 release notes

[Eric Wieser]

docs#Std.PRange

[Aaron Liu]

It's less consistent :(

[Yaël Dillies]

I am somewhat sad that, after having spent so much time making intervals nice to use in mathlib, I was not even told that such ranges were going to be added

[Markus Himmel]

Being an alternative to mathlib's intervals is not a goal of docs#Std.PRange. It is intended to be a more capable alternative to docs#Std.Range, built for programmers, mainly for iteration in for loops and to build slices of arrays and other data structures.

[Eric Wieser]

To be concrete, what I'm proposing initially is:

import Mathlib

variable {α}

namespace Set
variable [Preorder α]

instance : CoeOut (Std.PRange (.mk .open .open) α) (Set α) where coe x := Set.Ioo x.lower x.upper
instance : CoeOut (Std.PRange (.mk .open .closed) α) (Set α) where coe x := Set.Ioc x.lower x.upper
instance : CoeOut (Std.PRange (.mk .closed .open) α) (Set α) where coe x := Set.Ico x.lower x.upper
instance : CoeOut (Std.PRange (.mk .closed .closed) α) (Set α) where coe x := Set.Icc x.lower x.upper
instance : CoeOut (Std.PRange (.mk .unbounded .open) α) (Set α) where coe x := Set.Iio x.upper
instance : CoeOut (Std.PRange (.mk .unbounded .closed) α) (Set α) where coe x := Set.Iic x.upper
instance : CoeOut (Std.PRange (.mk .open .unbounded) α) (Set α) where coe x := Set.Ioi x.lower
instance : CoeOut (Std.PRange (.mk .closed .unbounded) α) (Set α) where coe x := Set.Ici x.lower

end Set

namespace Finset
variable [Preorder α]

instance [LocallyFiniteOrder α] : CoeOut (Std.PRange (.mk .open .open) α) (Finset α) where coe x := Finset.Ioo x.lower x.upper
instance [LocallyFiniteOrder α] : CoeOut (Std.PRange (.mk .open .closed) α) (Finset α) where coe x := Finset.Ioc x.lower x.upper
instance [LocallyFiniteOrder α] : CoeOut (Std.PRange (.mk .closed .open) α) (Finset α) where coe x := Finset.Ico x.lower x.upper
instance [LocallyFiniteOrder α] : CoeOut (Std.PRange (.mk .closed .closed) α) (Finset α) where coe x := Finset.Icc x.lower x.upper
instance [LocallyFiniteOrderBot α] : CoeOut (Std.PRange (.mk .unbounded .open) α) (Finset α) where coe x := Finset.Iio x.upper
instance [LocallyFiniteOrderBot α] : CoeOut (Std.PRange (.mk .unbounded .closed) α) (Finset α) where coe x := Finset.Iic x.upper
instance [LocallyFiniteOrderTop α] : CoeOut (Std.PRange (.mk .open .unbounded) α) (Finset α) where coe x := Finset.Ioi x.lower
instance [LocallyFiniteOrderTop α] : CoeOut (Std.PRange (.mk .closed .unbounded) α) (Finset α) where coe x := Finset.Ici x.lower

end Finset

#check (1...3 : Set ℕ)
#eval (1...3 : Finset ℕ)

[Kim Morrison]

Markus Himmel said:

Being an alternative to mathlib's intervals is not a goal of docs#Std.PRange. It is intended to be a more capable alternative to docs#Std.Range, built for programmers, mainly for iteration in for loops and to build slices of arrays and other data structures.

That said, if Mathlib decides it wants to use them, that's fine and great, if it works well. (Deduplication and having only a single way to say things is good!) Markus is just pointing out what the design constraints were here. :-)

[Eric Wieser]

I'd be curious to know if any duplication in mathlib can be reduced by changing making the i/c/o in Set.Iic etc parametrizable