Zulip Chat Archive

Stream: general

Topic: finite types with ordering


view this post on Zulip Scott Olson (Apr 16 2019 at 18:43):

In a couple of my projects I've found the need for a typeclass for finite types which either support a decidable_linear_order, or equivalently, have decidable_eq and a universe list (not just a universe finset). The trouble with using [fintype a] [decidable_linear_order a] itself is that it rules out lots of core types like unit which don't have decidable_linear_order unless I do it myself. Another option I found which works pretty well is [fintype a] [encodable a] which has greater coverage but seems somewhat roundabout and perhaps an abuse of encodable.

In fact, before I found mathlib I had defined my own fintype for these purposes which used a nodup universal list, but it's a lot of unnecessary duplication of work.

I guess my question is, what approach would people recommend?

view this post on Zulip Johan Commelin (Apr 16 2019 at 18:52):

I would PR an instance of decidable_linear_order for unit and the other types for which you think it should exist.

view this post on Zulip Scott Olson (Apr 16 2019 at 18:55):

Hmm, yeah, I'm not sure why I didn't consider that... it's probably the simplest way to go.

view this post on Zulip Neil Strickland (Apr 16 2019 at 18:56):

I also did a version of this (with a typeclass called enumeration). Some version or other should be in mathlib. I could make a PR of mine if people thought that would be useful. I am not sure whether we need to worry about diamonds, though. We would want to have an instance converting enumeration to fintype, and instances deriving numerations and fintypes on α × β from those on α and β. That gives two ways of getting from enumeration α and enumeration β to fintype (α × β), but the target is a subsingleton so perhaps it does not matter.

view this post on Zulip Scott Olson (Apr 16 2019 at 19:08):

That would be cool. It's also possible to implement a derive macro for fintype and/or enumeration so something like @[derive enumeration] inductive state | A | B works. (I had this working with my custom fintypewhich was convenient for readable finite automata states.)

view this post on Zulip Johan Commelin (Apr 16 2019 at 19:10):

That gives two ways of getting from enumeration α and enumeration β to fintype (α × β), but the target is a subsingleton so perhaps it does not matter.

Sadly, this does matter, currently. The standard solution seems to be to make enumeration redundant by adding the fintype instance into it (i.e. by extending fintype). You can provide a constructor which doesn't need the fintype instance, but in this way you can make sure that the product will have the correct fintype instance.


Last updated: May 15 2021 at 00:39 UTC