Согласованные формулировки множеств в Coq?

Я совершенно новый в Coq и пытаюсь разработать структуру, основанную на моих исследованиях. Моя работа довольно тяжелая, и у меня проблемы с ее кодированием из-за того, как Coq, кажется, обрабатывает множества.

Есть Type и Set, которые они называют "sorts", и я могу использовать их для определения нового набора:

Variable X: Type.

И тогда там кодировка (sub) библиотеки устанавливает как Ensembles ', которые являются функциями от некоторого Type до Prop. Другими словами, они являются предикатами на Type:

Variable Y: Ensemble X.

Ensemble больше напоминают правильные математические множества. Кроме того, они основаны на многих других библиотеках. Я попытался сосредоточиться на них: определяя один универсальный набор U: Set, а затем ограничивая себя (sub) Ensemble на U. Но нет. Ensemble нельзя использовать как типы для других переменных или определить новые подмножества:

Variable y: Y.           (* Error *)
Variable Z: Ensemble Y.  (* Error *)

Теперь я знаю, что есть несколько способов обойти это. Вопрос "Параметр подмножества" предлагает два. Оба используют принуждения. Первая привязка к Set s. Второй по существу использует Ensemble (хотя и не по имени). Но оба требуют довольно некоторого механизма для достижения чего-то такого простого.

Вопрос: Каков рекомендуемый способ последовательного (и элегантного) управления наборами?

Пример: Вот пример того, что я хочу сделать: Предположим, что установлен DD. Определим пару dm = (D, <), где D - конечное подмножество DD и < является строгим частичным порядком на D.

Я уверен, что с достаточным возиться с принуждениями или другими структурами я мог бы это сделать; но не в особенно читаемом виде; и без хорошей интуиции о том, как манипулировать структурой дальше. Например, следующие проверки типов:

Record OrderedSet {DD: Set} : Type := {
  D     : (Ensemble DD);
  order : (relation {d | In _ D d});

  is_finite         : (Finite _ D);
  is_strict_partial : (is_strict_partial_order order)
}.

Но я не настолько уверен в этом, чего хочу; и это, конечно, выглядит не очень красиво. Обратите внимание, что я иду назад и вперед между Set и Ensemble кажущимся произвольным способом.

Существует множество библиотек, которые используют Ensemble s, поэтому должен быть хороший способ их лечения, но эти библиотеки, похоже, не очень хорошо документированы (или... вообще).

Обновление:. Чтобы усложнить ситуацию, также существует ряд других реализаций набора, например MSets. Кажется, что это совершенно отдельный и несовместимый с Ensemble. По какой-то причине он также использует bool, а не Prop. Существует также FSets, но, похоже, это устаревшая версия MSets.

Ответ 1