У меня есть набор в качестве параметра:
Parameter Q:Set.
Теперь я хочу определить еще один параметр, который является подмножеством Q. Что-то вроде:
Parameter F: subset Q.
Как я могу это определить? Я думаю, что я могу добавить ограничение позже как аксиому, но кажется более естественным выразить его непосредственно в типе F.
Вы не можете выразить это прямо.
Ошибочно думать об объектах в 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 часто бывает полезен при работе со слабыми суммами.
¹ В языке модулей есть подтипы, но здесь это не имеет значения. А приведения подделывают подтипы достаточно хорошо для многих применений, но они не настоящие.
