coq - 在 ssreflect finset 理解中使用条件

Question

我有一个函数 f，它接受 fintype A 的 ax 和 P x 的证明来返回 fintype B 的元素。我想为所有满足 P 的 x 返回 fx 的 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-type {x : A ; P x} 并修改了一点 f，但感觉比它应该的更复杂。有没有一种简单/可读的方法来做到这一点？

Answer 1

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

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

但确实，f这是一个有点奇怪的功能，我想我们需要了解有关您的用例的更多详细信息才能了解您要去哪里。