如何检查两个 FStar.Set 的相等性

Question

在FStar中如何判断两个集合是否相等？以下表达式的类型为 Type0 而不是 Tot Prims.bool 所以我不确定如何使用它来确定集合是否相等（例如在条件中）。是否应该使用其他函数来代替 Set.equal？

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

Answer 1

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

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

您可以 add/remove 值（即创建一个新的 lambda），或要求一个值作为成员（即应用该函数）。

然而，在比较两组类型 T 时，你运气不好：对于 s1 和 s2 两组，s1 = s2 表示对于任何值 x : T、s1 x = s2 x。当 T 的居民集是无穷大时，这是不可计算的。

解决方法函数表示不适合你。您应该有一个表示，其比较是可计算的。 FStar.OrdSet.fst 将集合定义为列表：您应该改用它。

请注意，此 OrdSet 模块需要对集合中保存的值进行总排序。（如果你想要一组无序的值，我 implemented that 刚才，但它有点 hacky...）

How to check equality of two FStar.Set's