[Definitional equality - Metha](https://b-mehta.github.io/formalising-mathematics-notes/Part_1/equality.html#definitional-equality "Link to this heading") 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` and `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 `x` and `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`, and `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](https://adam.math.hhu.de/) 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=0` and `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`, `r` or `0 + r` are definitionally equal to each other. Tactics like `exact` and `rfl` work up to definitional equality. For example, the following proof works in Lean: example (x : ℕ) : x + 0 = x := by rfl which is perhaps not what you would expect if you have played the natural number game; I explicitly disabled this hack there. However the following does not work: example (x : ℕ) : 0 + x = x := by rfl -- type mismatch Similarly, this code works: example (x y : ℕ) (h : x + 0 = y) : x = y := by exact h because hypothesis `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 _definition_ of `not P` is `P → False`, so the `intro` tactic works here: example (P : Prop) : ¬ P := by intro h /- tactic state now P : Prop h : P ⊢ False -/ sorry (although the goal is of course not provable). The above text is copied from the **Equality** section of [[Formalising Mathematics - Metha]] <iframe src="https://b-mehta.github.io/formalising-mathematics-notes/Part_1/equality.html#definitional-equality":text=apply,-"%EF%83%81" width="100%" height="700px"></iframe> https://b-mehta.github.io/formalising-mathematics-notes/Part_1/equality.html#definitional-equality https://b-mehta.github.io/formalising-mathematics-notes/Part_1/equality.html#definitional-equality