Maximum and Minimum

Posted on 2017-04-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 MaxAndMin
  ( max, min, _test_max_min, main_max_min
  ) where

import Testing
import Booleans
import And
import NaturalNumbers
import Plus
import Times
import LessThanOrEqualTo

With $\nleq$ in hand we can also define max and min functions. These are less interesting since they do not have to be defined recursively.

We define $\nmax : \nats \times \nats \rightarrow \nats$ by \[\nmax(a,b) = \bif{\nleq(a,b)}{b}{a}\] and $\nmin : \nats \times \nats \rightarrow \nats$ by \[\nmin(a,b) = \bif{\nleq(a,b)}{a}{b}.\]

In Haskell:

max :: (Natural n) => n -> n -> n
max a b = if leq a b then b else a

min :: (Natural n) => n -> n -> n
min a b = if leq a b then a else b

Special cases.

Let $a \in \nats$. Then we have the following.

$\nmax(\zero,a) = a$.
$\nmax(a,a) = a$.
$\nmin(\zero,a) = \zero$.
$\nmin(a,a) = a$.

We have \[\begin{eqnarray*} & & \nmax(\zero,a) \\ & \href{/posts/arithmetic-made-difficult/MaxAndMin.html#def-max} = & \bif{\nleq(\zero,a)}{a}{\zero} \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#thm-leq-zero} = & \bif{\btrue}{a}{\zero} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & a \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \nmax(a,a) \\ & \href{/posts/arithmetic-made-difficult/MaxAndMin.html#def-max} = & \bif{\nleq(a,a)}{a}{a} \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#thm-leq-reflexive} = & \bif{\btrue}{a}{a} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & a \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \nmin(\zero,a) \\ & \href{/posts/arithmetic-made-difficult/MaxAndMin.html#def-min} = & \bif{\nleq(\zero,a)}{\zero}{a} \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#thm-leq-zero} = & \bif{\btrue}{\zero}{a} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \zero \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \nmin(a,a) \\ & \href{/posts/arithmetic-made-difficult/MaxAndMin.html#def-min} = & \bif{\nleq(a,a)}{a}{a} \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#thm-leq-reflexive} = & \bif{\btrue}{a}{a} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & a \end{eqnarray*}\] as claimed.

_test_max_zero :: (Natural n, Equal n)
  => n -> Test (n -> Bool)
_test_max_zero _ =
  testName "a == max(a,0) and a == max(0,a)" $
  \a -> and (eq a (max a zero)) (eq a (max zero a))


_test_max_idempotent :: (Natural n, Equal n)
  => n -> Test (n -> Bool)
_test_max_idempotent _ =
  testName "a == max(a,a)" $
  \a -> eq (max a a) a


_test_min_zero :: (Natural n, Equal n)
  => n -> Test (n -> Bool)
_test_min_zero _ =
  testName "0 == min(a,0) and 0 == min(0,a)" $
  \a -> and (eq zero (min a zero)) (eq zero (min zero a))


_test_min_idempotent :: (Natural n, Equal n)
  => n -> Test (n -> Bool)
_test_min_idempotent _ =
  testName "a == min(a,a)" $
  \a -> eq (min a a) a

$\nmax$ and $\nmin$ are commutative.

Let $a,b \in \nats$. Then we have the following.

$\nmax(a,b) = \nmax(b,a)$.
$\nmin(a,b) = \nmin(b,a)$.

If $(a,b) = , we have \[\begin{eqnarray*} & & \nmax(a,b) \\ & \href{/posts/arithmetic-made-difficult/MaxAndMin.html#def-max} = & \bif{\nleq(a,b)}{b}{a} \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-involution} = & \bif{\bnot(\bnot(\nleq(a,b)))}{b}{a} \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-ifnot} = & \bif{\bnot(\nleq(a,b))}{a}{b} \\ & = & \bif{\nleq(b,a)}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/MaxAndMin.html#def-max} = & \nmax(b,a) \end{eqnarray*}\] as claimed; similarly, if $\nleq(b,a) = \bfalse$ then $\nmax(a,b) = \nmax(b,a)$. Suppose then that $\nleq(a,b) = \nleq(b,a) = \btrue$. By antisymmetry we have $a = b$, and thus $\nmax(a,b) = \nmax(b,a)$.
If $(a,b) = , we have \[\begin{eqnarray*} & & \nmin(a,b) \\ & \href{/posts/arithmetic-made-difficult/MaxAndMin.html#def-min} = & \bif{\nleq(a,b)}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-involution} = & \bif{\bnot(\bnot(\nleq(a,b)))}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-ifnot} = & \bif{\bnot(\nleq(a,b))}{b}{a} \\ & = & \bif{\nleq(b,a)}{b}{a} \\ & \href{/posts/arithmetic-made-difficult/MaxAndMin.html#def-min} = & \nmin(b,a) \end{eqnarray*}\] as claimed; similarly, if $\nleq(b,a) = \bfalse$ then $\nmin(a,b) = \nmin(b,a)$. Suppose then that $\nleq(a,b) = \nleq(b,a) = \btrue$. By antisymmetry we have $a = b$, and thus $\nmin(a,b) = \nmin(b,a)$.

_test_max_commutative :: (Natural n, Equal n)
  => n -> Test (n -> n -> Bool)
_test_max_commutative _ =
  testName "max(a,b) == max(b,a)" $
  \a b -> eq (max a b) (max b a)


_test_min_commutative :: (Natural n, Equal n)
  => n -> Test (n -> n -> Bool)
_test_min_commutative _ =
  testName "min(a,b) == min(b,a)" $
  \a b -> eq (min a b) (min b a)

$\nplus$ and $\next$ distribute over $\nmax$ and $\nmin$.