set - ¿Formulaciones consistentes de conjuntos en Coq?

subset

Question

Soy bastante nuevo en Coq y trato de desarrollar un marco basado en mi investigación. Mi trabajo es bastante pesado y tengo problemas para codificarlo debido a la forma en que Coq parece tratar los conjuntos.

Hay Type and Set , que llaman ''géneros'', y puedo usarlos para definir un nuevo conjunto:

Variable X: Type.

Y luego hay una biblioteca que codifica (sub) establece como '' Conjuntos '', que son funciones de algún Type a una Prop . En otras palabras, son predicados en un Type :

Variable Y: Ensemble X.

Ensemble s se parecen más a conjuntos matemáticos apropiados. Además, están basados ​​en muchas otras bibliotecas. Intenté centrarme en ellos: definir un conjunto universal U: Set , y luego limitarme a (sub) Ensemble en U Pero no. Ensemble no se pueden usar como tipos para otras variables, ni para definir nuevos subconjuntos:

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

Ahora, sé que hay varias formas de evitar eso. La pregunta " Parámetro del subconjunto " ofrece dos. Ambos usan coacciones. La primera se adhiere a Set s. El segundo esencialmente usa Ensemble s (aunque no por su nombre). Pero ambos requieren bastante maquinaria para lograr algo tan simple.

Pregunta: ¿Cuál es la forma recomendada de manejo sistemático (y elegante) de los conjuntos?

Ejemplo: Aquí hay un ejemplo de lo que quiero hacer: Supongamos un conjunto de DD . Defina un par dm = (D, <) donde D es un subconjunto finito de DD y < es un orden parcial estricto en D.

Estoy seguro de que con el suficiente retoque con las coerciones u otras estructuras, podría lograrlo; pero no de una manera particularmente legible; y sin una buena intuición de cómo manipular la estructura aún más. Por ejemplo, las siguientes verificaciones de tipo:

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)
}.

Pero no estoy tan seguro de que sea lo que quiero; y ciertamente no se ve muy bonito. Tenga en cuenta que voy hacia atrás y hacia adelante entre Set y Ensemble de una manera aparentemente arbitraria.

Hay muchas bibliotecas que usan Ensemble s, por lo que debe haber una buena manera de tratarlas, pero esas bibliotecas no parecen estar documentadas muy bien (o ... en absoluto).

Actualización: Para complicar aún más las cosas, parece haber otras implementaciones de conjuntos, como MSets . Este parece estar completamente separado e incompatible con Ensemble . También usa bool lugar de Prop por alguna razón. También hay FSets , pero parece ser una versión obsoleta de MSets.

Answer 1

Han pasado (literalmente) años desde que usé Coq, pero déjame intentar ayudar.

Creo que matemáticamente hablando U: Set es como decir que U es un universo de elementos y Ensemble U significaría un conjunto de elementos de ese universo . Por lo tanto, para nociones y definiciones genéricas seguramente usará Set y Ensemble es una forma posible de razonar sobre subconjuntos de elementos.

Sugiero que eche un vistazo al gran trabajo de Matthieu Sozeau, quien introdujo las clases de tipos en Coq , una característica muy útil basada en las clases de tipos de Haskell. En particular, en la biblioteca estándar encontrará una definición basada en la clase de un pedido parcial que menciona en su pregunta.

Otra referencia sería la biblioteca CoLoR que formaliza las nociones necesarias para demostrar la terminación de la reescritura del término. Tiene un conjunto bastante grande de definiciones de objetivos genéricos sobre pedidos y qué no.