And

Posted on 2018-01-15 by nbloomf

Tags: arithmetic-made-difficult, literate-haskell

\(\newcommand{\hyp}[2]{\stackrel{\tiny\text{hyp}}{#2}}\) \(\newcommand{\let}[2]{\stackrel{\tiny\text{let}}{#2}}\) \(\newcommand{\a}{a}\) \(\newcommand{\b}{b}\) \(\newcommand{\c}{c}\) \(\newcommand{\p}{p}\) \(\newcommand{\q}{q}\) \(\newcommand{\r}{r}\) \(\newcommand{\s}{s}\) \(\newcommand{\x}{x}\) \(\newcommand{\y}{y}\) \(\newcommand{\z}{z}\) \(\newcommand{\bool}{\mathbb{B}}\) \(\newcommand{\btrue}{\mathsf{true}}\) \(\newcommand{\bfalse}{\mathsf{false}}\) \(\newcommand{\bnot}{\mathsf{not}}\) \(\newcommand{\band}{\mathbin{\mathsf{and}}}\) \(\newcommand{\bor}{\mathbin{\mathsf{or}}}\) \(\newcommand{\bimpl}{\mathbin{\mathsf{impl}}}\) \(\newcommand{\beq}{\mathsf{eq}}\) \(\newcommand{\bif}[3]{\mathsf{if}\left(#1,#2,#3\right)}\) \(\newcommand{\id}{\mathsf{id}}\) \(\newcommand{\compose}{\mathsf{compose}}\) \(\newcommand{\const}{\mathsf{const}}\) \(\newcommand{\apply}{\mathsf{apply}}\) \(\newcommand{\flip}{\mathsf{flip}}\) \(\newcommand{\flipB}{\mathsf{flip2}}\) \(\newcommand{\flipC}{\mathsf{flip3}}\) \(\newcommand{\flipD}{\mathsf{flip4}}\) \(\newcommand{\flipE}{\mathsf{flip5}}\) \(\newcommand{\clone}{\mathsf{clone}}\) \(\newcommand{\cloneC}{\mathsf{clone3}}\) \(\newcommand{\composeAonB}{\mathsf{compose1on2}}\) \(\newcommand{\composeAonC}{\mathsf{compose1on3}}\) \(\newcommand{\composeAonD}{\mathsf{compose1on4}}\) \(\newcommand{\composeBonA}{\mathsf{compose2on1}}\) \(\newcommand{\composeBonB}{\mathsf{compose2on2}}\) \(\newcommand{\composeConA}{\mathsf{compose3on1}}\) \(\newcommand{\ptrue}{\mathsf{ptrue}}\) \(\newcommand{\pfalse}{\mathsf{pfalse}}\) \(\newcommand{\pnot}{\mathsf{pnot}}\) \(\newcommand{\pand}{\mathbin{\mathsf{pand}}}\) \(\newcommand{\por}{\mathbin{\mathsf{por}}}\) \(\newcommand{\pimpl}{\mathbin{\mathsf{pimpl}}}\) \(\newcommand{\fst}{\mathsf{first}}\) \(\newcommand{\snd}{\mathsf{second}}\) \(\newcommand{\dup}{\mathsf{dup}}\) \(\newcommand{\tup}{\mathsf{tup}}\) \(\newcommand{\tSwap}{\mathsf{swap}_{\times}}\) \(\newcommand{\tPair}{\mathsf{pair}_{\times}}\) \(\newcommand{\tAssocL}{\mathsf{assocL}_{\times}}\) \(\newcommand{\tAssocR}{\mathsf{assocR}_{\times}}\) \(\newcommand{\tupL}{\mathsf{tupL}}\) \(\newcommand{\tupR}{\mathsf{tupR}}\) \(\newcommand{\uncurry}{\mathsf{uncurry}}\) \(\newcommand{\curry}{\mathsf{curry}}\) \(\newcommand{\lft}{\mathsf{left}}\) \(\newcommand{\rgt}{\mathsf{right}}\) \(\newcommand{\either}{\mathsf{either}}\) \(\newcommand{\uSwap}{\mathsf{swap}_{+}}\) \(\newcommand{\uPair}{\mathsf{pair}_{+}}\) \(\newcommand{\uAssocL}{\mathsf{assocL}_{+}}\) \(\newcommand{\uAssocR}{\mathsf{assocR}_{+}}\) \(\newcommand{\isLft}{\mathsf{isLeft}}\) \(\newcommand{\isRgt}{\mathsf{isRight}}\) \(\newcommand{\nats}{\mathbb{N}}\) \(\newcommand{\zero}{\mathsf{0}}\) \(\newcommand{\next}{\mathsf{next}}\) \(\newcommand{\unnext}{\mathsf{unnext}}\) \(\newcommand{\iszero}{\mathsf{isZero}}\) \(\newcommand{\prev}{\mathsf{prev}}\) \(\newcommand{\natrec}{\mathsf{natrec}}\) \(\newcommand{\simprec}{\mathsf{simprec}}\) \(\newcommand{\bailrec}{\mathsf{bailrec}}\) \(\newcommand{\mutrec}{\mathsf{mutrec}}\) \(\newcommand{\dnatrec}{\mathsf{dnatrec}}\) \(\newcommand{\normrec}{\mathsf{normrec}}\) \(\newcommand{\findsmallest}{\mathsf{findsmallest}}\) \(\newcommand{\mnormrec}{\mathsf{mnormrec}}\) \(\newcommand{\nequal}{\mathsf{eq}}\) \(\newcommand{\nplus}{\mathsf{plus}}\) \(\newcommand{\ntimes}{\mathsf{times}}\) \(\newcommand{\nleq}{\mathsf{leq}}\) \(\newcommand{\ngeq}{\mathsf{geq}}\) \(\newcommand{\nminus}{\mathsf{minus}}\) \(\newcommand{\nmax}{\mathsf{max}}\) \(\newcommand{\nmin}{\mathsf{min}}\) \(\newcommand{\ndivalg}{\mathsf{divalg}}\) \(\newcommand{\nquo}{\mathsf{quo}}\) \(\newcommand{\nrem}{\mathsf{rem}}\) \(\newcommand{\ndiv}{\mathsf{div}}\) \(\newcommand{\ngcd}{\mathsf{gcd}}\) \(\newcommand{\ncoprime}{\mathsf{coprime}}\) \(\newcommand{\nlcm}{\mathsf{lcm}}\) \(\newcommand{\nmindiv}{\mathsf{mindiv}}\) \(\newcommand{\nisprime}{\mathsf{isPrime}}\) \(\newcommand{\npower}{\mathsf{power}}\) \(\newcommand{\nchoose}{\mathsf{choose}}\) \(\newcommand{\dom}{\mathsf{dom}}\) \(\newcommand{\cod}{\mathsf{cod}}\) \(\newcommand{\lists}[1]{\mathsf{List}(#1)}\) \(\newcommand{\nil}{\mathsf{nil}}\) \(\newcommand{\cons}{\mathsf{cons}}\) \(\newcommand{\uncons}{\mathsf{uncons}}\) \(\newcommand{\isnil}{\mathsf{isNil}}\) \(\newcommand{\tail}{\mathsf{tail}}\) \(\newcommand{\head}{\mathsf{head}}\) \(\newcommand{\foldr}{\mathsf{foldr}}\) \(\newcommand{\foldl}{\mathsf{foldl}}\) \(\newcommand{\tacunfoldN}{\mathsf{tacunfoldN}}\) \(\newcommand{\unfoldN}{\mathsf{unfoldN}}\) \(\newcommand{\dfoldr}{\mathsf{dfoldr}}\) \(\newcommand{\cfoldr}{\mathsf{cfoldr}}\) \(\newcommand{\bfoldr}{\mathsf{bfoldr}}\) \(\newcommand{\dbfoldr}{\mathsf{dbfoldr}}\) \(\newcommand{\lfoldr}{\mathsf{lfoldr}}\) \(\newcommand{\snoc}{\mathsf{snoc}}\) \(\newcommand{\revcat}{\mathsf{revcat}}\) \(\newcommand{\rev}{\mathsf{rev}}\) \(\newcommand{\last}{\mathsf{last}}\) \(\newcommand{\cat}{\mathsf{cat}}\) \(\newcommand{\addlength}{\mathsf{addlength}}\) \(\newcommand{\length}{\mathsf{length}}\) \(\newcommand{\head}{\mathsf{head}}\) \(\newcommand{\at}{\mathsf{at}}\) \(\newcommand{\map}{\mathsf{map}}\) \(\newcommand{\range}{\mathsf{range}}\) \(\newcommand{\zip}{\mathsf{zip}}\) \(\newcommand{\zipPad}{\mathsf{zipPad}}\) \(\newcommand{\unzip}{\mathsf{unzip}}\) \(\newcommand{\prefix}{\mathsf{prefix}}\) \(\newcommand{\suffix}{\mathsf{suffix}}\) \(\newcommand{\lcp}{\mathsf{lcp}}\) \(\newcommand{\lcs}{\mathsf{lcs}}\) \(\newcommand{\all}{\mathsf{all}}\) \(\newcommand{\any}{\mathsf{any}}\) \(\newcommand{\tails}{\mathsf{tails}}\) \(\newcommand{\inits}{\mathsf{inits}}\) \(\newcommand{\filter}{\mathsf{filter}}\) \(\newcommand{\elt}{\mathsf{elt}}\) \(\newcommand{\addcount}{\mathsf{addcount}}\) \(\newcommand{\count}{\mathsf{count}}\) \(\newcommand{\repeat}{\mathsf{repeat}}\) \(\newcommand{\sublist}{\mathsf{sublist}}\) \(\newcommand{\infix}{\mathsf{infix}}\) \(\newcommand{\select}{\mathsf{select}}\) \(\newcommand{\unique}{\mathsf{unique}}\) \(\newcommand{\delete}{\mathsf{delete}}\) \(\newcommand{\dedupeL}{\mathsf{dedupeL}}\) \(\newcommand{\dedupeR}{\mathsf{dedupeR}}\) \(\newcommand{\common}{\mathsf{common}}\) \(\newcommand{\disjoint}{\mathsf{disjoint}}\) \(\newcommand{\sublists}{\mathsf{sublists}}\) \(\newcommand{\take}{\mathsf{take}}\) \(\newcommand{\drop}{\mathsf{drop}}\) \(\newcommand{\takeBut}{\mathsf{takeBut}}\) \(\newcommand{\dropBut}{\mathsf{dropBut}}\) \(\newcommand{\takeWhile}{\mathsf{takeWhile}}\) \(\newcommand{\dropWhile}{\mathsf{dropWhile}}\)

This page is part of a series on Arithmetic Made Difficult.

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

{-# LANGUAGE NoImplicitPrelude #-}
module And (
  and, _test_and, main_and
) where

import Testing
import Booleans
import Not

Next, \(\band\).

We define a map \(\band : \bool \rightarrow \bool \rightarrow \bool\) by \[\band(p,q) = \bif{p}{\bif{q}{\btrue}{\bfalse}}{\bfalse}.\]

In Haskell:

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

We can compute \(\band\) explicitly.

We have \[\begin{eqnarray*} \band(\btrue,\btrue) & = & \btrue \\ \band(\btrue,\bfalse) & = & \bfalse \\ \band(\bfalse,\btrue) & = & \bfalse \\ \band(\bfalse,\bfalse) & = & \bfalse. \end{eqnarray*}\]

Note that \[\begin{eqnarray*} & & \band(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/And.html#def-and} = & \bif{\btrue}{\bif{\btrue}{\btrue}{\bfalse}}{\bfalse} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{\btrue}{\btrue}{\bfalse} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \btrue \end{eqnarray*}\] that \[\begin{eqnarray*} & & \band(\btrue,\bfalse) \\ & \href{/posts/arithmetic-made-difficult/And.html#def-and} = & \bif{\btrue}{\bif{\bfalse}{\btrue}{\bfalse}}{\bfalse} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\btrue}{\bfalse}{\bfalse} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bfalse \end{eqnarray*}\] that \[\begin{eqnarray*} & & \band(\bfalse,\btrue) \\ & \href{/posts/arithmetic-made-difficult/And.html#def-and} = & \bif{\bfalse}{\bif{\btrue}{\btrue}{\bfalse}}{\bfalse} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bfalse \end{eqnarray*}\] and that \[\begin{eqnarray*} & & \band(\bfalse,\bfalse) \\ & \href{/posts/arithmetic-made-difficult/And.html#def-and} = & \bif{\bfalse}{\bif{\bfalse}{\btrue}{\bfalse}}{\bfalse} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bfalse \end{eqnarray*}\] as claimed.

_test_and_true_true :: (Boolean b, Equal b)
  => b -> Test Bool
_test_and_true_true p =
  testName "and(true,true) == true" $
  eq (and true true) (true `withTypeOf` p)


_test_and_true_false :: (Boolean b, Equal b)
  => b -> Test Bool
_test_and_true_false p =
  testName "and(true,false) == false" $
  eq (and true false) (false `withTypeOf` p)


_test_and_false_true :: (Boolean b, Equal b)
  => b -> Test Bool
_test_and_false_true p =
  testName "and(false,true) == false" $
  eq (and false true) (false `withTypeOf` p)


_test_and_false_false :: (Boolean b, Equal b)
  => b -> Test Bool
_test_and_false_false p =
  testName "and(false,false) == false" $
  eq (and false false) (false `withTypeOf` p)

\(\bfalse\) absorbs under \(\band\).

If \(a \in \bool\), we have \[\band(\bfalse,a) = \band(a,\bfalse) = \bfalse.\]

If \(a = \btrue\) we have \[\begin{eqnarray*} & & \band(\bfalse,\btrue) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-eval-false-true} = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-eval-true-false} = & \band(\btrue,\bfalse) \end{eqnarray*}\] and if \(a = \bfalse\) we have \[\begin{eqnarray*} & & \band(\bfalse,\bfalse) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-eval-false-false} = & \bfalse \end{eqnarray*}\] as claimed.

_test_and_false :: (Boolean b, Equal b)
  => b -> Test (b -> Bool)
_test_and_false b =
  testName "and(false,p) == false" $
  \p -> eq (and false p) (false `withTypeOf` b)

\(\btrue\) is neutral under \(\band\).

If \(a \in \bool\), we have \[\band(\btrue,a) = \band(a,\btrue) = a.\]

If \(a = \btrue\) we have \[\begin{eqnarray*} & & \band(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-eval-true-true} = & \btrue \end{eqnarray*}\] and if \(a = \bfalse\) we have \[\begin{eqnarray*} & & \band(\btrue,\bfalse) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-eval-true-false} = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-eval-false-true} = & \band(\bfalse,\btrue) \end{eqnarray*}\] as claimed.

_test_and_true :: (Boolean b, Equal b)
  => b -> Test (b -> Bool)
_test_and_true _ =
  testName "and(true,p) == p" $
  \p -> eq (and true p) p

\(\band\) interacts with \(\bnot\).

If \(a \in \bool\), we have \(\band(a,\bnot(a)) = \bfalse\).

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

_test_and_not :: (Boolean b, Equal b)
 => b -> Test (b -> Bool)
_test_and_not b =
  testName "and(p,not(p)) == false" $
  \p -> eq (and p (not p)) (false `withTypeOf` b)

\(\band\) is idempotent.

If \(a \in \bool\), we have \(\band(a,a) = a\).

If \(a = \btrue\) we have \[\begin{eqnarray*} & & \band(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-eval-true-true} = & \btrue \end{eqnarray*}\] and if \(a = \bfalse\) we have \[\begin{eqnarray*} & & \band(\bfalse,\bfalse) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-eval-false-false} = & \bfalse \end{eqnarray*}\] as claimed.

