Predicates

Posted on 2018-01-07 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 Predicates (
  pnot, pand, por, ptrue, pfalse, _test_predicate, main_predicate
) where

import Testing
import Booleans
import Not
import And
import Or

In the last post we defined the algebra of boolean values, true and false. Today we’ll look at predicates – functions from some set $A$ to $\bool$. It turns out the algebra on $\bool$ can be lifted to predicates, and is useful enough to collect some definitions and properties in one place.

Let $A$ be a set. A predicate on $A$ is just a function $p : A \rightarrow \bool$. We define two special predicates, $\ptrue = \const(\btrue)$ and $\pfalse = \const(\bfalse)$.

In Haskell:

ptrue :: (Boolean b) => a -> b
ptrue _ = true

pfalse :: (Boolean b) => a -> b
pfalse _ = false

First, the basic logic operators lift.

Let $A$ be a set. We define $\pnot : \bool^A \rightarrow \bool^A$ by \[\pnot(p)(a) = \bnot(p(a)).\]

In Haskell:

pnot :: (Boolean b) => (a -> b) -> a -> b
pnot p a = not (p a)

$\pnot$ is an involution.

Let $A$ be a set. For all $p : A \rightarrow \bool$, we have \[\pnot(\pnot(p)) = p.\]

Let $a \in A$. Then we have \[\begin{eqnarray*} & & \pnot(\pnot(p))(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pnot} = & \bnot(\pnot(p)(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pnot} = & \bnot(\bnot(p(a))) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-involution} = & p(a) \end{eqnarray*}\] as needed.

_test_pnot_involutive :: (Boolean b, Equal b)
  => a -> b -> Test ((a -> b) -> a -> Bool)
_test_pnot_involutive _ b =
  testName "pnot(pnot(p)) == p" $
  \p x -> eq (pnot (pnot p) x) ((p x) `withTypeOf` b)

Special cases.

Let $A$ be a set. Then we have the following.

$\pnot(\ptrue) = \pfalse$.
$\pnot(\pfalse) = \ptrue$.
$\compose(\bnot)(\ptrue) = \pfalse$.
$\compose(\bnot)(\pfalse) = \ptrue$.

If $a \in A$, we have \[\begin{eqnarray*} & & \pnot(\ptrue)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pnot} = & \bnot(\ptrue(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-ptrue} = & \bnot(\const(\btrue)(a)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \bnot(\btrue) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-true} = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \const(\bfalse)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pfalse} = & \pfalse(a) \end{eqnarray*}\] as needed.
If $a \in A$, we have \[\begin{eqnarray*} & & \pnot(\pfalse)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pnot} = & \bnot(\pfalse(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pfalse} = & \bnot(\const(\bfalse)(a)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \bnot(\bfalse) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-false} = & \btrue \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \const(\btrue)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-ptrue} = & \ptrue(a) \end{eqnarray*}\] as needed.
If $a \in A$, we have \[\begin{eqnarray*} & & \compose(\bnot)(\ptrue)(a) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \bnot(\ptrue(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-ptrue} = & \bnot(\const(\btrue)(a)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \bnot(\btrue) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-true} = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \const(\bfalse)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pfalse} = & \pfalse(a) \end{eqnarray*}\] as needed.
If $a \in A$, we have \[\begin{eqnarray*} & & \compose(\bnot)(\pfalse)(a) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \bnot(\pfalse(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pfalse} = & \bnot(\const(\bfalse)(a)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \bnot(\bfalse) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-false} = & \btrue \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \const(\btrue)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-ptrue} = & \ptrue(a) \end{eqnarray*}\]

_test_pnot_ptrue :: (Boolean b, Equal b)
  => a -> b -> Test (a -> Bool)
_test_pnot_ptrue _ b =
  testName "pnot(ptrue) == pfalse" $
  \a -> eq ((pnot ptrue) a) ((pfalse a) `withTypeOf` b)


_test_pnot_pfalse :: (Boolean b, Equal b)
  => a -> b -> Test (a -> Bool)
_test_pnot_pfalse _ b =
  testName "pnot(pfalse) == ptrue" $
  \a -> eq ((pnot pfalse) a) ((ptrue a) `withTypeOf` b)


_test_not_ptrue :: (Boolean b, Equal b)
  => a -> b -> Test (a -> Bool)
_test_not_ptrue _ b =
  testName "(not . ptrue) == pfalse" $
  \a -> eq ((not . ptrue) a) ((pfalse a) `withTypeOf` b)


_test_not_pfalse :: (Boolean b, Equal b)
  => a -> b -> Test (a -> Bool)
