用户定义的枚举类型应该如何成为“finType”？
How should a user-defined enumerated type be made `finType`?
我想在Coq/SSReflect中创建一个归纳定义的枚举类型，比如
Inductive E: Type := A | B | C.
be finType 因为它显然是有限类型。
我有三种解决方案，但都比我预期的要复杂，而且永远不会令人满意。
在第一个解决方案中，我为 eqType、choiceType、countType 和 finType.
实现了 mixin
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 几乎是在枚举类型的相应归纳定义中自动给出的
有什么解决问题的好办法吗？
我在 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 该软件包现在可以在 extra-dev OPAM 存储库 (https://github.com/coq/opam-coq-archive/tree/master/extra-dev) 上以 coq-deriving 的形式获得。
我想在Coq/SSReflect中创建一个归纳定义的枚举类型，比如
Inductive E: Type := A | B | C.
be finType 因为它显然是有限类型。
我有三种解决方案，但都比我预期的要复杂，而且永远不会令人满意。
在第一个解决方案中，我为 eqType、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 几乎是在枚举类型的相应归纳定义中自动给出的
有什么解决问题的好办法吗？
我在 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 该软件包现在可以在 extra-dev OPAM 存储库 (https://github.com/coq/opam-coq-archive/tree/master/extra-dev) 上以 coq-deriving 的形式获得。