_test_and_idempotent :: (Boolean b, Equal b)
  => b -> Test (b -> Bool)
_test_and_idempotent _ =
  testName "and(p,p) == p" $
  \p -> eq (and p p) p

\(\band\) is commutative.

If \(a,b \in \bool\), we have \(\band(a,b) = \band(b,a)\).

If \(a = \btrue\) we have \[\begin{eqnarray*} & & \band(\btrue,b) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & b \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-right} = & \band(b,\btrue) \end{eqnarray*}\] and if \(a = \bfalse\) we have \[\begin{eqnarray*} & & \band(\bfalse,b) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-right} = & \band(b,\bfalse) \end{eqnarray*}\] as claimed.

_test_and_commutative :: (Boolean b, Equal b)
  => b -> Test (b -> b -> Bool)
_test_and_commutative _ =
  testName "and(p,q) == and(q,p)" $
  \p q -> eq (and p q) (and q p)

\(\band\) is associative.

For all \(a,b,c \in \bool\), we have \[\band(\band(a,b),c) = \band(a,\band(b,c)).\]

If \(a = \btrue\), we have \[\begin{eqnarray*} & & \band(\band(a,b),c) \\ & \let{a = \btrue} = & \band(\band(\btrue,b),c) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \band(b,c) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \band(\btrue,\band(b,c)) \\ & \let{a = \btrue} = & \band(a,\band(b,c)) \end{eqnarray*}\] as claimed. If \(a = \bfalse\), we have \[\begin{eqnarray*} & & \band(\band(a,b),c) \\ & \let{a = \bfalse} = & \band(\band(\bfalse,b),c) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \band(\bfalse,c) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \band(\bfalse,\band(b,c)) \end{eqnarray*}\] as claimed.

