Equality part 1: definitional equality.

I keep meaning to write something about equality in Lean, and on the tube home today I just managed to understand it a little bit better, so perhaps now is the time (although I won’t get to today’s revelation until part 2).

My post on building the natural numbers from first principles , written when I had had been learning Lean for only a few months, is a popular post. I explain how the natural numbers are defined in Lean, and also how addition of natural numbers is defined. As mathematicians we do not think twice about the facts that $0 + n = n$ and $n + 0 = n$ , but in Lean these two equalities have a different status, because of the definition of addition.

The definition of addition in Lean is “by induction on the second variable” — or more precisely by recursion on the second variable. Every natural number is either $0$ , or the “successor” $S(n)$ of a previously-defined natural number. Lean defines $x+0$ to be $x$ , and if we have defined $x+n$ already, then Lean defines $x+S(n)$ to be $S(x+n)$ . If you like, we can now prove by induction that $x+y$ has been defined for all $x$ and $y$ , by induction on $y$ . Lean’s notation for $S(n)$ is succ n or more precisely nat.succ n .

I highlight “defines” in the preceding paragraph because we now see some examples of so-called “definitional equality”. The equality $x+0=x$ for $x$ a natural number is a definitional equality — it is true by definition. However the equality $0+x=x$ is certainly true, but it is not true by definition — it is true because of a theorem. Indeed, one proves $0 + x = x$ by induction on $x$ , as is done fairly early on in the post linked to above.

As a mathematician I never really had to distinguish between these two kinds of equality. However, when writing Lean code, it is a good idea to keep track of which equalities should be true by definition and which ones are true because of some extra content. One very simple reason for this is that if your goal is an equality which is true by definition, however complicated the definitions involved may be, there is every chance that Lean will be able to prove it using the refl tactic (or, in term mode, the rfl term). This might sound silly but it is absolutely not — several times in the past I found myself stuck trying to prove something which felt obvious to me but for which I could not find the right lemmas in Lean’s library to do the job, and then it was pointed out to me that refl would solve the goal.

Over the last few months I worked intensely on the perfectoid project and during this time I had to work with equivalence classes. I have a traditional model of equivalence classes in my head — if $S$ is a set and $\sim$ is an equivalence relation on $S$ then the set $Q$ of equivalence classes for $\sim$ is, by definition, a set of subsets of $S$ , equipped with the canonical map $S\to Q$ sending $s\in S$ to its equivalence class $[s]$ . It was Patrick Massot who pointed out to me that in some sense this construction is misleading — one does not really need $Q$ to be precisely this set, in fact the main thing one needs is the universal property for $Q$ , namely that if $f:S\to T$ is a function such that $s_1\sim s_2\implies f(s_1)=f(s_2)$ then $f$ descends to a function $\overline{f}: Q\to T$ satisfying $\overline{f}([s])=f(s)$ for all $s\in S$ . Now all this is in Lean of course, but its implementation was something which I always found mysterious until recently, for the reasons I shall now explain.

The first, completely dumb, thing is that the descent $\overline{f}$ of $f$ is called the lift of $f$ in Lean. This huge change of notation disoriented me for a long time. A related piece of notation: the universal property $\overline{f}([s])=f(s)$ mentioned above has a name — it’s called “the computation principle” in Lean — and I had never heard it being called this before, which was an obstruction to my understanding when people were talking about this sort of thing on the Lean Zulip chat.

The second reason was that whilst Lean is completely capable of forming subsets of $S$ and making them into a new type $Q$ , Lean did not use this approach at all, using instead a new quotient axiom to make $Q$ which is explicitly added to the system, and then a certain amount of fuss is made about it right the end of Theorem Proving In Lean. For a long time I could not see the point of this quotient axiom at all; the only thing it seemed to do was to provide a second method for making quotient types which was not the standard way taught in undergraduate mathematics classes.

However, when actually working with equivalence relations and equivalence classes in a technical setting, the penny finally dropped: the computational principle is a definitional equality. In other words, the proof that $\overline{f}([s])=f(s)$ is refl. This really does change your workflow in practice; indeed I was very excited on a few occasions that what looked like some very complicated goal involving quotients turned out to be provable with refl. To appreciate the power of this, imagine how one would go about defining $\overline{f}$ using the traditional approach. We have some equivalence class $C$ , which is non-empty by definition. We want to define $\overline{f}(C)$ . How do we do this? Well we apply the computer scientists’ axiom of choice, which gives us an element $c\in C$ , and then we just return $f(c)$ . Now it is certainly a theorem that $\overline{f}([s])=f(s)$ , however the chances are that the $c\in [s]$ that we chose was not $s$ , and the fact that $f(c)=f(s)$ is true because it is a theorem that $f$ is constant on equivalence classes! In particular, $\overline{f}([s])=f(s)$ would not be true by definition with this approach.

Definitional equality is a powerful tool. If $x=y$ is true by definition, and $h$ is a function, then $h(x)=h(y)$ is also true by definition. If however $x$ and $y$ are only equal because of a theorem, then one is going to have to use Lean’s rewrite tactic with the theorem to prove that $h(x)=h(y)$ and in particular one is going to have to do some work. Seeing a gigantic goal disappear completely with the proof being refl is very satisfying, and when I understood the difference between definitional equality and equality-because-of-a-theorem I realised that refl is a powerful tool for finishing proofs. In fact I have even claimed in the past that refl is my favourite tactic, although I guess on occasion I have to confess that ring can be pretty useful too…

2 Responses to Equality part 1: definitional equality.

Pingback: Equality part 2: syntactic equality | Xena
cvsec says:

November 27, 2021 at 12:36 am

It’s also worth noting that quotients in Lean aren’t a superfluous axiom that can be alternatively constructed at user level; this is because constructing them as subsets require the axiom of function extensionality, whereas in Lean it’s function extensionality that’s a theorem proved from the quotient construction.

LikeLike