Coq中的Powerset和ensembles

Question

我对幺半群有以下定义

Class Monoid
  (K : Type)
  (op : K -> K -> K)
  (unit : K) := {
    (* few properties here *)
  }.

例如，我可以很容易地为单面(N, +, 0)实例化：

Instance Monoid_Instance_1 : Monoid nat plus O. 

效果很好。

我的问题是，我想实例化(P(P(G)), Union, Empty_set)这样的一元类，其中P(P(G))是集合G的powerset的powerset。理想情况下，我想要这样做：

Parameter G : Set.
Instance Monoid_Instance_2 : Monoid (Power_set (Power_set G)) Union Empty_set. 

它不能工作，因为Ensemble (Ensemble G)类型由Power_set返回(当然，上面的双Power_set是虚构的)

你知道我怎么能做到吗？是否需要更改Monoid的定义？

谢谢你的帮助。

Answer 1

Power_set是对Ensemble的操作，而不是对Set的操作。

Require Import Coq.Sets.Powerset.

Parameter S : Set.
Parameter E : Ensemble S.

Check Power_set _ (Power_set _ E).

Ensemble S已经是powerset的单体了。每个E : Ensemble S都是S的子集，反之亦然(将x : X理解为x ∈ X)。Ensembles是谓词：Ensemble X = (X -> Prop) = (X -> 2) = P X。

Conjecture C1 : forall x y z, Union _ (Union _ x y) z = Union _ x (Union _ y z).
Conjecture C2 : forall x, Union _ Empty_set x = x.

实际上，这些猜想假定谓词可拓性，这不是建设性的，但可以安全地添加。

你也许能证明

Power e1 : Ensemble (Ensemble t1)

In Empty (Power e1)

In e1 (Power e3) -> In e2 (Power e3) -> In (Union e1 e2) (Power e3)

，但你不能证明

Power e1 : Type

Empty : Power e1

Union : Power e1 -> Power e1 -> Power e1

。Power e1不是Prop、Set或Type，而是谓词。