Definitional vs propositional equality

Question

Theorem Proving in Lean highlights a distinction between definitional and propositional equality when creating recursive functions:

The example above shows that the defining equations for add hold definitionally, and the same is true of mul. The equation compiler tries to ensure that this holds whenever possible, as is the case with straightforward structural induction. In other situations, however, reductions hold only propositionally, which is to say, they are equational theorems that must be applied explicitly.

This question describes the difference between the two (and clarifies that “definitional equality” is a synonym for “judgmental equality”)

When does a function definition require using propositional equality instead of definitional?

Does it impact the runtime of the function, or is it only a concern when proving?

(Edited to remove the duplication with the previous Q)

Answer 1

My understanding is that two terms are definitionally equal if they reduce to the same term via partial evaluation. With add defined as

def add : Nat → Nat → Nat
  | m, zero   => m
  | m, succ n => succ (add m n)

• add a 1 and succ a are definitionally equal, since add a 1 reduces to succ (add a 0) which reduces to succ a
• add a (add b 5) and add a (add (add b 3) 2) are definitionally equal, since they both reduce to succ (succ (succ (succ (succ (add a b)))))

There are cases where two terms are equal but don't reduce to the same term (so are not definitionally equal). This is propositional equality. For example:

• add a 1 and add 1 a are not definitionally equal: add a 1 reduces to succ a but add 1 a cannot be reduced any further because it depends on a
• Likewise, add a (add b c) and add (add a b) c are not definitionally equal

You can prove that the above examples are equal and define values add_1_sym : forall a, add a 1 = add 1 a and add_trans : forall a b c, add a (add b c) = add (add a b) c, and use those values in rewrite and simp tactics (e.g. you can substitute an instance of add a 1 with add 1 a or vice versa)

---

Another case where you need propositional equality is for extensional equality, like function extensionality (equality of functions with different bodies). Consider:

def add_rev : Nat -> Nat -> Nat
  | zero, n => n
  | succ m, n => succ (add_rev m n)

You can prove that add and add_rev are equal, using induction to prove that forall n m, add n m = add_rev n m. But you can never prove that two functions with different bodies are definitionally equal.

---

In general, definitional equality is preferred but propositional equality is more general:

• Solving an arbitrary equality proof with definitional equality is trivial (just reduce both terms and check they are the same), but solving an arbitrary equality proof with propositional equality means solving the Halting Problem; thus, the human must manually provide the relevant propositional equalities to the proof assistant.

• However, any terms which are definitionally equal are prepositionally equal (if a and b reduce to some c, a = b reduces to c = c which is always true). But not all propositionally equal terms are definitionally equal (see above examples)

As for runtime cost: two functions can be propositionally equal but have different runtimes, but if two terms are definitionally equal, a sensible compiler will constant-fold them into the same.