ssreflect finset理解中的使用条件

Question

我有一个函数f，它接受一个fintype A的x和一个P x的证明，以返回fintype B的元素。我想返回满足P的所有x的f x的finset，可以这样写：

From mathcomp
Require Import ssreflect ssrbool fintype finset.

Variable A B : finType.
Variable P : pred A.
Variable f : forall x : A, P x -> B.

Definition myset := [set (@f x _) | x : A & P x].

然而，这失败了，因为Coq没有用右边的信息填充占位符，并且我不知道如何显式地提供它。

我没有找到关于如何做到这一点的指示，无论是在ssreflect代码中还是在书中。我意识到我可能可以通过使用sigma类型的{x :a；P}并修改一点f来做到这一点，但它感觉比应该的更复杂。有没有一种简单易读的方法可以做到这一点？

Answer 1

实际上，让事情按照你建议的方式工作的最简单的方法是使用sigma类型：

Definition myset := [set f (tagged x) | x : { x : A | P x }].

但事实上，f是一个有点奇怪的函数，我想我们需要了解更多关于你的用例的细节，才能理解你的目标。