_test_and_associative :: (Boolean b, Equal b)
  => b -> Test (b -> b -> b -> Bool)
_test_and_associative _ =
  testName "and(and(p,q),r) == and(p,and(q,r))" $
  \p q r -> eq (and (and p q) r) (and p (and q r))

\(\band\) interacts with \(\bif{\ast}{\ast}{\ast}\) in the second argument.

Let \(p,q,r \in \bool\). Then we have \[\band(p,\bif{p}{q}{r}) = \band(p,q).\]

If \(p = \btrue\), we have \[\begin{eqnarray*} & & \band(\btrue,\bif{\btrue}{q}{r}) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \band(\btrue,q) \end{eqnarray*}\] as claimed. If \(p = \bfalse\), we have \[\begin{eqnarray*} & & \band(\bfalse,\bif{\bfalse}{q}{r}) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \band(\bfalse,q) \end{eqnarray*}\] as claimed.

_test_and_if_cancel :: (Boolean b, Equal b)
  => b -> Test (b -> b -> b -> Bool)
_test_and_if_cancel _ =
  testName "and(p,if(p,q,r)) == and(p,q)" $
  \p q r -> eq (and p (ifThenElse p q r)) (and p q)

\(\band\) in the hypothesis of \(\bif{\ast}{\ast}{\ast}\) expands.

