Find Smallest

Posted on 2017-12-29 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 FindSmallest (
  findSmallest, _test_findSmallest, main_findSmallest
) where

import Testing
import Booleans
import And
import DisjointUnions
import NaturalNumbers
import BailoutRecursion
import Plus
import LessThanOrEqualTo

The Well-Ordering Principle on \(\nats\) gives a sufficient condition under which a natural number minimal with respect to a given property must exist; namely, that the set of all natural numbers with that property is not empty. WOP can come in really handy when we want to show that, say, the smallest number \(k\) with property foo exists, and reason about it. Unfortunately, WOP alone is nonconstructive – it tells us nothing about how to actually find anything. Today we’ll establish a weak constructive form of WOP.

More precisely, given a predicate \(\sigma : \nats \rightarrow \bool\) and two natural numbers \(k\) and \(n\), we’ll define an operator \(\Theta\) such that \(\Theta(\next(n),k)\) is the smallest number \(t\) between \(k\) and \(\nplus(k,n)\) such that \(\sigma(t) = \btrue\), if any such number exists, and \(\ast\) otherwise.

Let \(\sigma : \nats \rightarrow \bool\). Define \(\varphi : \nats \rightarrow 1 + \nats\) by \[\varphi(k) = \lft(\ast),\] \(\beta : \nats \times \nats \rightarrow \bool\) by \[\beta(n,k) = \sigma(k),\] \(\psi : \nats \times \nats \rightarrow 1 + \nats\) by \[\psi(n,k) = \rgt(k),\] and \(\omega : \nats \times \nats \rightarrow \nats\) by \[\omega(n,k) = \next(k).\] We then define \[\findsmallest() : \bool^\nats \rightarrow \nats \times \nats \rightarrow 1 + \nats\] by \[\findsmallest(\sigma)(n,k) = \bailrec(\varphi)(\beta)(\psi)(\omega)(n,k).\]

In Haskell:

findSmallest :: (Natural n) => (n -> Bool) -> n -> n -> Union () n
findSmallest sigma = bailoutRec phi beta psi omega
  where
    phi _ = lft ()
    beta _ k = sigma k
    psi _ k = rgt k
    omega _ k = next k

Because \(\findsmallest(\sigma)\) is defined in terms of bailout recursion, it is the unique solution to a system of functional equations.

Let \(\sigma : \nats \rightarrow \bool\) be a map. Then \(\findsmallest(\sigma) : \nats \times \nats \rightarrow 1 + \nats\) is the unique solution \(f : \nats \times \nats \rightarrow 1 + \nats\) to the following system of equations for all \(n,k \in \nats\). \[\left\{\begin{array}{l} f(\zero,k) = \lft(\ast) \\ f(\next(n),k) = \bif{\sigma(k)}{\rgt(k)}{f(n,\next(k))} \end{array}\right.\]

_test_findSmallest_zero_left :: (Natural n, Equal n)
  => n -> Test ((n -> Bool) -> n -> Bool)
_test_findSmallest_zero_left _ =
  testName "findSmallest(sigma)(0,k) == lft(*)" $
  \sigma k -> eq (findSmallest sigma zero k) (lft ())


_test_findSmallest_next_left :: (Natural n, Equal n)
  => n -> Test ((n -> Bool) -> n -> n -> Bool)
_test_findSmallest_next_left _ =
  testName "findSmallest(sigma)(next(n),k) == if(sigma(k),rgt(k),findSmallest(sigma)(n,next(k)))" $
  \sigma n k -> eq
    (findSmallest sigma (next n) k)
    (if sigma k then rgt k else findSmallest sigma n (next k))

First, if \(\findsmallest(\sigma)\) returns a result \(\rgt(t)\), then \(t\) satisfies \(\sigma\).

Let \(\sigma : \nats \rightarrow \bool\), with \(n,k,t \in \nats\). If \(\findsmallest(\sigma)(n,k) = \rgt(t)\), then \(\sigma(t) = \btrue\).

We proceed by induction on \(n\). For the base case \(n = \zero\), note that \[\findsmallest(\sigma)(\zero,k) = \lft(\ast),\] so the implication holds vacuously. For the inductive step, suppose we have \(n\) such that for all \(k\) and \(t\), if \(\findsmallest(\sigma)(n,k) = \rgt(t)\) then \(\sigma(t) = \btrue\). Suppose further that \(\findsmallest(\sigma)(\next(n),k) = \rgt(t)\). Now we have \[\findsmallest(\sigma)(\next(n),k) = \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(n,\next(k))}.\] We have two possibilities. If \(\sigma(k) = \btrue\), then \[\findsmallest(\sigma)(n,k) = \rgt(k),\] with \(\sigma(k) = \btrue\) as needed. If \(\sigma(k) = \bfalse,\) we have \[\rgt(t) = \findsmallest(\sigma)(\next(n),k) = \findsmallest(\sigma)(n,\next(k)),\] and by the inductive hypothesis, \(\sigma(t) = \btrue\) as needed.

