从 ssreflect finset 中提取/使用成员资格证明

Question

编辑：我通过引入一个结构来使该示例更加精简，该结构通过将所述元素的成员资格证明携带到一个集合来扩充元素：

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 到 return 相同的集合，其中所有 dbranches 都是 "cons-ed" 和 t.

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

然后我写了 uniq_cons，它试图将 dcons 提升到一组 dbbranches。但是，其参数 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.v 中找到 "extract" 或使用该信息的方法，而且 Coq 本身无法做到这一点。预先感谢您的帮助。

Answer 1

要回答您修改后的问题，您可以这样做：

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 强制转换为 T 的子类型 sT : subType P，前提是谓词 P 持有 x。根据定义，enum A 的所有元素都在 A 中，此函数的行为与 Some 相同。最后，pmap 将部分函数映射到序列上，丢弃所有 None 结果。

从 ssreflect finset 中提取/使用成员资格证明

Extract / use membership proof from a ssreflect finset

coq

ssreflect