---
title: Disjoint
author: nbloomf
date: 2018-01-22
tags: arithmetic-made-difficult, literate-haskell
slug: disjoint
---

> {-# LANGUAGE NoImplicitPrelude #-}
> module Disjoint (
>   disjoint, _test_disjoint, main_disjoint
> ) where
> 
> import Testing
> import Booleans
> import And
> import NaturalNumbers
> import Lists
> import HeadAndTail
> import Reverse
> import Cat
> import Dedupe
> import Common

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

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

In Haskell:

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

::::::::::::::::::::

$\nil$ is disjoint with every list.

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

::: proof ::::::::::
Note that
$$\begin{eqnarray*}
 &   & \disjoint(\nil,x) \\
 & = & \isnil(\common(\nil,x)) \\
 & = & \isnil(\nil) \\
 &     \href{@head-tail@#thm-isnil-nil}
   = & \btrue
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

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

:::::: theorem :::::
Let $A$ be a set. For all $x,y \in \lists{A}$ we have $$\disjoint(x,\dedupeL(y)) = \disjoint(x,y).$$

::: proof ::::::::::
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 :::::::::::

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

:::::: theorem :::::
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)).$$

::: proof ::::::::::
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 :::::::::::

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

:::::: theorem :::::
Let $A$ be a set. For all $x,y \in \lists{A}$ we have $$\disjoint(x,\rev(y)) = \disjoint(x,y).$$

::: proof ::::::::::
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 :::::::::::

> _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)