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