7 Equality

\(\newcommand{\la}{\lambda} \newcommand{\Ga}{\Gamma} \newcommand{\ra}{\rightarrow} \newcommand{\Ra}{\Rightarrow} \newcommand{\La}{\Leftarrow} \newcommand{\tl}{\triangleleft} \newcommand{\ir}[3]{\displaystyle\frac{#2}{#3}~{\textstyle #1}}\)

This chapter is a peek under the hood. In it, we see that the definition of propositional equality (≡) is just another inductive datatype. refl is the unique constructor of this datatype. An equivalent definition is used in Coq, but this is not the only possible definition of equality. Homotopy type theory (which people work on using both Agda and Coq) uses a more general idea.

Here’s the data definition.

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

Recall our discussion of structural, definitional, and propositional equality in the Naturals chapter. This definition takes Agda’s internal notion of definitional equality (two expressions are equal if they reduce to two structurally-equal expressions) and makes it available at the user level as propositional equality.

That seems straightforward enough, but just as the natural numbers are important enough to merit special treatment in the Agda implementation, the frequent use of equality in the kinds of logical reasoning we wish to do has resulted in some additional Agda features which takes some time to understand and appreciate.

7.1 Equality is an equivalence relation

There is only one constructor for equality, refl, so when we case-split on an equality, Agda will try to make the two sides equal through a process known as unification. This does not always succeed. For simple cases, such as an equality of the form y ≡ z, where y and z are variables, Agda will replace occurrences of z with y in the goal and context. In effect, it is doing a simple rewrite. But if y and z are replaced by expressions of even modest complexity, unification will often fail (the kind of problem it is trying to solve is undecidable in general).

We see unification at work in the interactive proofs of symmetry and transitivity of equality.

7.2 Congruence and substitution

We are now able to prove cong, which we previously imported from the Agda standard library. There are various forms of congruence theorems, and two are presented here: a version for functions of two variables, and one where the equality concerns the function rather than its arguments. Finally, there is a general substitution theorem, which says that if two things are equal, then any property of one is also a property of the other. With a suitable definition of "property", this can be used to do targetted rewrites (rewriting some occurrences rather than all).

7.3 Rewriting expanded

This section of PLFA explains dot patterns, though they did briefly appear earlier. It also explains Agda’s rewrite feature as syntactic sugar for a particular use of with. But we saw earlier that with was syntactic sugar for a particular use of a helper function. In other words, when we use rewrite, Agda must construct a special helper function to do the work, making use of unification. You can perhaps appreciate how this process might be brittle and might fail in complex situations. Sometimes we can "desugar" and adjust things manually. The subst function proved above can also be useful, though it can be awkward to use.

7.4 Leibniz equality

The material in PLFA on Leibniz equality and universe polymorphism is not needed in what follows, and is somewhat specialized. I am leaving it as optional reading. The main reason to do this reading is that the ideas may show up if you look at Agda source code written by experts (including the Agda standard library) and a little preparation will avoid you getting confused later.

Leibniz equality is the converse of the substitution theorem mentioned above: if two things have the same properties, then they are Leibniz-equal. Formalizing this in Agda introduces the need to have a hierarchy of sets. This goes back to the first attempts by Frege to formalize logic, and Russell’s paradox which poked a hole in it. Russell’s paradox can be described as follows: if we form the set of all sets that do not contain themselves, does that set contain itself or not? Either possibility leads to a contradiction.

The problem lies in permitting the construction "a set that contains itself". Russell’s stratified type theory, created to avoid the paradox, does not permit this. In Agda, the rule is that if something is formed by quantifying over Set, then the result cannot be in Set; it has to be in Set₁. This is the reason for the type signature of _≐_.

Here is an exposition of how allowing Set : Set (which can be done with a compiler flag or pragma in Agda) lets one prove the False proposition in Agda. I’ve put the link here for reference, but you’ll need to read through the Quantifiers chapter to be able to understand it, and it’s not necessary for you to read it.

http://liamoc.net/posts/2015-09-10-girards-paradox.html

The point is that there needs to be an infinite hierarchy of Set instances in Agda. (It isn’t absolutely necessary for it to be infinite, but cutting it off at some finite level ultimately limits what can be done.) It then follows that one might like to generalize ideas, such as equality, to arbitrary levels of the Set hierarchy. That is universe polymorphism, as discussed here in PLFA.

I have assigned no exercises for this chapter.