Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

A collection of set utilities, useful when working with symbolic sets. To the extent possible, the functions in this module follow those of Data.Set so importing qualified is the recommended workflow.

Note that unlike Data.Set, SBV sets can be infinite, represented as a complement of some finite set. This means that a symbolic set is either finite, or its complement is finite. (If the underlying domain is finite, then obviously both the set itself and its complement will always be finite.) Therefore, there are some differences in the API from Haskell sets. For instance, you can take the complement of any set, which is something you cannot do in Haskell! Conversely, you cannot compute the size of a symbolic set (as it can be infinite!), nor you can turn it into a list or necessarily enumerate its elements.

**A note on cardinality**: You can indirectly talk about cardinality: `hasSize`

can be used to state that the set is finite and has size `k`

for a user-specified symbolic
integer `k`

.

## Synopsis

- empty :: forall a. HasKind a => SSet a
- full :: forall a. HasKind a => SSet a
- universal :: forall a. HasKind a => SSet a
- singleton :: forall a. (Ord a, SymVal a) => SBV a -> SSet a
- fromList :: forall a. (Ord a, SymVal a) => [a] -> SSet a
- complement :: forall a. (Ord a, SymVal a) => SSet a -> SSet a
- insert :: forall a. (Ord a, SymVal a) => SBV a -> SSet a -> SSet a
- delete :: forall a. (Ord a, SymVal a) => SBV a -> SSet a -> SSet a
- member :: (Ord a, SymVal a) => SBV a -> SSet a -> SBool
- notMember :: (Ord a, SymVal a) => SBV a -> SSet a -> SBool
- null :: HasKind a => SSet a -> SBool
- isEmpty :: HasKind a => SSet a -> SBool
- isFull :: HasKind a => SSet a -> SBool
- isUniversal :: HasKind a => SSet a -> SBool
- hasSize :: (Ord a, SymVal a) => SSet a -> SInteger -> SBool
- isSubsetOf :: (Ord a, SymVal a) => SSet a -> SSet a -> SBool
- isProperSubsetOf :: (Ord a, SymVal a) => SSet a -> SSet a -> SBool
- disjoint :: (Ord a, SymVal a) => SSet a -> SSet a -> SBool
- union :: (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
- unions :: (Ord a, SymVal a) => [SSet a] -> SSet a
- intersection :: (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
- intersections :: (Ord a, SymVal a) => [SSet a] -> SSet a
- difference :: (Ord a, SymVal a) => SSet a -> SSet a -> SSet a
- (\\) :: (Ord a, SymVal a) => SSet a -> SSet a -> SSet a

# Constructing sets

full :: forall a. HasKind a => SSet a Source #

Full set.

`>>>`

U :: {SInteger}`full :: SSet Integer`

Note that the universal set over a type is represented by the letter `U`

.

singleton :: forall a. (Ord a, SymVal a) => SBV a -> SSet a Source #

Singleton list.

`>>>`

{2} :: {SInteger}`singleton 2 :: SSet Integer`

fromList :: forall a. (Ord a, SymVal a) => [a] -> SSet a Source #

Conversion from a list.

`>>>`

{} :: {SInteger}`fromList ([] :: [Integer])`

`>>>`

{1,2,3} :: {SInteger}`fromList [1,2,3]`

`>>>`

{3,5,12} :: {SInteger}`fromList [5,5,5,12,12,3]`

complement :: forall a. (Ord a, SymVal a) => SSet a -> SSet a Source #

Complement.

`>>>`

True`empty .== complement (full :: SSet Integer)`

Complementing twice gets us back the original set:

`>>>`

Q.E.D.`prove $ \(s :: SSet Integer) -> complement (complement s) .== s`

# Equality of sets

We can compare sets for equality:

`>>>`

True`empty .== (empty :: SSet Integer)`

`>>>`

True`full .== (full :: SSet Integer)`

`>>>`

False`full ./= (full :: SSet Integer)`

`>>>`

Satisfiable. Model: s0 = U - {Just 0} :: {Maybe Integer} s1 = {} :: {Maybe Integer} s2 = U :: {Maybe Integer}`sat $ \(x::SSet (Maybe Integer)) y z -> distinct [x, y, z]`

However, if we compare two sets that are constructed as regular or in the complement form, we have to use a proof to establish equality:

`>>>`

Falsifiable`prove $ full .== (empty :: SSet Integer)`

The reason for this is that there is no way in Haskell to compare an infinite set to any other set, as infinite sets are not representable at all! So, we have to delay the judgment to the SMT solver. If you try to constant fold, you will get:

`>>>`

<symbolic> :: SBool`full .== (empty :: SSet Integer)`

indicating that the result is a symbolic value that needs a decision procedure to be determined!

# Insertion and deletion

insert :: forall a. (Ord a, SymVal a) => SBV a -> SSet a -> SSet a Source #

Insert an element into a set.

Insertion is order independent:

`>>>`

Q.E.D.`prove $ \x y (s :: SSet Integer) -> x `insert` (y `insert` s) .== y `insert` (x `insert` s)`

Deletion after insertion is not necessarily identity:

`>>>`

Falsifiable. Counter-example: s0 = 0 :: Integer s1 = {0} :: {Integer}`prove $ \x (s :: SSet Integer) -> x `delete` (x `insert` s) .== s`

But the above is true if the element isn't in the set to start with:

`>>>`

Q.E.D.`prove $ \x (s :: SSet Integer) -> x `notMember` s .=> x `delete` (x `insert` s) .== s`

Insertion into a full set does nothing:

`>>>`

Q.E.D.`prove $ \x -> insert x full .== (full :: SSet Integer)`

delete :: forall a. (Ord a, SymVal a) => SBV a -> SSet a -> SSet a Source #

Delete an element from a set.

Deletion is order independent:

`>>>`

Q.E.D.`prove $ \x y (s :: SSet Integer) -> x `delete` (y `delete` s) .== y `delete` (x `delete` s)`

Insertion after deletion is not necessarily identity:

`>>>`

Falsifiable. Counter-example: s0 = 0 :: Integer s1 = {} :: {Integer}`prove $ \x (s :: SSet Integer) -> x `insert` (x `delete` s) .== s`

But the above is true if the element is in the set to start with:

`>>>`

Q.E.D.`prove $ \x (s :: SSet Integer) -> x `member` s .=> x `insert` (x `delete` s) .== s`

Deletion from an empty set does nothing:

`>>>`

Q.E.D.`prove $ \x -> delete x empty .== (empty :: SSet Integer)`

# Query

member :: (Ord a, SymVal a) => SBV a -> SSet a -> SBool Source #

Test for membership.

`>>>`

Q.E.D.`prove $ \x -> x `member` singleton (x :: SInteger)`

`>>>`

Q.E.D.`prove $ \x (s :: SSet Integer) -> x `member` (x `insert` s)`

`>>>`

Q.E.D.`prove $ \x -> x `member` (full :: SSet Integer)`

notMember :: (Ord a, SymVal a) => SBV a -> SSet a -> SBool Source #

Test for non-membership.

`>>>`

Falsifiable. Counter-example: set = {0} :: {Integer} s0 = 0 :: Integer`prove $ \x -> x `notMember` observe "set" (singleton (x :: SInteger))`

`>>>`

Q.E.D.`prove $ \x (s :: SSet Integer) -> x `notMember` (x `delete` s)`

`>>>`

Q.E.D.`prove $ \x -> x `notMember` (empty :: SSet Integer)`

null :: HasKind a => SSet a -> SBool Source #

Is this the empty set?

`>>>`

True`null (empty :: SSet Integer)`

`>>>`

Q.E.D.`prove $ \x -> null (x `delete` singleton (x :: SInteger))`

`>>>`

Falsifiable`prove $ null (full :: SSet Integer)`

Note how we have to call `prove`

in the last case since dealing
with infinite sets requires a call to the solver and cannot be
constant folded.

isFull :: HasKind a => SSet a -> SBool Source #

Is this the full set?

`>>>`

Falsifiable`prove $ isFull (empty :: SSet Integer)`

`>>>`

Falsifiable. Counter-example: set = U - {0} :: {Integer} s0 = 0 :: Integer`prove $ \x -> isFull (observe "set" (x `delete` (full :: SSet Integer)))`

`>>>`

True`isFull (full :: SSet Integer)`

Note how we have to call `prove`

in the first case since dealing
with infinite sets requires a call to the solver and cannot be
constant folded.

hasSize :: (Ord a, SymVal a) => SSet a -> SInteger -> SBool Source #

Does the set have the given size? It implicitly asserts that the set
it is operating on is finite. Also see `card`

.

`>>>`

Q.E.D.`prove $ \i -> hasSize (empty :: SSet Integer) i .== (i .== 0)`

`>>>`

Unsatisfiable`sat $ \i -> hasSize (full :: SSet Integer) i`

- >>> prove $ a b i j k -> hasSize (a :: SSet Integer) i .&& hasSize (b :: SSet Integer) j .&& hasSize (a
`union`

b) k .=> k .>= i`smax`

j Q.E.D. - >>> prove $ a b i j k -> hasSize (a :: SSet Integer) i .&& hasSize (b :: SSet Integer) j .&& hasSize (a
`intersection`

b) k .=> k .<= i`smin`

j Q.E.D. - >>> prove $ a k -> hasSize (a :: SSet Integer) k .=> k .>= 0 Q.E.D.

isSubsetOf :: (Ord a, SymVal a) => SSet a -> SSet a -> SBool Source #

Subset test.

`>>>`

Q.E.D.`prove $ empty `isSubsetOf` (full :: SSet Integer)`

`>>>`

Q.E.D.`prove $ \x (s :: SSet Integer) -> s `isSubsetOf` (x `insert` s)`

`>>>`

Q.E.D.`prove $ \x (s :: SSet Integer) -> (x `delete` s) `isSubsetOf` s`

isProperSubsetOf :: (Ord a, SymVal a) => SSet a -> SSet a -> SBool Source #

Proper subset test.

`>>>`

Q.E.D.`prove $ empty `isProperSubsetOf` (full :: SSet Integer)`

`>>>`

Falsifiable. Counter-example: s0 = 0 :: Integer s1 = U :: {Integer}`prove $ \x (s :: SSet Integer) -> s `isProperSubsetOf` (x `insert` s)`

`>>>`

Q.E.D.`prove $ \x (s :: SSet Integer) -> x `notMember` s .=> s `isProperSubsetOf` (x `insert` s)`

`>>>`

Falsifiable. Counter-example: s0 = 0 :: Integer s1 = U - {0,1} :: {Integer}`prove $ \x (s :: SSet Integer) -> (x `delete` s) `isProperSubsetOf` s`

`>>>`

Q.E.D.`prove $ \x (s :: SSet Integer) -> x `member` s .=> (x `delete` s) `isProperSubsetOf` s`

disjoint :: (Ord a, SymVal a) => SSet a -> SSet a -> SBool Source #

Disjoint test.

`>>>`

True`disjoint (fromList [2,4,6]) (fromList [1,3])`

`>>>`

False`disjoint (fromList [2,4,6,8]) (fromList [2,3,5,7])`

`>>>`

False`disjoint (fromList [1,2]) (fromList [1,2,3,4])`

`>>>`

Q.E.D.`prove $ \(s :: SSet Integer) -> s `disjoint` complement s`

`>>>`

Solution #1: s0 = {} :: {Integer} This is the only solution.`allSat $ \(s :: SSet Integer) -> s `disjoint` s`

The last example is particularly interesting: The empty set is the
only set where `disjoint`

is not reflexive!

Note that disjointness of a set from its complement is guaranteed by the fact that all types are inhabited; an implicit assumption we have in classic logic which is also enjoyed by Haskell due to the presence of bottom!

# Combinations

union :: (Ord a, SymVal a) => SSet a -> SSet a -> SSet a Source #

Union.

`>>>`

True`union (fromList [1..10]) (fromList [5..15]) .== (fromList [1..15] :: SSet Integer)`

`>>>`

Q.E.D.`prove $ \(a :: SSet Integer) b -> a `union` b .== b `union` a`

`>>>`

Q.E.D.`prove $ \(a :: SSet Integer) b c -> a `union` (b `union` c) .== (a `union` b) `union` c`

`>>>`

Q.E.D.`prove $ \(a :: SSet Integer) -> a `union` full .== full`

`>>>`

Q.E.D.`prove $ \(a :: SSet Integer) -> a `union` empty .== a`

`>>>`

Q.E.D.`prove $ \(a :: SSet Integer) -> a `union` complement a .== full`

intersection :: (Ord a, SymVal a) => SSet a -> SSet a -> SSet a Source #

Intersection.

`>>>`

True`intersection (fromList [1..10]) (fromList [5..15]) .== (fromList [5..10] :: SSet Integer)`

`>>>`

Q.E.D.`prove $ \(a :: SSet Integer) b -> a `intersection` b .== b `intersection` a`

`>>>`

Q.E.D.`prove $ \(a :: SSet Integer) b c -> a `intersection` (b `intersection` c) .== (a `intersection` b) `intersection` c`

`>>>`

Q.E.D.`prove $ \(a :: SSet Integer) -> a `intersection` full .== a`

`>>>`

Q.E.D.`prove $ \(a :: SSet Integer) -> a `intersection` empty .== empty`

`>>>`

Q.E.D.`prove $ \(a :: SSet Integer) -> a `intersection` complement a .== empty`

`>>>`

Q.E.D.`prove $ \(a :: SSet Integer) b -> a `disjoint` b .=> a `intersection` b .== empty`

intersections :: (Ord a, SymVal a) => [SSet a] -> SSet a Source #

Intersections. Equivalent to

. Note that
Haskell's `foldr`

`intersection`

`full`

`Set`

does not support this operation as it does not have a
way of representing universal sets.

`>>>`

Q.E.D.`prove $ intersections [] .== (full :: SSet Integer)`

difference :: (Ord a, SymVal a) => SSet a -> SSet a -> SSet a Source #

Difference.

`>>>`

Q.E.D.`prove $ \(a :: SSet Integer) -> empty `difference` a .== empty`

`>>>`

Q.E.D.`prove $ \(a :: SSet Integer) -> a `difference` empty .== a`

`>>>`

Q.E.D.`prove $ \(a :: SSet Integer) -> full `difference` a .== complement a`

`>>>`

Q.E.D.`prove $ \(a :: SSet Integer) -> a `difference` a .== empty`