---
title : "Relations: Inductive definition of relations"
permalink : /Relations/
---
```agda
module plfa.part1.Relations where
```
After having defined operations such as addition and multiplication,
the next step is to define relations, such as _less than or equal_.
## Imports
```agda
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Nat.Properties using (+-comm; +-identityʳ; *-comm)
```
## Defining relations
The relation _less than or equal_ has an infinite number of
instances. Here are a few of them:
0 ≤ 0 0 ≤ 1 0 ≤ 2 0 ≤ 3 ...
1 ≤ 1 1 ≤ 2 1 ≤ 3 ...
2 ≤ 2 2 ≤ 3 ...
3 ≤ 3 ...
...
And yet, we can write a finite definition that encompasses
all of these instances in just a few lines. Here is the
definition as a pair of inference rules:
z≤n --------
zero ≤ n
m ≤ n
s≤s -------------
suc m ≤ suc n
And here is the definition in Agda:
```agda
data _≤_ : ℕ → ℕ → Set where
z≤n : ∀ {n : ℕ}
--------
→ zero ≤ n
s≤s : ∀ {m n : ℕ}
→ m ≤ n
-------------
→ suc m ≤ suc n
```
Here `z≤n` and `s≤s` (with no spaces) are constructor names, while
`zero ≤ n`, and `m ≤ n` and `suc m ≤ suc n` (with spaces) are types.
This is our first use of an _indexed_ datatype, where the type `m ≤ n`
is indexed by two naturals, `m` and `n`. In Agda any line beginning
with two or more dashes is a comment, and here we have exploited that
convention to write our Agda code in a form that resembles the
corresponding inference rules, a trick we will use often from now on.
Both definitions above tell us the same two things:
* _Base case_: for all naturals `n`, the proposition `zero ≤ n` holds.
* _Inductive case_: for all naturals `m` and `n`, if the proposition
`m ≤ n` holds, then the proposition `suc m ≤ suc n` holds.
In fact, they each give us a bit more detail:
* _Base case_: for all naturals `n`, the constructor `z≤n`
produces evidence that `zero ≤ n` holds.
* _Inductive case_: for all naturals `m` and `n`, the constructor
`s≤s` takes evidence that `m ≤ n` holds into evidence that
`suc m ≤ suc n` holds.
For example, here in inference rule notation is the proof that
`2 ≤ 4`:
z≤n -----
0 ≤ 2
s≤s -------
1 ≤ 3
s≤s ---------
2 ≤ 4
And here is the corresponding Agda proof:
```agda
_ : 2 ≤ 4
_ = s≤s (s≤s z≤n)
```
## Implicit arguments
This is our first use of implicit arguments. In the definition of
inequality, the two lines defining the constructors use `∀`, very
similar to our use of `∀` in propositions such as:
+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
However, here the declarations are surrounded by curly braces `{ }`
rather than parentheses `( )`. This means that the arguments are
_implicit_ and need not be written explicitly; instead, they are
_inferred_ by Agda's typechecker. Thus, we write `+-comm m n` for the
proof that `m + n ≡ n + m`, but `z≤n` for the proof that `zero ≤ n`,
leaving `n` implicit. Similarly, if `m≤n` is evidence that `m ≤ n`,
we write `s≤s m≤n` for evidence that `suc m ≤ suc n`, leaving both `m`
and `n` implicit.
If we wish, it is possible to provide implicit arguments explicitly by
writing the arguments inside curly braces. For instance, here is the
Agda proof that `2 ≤ 4` repeated, with the implicit arguments made
explicit:
```agda
_ : 2 ≤ 4
_ = s≤s {1} {3} (s≤s {0} {2} (z≤n {2}))
```
One may also identify implicit arguments by name:
```agda
_ : 2 ≤ 4
_ = s≤s {m = 1} {n = 3} (s≤s {m = 0} {n = 2} (z≤n {n = 2}))
```
In the latter format, you can choose to only supply some implicit arguments:
```agda
_ : 2 ≤ 4
_ = s≤s {n = 3} (s≤s {n = 2} z≤n)
```
It is not permitted to swap implicit arguments, even when named.
We can ask Agda to use the same inference to try and infer an _explicit_ term,
by writing `_`. For instance, we can define a variant of the proposition
`+-identityʳ` with implicit arguments:
```agda
+-identityʳ′ : ∀ {m : ℕ} → m + zero ≡ m
+-identityʳ′ = +-identityʳ _
```
We use `_` to ask Agda to infer the value of the _explicit_ argument from
context. There is only one value which gives us the correct proof, `m`, so Agda
happily fills it in.
If Agda fails to infer the value, it reports an error.
## Precedence
We declare the precedence for comparison as follows:
```agda
infix 4 _≤_
```
We set the precedence of `_≤_` at level 4, so it binds less tightly
than `_+_` at level 6 and hence `1 + 2 ≤ 3` parses as `(1 + 2) ≤ 3`.
We write `infix` to indicate that the operator does not associate to
either the left or right, as it makes no sense to parse `1 ≤ 2 ≤ 3` as
either `(1 ≤ 2) ≤ 3` or `1 ≤ (2 ≤ 3)`.
## Decidability
Given two numbers, it is straightforward to compute whether or not the
first is less than or equal to the second. We don't give the code for
doing so here, but will return to this point in
Chapter [Decidable](/Decidable/).
## Inversion
In our definitions, we go from smaller things to larger things.
For instance, from `m ≤ n` we can conclude `suc m ≤ suc n`,
where `suc m` is bigger than `m` (that is, the former contains
the latter), and `suc n` is bigger than `n`. But sometimes we
want to go from bigger things to smaller things.
There is only one way to prove that `suc m ≤ suc n`, for any `m`
and `n`. This lets us invert our previous rule.
```agda
inv-s≤s : ∀ {m n : ℕ}
→ suc m ≤ suc n
-------------
→ m ≤ n
inv-s≤s (s≤s m≤n) = m≤n
```
Here `m≤n` (with no spaces) is a variable name while
`m ≤ n` (with spaces) is a type, and the latter
is the type of the former. It is a common convention
in Agda to derive a variable name by removing
spaces from its type.
Not every rule is invertible; indeed, the rule for `z≤n` has
no non-implicit hypotheses, so there is nothing to invert.
But often inversions of this kind hold.
Another example of inversion is showing that there is
only one way a number can be less than or equal to zero.
```agda
inv-z≤n : ∀ {m : ℕ}
→ m ≤ zero
--------
→ m ≡ zero
inv-z≤n z≤n = refl
```
## Properties of ordering relations
Relations pop up all the time, and mathematicians have agreed
on names for some of the most common properties.
* _Reflexive_. For all `n`, the relation `n ≤ n` holds.
* _Transitive_. For all `m`, `n`, and `p`, if `m ≤ n` and
`n ≤ p` hold, then `m ≤ p` holds.
* _Anti-symmetric_. For all `m` and `n`, if both `m ≤ n` and
`n ≤ m` hold, then `m ≡ n` holds.
* _Total_. For all `m` and `n`, either `m ≤ n` or `n ≤ m`
holds.
The relation `_≤_` satisfies all four of these properties.
There are also names for some combinations of these properties.
* _Preorder_. Any relation that is reflexive and transitive.
* _Partial order_. Any preorder that is also anti-symmetric.
* _Total order_. Any partial order that is also total.
If you ever bump into a relation at a party, you now know how
to make small talk, by asking it whether it is reflexive, transitive,
anti-symmetric, and total. Or instead you might ask whether it is a
preorder, partial order, or total order.
Less frivolously, if you ever bump into a relation while reading a
technical paper, this gives you a way to orient yourself, by checking
whether or not it is a preorder, partial order, or total order. A
careful author will often call out these properties---or their
lack---for instance by saying that a newly introduced relation is a
partial order but not a total order.
#### Exercise `orderings` (practice) {#orderings}
Give an example of a preorder that is not a partial order.
```agda
-- Your code goes here
-- Divides relation on ints
```
Give an example of a partial order that is not a total order.
```agda
-- Your code goes here
-- Divides relation on nats
```
## Reflexivity
The first property to prove about comparison is that it is reflexive:
for any natural `n`, the relation `n ≤ n` holds. We follow the
convention in the standard library and make the argument implicit,
as that will make it easier to invoke reflexivity:
```agda
≤-refl : ∀ {n : ℕ}
-----
→ n ≤ n
≤-refl {zero} = z≤n
≤-refl {suc n} = s≤s ≤-refl
```
The proof is a straightforward induction on the implicit argument `n`.
In the base case, `zero ≤ zero` holds by `z≤n`. In the inductive
case, the inductive hypothesis `≤-refl {n}` gives us a proof of `n ≤
n`, and applying `s≤s` to that yields a proof of `suc n ≤ suc n`.
It is a good exercise to prove reflexivity interactively in Emacs,
using holes and the `C-c C-c`, `C-c C-,`, and `C-c C-r` commands.
## Transitivity
The second property to prove about comparison is that it is
transitive: for any naturals `m`, `n`, and `p`, if `m ≤ n` and `n ≤ p`
hold, then `m ≤ p` holds. Again, `m`, `n`, and `p` are implicit:
```agda
≤-trans : ∀ {m n p : ℕ}
→ m ≤ n
→ n ≤ p
-----
→ m ≤ p
≤-trans z≤n _ = z≤n
≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p)
```
Here the proof is by induction on the _evidence_ that `m ≤ n`. In the
base case, the first inequality holds by `z≤n` and must show `zero ≤ p`,
which follows immediately by `z≤n`. In this case, the fact that
`n ≤ p` is irrelevant, and we write `_` as the pattern to indicate
that the corresponding evidence is unused.
In the inductive case, the first inequality holds by `s≤s m≤n`
and the second inequality by `s≤s n≤p`, and so we are given
`suc m ≤ suc n` and `suc n ≤ suc p`, and must show `suc m ≤ suc p`.
The inductive hypothesis `≤-trans m≤n n≤p` establishes
that `m ≤ p`, and our goal follows by applying `s≤s`.
The case `≤-trans (s≤s m≤n) z≤n` cannot arise, since the first
inequality implies the middle value is `suc n` while the second
inequality implies that it is `zero`. Agda can determine that such a
case cannot arise, and does not require (or permit) it to be listed.
Alternatively, we could make the implicit parameters explicit:
```agda
≤-trans′ : ∀ (m n p : ℕ)
→ m ≤ n
→ n ≤ p
-----
→ m ≤ p
≤-trans′ zero _ _ z≤n _ = z≤n
≤-trans′ (suc m) (suc n) (suc p) (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans′ m n p m≤n n≤p)
```
One might argue that this is clearer or one might argue that the extra
length obscures the essence of the proof. We will usually opt for
shorter proofs.
The technique of induction on evidence that a property holds (e.g.,
inducting on evidence that `m ≤ n`)---rather than induction on
values of which the property holds (e.g., inducting on `m`)---will turn
out to be immensely valuable, and one that we use often.
Again, it is a good exercise to prove transitivity interactively in Emacs,
using holes and the `C-c C-c`, `C-c C-,`, and `C-c C-r` commands.
## Anti-symmetry
The third property to prove about comparison is that it is
antisymmetric: for all naturals `m` and `n`, if both `m ≤ n` and
`n ≤ m` hold, then `m ≡ n` holds:
```agda
≤-antisym : ∀ {m n : ℕ}
→ m ≤ n
→ n ≤ m
-----
→ m ≡ n
≤-antisym z≤n z≤n = refl
≤-antisym (s≤s m≤n) (s≤s n≤m) = cong suc (≤-antisym m≤n n≤m)
```
Again, the proof is by induction over the evidence that `m ≤ n`
and `n ≤ m` hold.
In the base case, both inequalities hold by `z≤n`, and so we are given
`zero ≤ zero` and `zero ≤ zero` and must show `zero ≡ zero`, which
follows by reflexivity. (Reflexivity of equality, that is, not
reflexivity of inequality.)
In the inductive case, the first inequality holds by `s≤s m≤n` and the
second inequality holds by `s≤s n≤m`, and so we are given `suc m ≤ suc n`
and `suc n ≤ suc m` and must show `suc m ≡ suc n`. The inductive
hypothesis `≤-antisym m≤n n≤m` establishes that `m ≡ n`, and our goal
follows by congruence.
#### Exercise `≤-antisym-cases` (practice) {#leq-antisym-cases}
The above proof omits cases where one argument is `z≤n` and one
argument is `s≤s`. Why is it ok to omit them?
```agda
-- Your code goes here
-- Because if one of the implicit arguments (`m` or `n`) is zero, it cannot be greater than anything else that's non-zero
≤-antisym' : ∀ {m n : ℕ}
→ m ≤ n
→ n ≤ m
-----
→ m ≡ n
≤-antisym' z≤n z≤n = refl
≤-antisym' (s≤s m≤n) (s≤s n≤m) = cong suc (≤-antisym m≤n n≤m)
-- The case for the constructor s≤s is impossible
-- because unification ended with a conflicting equation
-- suc n ≟ zero
-- Possible solution: remove the clause, or use an absurd pattern ().
-- when checking that the pattern s≤s n≤m has type n ≤ zero
-- ≤-antisym' z≤n (s≤s n≤m) = ?
-- ≤-antisym' (s≤s n≤m) z≤n = ?
```
## Total
The fourth property to prove about comparison is that it is total:
for any naturals `m` and `n` either `m ≤ n` or `n ≤ m`, or both if
`m` and `n` are equal.
We specify what it means for inequality to be total:
```agda
data Total (m n : ℕ) : Set where
forward :
m ≤ n
---------
→ Total m n
flipped :
n ≤ m
---------
→ Total m n
```
Evidence that `Total m n` holds is either of the form
`forward m≤n` or `flipped n≤m`, where `m≤n` and `n≤m` are
evidence of `m ≤ n` and `n ≤ m` respectively.
(For those familiar with logic, the above definition
could also be written as a disjunction. Disjunctions will
be introduced in Chapter [Connectives](/Connectives/).)
This is our first use of a datatype with _parameters_,
in this case `m` and `n`. It is equivalent to the following
indexed datatype:
```agda
data Total′ : ℕ → ℕ → Set where
forward′ : ∀ {m n : ℕ}
→ m ≤ n
----------
→ Total′ m n
flipped′ : ∀ {m n : ℕ}
→ n ≤ m
----------
→ Total′ m n
```
Each parameter of the type translates as an implicit parameter of each
constructor. Unlike an indexed datatype, where the indexes can vary
(as in `zero ≤ n` and `suc m ≤ suc n`), in a parameterised datatype
the parameters must always be the same (as in `Total m n`).
Parameterised declarations are shorter, easier to read, and
occasionally aid Agda's termination checker, so we will use them in
preference to indexed types when possible.
With that preliminary out of the way, we specify and prove totality:
```agda
≤-total : ∀ (m n : ℕ) → Total m n
≤-total zero n = forward z≤n
≤-total (suc m) zero = flipped z≤n
≤-total (suc m) (suc n) with ≤-total m n
... | forward m≤n = forward (s≤s m≤n)
... | flipped n≤m = flipped (s≤s n≤m)
```
In this case the proof is by induction over both the first
and second arguments. We perform a case analysis:
* _First base case_: If the first argument is `zero` and the
second argument is `n` then the forward case holds,
with `z≤n` as evidence that `zero ≤ n`.
* _Second base case_: If the first argument is `suc m` and the
second argument is `zero` then the flipped case holds, with
`z≤n` as evidence that `zero ≤ suc m`.
* _Inductive case_: If the first argument is `suc m` and the
second argument is `suc n`, then the inductive hypothesis
`≤-total m n` establishes one of the following:
+ The forward case of the inductive hypothesis holds with `m≤n` as
evidence that `m ≤ n`, from which it follows that the forward case of the
proposition holds with `s≤s m≤n` as evidence that `suc m ≤ suc n`.
+ The flipped case of the inductive hypothesis holds with `n≤m` as
evidence that `n ≤ m`, from which it follows that the flipped case of the
proposition holds with `s≤s n≤m` as evidence that `suc n ≤ suc m`.
This is our first use of the `with` clause in Agda. The keyword
`with` is followed by an expression and one or more subsequent lines.
Each line begins with an ellipsis (`...`) and a vertical bar (`|`),
followed by a pattern to be matched against the expression
and the right-hand side of the equation.
Every use of `with` is equivalent to defining a helper function. For
example, the definition above is equivalent to the following:
```agda
≤-total′ : ∀ (m n : ℕ) → Total m n
≤-total′ zero n = forward z≤n
≤-total′ (suc m) zero = flipped z≤n
≤-total′ (suc m) (suc n) = helper (≤-total′ m n)
where
helper : Total m n → Total (suc m) (suc n)
helper (forward m≤n) = forward (s≤s m≤n)
helper (flipped n≤m) = flipped (s≤s n≤m)
```
This is also our first use of a `where` clause in Agda. The keyword `where` is
followed by one or more definitions, which must be indented. Any variables
bound on the left-hand side of the preceding equation (in this case, `m` and
`n`) are in scope within the nested definition, and any identifiers bound in the
nested definition (in this case, `helper`) are in scope in the right-hand side
of the preceding equation.
If both arguments are equal, then both cases hold and we could return evidence
of either. In the code above we return the forward case, but there is a
variant that returns the flipped case:
```agda
≤-total″ : ∀ (m n : ℕ) → Total m n
≤-total″ m zero = flipped z≤n
≤-total″ zero (suc n) = forward z≤n
≤-total″ (suc m) (suc n) with ≤-total″ m n
... | forward m≤n = forward (s≤s m≤n)
... | flipped n≤m = flipped (s≤s n≤m)
```
It differs from the original code in that it pattern
matches on the second argument before the first argument.
## Monotonicity
If one bumps into both an operator and an ordering at a party, one may ask if
the operator is _monotonic_ with regard to the ordering. For example, addition
is monotonic with regard to inequality, meaning:
∀ {m n p q : ℕ} → m ≤ n → p ≤ q → m + p ≤ n + q
The proof is straightforward using the techniques we have learned, and is best
broken into three parts. First, we deal with the special case of showing
addition is monotonic on the right:
```agda
+-monoʳ-≤ : ∀ (n p q : ℕ)
→ p ≤ q
-------------
→ n + p ≤ n + q
+-monoʳ-≤ zero p q p≤q = p≤q
+-monoʳ-≤ (suc n) p q p≤q = s≤s (+-monoʳ-≤ n p q p≤q)
```
The proof is by induction on the first argument.
* _Base case_: The first argument is `zero` in which case
`zero + p ≤ zero + q` simplifies to `p ≤ q`, the evidence
for which is given by the argument `p≤q`.
* _Inductive case_: The first argument is `suc n`, in which case
`suc n + p ≤ suc n + q` simplifies to `suc (n + p) ≤ suc (n + q)`.
The inductive hypothesis `+-monoʳ-≤ n p q p≤q` establishes that
`n + p ≤ n + q`, and our goal follows by applying `s≤s`.
Second, we deal with the special case of showing addition is
monotonic on the left. This follows from the previous
result and the commutativity of addition:
```agda
+-monoˡ-≤ : ∀ (m n p : ℕ)
→ m ≤ n
-------------
→ m + p ≤ n + p
+-monoˡ-≤ m n p m≤n rewrite +-comm m p | +-comm n p = +-monoʳ-≤ p m n m≤n
```
Rewriting by `+-comm m p` and `+-comm n p` converts `m + p ≤ n + p` into
`p + m ≤ p + n`, which is proved by invoking `+-monoʳ-≤ p m n m≤n`.
Third, we combine the two previous results:
```agda
+-mono-≤ : ∀ (m n p q : ℕ)
→ m ≤ n
→ p ≤ q
-------------
→ m + p ≤ n + q
+-mono-≤ m n p q m≤n p≤q = ≤-trans (+-monoˡ-≤ m n p m≤n) (+-monoʳ-≤ n p q p≤q)
```
Invoking `+-monoˡ-≤ m n p m≤n` proves `m + p ≤ n + p` and invoking
`+-monoʳ-≤ n p q p≤q` proves `n + p ≤ n + q`, and combining these with
transitivity proves `m + p ≤ n + q`, as was to be shown.
#### Exercise `*-mono-≤` (stretch)
Show that multiplication is monotonic with regard to inequality.
```agda
-- Your code goes here
*-monoʳ-≤ : ∀ (n p q : ℕ)
→ p ≤ q
→ n * p ≤ n * q
*-monoʳ-≤ zero p q p≤q = z≤n
-- Goal: p + n * p ≤ q + n * q
*-monoʳ-≤ (suc n) p q p≤q =
let n*p≤n*q = (*-monoʳ-≤ n p q p≤q) in
+-mono-≤ p q (n * p) (n * q) p≤q n*p≤n*q
*-monoˡ-≤ : ∀ (m n p : ℕ)
→ m ≤ n
→ m * p ≤ n * p
*-monoˡ-≤ m n p m≤n rewrite *-comm m p | *-comm n p = *-monoʳ-≤ p m n m≤n
*-mono-≤ : ∀ (m n p q : ℕ)
→ m ≤ n
→ p ≤ q
→ m * p ≤ n * q
*-mono-≤ m n p q m≤n p≤q = ≤-trans (*-monoˡ-≤ m n p m≤n) (*-monoʳ-≤ n p q p≤q)
```
## Strict inequality {#strict-inequality}
We can define strict inequality similarly to inequality:
```agda
infix 4 _<_
data _<_ : ℕ → ℕ → Set where
z<s : ∀ {n : ℕ}
------------
→ zero < suc n
s<s : ∀ {m n : ℕ}
→ m < n
-------------
→ suc m < suc n
```
The key difference is that zero is less than the successor of an
arbitrary number, but is not less than zero.
Clearly, strict inequality is not reflexive. However it is
_irreflexive_ in that `n < n` never holds for any value of `n`.
Like inequality, strict inequality is transitive.
Strict inequality is not total, but satisfies the closely related property of
_trichotomy_: for any `m` and `n`, exactly one of `m < n`, `m ≡ n`, or `m > n`
holds (where we define `m > n` to hold exactly when `n < m`).
It is also monotonic with regards to addition and multiplication.
Most of the above are considered in exercises below. Irreflexivity
requires negation, as does the fact that the three cases in
trichotomy are mutually exclusive, so those points are deferred to
Chapter [Negation](/Negation/).
It is straightforward to show that `suc m ≤ n` implies `m < n`,
and conversely. One can then give an alternative derivation of the
properties of strict inequality, such as transitivity, by
exploiting the corresponding properties of inequality.
#### Exercise `<-trans` (recommended) {#less-trans}
Show that strict inequality is transitive. Use a direct proof. (A later
exercise exploits the relation between < and ≤.)
```agda
-- Your code goes here
<-trans : ∀ {m n p : ℕ}
→ m < n
→ n < p
→ m < p
<-trans z<s (s<s n<p) = z<s
<-trans (s<s m<n) (s<s n<p) = s<s (<-trans m<n n<p)
```
#### Exercise `trichotomy` (practice) {#trichotomy}
Show that strict inequality satisfies a weak version of trichotomy, in
the sense that for any `m` and `n` that one of the following holds:
* `m < n`,
* `m ≡ n`, or
* `m > n`.
Define `m > n` to be the same as `n < m`.
You will need a suitable data declaration,
similar to that used for totality.
(We will show that the three cases are exclusive after we introduce
[negation](/Negation/).)
```agda
-- Your code goes here
infix 4 _>_
-- NOTE: This does not work as it has incomplete cases
-- _>_ : ∀ {m n : ℕ} → n < m
-- _>_ {suc m} {zero} = z<s
-- _>_ {suc m} {suc n} = s<s {n} {m} (_>_ {m} {n})
-- NOTE: no relation to `_<_`
data _>_ : ℕ → ℕ → Set where
s>z : ∀ {n : ℕ} → suc n > zero
s>s : ∀ {m n : ℕ} → m > n → suc m > suc n
data Trichotomy (m n : ℕ) : Set where
forward : m > n → Trichotomy m n
flipped : n > m → Trichotomy m n
equal : m ≡ n → Trichotomy m n
-- NOTE: relation to `_<_`, but seems complicated
-- data _>_ : ∀ {m n : ℕ} {n<m : n < m} → Set where
-- s>z : ∀ {m : ℕ} → _>_ {suc m} {zero} {z<s}
-- s>s : ∀ {m n : ℕ} → (n<m : n < m) → _>_ {suc m} {suc n} {s<s n<m}
-- data Trichotomy (m n : ℕ) : Set where
-- forward : (n<m : n < m) → _>_ {m} {n} {n<m} → Trichotomy m n
-- flipped : (m<n : m < n) → _>_ {n} {m} {m<n} → Trichotomy m n
-- equal : m ≡ n → Trichotomy m n
```
#### Exercise `+-mono-<` (practice) {#plus-mono-less}
Show that addition is monotonic with respect to strict inequality.
As with inequality, some additional definitions may be required.
```agda
-- Your code goes here
+-monoʳ-< : ∀ (n p q : ℕ)
→ p < q
→ n + p < n + q
+-monoʳ-< zero p q p<q = p<q
+-monoʳ-< (suc n) p q p<q = s<s (+-monoʳ-< n p q p<q)
+-monoˡ-< : ∀ (m n p : ℕ)
→ m < n
→ m + p < n + p
+-monoˡ-< m n p m<n rewrite +-comm m p | +-comm n p = +-monoʳ-< p m n m<n
+-mono-< : ∀ (m n p q : ℕ)
→ m < n
→ p < q
→ m + p < n + q
+-mono-< m n p q m<n p<q = <-trans (+-monoˡ-< m n p m<n) (+-monoʳ-< n p q p<q)
```
#### Exercise `≤→<, <→≤` (recommended) {#leq-iff-less}
Show that `suc m ≤ n` implies `m < n`, and conversely.
```agda
-- Your code goes here
-- -- NOTE: This doesn't work!
-- -- Case splitting on both m and n seemed to give me absurd cases like the one below.
-- -- The choice of what to match on is very important
-- suc-inv-mono-≤ : ∀ (m n : ℕ) → suc (suc m) ≤ suc n → suc m ≤ n
-- suc-inv-mono-≤ zero zero suc-suc-≤-suc = {!!}
-- suc-inv-mono-≤ zero (suc n) suc-suc-≤-suc = {!!}
-- suc-inv-mono-≤ (suc m) n suc-suc-≤-suc = {!!}
-- -- NOTE: This works, but it's unnecessary as we can match on the proof directly in ≤→<
-- suc-inv-mono-≤ : ∀ (m n : ℕ) → suc (suc m) ≤ suc n → suc m ≤ n
-- suc-inv-mono-≤ m n (s≤s x) = x
≤→< : ∀ (m n : ℕ) → suc m ≤ n → m < n
≤→< zero (suc n) suc-m≤n = z<s
-- NOTE: This was a dead end - I only had to pattern match on the proof
-- ≤→< (suc m) (suc n) suc-m≤n = s<s (≤→< m n (suc-inv-mono-≤ m n suc-m≤n))
≤→< (suc m) (suc n) (s≤s suc-m≤n) = s<s (≤→< m n suc-m≤n)
<→≤ : ∀ {m n : ℕ} → m < n → suc m ≤ n
<→≤ z<s = s≤s z≤n
<→≤ {suc m} {suc n} (s<s m<n) = s≤s (<→≤ m<n)
```
#### Exercise `<-trans-revisited` (practice) {#less-trans-revisited}
Give an alternative proof that strict inequality is transitive,
using the relation between strict inequality and inequality and
the fact that inequality is transitive.
```agda
-- Your code goes here
suc-suc≤→suc≤ : ∀ {m n : ℕ} → suc (suc m) ≤ n → suc m ≤ n
suc-suc≤→suc≤ {zero} {suc n} suc-suc≤ = s≤s z≤n
suc-suc≤→suc≤ {suc m} {suc n} (s≤s suc-suc≤) = s≤s (suc-suc≤→suc≤ suc-suc≤)
<-trans-revisited : ∀ (m n p : ℕ)
→ m < n
→ n < p
→ m < p
<-trans-revisited m n p m<n n<p =
let suc-suc≤ = (≤-trans (s≤s (<→≤ m<n)) (<→≤ n<p))
in ≤→< _ _ (suc-suc≤→suc≤ suc-suc≤)
```
## Even and odd
As a further example, let's specify even and odd numbers. Inequality
and strict inequality are _binary relations_, while even and odd are
_unary relations_, sometimes called _predicates_:
```agda
data even : ℕ → Set
data odd : ℕ → Set
data even where
zero :
---------
even zero
suc : ∀ {n : ℕ}
→ odd n
------------
→ even (suc n)
data odd where
suc : ∀ {n : ℕ}
→ even n
-----------
→ odd (suc n)
```
A number is even if it is zero or the successor of an odd number,
and odd if it is the successor of an even number.
This is our first use of a mutually recursive datatype declaration.
Since each identifier must be defined before it is used, we first
declare the indexed types `even` and `odd` (omitting the `where`
keyword and the declarations of the constructors) and then
declare the constructors (omitting the signatures `ℕ → Set`
which were given earlier).
This is also our first use of _overloaded_ constructors,
that is, using the same name for constructors of different types.
Here `suc` means one of three constructors:
suc : ℕ → ℕ
suc : ∀ {n : ℕ}
→ odd n
------------
→ even (suc n)
suc : ∀ {n : ℕ}
→ even n
-----------
→ odd (suc n)
Similarly, `zero` refers to one of two constructors. Due to how it
does type inference, Agda does not allow overloading of defined names,
but does allow overloading of constructors. It is recommended that
one restrict overloading to related meanings, as we have done here,
but it is not required.
We show that the sum of two even numbers is even:
```agda
e+e≡e : ∀ {m n : ℕ}
→ even m
→ even n
------------
→ even (m + n)
o+e≡o : ∀ {m n : ℕ}
→ odd m
→ even n
-----------
→ odd (m + n)
e+e≡e zero en = en
e+e≡e (suc om) en = suc (o+e≡o om en)
o+e≡o (suc em) en = suc (e+e≡e em en)
```
Corresponding to the mutually recursive types, we use two mutually recursive
functions, one to show that the sum of two even numbers is even, and the other
to show that the sum of an odd and an even number is odd.
This is our first use of mutually recursive functions. Since each identifier
must be defined before it is used, we first give the signatures for both
functions and then the equations that define them.
To show that the sum of two even numbers is even, consider the
evidence that the first number is even. If it is because it is zero,
then the sum is even because the second number is even. If it is
because it is the successor of an odd number, then the result is even
because it is the successor of the sum of an odd and an even number,
which is odd.
To show that the sum of an odd and even number is odd, consider the
evidence that the first number is odd. If it is because it is the
successor of an even number, then the result is odd because it is the
successor of the sum of two even numbers, which is even.
#### Exercise `o+o≡e` (stretch) {#odd-plus-odd}
Show that the sum of two odd numbers is even.
```agda
-- Your code goes here
o+o≡e : ∀ {m n : ℕ}
→ odd m
→ odd n
→ even (m + n)
o+o≡e (suc zero) (suc n) = suc (suc n)
o+o≡e (suc (suc m)) (suc n) = suc (suc (o+o≡e m (suc n)))
```
#### Exercise `Bin-predicates` (stretch) {#Bin-predicates}
Recall that
Exercise [Bin](/Naturals/#Bin)
defines a datatype `Bin` of bitstrings representing natural numbers.
Representations are not unique due to leading zeros.
Hence, eleven may be represented by both of the following:
⟨⟩ I O I I
⟨⟩ O O I O I I
Define a predicate
Can : Bin → Set
over all bitstrings that holds if the bitstring is canonical, meaning
it has no leading zeros; the first representation of eleven above is
canonical, and the second is not. To define it, you will need an
auxiliary predicate
One : Bin → Set
that holds only if the bitstring has a leading one. A bitstring is
canonical if it has a leading one (representing a positive number) or
if it consists of a single zero (representing zero).
Show that increment preserves canonical bitstrings:
Can b
------------
Can (inc b)
Show that converting a natural to a bitstring always yields a
canonical bitstring:
----------
Can (to n)
Show that converting a canonical bitstring to a natural
and back is the identity:
Can b
---------------
to (from b) ≡ b
Hint: For each of these, you may first need to prove related
properties of `One`. It may also help to prove the following:
One b
----------
1 ≤ from b
1 ≤ n
---------------------
to (2 * n) ≡ (to n) O
```agda
-- Your code goes here
data Bin : Set where
⟨⟩ : Bin
_O : Bin → Bin
_I : Bin → Bin
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (rest O) = rest I
inc (rest I) = (inc rest) O
to : ℕ → Bin
to zero = ⟨⟩ O
to (suc n) = inc (to n)
from : Bin → ℕ
from ⟨⟩ = 0
from (rest O) = 2 * (from rest)
from (rest I) = 1 + 2 * (from rest)
-- Also need to show that inc is canonical as in `inc-can`
data One : Bin -> Set where
one : One (⟨⟩ I)
suc : ∀ {b : Bin} → One b → One (inc b)
-- NOTE: Using a bin-law from Induction.lagda.md
from-inc-suc-from : ∀ (b : Bin) → from (inc b) ≡ suc (from b)
from-inc-suc-from ⟨⟩ = refl
from-inc-suc-from (b O) = refl
from-inc-suc-from (b I) rewrite cong (\x → 2 * x) (from-inc-suc-from b) | *-comm 2 (1 + (from b)) | cong (\x → 2 + x) (*-comm (from b) 2) = refl
1≤from-one : ∀ {b : Bin} → One b → 1 ≤ from b
1≤from-one one = s≤s z≤n
1≤from-one (suc {b} x) rewrite from-inc-suc-from b = s≤s z≤n
data Can : Bin → Set where
zero-bin : Can (⟨⟩ O)
leading : ∀ {b : Bin} → One b → Can b
inc-can : ∀ {b : Bin} → Can b → Can (inc b)
inc-can zero-bin = leading one
inc-can (leading x) = leading (suc x)
to-can : (n : ℕ) → Can (to n)
to-can zero = zero-bin
to-can (suc n) = inc-can (to-can n)
```
## Standard library
Definitions similar to those in this chapter can be found in the standard library:
```agda
import Data.Nat using (_≤_; z≤n; s≤s; _<_)
import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total;
+-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
```
In the standard library, `≤-total` is formalised in terms of
disjunction (which we define in
Chapter [Connectives](/Connectives/)),
and `+-monoʳ-≤`, `+-monoˡ-≤`, `+-mono-≤` are proved differently than here,
and more arguments are implicit.
## Unicode
This chapter uses the following unicode:
≤ U+2264 LESS-THAN OR EQUAL TO (\<=, \le)
≥ U+2265 GREATER-THAN OR EQUAL TO (\>=, \ge)
ˡ U+02E1 MODIFIER LETTER SMALL L (\^l)
ʳ U+02B3 MODIFIER LETTER SMALL R (\^r)
The commands `\^l` and `\^r` give access to a variety of superscript
leftward and rightward arrows in addition to superscript letters `l` and `r`.