coq - サブセットパラメータ

Question

パラメータとしてセットがあります：

Parameter Q:Set.

ここで、Qのサブセットである別のパラメーターを定義したいと思います。次のようなものです。

Parameter F: subset Q.

どうすればそれを定義できますか？後で公理として制限を追加できると思いますが、Fのタイプで直接表現する方が自然なようです。

Answer 1

直接表現することはできません。

のオブジェクトSetを数学的なセットと考えるのは誤解を招きます。Setは一種のデータ型であり、プログラミング言語で見られるのと同じ種類の型です（ただし、Coqの型は非常に強力です）。

Coqにはサブタイピングがありません¹。F2つのタイプQが異なる場合、数学モデルに関する限り、それらは互いに素です。

通常のアプローチは、完全に関連するセットとして宣言し、からへFの正規の注入を宣言することです。明白なことを超えて、そのインジェクションの興味深いプロパティを指定する必要があります。FQ

Parameter Q : Set.
Parameter F : Set.
Parameter inj_F_Q : F -> Q.
Axiom inj_F_Q_inj : forall x y : F, inj_F_Q x = inj_F_Q y -> x = y.
Coercion inj_F_Q : F >-> Q.

その最後の行は、からFへの強制を宣言していQます。Fこれにより、コンテキストでタイプが必要な場所にタイプのオブジェクトを配置できますQ。型推論エンジンはへの呼び出しを挿入しますinj_F_Q。型推論エンジンは非常に優れていますが、完全ではないため、強制を明示的に記述する必要があります（完全は数学的に不可能です）。Coqリファレンスマニュアルには強制に関する章があります。少なくともそれをすくい取る必要があります。

別のアプローチは、拡張プロパティを使用してサブセットを定義することです。つまりP、セット（タイプ）Qで述語を宣言し、から定義FしPます。

Parameter Q : Set.
Parameter P : Q -> Prop.
Definition G := sig P.
Definition inj_G_Q : G -> Q := @proj1_sig Q P.
Coercion inj_G_Q : G >-> Q.

sigは仕様、つまり弱い合計タイプ、つまりオブジェクトとそのオブジェクトが特定のプロパティを持っていることの証明で構成されるペアです。sig Peta-equivalent {x | P x}（これは構文糖衣sig (fun x => P x)です）。短い形式と長い形式のどちらを好むかを決定する必要があります（一貫性を保つ必要があります）。Program土語は、弱い合計で作業するときに役立つことがよくあります。

¹ _{モジュール言語にはサブタイピングがありますが、ここでは関係ありません。そして、強制は多くの用途に十分な偽のサブタイピングを行いますが、それらは本物ではありません。}