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 and , 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 , or the “successor” of a previously-defined natural number. Lean defines to be , and if we have defined already, then Lean defines to be . If you like, we can now prove by induction that has been defined for all and , by induction on . Lean’s notation for 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 for a natural number is a definitional equality — it is true by definition. However the equality is certainly true, but it is not true by definition — it is true because of a theorem. Indeed, one proves by induction on , 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 is a set and is an equivalence relation on then the set of equivalence classes for is, by definition, a set of subsets of , equipped with the canonical map sending to its equivalence class . It was Patrick Massot who pointed out to me that in some sense this construction is misleading — one does not really need to be precisely this set, in fact the main thing one needs is the universal property for , namely that if is a function such that then descends to a function satisfying for all . 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 of is called the lift of in Lean. This huge change of notation disoriented me for a long time. A related piece of notation: the universal property 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 and making them into a new type , Lean did not use this approach at all, using instead a new quotient axiom to make 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 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 using the traditional approach. We have some equivalence class , which is non-empty by definition. We want to define . How do we do this? Well we apply the computer scientists’ axiom of choice, which gives us an element , and then we just return . Now it is certainly a theorem that , however the chances are that the that we chose was not , and the fact that is true because it is a theorem that is constant on equivalence classes! In particular, would not be true by definition with this approach.
Definitional equality is a powerful tool. If is true by definition, and is a function, then is also true by definition. If however and 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 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…
Pingback: Equality part 2: syntactic equality | Xena
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.