Less Than or Equal To

Posted on 2017-04-05 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 LessThanOrEqualTo
 ( leq, _test_leq, main_leq
 ) where

import Testing
import Booleans
import Not
import And
import Or
import DisjointUnions
import NaturalNumbers
import Plus
import Times
import Minus

Next we’d like to nail down what it means for one natural number to be less than or equal to another. Note that while \(\nplus\) and \(\ntimes\) have signatures \[\nats \times \nats \rightarrow \nats,\] “less than or equal to” (which I will abbrebiate to leq from now on) does not. In fact relations like this are typically defined as a set of pairs. To make “less than” computable, we will instead (try to) define it as a function with signature \[\nats \times \nats \rightarrow \bool.\] In fact, we can make a reasonable attempt on \(\nleq\) without using (explicit) recursion at all.

Define \(\nleq : \nats \times \nats \rightarrow \bool\) by \[\nleq(a,b) = \isRgt(\nminus(b,a)).\]

In Haskell:

leq :: (Natural n) => n -> n -> Bool
leq a b = isRgt (minus b a)

First some basic (but important!) special cases.

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

\(\nleq(\zero,a) = \btrue\).
\(\nleq(\next(a),\zero) = \bfalse\).
\(\nleq(\next(\next(a)),\next(\zero)) = \bfalse\).
\(\nleq(\next(a),a) = \bfalse\).
\(\nleq(a,\nplus(a,b)) = \btrue\).

We have \[\begin{eqnarray*} & & \nleq(\zero,a) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#dfn-leq} = & \isRgt(\nminus(a,\zero)) \\ & = & \isRgt(\rgt(a)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-isRgt-rgt} = & \btrue \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \nleq(\next(a),\zero) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#dfn-leq} = & \isRgt(\nminus(\zero,\next(a))) \\ & \href{/posts/arithmetic-made-difficult/Minus.html#thm-minus-zero-next} = & \isRgt(\lft(\ast)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-isRgt-lft} = & \bfalse \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \nleq(\next(\next(a)),\next(\zero)) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#dfn-leq} = & \isRgt(\nminus(\next(\zero),\next(\next(a)))) \\ & \href{/posts/arithmetic-made-difficult/Minus.html#thm-minus-next-cancel} = & \isRgt(\nminus(\zero,\next(a))) \\ & \href{/posts/arithmetic-made-difficult/Minus.html#thm-minus-zero-next} = & \isRgt(\lft(\ast)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-isRgt-lft} = & \bfalse \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \nleq(\next(a),a) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#dfn-leq} = & \isRgt(\nminus(a,\next(a))) \\ & \href{/posts/arithmetic-made-difficult/Minus.html#thm-minus-next-self} = & \isRgt(\lft(\ast)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#thm-isRgt-lft} = & \bfalse \end{eqnarray*}\] as claimed.
We have \(\nminus(\nplus(a,b),a) = \rgt(b)\), so \(\nleq(a,\nplus(a,b)) = \btrue\).

_test_leq_next_nat_zero :: (Natural n, Equal n)
  => n -> Test (n -> Bool)
_test_leq_next_nat_zero _ =
  testName "leq(next(a),zero) == false" $
  \a -> eq (leq (next a) zero) false


_test_leq_next_next_nat_one :: (Natural n, Equal n)
  => n -> Test (n -> Bool)
_test_leq_next_next_nat_one _ =
  testName "leq(next(next(a)),next(zero)) == false" $
  \a -> eq (leq (next (next a)) (next zero)) false


_test_leq_next_nat :: (Natural n, Equal n)
  => n -> Test (n -> Bool)
_test_leq_next_nat _ =
  testName "leq(next(a),a) == false" $
  \a -> eq (leq (next a) a) false


_test_leq_right_plus :: (Natural n, Equal n)
  => n -> Test (n -> n -> Bool)
_test_leq_right_plus _ =
  testName "leq(a,plus(a,b)) == true" $
  \a b -> eq (leq a (plus a b)) true

This lemma will also come in handy.

For all \(a,b \in \nats\) we have \(\nleq(\next(a),\next(b)) = \nleq(a,b)\).

We have \[\begin{eqnarray*} & & \nleq(\next(a),\next(b)) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#dfn-leq} = & \isRgt(\nminus(\next(b),\next(a))) \\ & \href{/posts/arithmetic-made-difficult/Minus.html#thm-minus-next-cancel} = & \isRgt(\nminus(b,a)) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#dfn-leq} = & \nleq(a,b) \end{eqnarray*}\] as claimed.

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

We can characterize \(\nleq(a,b)\) in terms of the solubility of the equation \(b = \nplus(a,x)\) as follows.

Let \(a,b \in \nats\). Then \(\nleq(a,b) = \btrue\) if and only if there exists a \(c \in \nats\) such that \(b = \nplus(a,c)\).

We have \(\nleq(a,b) = \btrue\) if and only if \(\nminus(b,a) = \rgt(c)\) for some \(c \in \nats\), if and only if \(b = \nplus(a,c)\) for some \(c \in \nats\).

From here we can more easily prove some familiar properties of \(\nleq\).

We have the following.

(Reflexivity) Let \(a \in \nats\). Then \(\nleq(a,a)\).
(Antisymmetry) Let \(a,b \in \nats\). If \(\nleq(a,b)\) and \(\nleq(b,a)\), then \(a = b\).
(Transitivity) Let \(a,b,c \in \nats\). If \(\nleq(a,b)\) and \(\nleq(b,c)\), then \(\nleq(a,c)\).

We have \(a = \nplus(a,\zero)\), so that \(\nminus(a,a) = \zero\), thus \(\nleq(a,a) = \btrue\).
Suppose \(\nleq(a,b)\) and \(\nleq(b,a)\); then there exist \(u,v \in \nats\) such that \(b = \nplus(a,u)\) and \(a = \nplus(b,v)\). Now \[\begin{eqnarray*} & & \nplus(a,\zero) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-zero-right} = & a \\ & = & \nplus(b,v) \\ & = & \nplus(\nplus(a,u),v) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-associative} = & \nplus(a,\nplus(u,v)) \end{eqnarray*}\] so that \(\zero = \nplus(u,v)\), and thus \(u = v = \zero\). So \(b = \nplus(a,\zero) = a\) as claimed.
Suppose \(\nleq(a,b)\) and \(\nleq(b,c)\); then there exist \(u,v \in \nats\) such that \(b = \nplus(a,u)\) and \(c = \nplus(b,v)\). Now \[\begin{eqnarray*} & & c \\ & = & \nplus(b,v) \\ & = & \nplus(\nplus(a,u),v) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-associative} = & \nplus(a,\nplus(u,v)) \end{eqnarray*}\] as needed.

