时间戳

首页 > 解决方案 > 为 coq 中的记录导出规范结构（ssreflect）

coq - 为 coq 中的记录导出规范结构（ssreflect）

问题描述

鉴于以下假设：

Variable A : finType.
Variable B : finType.
Variable C : finType.

以及定义为的记录：

Record example := Example {
       example_A : A;
       example_B : B;
       example_C : C;
}.

直觉上，这个例子似乎也必须是 of finType。

查看其他代码库，我看到人们finType使用表单的构造仅使用一个非证明项导出记录

Definition <record>_subType := Eval hnf in [subtype for <record-accessor>].
Definition <record>_finMixin := Eval hnf in [finMixin of <record> by <:].

但在这种情况下，记录有多个字段。

是否有一种自动方法可以为记录派生 fintype，如果没有，如何为记录派生 fintype？

标签： coqssreflect

解决方案

数学组件中的许多接口实现可以通过显示您的类型是实现该接口的某些其他类型的缩回来派生。在您的示例中，我们只需将记录转换为元组。

From mathcomp Require Import
  ssreflect ssrfun ssrbool ssrnat eqtype seq choice fintype.

Variables A B C : finType.

Record example := Example {
  example_A : A;
  example_B : B;
  example_C : C
}.

Definition prod_of_example e :=
  let: Example a b c := e in (a, b, c).

Definition example_of_prod p :=
  let: (a, b, c) := p in Example a b c.

Lemma prod_of_exampleK : cancel prod_of_example example_of_prod.
Proof. by case. Qed.

Definition example_eqMixin :=
  CanEqMixin prod_of_exampleK.
Canonical example_eqType :=
  Eval hnf in EqType example example_eqMixin.
Definition example_choiceMixin :=
  CanChoiceMixin prod_of_exampleK.
Canonical example_choiceType :=
  Eval hnf in ChoiceType example example_choiceMixin.
Definition example_countMixin :=
  CanCountMixin prod_of_exampleK.
Canonical example_countType :=
  Eval hnf in CountType example example_countMixin.
Definition example_finMixin :=
  CanFinMixin prod_of_exampleK.
Canonical example_finType :=
  Eval hnf in FinType example example_finMixin.

在此代码段的末尾，example被声明为finType. （请注意，所有其他声明eqType,choiceType等也是必需的，因为finType它是这些声明的子类。）

推荐阅读