_test_findSmallest_satisfies :: (Natural n, Equal n)
  => n -> Test ((n -> Bool) -> n -> n -> Bool)
_test_findSmallest_satisfies _ =
  testName "if findSmallest(sigma)(n,k) == rgt(t) then sigma(t) == true" $
  \sigma n k -> case findSmallest sigma n k of
    Right t -> eq (sigma t) true
    Left () -> true

Next, if \(\findsmallest(\sigma)(\next(n),k)\) returns a result \(\rgt(t)\), then \(t\) is bounded; specifically, \(\nleq(k,t)\) and \(\nleq(t,\nplus(n,k))\).

If \(\findsmallest(\sigma)(\next(n),k) = \rgt(t)\), then \(\nleq(k,t)\) and \(\nleq(t,\nplus(n,k))\).

We proceed by induction on \(n\). For the base case \(n = \zero\), if \(\findsmallest(\sigma)(\next(n),k) = \rgt(t)\) we have \[\begin{eqnarray*} & & \findsmallest(\sigma)(\next(\zero),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(\zero,\next(k))} \\ & = & \bif{\sigma(k)}{\rgt(k)}{\lft(\ast)}. \end{eqnarray*}\] In particular, we must have \(\sigma(k) = \btrue\) and \(t = k\). Thus \(\nleq(k,t)\) and \(\nleq(t,\nplus(n,k))\) as needed.

For the inductive step, suppose the implication holds for all \(k\) and \(t\) for some \(n\), and suppose further that \(\findsmallest(\sigma)(\next(\next(n)),k) = \rgt(t)\). Now \[\begin{eqnarray*} & & \rgt(t) \\ & = & \findsmallest(\sigma)(\next(\next(n)),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(\next(n),\next(k))}. \end{eqnarray*}\] We have two possibilities. If \(\sigma(k) = \btrue\), then \(\rgt(t) = \rgt(k)\), so that \(\nleq(k,t)\) and \(\nleq(t,\nplus(n,k))\) as needed. If \(\sigma(k) = \bfalse\), we have \(\rgt(t) = \findsmallest(\sigma)(\next(n),\next(k))\). By the inductive hypothesis, we have \(\nleq(\next(k),t)\) and \(\nleq(t,\nplus(\next(n),\next(k)))\). By transitivity we thus have \(\nleq(k,t)\) and \(\nleq(t,\nplus(\next(\next(n)),k))\) as needed.

_test_findSmallest_bounded :: (Natural n, Equal n)
  => n -> Test ((n -> Bool) -> n -> n -> Bool)
_test_findSmallest_bounded _ =
  testName "if findSmallest(sigma)(next(n),k) == rgt(t) then leq(k,t) and leq(t,plus(n,k))" $
  \sigma n k -> case findSmallest sigma (next n) k of
    Right t -> and (leq k t) (leq t (plus n k))
    Left () -> true

\(\findsmallest(\sigma)(\next(n),k)\) returns \(\lft(\ast)\) if and only if \(\sigma\) is false for all \(u\) between \(k\) and \(\nplus(n,k)\).

Let \(\sigma : \nats \rightarrow \bool\) and \(n,k \in \nats\). Then \(\findsmallest(\sigma)(\next(n),k) = \lft(\ast)\) if and only if \(\sigma(t) = \bfalse\) for all \(t\) with \(\nleq(k,t)\) and \(\nleq(t,\nplus(n,k))\).

We prove the “only if” direction by induction on \(n\). For the base case \(n = \zero\), suppose \(\findsmallest(\sigma)(\next(\zero),k) = \lft(\ast)\). Expanding, we have \[\begin{eqnarray*} & & \lft(\ast) \\ & = & \findsmallest(\sigma)(\next(\zero),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(\zero,\next(k))} \\ & = & \bif{\sigma(k)}{\rgt(k)}{\lft(\ast)} \end{eqnarray*}\] Thus \(\sigma(k) = \bfalse\). Now if \(\nleq(k,t)\) and \(\nleq(t,\nplus(\zero,k))\), we have \(t = k\) by antisymmetry, and thus \(\sigma(t) = \bfalse\) for all \(\nleq(k,t)\) and \(\nleq(t,\nplus(n,k))\) as needed. For the inductive step, suppose the implication holds for all \(k\) for some \(n\), and suppose further that \(\findsmallest(\sigma)(\next(\next(n)),k) = \lft(\ast)\). Expanding, we have \[\begin{eqnarray*} & & \lft(\ast) \\ & = & \findsmallest(\sigma)(\next(\next(n)),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(\next(n),\next(k))}. \end{eqnarray*}\] Now we must have \(\sigma(k) = \bfalse\), and moreover \(\findsmallest(\sigma)(\next(n),\next(k)) = \lft(\ast)\). By the inductive hypothesis, we have \(\sigma(t) = \bfalse\) whenever \(\nleq(\next(k),t)\) and \(\nleq(t,\nplus(\next(n),\next(k)))\); thus \(\sigma(t) = \bfalse\) whenever \(\nleq(k,t)\) and \(\nleq(t,\nplus(\next(\next(n)),k))\) as needed.

