1

编辑：我通过引入一个结构，通过将所述元素的成员资格证明携带到一个集合来增加一个元素，从而使这个例子变得更加简单：

Structure elem_and_in_proof {T : finType} (s : {set T}) := {el :> T ; Helin : el \in s}.

Canonical eip_subType {T : finType} (s : {set T}) := Eval hnf in [subType for (@el T s)].
Canonical eip_eqType {T : finType} (s : {set T}) := Eval hnf in EqType _ [eqMixin of (elem_and_in_proof s) by <:].
Canonical eip_choiceType {T : finType} (s : {set T}) := Eval hnf in ChoiceType _ [choiceMixin of (elem_and_in_proof s) by <:].
Canonical eip_countType {T : finType} (s : {set T}) := Eval hnf in CountType _ [countMixin of (elem_and_in_proof s) by <:].
Canonical eip_subCountType {T : finType} (s : {set T}) := Eval hnf in [subCountType of (elem_and_in_proof s)].
Canonical eip_finType {T : finType} (s : {set T}) := Eval hnf in FinType _ [finMixin of (elem_and_in_proof s) by <:].

但是，我需要将此转换应用于任何给定的集合，而且我似乎也无法做到：

Lemma equip_set_with_Helin {ft : finType} (s : {set ft}) : {set (elem_and_in_proof s)}.
Proof.
Admitted.

由于equip_set_with_Helin 允许我编写 uniq_cons 函数，因此将不胜感激有关此问题或原始问题的任何帮助。谢谢！

我有一个类型 dbranch，由有限类型 ft 上的序列和该序列的 uniq 证明组成。我希望能够，给定 ft 类型的元素 t 和 dbranch 上的 finset 以返回相同的集合，其中所有 dbranches 都已与 t 进行“cons-ed”。

我需要为分支编写一个 cons 函数，该函数将假设给定元素还不是分支的一部分作为参数。我不知道如何把它写成一个普通的函数，所以我把它当作一个证明。

然后我编写了 uniq_cons，它试图将 dcons 提升到一组 dbranches。然而，它的论点 H 的应用需要证明 b \in t （这是我代码中的占位符）。

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.

Definition dcons (t : ft) (b : dbranch) (H : t \notin (branch b)) : dbranch.
Proof.
exists (t :: b) ; apply/andP ; split.
  - apply H.
  - apply (buniq b).
Qed.  

Definition uniq_cons (al : ft) (t : {set dbranch}) (H : forall b, (b \in t -> al \notin (branch b))) := 
  [set (dcons al b (H b _)) | b in t].

b 在 t 中的事实应该是显而易见的，因为它直接出现在综合符号中。但是，我无法在 finset.va 中找到“提取”或使用该信息的方法，并且 Coq 无法自行完成。预先感谢您的帮助。

4

1 回答 1

2

要回答您修改后的问题，您可以执行以下操作：

From mathcomp
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finset.

Definition equip (T : finType) (A : {set T}) : {set {x : T | x \in A}} :=
  [set x in pmap insub (enum A)].

该序列enum A枚举了集合的所有元素A。该insub : T -> option sT函数将元素强制x : T转换为 的子类型sT : subType P，T前提是谓词P为x。鉴于 的所有元素enum A都在A定义中，这个函数的行为就像Some. 最后，pmap将偏函数映射到序列上，丢弃所有None结果。

于 2019-02-19T03:33:54.580 回答