Relations II – Properties

Last time we defined a relation between the natural numbers that we call inequality (“less than or equal to”), \(\leq\). We opted for this relation instead of strict inequality, \(<\), because it had the property of reflexivity, and we wanted to truthfully assert \(n \leq n\) for any natural number \(n\), which—interpreted as a type—means that it is always inhabited by a term. We will now prove that inequality satisfies the following three properties: reflexivity, transitivity, and antisymmetry.

Before doing that, it is worth pausing to ask just what a property really is. In ordinary speech, we say that a thing “has” such-and-such a property, and we might imagine that the property “attaches to” or is “inherent in” that thing. There is much debate in philosophy (specifically, metaphysics) about what properties amount to. We won’t get into that convoluted debate here. In mathematics, we always try to reduce vague or imprecise notions to either a concrete object or to a clearly-defined statement that something “holds” given some condition(s). In our present case, for example, to say that inequality, \(\leq\), “has” the property of reflexivity means that we can always construct a term or proof of that type, and we do so with a function.

Reflexivity

Recall that inequality is a type family or a collection of types, represented by the curried function \(\_\leq\_: \mathbb{N \to N} \to \mathtt{Set}\), such that each type in the collection is indexed by two natural numbers, e.g., \(1 \leq 2\). Therefore, to say that inequality has the property of reflexivity means that every inequality type of the form \(n \leq n\) is inhabited, or, put differently, that for any natural number \(n\), we can construct a term of the type \(n \leq n\). The proof in Agda code is as follows:

≤-refl : ∀ {n : ℕ} → n ≤ n
≤-refl {0} = z≤n
≤-refl {suc n} = s≤s ≤-refl

The first line (the signature) says that the means by which we can construct that term is a function called \(\text{≤-refl}\), which, given any natural number \(n\), returns (or is) a term of type \(n \leq n\); that is, \(\text{≤-refl}\ \{n\}: n \leq n\). We have to check that this function works on all natural numbers and, as you might guess, we use induction for that.

First we try with argument zero: \(\text{≤-refl}\ \{0\}\) (the base case), then with any successor: \(\text{≤-refl}\ \{\text{suc}\ n \}\) (the inductive step), which requires a recursive call to the inductive hypothesis: \(\text{≤-refl}\ \{n\}\).

\[\begin{align} \text{≤-refl} &: \forall\ \{n: \mathbb{N}\} \to n \leq n\\ \text{≤-refl}\ \{0\} &: 0 \leq 0\\ \text{≤-refl} &= \text{z≤n} \end{align}\]

Recall from the previous entry that \(\text{z≤n}\) is a term (a constant or nullary function) of types whose form is \(0 \leq n\), where \(n\) is any number including zero. Therefore, the proof \(\text{≤-refl} = \text{z≤n} : 0 \leq 0\) follows. Pretty straightforward.

\[\begin{align} \text{≤-refl} &: \forall\ \{n: \mathbb{N}\} \to n \leq n\\ \text{≤-refl}\ \{\text{suc}\ n\} &: \text{suc}\ n \leq \text{suc}\ n\\ \text{≤-refl}\ \{\text{suc}\ n\} &= \text{s≤s\ ≤-refl}\ \{n\}\\ \text{≤-refl} &= \text{s≤s\ ≤-refl} \end{align}\]

Again, from our previous entry, we know that the constructor \(\text{s≤s}\) is a function that, given any two naturals \(m\) and \(n\), constructs a term of \(\mathtt{suc}\ m \leq \mathtt{suc}\ n\), provided there is a term of \(m \leq n\). So for \(\text{s≤s}\) to construct a term of \(\mathtt{suc}\ n \leq \mathtt{suc}\ n\), it needs a term of the type \(n \leq n\). But that term is precisely the inductive hypothesis \(\text{≤-refl}\ \{n\}\). Therefore, applying \(\text{≤-refl}\) to \(\{\text{suc}\ n\}\) gives us the term \(\text{s≤s\ ≤-refl}\ \{n\}\) whose type is \(\mathtt{suc}\ n \leq \mathtt{suc}\ n\). Omitting the implicit arguments in curly braces gives us the equation on line 4 above. This completes the proof. \(\blacksquare\)

Transitivity

Inequality is also transitive. Logically, if \(m\leq n\) is true, and \(n \leq p\) is true, then it follows that \(m\leq p\) is also true. Constructively, if we can construct a term of \(m\leq n\) and a term of \(n \leq p\), then we can construct a term of \(m \leq p\). And we can do this with a function we’ll call \(\text{≤-trans}\).

