Вы не можете выразить это напрямую.
Ошибочно думать об объектах в Set как о математических множествах.Set - это типы данных, те же типы, что и в языках программирования (за исключением того, что типы Coq очень мощные).
Coq не имеет подтипов¹.Если два типа F и Q различны, то они не пересекаются в математической модели.
Обычный подход состоит в объявлении F как полностью связанного набора, иобъявить каноническую инъекцию от F до Q.Вы захотите указать любое интересное свойство этой инъекции, кроме очевидного.
Parameter Q : Set.
Parameter F : Set.
Parameter inj_F_Q : F -> Q.
Axiom inj_F_Q_inj : forall x y : F, inj_F_Q x = inj_F_Q y -> x = y.
Coercion inj_F_Q : F >-> Q.
Эта последняя строка объявляет приведение от F до Q.Это позволяет помещать объект типа F везде, где для контекста требуется тип Q.Модуль вывода типов вставит вызов inj_F_Q.Время от времени вам нужно будет явно приводить приведение, поскольку механизм вывода типов, хотя и очень хороший, не идеален (совершенство было бы математически невозможно).В справочном руководстве Coq есть глава о принуждениях;Вы должны хотя бы просмотреть его.
Другой подход - определить ваше подмножество с помощью экстенсионального свойства, то есть объявить предикат P в наборе (тип) Q и определить F из P.
Parameter Q : Set.
Parameter P : Q -> Prop.
Definition G := sig P.
Definition inj_G_Q : G -> Q := @proj1_sig Q P.
Coercion inj_G_Q : G >-> Q.
sig - это спецификация, то есть тип слабой суммы, то есть пара, состоящая из объекта и доказательства того, что указанный объект обладает определенным свойством.sig P эквивалентно {x | P x} (что является синтаксическим сахаром sig (fun x => P x)).Вы должны решить, предпочитаете ли вы короткую или длинную форму (вы должны быть последовательными).Язык Program часто полезен при работе со слабыми суммами.
¹ В языке модуля есть подтипы, но здесь это не актуально.И принуждения подделывают подтипы достаточно хорошо для многих целей, но они не настоящие.