4

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

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

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

在第一个解决方案中，我为、 和eqType实现choiceType了mixin 。countTypefinType

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

有什么好主意可以解决这个问题吗？

4

1 回答 1

3

我在 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。

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

于 2019-10-04T02:41:08.423 回答