Как пользовательский перечислимый тип должен быть сделан `finType`? - PullRequest
Новая
       69

Как пользовательский перечислимый тип должен быть сделан `finType`?

4 голосов
/ 03 октября 2019

Я хочу сделать индуктивно определенный перечислимый тип в 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 почти автоматически даются при соответствующем индуктивном определении перечисляемых типов.

Есть ли хорошая идея для решения проблемы?

1 Ответ

2 голосов
/ 04 октября 2019

Я написал библиотеку для общего программирования на 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-dev OPAM хранилище (https://github.com/coq/opam-coq-archive/tree/master/extra-dev).

...