Example uses of MSets in Coq

Question

MSets appear to be the way to go for OCaml-style finite sets. Sadly, I can't find example uses.

How can I define an empty MSet or a singleton MSet? How can I union two MSets together?

Answer 1

Let me show a simple example for finite sets of natural numbers:

From Coq
Require Import MSets Arith.

(* We can make a set out of an ordered type *)
Module S := Make Nat_as_OT.

Definition test := S.union (S.singleton 42)
                           (S.empty).

(* membership *)
Compute S.mem 0 test.   (* evaluates to `false` *)
Compute S.mem 42 test.  (* evaluates to `true`  *)

Compute S.is_empty test.     (* evaluates to `false` *)
Compute S.is_empty S.empty.  (* evaluates to `true` *)

You can read Coq.MSets.MSetInterface to discover the operations and specifications MSets provide.