_test_leq_reflexive :: (Natural n, Equal n)
  => n -> Test (n -> Bool)
_test_leq_reflexive _ =
  testName "leq(a,a) == true" $
  \a -> eq (leq a a) true


_test_leq_antisymmetric :: (Natural n, Equal n)
  => n -> Test (n -> n -> Bool)
_test_leq_antisymmetric _ =
  testName "if and(leq(a,b),leq(b,a)) then eq(a,b)" $
  \a b -> if and (leq a b) (leq b a)
    then eq a b
    else true


_test_leq_transitive :: (Natural n, Equal n)
  => n -> Test (n -> n -> n -> Bool)
_test_leq_transitive _ =
  testName "if and(leq(a,b),leq(b,c)) then leq(a,c)" $
  \a b c -> if and (leq a b) (leq b c)
    then leq a c
    else true

Now \(\nleq\) interacts nicely with \(\nplus\).

The following hold for all \(a,b,c,d \in \nats\).

\(\nleq(a,b) = \nleq(\nplus(a,c),\nplus(b,c))\).
\(\nleq(a,b) = \nleq(\nplus(c,a),\nplus(c,b))\).
If \(\nleq(a,b)\) and \(\nleq(c,d)\), then \(\nleq(\nplus(a,c),\nplus(b,d))\).

