Stream: Beginner Questions

Topic: Set Comprehension in FSet

Liangrun Da (Sep 02 2024 at 14:30):

Hi everyone,

I’m currently using set comprehension with Set, like in the following function:

fun set_less_than :: "nat ⇒ nat set" where
  "set_less_than n = {x. x < n}"

I’m now looking to use FSet instead of Set and want to know if there’s a set comprehension equivalent available for FSet. I’ve browsed through the FSet source code but couldn’t find anything that directly provides this functionality.

Does anyone know if such a feature exists in Isabelle’s standard library?

fun fset_less_than :: "nat ⇒ nat fset" where
  "fset_less_than n = undefined"

Thanks!

John Park (Sep 05 2024 at 17:43):

fset_of_list [0..<n]

Chelsea Edmonds (Sep 06 2024 at 15:53):

For the example, you've given fset_of_list is definitely one approach. More generally (noting I have not used the FSet library myself), keep in mind set comprehensions in Isabelle is pretty syntax for filters. A quick search showed there was also a definitition for filter in the FSet library too (just perhaps not the same nice notation!).

John Park (Sep 07 2024 at 08:10):

Set comprehension like {x. x<n} uses not filter of another set, but Collect, which essentially converts an arbitrary predicate, \x. x<n in this case, into a set. But in general, it's impossible to convert arbitrary predicate on an infinitely large type like nat into a finite set, which I suppose is unfortunately what the original question is all about. So in short, no, I don't think it's possible to reasonably (i.e. not using Abs_fset) define such a set with any sort of set comprehension.

The trick with list comprehension is based on the intrinsic finiteness of list.

Chelsea Edmonds (Sep 07 2024 at 11:11):

That's definitely correct, apologies I rushed my first answer! Filters on sets are defined as a special case of collect when it's working from a predefined set (i.e. {x \in A. P x} ). I would say that if the original question was more asking about set comprehensions generally instead of just that specific example, the filter function on FSets could still be useful if your comprehension looks more like the above and if A is already defined as a finite set.

Liangrun Da (Sep 13 2024 at 10:02):

Thank you both for the answers! They did enhance my understanding of set comprehension in Isabelle and solve my problems.

Last updated: Dec 21 2024 at 16:20 UTC