Count

Posted on 2017-05-21 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 Count
  ( count, addcount, _test_count, main_count
  ) where

import Testing
import Tuples
import NaturalNumbers
import Plus
import Lists
import LeftFold
import Snoc
import Reverse
import Cat
import Length
import Filter

Today we’ll define \(\count\), which takes an \(A\) and a \(\lists{A}\) and returns the number of items in the \(\lists{A}\) that are identical to the \(A\). As usual we’ll define this as a fold. Note that – unlike some of the other list functions we’ve seen – in principle, \(\count\) shouldn’t care so much what order the items in its input come in. Moreover, note that \(\count\) necessarily must examine every item in its input if it’s going to return the correct answer. When this happens – we don’t care about order but have to look at every item – the left fold operator can be used instead of the right fold, with the advantage that left fold is more space efficient.

When dealing with left folds, it is often handier to parameterize on the base case, so that’s what we’ll do.

Let \(A\) be a set with \(a \in A\), and define \(\varphi : \nats \times A \rightarrow \nats\) by \[\varphi(k,b) = \bif{\beq(a,b)}{\next(k)}{k}.\] Now we define \(\addcount(a) : \nats \times \lists{A} \rightarrow \nats\) by \[\addcount(a)(n,x) = \foldl(\varphi)(n)(x).\]

In Haskell:

addcount:: (List t, Equal a, Natural n) => a -> n -> t a -> n
addcount a = foldl phi
  where
    phi k b = if eq a b then next k else k

Since \(\addcount\) is defined as a left fold, it can be characterized as the unique solution to a system of functional equations.