We also prove the “if” direction by induction on \(n\). For the base case \(n = \zero\), suppose \(\sigma(t) = \bfalse\) when \(\nleq(k,t)\) and \(\nleq(t,\nplus(\zero,k))\); by antisymmetry, we have \(\sigma(k) = \bfalse\), and thus \[\begin{eqnarray*} & & \findsmallest(\sigma)(\next(\zero),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(\zero,k)} \\ & = & \bif{\sigma(k)}{\rgt(k)}{\lft(\ast)} \\ & = & \bif{\bfalse}{\rgt(k)}{\lft(\ast)} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \lft(\ast) \end{eqnarray*}\] as needed. For the inductive step, suppose the implication holds for all \(k\) for some \(n\), and suppose further that \(\sigma(t) = \bfalse\) whenever \(\nleq(k,t)\) and \(\nleq(t,\nplus(\next(n),k))\). Then we have \(\sigma(k) = \bfalse\), and we also have \(\sigma(t) = \bfalse\) whenever \(\nleq(\next(k),t)\) and \(\nleq(t,\nplus(n,\next(k)))\), and by the inductive hypothesis, \(\findsmallest(\sigma)(\next(n),\next(k)) = \lft(\ast)\). Now \[\begin{eqnarray*} & & \findsmallest(\sigma)(\next(\next(n)),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(\next(n),\next(k))} \\ & = & \bif{\sigma(k)}{\rgt(k)}{\lft(\ast)} \\ & = & \bif{\bfalse}{\rgt(k)}{\lft(\ast)} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \lft(\ast) \end{eqnarray*}\] as needed.

_test_findSmallest_return_lft :: (Natural n, Equal n)
  => n -> Test ((n -> Bool) -> n -> n -> n -> Bool)
_test_findSmallest_return_lft _ =
  testName "if eq(findSmallest(sigma)(next(n),k),lft(*)) and leq(k,t) and leq(t,plus(n,k)) then eq(sigma(t),false)" $
  \sigma n k t -> if and (leq k t) (leq t (plus n k))
    then if eq (findSmallest sigma (next n) k) (lft ())
      then eq (sigma t) false
      else true
    else true

If \(\findsmallest(\sigma)(n,k)\) returns a value, then \(\findsmallest(\sigma)(t,k)\) does not, where \(t\) is the difference between \(k\) and the returned value.

If \(\findsmallest(\sigma)(n,k) = \rgt(\nplus(k,\next(t)))\), then \(\findsmallest(\sigma)(t,k) = \lft(\ast)\).

We proceed by induction on \(t\). For the base case \(t = \zero\), note that \[\findsmallest(\sigma)(\zero,k) = \lft(\ast),\] so the implication holds regardless of \(n\) and \(k\). For the inductive step, suppose the implication holds for all \(n\) and \(k\) for some \(t\), and suppose further that \[\findsmallest(\sigma)(n,k) = \rgt(\nplus(k,\next(\next(t)))).\] Now we must have \(n = \next(m)\) for some \(m\), and moreover \[\begin{eqnarray*} & & \rgt(\nplus(\next(k),\next(t))) \\ & = & \rgt(\nplus(k,\next(\next(t)))) \\ & = & \findsmallest(\sigma)(\next(m),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(m,\next(k))} \end{eqnarray*}\] Note that \(\sigma(k)\) cannot be \(\btrue\), as in this case we have \(k = \nplus(k,\next(\next(t)))\). So we have \(\sigma(k) = \bfalse\) and \[\begin{eqnarray*} & & \rgt(\nplus(\next(k),\next(t))) \\ & = & \findsmallest(\sigma)(m,\next(k)). \end{eqnarray*}\] By the inductive hypothesis, we have \(\findsmallest(\sigma)(t,\next(k)) = \lft(\ast)\), and thus \[\begin{eqnarray*} & & \findsmallest(\sigma)(\next(t),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(t,\next(k))} \\ & = & \findsmallest(\sigma)(t,\next(k)) \\ & = & \lft(\ast) \end{eqnarray*}\] as needed.

