我有一个由有限类型上的序列和该序列的 uniq 证明组成的结构。这应该描述一个明显有限的类型，但我不知道如何证明这一点。
我以为我可以使用 UniqFinMixin，但是它需要 - 如果我理解正确的话 - 提供该类型的所有元素的显式序列，我不知道如何计算。我尝试在有限类型上使用 Finite.enum，但它只生成一个包含有限类型所有元素的 seq，我没有找到计算所有子序列/排列的优雅方法。
From mathcomp
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype.
From mathcomp
Require Import tuple finfun bigop finset.
Variable ft : finType.
Structure dbranch := {branch :> seq ft ; buniq : uniq branch}.
Canonical dbranch_subType := Eval hnf in [subType for branch].
Canonical dbranch_eqType := Eval hnf in EqType _ [eqMixin of dbranch by <:].
Canonical dbranch_choiceType := Eval hnf in ChoiceType _ [choiceMixin of dbranch by <:].
Canonical dbranch_countType := Eval hnf in CountType _ [countMixin of dbranch by <:].
Canonical dbranch_subCountType := Eval hnf in [subCountType of dbranch].
Lemma dbranchFin : Finite.mixin_of [eqType of dbranch].
Admitted. (* :-( *)
Canonical dbranch_finType := Eval hnf in FinType _ dbranchFin.
在这里没有一种简单的方法可以导出 finType 对我来说似乎很奇怪，但是我在 finset.v 文件中找不到它。预先感谢您的帮助。
最佳答案
您可以证明 dbranch 嵌入到另一个 finType 中——例如，大小受 ft 限制的 #|ft| 元素列表的类型。
Lemma size_dbranch d : size (branch d) < #|ft|.+1.
Proof.
rewrite ltnS [card]unlock uniq_leq_size ?buniq // => ?.
by rewrite mem_enum.
Qed.
Definition tag_of_dbranch d : {k : 'I_#|ft|.+1 & k.-tuple ft} :=
@Tagged _ (Sub (size (branch d)) (size_dbranch d))
(fun k : 'I_#|ft|.+1 => k.-tuple ft)
(in_tuple (branch d)).
Definition dbranch_of_tag (t : {k : 'I_#|ft|.+1 & k.-tuple ft}) : option dbranch :=
insub (val (tagged t)).
Lemma tag_of_dbranchK : pcancel tag_of_dbranch dbranch_of_tag.
Proof. by rewrite /tag_of_dbranch /dbranch_of_tag=> x; rewrite valK. Qed.
Definition dbranch_finMixin := PcanFinMixin tag_of_dbranchK.
Canonical dbranch_finType := Eval hnf in FinType dbranch dbranch_finMixin.
关于coq - 从带有 uniq 的 finType 上的 seq 派生 ssreflect finType，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/54738603/