10

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

彼らが「並べ替え」と呼ぶ とがTypeありSet、それらを使用して新しいセットを定義できます。

Variable X: Type.

そして、「Ensembles」として（サブ）セットをエンコードするライブラリがあります。これは、 someTypeから aまでの関数Propです。つまり、これらは次の述語Typeです。

Variable Y: Ensemble X.

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

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

今、私はそれを回避する方法がいくつかあることを知っています。質問「サブセットパラメータ」は2つ提供しています。どちらも強制を使用します。最初は s に固執しSetます。2 番目は基本的にEnsembles を使用します (ただし、名前ではありません)。しかし、どちらも非常に単純なことを達成するにはかなりの機械が必要です。

質問:セットを一貫して (そしてエレガントに) 処理するための推奨される方法は何ですか?

例:これが私がやりたいことの例です: セット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、一見恣意的な方法で行ったり来たりしていることに注意してください。

sを使用するライブラリはたくさんあるEnsembleので、それらを扱う良い方法があるに違いありませんが、それらのライブラリはあまりよく文書化されていないようです (または... まったく)。

更新:さらに複雑なことに、MSetsなど、他にも多くのセットの実装があるようです。これは完全に別物で、 と互換性がないようEnsembleです。boolというよりPropもなぜか使っています。FSetsもありますが、古いバージョンの MSets のようです。

4

1 に答える 1

4

私が Coq を使ってから (文字通り) 何年も経ちましたが、助けてあげましょう。

数学的に言えば、 は要素の宇宙であり、その宇宙からの一連の要素を意味するU: Setと言うようなものだと思います。したがって、一般的な概念と定義については、ほぼ確実に使用するものであり、要素のサブセットについて推論するための 1 つの可能な方法です。UEnsemble USetEnsemble

Haskell の型クラスに基づいた非常に便利な機能であるCoq に型クラスを導入した Matthieu Sozeau の素晴らしい作品をご覧になることをお勧めします。特に標準ライブラリには、質問で言及したPartialOrderのクラスベースの定義があります。

別の参考文献は、用語書き換えの終了を証明するために必要な概念を形式化するCoLoR ライブラリです。これには、注文とその他に関する一般的な目的の定義のかなり大きなセットがあります。

于 2013-06-02T01:31:36.440 に答える