_test_findSmallest_value_lft :: (Natural n, Equal n)
  => n -> Test ((n -> Bool) -> n -> n -> n -> Bool)
_test_findSmallest_value_lft _ =
  testName "if findSmallest(sigma)(n,k) == rgt(plus(k,next(t))) then findSmallest(sigma)(t,k) = lft(*)" $
  \sigma n k t -> if eq (findSmallest sigma n k) (rgt (plus k (next t)))
    then eq (findSmallest sigma t k) (lft ())
    else true

Finally, \(\findsmallest(\sigma)\) returns a least value.

If \(\findsmallest(\sigma)(\next(n),k) = \rgt(t)\), and if \(u \in \nats\) such that \(\sigma(u) = \btrue\), \(\nleq(k,u)\), and \(\nleq(u,\nplus(n,k))\), then \(\nleq(t,u)\).

We proceed by induction on \(n\). For the base case \(n = \zero\), suppose \[\begin{eqnarray*} & & \rgt(t) \\ & = & \findsmallest(\sigma)(\next(\zero),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\lft(\ast)}. \end{eqnarray*}\] We must have \(\sigma(k) = \btrue\) and thus \(k = t\). Then we have \(\nleq(t,u)\) whenever \(\nleq(k,u)\) as needed.

For the inductive step, suppose the implication holds for all \(k\), \(t\), and \(u\) for some \(n\), and suppose further that \(\findsmallest(\sigma)(\next(\next(n)),k) = \rgt(t)\). Now \(t = \nplus(k,m)\) for some \(m\) since \(\nleq(k,t)\). We have \[\begin{eqnarray*} & & \rgt(\nplus(k,m)) \\ & = & \rgt(t) \\ & = & \findsmallest(\sigma)(\next(\next(n)),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(\next(n),\next(k))}. \end{eqnarray*}\] If \(\sigma(k) = \btrue\), then \(t = k\), and we again have \(\nleq(t,u)\) as needed. If instead \(\sigma(k) = \bfalse\), we have \[\rgt(t) = \findsmallest(\sigma)(\next(n),\next(k)).\] By the inductive hypothesis, if \(\sigma(u) = \btrue\) and \(\nleq(\next(k),u)\) and \(\nleq(u,\nplus(n,\next(k)))\), then \(\nleq(t,u)\). Suppose \(\sigma(u) = \btrue\), \(\nleq(k,u)\), and \(\nleq(u,\nplus(\next(n),k))\). Since \(\sigma(k) = \bfalse\), we have \(\nleq(\next(k),u)\), so by the inductive hypothesis, \(\nleq(t,u)\) as needed.

_test_findSmallest_minimal :: (Natural n, Equal n)
  => n -> Test ((n -> Bool) -> n -> n -> n -> n -> Bool)
_test_findSmallest_minimal _ =
  testName "if findSmallest(sigma)(next(n),k) == rgt(t) and sigma(u) and leq(k,u) and leq(u,plus(n,k)) then leq(t,u)" $
  \sigma n k _ u -> case findSmallest sigma (next n) k of
    Right t -> if and (sigma u) (and (leq k u) (leq u (plus n k)))
      then leq t u
      else true
    Left () -> true

To summarize:

Let \(\sigma : \nats \rightarrow \bool\) and \(n,k \in \nats\).

If \(\findsmallest(\sigma)(\next(n),k) = \rgt(t)\), then \(\sigma(t)\), \(\nleq(k,t)\), and \(\nleq(t,\nplus(n,k))\), and if \(u \in \nats\) such that \(\sigma(u)\), \(\nleq(k,u)\), and \(\nleq(u,\nplus(n,k))\), then \(\nleq(t,u)\).
If \(\findsmallest(\sigma)(\next(n),k) = \lft(\ast)\), then there does not exist \(u \in \nats\) such that \(\sigma(u)\), \(\nleq(k,u)\), and \(\nleq(u,\nplus(n,k))\).

Testing

Suite:

_test_findSmallest ::
  ( TypeName n, Natural n, Equal n, Arbitrary n, CoArbitrary n, Show n
  ) => Int -> Int -> n -> IO ()
_test_findSmallest size cases n = do
  testLabel1 "findSmallest" n

  let args = testArgs size cases

  runTest args (_test_findSmallest_zero_left n)
  runTest args (_test_findSmallest_next_left n)
  runTest args (_test_findSmallest_satisfies n)
  runTest args (_test_findSmallest_bounded n)
  runTest args (_test_findSmallest_return_lft n)
  runTest args (_test_findSmallest_value_lft n)
  runTest args (_test_findSmallest_minimal n)

Main:

main_findSmallest :: IO ()
main_findSmallest = do
  _test_findSmallest 50 100 (zero :: Unary)