用户定义的枚举类型应该如何制作为“finType”？

Question

我想在 Coq/SSReflect 中创建一个归纳定义的枚举类型，例如

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

因为finType它显然是有限类型。我有三个解决方案来做到这一点，但所有的解决方案都比我预期的要复杂，而且永远不会令人满意。

在第一个解决方案中，我为eqType、choiceType和实现了 mixin countType。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).

它运作良好，但我想要一个更简单的解决方案。

第二种解决方案是仅使用序数类型

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.

但它需要在进一步的证明中进行涉及的案例分析（或者，需要定义一些我不想做的引理）。

作为第三种可能的解决方案，adhoc_seq_sub_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_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].

然而，它定义了与原始归纳类型不同的类型E，这意味着我们总是需要在进一步的证明中将它们相互转换。此外，它需要我们实现eqType（这也是显而易见的，可以默认不进行任何实现）。

由于我想定义许多枚举类型，因此为每种类型提供如此复杂的定义并不好。我期望的一个解决方案是，这样的eqType和finType几乎在枚举类型的相应归纳定义中自动给出。

有什么好的办法可以解决这个问题吗？

Answer 1

我在 Coq 中编写了一个泛型编程库，允许您编写如下代码：

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.

该库仍处于实验阶段，已转储到我的Coq utils 存储库中。代码非常不稳定。在底层，它使用 Coq 自动生成的归纳原理来对所有这些类所需的运算符进行编程。一个很好的功能是，为相等而生成的代码非常接近手写的代码 - 检查一下您编写的结果Compute (@eq_op E_eqType)！

编辑我已将该文件提取到一个独立的库中（https://github.com/arthuraa/deriving）。一旦变得更加稳定，这将成为 OPAM。

编辑 2coq-deriving该软件包现已在extra-devOPAM 存储库 ( https://github.com/coq/opam-coq-archive/tree/master/extra-dev ) 上提供。