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