How should a user-defined enumerated type be made `finType`?

Question

I want to make an inductively-defined enumerated type in Coq/SSReflect like

Inductive E: Type := A | B | C.

be finType because it is apparently a finite type. I have three solutions to do it but all are involved than I expected and never be satisfactory.

In the first solution, I implemented mixin's for eqType, choiceType, countType and finType.

Require Import all_ssreflect.

Inductive E := A | B | C.

Definition E_to_ord (e:E) : 'I_3.
  by apply Ordinal with (match e with A => 0 | B => 1 | C => 2 end); case e.
Defined.

Definition E_of_ord (i:'I_3) : E.
  by case i=>m ltm3; apply(match m with 0 => A | 1 => B | _ => C end).
Defined.

Lemma E_cancel: cancel E_to_ord E_of_ord. by case. Qed.

Definition E_eq s1 s2 := E_to_ord s1 == E_to_ord s2.
Definition E_eqP: Equality.axiom E_eq. by do 2 case; constructor. Defined.
Canonical E_eqType := Eval hnf in EqType E (EqMixin E_eqP).
Canonical E_choiceType := Eval hnf in ChoiceType E (CanChoiceMixin E_cancel).
Canonical E_countType := Eval hnf in CountType E (CanCountMixin E_cancel).
Canonical E_finType := Eval hnf in FinType E (CanFinMixin E_cancel).

It works well but I want a simpler solution.

The second solution is to just use an ordinal type

Require Import all_ssreflect.

Definition E: predArgType := 'I_3.
Definition A: E. by apply Ordinal with 0. Defined.
Definition B: E. by apply Ordinal with 1. Defined.
Definition C: E. by apply Ordinal with 2. Defined.

but it requires an involved case analysis in further proofs (or, some lemmas need to be defined which I don't want to do).

As the third possible solution, adhoc_seq_sub_finType could be used.

Require Import all_ssreflect.

Inductive E := A | B | C.

Definition E_to_ord (e:E) : 'I_3.
  by apply Ordinal with (match e with A => 0 | B => 1 | C => 2 end); case e.
Defined.
Definition E_eq s1 s2 := E_to_ord s1 == E_to_ord s2.
Definition E_eqP: Equality.axiom E_eq. by do 2 case; constructor. Defined.
Canonical E_eqType := Eval hnf in EqType E (EqMixin E_eqP).

Definition E_fn := adhoc_seq_sub_finType [:: A; B; C].

However, it defines a different type from the original inductive type E, which means that we always need to convert them each other in further proofs. Additionally, it requires us to implement eqType (which is also obvious and could be default without any implementation).

Since I want to define many enumerated types, it wouldn't be nice to give such involved definitions for every type. A solution I expected is that such eqType and finType are almost altomatically given at the corresponding inductive definition of enumerated types.

Is there any good idea to solve the problem?

Answer 1

I have written a library for generic programming in Coq that allows you to write code like this:

From mathcomp Require Import ssreflect ssrfun eqtype choice seq fintype.
From CoqUtils Require Import void generic.

Inductive E := A | B | C.

(* Convince Coq that E is an inductive type *)
Definition E_coqIndMixin :=
  Eval simpl in [coqIndMixin for E_rect].
Canonical E_coqIndType :=
  Eval hnf in CoqIndType _ E E_coqIndMixin.

(* Derive a bunch of generic instances *)
Definition E_eqMixin :=
  Eval simpl in [indEqMixin for E].
Canonical E_eqType :=
  Eval hnf in EqType E E_eqMixin.
Definition E_choiceMixin :=
  Eval simpl in [indChoiceMixin for E].
Canonical E_choiceType :=
  Eval hnf in ChoiceType E E_choiceMixin.
Definition E_countMixin :=
  Eval simpl in [indCountMixin for E].
Canonical E_countType :=
  Eval hnf in CountType E E_countMixin.
Definition E_finMixin :=
  Eval simpl in [indFinMixin for E].
Canonical E_finType :=
  Eval hnf in FinType E E_finMixin.

The library is still experimental and is dumped into my Coq utils repository. The code is very unstable. Under the hood, it uses the induction principles automatically generated by Coq to program the operators required by all these classes. One nice feature is that the code generated for equality is pretty close to what one would write by hand -- check what you get if you write Compute (@eq_op E_eqType)!

Edit I have extracted that file into a standalone library (https://github.com/arthuraa/deriving). This will make into OPAM once it becomes more stable.

Edit 2 The package is now available as coq-deriving on the extra-dev OPAM repository (https://github.com/coq/opam-coq-archive/tree/master/extra-dev).