Let \(A\) be a set with \(a \in A\). Then \(\addcount\) is the unique map \(f : \nats \times \lists{A} \rightarrow \nats\) satisfying the following system of equations for all \(k \in \nats\), \(b \in A\), and \(x \in \lists{A}\). \[\left\{\begin{array}{l} f(k,\nil) = k \\ f(k,\cons(b,x)) = f(\bif{\beq(a,b)}{\next(k)}{k},x) \end{array}\right.\]

_test_addcount_nil :: (List t, Equal a, Natural n, Equal n)
  => t a -> n -> Test (a -> n -> Bool)
_test_addcount_nil t _ =
  testName "addcount(a)(k,nil) == k" $
  \a k -> eq (addcount a k (nil `withTypeOf` t)) k


_test_addcount_cons :: (List t, Equal a, Natural n, Equal n)
  => t a -> n -> Test (a -> n -> a -> t a -> Bool)
_test_addcount_cons _ _ =
  testName "addcount(a)(k,cons(b,x)) == addcount(a)(if(eq(a,b),next(k),k),x)" $
  \a k b x -> eq (addcount a k (cons b x)) (addcount a (if eq a b then next k else k) x)

\(\addcount\) interacts with \(\next\).

Let \(A\) be a set with \(a \in A\). For all \(k \in \nats\) and \(x \in \lists{A}\), we have \[\addcount(a)(\next(k),x) = \next(\addcount(a)(k,x)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \addcount(a)(\next(k),\nil) \\ & = & \next(k) \\ & = & \next(\addcount(a)(k,\nil)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(k\) for some \(x\) and let \(b \in A\). Now \[\begin{eqnarray*} & & \addcount(a)(\next(k),\cons(b,x)) \\ & = & \addcount(a)(\bif{\beq(a,b)}{\next(\next(k))}{\next(k)},x) \\ & = & \next(\addcount(a)(\bif{\beq(a,b)}{\next(k)}{k},x)) \\ & = & \next(\addcount(a)(k,\cons(b,x))) \end{eqnarray*}\] as needed.

_test_addcount_next :: (List t, Equal a, Natural n, Equal n)
  => t a -> n -> Test (a -> n -> t a -> Bool)
_test_addcount_next _ _ =
  testName "addcount(a)(next(k),x) == next(addcount(a)(k,x))" $
  \a k x -> eq (addcount a (next k) x) (next (addcount a k x))

Now \(\addcount\) interacts with \(\snoc\).

Let \(A\) be a set with \(a \in A\). For all \(b \in A\) and \(x \in \lists{A}\), we have \[\addcount(a)(k,\snoc(b,x)) = \addcount(a)(\bif{\beq(a,b)}{\next(k)}{k},x).\]

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

_test_addcount_snoc :: (List t, Equal a, Natural n, Equal n)
  => t a -> n -> Test (a -> n -> a -> t a -> Bool)
_test_addcount_snoc _ _ =
  testName "addcount(a)(k,snoc(b,x)) == addcount(a)(if(eq(a,b),next(k),k),x)" $
  \a k b x -> eq (addcount a k (snoc b x)) (addcount a (if eq a b then next k else k) x)

\(\addcount\) interacts with \(\rev\).

Let \(A\) be a set with \(a \in A\). For all \(k \in \nats\) and \(x \in \lists{A}\), we have \[\addcount(a)(k,\rev(x)) = \addcount(a)(k,x).\]

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

_test_addcount_rev :: (List t, Equal a, Natural n, Equal n)
  => t a -> n -> Test (a -> n -> t a -> Bool)
_test_addcount_rev _ _ =
  testName "addcount(a)(k,rev(x)) == addcount(a)(k,x)" $
  \a k x -> eq (addcount a k (rev x)) (addcount a k x)

We can also characterize \(\addcount\) as a right fold.

Let \(A\) be a set with \(a \in A\), and define \(\psi : A \times \nats \rightarrow \nats\) by \[\psi(b,k) = \bif{\beq(a,b)}{\next(k)}{k}.\] Then we have \[\addcount(a)(k,x) = \foldr(k)(\psi)(x).\]

Note that \[\begin{eqnarray*} & & \addcount(a)(k,\nil) \\ & = & k \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & \foldr(k)(\psi)(\nil) \end{eqnarray*}\] and \[\begin{eqnarray*} & & \addcount(a)(k,\cons(b,x)) \\ & = & \addcount(a)(\bif{\beq(a,b)}{\next(k)}{k},x) \\ & = & \bif{\beq(a,b)}{\addcount(a)(\next(k),x)}{\addcount(a)(k,x)} \\ & = & \bif{\beq(a,b)}{\next(\addcount(a)(k,x))}{\addcount(a)(k,x)} \\ & = & \psi(b,\addcount(a)(k,x)). \end{eqnarray*}\] By the universal property of right fold, the equality holds for all \(x\).

_test_addcount_foldr :: (List t, Equal a, Natural n, Equal n)
  => t a -> n -> Test (a -> n -> t a -> Bool)
_test_addcount_foldr _ _ =
  testName "addcount(a)(k,x) == foldr(k,psi)(x)" $
  \a k x ->
    let psi b m = if eq a b then next m else m in
    eq (addcount a k x) (foldr k psi x)

So we can evaluate \(\addcount\) as a left fold, but reason about \(\count\) as a right fold. Since \(\addcount(a)\) is also a right fold, it can be characterized as the unique solution to a (different) system of functional equations.

Let \(A\) be a set with \(a \in A\). Now \(\addcount(a)\) is the unique map \(f : \nats \times \lists{A} \rightarrow \nats\) satisfying the following equations for all \(b \in A\) and \(x \in \lists{A}\). \[\left\{\begin{array}{l} f(k,\nil) = k \\ f(k,\cons(b,x)) = \bif{\beq(a,b)}{\next(f(k,x))}{f(k,x)} \end{array}\right.\]

_test_addcount_foldr_cons :: (List t, Equal a, Natural n, Equal n)
  => t a -> n -> Test (a -> n -> a -> t a -> Bool)
_test_addcount_foldr_cons _ _ =
  testName "addcount(a)(k,cons(b,x)) == if(eq(a,b),next(addcount(a)(k,x)),addcount(a)(k,x))" $
  \a k b x -> eq
    (addcount a k (cons b x))
    (if eq a b then next (addcount a k x) else addcount a k x)

We define \(\count\) in terms of \(\addcount\).

Let \(A\) be a set with \(a \in A\). We define \(\count : A \rightarrow \nats^{\lists{A}}\) by \[\count(a)(x) = \addcount(a)(\zero,x).\]

In Haskell:

count :: (List t, Equal a, Natural n) => a -> t a -> n
count a = addcount a zero

Since \(\count\) is defined in terms of \(\addcount\), it is also the unique solution to a system of functional equations.

Let \(A\) be a set with \(a \in A\). Then \(\count(a)\) is the unique map \(f : \lists{A} \rightarrow \nats\) which satisfies the following system of equations for all \(b \in A\) and \(x \in \lists{A}\). \[\left\{\begin{array}{l} f(\nil) = \zero \\ f(\cons(b,x)) = \bif{\beq(a,b)}{\next(f(x))}{f(x)} \end{array}\right.\]

_test_count_nil :: (List t, Equal a, Natural n, Equal n)
  => t a -> n -> Test (a -> Bool)
_test_count_nil t k =
  testName "count(a)(nil) == zero" $
  \a -> eq (count a (nil `withTypeOf` t)) (zero `withTypeOf` k)


_test_count_cons :: (List t, Equal a, Natural n, Equal n)
  => t a -> n -> Test (a -> a -> t a -> Bool)
_test_count_cons _ k =
  testName "count(a)(cons(b,x)) == if(eq(a,b),next(count(a)(x)),count(a)(x))" $
  \a b x -> eq
    ((count a (cons b x)) `withTypeOf` k)
    (if eq a b then next (count a x) else count a x)

A special case.

Let \(A\) be a set, with \(a,b \in A\). Then \[\count(a,\cons(b,\nil)) = \bif{\beq(a,b)}{\next(\zero)}{\zero}.\]

Note that \[\begin{eqnarray*} & & \count(a,\cons(b,\nil)) \\ & = & \foldl(\zero){\varphi(a)}(\cons(b,\nil)) \\ & = & \foldl(\varphi(a)(b,\zero)){\varphi(a)}(\nil) \\ & = & \varphi(a)(b,\zero) \\ & = & \bif{\beq(a,b)}{\next(\zero)}{\zero} \end{eqnarray*}\] as claimed.

_test_count_one :: (List t, Equal a, Natural n, Equal n)
  => t a -> n -> Test (a -> a -> Bool)
_test_count_one t k =
  testName "count(a,cons(b,nil)) == if(eq(a,b),next(zero),zero)" $
  \a b -> eq
    (count a (cons b (nil `withTypeOf` t)))
    (if eq a b then (next zero `withTypeOf` k) else zero)

\(\count\) interacts with \(\snoc\).

Let \(A\) be a set with \(a \in A\). For all \(b \in A\) and \(x \in \lists{A}\), we have \[\count(a)(\snoc(b,x)) = \bif{\beq(a,b)}{\next(\count(a)(x))}{\count(a)(x)}.\]

Note that \[\begin{eqnarray*} & & \count(a)(\snoc(b,x)) \\ & = & \addcount(a)(\zero,\snoc(b,x)) \\ & = & \bif{\beq(a,b)}{\next(\addcount(a)(\zero,x))}{\addcount(a)(\zero,x)} \\ & = & \bif{\beq(a,b)}{\next(\count(a)(x))}{\count(a)(x)} \end{eqnarray*}\] as claimed.

_test_count_snoc :: (List t, Equal a, Natural n, Equal n)
  => t a -> n -> Test (a -> a -> t a -> Bool)
_test_count_snoc _ k =
  testName "count(a)(snoc(b,x)) == count(a)(if(eq(a,b),next(k),k),x)" $
  \a b x -> eq
    ((count a (snoc b x)) `withTypeOf` k)
    (if eq a b then next (count a x) else count a x)

\(\count\) interacts with \(\rev\).

Let \(A\) be a set with \(a \in A\). For all \(x \in \lists{A}\) we have \[\count(a)(\rev(x)) = \count(a)(x).\]

Note that \[\begin{eqnarray*} & & \count(a)(\rev(x)) \\ & = & \addcount(a)(\zero,\rev(x)) \\ & = & \addcount(a)(\zero,x) \\ & = & \count(a)(x) \end{eqnarray*}\] as claimed.

_test_count_rev :: (List t, Equal a, Natural n, Equal n)
  => t a -> n -> Test (a -> t a -> Bool)
_test_count_rev _ k =
  testName "count(a)(rev(x)) == count(a)(x)" $
  \a x -> eq (count a (rev x)) ((count a x) `withTypeOf` k)

\(\count\) interacts with \(\cat\).

Let \(A\) be a set. For all \(a \in A\) and \(x,y \in \lists{A}\) we have \[\count(a,\cat(x,y)) = \nplus(\count(a,x),\count(a,y)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \count(a,\cat(x,y)) \\ & = & \count(a,\cat(\nil,y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-nil} = & \count(a,y) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-zero} = & \nplus(\zero,\count(a,y)) \\ & = & \nplus(\count(a,\nil),\count(a,y)) \\ & = & \nplus(\count(a,x),\count(a,y)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(y\) and \(a\) for some \(x\), and let \(b \in A\). We consider two possibilities. If \(a = b\), we have \[\begin{eqnarray*} & & \count(a,\cat(\cons(b,x),y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \count(a,\cons(b,\cat(x,y))) \\ & = & \bif{\beq(a,b)}{\next(\count(a,\cat(x,y)))}{\count(a,\cat(x,y))} \\ & = & \next(\count(a,\cat(x,y))) \\ & = & \next(\nplus(\count(a,x),\count(a,y))) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-next} = & \nplus(\next(\count(a,x)),\count(a,y)) \\ & = & \nplus(\bif{\beq(a,b)}{\next(\count(a,x))}{\count(a,x)},\count(a,y)) \\ & = & \nplus(\count(a,\cons(b,x)),\count(a,y)) \end{eqnarray*}\] as needed. If \(a \neq b\), we have \[\begin{eqnarray*} & & \count(a,\cat(\cons(b,x),y)) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#cor-cat-cons} = & \count(a,\cons(b,\cat(x,y))) \\ & = & \bif{\beq(a,b)}{\next(\count(a,\cat(x,y)))}{\count(a,\cat(x,y))} \\ & = & \count(a,\cat(x,y)) \\ & = & \nplus(\count(a,x),\count(a,y)) \\ & = & \nplus(\bif{\beq(a,b)}{\next(\count(a,x))}{\count(a,x)},\count(a,y)) \\ & = & \nplus(\count(a,\cons(b,x)),\count(a,y)) \end{eqnarray*}\] as needed.

_test_count_cat :: (List t, Equal a, Natural n, Equal n)
   => t a -> n -> Test (a -> t a -> t a -> Bool)
_test_count_cat _ k =
  testName "count(a,cat(x,y)) == plus(count(a,x),count(a,y))" $
  \a x y -> eq
    ((count a (cat x y)) `withTypeOf` k)
    (plus (count a x) (count a y))

\(\count\) is a \(\length\).

Let \(A\) be a set. We have \[\count(a,x) = \length(\filter(\beq(a,-),x)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \count(a,x) \\ & = & \count(a,\nil) \\ & = & \foldr(\zero)(\varphi(a))(\nil) \\ & \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil} = & \zero \\ & = & \length(\nil) \\ & = & \length(\filter(\beq(a,-),\nil)) \\ & = & \length(\filter(\beq(a,-),x)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\) and let \(b \in A\). We consider two possibilities. If \(a = b\), we have \[\begin{eqnarray*} & & \count(a,\cons(b,x)) \\ & = & \count(a,\cons(a,x)) \\ & = & \bif{\beq(a,a)}{\next(\count(a,x))}{\count(a,x)} \\ & = & \next(\count(a,x)) \\ & = & \next(\length(\filter(\beq(a,-),x))) \\ & = & \length(\cons(a,\filter(\beq(a,-),x))) \\ & = & \length(\filter(\beq(a,-),\cons(a,x))) \end{eqnarray*}\] as needed. If \(a \neq b\), we have \[\begin{eqnarray*} & & \count(a,\cons(b,x)) \\ & = & \bif{\beq(a,b)}{\next(\count(a,x))}{\count(a,x)} \\ & = & \count(a,x) \\ & = & \length(\filter(\beq(a,-),x)) \\ & = & \length(\filter(\beq(a,-),\cons(b,x))) \end{eqnarray*}\] as needed.

_test_count_length :: (List t, Equal a, Natural n, Equal n)
  => t a -> n -> Test (a -> t a -> Bool)
_test_count_length _ k =
  testName "count(a,x) == length(filter(eq(a,-),x))" $
  \a x -> eq
    (count a x `withTypeOf` k)
    (length (filter (eq a) x))

\(\count\) interacts with \(\map(f)\) when \(f\) is injective.

Let \(A\) and \(B\) be sets and \(f : A \rightarrow B\) an injective map. Then \[\count(a,x) = \count(f(a),\map(f)(x)).\]

We proceed by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*} & & \count(a,x) \\ & = & \count(a,\nil) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-nil} = & \count(a,\map(f)(\nil)) \\ & = & \count(a,\map(f)(x)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(x\), and let \(b \in A\). We consider two possibilities. If \(a = b\), then \(f(a) = f(b)\), and we have \[\begin{eqnarray*} & & \count(a,\cons(b,x)) \\ & = & \count(a,\cons(a,x)) \\ & = & \next(\count(a,x)) \\ & = & \next(\count(f(a),\map(f)(x))) \\ & = & \count(f(a),\cons(f(a),\map(f)(x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \count(f(a),\map(f)(\cons(a,x))) \\ & = & \count(f(a),\map(f)(\cons(b,x))) \end{eqnarray*}\] as needed. If \(a \neq b\), then we have \(f(a) \neq f(b)\) (since \(f\) is injective), so that \[\begin{eqnarray*} & & \count(a,\cons(b,x)) \\ & = & \count(a,x) \\ & = & \count(f(a),\map(f)(x)) \\ & = & \count(f(a),\cons(f(b),\map(f)(x))) \\ & \href{/posts/arithmetic-made-difficult/Map.html#cor-map-cons} = & \count(f(a),\map(f)(\cons(b,x))) \end{eqnarray*}\] as needed.

Testing

Suite:

_test_count ::
  ( TypeName a, Equal a, Show a, Arbitrary a, CoArbitrary a
  , TypeName (t a), List t
  , TypeName n, Natural n, Equal n, Show n, Arbitrary n
  , Show (t a), Equal (t a), Arbitrary (t a), Equal (t (Pair a a))
  ) => Int -> Int -> t a -> n -> IO ()
_test_count size cases t n = do
  testLabel2 "count" t n

  let args = testArgs size cases

  runTest args (_test_addcount_nil t n)
  runTest args (_test_addcount_cons t n)
  runTest args (_test_addcount_next t n)
  runTest args (_test_addcount_snoc t n)
  runTest args (_test_addcount_rev t n)
  runTest args (_test_addcount_foldr t n)
  runTest args (_test_addcount_foldr_cons t n)

  runTest args (_test_count_nil t n)
  runTest args (_test_count_cons t n)
  runTest args (_test_count_one t n)
  runTest args (_test_count_snoc t n)
  runTest args (_test_count_rev t n)
  runTest args (_test_count_cat t n)
  runTest args (_test_count_length t n)

Main:

main_count :: IO ()
main_count = do
  _test_count 20 100 (nil :: ConsList Bool)  (zero :: Unary)
  _test_count 20 100 (nil :: ConsList Unary) (zero :: Unary)