A `LocallyFiniteOrderBot` is a `LocallyFiniteOrder`

Stream: mathlib4

[Etienne Marion]

Is there a reason why this is not in Mathlib?

import Mathlib

variable {α : Type*} [Preorder α] [LocallyFiniteOrderBot α]

noncomputable instance : LocallyFiniteOrder α where
  finsetIcc a b := ((Set.finite_Iic b).subset (@Set.Icc_subset_Iic_self _ _ a b)).toFinset
  finsetIco a b := ((Set.finite_Iio b).subset (@Set.Ico_subset_Iio_self _ _ a b)).toFinset
  finsetIoc a b := ((Set.finite_Iic b).subset (@Set.Ioc_subset_Iic_self _ _ a b)).toFinset
  finsetIoo a b := ((Set.finite_Iio b).subset (@Set.Ioo_subset_Iio_self _ _ a b)).toFinset
  finset_mem_Icc a b x := by simp
  finset_mem_Ico a b x := by simp
  finset_mem_Ioc a b x := by simp
  finset_mem_Ioo a b x := by simp

[Kevin Buzzard]

I guess it might cause a diamond with docs#LocallyFiniteOrder.toLocallyFiniteOrderBot and in general I guess there's a risk that you're using the typeclass system to create data which users might want to create differently, but your instance looks more natural mathematically than the one in the other direction which we seem to have.

[Eric Wieser]

LocallyFiniteOrder instances are supposed to be computable where possible

[Etienne Marion]

Is it because of some defeq issues?

[Eric Wieser]

Here's the kosher version:

import Mathlib

variable {α : Type*} [Preorder α] [LocallyFiniteOrderBot α]

/-- Not an instance as it would cause diamonds. -/
def LocallyFiniteOrderBot.toLocallyFiniteOrder [DecidableLE α] [DecidableLT α] :
    LocallyFiniteOrder α where
  finsetIcc a b := Finset.Iic b |>.filter (a ≤ ·)
  finsetIco a b := Finset.Iio b |>.filter (a ≤ ·)
  finsetIoc a b := Finset.Iic b |>.filter (a < ·)
  finsetIoo a b := Finset.Iio b |>.filter (a < ·)
  finset_mem_Icc a b x := by simp [and_comm]
  finset_mem_Ico a b x := by simp [and_comm]
  finset_mem_Ioc a b x := by simp [and_comm]
  finset_mem_Ioo a b x := by simp [and_comm]

[Eric Wieser]

Etienne Marion said:

Is it because of some defeq issues?

Yes, if you did the same thing for LocallyFiniteOrderTop then you'd have a non-defeq instance diamond

[Etienne Marion]

I see, thank you!

[Eric Wieser]

I think the above would be fine to add to mathlib as a means to resolve this thread and future questions like it, but I doubt it would actually be useful anywhere else.

[Etienne Marion]

I asked the question because I wanted to talk about Finset.Iic and Finset.Icc in the same theorem, and I realized that results like docs#Finset.Icc_subset_Iic_self asume both LocallyFiniteOrderBot and LocallyFiniteOrder, which seemed weird to me as one implies the other. But I guess this is the best way.

[Eric Wieser]

From the docs for LocallyFiniteOrderBot:

This is slightly weaker than LocallyFiniteOrder + OrderBot as it allows empty types.

[Etienne Marion]

Yes I saw that but I thought it meant LocallyFiniteOrderBot alone is the same but allows empty types (which it really is), but in practice in mathlib you need both LocallyFiniteOrderBot and LocallyFiniteOrder to have this only slightly weaker version.

[Etienne Marion]

Maybe it's worth making the docstring more precise?