coq - 应如何将用户定义的枚举类型设为 `finType` ？

Question

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

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

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

在第一个解决方案中，我为 eqType 实现了 mixin , choiceType , 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 repository 中.代码是 非常不稳定。在底层，它使用 Coq 自动生成的归纳原理来对所有这些类所需的运算符进行编程。一个很好的特性是，为相等而生成的代码非常接近手工编写的代码——如果你写 Compute (@eq_op E_eqType) 看看你会得到什么。 !

编辑 我已将该文件解压缩到一个独立的库中 ( https://github.com/arthuraa/deriving )。一旦它变得更加稳定，这将成为OPAM。

编辑 2 该软件包现在可用作 coq-deriving在 extra-dev OPAM 存储库 ( https://github.com/coq/opam-coq-archive/tree/master/extra-dev )。