Empty set.

>>> empty :: SSet Integer
{} :: {SInteger}

Full set.

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

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

Synonym for full.

Singleton list.

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

Conversion from a list.

>>> fromList ([] :: [Integer])
{} :: {SInteger}
>>> fromList [1,2,3]
{1,2,3} :: {SInteger}
>>> fromList [5,5,5,12,12,3]
{3,5,12} :: {SInteger}

Complement.

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

Complementing twice gets us back the original set:

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

Insert an element into a set.

Insertion is order independent:

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

Deletion after insertion is not necessarily identity:

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

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

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

Insertion into a full set does nothing:

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

Delete an element from a set.

Deletion is order independent:

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

Insertion after deletion is not necessarily identity:

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

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

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

Deletion from an empty set does nothing:

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

Test for membership.

>>> 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)
Q.E.D.

Test for non-membership.

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

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

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

Is this the empty set?

>>> null (empty :: SSet Integer)
True

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

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

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.

Synonym for null.

Is this the full set?

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

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

>>> isFull (full :: SSet Integer)
True

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.

Synonym for isFull.

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

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

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

>>> 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.

Subset test.

>>> 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
Q.E.D.

Proper subset test.

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

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

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

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

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

Disjoint test.

>>> disjoint (fromList [2,4,6])   (fromList [1,3])
True
>>> disjoint (fromList [2,4,6,8]) (fromList [2,3,5,7])
False
>>> disjoint (fromList [1,2])     (fromList [1,2,3,4])
False
>>> prove $ \(s :: SSet Integer) -> s `disjoint` complement s
Q.E.D.
>>> allSat $ \(s :: SSet Integer) -> s `disjoint` s
Solution #1:
  s0 = {} :: {Integer}
This is the only solution.

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!

Union.

>>> union (fromList [1..10]) (fromList [5..15]) .== (fromList [1..15] :: SSet Integer)
True
>>> 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
Q.E.D.

Unions. Equivalent to foldr union empty.

>>> prove $ unions [] .== (empty :: SSet Integer)
Q.E.D.

Intersection.

>>> intersection (fromList [1..10]) (fromList [5..15]) .== (fromList [5..10] :: SSet Integer)
True
>>> 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
Q.E.D.

Intersections. Equivalent to foldr intersection full. Note that Haskell's Set does not support this operation as it does not have a way of representing universal sets.

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

Difference.

>>> 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
Q.E.D.

Synonym for difference.