Coq中MSets的示例用法 [英] Example uses of MSets in Coq

问题描述

MSets 似乎是使用OCaml风格的有限集的方法。可悲的是，我找不到示例用法。

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

如何定义空的 MSet 或单例 MSet ？如何将两个 MSets 结合在一起？

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

推荐答案

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

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

您可以阅读 Coq.MSets.MSetInterface 来发现操作和规格提供 MSet 。

这篇关于Coq中MSets的示例用法的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！