Используйте условие в понимании финсета ssreflect

Question

У меня есть функция f, которая берет топор финтипа A и доказательство P x, чтобы вернуть элемент финтипа B. Я хочу вернуть finset из fx для всех x, удовлетворяющих P, что можно записать так:

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, так и в книге.Я понимаю, что мог бы сделать это, используя сигма-тип {x: A;P x} и модифицирует бит f, но он кажется более запутанным, чем следовало бы.Есть ли простой / читабельный способ сделать это?

Answer 1

На самом деле самый простой способ заставить вещи работать так, как вы предлагаете, - это использовать сигма-тип:

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

Но на самом деле, f - немного странная функция, я думаю, нам нужно узнать больше деталей о вашем сценарии использования, чтобы понять, куда вы идете.