The PLFA offers us two ways to prove transitivity: one way is by using implicit arguments and using induction, not on the variables, but on the proof/term of the types.¹ This has the advantage of simplifying the notation. The other way is by making the parameters explicit, which we do by enclosing them in parentheses, and then using induction on the variables. This, however, makes the proof longer but perhaps clearer. We’ll go with the longer method first, and then the shorter one.

Base case

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

\[\begin{align} \text{≤-trans}' &: \forall\ (m\ n\ p\ : \mathbb{N}) \to m \leq n \to n \leq p \to m \leq p\\ \text{≤-trans}'\ 0 &: \forall\ (n\ p\ : \mathbb{N})\to 0 \leq n \to n \leq p \to 0 \leq p\\ \text{≤-trans}'\ (0\; \_) &: \forall\ (n : \mathbb{N}) \to 0 \leq n \to n \leq p \to 0 \leq p\\ \text{≤-trans}'\ (0\; \_\; \_) &: 0\leq n \to n \leq p \to 0 \leq p\\ \text{≤-trans}'\ (0\; \_\; \_)\ \text{z≤n} &: n \leq p \to 0 \leq p\\ \text{≤-trans}'\ (0\; \_\; \_)\ \text{z≤n}\; \_ &: 0 \leq p\\ \text{≤-trans}'\ (0\; \_\; \_)\ \text{z≤n}\; \_ &= \text{z≤n} \end{align}\]

We first set \(m = 0\) (second line), and leave \(n\) and \(p\) be whatever values (third and fourth lines) by putting an underscore (a dummy term). On the fifth line, we provide the function \(\text{≤-trans}\ (0\; \_\; \_)\) with a proof/term of \(0 \leq n\). We know that this term is \(\text{z≤n}\). We then get the function \(\text{≤-trans}\ (0\; \_\; \_)\ \text{z≤n}\), which requires a proof of \(n \leq p\) that, once given, will finally return a term of \(0 \leq p\). But we already know that the proof/term of the latter is also \(\text{z≤n}\). So we don’t even bother specifying what the term of \(n \leq p\) is, and just put another dummy term.

As we can see, the derivation is a bit cumbersome, but the logic should not be hard to follow. If instead of using induction on variables we use induction on proof/terms and make the variables implicit (and omit them), then the proof is much shorter. In Agda code:

≤-trans : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p
≤-trans z≤n       _          =  z≤n

\[\begin{align} \text{≤-trans} &: \forall\ \{m\ n\ p\ : \mathbb{N}\} \to m \leq n \to n \leq p \to m \leq p\\ \text{≤-trans} &: 0 \leq n \to n \leq p \to 0 \leq p\\ \text{≤-trans}\ \text{z≤n} &: n \leq p \to 0 \leq p\\ \text{≤-trans}\ \text{z≤n}\;\; \_ \;\; &: 0 \leq p\\ \text{≤-trans}\ \text{z≤n}\;\; \_ \;\; &= \text{z≤n} \end{align}\]

The proof is by induction on the evidence/proof/term of the first type \(m\leq n\). This will allow us to omit all implicit arguments between curly braces, making the notation easier to read.

Inductive step

Returning to the first method, we’ll go ahead and prove the inductive step. Now, due to space constraints, it’s not possible to display currying for this step—the expressions are just too long and exceed the margins of this website. So the proof will be slightly more verbose.

In the base case, the proof ended with the construction of the term \(\text{≤-trans}\ (0\; \_ \; \_)\; \text{z≤n}\; \_\) whose type is \(0 \leq p\).

In the inductive hypothesis, the proof is “assumed” to be the term \(\text{≤-trans}\ (m\; n \; p)\; \text{m≤n}\; \text{n≤p}\) of type \(m \leq p\).

In the inductive step, the explicit arguments for \(\text{≤-trans}\) will be \(\text{≤-trans}\ (\mathtt{suc}\ m \; \mathtt{suc}\ n \; \mathtt{suc}\ p)\). This function has the following function type:

\[ \mathtt{suc}\ m \leq \mathtt{suc}\ n \to \mathtt{suc}\ n \leq \mathtt{suc}\ p \to \mathtt{suc}\ m \leq \mathtt{suc}\ p \]

To get started, we need a term/proof of \(\mathtt{suc}\ m \leq \mathtt{suc}\ n\). From our previous entry, we know that this term is \((\text{s≤s m≤n})\). Once given, we get the function \(\text{≤-trans}\ (\mathtt{suc}\ m \; \mathtt{suc}\ n \; \mathtt{suc}\ p)\ (\text{s≤s m≤n})\) whose type is:

\[ \mathtt{suc}\ n \leq \mathtt{suc}\ p \to \mathtt{suc}\ m \leq \mathtt{suc}\ p \]

Now we need a term/proof of \(\mathtt{suc}\ n \leq \mathtt{suc}\ p\), that is, \((\text{s≤s n≤p})\). Given that term, we now finally reach the term \(\text{≤-trans}\ (\mathtt{suc}\ m) \; (\mathtt{suc}\ n) \; (\mathtt{suc}\ p)\ (\text{s≤s m≤n})\ (\text{s≤s n≤p})\) whose type is:

As before, the inductive steps follows from the inductive hypothesis, for remember that in the inductive hypothesis we have the term \(\text{≤-trans}\ (m\; n \; p)\; \text{m≤n}\; \text{n≤p}\) whose type is \(m \leq p\). So if we apply the constructor \(\text{s≤s}\) to that term, we should get a term of type \(\mathtt{suc}\ m \leq \mathtt{suc}\ p\). Therefore, the term of the inductive hypothesis

\[ \text{≤-trans}\ (\mathtt{suc}\ m \; \mathtt{suc}\ n \; \mathtt{suc}\ p)\ (\text{s≤s m≤n})\ (\text{s≤s n≤p}) \]

\[ \text{s≤s}\ (\text{≤-trans}\ (m\; n \; p)\; \text{m≤n}\; \text{n≤p}) \]

Again, the notation becomes unwieldy with this explicit method, and that’s why the PLFA recommends the shorter method. In Agda code, the inductive step with the shorter method is proved as follows:

≤-trans (s≤s m≤n) (s≤s n≤p)  =  s≤s (≤-trans m≤n n≤p)

Antisymmetry

This property can be stated as the following logical proposition: if both \(m\leq n\) and \(n\leq m\) are true, then \(m\) and \(n\) are actually equal, that is, \(m \equiv n\). In constructive terms, the property means that if we can construct a term of both \(m \leq n\) and \(n \leq m\), then we can construct a term of the equality/identity type \(m \equiv n\).

≤-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 construction is by means of a function we call \(\text{≤-antisym}\), and we proceed by induction.

In the base case, using the longer method of explicit parameters and induction on the first variable, we set \(m\) to \(0\). Then \(\text{≤-antisym}\) first takes a term of \(0 \leq n\) and then a term of \(n \leq 0\). In both cases, that term is \(\text{z≤n}\). So we get \(\text{≤-antisym z≤n z≤n}\ : 0 \equiv 0\). What term is it that constitutes proof that a thing is equal to itself? That’s right: \(\mathtt{refl}\). Therefore, \(\text{≤-antisym z≤n z≤n}\) is \(\mathtt{refl}\).

Equivalently, we could shorten this by just considering the terms or proofs that \(m\leq n\) and \(n\leq m\) hold, which in the base case is \(\text{z≤n}\) for both.

The inductive hypothesis states that \(\text{≤-antisym m≤n n≤m}\) is the term/proof of \(m \equiv n\).

In the inductive step, we consider the terms or proofs for \(\mathtt{suc}\ m \leq \mathtt{suc}\ n\) and \(\mathtt{suc}\ n \leq \mathtt{suc}\ m\). The term for the first is \(\text{s≤s m≤n}\), and the term for the second is \(\text{s≤s n≤m}\). So we get the term \(\text{≤-antisym (s≤s m≤n) (s≤s n≤m)}\) whose type is \(\mathtt{suc}\ m \equiv \mathtt{suc}\ n\).

So if in the inductive hypothesis we have evidence of \(m\equiv n\), and in the inductive step we have evidence of \(\mathtt{suc}\ m \equiv \mathtt{suc}\ n\), then all we need to do now is apply the successor function \(\mathtt{suc}\) to the inductive hypothesis and we get the term \(\mathtt{suc}\ (\text{≤-antisym m≤n n≤m})\), which is congruent with \(\text{≤-antisym (s≤s m≤n) (s≤s n≤m)}\). Remember that congruence must be specified in the Agda code:

≤-antisym (s≤s m≤n) (s≤s n≤m)  =  cong suc (≤-antisym m≤n n≤m)

At least, this is how I understand it.↩︎