---
title: Less Than or Equal To
author: nbloomf
date: 2017-04-05
tags: arithmetic-made-difficult, literate-haskell
slug: leq
---

> {-# 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.

:::::: definition ::
[]{#dfn-leq}
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.

:::::: theorem :::::
[]{#thm-leq-zero}[]{#thm-leq-next-zero}[]{#thm-leq-next-next-one}[]{#thm-leq-next-nat}[]{#thm-leq-nat-plus}
Let $a,b \in \nats$. Then we have the following.

1. $\nleq(\zero,a) = \btrue$.
2. $\nleq(\next(a),\zero) = \bfalse$.
3. $\nleq(\next(\next(a)),\next(\zero)) = \bfalse$.
4. $\nleq(\next(a),a) = \bfalse$.
5. $\nleq(a,\nplus(a,b)) = \btrue$.

::: proof ::::::::::
1. We have
$$\begin{eqnarray*}
 &   & \nleq(\zero,a) \\
 &     \href{@leq@#dfn-leq}
   = & \isRgt(\nminus(a,\zero)) \\
 & = & \isRgt(\rgt(a)) \\
 &     \href{@disjoint-unions@#thm-isRgt-rgt}
   = & \btrue
\end{eqnarray*}$$
as claimed.
2. We have
$$\begin{eqnarray*}
 &   & \nleq(\next(a),\zero) \\
 &     \href{@leq@#dfn-leq}
   = & \isRgt(\nminus(\zero,\next(a))) \\
 &     \href{@minus@#thm-minus-zero-next}
   = & \isRgt(\lft(\ast)) \\
 &     \href{@disjoint-unions@#thm-isRgt-lft}
   = & \bfalse
\end{eqnarray*}$$
as claimed.
3. We have
$$\begin{eqnarray*}
 &   & \nleq(\next(\next(a)),\next(\zero)) \\
 &     \href{@leq@#dfn-leq}
   = & \isRgt(\nminus(\next(\zero),\next(\next(a)))) \\
 &     \href{@minus@#thm-minus-next-cancel}
   = & \isRgt(\nminus(\zero,\next(a))) \\
 &     \href{@minus@#thm-minus-zero-next}
   = & \isRgt(\lft(\ast)) \\
 &     \href{@disjoint-unions@#thm-isRgt-lft}
   = & \bfalse
\end{eqnarray*}$$
as claimed.
4. We have
$$\begin{eqnarray*}
 &   & \nleq(\next(a),a) \\
 &     \href{@leq@#dfn-leq}
   = & \isRgt(\nminus(a,\next(a))) \\
 &     \href{@minus@#thm-minus-next-self}
   = & \isRgt(\lft(\ast)) \\
 &     \href{@disjoint-unions@#thm-isRgt-lft}
   = & \bfalse
\end{eqnarray*}$$
as claimed.
5. We have $\nminus(\nplus(a,b),a) = \rgt(b)$, so $\nleq(a,\nplus(a,b)) = \btrue$.
::::::::::::::::::::

::: test :::::::::::

> _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.

:::::: theorem :::::
[]{#thm-leq-next-cancel}
For all $a,b \in \nats$ we have $\nleq(\next(a),\next(b)) = \nleq(a,b)$.

::: proof ::::::::::
We have
$$\begin{eqnarray*}
 &   & \nleq(\next(a),\next(b)) \\
 &     \href{@leq@#dfn-leq}
   = & \isRgt(\nminus(\next(b),\next(a))) \\
 &     \href{@minus@#thm-minus-next-cancel}
   = & \isRgt(\nminus(b,a)) \\
 &     \href{@leq@#dfn-leq}
   = & \nleq(a,b)
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

> _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.

:::::: theorem :::::
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)$.

::: proof ::::::::::
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$.

:::::: theorem :::::
[]{#thm-leq-reflexive}[]{#thm-leq-antisymmetric}[]{#thm-leq-transitive}
We have the following.

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

::: proof ::::::::::
1. We have $a = \nplus(a,\zero)$, so that $\nminus(a,a) = \zero$, thus $\nleq(a,a) = \btrue$.
2. 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{@plus@#thm-plus-zero-right}
   = & a \\
 & = & \nplus(b,v) \\
 & = & \nplus(\nplus(a,u),v) \\
 &     \href{@plus@#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.
3. 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{@plus@#thm-plus-associative}
   = & \nplus(a,\nplus(u,v))
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

> _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$.

:::::: theorem :::::
[]{#thm-leq-plus-compatible-right}[]{#thm-leq-plus-compatible-left}
The following hold for all $a,b,c,d \in \nats$.

1. $\nleq(a,b) = \nleq(\nplus(a,c),\nplus(b,c))$.
2. $\nleq(a,b) = \nleq(\nplus(c,a),\nplus(c,b))$.
3. If $\nleq(a,b)$ and $\nleq(c,d)$, then $\nleq(\nplus(a,c),\nplus(b,d))$.

::: proof ::::::::::
1. 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{@leq@#thm-leq-plus-compatible-right}
   = & \nleq(\next(a),\next(b)) \\
 &     \href{@leq@#thm-leq-next-cancel}
   = & \nleq(a,b)
\end{eqnarray*}$$
as needed.
2. We have $$\nleq(\nplus(c,a),\nplus(c,b)) = \nleq(\nplus(a,c),\nplus(b,c)) = \nleq(a,b).$$
3. We have $$\btrue = \nleq(a,b) = \nleq(\nplus(a,c),\nplus(b,c))$$ and
$$\begin{eqnarray*}
 &   & \btrue \\
 & = & \nleq(c,d) \\
 &     \href{@leq@#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 :::::::::::

> _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$.

:::::: theorem :::::
The following hold for all $a,b \in \nats$.

1. If $\nleq(a,b)$ is false, then $\nleq(b,a)$ is true.
2. 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)$.
3. If $\nleq(a,\next(b))$, then either $\nleq(a,b)$ or $a = \next(b)$.
4. If $\nleq(b,a)$ and $\nleq(a,\next(b))$, then either $a = b$ or $a = \next(b)$.

::: proof ::::::::::
1. 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.
2. 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.
3. 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)$.
4. By (3), either $a = \next(b)$ or $\nleq(a,b)$; if $\nleq(a,b)$, then by antisymmetry we have $a = b$ as claimed.
::::::::::::::::::::

::: test :::::::::::

> _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$:

:::::: theorem :::::
The following hold for all $a,b,c,d \in \nats$.

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

::: proof ::::::::::
1. 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.
2. 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{@leq@#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{@leq@#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 :::::::::::

> _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)