Получите ssreflect finType из seq над finType с помощью uniq - PullRequest
Новая
       25

Получите ssreflect finType из seq над finType с помощью uniq

0 голосов
/ 18 февраля 2019

У меня есть структура, состоящая из последовательности над конечным типом и доказательства uniq этой последовательности.Это должно описывать тип, который, конечно, конечен, но я не вижу, как это показать.

Я думал, что мог бы использовать UniqFinMixin, однако он требует - если я правильно понимаю - предоставить явный seq всех элементов типа, который я не знаю, как вычислить.Я попытался использовать Finite.enum для конечного типа, но он производит только последовательность со всеми элементами конечного типа, и я не нашел элегантного способа вычисления всех подпоследовательностей / перестановок. 

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.Заранее благодарю за помощь.

1 Ответ

0 голосов
/ 18 февраля 2019

Можно показать, что 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.
...