Relations: Inductive definition of relations
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
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ʳ)
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: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 propositionzero ≤ n
holds. - Inductive case: for all naturals
m
andn
, if the propositionm ≤ n
holds, then the propositionsuc m ≤ suc n
holds.
In fact, they each give us a bit more detail:
- Base case: for all naturals
n
, the constructorz≤n
produces evidence thatzero ≤ n
holds. - Inductive case: for all naturals
m
andn
, the constructors≤s
takes evidence thatm ≤ n
holds into evidence thatsuc 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:_ : 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.
2 ≤ 4
repeated, with the implicit arguments made explicit:_ : 2 ≤ 4 _ = s≤s {1} {3} (s≤s {0} {2} (z≤n {2}))One may also identify implicit arguments by name:
_ : 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:
_ : 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:+-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: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.
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.
suc m ≤ suc n
, for any m
and n
. This lets us invert our previous rule.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.
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 relationn ≤ n
holds. - Transitive. For all
m
,n
, andp
, ifm ≤ n
andn ≤ p
hold, thenm ≤ p
holds. - Anti-symmetric. For all
m
andn
, if bothm ≤ n
andn ≤ m
hold, thenm ≡ n
holds. - Total. For all
m
andn
, eitherm ≤ n
orn ≤ 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)
Give an example of a preorder that is not a partial order.
-- Your code goes here
Give an example of a partial order that is not a total order.
-- Your code goes here
Reflexivity
The first property to prove about comparison is that it is reflexive: for any naturaln
, 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:≤-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 naturalsm
, n
, and p
, if m ≤ n
and n ≤ p
hold, then m ≤ p
holds. Again, m
, n
, and p
are implicit:≤-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.
≤-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 naturalsm
and n
, if both m ≤ n
and n ≤ m
hold, then m ≡ n
holds:≤-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)
The above proof omits cases where one argument is z≤n
and one argument is s≤s
. Why is it ok to omit them?
-- Your code goes here
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.
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.)
This is our first use of a datatype with parameters, in this casem
and n
. It is equivalent to the following indexed datatype: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.
≤-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 isn
then the forward case holds, withz≤n
as evidence thatzero ≤ n
.Second base case: If the first argument is
suc m
and the second argument iszero
then the flipped case holds, withz≤n
as evidence thatzero ≤ suc m
.Inductive case: If the first argument is
suc m
and the second argument issuc 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 thatm ≤ n
, from which it follows that the forward case of the proposition holds withs≤s m≤n
as evidence thatsuc m ≤ suc n
.The flipped case of the inductive hypothesis holds with
n≤m
as evidence thatn ≤ m
, from which it follows that the flipped case of the proposition holds withs≤s n≤m
as evidence thatsuc 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.
with
is equivalent to defining a helper function. For example, the definition above is equivalent to the following:≤-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.
≤-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:+-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 casezero + p ≤ zero + q
simplifies top ≤ q
, the evidence for which is given by the argumentp≤q
.Inductive case: The first argument is
suc n
, in which casesuc n + p ≤ suc n + q
simplifies tosuc (n + p) ≤ suc (n + q)
. The inductive hypothesis+-monoʳ-≤ n p q p≤q
establishes thatn + p ≤ n + q
, and our goal follows by applyings≤s
.
+-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
.
+-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.
-- Your code goes here
Strict inequality
We can define strict inequality similarly to inequality: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.
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)
Show that strict inequality is transitive. Use a direct proof. (A later exercise exploits the relation between < and ≤.)
-- Your code goes here
Exercise trichotomy
(practice)
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.)
-- Your code goes here
Exercise +-mono-<
(practice)
Show that addition is monotonic with respect to strict inequality. As with inequality, some additional definitions may be required.
-- Your code goes here
Exercise ≤→<, <→≤
(recommended)
Show that suc m ≤ n
implies m < n
, and conversely.
-- Your code goes here
Exercise <-trans-revisited
(practice)
Give an alternative proof that strict inequality is transitive, using the relation between strict inequality and inequality and the fact that inequality is transitive.
-- Your code goes here
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: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.
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)
Show that the sum of two odd numbers is even.
-- Your code goes here
Exercise Bin-predicates
(stretch)
Recall that Exercise 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
-- Your code goes here
Standard library
Definitions similar to those in this chapter can be found in the standard library: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), 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
.