如何检查两个FStar.et的相等

Question

如何在FStar中检查两个集合是否相等？下面的表达式类型为Type0，而不是Tot Prims.bool，因此我不确定如何使用它来确定集合是否相等(例如，在条件中)。是否应该使用不同的函数而不是Set.equal？

Set.equal (Set.as_set [1; 2; 3]) Set.empty

Answer 1

FStar.Set中定义的集合使用函数作为表示。因此，例如，整数的集合s就是将整数映射到布尔函数的函数。例如，set {1, 2}表示为以下函数：

// {1, 2}
fun x -> if x = 1 then true
         else (
            if x = 2 then true
            else false 
         )

您可以添加/删除值(也就是说，创建一个新的lambda)，或者请求一个值作为一个成员(即应用该函数)。

然而，当要比较两组类型的T时，您就不走运了:对于s1和s2两组，s1 = s2意味着对于任何值x : T，s1 x = s2 x。当T的居民集是不有限的，这是不可计算的。

解决方案函数表示不适合您。您应该有一个表示，其比较关系是可计算的。FStar.OrdSet.fst将集合定义为列表:您应该使用该集合。

请注意，此OrdSet模块需要对集合中持有的值进行总体排序。(如果您想要一组无序值，我刚才是实现了，但它有点麻烦.)