Skip to content

2.18 Naming Conventions

Names in Lean carry meaning.

lean proof-assistant type-theory logic proof-theory

Names in Lean carry meaning. They determine how easily a proof can be read, refactored, and extended. Good naming makes the structure of the argument visible without inspecting every term.

Problem

You want names that reflect the role of each hypothesis and intermediate result, instead of relying on generic placeholders like h, h1, h2.

Principles

Use names that encode:

  • the proposition or structure being described
  • the direction of implication
  • the relationship between objects

Prefer short but meaningful identifiers over long descriptive phrases.

Naming Hypotheses

For implications, include both source and target.

theorem naming_implication
    (P Q R : Prop)
    (hPQ : P -> Q)
    (hQR : Q -> R)
    (hp : P) :
    R := by
  exact hQR (hPQ hp)

The name hPQ indicates a map from P to Q. This avoids confusion in longer chains.

Bad:

(h1 : P -> Q) (h2 : Q -> R)

Good:

(hPQ : P -> Q) (hQR : Q -> R)

Naming Proofs of Propositions

Use the prefix h for hypotheses, followed by the proposition or role.

hp  : P
hq  : Q
hnp : ¬ P
hpq : P ∧ Q

For conjunctions:

rcases hpq with ⟨hp, hq⟩

The names match the components.

Naming Equalities

Use names that describe the relation.

hAB : a = b
hBC : b = c

Then:

rw [hAB, hBC]

reads naturally as a chain.

For properties:

hzero : n = 0
hsucc : n = k + 1

Avoid ambiguous names like h1, which do not indicate what is being rewritten.

Naming Existential Witnesses

For existentials, use a base name for the witness and a related name for its property.

rcases h with ⟨n, hn⟩

For multiple properties:

rcases h with ⟨n, hn₁, hn₂⟩

Or more descriptive:

rcases h with ⟨n, hn_eq, hn_bound⟩

The suffix indicates the meaning of each proof.

Naming in Case Analysis

Name each branch variable to reflect its origin.

cases h with
| inl hp =>
  ...
| inr hq =>
  ...

For natural numbers:

cases n with
| zero =>
  ...
| succ k =>
  ...

The name k indicates the predecessor.

Naming Intermediate Results

Use have with meaningful names.

have hq : Q := hPQ hp
have hr : R := hQR hq

The name should reflect the type. Avoid:

have h1 : Q := ...

unless the context is extremely small.

Naming Functions and Predicates

Use uppercase letters for propositions and predicates:

P Q R : Prop
P : α -> Prop

Use lowercase for values:

x y z : α
n m k : Nat

For functions:

f g : α -> β

When a function has a role, encode it:

next : Nat -> Nat
pred : Nat -> Nat

Naming with Indices

When several similar objects appear, use indexed names.

h₁ h₂ h₃

or:

hPQ₁ hPQ₂

Unicode subscripts are often clearer than numeric suffixes.

hp₁ hp₂

is preferable to:

hp1 hp2

Naming in Chains

For equality chains, maintain consistent naming.

hAB : a = b
hBC : b = c
hCD : c = d

This makes both rw and calc readable.

calc
  a = b := hAB
  _ = c := hBC
  _ = d := hCD

Naming Avoids Errors

Good naming prevents mistakes.

Bad:

rw [h1, h2]

You must inspect h1 and h2 to know what they do.

Good:

rw [hAB, hBC]

The direction and meaning are visible.

Naming and Refactoring

When proofs grow, names allow local changes.

have hq : Q := hPQ hp

If the proof of Q changes, only this line needs modification. The rest of the proof remains stable.

Unnamed intermediate expressions force you to rewrite multiple lines.

Naming for Readability

Compare:

exact h3 (h2 (h1 hp))

versus:

have hq : Q := hPQ hp
have hr : R := hQR hq
exact hRS hr

The second version is longer but explains the argument.

Naming for Patterns

Use consistent names across similar proofs.

For implication chains:

hPQ : P -> Q
hQR : Q -> R

For conjunction:

hp : P
hq : Q

For disjunction:

hp : P
hq : Q

For existentials:

x  : α
hx : P x

Consistency reduces cognitive load.

Naming Exceptions

Short names are acceptable when:

  • the proof is one or two lines
  • the meaning is obvious from context
  • the variable is used once

Example:

intro h
exact h

Here h is sufficient.

Common Patterns

Implication:

hPQ : P -> Q
hp  : P

Conjunction:

hpq : P ∧ Q
⟨hp, hq⟩

Disjunction:

cases h with
| inl hp => ...
| inr hq => ...

Existential:

⟨x, hx⟩

Equality:

hAB : a = b

Common Pitfalls

Do not reuse the same name for different meanings in the same scope.

Do not use names that conflict with Lean keywords or standard library identifiers.

Do not overuse single-letter names in long proofs.

Do not encode too much information into a name. hPQ_to_R_via_trans is harder to read than hPR.

Do not change naming conventions within the same file.

Takeaway

Names encode structure. Use them to reflect the logical role of each term: source and target for implications, components for conjunctions, branches for disjunctions, witnesses for existentials, and chains for equalities. Consistent naming turns a proof into a readable argument.