Coq 中 MSet 的使用示例

MSets https://coq.inria.fr/library/Coq.MSets.MSets.html似乎是 OCaml 式有限集的最佳选择。可悲的是，我找不到示例用途。

如何定义一个空的MSet或单身人士MSet？我怎样才能结合两个MSets一起？

让我展示一个有限自然数集的简单示例：

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` *)

你可以阅读Coq.MSets.MSetInterface https://coq.inria.fr/library/Coq.MSets.MSetInterface.html了解操作和规格MSets 提供。