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

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函数，因此对于这个问题或原始问题的任何帮助都将不胜感激。谢谢!

我有一个由有限型ft上的序列组成的模d分支，以及这个序列的uniq的证明。我想要能够，给定一个类型为ft的元素t，并在d分支上设置一个finset来返回相同的集合，其中所有的d分支都是t的“cons”。

我需要为分支编写一个反函数，该函数以给定元素还不是分支的一部分这一假设作为参数。我不知道怎么把它写成一个常用的函数，所以我把它作为一个证明。

然后，我编写了uniq_cons，它试图将dcon提升到一组d分支中。但是，它的参数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中找不到一种“提取”或使用该信息的方法，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结果。