Deriving a cannonical structure for a record in coq (ssreflect)

Question

Given the following assumptions:

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

and a record defined as:

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

Intuitively, it would seem that example would also have to be of finType.

Looking at other code-bases, I have seen people derive finType for records with only one non-proof term using a construction of the form

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

But in this case, there are multiple fields to the record.

Is there an automatic way to derive fintype for the record, if not, how can fintype be derived for the record?

score 3 · Accepted Answer · answered Jul 25 '18 at 15:01

Many interface implementations in mathematical components can be derived by showing that your type is a retract of some other type that implements that interface. In your example, we just have to convert the record to a tuple.

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.

At the end of this snippet, example is declared as a finType. (Note that all the other declarations of eqType, choiceType, etc, are also necessary, since finType is a subclass of those.)

Deriving a cannonical structure for a record in coq (ssreflect)

1 Answers1