# Not

Posted on 2018-01-14 by nbloomf

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

{-# LANGUAGE NoImplicitPrelude #-}
module Not (
not, _test_not, main_not
) where

import Testing
import Booleans

In the last post, we defined the booleans $$\bool$$. We can define the usual logical operators in terms of $$\bif{\ast}{\ast}{\ast}$$. First, $$\bnot$$.

We define $$\bnot : \bool \rightarrow \bool$$ by $\bnot(p) = \bif{p}{\bfalse}{\btrue}.$

not :: (Boolean b) => b -> b
not p = ifThenElse p false true

We can compute $$\bnot$$ explicitly.

We have $$\bnot(\btrue) = \bfalse$$ and $$\bnot(\bfalse) = \btrue$$.

Note that $\begin{eqnarray*} & & \bnot(\btrue) \\ & \href{/posts/arithmetic-made-difficult/Not.html#def-not} = & \bif{\btrue}{\bfalse}{\btrue} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bfalse \end{eqnarray*}$ and $\begin{eqnarray*} & & \bnot(\bfalse) \\ & \href{/posts/arithmetic-made-difficult/Not.html#def-not} = & \bif{\bfalse}{\bfalse}{\btrue} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \btrue \end{eqnarray*}$ as claimed.

_test_not_true :: (Boolean b, Equal b)
=> b -> Test Bool
_test_not_true p =
testName "not(true) == false" $eq (not (true withTypeOf p)) false _test_not_false :: (Boolean b, Equal b) => b -> Test Bool _test_not_false p = testName "not(false) == true"$
eq (not (false withTypeOf p)) true

$$\bnot$$ is an involution.

For all $$a \in \bool$$ we have $$\bnot(\bnot(a)) = a$$.

If $$a = \btrue$$ we have $\begin{eqnarray*} & & \bnot(\bnot(\btrue)) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-true} = & \bnot(\bfalse) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-false} = & \btrue \end{eqnarray*}$ and if $$a = \bfalse$$, we have $\begin{eqnarray*} & & \bnot(\bnot(\bfalse)) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-false} = & \bnot(\btrue) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-true} = & \bfalse \end{eqnarray*}$ as claimed.

_test_not_involutive :: (Boolean b, Equal b)
=> b -> Test (b -> Bool)
_test_not_involutive _ =
testName "not(not(p)) == p" $\p -> eq (not (not p)) p $$\bif{\ast}{\ast}{\ast}$$ interacts with $$\bnot$$. Let $$A$$ be a set with $$p \in \bool$$ and $$a,b \in A$$. We have $\bif{\bnot(p)}{a}{b} = \bif{p}{b}{a}.$ If $$p = \btrue$$, we have $\begin{eqnarray*} & & \bif{\bnot(p)}{a}{b} \\ & \let{p = \btrue} = & \bif{\bnot(\btrue)}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-true} = & \bif{\bfalse}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & b \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{\btrue}{b}{a} \\ & \let{p = \btrue} = & \bif{p}{b}{a} \end{eqnarray*}$ and if $$p = \bfalse$$, we have $\begin{eqnarray*} & & \bif{\bnot(p)}{a}{b} \\ & \let{p = \bfalse} = & \bif{\bnot(\bfalse)}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-false} = & \bif{\btrue}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & a \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\bfalse}{b}{a} \\ & \let{p = \bfalse} = & \bif{p}{b}{a} \end{eqnarray*}$ as needed. _test_if_not :: (Equal a) => a -> Test (Bool -> a -> a -> Bool) _test_if_not _ = testName "if(not(p),a,b) == if(p,b,a)"$
\p a b -> eq (ifThenElse (not p) a b) (ifThenElse p b a)

## Testing

Suite:

_test_not ::
( Equal a, Show a, Arbitrary a, CoArbitrary a, TypeName a
, Equal b, Show b, Arbitrary b, CoArbitrary b, TypeName b, Boolean b
) => Int -> Int -> b -> a -> IO ()

_test_not size cases p x = do
testLabel2 "Bool" p x

let args = testArgs size cases

runTest args (_test_not_true p)
runTest args (_test_not_false p)
runTest args (_test_not_involutive p)
runTest args (_test_if_not x)

Main:

main_not :: IO ()
main_not = do
_test_not 20 100 (true :: Bool) ()
_test_not 20 100 (true :: Bool) (true :: Bool)