computable enumeration

Stream: lean4

[James Gallicchio]

Is there a typeclass for types that have a computable enumeration? Fintype is backed by a multiset, and I can't extract a list from that (at least, not safely).

use case: I have a simple inductive like inductive Foo | baz | bar and want to represent Foo -> Nat in a more performant way than a closure. it would be nice to have a generic way to encode enum-indexed vectors as e.g. arrays.

[Mario Carneiro]

docs4#FinEnum is a mathlib type for that

[Tomas Skrivan]

It looks like that FinEnum is not intended to be run as a program. Do I understand it correctly that the enumeration for e.g. product type goes via List of all the elements? This has to be horribly slow.

instance prod {β} [FinEnum α] [FinEnum β] : FinEnum (α × β) :=
  ofList (toList α ×ˢ toList β) fun x => by cases x ; simp

[James Gallicchio]

That must have just been for ease of proving... maybe we reimplement it with division.

[James Gallicchio]

Also somewhat annoying that it's in mathlib. would you be open to PRs to move it and its dependencies? (they seem not too bad)

[Tomas Skrivan]

Reimplementing it and moving to std would be really nice!

[James Gallicchio]

are you using something like this in scilean already? / would you use it if it were in Std? :)

[Kyle Miller]

If you have a simple inductive type that's an enumeration like the one you show, then Lean will automatically generate a function called Foo.toCtorIdx : Foo -> Nat.

If you want the left inverse to it, then deriving DecidableEq (given by core Lean) generates two undocumented declarations: Foo.ofNat and Foo.ofNat_toCtorIdx

[James Gallicchio]

It'd be awfully nice to also have a deriving handler for arbitrary inductives. Hm.

[Yaël Dillies]

If you're going to reimplement FinEnum, I have a wishlist. Don't have time to look for it now, but search for Enum in #mathlib4.

[Kyle Miller]

For enum inductive types again, the Mathlib deriving Fintype handler will use these functions and define a couple more undocumented declarations in this function, for example it gives you a Foo.enumList : List Foo list that enumerates the elements.

[Kyle Miller]

I've thought a little bit about writing a derive handler to generate an injection to Nat in general (it'd be useful for Encodable/Countable).

For inductive types that aren't recursive, it shouldn't be too hard to make FinEnum instances using the proxy_type% elaborator that's in mathlib. You just need enough FinEnum instances for basic types (I think it's Unit, PLift, Sigma, Empty, and Sum), which should all be there, though they can be inefficient as written as Tomas pointed out...

[Kyle Miller]

James Gallicchio said:

That must have just been for ease of proving...

If I were to guess, it's partly for ease of definition (the existence of the instance proves that the type is a FinEnum) and partly because it probably grew out of Fintype, which also uses List deep down to enumerate the elements.

[Eric Wieser]

James Gallicchio said:

That must have just been for ease of proving... maybe we reimplement it with division.

docs4#finProdFinEquiv is that division

[Tomas Skrivan]

James Gallicchio said:

are you using something like this in scilean already? / would you use it if it were in Std? :)

I have my own type that has exactly that but bijection with a {i : USize // i < card} i.e. Fin n living on USize rather then on Nat. If cardinality of the type is bigger then USize.size then the map does not give any formal guarantees. I use it for accessing array elements, so having index types bigger then USize.size is a bad idea anyway.

Actually, I do not care too much if it lives in Std or Mathlib as I depend on both.

I would definitely like to have the version with Fin n. My usage of USize might be an unnecessary optimization.