1

How can you check whether two sets are equal in FStar? The following expression is of type Type0 not Tot Prims.bool so I'm not sure how to use it to determine if the sets are equal (for example in a conditional). Is there a different function that should be used instead of Set.equal?

Set.equal (Set.as_set [1; 2; 3]) Set.empty
JDN
  • 509
  • 3
  • 8
  • 14

1 Answers1

3

The sets defined in FStar.Set are using functions as representation. Therefore, a set s of integers for instance, is nothing else than a function mapping integers to booleans. For instance, the set {1, 2} is represented as the following function:

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

You can add/remove value (that is, crafting a new lambda), or asks for a value being a member (that is, applying the function).

However, when it comes to comparing two sets of type T, you're out of luck : for s1 and s2 two sets, s1 = s2 means that for any value x : T, s1 x = s2 x. When the set of T's inhabitants is inifinite, this is not computable.

Solution The function representation is not suitable for you. You should have a representation whose comparaison is computable. FStar.OrdSet.fst defines sets as lists: you should use that one instead.

Note that this OrdSet module requires a total order on the values held in the set. (If you want have set of non-ordered values, I implemented that a while ago, but it's a bit hacky...)

Lucas Franceschino
  • 61
  • 3