How to create a Powerset of MSetList?

Using Rocq
2

The construction of set shows that you are using the Make function with a module as argument. If you type Print Make., you see that this is a functor taking a module of type OrderedType as argument, and it produces a module with many fields, among which t, eq, eq_equiv, lt, lt_strorder, lt_compat, compare, compare_spec, and eq_dec. If you type Print OrderedType., you see that these field are the ones required to make an OrderedType.

So Make constructs all the fields that would be required to call Make again, thus producing the powerset.

You can just type :

Module pset := Make set.

and you will simply obtain a structure of sets, whose elements are in set.t. The following example was tested with coq 8.15.

Require Import 
        Coq.MSets.MSetList
        Coq.Strings.String 
        Coq.Structures.OrdersEx.

Module set := Make OrdersEx.String_as_OT.

Module pset := Make set.

Definition set1 := set.add "A"%string set.empty.
Definition set2 := set.add "B"%string set.empty.
Definition set3 := set.add "C"%string set1.

Definition pset1 := pset.add set1 (pset.add set2 pset.empty).

Compute pset.mem set3 pset1.
Compute pset.mem set2 pset1.
1 Like