finite types with ordering

Stream: general

[Scott Olson]

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?

[Johan Commelin]

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

[Scott Olson]

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

[Neil Strickland]

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.

[Scott Olson]

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.)

[Johan Commelin]

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.