_test_not_pfalse _ b =
  testName "(not . pfalse) == ptrue" $
  \a -> eq ((not . pfalse) a) ((ptrue a) `withTypeOf` b)

Next, $\pand$.

Let $A$ be a set. We define $\pand : \bool^A \times \bool^A \rightarrow \bool^A$ by \[\pand(p,q)(a) = \band(p(a),q(a)).\]

In Haskell:

pand :: (a -> Bool) -> (a -> Bool) -> a -> Bool
pand p q a = and (p a) (q a)

The usual properties of $\band$ lift to $\pand$.

Let $A$ be a set. The following hold for all p,q,r ^A$.

$\pand(\pfalse,p) = \pand(p,\pfalse) = \pfalse$.
$\pand(\ptrue,p) = \pand(p,\ptrue) = p$.
$\pand(p,p) = p$.
$\pand(p,q) = \pand(q,p)$.
$\pand(\pand(p,q),r) = \pand(p,\pand(q,r))$.

For all $a \in A$ we have \[\begin{eqnarray*} & & \pand(\pfalse,p)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pand} = & \band(\pfalse(a),p(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pfalse} = & \band(\const(\bfalse)(a),p(a)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \band(\bfalse,p(a)) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \const(\bfalse)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pfalse} = & \pfalse(a) \end{eqnarray*}\] as needed; similarly for the other equality.
For all $a \in A$, we have \[\begin{eqnarray*} & & \pand(\ptrue,p)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pand} = & \band(\ptrue(a),p(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-ptrue} = & \band(\const(\btrue)(a),p(a)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \band(\btrue,p(a)) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & p(a) \end{eqnarray*}\] as needed.
For all $a \in A$, we have \[\begin{eqnarray*} & & \pand(p,p)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pand} = & \band(p(a),p(a)) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-idempotent} = & p(a) \end{eqnarray*}\] as needed.
For all $a \in A$, we have \[\begin{eqnarray*} & & \pand(p,q)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pand} = & \band(p(a),q(a)) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-commutative} = & \band(q(a),p(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pand} = & \pand(q,p)(a) \end{eqnarray*}\] as needed.
For all $a \in A$, we have \[\begin{eqnarray*} & & \pand(\pand(p,q),r)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pand} = & \band(\pand(p,q)(a),r(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pand} = & \band(\band(p(a),q(a)),r(a)) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-associative} = & \band(p(a),\band(q(a),r(a))) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pand} = & \band(p(a),\pand(q,r)(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pand} = & \pand(p,\pand(q,r))(a) \end{eqnarray*}\] as needed.

_test_pand_pfalse
  :: a -> Test ((a -> Bool) -> a -> Bool)
_test_pand_pfalse _ =
  testName "pand(pfalse,p) == pfalse" $
  \p a -> eq ((pand pfalse p) a) (pfalse a)


_test_pand_ptrue
  :: a -> Test ((a -> Bool) -> a -> Bool)
_test_pand_ptrue _ =
  testName "pand(ptrue,p) == p" $
  \p a -> eq ((pand ptrue p) a) (p a)


_test_pand_idempotent
  :: a -> Test ((a -> Bool) -> a -> Bool)
_test_pand_idempotent _ =
  testName "pand(p,p) == p" $
  \p a -> eq ((pand p p) a) (p a)


_test_pand_commutative
  :: a -> Test ((a -> Bool) -> (a -> Bool) -> a -> Bool)
_test_pand_commutative _ =
  testName "pand(p,q) == pand(q,p)" $
  \p q a -> eq ((pand p q) a) ((pand q p) a)


_test_pand_associative
  :: a -> Test ((a -> Bool) -> (a -> Bool) -> (a -> Bool) -> a -> Bool)
_test_pand_associative _ =
  testName "pand(pand(p,q),r) == pand(p,pand(q,r))" $
  \p q r a -> eq ((pand (pand p q) r) a) ((pand p (pand q r)) a)

Then $\por$.

Let $A$ be a set. We define $\por : \bool^A \times \bool^A \rightarrow \bool^A$ by \[\por(p,q)(a) = \bor(p(a),q(a)).\]

In Haskell:

por :: (a -> Bool) -> (a -> Bool) -> a -> Bool
por p q a = or (p a) (q a)

The usual properties of $\bor$ lift to $\por$.

Let $A$ be a set. The following hold for all $p,q,r \in \bool^A$.

