4.1 Definitional Equality

Definitional equality is the built-in notion of equality used by the kernel of Lean. Two expressions are definitionally equal when they reduce to the same normal form by computation. This reduction is automatic and does not require a proof term. In practice, this is the mechanism that allows many goals to close with rfl.

The reduction system includes several standard rules. Beta reduction applies when a function is applied to an argument. Delta reduction unfolds definitions. Iota reduction simplifies pattern matches by selecting the appropriate branch. Zeta reduction expands local let bindings. Together, these rules form the operational semantics that Lean uses during type checking.

A simple example illustrates the role of computation. Consider a definition:

def add1 (n : Nat) : Nat :=
  n + 1

Now examine the goal:

example : add1 2 = 3 := by
  rfl

The proof succeeds because add1 2 unfolds to 2 + 1, which computes to 3. Both sides reduce to the same normal form, so the kernel accepts rfl without further reasoning. No explicit rewriting step is needed.

Definitional equality also governs function application. If a function is defined by pattern matching, Lean reduces applications by selecting the matching branch. For example:

def isZero (n : Nat) : Bool :=
  match n with
  | 0     => true
  | _ + 1 => false

Then:

#eval isZero 0      -- true
#eval isZero 5      -- false

Inside proofs, the same computation applies. If a goal involves isZero 0, it reduces directly to true. This behavior is critical when designing definitions, since a well-chosen definition can eliminate the need for later rewriting.

Definitional equality is not symmetric with arbitrary rewriting. It is constrained by the reduction rules. If two expressions do not reduce to the same form, rfl will fail even if they are logically equal. For example:

example (a b : Nat) : a + b = b + a := by
  -- rfl fails
  admit

The expressions a + b and b + a do not reduce to the same normal form. This equality requires a propositional proof, not definitional equality.

A practical guideline is to design definitions so that expected equalities become definitional. For instance, defining functions in a way that exposes computation at the top level often allows rfl or simp to solve goals immediately. This reduces proof complexity and improves automation.

Another important aspect is transparency. Lean controls which definitions are unfolded during reduction. Some definitions are marked as reducible, others as semireducible or irreducible. This affects whether delta reduction applies automatically. In most basic developments, default transparency is sufficient, but performance and predictability can require explicit control.

Definitional equality also interacts with type inference. When Lean checks that a term has a given type, it allows the type to match up to definitional equality. This means that small differences in form are ignored if they compute to the same structure. This flexibility is essential for working with dependent types, where types themselves contain computations.

In summary, definitional equality is computation inside the type system. It removes the need for explicit proofs in many simple cases. Effective use of Lean depends on recognizing when computation is enough and when a propositional argument is required.