Coqのセットの一貫した配合？

Question

私はCoqでかなり新しく、私の研究に基づいてフレームワークを開発しようとしています。私の仕事はかなり定義が重く、Coqがセットを扱うように見えるため、エンコードに問題があります。

あり、彼らは「種類」と呼ぶTypeとSetは、ある、と私は新しいセットを定義するためにそれらを使用することができます。

Variable X: Type. 

をそしてライブラリのエンコーディング（サブ）セットは「Ensembles」とあります、 TypeからPropまでの機能である。言い換えれば、彼らはType上の述語です：

Variable Y: Ensemble X. 

Ensemble sがより適切な数学的なセットのように感じます。さらに、それらは多くの他のライブラリによって構築されています。私はそれらに焦点を当ててみました：1つのユニバーサルセットU: Setを定義し、Uの（サブ）Ensembleに自分自身を制限する。しかし、いいえ。 Ensemble sが他の変数の型として使用することはできません、また、新たなサブセットを定義するには：

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

は今、私はそれを回避するにはいくつかの方法があることを知っています。質問 "Subset parameter"は2つを提供します。どちらも強制変換を使用します。最初はSetに固執します。 2番目は基本的にEnsembleを使用します（名前ではありません）。しかし、どちらも簡単なことを達成するためには、どちらもかなりの機械が必要です。

質問：一貫して（エレガントに）ハンドリングセットの推奨方法は何ですか？

例：は、ここで私が何をしたいの例です：セットDDを想定します。一対DがDDの有限の部分集合であり、DM =（D、<）と<が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を使用するライブラリはたくさんありますので、それらを扱うには良い方法が必要ですが、それらのライブラリは文書化されていないようです（まったく...）。

更新：さらに問題を複雑にするために、MSetsのように、他の多くの設定実装もあるようです。これは完全に分離しており、Ensembleと互換性がないようです。何らかの理由でPropではなくboolも使用します。 FSetsもありますが、MSetsの古いバージョンのようです。

Answer 1

私はCoqを使用してから数年が経過していますが、手伝ってください。

私は数学的にU: Setを話すことUは、その宇宙から要素のセットを意味するであろう要素とEnsemble Uの宇宙であるというようなことだと思います。だから一般的な概念と定義のために、ほとんどの場合SetとEnsembleを使用して、要素のサブセットについて推論することができます。

私は、type classes to Coqを紹介したMatthieu Sozeauの素晴らしい仕事を見てみることをお勧めします。これは、Haskellのタイプクラスに基づいた非常に便利な機能です。特に標準ライブラリでは、あなたの質問で言及したPartialOrderのクラスベースの定義を見つけるでしょう。

用語の書き換えの終了を証明するのに必要な正式化の概念は、もう1つ参考になります（CoLoR library）。それはかなり大きいセットがgeneric purpose definitionsと注文にあります。