Let \(A\) be a set with \(a,b \in A\), and let \(p,q \in \bool\). Then we have \[\bif{\band(p,q)}{a}{b} = \bif{p}{\bif{q}{a}{b}}{b}.\]

If \(p = \btrue\), we have \[\begin{eqnarray*} & & \bif{\band(\btrue,q)}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \bif{q}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{\btrue}{\bif{q}{a}{b}}{b} \end{eqnarray*}\] and if \(p = \bfalse\), we have \[\begin{eqnarray*} & & \bif{\band(\bfalse,q)}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \bif{\bfalse}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & b \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\bfalse}{\bif{q}{a}{b}}{b} \end{eqnarray*}\] as claimed.

_test_and_if_hypothesis :: (Boolean b, Equal b, Equal a)
  => b -> a -> Test (b -> b -> a -> a -> Bool)
_test_and_if_hypothesis _ _ =
  testName "if(and(p,q),a,b) == if(p,if(q,a,b),b)" $
  \p q a b -> eq
    (ifThenElse (and p q) a b)
    (ifThenElse p (ifThenElse q a b) b)

Testing

Suite:

_test_and ::
  ( Equal a, Arbitrary a, CoArbitrary a, Show a, TypeName a
  , Boolean b, Arbitrary b, Show b, Equal b, TypeName b
  )
  => b -> a -> Int -> Int -> IO ()
_test_and p x size cases = do
  testLabel2 "and" p x

  let args = testArgs size cases

  runTest args (_test_and_true_true p)
  runTest args (_test_and_true_false p)
  runTest args (_test_and_false_true p)
  runTest args (_test_and_false_false p)
  runTest args (_test_and_false p)
  runTest args (_test_and_true p)
  runTest args (_test_and_not p)
  runTest args (_test_and_idempotent p)
  runTest args (_test_and_commutative p)
  runTest args (_test_and_associative p)
  runTest args (_test_and_if_cancel p)
  runTest args (_test_and_if_hypothesis p x)

Main:

main_and :: IO ()
main_and = _test_and (true :: Bool) (true :: Bool) 20 100