Coq中集合的一致公式？

Question

我是Coq的新手，試圖根據我的研究開發一個框架。我的工作非常沉重，我無法編碼，因爲Coq似乎處理了集合。

有Type和Set，他們稱之爲「排序」，我可以使用它們來定義一組新：

Variable X: Type. 

然後還有一個圖書館編碼（子）設置爲「Ensembles」，其功能從Type到Prop。換句話說，他們是在一個Type謂詞：

Variable Y: Ensemble X. 

Ensemble的手感更像是適當的數學套。另外，它們是由許多其他圖書館建立的。我試着把注意力集中在它們上面：定義一個通用集合U: Set，然後將自己限制爲U上的（子）Ensemble s。但不是。 Ensemble s不能被用作類型的其他變量，也不能定義新的子集：

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

現在，我知道有幾個方式來解決這一點。問題「Subset parameter」提供了兩個。兩者都使用強制。第一個堅持到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。

Answer 1

自從我使用Coq以來，（從字面上看）已經有好幾年了，但讓我試着去幫忙。

我覺得從數學上講U: Set好像是說U是元素的宇宙，然後Ensemble U將意味着一組來自宇宙元素。因此，對於泛型概念和定義，您幾乎可以肯定使用Set和Ensemble是關於推理元素子集的一種可能方式。

我建議你看看Matthieu Sozeau介紹的type classes to Coq這個基於Haskell類型類的非常有用的特性。特別是在標準庫中，您會發現您在問題中提到的PartialOrder的基於類的定義。

另一個參考文獻是CoLoR library正式化了證明終止術語重寫所需的概念。訂單上有相當大的一套generic purpose definitions，什麼不是。