We proceed by induction on \(c\). For the base case, note that \[\nleq(\nplus(a,\zero),\nplus(b,\zero)) = \nleq(a,b)\] as needed. For the inductive step, suppose the result holds for some \(c\). Now \[\begin{eqnarray*} & & \nleq(\nplus(a,\next(c)),\nplus(b,\next(c))) \\ & = & \nleq(\nplus(\next(a),c),\nplus(\next(b),c)) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#thm-leq-plus-compatible-right} = & \nleq(\next(a),\next(b)) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#thm-leq-next-cancel} = & \nleq(a,b) \end{eqnarray*}\] as needed.
We have \[\nleq(\nplus(c,a),\nplus(c,b)) = \nleq(\nplus(a,c),\nplus(b,c)) = \nleq(a,b).\]
We have \[\btrue = \nleq(a,b) = \nleq(\nplus(a,c),\nplus(b,c))\] and \[\begin{eqnarray*} & & \btrue \\ & = & \nleq(c,d) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#thm-leq-plus-compatible-right} = & \nleq(\nplus(c,b),\nplus(d,b)) \\ & = & \nleq(\nplus(b,c),\nplus(b,d)). \end{eqnarray*}\] The result holds by transitivity.

_test_leq_plus_nat_right :: (Natural n, Equal n)
  => n -> Test (n -> n -> n -> Bool)
_test_leq_plus_nat_right _ =
  testName "leq(a,b) == leq(plus(a,c),plus(b,c))" $
  \a b c -> eq (leq a b) (leq (plus a c) (plus b c))


_test_leq_plus_nat_left :: (Natural n, Equal n)
  => n -> Test (n -> n -> n -> Bool)
_test_leq_plus_nat_left _ =
  testName "leq(a,b) == leq(plus(c,a),plus(c,b))" $
  \a b c -> eq (leq a b) (leq (plus c a) (plus c b))


_test_leq_plus_compatible :: (Natural n, Equal n)
  => n -> Test (n -> n -> n -> n -> Bool)
_test_leq_plus_compatible _ =
  testName "if and(leq(a,b),leq(c,d)) then leq(plus(a,c),plus(b,d))" $
  \a b c d -> if and (leq a b) (leq c d)
    then leq (plus a c) (plus b d)
    else true

We can perform case analysis using \(\nleq\).

The following hold for all \(a,b \in \nats\).

If \(\nleq(a,b)\) is false, then \(\nleq(b,a)\) is true.
Precisely one of the following is true: (i) \(a = b\), (ii) \(a \neq b\) and \(\nleq(a,b)\), and (iii) \(a \neq b\) and \(\nleq(b,a)\).
If \(\nleq(a,\next(b))\), then either \(\nleq(a,b)\) or \(a = \next(b)\).
If \(\nleq(b,a)\) and \(\nleq(a,\next(b))\), then either \(a = b\) or \(a = \next(b)\).

If \(\nleq(a,b)\) is false, we have \(\nminus(b,a) = \lft(\ast)\). Now \(\nminus(a,b) \rgt(c)\) for some \(c\), so that \(\nminus(b,a)\) is true.
If \(a \neq b\) and \(\nleq(a,b)\) is false, then \(\nleq(b,a)\) is true. If \(a \neq b\) and both \(\nleq(a,b)\) and \(\nleq(b,a)\), then \(a = b\), which is absurd.
Say \(\next(b) = \nplus(a,c)\). If \(c = \zero\), we have \(a = \next(b)\). If \(c = \next(d)\), we have \[\next(b) = \nplus(a,\next(d)) = \next(\nplus(a,d))\] so that \(b = \nplus(a,d)\) and thus \(\nleq(a,b)\).
By (3), either \(a = \next(b)\) or \(\nleq(a,b)\); if \(\nleq(a,b)\), then by antisymmetry we have \(a = b\) as claimed.

_test_leq_swap_false :: (Natural n, Equal n)
  => n -> Test (n -> n -> Bool)
_test_leq_swap_false _ =
  testName "if not(leq(a,b)) then leq(b,a)" $
  \a b -> if not (leq a b)
    then leq b a
    else true


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


_test_leq_next_dichotomy :: (Natural n, Equal n)
  => n -> Test (n -> n -> Bool)
_test_leq_next_dichotomy _ =
  testName "if leq(a,next(b)) then or(leq(a,b),eq(a,next(b)))" $
  \a b -> if leq a (next b)
    then or (leq a b) (eq a (next b))
    else true


_test_leq_next_squeeze :: (Natural n, Equal n)
  => n -> Test (n -> n -> Bool)
_test_leq_next_squeeze _ =
  testName "if and(leq(b,a),leq(a,next(b))) then or(eq(a,b),eq(a,next(b)))" $
  \a b -> if and (leq b a) (leq a (next b))
    then or (eq a b) (eq a (next b))
    else true

And here comes \(\ntimes\):

The following hold for all \(a,b,c,d \in \nats\).

\(\nleq(a,b) = \nleq(\ntimes(a,\next(c)),\nplus(b,\next(c)))\).
Let \(a,b,c,d \in \nats\). If \(\nleq(a,b)\) and \(\nleq(c,d)\), then \(\nleq(\ntimes(a,c),\ntimes(b,d))\).

We proceed by induction on \(c\). For the base case, note that \[\nleq(\ntimes(a,\next(\zero)),\ntimes(b,\next(\zero))) = \nleq(a,b).\] For the inductive step, suppose the result holds for some \(c\). We consider three possibilities. First suppose \(a = b\); in this case we have \(\nleq(a,b) = \btrue\) and \[\ntimes(a,\next(\next(c))) = \ntimes(b,\next(\next(c))),\] so the conclusion holds. Next, suppose \(a \neq b\) and \(\nleq(a,b) = \btrue\). By the inductive hypothesis we have \[\nleq(\ntimes(a,\next(c)),\nplus(b,\next(c))) = \btrue,\] and so \[\begin{eqnarray*} & & \btrue \\ & = & \nleq(\nplus(\ntimes(a,\next(c)),a),\nplus(\ntimes(b,\next(c)),b)) \\ & = & \nleq(\ntimes(a,\next(\next(c))),\ntimes(b,\next(\next(c)))) \end{eqnarray*}\] as needed. Finally, suppose \(a \neq b\) and \(\nleq(a,b)\) is false. Then \(\nleq(b,a)\) is true, and by the prior argument we have \[\nleq(b,a) = \nleq(\ntimes(a,\next(\next(c))),\ntimes(b,\next(\next(c)))).\] Note that \[\ntimes(a,\next(\next(c))) \neq \ntimes(b,\next(\next(c)))\] (since \(a \neq b\)). So we have \[\nleq(\ntimes(a,\next(\next(c))),\nplus(b,\next(\next(c))))\] as needed.
There are two possibilities for \(c\). If \(c = \zero\), then we have \[\begin{eqnarray*} & & \nleq(\ntimes(a,c),\ntimes(b,d)) \\ & = & \nleq(\zero,\ntimes(b,d)) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#thm-leq-zero} = & \btrue \end{eqnarray*}\] Suppose instead that \(c = \next(u)\). Now there are two possibilities for \(b\). If \(b = \zero\), then in fact \(a = \zero\), and we have \[\begin{eqnarray*} & & \nleq(\ntimes(a,c),\ntimes(b,d)) \\ & = & \nleq(\zero,\zero) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#thm-leq-reflexive} = & \btrue \end{eqnarray*}\] as needed. Suppose then that \(b = \next(v)\). Now we have \[\begin{eqnarray*} & & \btrue \\ & = & \nleq(\ntimes(a,\next(u)),\ntimes(b,\next(u))) \\ & = & \nleq(\ntimes(a,c),\ntimes(b,c)) \end{eqnarray*}\] and \[\begin{eqnarray*} & & \btrue \\ & = & \nleq(\ntimes(c,\next(v)),\ntimes(d,\next(v))) \\ & = & \nleq(\ntimes(b,c),\ntimes(b,d)). \end{eqnarray*}\] The conclusion holds by transitivity.

_test_leq_times_compatible :: (Natural n, Equal n)
  => n -> Test (n -> n -> n -> Bool)
_test_leq_times_compatible _ =
  testName "leq(a,b) == leq(times(a,next(c)),times(b,next(c)))" $
  \a b c -> eq (leq a b) (leq (times a (next c)) (times b (next c)))

That’s enough.

Testing

Suite:

_test_leq :: (TypeName n, Natural n, Equal n, Arbitrary n, Show n)
  => Int -> Int -> n -> IO ()
_test_leq size cases n = do
  testLabel1 "leq" n
  let args = testArgs size cases

  runTest args (_test_leq_next_nat_zero n)
  runTest args (_test_leq_next_next_nat_one n)
  runTest args (_test_leq_next_nat n)
  runTest args (_test_leq_right_plus n)
  runTest args (_test_leq_next_cancel n)
  runTest args (_test_leq_reflexive n)
  runTest args (_test_leq_antisymmetric n)
  runTest args (_test_leq_transitive n)
  runTest args (_test_leq_plus_nat_right n)
  runTest args (_test_leq_plus_nat_left n)
  runTest args (_test_leq_plus_compatible n)
  runTest args (_test_leq_swap_false n)
  runTest args (_test_leq_trichotomy n)
  runTest args (_test_leq_next_dichotomy n)
  runTest args (_test_leq_next_squeeze n)
  runTest args (_test_leq_times_compatible n)

Main:

main_leq :: IO ()
main_leq = do
  _test_leq 50 100 (zero :: Unary)