# Disjoint

Posted on 2018-01-22 by nbloomf

This post is literate Haskell; you can load the source into GHCi and play along.

{-# LANGUAGE NoImplicitPrelude #-}
module Disjoint (
disjoint, _test_disjoint, main_disjoint
) where

import Testing
import Booleans
import And
import NaturalNumbers
import Lists
import Reverse
import Cat
import Dedupe
import Common

Today we’ll define a relation to detect when two lists have no items in common.

We define $$\disjoint : \lists{A} \times \lists{A} \rightarrow \bool$$ by $\disjoint(x,y) = \isnil(\common(x,y)).$

disjoint :: (List t, Equal a) => t a -> t a -> Bool
disjoint x y = isNil (common x y)

$$\nil$$ is disjoint with every list.

Let $$A$$ be a set. For all $$x \in \lists{A}$$, we have $\disjoint(\nil,x) = \btrue.$

Note that $\begin{eqnarray*} & & \disjoint(\nil,x) \\ & = & \isnil(\common(\nil,x)) \\ & = & \isnil(\nil) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-isnil-nil} = & \btrue \end{eqnarray*}$ as claimed.

_test_disjoint_nil :: (List t, Equal a, Equal (t a))
=> t a -> Test (t a -> Bool)
_test_disjoint_nil _ =
testName "disjoint(nil,x) == true" $\x -> eq (disjoint nil x) true $$\disjoint$$ interacts with $$\dedupeL$$. Let $$A$$ be a set. For all $$x,y \in \lists{A}$$ we have $\disjoint(x,\dedupeL(y)) = \disjoint(x,y).$ Note that $\begin{eqnarray*} & & \disjoint(x,\dedupeL(y)) \\ & = & \isnil(\common(x,\dedupeL(y))) \\ & = & \isnil(\common(x,y)) \\ & = & \disjoint(x,y) \end{eqnarray*}$ as claimed. _test_disjoint_dedupeL_right :: (List t, Equal a, Equal (t a)) => t a -> Test (t a -> t a -> Bool) _test_disjoint_dedupeL_right _ = testName "disjoint(x,dedupeL(y)) == disjoint(x,y)"$
\x y -> eq
(disjoint x (dedupeL y))
(disjoint x y)

Disjoint interacts with $$\cat$$.

Let $$A$$ be a set. For all $$x,y,z \in \lists{A}$$ we have $\disjoint(\cat(x,y),z) = \band(\disjoint(x,z),\disjoint(y,z)).$

Note that $\begin{eqnarray*} & & \disjoint(\cat(x,y),z) \\ & = & \isnil(\common(\cat(x,y),z)) \\ & = & \isnil(\cat(\common(x,z),\common(y,z))) \\ & = & \band(\isnil(\common(x,z)),\isnil(\common(y,z))) \\ & = & \band(\disjoint(x,z),\disjoint(y,z)) \end{eqnarray*}$ as claimed.

_test_disjoint_cat_left :: (List t, Equal a, Equal (t a))
=> t a -> Test (t a -> t a -> t a -> Bool)
_test_disjoint_cat_left _ =
testName "disjoint(cat(x,y),z) == and(disjoint(x,z),disjoint(y,z))" $\x y z -> eq (disjoint (cat x y) z) (and (disjoint x z) (disjoint y z)) $$\disjoint$$ interacts with $$\rev$$. Let $$A$$ be a set. For all $$x,y \in \lists{A}$$ we have $\disjoint(x,\rev(y)) = \disjoint(x,y).$ Note that $\begin{eqnarray*} & & \disjoint(x,\rev(y)) \\ & = & \isnil(\common(x,\rev(y))) \\ & = & \isnil(\common(x,y)) \\ & = & \disjoint(x,y) \end{eqnarray*}$ as claimed. _test_disjoint_rev_right :: (List t, Equal a, Equal (t a)) => t a -> Test (t a -> t a -> Bool) _test_disjoint_rev_right _ = testName "disjoint(x,rev(y)) == disjoint(x,y)"$
\x y -> eq
(disjoint x (rev y))
(disjoint x y)

## Testing

Suite:

_test_disjoint ::
( TypeName a, Equal a, Show a, Arbitrary a, CoArbitrary a
, TypeName (t a), List t
, Equal (t a), Show (t a), Arbitrary (t a), Equal (t (t a))
) => Int -> Int -> t a -> IO ()
_test_disjoint size cases t = do
testLabel1 "disjoint" t

let args = testArgs size cases

runTest args (_test_disjoint_nil t)
runTest args (_test_disjoint_dedupeL_right t)
runTest args (_test_disjoint_cat_left t)
runTest args (_test_disjoint_rev_right t)

Main:

main_disjoint :: IO ()
main_disjoint = do
_test_disjoint 20 100 (nil :: ConsList Bool)
_test_disjoint 20 100 (nil :: ConsList Unary)