All and Any

Posted on 2017-05-10 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 AllAndAny
  ( all, any, _test_all_any, main_all_any
  ) where

import Testing
import Booleans
import Not
import And
import Or
import Predicates
import NaturalNumbers
import Lists
import Snoc
import Reverse
import Cat
import Map

Today we’ll define two boolean functions for lists called \(\all\) and \(\any\). Each one takes as an argument a predicate \(A \rightarrow \bool\), and then tests whether all or any of the items in a list of type \(\lists{A}\) satisfy the predicate.

Let \(A\) be a set and \(p : A \rightarrow \bool\) a predicate. Define \(\varphi : A \times \bool \rightarrow \bool\) by \[\varphi(a,q) = \band(p(a),q).\] Now define \(\all : \bool^A \rightarrow \bool^{\lists{A}}\) by \[\all(p)(x) = \foldr(\btrue)(\varphi)(x).\]

In Haskell:

all :: (Boolean b, List t) => (a -> b) -> t a -> b
all p = foldr true phi
  where
    phi a q = and (p a) q

Since \(\all(p)\) is defined as a \(\foldr(\ast)(\ast)\), it is the unique solution to a system of functional equations.

Let \(A\) be a set and \(p : A \rightarrow \bool\) a predicate. Then \(\all(p)\) is the unique solution \(f : \lists{A} \rightarrow \bool\) to the following equations for all \(a \in A\) and \(x \in \lists{A}\). \[\left\{\begin{array}{l} f(\nil) = \btrue \\ f(\cons(a,x)) = \band(p(a),f(x)) \end{array}\right.\]

_test_all_nil :: (List t, Equal a)
  => t a -> Test ((a -> Bool) -> Bool)
_test_all_nil t =
  testName "all(p)(nil) == true" $
  \p -> all p (nil `withTypeOf` t)


_test_all_cons :: (List t, Equal a)
  => t a -> Test ((a -> Bool) -> a -> t a -> Bool)
_test_all_cons _ =
  testName "all(p)(cons(a,x)) == and(p(a),all(p)(x))" $
  \p a x -> eq (all p (cons a x)) (and (p a) (all p x))

\(\all\) interacts with \(\snoc\).

Let \(A\) be a set. For all \(p : A \rightarrow \bool\), \(a \in A\), and \(x \in \lists{A}\), we have \[\all(p,\snoc(a,x)) = \band(p(a),\all(p,x)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \all(p,\snoc(a,x)) \\ & = & \all(p,\snoc(a,\nil)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \all(p,\cons(a,\nil)) \\ & = & \band(p(a),\all(p,\nil)) \\ & = & \band(p(a),\all(p,x)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(p\) and \(a\) for some \(x\) and let \(b \in A\). Using the inductive step, we have \[\begin{eqnarray*} & & \all(p,\snoc(a,\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \all(p,\cons(b,\snoc(a,x))) \\ & = & \band(p(b),\all(p,\snoc(a,x))) \\ & = & \band(p(b),\band(p(a),\all(p,x))) \\ & = & \band(p(a),\band(p(b),\all(p,x))) \\ & = & \band(p(a),\all(p,\cons(b,x))) \end{eqnarray*}\] as needed.

_test_all_snoc :: (List t, Equal a)
  => t a -> Test ((a -> Bool) -> a -> t a -> Bool)
_test_all_snoc _ =
  testName "all(p)(snoc(a,x)) == and(p(a),all(p)(x))" $
  \p a x -> eq (all p (snoc a x)) (and (p a) (all p x))

\(\all\) can also be characterized as a folded map.

\[\all(p,x) = \foldr(\btrue)(\band)(\map(p)(x)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \all(p,x) \\ & = & \all(p,\nil) \\ & = & \btrue \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & \foldr(\btrue)(\band)(\nil) \\ & = & \foldr(\btrue)(\band)(\map(p)(\nil)) \\ & = & \foldr(\btrue)(\band)(\map(p)(x)) \end{eqnarray*}\] as claimed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). Now \[\begin{eqnarray*} & & \all(p,\cons(a,x)) \\ & = & \band(p(a),\all(p,x)) \\ & = & \band(p(a),\foldr(\btrue)(\band)(\map(p)(x))) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \foldr(\btrue)(\band)(\cons(p(a),\map(p)(x))) \\ & = & \foldr(\btrue)(\band)(\map(p)(\cons(a,x))) \end{eqnarray*}\] as needed.

_test_all_fold_and :: (List t, Equal a)
  => t a -> Test ((a -> Bool) -> t a -> Bool)
_test_all_fold_and _ =
  testName "all(p,x) == foldr(true,and)(map(p)(x))" $
  \p x -> eq (all p x) (foldr true and (map p x))

Two special cases.

Let \(A\) be a set and \(p : A \rightarrow \bool\) a predicate. The following hold for all \(x \in \lists{A}\).

\(\all(\ptrue)(x) = \btrue\).
\(\all(\pfalse)(x) = \bfalse\) if and only if \(x \neq \nil\).

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \all(\ptrue,x) \\ & = & \all(\ptrue,\nil) \\ & = & \btrue \end{eqnarray*}\] as claimed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). Now \[\begin{eqnarray*} & & \all(\ptrue)(\cons(a,x)) \\ & = & \band(\ptrue(a),\all(\ptrue)(x)) \\ & = & \band(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-eval-true-true} = & \btrue \end{eqnarray*}\] as claimed.
We have two possibilities for \(x\). If \(x = \nil\), we have \[\begin{eqnarray*} & & \all(\pfalse)(\nil) \\ & = & \btrue, \end{eqnarray*}\] while if \(x = \cons(a,u)\), we have \[\begin{eqnarray*} & & \all(\pfalse)(\cons(a,u)) \\ & = & \band(\pfalse(a),\all(\pfalse)(u)) \\ & = & \band(\bfalse,\all(\pfalse)(u)) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \bfalse \end{eqnarray*}\] as needed.

_test_all_const_true :: (List t, Equal a)
  => t a -> Test (t a -> Bool)
_test_all_const_true _ =
  testName "all(ptrue)(x) == true" $
  \x -> eq (all ptrue x) (true :: Bool)


_test_all_const_false :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> Bool)
_test_all_const_false _ =
  testName "all(pfalse)(x) == false iff x /= nil" $
  \x -> eq
    (eq (all pfalse x) (false :: Bool))
    (not (eq x nil))

\(\all\) interacts with \(\cat\).

Let \(A\) be a set and \(p : A \rightarrow \bool\). For all \(x,y \in \lists{A}\) we have \[\all(p,\cat(x,y)) = \band(\all(p)(x),\all(p)(y)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \all(p)(\cat(x,y)) \\ & = & \all(p)(\cat(\nil,y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \all(p)(y) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \band(\btrue,\all(p)(y)) \\ & = & \band(\all(p)(\nil),\all(p)(y)) \\ & = & \band(\all(p)(x),\all(p)(y)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). Now \[\begin{eqnarray*} & & \all(p)(\cat(\cons(a,x),y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \all(p)(\cons(a,\cat(x,y))) \\ & = & \band(p(a),\all(p)(\cat(x,y))) \\ & = & \band(p(a),\band(\all(p)(x),\all(p)(y))) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-associative} = & \band(\band(p(a),\all(p)(x)),\all(p)(y)) \\ & = & \band(\all(p)(\cons(a,x)),\all(p)(y)) \end{eqnarray*}\] as needed.

_test_all_cat :: (List t, Equal a)
  => t a -> Test ((a -> Bool) -> t a -> t a -> Bool)
_test_all_cat _ =
  testName "all(p,cat(x,y)) == all(p,x) && all(p,y)" $
  \p x y -> eq (all p (cat x y)) (and (all p x) (all p y))

\(\all\) interacts with \(\rev\).

Let \(A\) be a set and \(p : A \rightarrow \bool\). For all \(x \in \lists{A}\) we have \[\all(p,\rev(x)) = \all(p,x).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \all(p,\rev(x)) \\ & = & \all(p,\rev(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \all(p,\nil) \\ & = & \all(p,x) \end{eqnarray*}\] as claimed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). Using the inductive hypothesis, we have \[\begin{eqnarray*} & & \all(p,\rev(\cons(a,x))) \\ & = & \all(p,\rev(\cat(\cons(a,\nil),x))) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-rev-cat-antidistribute} = & \all(p,\cat(\rev(x),\rev(\cons(a,\nil)))) \\ & = & \band(\all(p,\rev(x)),\all(p,\rev(\cons(a,\nil)))) \\ & = & \band(\all(p,x),\all(p,\cons(a,\nil))) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-commutative} = & \band(\all(p,\cons(a,\nil)),\all(p,x)) \\ & = & \all(p,\cat(\cons(a,\nil),x)) \\ & = & \all(p,\cons(a,x)) \end{eqnarray*}\] as claimed.

_test_all_rev :: (List t, Equal a)
  => t a -> Test ((a -> Bool) -> t a -> Bool)
_test_all_rev _ =
  testName "all(p,rev(x)) == all(p,x)" $
  \p x -> eq (all p (rev x)) (all p x)

\(\all\) interacts with \(\pimpl\).

Let \(A\) be a set and \(p,q : A \rightarrow \bool\). If \(\pimpl(p,q)\), then \[\bimpl(\all(p,x),\all(q,x)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \bimpl(\all(p,\nil),\all(q,\nil)) \\ & = & \bimpl(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \btrue \end{eqnarray*}\] as needed. For the inductive step, suppose the implication holds for some \(x\) and let \(a \in A\). Now \(\bimpl(p(a),q(a))\), and by the induction hypothesis \(\bimpl(\all(p,x),\all(q,x))\). Then we have \[\begin{eqnarray*} & & \bimpl(\all(p,\cons(a,x)),\all(q,\cons(a,x))) \\ & = & \bimpl(\band(p(a),\all(p,x)),\band(q(a),\all(q),x)) \\ & = & \btrue \end{eqnarray*}\] as needed.

\(\all\) interacts with \(\map\).

Let \(A\) and \(B\) be sets with \(f : A \rightarrow B\) and \(p : B \rightarrow \bool\). Then for all \(x \in \lists{A}\) we have \[\all(p)(\map(f)(x)) = \all(p \circ f)(x).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \all(p)(\map(f)(x)) \\ & = & \all(p)(\map(f)(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \all(p)(\nil) \\ & = & \btrue \\ & = & \all(p \circ f)(\nil) \\ & = & \all(p \circ f)(x) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). Now \[\begin{eqnarray*} & & \all(p)(\map(f)(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \all(p)(\cons(f(a),\map(f)(x))) \\ & = & \band(p(f(a)),\all(p)(\map(f)(x))) \\ & = & \band((p \circ f)(a),\all(p \circ f)(x)) \\ & = & \all(p \circ f)(\cons(a,x)) \end{eqnarray*}\] as needed.

_test_all_map :: (List t, Equal a)
  => t a -> Test ((a -> a) -> (a -> Bool) -> t a -> Bool)
_test_all_map _ =
  testName "all(p)(map(f)(x)) == all(p . f)(x)" $
  \f p x -> eq (all p (map f x)) (all (p . f) x)

\(\any\) is defined similarly.

Let \(A\) be a set and \(p : A \rightarrow \bool\) a predicate. Define \(\varphi : A \times \bool \rightarrow \bool\) by \[\varphi(a,q) = \bor(p(a),q).\] Now define \(\any : \bool^A \rightarrow \bool^{\lists{A}}\) by \[\all(p)(x) = \foldr(\bfalse)(\varphi)(x).\]

In Haskell:

any :: (Boolean b, List t) => (a -> b) -> t a -> b
any p = foldr false phi
  where
    phi a q = or (p a) q

Since \(\any\) is defined as a fold, it is the unique solution to a system of functional equations.

Let \(A\) be a set and \(p\) a predicate on \(A\). \(\any(p)\) is the unique map \(f : \lists{A} \rightarrow \bool\) satisfying the following equations for all \(a \in A\) and \(x \in \lists{A}\). \[\left\{\begin{array}{l} f(\nil) = \bfalse \\ f(\cons(a,x)) = \bor(p(a),f(x)) \end{array}\right.\]

_test_any_nil :: (List t, Equal a)
  => t a -> Test ((a -> Bool) -> Bool)
_test_any_nil t =
  testName "any(p)(nil) == false" $
  \p -> eq (any p (nil `withTypeOf` t)) false


_test_any_cons :: (List t, Equal a)
  => t a -> Test ((a -> Bool) -> a -> t a -> Bool)
_test_any_cons _ =
  testName "any(p)(cons(a,x)) == or(p(a),any(p)(x))" $
  \p a x -> eq (any p (cons a x)) (or (p a) (any p x))

\(\any\) can also be characterized as a folded map.

Let \(A\) be a set with \(p\) a predicate on \(A\). Then \[\any(p,x) = \foldr(\bfalse)(\bor)(\map(p)(x)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \any(p,x) \\ & = & \any(p,\nil) \\ & = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & \foldr(\bfalse)(\bor)(\nil) \\ & = & \foldr(\bfalse)(\bor)(\map(p)(\nil)) \\ & = & \foldr(\bfalse)(\bor)(\map(p)(x)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). Then we have \[\begin{eqnarray*} & & \any(p,\cons(a,x)) \\ & = & \bor(p(a),\any(x)) \\ & = & \bor(p(a),\foldr(\bfalse)(\bor)(\map(p)(x))) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-cons} = & \foldr(\bfalse)(\bor)(\cons(p(a),\map(p)(x))) \\ & = & \foldr(\bfalse)(\bor)(\map(p)(\cons(a,x))) \end{eqnarray*}\] as needed.

_test_any_fold_or :: (List t, Equal a)
  => t a -> Test ((a -> Bool) -> t a -> Bool)
_test_any_fold_or _ =
  testName "any(p,x) == foldr(false,or)(map(p)(x))" $
  \p x -> eq (any p x) (foldr false or (map p x))

A version of DeMorgan’s law holds for \(\any\) and \(\all\).

Let \(A\) be a set with \(p : A \rightarrow \bool\). Then the following hold for all \(x \in \lists{A}\).

\(\any(p,x) = \bnot(\all(\bnot \circ p,x))\).
\(\all(p,x) = \bnot(\any(\bnot \circ p,x))\).

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \bnot(\all(\bnot \circ p,x)) \\ & = & \bnot(\all(\bnot \circ p,\nil)) \\ & = & \bnot(\btrue) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-true} = & \bfalse \\ & = & \foldr(\bfalse)(\varphi(p))(\nil) \\ & = & \foldr(\bfalse)(\varphi(p))(x) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\) and let \(a \in A\). Then we have \[\begin{eqnarray*} & & \bnot(\all(\bnot \circ p,\cons(a,x))) \\ & = & \bnot(\band(\bnot(p(a)),\all(\bnot \circ p,x))) \\ & = & \bor(\bnot(\bnot(p(a))),\bnot(\all(\bnot \circ p,x))) \\ & = & \bor(p(a),\any(p,x)) \\ & = & \any(p,\cons(a,x)) \end{eqnarray*}\] as needed.
Note that \[\begin{eqnarray*} & & \bnot(\any(\bnot \circ p,x)) \\ & = & \bnot(\bnot(\all(\bnot \circ \bnot \circ p,x))) \\ & = & \all(p,x) \end{eqnarray*}\] as claimed.

_test_any_not_all :: (List t, Equal a)
  => t a -> Test ((a -> Bool) -> t a -> Bool)
_test_any_not_all _ =
  testName "any(p,x) == not(all(not . p, x))" $
  \p x -> eq (any p x) (not (all (not . p) x))


_test_all_not_any :: (List t, Equal a)
  => t a -> Test ((a -> Bool) -> t a -> Bool)
_test_all_not_any _ =
  testName "all(p,x) == not(any(not . p, x))" $
  \p x -> eq (all p x) (not (any (not . p) x))

Two special cases.

Let \(A\) be a set and \(p : A \rightarrow \bool\) a predicate. The following hold for all \(x \in \lists{A}\).

\(\any(\pfalse)(x) = \bfalse\).
\(\any(\ptrue)(x) = \btrue\) if and only if \(x \neq \nil\).

Note that \[\begin{eqnarray*} & & \any(\pfalse)(x) \\ & = & \bnot(\all(\bnot \circ \pfalse)(x)) \\ & = & \bnot(\all(\ptrue)(x)) \\ & = & \bnot(\btrue) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-true} = & \bfalse \end{eqnarray*}\] as claimed.
If \(x = \nil\), we have \[\begin{eqnarray*} & & \any(\pfalse)(x) \\ & = & \btrue, \end{eqnarray*}\] while if \(x = \cons(a,u)\) we have \[\begin{eqnarray*} & & \any(\ptrue)(\cons(a,u)) \\ & = & \bnot(\all(\bnot \circ \ptrue)(\cons(a,u))) \\ & = & \bnot(\all(\pfalse)(\cons(a,u))) \\ & = & \bnot(\bfalse) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-false} = & \btrue \end{eqnarray*}\] as needed.

_test_any_const_false :: (List t, Equal a)
  => t a -> Test (t a -> Bool)
_test_any_const_false _ =
  testName "any(pfalse,x) == false" $
  \x -> eq (any pfalse x) (false :: Bool)


_test_any_const_true :: (List t, Equal a, Equal (t a))
  => t a -> Test (t a -> Bool)
_test_any_const_true _ =
  testName "any(ptrue,x) == true iff x /= nil" $
  \x -> eq
    (eq (any ptrue x) (true :: Bool))
    (not (eq x nil))

\(\any\) interacts with \(\cat\).

Let \(A\) be a set and \(p : A \rightarrow \bool\). For all \(x,y \in \lists{A}\) we have \[\any(p,\cat(x,y)) = \bor(\any(p)(x),\any(p)(y)).\]

Note that \[\begin{eqnarray*} & & \any(p,\cat(x,y)) \\ & = & \bnot(\all(\bnot \circ p,\cat(x,y))) \\ & = & \bnot(\band(\all(\bnot \circ p,x),\all(\bnot \circ p,y))) \\ & = & \bor(\bnot(\all(\bnot \circ p,x)),\bnot(\all(\bnot \circ p,y))) \\ & = & \bor(\any(p,x),\any(p,y)) \end{eqnarray*}\] as claimed.

_test_any_cat :: (List t, Equal a)
  => t a -> Test ((a -> Bool) -> t a -> t a -> Bool)
_test_any_cat _ =
  testName "any(p,cat(x,y)) == any(p,x) || any(p,y)" $
  \p x y -> eq (any p (cat x y)) (or (any p x) (any p y))

\(\any\) interacts with \(\rev\).

Let \(A\) be a set and \(p : A \rightarrow \bool\). For all \(x,y \in \lists{A}\) we have \[\any(p,\rev(x)) = \any(p,x).\]

Note that \[\begin{eqnarray*} & & \any(p,\rev(x)) \\ & = & \bnot(\all(\bnot \circ p,\rev(x))) \\ & = & \bnot(\all(\bnot \circ p,x)) \\ & = & \any(p,x) \end{eqnarray*}\] as claimed.

_test_any_rev :: (List t, Equal a)
  => t a -> Test ((a -> Bool) -> t a -> Bool)
_test_any_rev _ =
  testName "any(p,rev(x)) == any(p,x)" $
  \p x -> eq (any p (rev x)) (any p x)

\(\any\) interacts with \(\map\).

Let \(A\) and \(B\) be sets with \(f : A \rightarrow B\) and \(p : B \rightarrow \bool\). Then for all \(x \in \lists{A}\) we have \[\any(p)(\map(f)(x)) = \any(p \circ f)(x).\]

Note that \[\begin{eqnarray*} & & \any(p,\map(f)(x)) \\ & = & \bnot(\all(\bnot \circ p,\map(f)(x))) \\ & = & \bnot(\all((\bnot \circ p) \circ f,x)) \\ & = & \bnot(\all(\bnot \circ (p \circ f),x)) \\ & = & \any(p \circ f,x) \end{eqnarray*}\] as claimed.

_test_any_map :: (List t, Equal a)
  => t a -> Test ((a -> a) -> (a -> Bool) -> t a -> Bool)
_test_any_map _ =
  testName "any(p)(map(f)(x)) == any(p . f)(x)" $
  \f p x -> eq (any p (map f x)) (any (p . f) x)

Testing

Suite:

_test_all_any ::
  ( TypeName a, Show a, Equal a, Arbitrary a, CoArbitrary a
  , TypeName (t a), List t
  , Show (t a), Equal (t a), Arbitrary (t a)
  ) => Int -> Int -> t a -> IO ()
_test_all_any size cases t = do
  testLabel1 "all & any" t
  let args = testArgs size cases

  runTest args (_test_all_nil t)
  runTest args (_test_all_cons t)
  runTest args (_test_all_snoc t)
  runTest args (_test_all_fold_and t)
  runTest args (_test_all_const_true t)
  runTest args (_test_all_const_false t)
  runTest args (_test_all_cat t)
  runTest args (_test_all_rev t)
  runTest args (_test_all_map t)

  runTest args (_test_any_nil t)
  runTest args (_test_any_cons t)
  runTest args (_test_any_fold_or t)
  runTest args (_test_any_not_all t)
  runTest args (_test_all_not_any t)
  runTest args (_test_all_const_false t)
  runTest args (_test_all_const_true t)
  runTest args (_test_any_cat t)
  runTest args (_test_any_rev t)
  runTest args (_test_any_map t)

Main:

main_all_any :: IO ()
main_all_any = do
  _test_all_any 20 100 (nil :: ConsList Bool)
  _test_all_any 20 100 (nil :: ConsList Unary)