Is there a way to enumerate the values of a finite inductive type in Coq?
E.g., consider the type:
Inductive state := A | B | C | D | E.
Is there any way to take this definition and from it, programmatically gain access to A, B, C, D, and E? I know in a proof I can use the induction tactic to prove for each case, but I want to be able to loop over the values of the type.
It depends on what you mean by "enumerate". In the Mathematical Components libraries, there is a finType interface for types with finitely many elements (https://math-comp.github.io/htmldoc/mathcomp.ssreflect.fintype.html). If T : finType, the term enum T collects all elements of T in a list.
It used to be the case that you had to build instances of this interface by hand. Since this process is tedious, I built a library for automating it. Maybe the library is overkill for your needs, but there is some code for inferring all the constructors of a type based on its induction principle. If you are interested in this, I can explain how it works in more detail.
I have also heard that the Ltac2 tactic language allows you to access the list of constructors of an inductive type, but I don't know how this works...