$\por(\ptrue,p) = \por(p,\ptrue) = \ptrue$.
$\por(\pfalse,p) = \por(p,\pfalse) = p$.
$\por(p,p) = p$.
$\por(p,q) = \por(q,p)$.
$\por(\por(p,q),r) = \por(p,\por(q,r))$.

For all $a \in A$, we have \[\begin{eqnarray*} & & \por(\ptrue,p)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-por} = & \bor(\ptrue(a),p(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-ptrue} = & \bor(\const(\btrue)(a),p(a)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \bor(\btrue,p(a)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \btrue \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \const(\btrue)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-ptrue} = & \ptrue(a) \end{eqnarray*}\] as needed; the other equality is similar.
For all $a \in A$, we have \[\begin{eqnarray*} & & \por(\pfalse,p)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-por} = & \bor(\pfalse(a),p(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pfalse} = & \bor(\const(\bfalse)(a),p(a)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \bor(\bfalse,p(a)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-left} = & p(a) \end{eqnarray*}\] as needed; the other equality is similar.
For all $a \in A$, we have \[\begin{eqnarray*} & & \por(p,p)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-por} = & \bor(p(a),p(a)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-idempotent} = & p(a) \end{eqnarray*}\] as needed.
For all $a \in A$, we have \[\begin{eqnarray*} & & \por(p,q)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-por} = & \bor(p(a),q(a)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-commutative} = & \bor(q(a),p(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-por} = & \por(q,p)(a) \end{eqnarray*}\] as needed.
For all $a \in A$, we have \[\begin{eqnarray*} & & \por(\por(p,q),r)(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-por} = & \bor(\por(p,q)(a),r(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-por} = & \bor(\bor(p(a),q(a)),r(a)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-associative} = & \bor(p(a),\bor(q(a),r(a))) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-por} = & \bor(p(a),\por(q,r)(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-por} = & \por(p,\por(q,r))(a) \end{eqnarray*}\] as needed.

_test_por_ptrue :: (Boolean b, Equal b)
  => a -> b -> Test ((a -> Bool) -> a -> Bool)
_test_por_ptrue _ _ =
  testName "por(ptrue,p) == ptrue" $
  \p a -> eq ((por ptrue p) a) (ptrue a)


_test_por_pfalse :: (Boolean b, Equal b)
  => a -> b -> Test ((a -> Bool) -> a -> Bool)
_test_por_pfalse _ _ =
  testName "por(pfalse,p) == p" $
  \p a -> eq ((por pfalse p) a) (p a)


_test_por_idempotent :: (Boolean b, Equal b)
  => a -> b -> Test ((a -> Bool) -> a -> Bool)
_test_por_idempotent _ _ =
  testName "por(p,p) == p" $
  \p a -> eq ((por p p) a) (p a)


_test_por_commutative
  :: a -> Test ((a -> Bool) -> (a -> Bool) -> a -> Bool)
_test_por_commutative _ =
  testName "por(p,q) == por(q,p)" $
  \p q a -> eq ((por p q) a) ((por q p) a)


_test_por_associative
  :: a -> Test ((a -> Bool) -> (a -> Bool) -> (a -> Bool) -> a -> Bool)
_test_por_associative _ =
  testName "por(por(p,q),r) == por(p,por(q,r))" $
  \p q r a -> eq ((por (por p q) r) a) ((por p (por q r)) a)

And $\pnot$, $\pand$, and $\por$ interact.

Let $A$ be a set. The following hold for all $p,q,r \in \bool^A$.

$\pnot(\pand(p,q)) = \por(\pnot(p),\pnot(q))$.
$\pnot(\por(p,q)) = \pand(\pnot(p),\pnot(q))$.
$\pand(p,\por(q,r)) = \por(\pand(p,q),\pand(p,r))$.
$\bor(p,\pand(q,r)) = \pand(\por(p,q),\por(p,r))$.

For all $a \in A$, we have \[\begin{eqnarray*} & & \pnot(\pand(p,q))(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pnot} = & \bnot(\pand(p,q)(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pand} = & \bnot(\band(p(a),q(a))) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-demorgan-not-and} = & \bor(\bnot(p(a)),\bnot(q(a))) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pnot} = & \bor(\pnot(p)(a),\bnot(q(a))) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pnot} = & \bor(\pnot(p)(a),\pnot(q)(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-por} = & \por(\pnot(p),\pnot(q))(a) \end{eqnarray*}\] as needed.
For all $a \in A$, we have \[\begin{eqnarray*} & & \pnot(\por(p,q))(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pnot} = & \bnot(\por(p,q)(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-por} = & \bnot(\bor(p(a),q(a))) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-demorgan-not-or} = & \band(\bnot(p(a)),\bnot(q(a))) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pnot} = & \band(\pnot(p)(a),\bnot(q(a))) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pnot} = & \band(\pnot(p)(a),\pnot(q)(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pand} = & \pand(\pnot(p),\pnot(q))(a) \end{eqnarray*}\] as needed.
For all $a \in A$, we have \[\begin{eqnarray*} & & \pand(p,\por(q,r))(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pand} = & \band(p(a),\por(q,r)(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-por} = & \band(p(a),\bor(q(a),r(a))) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-and-or-distribute} = & \bor(\band(p(a),q(a)),\band(p(a),r(a))) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pand} = & \bor(\pand(p,q)(a),\band(p(a),r(a))) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pand} = & \bor(\pand(p,q)(a),\pand(p,r)(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-por} = & \por(\pand(p,q),\pand(p,r))(a) \end{eqnarray*}\] as needed.
For all $a \in A$, we have \[\begin{eqnarray*} & & \por(p,\pand(q,r))(a) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-por} = & \bor(p(a),\pand(q,r)(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pand} = & \bor(p(a),\band(q(a),r(a))) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-and-distribute} = & \band(\bor(p(a),q(a)),\bor(p(a),r(a))) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-por} = & \band(\por(p,q)(a),\bor(p(a),r(a))) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-por} = & \band(\por(p,q)(a),\por(p,r)(a)) \\ & \href{/posts/arithmetic-made-difficult/Predicates.html#def-pand} = & \pand(\por(p,q),\por(p,r))(a) \end{eqnarray*}\] as needed.

_test_pnot_pand
  :: a -> Test ((a -> Bool) -> (a -> Bool) -> a -> Bool)
_test_pnot_pand _ =
  testName "pnot(pand(p,q)) == por(pnot(p),pnot(q))" $
  \p q a -> eq ((pnot (pand p q)) a) ((por (pnot p) (pnot q)) a)


_test_pnot_por
  :: a -> Test ((a -> Bool) -> (a -> Bool) -> a -> Bool)
_test_pnot_por _ =
  testName "pnot(por(p,q)) == pand(pnot(p),pnot(q))" $
  \p q a -> eq ((pnot (por p q)) a) ((pand (pnot p) (pnot q)) a)


_test_pand_por
  :: a -> Test ((a -> Bool) -> (a -> Bool) -> (a -> Bool) -> a -> Bool)
_test_pand_por _ =
  testName "pand(p,por(q,r)) == por(pand(p,q),pand(p,r))" $
  \p q r a -> eq ((pand p (por q r)) a) ((por (pand p q) (pand p r)) a)


_test_por_pand
  :: a -> Test ((a -> Bool) -> (a -> Bool) -> (a -> Bool) -> a -> Bool)
_test_por_pand _ =
  testName "por(p,pand(q,r)) == pand(por(p,q),por(p,r))" $
  \p q r a -> eq ((por p (pand q r)) a) ((pand (por p q) (por p r)) a)

Implication lifts to predicates.

Let $A$ be a set. We define $\pimpl : \bool^A \times \bool^A \rightarrow \bool^A$ by \[\pimpl(p,q)(a) = \bimpl(p(a),q(a)).\]

Testing

Suite:

_test_predicate ::
  ( Equal a, Arbitrary a, CoArbitrary a, Show a, TypeName a
  , TypeName b, Boolean b, Equal b, Arbitrary b
  ) => a -> b -> Int -> Int -> IO ()
_test_predicate x p size cases = do
  testLabel1 "predicate" x

  let args = testArgs size cases

  runTest args (_test_pnot_involutive x p)
  runTest args (_test_pnot_ptrue x p)
  runTest args (_test_pnot_pfalse x p)
  runTest args (_test_not_ptrue x p)
  runTest args (_test_not_pfalse x p)

  runTest args (_test_pand_pfalse x)
  runTest args (_test_pand_ptrue x)
  runTest args (_test_pand_idempotent x)
  runTest args (_test_pand_commutative x)
  runTest args (_test_pand_associative x)

  runTest args (_test_por_ptrue x p)
  runTest args (_test_por_pfalse x p)
  runTest args (_test_por_idempotent x p)
  runTest args (_test_por_commutative x)
  runTest args (_test_por_associative x)

  runTest args (_test_pnot_pand x)
  runTest args (_test_pnot_por x)
  runTest args (_test_pand_por x)
  runTest args (_test_por_pand x)

Main:

main_predicate :: IO ()
main_predicate = _test_predicate (true :: Bool) (true :: Bool) 20 100