Use condition in a ssreflect finset comprehension

Question

I have a function f that takes a x of fintype A and a proof of P x to return an element of fintype B. I want to return the finset of f x for all x satisfying P, which could be written like this :

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].

However, this fails as Coq does not fill the placeholder with the information on the right, and I do not know how to provide it explicitly.

I did not find an indication on how to do that, both in the ssreflect code and book. I realize that I could probably do it by using a sigma-type {x : A ; P x} and modifying a bit f, but it feels more convoluted than it should. Is there a simple / readable way to do that ?

ejgallego ejgallego · Accepted Answer · 2019-05-02T07:26:05

Actually the easiest way to make things work in the way you propose is to use a sigma type:

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

But indeed, f is a bit of a strange function, I guess we'll need to know more details about your use case to understand where are you going.

Use condition in a ssreflect finset comprehension

1 Answers