Formulazioni coerenti di insiemi in Coq?

Question

Sono abbastanza nuovo in Coq e sto cercando di sviluppare un framework basato sulla mia ricerca. Il mio lavoro è abbastanza definito e ho problemi a codificarlo a causa del modo in cui Coq sembra trattare gli insiemi.

ci sono Type e Set, che loro chiamano 'tipi', e li può usare per definire una nuova serie:

Variable X: Type. 

E poi c'è una codifica libreria (sub) definisce come 'Ensembles', che sono funzioni da alcuni Type a Prop. In altre parole, essi sono predicati su un Type:

Variable Y: Ensemble X. 

Ensemble s sentono più come corrette insiemi matematici. Inoltre, sono basati su molte altre librerie. Ho cercato di focalizzarmi su di loro: definire un set universale U: Set, e quindi limitarmi a (sotto) Ensemble s su U. Ma no. Ensemble s non possono essere utilizzati come tipi per altre variabili, né di definire nuovi sottoinsiemi:

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

Ora, so che ci sono diversi modi per aggirare questo. La domanda "Subset parameter" ne offre due. Entrambi usano la coercizione. Il primo si attacca a Set s. Il secondo essenzialmente utilizza Ensemble s (sebbene non per nome). Ma entrambi richiedono un certo macchinario per realizzare qualcosa di così semplice.

Domanda: Qual è il modo consigliato di gestire in modo coerente (ed elegante) i set?

Esempio: Ecco un esempio di quello che voglio fare: Assumiamo un insieme DD. Definire una coppia dm = (D, <) dove D è un sottoinsieme finito di DD e < è un ordine parziale rigoroso su D.

Sono sicuro che con abbastanza armeggiare con coercizioni o altre strutture, potrei realizzarlo; ma non in un modo particolarmente leggibile; e senza una buona intuizione su come manipolare ulteriormente la struttura. Ad esempio, i seguenti tipi di controlli:

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

Ma non sono così sicuro che sia quello che voglio; e certamente non sembra molto carino. Si noti che sto andando avanti e indietro tra Set e Ensemble in modo apparentemente arbitrario.

Ci sono un sacco di librerie là fuori che usano Ensemble s, quindi ci deve essere un buon modo per trattarle, ma quelle librerie non sembrano essere documentate molto bene (o ... affatto).

Aggiornamento: Per complicare ulteriormente le cose, sembra che ci siano anche altre implementazioni, come MSets. Questo sembra essere completamente separato e incompatibile con Ensemble. Utilizza anche bool anziché Prop per qualche motivo. C'è anche FSets, ma sembra essere una versione obsoleta di MSets.

Answer 1

Sono passati (letteralmente) anni da quando ho usato Coq, ma lasciatemi provare ad aiutare.

Credo che matematicamente parlando U: Set è come dire U è un universo di elementi e Ensemble U allora significherebbe un insieme di elementi provenienti da quell'universo. Quindi per le nozioni e le definizioni generiche si utilizzerà quasi certamente Set e Ensemble è un modo possibile di ragionare su sottoinsiemi di elementi.

Ti suggerisco di dare un'occhiata all'ottimo lavoro di Matthieu Sozeau che ha introdotto type classes to Coq, una funzione molto utile basata sulle classi di tipi di Haskell. In particolare nella libreria standard troverai una definizione basata sulla classe di uno PartialOrder che hai menzionato nella tua domanda.

Un altro riferimento sarebbe il numero CoLoR library che formalizza le nozioni necessarie per dimostrare la cessazione della riscrittura a termine. Ha un set abbastanza grande di generic purpose definitions per gli ordini e quant'altro.