Or: how I learnt to stop worrying, and figured out a proof that equality was an equivalence relation.
What is the definition of = ?
I used to teach a course where I defined the notion of what it meant for two integers to be congruent modulo N. Here N is an integer, and two integers a and b are said to be congruent modulo N if their difference is a multiple of N. For example, 37 and 57 are congruent modulo 10.
I would go on to prove that congruence modulo N is an equivalence relation on the integers. Reminder: an equivalence relation on X is a binary relation on X which is reflexive, symmetric and transitive. The proof I gave never assumed that N was non-zero, and congruence modulo 0 is the same relation as equality, so you might like to deduce from this that equality on the integers is an equivalence relation. Well, tough darts. In the proof that congruence modulo N is an equivalence relation, it turns out that we assume that equality is an equivalence relation, as you can readily check if you type it into a theorem prover.
So how do we prove that equality is an equivalence relation? In my 1st year undergraduate lecture notes this is stated as an “obvious example” of an equivalence relation. Euclid was more cautious — he explicitly noted that he would be assuming transitivity and reflexivity of equality in his common notions 1 and 4, and symmetry followed from his use of language — he would say “this collection of things are equal” e.g. “all right angles are equal”: so equality of two things was a predicate on unordered pairs for him, and symmetry was hence built in.
I also looked at my 3rd year logic and set theory notes, to try and figure out the definition of = , but they were also no help. There is some waffle about “the interpretation in a model is the diagonal of 
x = y means that the two terms x and y are actually the same term, but don’t get me started about what mathematicians mean when they say two things are “the same”, e.g. “the same proof” or “canonical isomorphism is denoted by =” or all the other highly useful and yet irritatingly non-rigorous stuff we say. Anyway, just “defining” equality to mean another word or phrase which is synonymous with equality isn’t going to get us anywhere. Ultimately my impression is that you might just assume that equality is an equivalence relation, when setting up mathematics via first order logic and ZFC set theory. I’m no logician though — feel free to correct me in the comments. This post is about a different way to approach things, which part of me finds a whole lot more satisfactory.
A definition of equality.
Lean’s type theory contains a definition of equality! This is great because it means we know where we stand. Here’s the definition:
inductive eq {X : Type} : X → X → Prop
| refl (a : X) : eq a a
infix ` = `:50 := eqWhat does all that baloney mean? Well, this is an inductive definition of a binary relation. Let X be a type or a set or however you want to think of a collection of stuff. The binary relation eq on X takes as input two things in X, call them a and b, and spits out a true-false statement eq a b. We’ll get to the definition in a second, but that last line means “the notation a = b is defined to mean eq a b, with BIDMAS-power 50”. Let’s use the = notation from now on instead of eq, because it’s familiar-looking.
So, let’s get to the heart of the matter: how do we define a = b? Well, Lean’s definition says the following: “there is only one tool we have to prove the equality of two things, and it’s the theorem refl a, which is a proof of the statement a = a. That’s it.” Thanks to Andrej Bauer who on Twitter pointed out that a neat way to think about this definition is: equality is the smallest binary relation which is reflexive. Andrej also tells me that this is Martin-Löf’s definition of equality.
OK great. We have now apparently defined the true-false statement a = b, and we can prove that a = a is true, so this is a good start. But how the heck are we going to go from this to symmetry and transitivity? We’re going to use induction!
Inductive types: a reminder
In my last post, I waffled on about inductive types. I was going to talk about equality in that post, but it had already got quite long, so I thought I’d deal with equality separately, and so here we are. The take home message from the last post was that if you define something as an inductive type in a type theory like Lean’s, then Lean automatically generates a new axiom in the system called the recursor for that type. This axiom is generated automatically by the rules of the calculus of inductive constructions. For example, if you define the natural numbers inductively using Peano’s axioms, then the recursor is just the statements that induction and recursion are true (propositions are types in Lean, so one function can be interpreted in two ways depending on whether you apply it in the Prop universe or the Type universe). The recursor attached to an inductive type is a way of saying “if you want to do something to every instance of the thing you’re defining, it suffices to do it for all the constructors”, and a special case of it is the “inductor”, which says, in our case, that if you want to deduce something from a = b then all you have to do is make sure you can prove it in the special case a = a. Formally, the inductor for = is the following statement:
eq.inductor (X : Type) (R : X → X → Prop)
(h : ∀ x, R x x) (a b : X) : a = b → R a bNote the fancy type theory R : X → X → Prop for what a mathematician would call “R is a binary relation on X” (reason: R : X → X → Prop means 
R on X such that R x x is true for all x, and if you know that a = b, then R a b is true. That’s the tool we have. Again let’s go back to Andrej’s observation: the definition of equality can be thought of as saying that it is the smallest (or the initial) binary relation which is reflexive, and the inductor then makes this rigorous by saying that any other reflexive binary relation must contain equality.
Summary : we are armed with two things, and two things only. (1) a proof of ∀ a, a = a and (2) a proof that if R is a binary relation on X and ∀ x, R x x is true, then a = b implies R a b.
The game now is to prove that = is symmetric and transitive, without accidentally assuming it! And what better framework to play that game in, than Lean! (because trust me, if you play it on paper, you are so going to mess this one up).
The equivalence relation game
Insert coin. That’s hard mode, i.e. spoiler-free. Copy and paste the code at the other end of that link into VS Code if you have Lean installed locally if you want a much speedier experience. The game is to prove symm and trans from refl and ind. I would work out the maths proofs first.
If you want no spoilers at all, stop reading now. I usually post some art generated by my children in my blog posts so perhaps now is a good time to do this. If you want to hear more about equality, and in particular have one or more hints and spoilers, read on.
Tactic hint alert
refine is a great tactic. It’s like apply on steroids. You can do everything with intros, apply, refine and exact. You can read about what these tactics do here, in Lean’s documentation. All Lean proofs can be done in just two or three lines.
Hint alert
Life is easier if we have more tools than just ind. The thing about ind is it wants as input a binary relation. A simpler object than a binary relation on X is a subset of X, or equivalently its characteristic function P : X → Prop (sending the elements of the subset to true and the other elements to false). Here’s something which you believe about equality: if a = b and P a is true, then P b is true. This is a much cleaner statement than ind — it’s just as powerful, and more flexible. Logicians call it the substitution property of equality. Applying it is the way Lean’s rewrite or rw tactic works. Why not try to prove it first? It makes the proof of trans much easier — it’s basically a master sword. Here’s the statement. Just cut and paste it before symm. Of course, you’ve got to prove it (using ind and refl).
theorem subst (hab : a ∼ b) (P : X → Prop) : P a → P b :=
begin
sorry
end
Xena 
Thanks to David Corfield on Twitter for pointing out these slides of Mike Shulman’s (at least, he claims they’re Shulman’s — the slides don’t have an author mentioned, but they’re hosted on Shulman’s website): https://home.sandiego.edu/~shulman/papers/induction.pdf . They contain everything here and some more too (including some good jokes), and of course written by an expert. Spoiler alert: they contain a proof of symm from ind. Note however the last page — “is yes!” should say “is no!” in Lean’s type theory. For me, this use of equality is going too far (we have a perfectly good concept of isomophism which does this job…)
LikeLike
They are definitely by Mike Shulman: there were two Mike’s teaching at Mathcamp one summer, and there is a Mathcamp tradition that one cannot have two staff members with the same name. So Mike Shulman became “Anti-Mike”, or Anti for short.
On an unrelated note, the Lean proofs suggested make use of tactics. But when proving such subtle things, we might wish to avoid tactic mode, as the tactics might be hiding the use of things that we don’t want to use to prove the results.
LikeLike
Yes, that’s me. Thanks for explaining the “name thing”, Julian (and hi!).
Ironically, more recently I’ve becomes somewhat disillusioned with this definition of equality. It’s fine for proving general properties of equality that apply to all types, like the fact that equality is an equivalence relation and satisfies substitution. (For some extra irony, in set-level mathematics that’s about it for general properties of equality — only in HoTT does equality on a general type have a richer structure that we can explore.)
But when working in practice with equality, the thing we need most often is that at specific types, equality has a specific characterization. For instance, two ordered pairs are equal iff their components are equal. Two functions are equal iff they take equal values on each input. Two natural numbers are equal iff they are both zero or they are both successors and their predecessors are equal. Two rational numbers a/b and c/d are equal iff the integers ad and bc are equal. Two integers mod n are equal if their difference as integers is divisible by n. And so on.
Some of these characterizations can be proven from the inductive definition of equality, but the proofs are not definitional and have to be transported across. And some of them (notably the one for functions) cannot be proven but have to be assumed axiomatically.
Thus, arguably, a better approach is to take these latter characterizations as definitions. One can then prove that equality thus-defined is an equivalence relation, and even satisfies the induction principle, by successively reducing more complicated types to simpler ones. Your example at the top of the post is an instance of this: once we know that equality of integers is an equivalence relation, we can deduce that equality of integers-mod-n is an equivalence relation. In turn, equality of integers can be reduced to equality of natural numbers (according to whatever your preferred definition of integers is), and the latter can be proven to be an equivalence relation by induction.
This approach was done formally for set-level mathematics in Observational Type Theory, although unfortunately, as far as I know, it was never completely implemented in a usable proof assistant. I’m currently working with Thorsten Altenkirch and Ambrus Kaposi on a Higher Observational Type Theory that will, we hope, achieve the same thing for HOTT. (Cubical type theories — including those for set-level mathematics, like XTT — are sort of a halfway point, incorporating some “observational” ideas while still defining identity types in a general way rather than specifically by type.)
LikeLike
As a fully paid up number theorist I have not really understood the importance of the difference between definitional and propositional equality. These induction gimmicks are kind of cool, but if you have an inductive type and your built-in recursor isn’t the right one, you can just make another one. The proofs I work on tend to be “propositional”, i.e. we do not rely on actual definitions and instead rely on a solid API and rewriting rather than proving things by `refl`. In short, I don’t care what Lean’s definition of the integers and rationals are, all I need is access to the relevant theorems (the integers are a ring, the rationals are a field etc).
LikeLike
I can understand that, but the question here is about foundations. If all you care about is knowing that equality is an equivalence relation, satisfies transport, and that equality of all particular types is what you want it to be, and you’re working at a set-level where the propositional/definitional distinction doesn’t come up much, then it shouldn’t matter to you whether equality is defined generally as an inductive type or computes on the structure of its type. I’m saying that once you lift the hood and start caring about how to prove all these things (which is sort of what this post was about, I thought — proving that equality is an equivalence relation), I now think it may be better to take the second approach.
LikeLike
Yes I understand your point 🙂 and thanks for making it!
LikeLike
What is “BIDMAS-power 50”??
LikeLike
You know that you do `*` and `/` before `+` and `-` because of a rule which in the UK we call BIDMAS or BODMAS and other people call PEMDAS? Well the *actual* rule is that symbols have a “binding power” which is some natural number, and you do the higher ones first. For example `+` has binding power 65 in Lean, and `*` has binding power 70, and brackets have binding power 1000. The `=` symbol has binding power 50 which is less than `+`, so `a + b = c` gets bracketed as `(a + b) = c` and not `a + (b = c)`.
LikeLike