“Syntactic equality is they look identical, definitional equality is they are the same, propositional equality is they turn out to be the same.” – Bhavik Mehta
As mathematicians we tend not to fuss too much about equality, at least at undergraduate level. When formalising mathematics in Lean’s type theory, it turns out that one has to think a bit more carefully about what is going on. In Lean there are three different kinds of equality which one has to be aware of, and the differences between them are “non-mathematical”. The strongest kind of equality is syntactic equality; this is the kind of equality that tactics like
simp care about. Then there is definitional equality; this is he kind of equality that tactics like
refl care about. Finally, there is propositional equality; this is the “usual” kind of equality as understood by mathematicians.
To give you a flavour of what this document is about, and in particular to indicate that these refined notions of equality are in some sense not “mathematical”, here is an example. Let x be a natural number. As mathematicians we would all agree that
0 + x = x and
x + 0 = x. Both of these are propositional equalities. However only one is a definitional equality, and neither of them are syntactic equalities.
Syntactic equality is the strongest kind of equality there is. Two expressions are syntactically equal if they are literally made by pressing the same keys on your keyboard in the same order.
x + 0 and
x + 0 are syntactically equal.
x + 0 and
x are not syntactically equal (even though they are mathematically equal).
rewrite tactic works at the syntactic equality level. For example, let’s say that your tactic state looks like this:
a b x : ℕ h : x + 0 = a ⊢ x = b
rw h will fail, even though
x + 0 = x. The reason it will fail is that
x + 0 and
x are not syntactically equal, so the
rw tactic will fail to find the left hand side of
h in the goal.
Definitional equality is a weaker kind of equality than syntactic equality – two things can sometimes be definitionally equal without being syntactically equal. A simple example is the following. In Lean,
¬P is notation for
not P, and
not P is defined to mean
P → false. So whilst
P → false are not syntactically equal, they are definitionally equal.
As the name suggests, definitional equality depends on definitions, and in particular depends on implementation details (that is, on exactly how things are defined under the hood). As such, definitional equality is in some sense “not a mathematical concept”. Here is an example to show you what I mean.
Addition on the natural numbers is defined “by induction”, or, more precisely, by recursion. If
y are natural numbers, then in the definition of
x + y we have to choose which one to induct on. The designers of Lean chose to induct on
y. This means that
x + 0 is defined to be
x + succ(y) is defined to be
succ(x + y).
This means that
x + 0 and
x are equal by the very definition of
+. To put it another way,
x + 0 and
x are definitionally equal.
However, players of the Natural number game will know, if we use this as the definition of addition, then to prove that
0 + x = x we need to use induction. The problem is that we cannot “unfold” the definition of
0 + x any further; the definition of
0 + x depends on whether
x = 0 or
x = succ(y) for some
y, so to make any progress in the proof of
0 + x = x we need to use more than just unfolding definitions; we need to use induction (to split into the cases
x=succ(y), when we can start simplifying
0 + x). As a result, although
0 + x = x is true, it is not definitionally true.
The fact that
x + 0 = x is a definitional equality, but
0 + x = x is not, means that definitional equality is in some sense not a mathematical concept. Furthermore, if the designers of Lean had decided to define addition by recursion on the first variable instead of the second, then of course our conclusions would be the other way around.
Note also: the fact that
x + 0 and
x are definitionally equal is specific to the natural numbers. Addition of real numbers is not defined by induction, it is defined in a far more complicated way using Cauchy sequences and quotients, and if
r : ℝ then none of
r + 0,
0 + r are definitionally equal to each other.
refl work up to definitional equality. For example, the following proof works:
example (x : ℕ) : x + 0 = x := begin refl end
which is perhaps not what you would expect if you have played the natural number game; I explicitly withhold this knowledge from the player (and occasionally get “bug reports” when people discover it). However the following does not work:
example (x : ℕ) : 0 + x = x := begin refl -- failed to unify 0 + x = x with ?m_2 = ?m_2 end
Similarly, this code works:
example (x y : ℕ) (h : x + 0 = y) : x = y := begin exact h, end
h is definitionally equal to the goal
x = y.
intro is another tactic which works up to definitional equality. If
P is a proposition, then
¬ P is notation for
not P, and the
not P is
P → false, so the
example (P : Prop) : ¬ P := begin intro h, /- tactic state now P : Prop h : P ⊢ false -/ sorry, end
(although the goal is of course not provable).
This is the weakest kind of equality, and the kind most familiar to mathematicians. Two terms
b are propositionally equal if you can prove
a = b, or equivalently if you can construct a term
h : a = b of type
a = b. For example, if
x is a natural then
x + 0,
0 + x and
x + 3 - 3 are all propositionally equal.
Appendix: syntactic equality again
What I said about syntactic equality is not strictly speaking true. The below paragraph fixes it, but can be ignored by everyone other then pedants.
There are actually a couple of ways that things can be syntactically equal without literally being made by pressing the same keys in the same order. Firstly, notation can be unfolded without breaking syntactic equality. For example the
= sign in
x = y is actually notation for the
eq function, and the terms
x = y and
eq x y are syntactically equal. Secondly, the names of globally quantified variables can change without breaking syntactical equality; for example
∃ x, x^2 = 4 and
∃ y, y^2 = 4 are syntactically equal.